steph/wasm-ifc
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Tracking PC through labels?

Browse Source
This commit is contained in:
Stephan Stanisic 2024-11-25 09:08:52 +01:00
parent 02bab4117d
commit 7c991a9570
2 changed files with 105 additions and 59 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

154
src/MiniWasm/Execution.hs
View File

@ -14,6 +14,7 @@ import Data.Maybe (fromJust)
import Debug.Trace qualified import Debug.Trace qualified
import MiniWasm.Syntax import MiniWasm.Syntax
import LIO.TCB import LIO.TCB
import Text.Printf
-- Wasm values -- Wasm values
data Value data Value
@ -103,6 +104,7 @@ data AdminInstr l
, continuation :: [Instr l] -- The instruction sequence to execute when branching out of this label. , 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. , 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). , 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. | -- Function call frame.
Frame Frame
@ -110,6 +112,7 @@ data AdminInstr l
, innerLocals :: [Labeled l Value] -- The local variables 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. , 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). , 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: | -- New administrative instructions:
-- Our interpreter implements control flow slightly differently from the -- 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. -- Replace the TODO stubs in this function with your code.
step :: Label l => Config l -> LIO l (Config l) step :: Label l => Config l -> LIO l (Config l)
step cfg = do step cfg = do
state@(LIOState pc c) <- getLIOStateTCB
case cfg.instrs of case cfg.instrs of
[] -> return cfg [] -> return cfg
instr : instrs -> instr : instrs ->
-- Comment this line out if you don't want debug -- Comment this line out if you don't want debug
debug instr cfg $ debug instr cfg state $
case instr of case instr of
Plain instr -> Plain instr ->
case (instr, cfg.stack) of case (instr, cfg.stack) of
@ -169,18 +173,18 @@ step cfg = do
return cfg{stack = v : stack, instrs} return cfg{stack = v : stack, instrs}
-- You can directly pattern match on the stack too. -- 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. -- 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 (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} 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 (I32_RelOp op, b : a : stack) -> do
V_I32 a' <- unlabel a V_I32 a' <- unlabel a
V_I32 b' <- unlabel b 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)} (LocalSet ix, x : stack) -> return cfg{stack, instrs, locals = fromJust (updateAt ix x cfg.locals)}
(Block (Params params) (Results results) body, stack) -> do (Block (Params params) (Results results) body, stack) -> do
LIOState pc _ <- getLIOStateTCB
return cfg return cfg
{ stack = drop (length params) stack { stack = drop (length params) stack
, instrs = , instrs =
@ -214,11 +219,13 @@ step cfg = do
, continuation = [] , continuation = []
, innerStack = take (length params) stack , innerStack = take (length params) stack
, body = map Plain body , body = map Plain body
, pc = pc
} }
: instrs : instrs
} }
(Loop (Params params) (Results results) body, stack) -> do (Loop (Params params) (Results results) body, stack) -> do
LIOState pc _ <- getLIOStateTCB
return cfg return cfg
{ stack = drop (length params) stack { stack = drop (length params) stack
, instrs = , instrs =
@ -227,10 +234,10 @@ step cfg = do
, continuation = [Loop (Params params) (Results results) body] , continuation = [Loop (Params params) (Results results) body]
, innerStack = take (length params) stack , innerStack = take (length params) stack
, body = map Plain body , body = map Plain body
, pc = pc
} }
: instrs : instrs
} }
(Br ix, stack) -> return cfg{instrs = Breaking ix stack : instrs} (Br ix, stack) -> return cfg{instrs = Breaking ix stack : instrs}
(BrIf ix, x : stack) -> do (BrIf ix, x : stack) -> do
@ -240,9 +247,20 @@ step cfg = do
_ -> return cfg{instrs = Plain (Br ix) : instrs, stack} _ -> return cfg{instrs = Plain (Br ix) : instrs, stack}
(Call fn, stack) -> do (Call fn, stack) -> do
s <- getLIOStateTCB LIOState pc _ <- getLIOStateTCB
vals <- mapM (label (lioLabel s) . defaultValue) func.locals.unwrap vals <- mapM (label pc . defaultValue) func.locals.unwrap
return cfg{instrs=Frame m (take n stack ++ vals) [] body : instrs, stack = drop n stack} return cfg
{ instrs =
Frame
{ resultsCount = m
, innerLocals = (take n stack ++ vals)
, innerStack = []
, body = body
, pc = pc
}
: instrs
, stack = drop n stack
}
where where
func = fromJust $ lookup fn cfg.funcs func = fromJust $ lookup fn cfg.funcs
n = length func.params.unwrap n = length func.params.unwrap
@ -260,22 +278,31 @@ step cfg = do
Breaking ix vs -> error "Breaking when not inside a label" Breaking ix vs -> error "Breaking when not inside a label"
Returning vs -> error "Returning when not inside a frame" Returning vs -> error "Returning when not inside a frame"
Label n k vs [] -> return cfg{stack = take n vs, instrs = []} Label n k vs [] pc' -> return cfg{stack = take n vs, instrs = []}
Label n k vs (Trapping msg : _) -> return cfg{instrs=[Trapping msg]} Label n k vs (Trapping msg : _) pc' -> return cfg{instrs=[Trapping msg]}
Label n k vs (Returning vs' : _) -> return cfg{instrs=Returning vs':instrs} Label n k vs (Returning vs' : _) pc' -> 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 0 vs' : _) pc' -> do
Label n k vs (Breaking ix vs' : _) -> return cfg{instrs = Breaking (ix-1) vs' : instrs} -- FIXME: Is this correct?
Label n k vs (e : es) -> do 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 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} 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" | 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 (Trapping msg : _) pc -> return cfg{instrs=[Trapping msg]}
Frame n locs vs (Returning vs' : _) -> return cfg{stack=(take n vs') ++ cfg.stack, instrs} Frame n locs vs (Returning vs' : _) pc -> return cfg{stack=(take n vs') ++ cfg.stack, instrs}
Frame n locs vs es -> do Frame n locs vs es pc' -> do
putLIOStateTCB $ LIOState pc' c
cfg' <- step cfg{stack=vs, instrs=es, locals=locs} -- add toLabeled 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" -- "Drop"
test1 :: LIO Lattice2 (Config Lattice2) test1 :: LIO Lattice2 (Config Lattice2)
@ -321,21 +348,18 @@ test6 = do
test7 :: LIO Lattice2 (Config Lattice2) test7 :: LIO Lattice2 (Config Lattice2)
test7 = do test7 = do
l5 <- label Low (V_I32 5) l5 <- label Low (V_I32 5)
lI32 <- label Low I32 stepUntilFinal $ Config [] [] [] [l5] [Plain (Block (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add])]
stepUntilFinal $ Config [] [] [] [l5] [Plain (Block (Params [lI32]) (Results [lI32]) [I32_Const 1, I32_BinOp Add])]
-- "Loop" -- "Loop"
test8 :: LIO Lattice2 (Config Lattice2) test8 :: LIO Lattice2 (Config Lattice2)
test8 = do test8 = do
l5 <- label Low (V_I32 5) l5 <- label Low (V_I32 5)
lI32 <- label Low I32 stepUntilFinal $ Config [] [] [] [l5] [Plain (Loop (Params [I32]) (Results [I32]) [I32_Const 1, I32_BinOp Add])]
stepUntilFinal $ Config [] [] [] [l5] [Plain (Loop (Params [lI32]) (Results [lI32]) [I32_Const 1, I32_BinOp Add])]
-- "BrIf-Block" -- "BrIf-Block"
test9 :: LIO Lattice2 (Config Lattice2) test9 :: LIO Lattice2 (Config Lattice2)
test9 = do test9 = do
l5 <- label Low (V_I32 5) 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])] 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" -- "BrIf-Loop"
@ -348,50 +372,45 @@ test10 = do
-- "Label-Nested" -- "Label-Nested"
test11 :: LIO Lattice2 (Config Lattice2) test11 :: LIO Lattice2 (Config Lattice2)
test11 = do test11 = do
lI32 <- label Low I32 stepUntilFinal $ Config [] [] [] [] [Plain (Block (Params []) (Results [I32]) [Block (Params []) (Results [I32, I32]) [I32_Const 5, I32_Const 6, I32_Const 7, BrIf 1]])]
stepUntilFinal $ Config [] [] [] [] [Plain (Block (Params []) (Results [lI32]) [Block (Params []) (Results [lI32, lI32]) [I32_Const 5, I32_Const 6, I32_Const 7, BrIf 1]])]
-- "Label-Mutates-Locals" -- "Label-Mutates-Locals"
test12 :: LIO Lattice2 (Config Lattice2) test12 :: LIO Lattice2 (Config Lattice2)
test12 = do test12 = do
l4 <- label Low (V_I32 4) l4 <- label Low (V_I32 4)
l5 <- label Low (V_I32 5) 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" -- "Call"
test13 :: LIO Lattice2 (Config Lattice2) test13 :: LIO Lattice2 (Config Lattice2)
test13 = do test13 = do
lI32 <- label Low I32
l7 <- label Low (V_I32 7) l7 <- label Low (V_I32 7)
l5 <- label Low (V_I32 5) 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)] stepUntilFinal $ Config f [] [l7] [] [Plain (I32_Const 5), Plain (Call "f"), Plain (LocalGet 0), Plain (I32_BinOp Add)]
-- "Return" -- "Return"
test14 :: LIO Lattice2 (Config Lattice2) test14 :: LIO Lattice2 (Config Lattice2)
test14 = do test14 = do
lI32 <- label Low I32 let f = [("f", Func "f" (Params [I32]) (Results [I32]) (Locals []) [LocalGet 0, I32_Const 1, I32_BinOp Add, Return, Unreachable])]
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")] stepUntilFinal $ Config f [] [] [] [Plain (I32_Const 5), Plain (Call "f")]
-- "Frame-Nested" -- "Frame-Nested"
test15 :: LIO Lattice2 (Config Lattice2) test15 :: LIO Lattice2 (Config Lattice2)
test15 = do test15 = do
lI32 <- label Low I32 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]]
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 [I32]) (Results [I32]) (Locals []) [Block (Params []) (Results [I32]) [LocalGet 0, I32_Const 1, I32_BinOp Add, Br 0, Unreachable]]
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)] fns = [("f", f), ("g", g)]
stepUntilFinal $ Config fns [] [] [] [Plain (I32_Const 5), Plain (Call "f"), Plain Drop] stepUntilFinal $ Config fns [] [] [] [Plain (I32_Const 5), Plain (Call "f"), Plain Drop]
ifcTest1 :: LIO Lattice2 (Config Lattice2) ifcTest1 :: LIO Lattice2 (Config Lattice2)
ifcTest1 = do ifcTest1 = do
lI32 <- label Low I32
hI32 <- label High I32
h1 <- label High (V_I32 1) 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 [ LocalGet 0
, Block (Params [lI32]) (Results [lI32]) -- if , Block (Params [I32]) (Results [I32]) -- if
[ Block (Params [lI32]) (Results [lI32]) -- else [ Block (Params [I32]) (Results [I32]) -- else
[ BrIf 0 [ BrIf 0
, I32_Const 1 , I32_Const 1
, Br 1 , Br 1
@ -401,6 +420,24 @@ ifcTest1 = do
] ]
stepUntilFinal $ Config [("f", f)] [] [h1] [] [Plain (LocalGet 0), Plain (Call "f")] 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 :: LIO Lattice2 (Config Lattice2) -> IO ()
sample ex = do sample ex = do
putStrLn "Running with state Low and clearance High" putStrLn "Running with state Low and clearance High"
@ -408,9 +445,16 @@ sample ex = do
let state = LIOState Low High let state = LIOState Low High
(config, state) <- runLIO ex state (config, state) <- runLIO ex state
putStrLn "Final stack:" putStrLn "Final state:"
print config
print state putStr "Program counter: "
print state.lioLabel
putStr "Stack: "
print config.stack
putStr "Locals: "
print config.locals
putStr "Memory: "
print config.memory
return () return ()
@ -444,6 +488,10 @@ executeModule m =
in let state = LIOState High High in let state = LIOState High High
in evalLIO (stepUntilFinal initialConfig) state -} in evalLIO (stepUntilFinal initialConfig) state -}
debug :: Label l => AdminInstr l -> Config l -> a -> a debug :: Label l => AdminInstr l -> Config l -> LIOState l -> a -> a
debug instr cfg = debug instr cfg (LIOState pc c) =
Debug.Trace.trace ("DEBUG: " ++ "\n\t(instr: " ++ show instr ++ ")\n\t(stack: " ++ show (map showTCB cfg.stack) ++ ")\n") Debug.Trace.trace (
show pc ++ "\t" ++
printf "%-16s" (show cfg.stack) ++ "\t" ++
show instr
)

10
src/MiniWasm/Syntax.hs
View File

@ -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. -- You can either pattern-match on the constructors, or use the .unwrap field to access the actual lists.
-- Labeled l -- Labeled l
-- Implicit flow with locals detected? -- Implicit flow with locals detected?
newtype Params l = Params { unwrap ::[Labeled l ValueType] } newtype Params l = Params { unwrap ::[ValueType] }
instance Label l => Show (Params l) where deriving Show
show (Params p) = show $ map showTCB p
newtype Results l = Results { unwrap :: [Labeled l ValueType] } newtype Results l = Results { unwrap :: [ValueType] }
instance Label l => Show (Results l) where deriving Show
show (Results p) = show $ map showTCB p
newtype Locals = Locals { unwrap :: [ValueType] } deriving (Show, Eq) newtype Locals = Locals { unwrap :: [ValueType] } deriving (Show, Eq)