From 2690a6ba8ff7998f8dbb778b93fa22976eadb4ac Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Sat, 21 Dec 2019 06:13:47 -0400 Subject: Properly track how the stack changes in the presence of discontinuities. --- stdlib/source/lux/target/jvm/bytecode.lux | 232 ++++++++++++++------- stdlib/source/lux/target/jvm/bytecode/address.lux | 8 +- .../source/lux/target/jvm/bytecode/environment.lux | 49 ++++- .../jvm/bytecode/environment/limit/stack.lux | 17 +- .../tool/compiler/phase/generation/jvm/runtime.lux | 25 +-- stdlib/source/test/lux/target/jvm.lux | 69 +++--- 6 files changed, 272 insertions(+), 128 deletions(-) (limited to 'stdlib') diff --git a/stdlib/source/lux/target/jvm/bytecode.lux b/stdlib/source/lux/target/jvm/bytecode.lux index 34e887bc1..5ad3d2204 100644 --- a/stdlib/source/lux/target/jvm/bytecode.lux +++ b/stdlib/source/lux/target/jvm/bytecode.lux @@ -9,7 +9,8 @@ ["." state (#+ State')] ["." function] ["." try (#+ Try)] - ["." exception (#+ exception:)]] + ["." exception (#+ exception:)] + ["." pipe (#+ when>)]] [data ["." product] ["." maybe] @@ -31,7 +32,8 @@ ["_" instruction (#+ Primitive-Array-Type Instruction Estimator) ("#@." monoid)] ["#." environment (#+ Environment) [limit - ["/." registry (#+ Register Registry)]]] + ["/." registry (#+ Register Registry)] + ["/." stack (#+ Stack)]]] ["/#" // #_ ["#." index (#+ Index)] [encoding @@ -50,7 +52,7 @@ (type: #export Label Nat) -(type: #export Resolver (Dictionary Label Address)) +(type: #export Resolver (Dictionary Label [Stack (Maybe Address)])) (type: #export Tracker {#program-counter Address @@ -110,18 +112,45 @@ (exception.report ["Label" (%.nat label)])) -(def: #export (set-label label) - (-> Label (Bytecode Any)) - (function (_ [pool environment tracker]) - (if (dictionary.contains? label (get@ #known tracker)) - (exception.throw ..label-has-already-been-set [label]) - (#try.Success [[pool - environment - (update@ #known - (dictionary.put label (get@ #program-counter tracker)) - tracker)] - [..relative-identity - []]])))) +(exception: #export (mismatched-environments {instruction Name} + {label Label} + {address Address} + {expected Stack} + {actual Stack}) + (exception.report + ["Instruction" (%.name instruction)] + ["Label" (%.nat label)] + ["Address" (/address.format address)] + ["Expected" (/stack.format expected)] + ["Actual" (/stack.format actual)])) + +(with-expansions [ (as-is (#try.Success [[pool + environment + (update@ #known + (dictionary.put label [actual (#.Some @here)]) + tracker)] + [..relative-identity + []]]))] + (def: #export (set-label label) + (-> Label (Bytecode Any)) + (function (_ [pool environment tracker]) + (let [@here (get@ #program-counter tracker)] + (case (dictionary.get label (get@ #known tracker)) + (#.Some [expected (#.Some address)]) + (exception.throw ..label-has-already-been-set [label]) + + (#.Some [expected #.None]) + (do try.monad + [[actual environment] (/environment.continue expected environment)] + ) + + #.None + (do try.monad + [[actual environment] (/environment.continue (|> environment + (get@ #/environment.stack) + (maybe.default /stack.empty)) + environment)] + )))))) (def: #export monad (Monad Bytecode) @@ -132,10 +161,9 @@ (: (Monad Try)) try.monad)) -(def: #export (fail error) +(def: #export fail (-> Text Bytecode) - (function (_ [pool environment tracker]) - (#try.Failure error))) + (|>> #try.Failure function.constant)) (def: #export (throw exception value) (All [e] (-> (exception.Exception e) e Bytecode)) @@ -191,6 +219,17 @@ [@4 5] ) +(def: discontinuity! + (Bytecode Any) + (function (_ [pool environment tracker]) + (do try.monad + [_ (/environment.stack environment)] + (#try.Success [[pool + (/environment.discontinue environment) + tracker] + [..relative-identity + []]])))) + (template [ ] [(def: #export (Bytecode Any) @@ -369,21 +408,29 @@ [dcmpl $4 $1 @_ _.dcmpl] [dcmpg $4 $1 @_ _.dcmpg] - [ireturn $1 $0 @_ _.ireturn] - [lreturn $2 $0 @_ _.lreturn] - [freturn $1 $0 @_ _.freturn] - [dreturn $2 $0 @_ _.dreturn] - [areturn $1 $0 @_ _.areturn] - [return $0 $0 @_ _.return] - [arraylength $1 $1 @_ _.arraylength] - [athrow $1 $0 @_ _.athrow] - [monitorenter $1 $0 @_ _.monitorenter] [monitorexit $1 $0 @_ _.monitorexit] ) +(template [ ] + [(def: #export + (Bytecode Any) + (do ..monad + [_ (..bytecode $0 @_ [])] + ..discontinuity!))] + + [ireturn $1 _.ireturn] + [lreturn $2 _.lreturn] + [freturn $1 _.freturn] + [dreturn $2 _.dreturn] + [areturn $1 _.areturn] + [return $0 _.return] + + [athrow $1 _.athrow] + ) + (def: #export (bipush byte) (-> U1 (Bytecode Any)) (..bytecode $0 $1 @_ _.bipush [byte])) @@ -597,12 +644,19 @@ (:: @ map (|>> #.Left) (//signed.s4 jump)) (:: @ map (|>> #.Right) (//signed.s2 jump)))))) +(exception: #export (unset-label {label Label}) + (exception.report + ["Label" (%.nat label)])) + (def: (resolve-label label resolver) - (-> Label Resolver (Try Address)) + (-> Label Resolver (Try [Stack Address])) (case (dictionary.get label resolver) - (#.Some address) - (#try.Success address) + (#.Some [actual (#.Some address)]) + (#try.Success [actual address]) + (#.Some [actual #.None]) + (exception.throw ..unset-label [label]) + #.None (exception.throw ..unknown-label [label]))) @@ -611,23 +665,32 @@ (-> Label (Bytecode Any)) (let [[estimator bytecode] ] (function (_ [pool environment tracker]) - (do try.monad - [environment' (|> environment - (/environment.consumes )) - program-counter' (step estimator (get@ #program-counter tracker))] - (wrap (let [@from (get@ #program-counter tracker)] - [[pool environment' (set@ #program-counter program-counter' tracker)] - [(function (_ resolver) - (do try.monad - [@to (..resolve-label label resolver) - jump (..jump @from @to)] - (case jump - (#.Left jump) - (exception.throw ..cannot-do-a-big-jump [label @from jump]) - - (#.Right jump) - (#try.Success [..no-exceptions (bytecode jump)])))) - []]]))))))] + (let [@here (get@ #program-counter tracker)] + (do try.monad + [environment' (|> environment + (/environment.consumes )) + actual (/environment.stack environment') + program-counter' (step estimator @here)] + (wrap (let [@from @here] + [[pool + environment' + (|> tracker + (when> [(get@ #known) (dictionary.contains? label) not] + [(update@ #known (dictionary.put label [actual #.None]))]) + (set@ #program-counter program-counter'))] + [(function (_ resolver) + (do try.monad + [[expected @to] (..resolve-label label resolver) + _ (exception.assert ..mismatched-environments [(name-of ) label @here expected actual] + (:: /stack.equivalence = expected actual)) + jump (..jump @from @to)] + (case jump + (#.Left jump) + (exception.throw ..cannot-do-a-big-jump [label @from jump]) + + (#.Right jump) + (#try.Success [..no-exceptions (bytecode jump)])))) + []]])))))))] [$1 ifeq _.ifeq] [$1 ifne _.ifne] @@ -655,14 +718,20 @@ (let [[estimator bytecode] _.goto] (function (_ [pool environment tracker]) (do try.monad - [program-counter' (step estimator (get@ #program-counter tracker))] - (wrap (let [@from (get@ #program-counter tracker)] - [[pool environment (set@ #program-counter program-counter' tracker)] + [#let [@here (get@ #program-counter tracker)] + program-counter' (step estimator @here)] + (wrap (let [@from @here] + [[pool + (/environment.discontinue environment) + (set@ #program-counter program-counter' tracker)] [(function (_ resolver) (case (dictionary.get label resolver) - (#.Some @to) + (#.Some [expected (#.Some @to)]) (do try.monad - [jump (..jump @from @to)] + [actual (/environment.stack environment) + _ (exception.assert ..mismatched-environments [(name-of _.goto) label @here expected actual] + (:: /stack.equivalence = expected actual)) + jump (..jump @from @to)] (case jump (#.Left jump) (exception.throw ..cannot-do-a-big-jump [label @from jump]) @@ -670,6 +739,9 @@ (#.Right jump) (#try.Success [..no-exceptions (bytecode jump)]))) + (#.Some [expected #.None]) + (exception.throw ..unset-label [label]) + #.None (exception.throw ..unknown-label [label]))) []]])))))) @@ -679,14 +751,20 @@ (let [[estimator bytecode] _.goto-w] (function (_ [pool environment tracker]) (do try.monad - [program-counter' (step estimator (get@ #program-counter tracker))] - (wrap (let [@from (get@ #program-counter tracker)] - [[pool environment (set@ #program-counter program-counter' tracker)] + [#let [@here (get@ #program-counter tracker)] + program-counter' (step estimator @here)] + (wrap (let [@from @here] + [[pool + (/environment.discontinue environment) + (set@ #program-counter program-counter' tracker)] [(function (_ resolver) (case (dictionary.get label resolver) - (#.Some @to) + (#.Some [expected (#.Some @to)]) (do try.monad - [jump (..jump @from @to)] + [actual (/environment.stack environment) + _ (exception.assert ..mismatched-environments [(name-of _.goto-w) label @here expected actual] + (:: /stack.equivalence = expected actual)) + jump (..jump @from @to)] (case jump (#.Left jump) (#try.Success [..no-exceptions (bytecode jump)]) @@ -694,6 +772,9 @@ (#.Right jump) (#try.Success [..no-exceptions (bytecode (/jump.lift jump))]))) + (#.Some [expected #.None]) + (exception.throw ..unset-label [label]) + #.None (exception.throw ..unknown-label [label]))) []]])))))) @@ -720,13 +801,17 @@ (wrap (let [@from (get@ #program-counter tracker)] [[pool environment' (set@ #program-counter program-counter' tracker)] [(function (_ resolver) - (let [get (: (-> Label (Maybe Address)) + (let [get (: (-> Label (Maybe [Stack (Maybe Address)])) (function (_ label) (dictionary.get label resolver)))] (case (do maybe.monad - [@default (get default) - @at-minimum (get at-minimum) - @afterwards (monad.map @ get afterwards)] + [[_ @default] (get default) + @default @default + [_ @at-minimum] (get at-minimum) + @at-minimum @at-minimum + @afterwards (|> afterwards + (monad.map @ get) + (monad.bind @ (monad.map @ product.right)))] (wrap [@default @at-minimum @afterwards])) (#.Some [@default @at-minimum @afterwards]) (do try.monad @@ -757,12 +842,15 @@ (wrap (let [@from (get@ #program-counter tracker)] [[pool environment' (set@ #program-counter program-counter' tracker)] [(function (_ resolver) - (let [get (: (-> Label (Maybe Address)) + (let [get (: (-> Label (Maybe [Stack (Maybe Address)])) (function (_ label) (dictionary.get label resolver)))] (case (do maybe.monad - [@default (get default) - @cases (monad.map @ (|>> product.right get) cases)] + [[_ @default] (get default) + @default @default + @cases (|> cases + (monad.map @ (|>> product.right get)) + (monad.bind @ (monad.map @ product.right)))] (wrap [@default @cases])) (#.Some [@default @cases]) (do try.monad @@ -785,8 +873,8 @@ [(def: #export ( class) (-> (Type ) (Bytecode Any)) (do ..monad - ## TODO: Make sure it's impossible to have indexes greater than U2. - [index (..lift (//constant/pool.class (//name.internal (..reflection class))))] + [## TODO: Make sure it's impossible to have indexes greater than U2. + index (..lift (//constant/pool.class (//name.internal (..reflection class))))] (..bytecode @_ [index])))] [$0 $1 new Class _.new] @@ -882,15 +970,19 @@ [@catch (..lift (//constant/pool.class (//name.internal (..reflection catch))))] (function (_ [pool environment tracker]) (#try.Success - [[pool environment tracker] + [[pool + environment + (|> tracker + (when> [(get@ #known) (dictionary.contains? @handler) not] + [(update@ #known (dictionary.put @handler [/stack.catch #.None]))]))] [(function (_ resolver) (do try.monad - [@start (..resolve-label @start resolver) - @end (..resolve-label @end resolver) + [[_ @start] (..resolve-label @start resolver) + [_ @end] (..resolve-label @end resolver) _ (if (/address.after? @start @end) (wrap []) (exception.throw ..invalid-range-for-try [@start @end])) - @handler (..resolve-label @handler resolver)] + [_ @handler] (..resolve-label @handler resolver)] (wrap [(row.row {#//exception.start @start #//exception.end @end #//exception.handler @handler diff --git a/stdlib/source/lux/target/jvm/bytecode/address.lux b/stdlib/source/lux/target/jvm/bytecode/address.lux index 4b58b1ca1..0af06f9e9 100644 --- a/stdlib/source/lux/target/jvm/bytecode/address.lux +++ b/stdlib/source/lux/target/jvm/bytecode/address.lux @@ -9,7 +9,9 @@ [format [binary (#+ Writer)]] [number - ["n" nat]]] + ["n" nat]] + [text + ["%" format (#+ Format)]]] [type abstract]] ["." // #_ @@ -65,4 +67,8 @@ (def: #export writer (Writer Address) (|>> :representation ///unsigned.writer/2)) + + (def: #export format + (Format Address) + (|>> :representation ///unsigned.value %.nat)) ) diff --git a/stdlib/source/lux/target/jvm/bytecode/environment.lux b/stdlib/source/lux/target/jvm/bytecode/environment.lux index 51927b96e..7ebacf5de 100644 --- a/stdlib/source/lux/target/jvm/bytecode/environment.lux +++ b/stdlib/source/lux/target/jvm/bytecode/environment.lux @@ -4,7 +4,8 @@ [monad (#+ do)] [monoid (#+ Monoid)]] [control - ["." try (#+ Try)]]] + ["." try (#+ Try)] + ["." exception (#+ exception:)]]] [/ ["/." limit (#+ Limit) ["/." stack (#+ Stack)] @@ -17,7 +18,7 @@ (type: #export Environment {#limit Limit - #stack Stack}) + #stack (Maybe Stack)}) (template [ ] [(def: #export ( type) @@ -25,7 +26,7 @@ (do try.monad [limit ( type)] (wrap {#limit limit - #stack /stack.empty})))] + #stack (#.Some /stack.empty)})))] [static /limit.static] [virtual /limit.virtual] @@ -45,25 +46,59 @@ [environment (left environment)] (right environment))))) +(exception: #export discontinuity) + +(def: #export (stack environment) + (-> Environment (Try Stack)) + (case (get@ #..stack environment) + (#.Some stack) + (#try.Success stack) + + #.None + (exception.throw ..discontinuity []))) + +(def: #export discontinue + (-> Environment Environment) + (set@ #..stack #.None)) + +(exception: #export (mismatched-stacks {expected Stack} + {actual Stack}) + (exception.report + ["Expected" (/stack.format expected)] + ["Actual" (/stack.format actual)])) + +(def: #export (continue expected environment) + (-> Stack Environment (Try [Stack Environment])) + (case (get@ #..stack environment) + (#.Some actual) + (if (:: /stack.equivalence = expected actual) + (#try.Success [actual environment]) + (exception.throw ..mismatched-stacks [expected actual])) + + #.None + (#try.Success [expected (set@ #..stack (#.Some expected) environment)]))) + (def: #export (consumes amount) (-> U2 Condition) ## TODO: Revisit this definition once lenses/optics have been implemented, ## since it can probably be simplified with them. (function (_ environment) (do try.monad - [stack' (/stack.pop amount (get@ #..stack environment))] - (wrap (set@ #..stack stack' environment))))) + [previous (..stack environment) + current (/stack.pop amount previous)] + (wrap (set@ #..stack (#.Some current) environment))))) (def: #export (produces amount) (-> U2 Condition) (function (_ environment) (do try.monad - [current (/stack.push amount (get@ #..stack environment)) + [previous (..stack environment) + current (/stack.push amount previous) #let [limit (|> environment (get@ [#..limit #/limit.stack]) (/stack.max current))]] (wrap (|> environment - (set@ #..stack current) + (set@ #..stack (#.Some current)) (set@ [#..limit #/limit.stack] limit)))))) (def: #export (has registry) diff --git a/stdlib/source/lux/target/jvm/bytecode/environment/limit/stack.lux b/stdlib/source/lux/target/jvm/bytecode/environment/limit/stack.lux index 87ad6a31b..fe72f79a5 100644 --- a/stdlib/source/lux/target/jvm/bytecode/environment/limit/stack.lux +++ b/stdlib/source/lux/target/jvm/bytecode/environment/limit/stack.lux @@ -6,6 +6,8 @@ ["." try (#+ Try)]] [data ["." maybe] + [text + ["%" format (#+ Format)]] [format [binary (#+ Writer)]]] [type @@ -19,9 +21,14 @@ U2 - (def: #export empty - Stack - (|> 0 /////unsigned.u2 maybe.assume :abstraction)) + (template [ ] + [(def: #export + Stack + (|> /////unsigned.u2 maybe.assume :abstraction))] + + [0 empty] + [1 catch] + ) (def: #export equivalence (Equivalence Stack) @@ -53,6 +60,10 @@ (:abstraction (/////unsigned.max/2 (:representation left) (:representation right)))) + + (def: #export format + (Format Stack) + (|>> :representation /////unsigned.value %.nat)) ) (def: #export length diff --git a/stdlib/source/lux/tool/compiler/phase/generation/jvm/runtime.lux b/stdlib/source/lux/tool/compiler/phase/generation/jvm/runtime.lux index c8076cada..f2349ff41 100644 --- a/stdlib/source/lux/tool/compiler/phase/generation/jvm/runtime.lux +++ b/stdlib/source/lux/tool/compiler/phase/generation/jvm/runtime.lux @@ -162,19 +162,18 @@ (def: (risky $unsafe) (-> (Bytecode Any) (Bytecode Any)) (do _.monad - [@from _.new-label - @to _.new-label + [@try _.new-label @handler _.new-label] ($_ _.compose - (_.try @from @to @handler //type.error) - (_.set-label @from) + (_.try @try @handler @handler //type.error) + (_.set-label @try) $unsafe ..some-injection _.areturn - (_.set-label @to) (_.set-label @handler) ..none-injection - _.areturn))) + _.areturn + ))) (def: decode-frac::name "decode_frac") (def: decode-frac::type (type.method [(list //type.text) //type.variant (list)])) @@ -189,7 +188,8 @@ ($_ _.compose ..this (_.invokestatic //type.frac "parseDouble" (type.method [(list //type.text) type.double (list)])) - (//value.wrap type.double)))))) + (//value.wrap type.double) + ))))) (def: #export log! (Bytecode Any) @@ -450,8 +450,7 @@ (list) (#.Some (do _.monad - [@from _.new-label - @to _.new-label + [@try _.new-label @handler _.new-label #let [$unsafe ..this unit _.aconst-null @@ -473,11 +472,10 @@ ## WTP )]] ($_ _.compose - (_.try @from @to @handler //type.error) - (_.set-label @from) + (_.try @try @handler @handler //type.error) + (_.set-label @try) $unsafe unit ..apply ..right-injection _.areturn - (_.set-label @to) (_.set-label @handler) ## T string-writer ## TW _.dup-x1 ## WTW @@ -520,8 +518,7 @@ left-projection::method right-projection::method - ..try::method - )) + ..try::method)) (row.row)))] (do ////.monad [_ (///.execute! class [class bytecode])] diff --git a/stdlib/source/test/lux/target/jvm.lux b/stdlib/source/test/lux/target/jvm.lux index 7b2283cb8..ab6cd5867 100644 --- a/stdlib/source/test/lux/target/jvm.lux +++ b/stdlib/source/test/lux/target/jvm.lux @@ -1314,14 +1314,16 @@ (function (_ goto) (<| (..bytecode (|>> (:coerce java/lang/Long) ("jvm leq" expected))) (do /.monad - [^value /.new-label - ^end /.new-label - _ (goto ^value) + [@skipped /.new-label + @value /.new-label + @end /.new-label + _ (goto @value) + _ (/.set-label @skipped) _ (..$Long::literal dummy) - _ (goto ^end) - _ (/.set-label ^value) + _ (goto @end) + _ (/.set-label @value) _ (..$Long::literal expected) - _ (/.set-label ^end)] + _ (/.set-label @end)] ..$Long::wrap))))]] ($_ _.and (_.lift "GOTO" (jump /.goto)) @@ -1339,17 +1341,17 @@ afterwards (:: @ map (n.% 10) random.nat)]) (..bytecode (|>> (:coerce java/lang/Long) ("jvm leq" expected))) (do /.monad - [^right /.new-label - ^wrong /.new-label - ^return /.new-label + [@right /.new-label + @wrong /.new-label + @return /.new-label _ (/.bipush (|> minimum /signed.value .nat /unsigned.u1 try.assume)) - _ (/.tableswitch minimum ^wrong [^right (list.repeat afterwards ^wrong)]) - _ (/.set-label ^wrong) + _ (/.tableswitch minimum @wrong [@right (list.repeat afterwards @wrong)]) + _ (/.set-label @wrong) _ (..$Long::literal dummy) - _ (/.goto ^return) - _ (/.set-label ^right) + _ (/.goto @return) + _ (/.set-label @right) _ (..$Long::literal expected) - _ (/.set-label ^return)] + _ (/.set-label @return)] ..$Long::wrap)) (<| (_.lift "LOOKUPSWITCH") (do random.monad @@ -1365,20 +1367,20 @@ dummy ..$Long::random]) (..bytecode (|>> (:coerce java/lang/Long) ("jvm leq" expected))) (do /.monad - [^right /.new-label - ^wrong /.new-label - ^return /.new-label + [@right /.new-label + @wrong /.new-label + @return /.new-label _ (..$Integer::literal (host.long-to-int choice)) - _ (/.lookupswitch ^wrong (list@map (function (_ option) + _ (/.lookupswitch @wrong (list@map (function (_ option) [(|> option /signed.s4 try.assume) - (if (i.= choice option) ^right ^wrong)]) + (if (i.= choice option) @right @wrong)]) options)) - _ (/.set-label ^wrong) + _ (/.set-label @wrong) _ (..$Long::literal dummy) - _ (/.goto ^return) - _ (/.set-label ^right) + _ (/.goto @return) + _ (/.set-label @right) _ (..$Long::literal expected) - _ (/.set-label ^return)] + _ (/.set-label @return)] ..$Long::wrap)) )) @@ -1392,23 +1394,24 @@ (..bytecode (|>> (:coerce java/lang/Long) ("jvm leq" expected))) (do /.monad [#let [$Exception (/type.class "java.lang.Exception" (list))] - ^start /.new-label - ^end /.new-label - ^handler /.new-label - ^return /.new-label - _ (/.try ^start ^end ^handler $Exception) - _ (/.set-label ^start) + @skipped /.new-label + @try /.new-label + @handler /.new-label + @return /.new-label + _ (/.try @try @handler @handler $Exception) + _ (/.set-label @try) _ (/.new $Exception) _ /.dup _ (..$String::literal exception) _ (/.invokespecial $Exception "" (/type.method [(list ..$String) /type.void (list)])) _ /.athrow + _ (/.set-label @skipped) _ (..$Long::literal dummy) - _ (/.goto ^return) - _ (/.set-label ^end) - _ (/.set-label ^handler) + _ (/.goto @return) + _ (/.set-label @handler) + _ /.pop _ (..$Long::literal expected) - _ (/.set-label ^return)] + _ (/.set-label @return)] ..$Long::wrap)))) (def: code -- cgit v1.2.3