diff --git a/flake.lock b/flake.lock index be75f57..09983e1 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1726560853, - "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", "owner": "numtide", "repo": "flake-utils", - "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", "type": "github" }, "original": { @@ -20,11 +20,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1729665710, - "narHash": "sha256-AlcmCXJZPIlO5dmFzV3V2XF6x/OpNWUV8Y/FMPGd8Z4=", + "lastModified": 1731676054, + "narHash": "sha256-OZiZ3m8SCMfh3B6bfGC/Bm4x3qc1m2SVEAlkV6iY7Yg=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "2768c7d042a37de65bb1b5b3268fc987e534c49d", + "rev": "5e4fbfb6b3de1aa2872b76d49fafc942626e2add", "type": "github" }, "original": { diff --git a/src/MiniWasm/Execution.hs b/src/MiniWasm/Execution.hs index cd7e221..06d049f 100644 --- a/src/MiniWasm/Execution.hs +++ b/src/MiniWasm/Execution.hs @@ -37,6 +37,8 @@ instance Label Lattice2 where Low `canFlowTo` High = True x `canFlowTo` y = x == y +instance (Show v, Label l) => Show (Labeled l v) where + show = showTCB -- Helper functions to manipulate MiniWasm values: @@ -99,14 +101,14 @@ data AdminInstr l Label { stackDepth :: Int -- The depth of the label's stack. This tells you how many values to 'take' from innerStack when exiting or branching out of the label. , continuation :: [Instr l] -- The instruction sequence to execute when branching out of this label. - , innerStack :: [Value] -- The inner stack of the label frame. + , innerStack :: [Labeled l Value] -- The inner stack of the label frame. , body :: [AdminInstr l] -- The instructions to execute inside this label (operating over the inner stack). } | -- Function call frame. Frame { resultsCount :: Int -- The number of outputs the function produces. This tells you how many values to 'take' from innerStack when returning from the function. - , innerLocals :: [Value] -- The local variables of this function call. - , innerStack :: [Value] -- The inner stack of this function call. + , innerLocals :: [Labeled l Value] -- The local variables of this function call. + , innerStack :: [Labeled l Value] -- The inner stack of this function call. , body :: [AdminInstr l] -- The instructions to execute as part of this function call (operating over the inner locals and inner stack). } | -- New administrative instructions: @@ -116,8 +118,8 @@ data AdminInstr l -- of a trap, return, or branch instruction. Trapping TrapReason -- The program is trapping. - | Breaking {target :: LabelIndex, values :: [Value]} -- The program is branching to label 'target' with args 'values'. - | Returning {results :: [Value]} -- The program is returning 'results' from a function. + | Breaking {target :: LabelIndex, values :: [Labeled l Value]} -- The program is branching to label 'target' with args 'values'. + | Returning {results :: [Labeled l Value]} -- The program is returning 'results' from a function. | Taint l -- Taint pc deriving Show @@ -140,6 +142,7 @@ data Config l = Config , instrs :: [AdminInstr l] -- Next instructions to be executed. , progcn :: l } + deriving Show -- The small-step evaluation function. -- @@ -166,32 +169,103 @@ step cfg = do -- You can directly pattern match on the stack too. -- The input program is validated before execution, so you can expect to find the right value types on the stack. (I32_BinOp op, b : a : stack) -> do - a' <- unlabel a - b' <- unlabel b - - v <- label (labelOf a `lub` labelOf b `lub` cfg.progcn) $ case (a', b') of - (V_I32 a'', V_I32 b'') -> V_I32 (evalBinOp op a'' b'') - (V_I64 a'', V_I64 b'') -> V_I64 (evalBinOp op a'' b'') - _ -> error "incompatiable binop" + V_I32 a' <- unlabel a + V_I32 b' <- unlabel b + v <- label (labelOf a `lub` labelOf b `lub` cfg.progcn) $ V_I32 (evalBinOp op a' b') return cfg{stack = v : stack, instrs} (I32_RelOp op, b : a : stack) -> do - a' <- unlabel a - b' <- unlabel b - - v <- label (labelOf a `lub` labelOf b `lub` cfg.progcn) $ case (a', b') of - (V_I32 a'', V_I32 b'') -> boolToI32 (evalRelOp op a'' b'') - (V_I64 a'', V_I64 b'') -> boolToI32 (evalRelOp op a'' b'') - _ -> error "incompatiable binop" + V_I32 a' <- unlabel a + V_I32 b' <- unlabel b + v <- label (labelOf a `lub` labelOf b `lub` cfg.progcn) $ boolToI32 (evalRelOp op a' b') + return cfg{stack = v : stack, instrs} + + (I64_BinOp op, b : a : stack) -> do + V_I64 a' <- unlabel a + V_I64 b' <- unlabel b + v <- label (labelOf a `lub` labelOf b `lub` cfg.progcn) $ V_I64 (evalBinOp op a' b') return cfg{stack = v : stack, instrs} - _ -> error "Missing or ill-typed operand(s) on the stack" + (I64_RelOp op, b : a : stack) -> do + V_I64 a' <- unlabel a + V_I64 b' <- unlabel b + v <- label (labelOf a `lub` labelOf b `lub` cfg.progcn) $ boolToI32 (evalRelOp op a' b') + return cfg{stack = v : stack, instrs} + + (LocalGet ix, stack) -> return cfg{stack = cfg.locals !! ix : stack, instrs} + (LocalSet ix, x : stack) -> return cfg{stack, instrs, locals = fromJust (updateAt ix x cfg.locals)} + + (Block (Params params) (Results results) body, stack) -> do + return cfg + { stack = drop (length params) stack + , instrs = + Label + { stackDepth = length results + , continuation = [] + , innerStack = take (length params) stack + , body = map Plain body + } + : instrs + } + + (Loop (Params params) (Results results) body, stack) -> do + return cfg + { stack = drop (length params) stack + , instrs = + Label + { stackDepth = length results + , continuation = [Loop (Params params) (Results results) body] + , innerStack = take (length params) stack + , body = map Plain body + } + : instrs + } + + + (Br ix, stack) -> return cfg{instrs = Breaking ix stack : instrs} + (BrIf ix, x : stack) -> do + x' <- unlabel x + case x' of + V_I32 0 -> return cfg{instrs, stack} + _ -> return cfg{instrs = Plain (Br ix) : instrs, stack} + + (Call fn, stack) -> do + vals <- mapM (label cfg.progcn . defaultValue) func.locals.unwrap + return cfg{instrs=Frame m (take n stack ++ vals) [] body : instrs, stack = drop n stack} + where + func = fromJust $ lookup fn cfg.funcs + n = length func.params.unwrap + m = length func.results.unwrap + body = map Plain func.body + + (Return, stack) -> return cfg{instrs = Returning stack : instrs} + + x -> error $ "Missing or ill-typed operand(s) on the stack\n" ++ show x -- Administrative instructions: Taint l -> return cfg{instrs, progcn = l} - _ -> error "instruction unknown" + Trapping msg -> return cfg{instrs = [Trapping msg]} + Breaking ix vs -> error "Breaking when not inside a label" + Returning vs -> error "Returning when not inside a frame" + Label n k vs [] -> return cfg{stack = take n vs, instrs = []} + Label n k vs (Trapping msg : _) -> return cfg{instrs=[Trapping msg]} + Label n k vs (Returning vs' : _) -> return cfg{instrs=Returning vs':instrs} + Label n k vs (Breaking 0 vs' : _) -> return cfg{instrs = map Plain k ++ instrs, stack = take n vs'} + Label n k vs (Breaking ix vs' : _) -> return cfg{instrs = Breaking (ix-1) vs' : instrs} + Label n k vs (e : es) -> do + cfg' <- step cfg{stack=vs, instrs=e:es} + return cfg'{stack=cfg.stack, instrs=(Label n k cfg'.stack cfg'.instrs) : instrs} + + Frame n locs vs [] | n == length vs -> return cfg{stack=vs ++ cfg.stack, instrs} + | otherwise -> error "Implicit return with not exactly the same number of arguments" + Frame n locs vs (Trapping msg : _) -> return cfg{instrs=[Trapping msg]} + Frame n locs vs (Returning vs' : _) -> return cfg{stack=(take n vs') ++ cfg.stack, instrs} + Frame n locs vs es -> do + cfg' <- step cfg{stack=vs, instrs=es, locals=locs} + return cfg'{stack=cfg.stack, instrs=(Frame n cfg'.locals cfg'.stack cfg'.instrs):instrs, locals=cfg.locals} +-- "Drop" test1 :: LIO Lattice2 (Config Lattice2) test1 = do l1 <- label Low (V_I32 1) @@ -199,16 +273,104 @@ test1 = do let config = Config [] [] [] [l1, l0] [Plain Drop, Plain Drop] Low stepUntilFinal config +-- "Add" test2 :: LIO Lattice2 (Config Lattice2) test2 = do let config = Config [] [] [] [] [Plain $ I32_Const 6, Taint High, Plain $ I32_Const 7, Plain $ I32_BinOp Add] Low stepUntilFinal config -test3 :: LIO Lattice2 (Config Lattice2) +-- "Relop" +test3 :: LIO Lattice2 (Config Lattice2) test3 = do let config = Config [] [] [] [] [Plain $ I32_Const 6, Taint High, Plain $ I32_Const 7, Plain $ I32_RelOp Lt] Low stepUntilFinal config +-- "LocalGet" +test4 :: LIO Lattice2 (Config Lattice2) +test4 = do + l7 <- label Low (V_I32 7) + let config = Config [] [] [l7] [] [Plain (LocalGet 0)] Low + stepUntilFinal config + +-- "Add64" +test5 :: LIO Lattice2 (Config Lattice2) +test5 = do + let config = Config [] [] [] [] [Plain (I64_Const 2), Plain (I64_Const 3), Plain (I64_BinOp Add)] Low + stepUntilFinal config + +-- "LocalSet" +test6 :: LIO Lattice2 (Config Lattice2) +test6 = do + l0 <- label Low (V_I32 0) + let config = Config [] [] [l0] [] [Plain (I32_Const 1), Plain (LocalSet 0)] Low + stepUntilFinal config + +-- "Block" +test7 :: LIO Lattice2 (Config Lattice2) +test7 = do + l5 <- label Low (V_I32 5) + lI32 <- label Low I32 + stepUntilFinal $ Config [] [] [] [l5] [Plain (Block (Params [lI32]) (Results [lI32]) [I32_Const 1, I32_BinOp Add])] Low + +-- "Loop" +test8 :: LIO Lattice2 (Config Lattice2) +test8 = do + l5 <- label Low (V_I32 5) + lI32 <- label Low I32 + stepUntilFinal $ Config [] [] [] [l5] [Plain (Loop (Params [lI32]) (Results [lI32]) [I32_Const 1, I32_BinOp Add])] Low + +-- "BrIf-Block" +test9 :: LIO Lattice2 (Config Lattice2) +test9 = do + l5 <- label Low (V_I32 5) + lI32 <- label Low I32 + stepUntilFinal $ Config [] [] [l5] [] [Plain (Block (Params []) (Results []) [LocalGet 0, I32_Const 1, I32_BinOp Sub, LocalSet 0, LocalGet 0, I32_Const 0, I32_RelOp Gt, BrIf 0, Unreachable])] Low + +-- "BrIf-Loop" +test10 :: LIO Lattice2 (Config Lattice2) +test10 = do + let l = Loop (Params []) (Results []) [LocalGet 0, I32_Const 1, I32_BinOp Sub, LocalSet 0, LocalGet 0, I32_Const 0, I32_RelOp Gt, BrIf 0] + l2 <- label Low (V_I32 2) + stepUntilFinal $ Config [] [] [l2] [] [Plain l] Low + +-- "Label-Nested" +test11 :: LIO Lattice2 (Config Lattice2) +test11 = do + lI32 <- label Low I32 + stepUntilFinal $ Config [] [] [] [] [Plain (Block (Params []) (Results [lI32]) [Block (Params []) (Results [lI32, lI32]) [I32_Const 5, I32_Const 6, I32_Const 7, BrIf 1]])] Low + +-- "Label-Mutates-Locals" +test12 :: LIO Lattice2 (Config Lattice2) +test12 = do + l4 <- label Low (V_I32 4) + l5 <- label Low (V_I32 5) + stepUntilFinal $ Config [] [] [l5] [] [Label 0 [] [l4] [Plain (LocalSet 0), Plain (LocalGet 0)]] Low + +-- "Call" +test13 :: LIO Lattice2 (Config Lattice2) +test13 = do + lI32 <- label Low I32 + l7 <- label Low (V_I32 7) + l5 <- label Low (V_I32 5) + let f = [("f", Func "f" (Params [lI32]) (Results [lI32]) (Locals []) [LocalGet 0, I32_Const 1, I32_BinOp Add])] + stepUntilFinal $ Config f [] [l7] [] [Plain (I32_Const 5), Plain (Call "f"), Plain (LocalGet 0), Plain (I32_BinOp Add)] Low + +-- "Return" +test14 :: LIO Lattice2 (Config Lattice2) +test14 = do + lI32 <- label Low I32 + let f = [("f", Func "f" (Params [lI32]) (Results [lI32]) (Locals []) [LocalGet 0, I32_Const 1, I32_BinOp Add, Return, Unreachable])] + stepUntilFinal $ Config f [] [] [] [Plain (I32_Const 5), Plain (Call "f")] Low + +-- "Frame-Nested" +test15 :: LIO Lattice2 (Config Lattice2) +test15 = do + lI32 <- label Low I32 + let f = Func "f" (Params [lI32]) (Results [lI32]) (Locals []) [LocalGet 0, Block (Params [lI32]) (Results [lI32]) [I32_Const 1, I32_BinOp Add, Call "g", I32_Const 1, I32_BinOp Add]] + g = Func "g" (Params [lI32]) (Results [lI32]) (Locals []) [Block (Params []) (Results [lI32]) [LocalGet 0, I32_Const 1, I32_BinOp Add, Br 0, Unreachable]] + fns = [("f", f), ("g", g)] + stepUntilFinal $ Config fns [] [] [] [Plain (I32_Const 5), Plain (Call "f"), Plain Drop] Low + sample :: LIO Lattice2 (Config Lattice2) -> IO () sample ex = do putStrLn "Running with state Low and clearance High" @@ -217,7 +379,7 @@ sample ex = do y <- evalLIO ex state putStrLn "Final stack:" - print $ map showTCB y.stack + print y return () diff --git a/src/MiniWasm/Syntax.hs b/src/MiniWasm/Syntax.hs index 841c6e7..15e7cd8 100644 --- a/src/MiniWasm/Syntax.hs +++ b/src/MiniWasm/Syntax.hs @@ -88,6 +88,7 @@ data Func l = , locals :: Locals -- The types of the function's local variables. , body :: [Instr l] -- The body of the function. } + deriving Show -- MiniWasm modules ("programs"). data Module l = diff --git a/src/MiniWasm/TestCases/SmallStep.hs b/src/MiniWasm/TestCases/SmallStep.hs index 6255d4d..8351ffe 100644 --- a/src/MiniWasm/TestCases/SmallStep.hs +++ b/src/MiniWasm/TestCases/SmallStep.hs @@ -2,6 +2,7 @@ module MiniWasm.TestCases.SmallStep where import MiniWasm.Execution import MiniWasm.Syntax +import LIO (~>) :: a -> b -> (a, b) (~>) = (,) @@ -17,187 +18,198 @@ infixr 5 ~> -- You can add your own or modify them, but be careful: Unlike the full program tests, these Configs -- are not validated before being executed. If you add an invalid config, it will crash with an -- unhelpful error like "ill-typed operands on the stack". -{- -smallStepTests :: [(String, [Config])] -smallStepTests = - [ "Nop" - ~> [ Config [] [] [] [] [Plain Nop] - , Config [] [] [] [] [] - ] - , "Drop" - ~> [ Config [] [] [] [V_I32 1, V_I32 0] [Plain Drop, Plain Drop] - , Config [] [] [] [V_I32 0] [Plain Drop] - , Config [] [] [] [] [] - ] - , "Unreachable" - ~> [ Config [] [] [] [] [Plain Unreachable] - , Config [] [] [] [] [Trapping UnreachableExecuted] - ] - , "Add" - ~> [ Config [] [] [] [] [Plain (I32_Const 2), Plain (I32_Const 3), Plain (I32_BinOp Add)] - , Config [] [] [] [V_I32 2] [Plain (I32_Const 3), Plain (I32_BinOp Add)] - , Config [] [] [] [V_I32 3, V_I32 2] [Plain (I32_BinOp Add)] - , Config [] [] [] [V_I32 5] [] - ] - , "Add64" - ~> [ Config [] [] [] [] [Plain (I64_Const 2), Plain (I64_Const 3), Plain (I64_BinOp Add)] - , Config [] [] [] [V_I64 2] [Plain (I64_Const 3), Plain (I64_BinOp Add)] - , Config [] [] [] [V_I64 3, V_I64 2] [Plain (I64_BinOp Add)] - , Config [] [] [] [V_I64 5] [] - ] - ]-} - {- - , "LocalGet" - ~> [ Config [] [] [V_I32 7] [] [Plain (LocalGet 0)] - , Config [] [] [V_I32 7] [V_I32 7] [] - ] - , "LocalSet" - ~> [ Config [] [] [V_I32 0] [] [Plain (I32_Const 1), Plain (LocalSet 0)] - , Config [] [] [V_I32 0] [V_I32 1] [Plain (LocalSet 0)] - , Config [] [] [V_I32 1] [] [] - ] - , "MemSize" - ~> [ Config [] [1 .. 10] [] [] [Plain MemSize] - , Config [] [1 .. 10] [] [V_I32 10] [] - ] - , "MemLoad" - ~> [ Config [] [1 .. 10] [] [] [Plain (I32_Const 2), Plain I32_Load, Plain (I32_Const 4), Plain I32_Load, Plain (I32_Const 5), Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] - , Config [] [1 .. 10] [] [V_I32 2] [Plain I32_Load, Plain (I32_Const 4), Plain I32_Load, Plain (I32_Const 5), Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] - , Config [] [1 .. 10] [] [V_I32 3] [Plain (I32_Const 4), Plain I32_Load, Plain (I32_Const 5), Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] - , Config [] [1 .. 10] [] [V_I32 4, V_I32 3] [Plain I32_Load, Plain (I32_Const 5), Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] - , Config [] [1 .. 10] [] [V_I32 5, V_I32 3] [Plain (I32_Const 5), Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] - , Config [] [1 .. 10] [] [V_I32 5, V_I32 5, V_I32 3] [Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] - , Config [] [1 .. 10] [] [V_I32 6, V_I32 5, V_I32 3] [Plain (I32_Const 10), Plain I32_Load] - , Config [] [1 .. 10] [] [V_I32 10, V_I32 6, V_I32 5, V_I32 3] [Plain I32_Load] - , Config [] [1 .. 10] [] [V_I32 6, V_I32 5, V_I32 3] [Trapping MemoryOutOfBounds] - ] - , "MemStore" - ~> [ Config [] [1, 2, 3] [] [] [Plain (I32_Const 1), Plain (I32_Const 5), Plain I32_Store, Plain (I32_Const 3), Plain (I32_Const 6), Plain I32_Store] - , Config [] [1, 2, 3] [] [V_I32 1] [Plain (I32_Const 5), Plain I32_Store, Plain (I32_Const 3), Plain (I32_Const 6), Plain I32_Store] - , Config [] [1, 2, 3] [] [V_I32 5, V_I32 1] [Plain I32_Store, Plain (I32_Const 3), Plain (I32_Const 6), Plain I32_Store] - , Config [] [1, 5, 3] [] [] [Plain (I32_Const 3), Plain (I32_Const 6), Plain I32_Store] - , Config [] [1, 5, 3] [] [V_I32 3] [Plain (I32_Const 6), Plain I32_Store] - , Config [] [1, 5, 3] [] [V_I32 6, V_I32 3] [Plain I32_Store] - , Config [] [1, 5, 3] [] [] [Trapping MemoryOutOfBounds] - ] - , "Block" - ~> [ Config [] [] [] [V_I32 5] [Plain (Block (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add])] - , Config [] [] [] [] [Label 1 [] [V_I32 5] ([Plain (I32_Const 1), Plain (I32_BinOp Add)])] - , Config [] [] [] [] [Label 1 [] [V_I32 1, V_I32 5] ([Plain (I32_BinOp Add)])] - , Config [] [] [] [] [Label 1 [] [V_I32 6] ([])] - , Config [] [] [] [V_I32 6] [] - ] - , "Loop" - ~> [ Config [] [] [] [V_I32 5] [Plain (Loop (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add])] - , Config [] [] [] [] [Label 1 [Loop (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add]] [V_I32 5] ([Plain (I32_Const 1), Plain (I32_BinOp Add)])] - , Config [] [] [] [] [Label 1 [Loop (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add]] [V_I32 1, V_I32 5] ([Plain (I32_BinOp Add)])] - , Config [] [] [] [] [Label 1 [Loop (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add]] [V_I32 6] ([])] - , Config [] [] [] [V_I32 6] [] - ] - , "BrIf-Block" - ~> [ Config [] [] [V_I32 5] [] [Plain (Block (Params []) (Results []) [LocalGet 0, I32_Const 1, I32_BinOp Sub, LocalSet 0, LocalGet 0, I32_Const 0, I32_RelOp Gt, BrIf 0, Unreachable])] - , Config [] [] [V_I32 5] [] [Label 0 [] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] - , Config [] [] [V_I32 5] [] [Label 0 [] [V_I32 5] [Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] - , Config [] [] [V_I32 5] [] [Label 0 [] [V_I32 1, V_I32 5] [Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] - , Config [] [] [V_I32 5] [] [Label 0 [] [V_I32 4] [Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] - , Config [] [] [V_I32 4] [] [Label 0 [] [] [Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] - , Config [] [] [V_I32 4] [] [Label 0 [] [V_I32 4] [Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] - , Config [] [] [V_I32 4] [] [Label 0 [] [V_I32 0, V_I32 4] [Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] - , Config [] [] [V_I32 4] [] [Label 0 [] [V_I32 1] [Plain (BrIf 0), Plain Unreachable]] - , Config [] [] [V_I32 4] [] [Label 0 [] [] [Plain (Br 0), Plain Unreachable]] - , Config [] [] [V_I32 4] [] [Label 0 [] [] [Breaking 0 [], Plain Unreachable]] - , Config [] [] [V_I32 4] [] [] - ] - , "BrIf-Loop" - ~> let l = Loop (Params []) (Results []) [LocalGet 0, I32_Const 1, I32_BinOp Sub, LocalSet 0, LocalGet 0, I32_Const 0, I32_RelOp Gt, BrIf 0] - in [ Config [] [] [V_I32 2] [] [Plain l] - , Config [] [] [V_I32 2] [] [Label 0 [l] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 2] [] [Label 0 [l] [V_I32 2] [Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 2] [] [Label 0 [l] [V_I32 1, V_I32 2] [Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 2] [] [Label 0 [l] [V_I32 1] [Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 1] [] [Label 0 [l] [] [Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 1] [] [Label 0 [l] [V_I32 1] [Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 1] [] [Label 0 [l] [V_I32 0, V_I32 1] [Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 1] [] [Label 0 [l] [V_I32 1] [Plain (BrIf 0)]] - , Config [] [] [V_I32 1] [] [Label 0 [l] [] [Plain (Br 0)]] - , Config [] [] [V_I32 1] [] [Label 0 [l] [] [Breaking 0 []]] - , Config [] [] [V_I32 1] [] [Plain l] - , Config [] [] [V_I32 1] [] [Label 0 [l] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 1] [] [Label 0 [l] [V_I32 1] [Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 1] [] [Label 0 [l] [V_I32 1, V_I32 1] [Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 1] [] [Label 0 [l] [V_I32 0] [Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 0] [] [Label 0 [l] [] [Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 0] [] [Label 0 [l] [V_I32 0] [Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 0] [] [Label 0 [l] [V_I32 0, V_I32 0] [Plain (I32_RelOp Gt), Plain (BrIf 0)]] - , Config [] [] [V_I32 0] [] [Label 0 [l] [V_I32 0] [Plain (BrIf 0)]] - , Config [] [] [V_I32 0] [] [Label 0 [l] [] []] - , Config [] [] [V_I32 0] [] [] - ] - , "Label-Nested" - ~> [ Config [] [] [] [] [Plain (Block (Params []) (Results [I32]) [Block (Params []) (Results [I32, I32]) [I32_Const 5, I32_Const 6, I32_Const 7, BrIf 1]])] - , Config [] [] [] [] [Label 1 [] [] [Plain (Block (Params []) (Results [I32, I32]) [I32_Const 5, I32_Const 6, I32_Const 7, BrIf 1])]] - , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [] [Plain (I32_Const 5), Plain (I32_Const 6), Plain (I32_Const 7), Plain (BrIf 1)]]] - , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [V_I32 5] [Plain (I32_Const 6), Plain (I32_Const 7), Plain (BrIf 1)]]] - , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [V_I32 6, V_I32 5] [Plain (I32_Const 7), Plain (BrIf 1)]]] - , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [V_I32 7, V_I32 6, V_I32 5] [Plain (BrIf 1)]]] - , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [V_I32 6, V_I32 5] [Plain (Br 1)]]] - , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [V_I32 6, V_I32 5] [Breaking 1 [V_I32 6, V_I32 5]]]] - , Config [] [] [] [] [Label 1 [] [] [Breaking 0 [V_I32 6, V_I32 5]]] - , Config [] [] [] [V_I32 6] [] - ] - , "Label-Mutates-Locals" - ~> [ Config [] [] [V_I32 5] [] [Label 0 [] [V_I32 4] [Plain (LocalSet 0), Plain (LocalGet 0)]] - , Config [] [] [V_I32 4] [] [Label 0 [] [] [Plain (LocalGet 0)]] - ] - , "Call" - ~> let f = [("f", Func "f" (Params [I32]) (Results [I32]) (Locals []) [LocalGet 0, I32_Const 1, I32_BinOp Add])] - in [ Config f [] [V_I32 7] [] [Plain (I32_Const 5), Plain (Call "f"), Plain (LocalGet 0), Plain (I32_BinOp Add)] - , Config f [] [V_I32 7] [V_I32 5] [Plain (Call "f"), Plain (LocalGet 0), Plain (I32_BinOp Add)] - , Config f [] [V_I32 7] [] [Frame 1 [V_I32 5] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Add)], Plain (LocalGet 0), Plain (I32_BinOp Add)] - , Config f [] [V_I32 7] [] [Frame 1 [V_I32 5] [V_I32 5] [Plain (I32_Const 1), Plain (I32_BinOp Add)], Plain (LocalGet 0), Plain (I32_BinOp Add)] - , Config f [] [V_I32 7] [] [Frame 1 [V_I32 5] [V_I32 1, V_I32 5] [Plain (I32_BinOp Add)], Plain (LocalGet 0), Plain (I32_BinOp Add)] - , Config f [] [V_I32 7] [] [Frame 1 [V_I32 5] [V_I32 6] [], Plain (LocalGet 0), Plain (I32_BinOp Add)] - , Config f [] [V_I32 7] [V_I32 6] [Plain (LocalGet 0), Plain (I32_BinOp Add)] - , Config f [] [V_I32 7] [V_I32 7, V_I32 6] [Plain (I32_BinOp Add)] - , Config f [] [V_I32 7] [V_I32 13] [] - ] - , "Return" - ~> let f = [("f", Func "f" (Params [I32]) (Results [I32]) (Locals []) [LocalGet 0, I32_Const 1, I32_BinOp Add, Return, Unreachable])] - in [ Config f [] [] [] [Plain (I32_Const 5), Plain (Call "f")] - , Config f [] [] [V_I32 5] [Plain (Call "f")] - , Config f [] [] [] [Frame 1 [V_I32 5] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Add), Plain Return, Plain Unreachable]] - , Config f [] [] [] [Frame 1 [V_I32 5] [V_I32 5] [Plain (I32_Const 1), Plain (I32_BinOp Add), Plain Return, Plain Unreachable]] - , Config f [] [] [] [Frame 1 [V_I32 5] [V_I32 1, V_I32 5] [Plain (I32_BinOp Add), Plain Return, Plain Unreachable]] - , Config f [] [] [] [Frame 1 [V_I32 5] [V_I32 6] [Plain Return, Plain Unreachable]] - , Config f [] [] [] [Frame 1 [V_I32 5] [V_I32 6] [Returning [V_I32 6], Plain Unreachable]] - , Config f [] [] [V_I32 6] [] - ] - , "Frame-Nested" - ~> let - f = Func "f" (Params [I32]) (Results [I32]) (Locals []) [LocalGet 0, Block (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add, Call "g", I32_Const 1, I32_BinOp Add]] - g = Func "g" (Params [I32]) (Results [I32]) (Locals []) [Block (Params []) (Results [I32]) [LocalGet 0, I32_Const 1, I32_BinOp Add, Br 0, Unreachable]] - fns = [("f", f), ("g", g)] - in - [ Config fns [] [] [] [Plain (I32_Const 5), Plain (Call "f"), Plain Drop] - , Config fns [] [] [V_I32 5] [Plain (Call "f"), Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Plain (LocalGet 0), Plain (Block (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add, Call "g", I32_Const 1, I32_BinOp Add])], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [V_I32 5] [Plain (Block (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add, Call "g", I32_Const 1, I32_BinOp Add])], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [V_I32 5] [Plain (I32_Const 1), Plain (I32_BinOp Add), Plain (Call "g"), Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [V_I32 1, V_I32 5] [Plain (I32_BinOp Add), Plain (Call "g"), Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [V_I32 6] [Plain (Call "g"), Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Plain (Block (Params []) (Results [I32]) [LocalGet 0, I32_Const 1, I32_BinOp Add, Br 0, Unreachable])], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Label 1 [] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Add), Plain (Br 0), Plain Unreachable]], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Label 1 [] [V_I32 6] [Plain (I32_Const 1), Plain (I32_BinOp Add), Plain (Br 0), Plain Unreachable]], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Label 1 [] [V_I32 1, V_I32 6] [Plain (I32_BinOp Add), Plain (Br 0), Plain Unreachable]], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Label 1 [] [V_I32 7] [Plain (Br 0), Plain Unreachable]], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Label 1 [] [V_I32 7] [Breaking 0 [V_I32 7], Plain Unreachable]], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [V_I32 7] [], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [V_I32 7] [Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [V_I32 1, V_I32 7] [Plain (I32_BinOp Add)]], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [] [Label 1 [] [V_I32 8] []], Plain Drop] - , Config fns [] [] [] [Frame 1 [V_I32 5] [V_I32 8] [], Plain Drop] - , Config fns [] [] [V_I32 8] [Plain Drop] - , Config fns [] [] [] [] + +smallStepTests :: LIO Lattice2 [(String, [Config Lattice2])] +smallStepTests = do + l0 <- label Low (V_I32 0) + l1 <- label Low (V_I32 1) + l2 <- label Low (V_I32 2) + l3 <- label Low (V_I32 3) + l4 <- label Low (V_I32 4) + l5 <- label Low (V_I32 5) + + l2_64 <- label Low (V_I64 2) + l3_64 <- label Low (V_I64 3) + l5_64 <- label Low (V_I64 5) + + return [ "Nop" + ~> [ Config [] [] [] [] [Plain Nop] Low + , Config [] [] [] [] [] Low ] - ] + , "Drop" + ~> [ Config [] [] [] [l1, l0] [Plain Drop, Plain Drop] Low + , Config [] [] [] [l0] [Plain Drop] Low + , Config [] [] [] [] [] Low + ] + , "Unreachable" + ~> [ Config [] [] [] [] [Plain Unreachable] Low + , Config [] [] [] [] [Trapping UnreachableExecuted] Low + ] + , "Add" + ~> [ Config [] [] [] [] [Plain (I32_Const 2), Plain (I32_Const 3), Plain (I32_BinOp Add)] Low + , Config [] [] [] [l2] [Plain (I32_Const 3), Plain (I32_BinOp Add)] Low + , Config [] [] [] [l3, l2] [Plain (I32_BinOp Add)] Low + , Config [] [] [] [l5] [] Low + ] + , "Add64" + ~> [ Config [] [] [] [] [Plain (I64_Const 2), Plain (I64_Const 3), Plain (I64_BinOp Add)] Low + , Config [] [] [] [l2_64] [Plain (I64_Const 3), Plain (I64_BinOp Add)] Low + , Config [] [] [] [l3_64, l2_64] [Plain (I64_BinOp Add)] Low + , Config [] [] [] [l5_64] [] Low + ] + ] + {- + , "LocalGet" + ~> [ Config [] [] [V_I32 7] [] [Plain (LocalGet 0)] + , Config [] [] [V_I32 7] [V_I32 7] [] + ] + , "LocalSet" + ~> [ Config [] [] [l0] [] [Plain (I32_Const 1), Plain (LocalSet 0)] + , Config [] [] [l0] [l1] [Plain (LocalSet 0)] + , Config [] [] [l1] [] [] + ] + , "MemSize" + ~> [ Config [] [1 .. 10] [] [] [Plain MemSize] + , Config [] [1 .. 10] [] [l10] [] + ] + , "MemLoad" + ~> [ Config [] [1 .. 10] [] [] [Plain (I32_Const 2), Plain I32_Load, Plain (I32_Const 4), Plain I32_Load, Plain (I32_Const 5), Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] + , Config [] [1 .. 10] [] [l2] [Plain I32_Load, Plain (I32_Const 4), Plain I32_Load, Plain (I32_Const 5), Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] + , Config [] [1 .. 10] [] [l3] [Plain (I32_Const 4), Plain I32_Load, Plain (I32_Const 5), Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] + , Config [] [1 .. 10] [] [l4, l3] [Plain I32_Load, Plain (I32_Const 5), Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] + , Config [] [1 .. 10] [] [l5, l3] [Plain (I32_Const 5), Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] + , Config [] [1 .. 10] [] [l5, l5, l3] [Plain I32_Load, Plain (I32_Const 10), Plain I32_Load] + , Config [] [1 .. 10] [] [V_I32 6, l5, l3] [Plain (I32_Const 10), Plain I32_Load] + , Config [] [1 .. 10] [] [l10, V_I32 6, l5, l3] [Plain I32_Load] + , Config [] [1 .. 10] [] [V_I32 6, l5, l3] [Trapping MemoryOutOfBounds] + ] + , "MemStore" + ~> [ Config [] [1, 2, 3] [] [] [Plain (I32_Const 1), Plain (I32_Const 5), Plain I32_Store, Plain (I32_Const 3), Plain (I32_Const 6), Plain I32_Store] + , Config [] [1, 2, 3] [] [l1] [Plain (I32_Const 5), Plain I32_Store, Plain (I32_Const 3), Plain (I32_Const 6), Plain I32_Store] + , Config [] [1, 2, 3] [] [l5, l1] [Plain I32_Store, Plain (I32_Const 3), Plain (I32_Const 6), Plain I32_Store] + , Config [] [1, 5, 3] [] [] [Plain (I32_Const 3), Plain (I32_Const 6), Plain I32_Store] + , Config [] [1, 5, 3] [] [l3] [Plain (I32_Const 6), Plain I32_Store] + , Config [] [1, 5, 3] [] [V_I32 6, l3] [Plain I32_Store] + , Config [] [1, 5, 3] [] [] [Trapping MemoryOutOfBounds] + ] + , "Block" + ~> [ Config [] [] [] [l5] [Plain (Block (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add])] + , Config [] [] [] [] [Label 1 [] [l5] ([Plain (I32_Const 1), Plain (I32_BinOp Add)])] + , Config [] [] [] [] [Label 1 [] [l1, l5] ([Plain (I32_BinOp Add)])] + , Config [] [] [] [] [Label 1 [] [V_I32 6] ([])] + , Config [] [] [] [V_I32 6] [] + ] + , "Loop" + ~> [ Config [] [] [] [l5] [Plain (Loop (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add])] + , Config [] [] [] [] [Label 1 [Loop (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add]] [l5] ([Plain (I32_Const 1), Plain (I32_BinOp Add)])] + , Config [] [] [] [] [Label 1 [Loop (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add]] [l1, l5] ([Plain (I32_BinOp Add)])] + , Config [] [] [] [] [Label 1 [Loop (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add]] [V_I32 6] ([])] + , Config [] [] [] [V_I32 6] [] + ] + , "BrIf-Block" + ~> [ Config [] [] [l5] [] [Plain (Block (Params []) (Results []) [LocalGet 0, I32_Const 1, I32_BinOp Sub, LocalSet 0, LocalGet 0, I32_Const 0, I32_RelOp Gt, BrIf 0, Unreachable])] + , Config [] [] [l5] [] [Label 0 [] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] + , Config [] [] [l5] [] [Label 0 [] [l5] [Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] + , Config [] [] [l5] [] [Label 0 [] [l1, l5] [Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] + , Config [] [] [l5] [] [Label 0 [] [l4] [Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] + , Config [] [] [l4] [] [Label 0 [] [] [Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] + , Config [] [] [l4] [] [Label 0 [] [l4] [Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] + , Config [] [] [l4] [] [Label 0 [] [l0, l4] [Plain (I32_RelOp Gt), Plain (BrIf 0), Plain Unreachable]] + , Config [] [] [l4] [] [Label 0 [] [l1] [Plain (BrIf 0), Plain Unreachable]] + , Config [] [] [l4] [] [Label 0 [] [] [Plain (Br 0), Plain Unreachable]] + , Config [] [] [l4] [] [Label 0 [] [] [Breaking 0 [], Plain Unreachable]] + , Config [] [] [l4] [] [] + ] + , "BrIf-Loop" + ~> let l = Loop (Params []) (Results []) [LocalGet 0, I32_Const 1, I32_BinOp Sub, LocalSet 0, LocalGet 0, I32_Const 0, I32_RelOp Gt, BrIf 0] + in [ Config [] [] [l2] [] [Plain l] + , Config [] [] [l2] [] [Label 0 [l] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l2] [] [Label 0 [l] [l2] [Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l2] [] [Label 0 [l] [l1, l2] [Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l2] [] [Label 0 [l] [l1] [Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l1] [] [Label 0 [l] [] [Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l1] [] [Label 0 [l] [l1] [Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l1] [] [Label 0 [l] [l0, l1] [Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l1] [] [Label 0 [l] [l1] [Plain (BrIf 0)]] + , Config [] [] [l1] [] [Label 0 [l] [] [Plain (Br 0)]] + , Config [] [] [l1] [] [Label 0 [l] [] [Breaking 0 []]] + , Config [] [] [l1] [] [Plain l] + , Config [] [] [l1] [] [Label 0 [l] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l1] [] [Label 0 [l] [l1] [Plain (I32_Const 1), Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l1] [] [Label 0 [l] [l1, l1] [Plain (I32_BinOp Sub), Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l1] [] [Label 0 [l] [l0] [Plain (LocalSet 0), Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l0] [] [Label 0 [l] [] [Plain (LocalGet 0), Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l0] [] [Label 0 [l] [l0] [Plain (I32_Const 0), Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l0] [] [Label 0 [l] [l0, l0] [Plain (I32_RelOp Gt), Plain (BrIf 0)]] + , Config [] [] [l0] [] [Label 0 [l] [l0] [Plain (BrIf 0)]] + , Config [] [] [l0] [] [Label 0 [l] [] []] + , Config [] [] [l0] [] [] + ] + , "Label-Nested" + ~> [ Config [] [] [] [] [Plain (Block (Params []) (Results [I32]) [Block (Params []) (Results [I32, I32]) [I32_Const 5, I32_Const 6, I32_Const 7, BrIf 1]])] + , Config [] [] [] [] [Label 1 [] [] [Plain (Block (Params []) (Results [I32, I32]) [I32_Const 5, I32_Const 6, I32_Const 7, BrIf 1])]] + , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [] [Plain (I32_Const 5), Plain (I32_Const 6), Plain (I32_Const 7), Plain (BrIf 1)]]] + , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [l5] [Plain (I32_Const 6), Plain (I32_Const 7), Plain (BrIf 1)]]] + , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [V_I32 6, l5] [Plain (I32_Const 7), Plain (BrIf 1)]]] + , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [V_I32 7, V_I32 6, l5] [Plain (BrIf 1)]]] + , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [V_I32 6, l5] [Plain (Br 1)]]] + , Config [] [] [] [] [Label 1 [] [] [Label 2 [] [V_I32 6, l5] [Breaking 1 [V_I32 6, l5]]]] + , Config [] [] [] [] [Label 1 [] [] [Breaking 0 [V_I32 6, l5]]] + , Config [] [] [] [V_I32 6] [] + ] + , "Label-Mutates-Locals" + ~> [ Config [] [] [l5] [] [Label 0 [] [l4] [Plain (LocalSet 0), Plain (LocalGet 0)]] + , Config [] [] [l4] [] [Label 0 [] [] [Plain (LocalGet 0)]] + ] + , "Call" + ~> let f = [("f", Func "f" (Params [I32]) (Results [I32]) (Locals []) [LocalGet 0, I32_Const 1, I32_BinOp Add])] + in [ Config f [] [V_I32 7] [] [Plain (I32_Const 5), Plain (Call "f"), Plain (LocalGet 0), Plain (I32_BinOp Add)] + , Config f [] [V_I32 7] [l5] [Plain (Call "f"), Plain (LocalGet 0), Plain (I32_BinOp Add)] + , Config f [] [V_I32 7] [] [Frame 1 [l5] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Add)], Plain (LocalGet 0), Plain (I32_BinOp Add)] + , Config f [] [V_I32 7] [] [Frame 1 [l5] [l5] [Plain (I32_Const 1), Plain (I32_BinOp Add)], Plain (LocalGet 0), Plain (I32_BinOp Add)] + , Config f [] [V_I32 7] [] [Frame 1 [l5] [l1, l5] [Plain (I32_BinOp Add)], Plain (LocalGet 0), Plain (I32_BinOp Add)] + , Config f [] [V_I32 7] [] [Frame 1 [l5] [V_I32 6] [], Plain (LocalGet 0), Plain (I32_BinOp Add)] + , Config f [] [V_I32 7] [V_I32 6] [Plain (LocalGet 0), Plain (I32_BinOp Add)] + , Config f [] [V_I32 7] [V_I32 7, V_I32 6] [Plain (I32_BinOp Add)] + , Config f [] [V_I32 7] [l13] [] + ] + , "Return" + ~> let f = [("f", Func "f" (Params [I32]) (Results [I32]) (Locals []) [LocalGet 0, I32_Const 1, I32_BinOp Add, Return, Unreachable])] + in [ Config f [] [] [] [Plain (I32_Const 5), Plain (Call "f")] + , Config f [] [] [l5] [Plain (Call "f")] + , Config f [] [] [] [Frame 1 [l5] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Add), Plain Return, Plain Unreachable]] + , Config f [] [] [] [Frame 1 [l5] [l5] [Plain (I32_Const 1), Plain (I32_BinOp Add), Plain Return, Plain Unreachable]] + , Config f [] [] [] [Frame 1 [l5] [l1, l5] [Plain (I32_BinOp Add), Plain Return, Plain Unreachable]] + , Config f [] [] [] [Frame 1 [l5] [V_I32 6] [Plain Return, Plain Unreachable]] + , Config f [] [] [] [Frame 1 [l5] [V_I32 6] [Returning [V_I32 6], Plain Unreachable]] + , Config f [] [] [V_I32 6] [] + ] + , "Frame-Nested" + ~> let + f = Func "f" (Params [I32]) (Results [I32]) (Locals []) [LocalGet 0, Block (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add, Call "g", I32_Const 1, I32_BinOp Add]] + g = Func "g" (Params [I32]) (Results [I32]) (Locals []) [Block (Params []) (Results [I32]) [LocalGet 0, I32_Const 1, I32_BinOp Add, Br 0, Unreachable]] + fns = [("f", f), ("g", g)] + in + [ Config fns [] [] [] [Plain (I32_Const 5), Plain (Call "f"), Plain Drop] + , Config fns [] [] [l5] [Plain (Call "f"), Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Plain (LocalGet 0), Plain (Block (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add, Call "g", I32_Const 1, I32_BinOp Add])], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [l5] [Plain (Block (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add, Call "g", I32_Const 1, I32_BinOp Add])], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [l5] [Plain (I32_Const 1), Plain (I32_BinOp Add), Plain (Call "g"), Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [l1, l5] [Plain (I32_BinOp Add), Plain (Call "g"), Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [V_I32 6] [Plain (Call "g"), Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Plain (Block (Params []) (Results [I32]) [LocalGet 0, I32_Const 1, I32_BinOp Add, Br 0, Unreachable])], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Label 1 [] [] [Plain (LocalGet 0), Plain (I32_Const 1), Plain (I32_BinOp Add), Plain (Br 0), Plain Unreachable]], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Label 1 [] [V_I32 6] [Plain (I32_Const 1), Plain (I32_BinOp Add), Plain (Br 0), Plain Unreachable]], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Label 1 [] [l1, V_I32 6] [Plain (I32_BinOp Add), Plain (Br 0), Plain Unreachable]], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Label 1 [] [V_I32 7] [Plain (Br 0), Plain Unreachable]], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [] [Label 1 [] [V_I32 7] [Breaking 0 [V_I32 7], Plain Unreachable]], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [] [Frame 1 [V_I32 6] [V_I32 7] [], Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [V_I32 7] [Plain (I32_Const 1), Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [l1, V_I32 7] [Plain (I32_BinOp Add)]], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [] [Label 1 [] [V_I32 8] []], Plain Drop] + , Config fns [] [] [] [Frame 1 [l5] [V_I32 8] [], Plain Drop] + , Config fns [] [] [V_I32 8] [Plain Drop] + , Config fns [] [] [] [] + ] + ] -} \ No newline at end of file