Implemented blocks, loops and functions. But probably still wrong

flake.lock

@@ -5,11 +5,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1726560853,
+        "lastModified": 1731533236,
-        "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=",
+        "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,
+        "lastModified": 1731676054,
-        "narHash": "sha256-AlcmCXJZPIlO5dmFzV3V2XF6x/OpNWUV8Y/FMPGd8Z4=",
+        "narHash": "sha256-OZiZ3m8SCMfh3B6bfGC/Bm4x3qc1m2SVEAlkV6iY7Yg=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "2768c7d042a37de65bb1b5b3268fc987e534c49d",
+        "rev": "5e4fbfb6b3de1aa2872b76d49fafc942626e2add",
         "type": "github"
       },
       "original": {

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.
+        , innerLocals :: [Labeled l Value] -- The local variables of this function call.
-        , innerStack :: [Value] -- The inner stack 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'.
+    | Breaking {target :: LabelIndex, values :: [Labeled l Value]} -- The program is branching to label 'target' with args 'values'.
-    | Returning {results :: [Value]} -- The program is returning 'results' from a function.
+    | 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
+                                V_I32 a' <- unlabel a
-                                b' <- unlabel b
+                                V_I32 b' <- unlabel b
-
+                                v <- label (labelOf a `lub` labelOf b `lub` cfg.progcn) $ V_I32 (evalBinOp op a' 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"
                                 return cfg{stack = v : stack, instrs}
 
                             (I32_RelOp op, b : a : stack) -> do
-                                a' <- unlabel a
+                                V_I32 a' <- unlabel a
-                                b' <- unlabel b
+                                V_I32 b' <- unlabel b
-
+                                v <- label (labelOf a `lub` labelOf b `lub` cfg.progcn) $ boolToI32 (evalRelOp op a' b')
-                                v <- label (labelOf a `lub` labelOf b `lub` cfg.progcn) $ case (a', b') of
+                                return cfg{stack = v : stack, instrs}
-                                    (V_I32 a'', V_I32 b'') -> boolToI32 (evalRelOp op a'' b'')
+                                                            
-                                    (V_I64 a'', V_I64 b'') -> boolToI32 (evalRelOp op a'' b'')
+                            (I64_BinOp op, b : a : stack) -> do
-                                    _ -> error "incompatiable binop"
+                                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 ()
 

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 =

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 :: LIO Lattice2 [(String, [Config Lattice2])]
-smallStepTests =
+smallStepTests = do
-    [ "Nop"
+    l0 <- label Low (V_I32 0)
-        ~> [ Config [] [] [] [] [Plain Nop]
+    l1 <- label Low (V_I32 1)
-           , Config [] [] [] [] []
+    l2 <- label Low (V_I32 2)
-           ]
+    l3 <- label Low (V_I32 3)
-    , "Drop"
+    l4 <- label Low (V_I32 4)
-        ~> [ Config [] [] [] [V_I32 1, V_I32 0] [Plain Drop, Plain Drop]
+    l5 <- label Low (V_I32 5)
-           , Config [] [] [] [V_I32 0] [Plain Drop]
+
-           , Config [] [] [] [] []
+    l2_64 <- label Low (V_I64 2)
-           ]
+    l3_64 <- label Low (V_I64 3)
-    , "Unreachable"
+    l5_64 <- label Low (V_I64 5)
-        ~> [ Config [] [] [] [] [Plain Unreachable]
+    
-           , Config [] [] [] [] [Trapping UnreachableExecuted]
+    return [ "Nop"
-           ]
+            ~> [ Config [] [] [] [] [Plain Nop] Low
-    , "Add"
+            , Config [] [] [] [] [] Low
-        ~> [ 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 [] [] [] []
             ]
-    ]
+        , "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 [] [] [] []
+                ]
+        ]
 -}