From 7c991a9570f1e9d193a18a1a33b8fec6b60e55ff Mon Sep 17 00:00:00 2001 From: Stephan Stanisic Date: Mon, 25 Nov 2024 09:08:52 +0100 Subject: [PATCH] Tracking PC through labels? --- src/MiniWasm/Execution.hs | 154 +++++++++++++++++++++++++------------- src/MiniWasm/Syntax.hs | 10 +-- 2 files changed, 105 insertions(+), 59 deletions(-) diff --git a/src/MiniWasm/Execution.hs b/src/MiniWasm/Execution.hs index 59b8bcb..7737075 100644 --- a/src/MiniWasm/Execution.hs +++ b/src/MiniWasm/Execution.hs @@ -14,6 +14,7 @@ import Data.Maybe (fromJust) import Debug.Trace qualified import MiniWasm.Syntax import LIO.TCB +import Text.Printf -- Wasm values data Value @@ -103,6 +104,7 @@ data AdminInstr l , continuation :: [Instr l] -- The instruction sequence to execute when branching out of this label. , 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). + , pc :: l -- pc of the inner label } | -- Function call frame. Frame @@ -110,6 +112,7 @@ data AdminInstr l , 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). + , pc :: l -- pc of the inner frame } | -- New administrative instructions: -- Our interpreter implements control flow slightly differently from the @@ -148,11 +151,12 @@ data Config l = Config -- Replace the TODO stubs in this function with your code. step :: Label l => Config l -> LIO l (Config l) step cfg = do + state@(LIOState pc c) <- getLIOStateTCB case cfg.instrs of [] -> return cfg instr : instrs -> -- Comment this line out if you don't want debug - debug instr cfg $ + debug instr cfg state $ case instr of Plain instr -> case (instr, cfg.stack) of @@ -169,18 +173,18 @@ step cfg = do return cfg{stack = v : stack, instrs} -- 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 - - -- V_I32 a' <- unlabel a - -- V_I32 b' <- unlabel b - -- s <- getLIOStateTCB - -- v <- label (labelOf a `lub` labelOf b `lub` (lioLabel s)) $ V_I32 (evalBinOp op a' b') - -- return cfg{stack = v : stack, instrs} - (I32_BinOp op, b : a : stack) -> do - let v = evalBinOp op <$> a <*> b + + V_I32 a' <- unlabel a + V_I32 b' <- unlabel b + s <- getLIOStateTCB + v <- label (labelOf a `lub` labelOf b `lub` (lioLabel s)) $ V_I32 (evalBinOp op a' b') return cfg{stack = v : stack, instrs} + -- (I32_BinOp op, b : a : stack) -> do + -- let v = evalBinOp op <$> a <*> b + -- return cfg{stack = v : stack, instrs} + (I32_RelOp op, b : a : stack) -> do V_I32 a' <- unlabel a V_I32 b' <- unlabel b @@ -206,6 +210,7 @@ step cfg = do (LocalSet ix, x : stack) -> return cfg{stack, instrs, locals = fromJust (updateAt ix x cfg.locals)} (Block (Params params) (Results results) body, stack) -> do + LIOState pc _ <- getLIOStateTCB return cfg { stack = drop (length params) stack , instrs = @@ -214,11 +219,13 @@ step cfg = do , continuation = [] , innerStack = take (length params) stack , body = map Plain body + , pc = pc } : instrs } (Loop (Params params) (Results results) body, stack) -> do + LIOState pc _ <- getLIOStateTCB return cfg { stack = drop (length params) stack , instrs = @@ -227,10 +234,10 @@ step cfg = do , continuation = [Loop (Params params) (Results results) body] , innerStack = take (length params) stack , body = map Plain body + , pc = pc } : instrs } - (Br ix, stack) -> return cfg{instrs = Breaking ix stack : instrs} (BrIf ix, x : stack) -> do @@ -240,9 +247,20 @@ step cfg = do _ -> return cfg{instrs = Plain (Br ix) : instrs, stack} (Call fn, stack) -> do - s <- getLIOStateTCB - vals <- mapM (label (lioLabel s) . defaultValue) func.locals.unwrap - return cfg{instrs=Frame m (take n stack ++ vals) [] body : instrs, stack = drop n stack} + LIOState pc _ <- getLIOStateTCB + vals <- mapM (label pc . defaultValue) func.locals.unwrap + return cfg + { instrs = + Frame + { resultsCount = m + , innerLocals = (take n stack ++ vals) + , innerStack = [] + , body = body + , pc = pc + } + : instrs + , stack = drop n stack + } where func = fromJust $ lookup fn cfg.funcs n = length func.params.unwrap @@ -260,22 +278,31 @@ step cfg = do 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 + Label n k vs [] pc' -> return cfg{stack = take n vs, instrs = []} + Label n k vs (Trapping msg : _) pc' -> return cfg{instrs=[Trapping msg]} + Label n k vs (Returning vs' : _) pc' -> return cfg{instrs=Returning vs':instrs} + Label n k vs (Breaking 0 vs' : _) pc' -> do + -- FIXME: Is this correct? + putLIOStateTCB $ LIOState (pc' `lub` pc) c + return cfg{instrs = map Plain k ++ instrs, stack = take n vs'} + Label n k vs (Breaking ix vs' : _) pc' -> return cfg{instrs = Breaking (ix-1) vs' : instrs} + Label n k vs (e : es) pc' -> do + putLIOStateTCB $ LIOState pc' c cfg' <- step cfg{stack=vs, instrs=e:es} -- add toLabeled - return cfg'{stack=cfg.stack, instrs=(Label n k cfg'.stack cfg'.instrs) : instrs} + LIOState pc'' c <- getLIOStateTCB + putLIOStateTCB state + return cfg'{stack=cfg.stack, instrs=(Label n k cfg'.stack cfg'.instrs pc'') : 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 + Frame n locs vs [] pc | 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 : _) pc -> return cfg{instrs=[Trapping msg]} + Frame n locs vs (Returning vs' : _) pc -> return cfg{stack=(take n vs') ++ cfg.stack, instrs} + Frame n locs vs es pc' -> do + putLIOStateTCB $ LIOState pc' c cfg' <- step cfg{stack=vs, instrs=es, locals=locs} -- add toLabeled - return cfg'{stack=cfg.stack, instrs=(Frame n cfg'.locals cfg'.stack cfg'.instrs):instrs, locals=cfg.locals} + LIOState pc'' c <- getLIOStateTCB + putLIOStateTCB state + return cfg'{stack=cfg.stack, instrs=(Frame n cfg'.locals cfg'.stack cfg'.instrs pc''):instrs, locals=cfg.locals} -- "Drop" test1 :: LIO Lattice2 (Config Lattice2) @@ -321,21 +348,18 @@ test6 = do 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])] + stepUntilFinal $ Config [] [] [] [l5] [Plain (Block (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add])] -- "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])] + stepUntilFinal $ Config [] [] [] [l5] [Plain (Loop (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add])] -- "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])] -- "BrIf-Loop" @@ -348,50 +372,45 @@ test10 = do -- "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]])] + stepUntilFinal $ Config [] [] [] [] [Plain (Block (Params []) (Results [I32]) [Block (Params []) (Results [I32, I32]) [I32_Const 5, I32_Const 6, I32_Const 7, BrIf 1]])] -- "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)]] + LIOState pc _ <- getLIOStateTCB + stepUntilFinal $ Config [] [] [l5] [] [Label 0 [] [l4] [Plain (LocalSet 0), Plain (LocalGet 0)] pc] -- "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])] + let f = [("f", Func "f" (Params [I32]) (Results [I32]) (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)] -- "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])] + let f = [("f", Func "f" (Params [I32]) (Results [I32]) (Locals []) [LocalGet 0, I32_Const 1, I32_BinOp Add, Return, Unreachable])] stepUntilFinal $ Config f [] [] [] [Plain (I32_Const 5), Plain (Call "f")] -- "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]] + 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)] stepUntilFinal $ Config fns [] [] [] [Plain (I32_Const 5), Plain (Call "f"), Plain Drop] ifcTest1 :: LIO Lattice2 (Config Lattice2) ifcTest1 = do - lI32 <- label Low I32 - hI32 <- label High I32 h1 <- label High (V_I32 1) - let f = Func "f" (Params [hI32]) (Results [lI32]) (Locals []) + let f = Func "f" (Params [I32]) (Results [I32]) (Locals []) [ LocalGet 0 - , Block (Params [lI32]) (Results [lI32]) -- if - [ Block (Params [lI32]) (Results [lI32]) -- else + , Block (Params [I32]) (Results [I32]) -- if + [ Block (Params [I32]) (Results [I32]) -- else [ BrIf 0 , I32_Const 1 , Br 1 @@ -401,6 +420,24 @@ ifcTest1 = do ] stepUntilFinal $ Config [("f", f)] [] [h1] [] [Plain (LocalGet 0), Plain (Call "f")] +ifcTest2 :: LIO Lattice2 (Config Lattice2) +ifcTest2 = do + h1 <- label High (V_I32 1) + l1 <- label Low (V_I32 1) + let f = Func "f" (Params [I32, I32]) (Results [I32]) (Locals []) + [ LocalGet 0 + , LocalGet 1 + , Block (Params [I32]) (Results [I32]) -- if + [ Block (Params [I32]) (Results [I32]) -- else + [ BrIf 0 + , I32_Const 1 + , Br 1 + ] + , I32_Const 0 + ] + ] + stepUntilFinal $ Config [("f", f)] [] [l1, h1] [] [Plain (LocalGet 0), Plain (LocalGet 1), Plain (Call "f")] + sample :: LIO Lattice2 (Config Lattice2) -> IO () sample ex = do putStrLn "Running with state Low and clearance High" @@ -408,9 +445,16 @@ sample ex = do let state = LIOState Low High (config, state) <- runLIO ex state - putStrLn "Final stack:" - print config - print state + putStrLn "Final state:" + + putStr "Program counter: " + print state.lioLabel + putStr "Stack: " + print config.stack + putStr "Locals: " + print config.locals + putStr "Memory: " + print config.memory return () @@ -444,6 +488,10 @@ executeModule m = in let state = LIOState High High in evalLIO (stepUntilFinal initialConfig) state -} -debug :: Label l => AdminInstr l -> Config l -> a -> a -debug instr cfg = - Debug.Trace.trace ("DEBUG: " ++ "\n\t(instr: " ++ show instr ++ ")\n\t(stack: " ++ show (map showTCB cfg.stack) ++ ")\n") +debug :: Label l => AdminInstr l -> Config l -> LIOState l -> a -> a +debug instr cfg (LIOState pc c) = + Debug.Trace.trace ( + show pc ++ "\t" ++ + printf "%-16s" (show cfg.stack) ++ "\t" ++ + show instr + ) diff --git a/src/MiniWasm/Syntax.hs b/src/MiniWasm/Syntax.hs index 15e7cd8..b50b3f4 100644 --- a/src/MiniWasm/Syntax.hs +++ b/src/MiniWasm/Syntax.hs @@ -20,13 +20,11 @@ type FuncName = String -- The name of a function. -- You can either pattern-match on the constructors, or use the .unwrap field to access the actual lists. -- Labeled l -- Implicit flow with locals detected? -newtype Params l = Params { unwrap ::[Labeled l ValueType] } -instance Label l => Show (Params l) where - show (Params p) = show $ map showTCB p +newtype Params l = Params { unwrap ::[ValueType] } + deriving Show -newtype Results l = Results { unwrap :: [Labeled l ValueType] } -instance Label l => Show (Results l) where - show (Results p) = show $ map showTCB p +newtype Results l = Results { unwrap :: [ValueType] } + deriving Show newtype Locals = Locals { unwrap :: [ValueType] } deriving (Show, Eq)