From 3024cd2ca194ba4963a16997673dab4dc80e63dd Mon Sep 17 00:00:00 2001 From: Stephan Stanisic Date: Wed, 6 Nov 2024 12:41:23 +0100 Subject: [PATCH] binops --- miniwasm.cabal | 2 +- src/MiniWasm/Execution.hs | 157 +++++++--- src/MiniWasm/Syntax.hs | 36 ++- src/MiniWasm/TestCases/Programs.hs | 428 ++++++++++++++-------------- src/MiniWasm/TestCases/SmallStep.hs | 4 +- src/MiniWasm/Validation.hs | 9 +- test/Main.hs | 2 + 7 files changed, 363 insertions(+), 275 deletions(-) diff --git a/miniwasm.cabal b/miniwasm.cabal index b0e4bc2..f665820 100644 --- a/miniwasm.cabal +++ b/miniwasm.cabal @@ -29,7 +29,7 @@ library hs-source-dirs: src exposed-modules: MiniWasm.Syntax - MiniWasm.Validation + --MiniWasm.Validation MiniWasm.Execution MiniWasm.TestCases.SmallStep MiniWasm.TestCases.Programs diff --git a/src/MiniWasm/Execution.hs b/src/MiniWasm/Execution.hs index 4a48389..168fa6d 100644 --- a/src/MiniWasm/Execution.hs +++ b/src/MiniWasm/Execution.hs @@ -8,10 +8,12 @@ module MiniWasm.Execution where import Data.Int (Int32, Int64) +import LIO import Data.Maybe (fromJust) import Debug.Trace qualified import MiniWasm.Syntax +import LIO.TCB -- Wasm values data Value @@ -19,6 +21,23 @@ data Value | V_I64 Int64 deriving (Show, Eq) +data Lattice2 = Low | High + deriving (Eq, Show, Read) + +instance Label Lattice2 where + lub :: Lattice2 -> Lattice2 -> Lattice2 + Low `lub` Low = Low + _ `lub` _ = High + + glb :: Lattice2 -> Lattice2 -> Lattice2 + High `glb` High = High + _ `glb` _ = Low + + canFlowTo :: Lattice2 -> Lattice2 -> Bool + Low `canFlowTo` High = True + x `canFlowTo` y = x == y + + -- Helper functions to manipulate MiniWasm values: -- Gives the default value for each MiniWasm type. @@ -60,6 +79,10 @@ _ !? _ = Nothing infixl 9 !? -- Same as !! +{- +i32.const use pc for label +-} + -- Updates the element in the list at the specified index, returning Nothing if the index is out of bounds. -- You can use this when interpreting the I32_Store and LocalSet instructions. updateAt :: Int -> a -> [a] -> Maybe [a] @@ -70,21 +93,21 @@ updateAt n a (a' : as) updateAt n a [] = Nothing -- Administrative instructions. -data AdminInstr - = Plain Instr -- Regular instruction. +data AdminInstr l + = Plain (Instr l) -- Regular instruction. | -- Label frame. 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] -- 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 :: [Value] -- The inner stack of the label frame. - , body :: [AdminInstr] -- 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). } | -- 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. - , body :: [AdminInstr] -- 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). } | -- New administrative instructions: -- Our interpreter implements control flow slightly differently from the @@ -95,61 +118,113 @@ data AdminInstr 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. - deriving (Show, Eq) + | Taint l -- Taint pc + deriving Show -- Reasons for which the program can trap. data TrapReason = UnreachableExecuted -- An 'Unreachable' instruction was executed. | MemoryOutOfBounds -- A memory load or store was out of bounds. - deriving (Show, Eq) + deriving Show -- Configurations -- -- The configuration represents the state of a running MiniWasm program. -- For simplicity, we use an _explicit_ value stack in our interpreter: -- instructions push/pop values from this stack. -data Config = Config - { funcs :: [(FuncName, Func)] -- Function lookup map. You can use the 'lookup' function to find a function by its name. +data Config l = Config + { funcs :: [(FuncName, Func l)] -- Function lookup map. You can use the 'lookup' function to find a function by its name. , memory :: [Int32] -- Linear memory. - , locals :: [Value] -- Local variables. - , stack :: [Value] -- Explicit value stack. - , instrs :: [AdminInstr] -- Next instructions to be executed. + , locals :: [Labeled l Value] -- Local variables. + , stack :: [Labeled l Value] -- Explicit value stack. + , instrs :: [AdminInstr l] -- Next instructions to be executed. + , progcn :: l } - deriving (Show, Eq) -- The small-step evaluation function. -- -- Replace the TODO stubs in this function with your code. -step :: Config -> Config -step cfg = +step :: Label l => Config l -> LIO l (Config l) +step cfg = do case cfg.instrs of - [] -> cfg + [] -> return cfg instr : instrs -> -- Comment this line out if you don't want debug - --debug instr cfg $ + debug instr cfg $ case instr of Plain instr -> case (instr, cfg.stack) of - (Nop, _) -> cfg{instrs} -- Evaluating Nop does nothing, so just update the list of remaining instructions. - (Drop, _ : stack) -> cfg{stack, instrs} -- Evaluating Drop just pops and discards the top value from the stack. - (Unreachable, _) -> cfg{instrs = [Trapping UnreachableExecuted]} - (I32_Const i, stack) -> cfg{stack = V_I32 i : stack, instrs} + (Nop, _) -> return cfg{instrs} -- Evaluating Nop does nothing, so just update the list of remaining instructions. + (Drop, _ : stack) -> return cfg{stack, instrs} -- Evaluating Drop just pops and discards the top value from the stack. + (Unreachable, _) -> return cfg{instrs = [Trapping UnreachableExecuted]} + (I32_Const i, stack) -> do + v <- label cfg.progcn (V_I32 i) + return cfg{stack = v : stack, instrs} + (I64_Const i, stack) -> do + v <- label cfg.progcn (V_I64 i) + 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, V_I32 b : V_I32 a : stack) -> cfg{stack = V_I32 (evalBinOp op a b) : stack, instrs} - (I32_RelOp op, V_I32 b : V_I32 a : stack) -> cfg{stack = boolToI32 (evalRelOp op a b) : stack, instrs} - (I64_Const i, stack) -> cfg{stack = V_I64 i : stack, instrs} - (I64_BinOp op, V_I64 b : V_I64 a : stack) -> cfg{stack = V_I64 (evalBinOp op a b) : stack, instrs} - (I64_RelOp op, V_I64 b : V_I64 a : stack) -> cfg{stack = boolToI32 (evalRelOp op a b) : stack, instrs} - _ -> error "Missing or ill-typed operand(s) on the stack" - -- Administrative instructions: + (I32_BinOp op, b : a : stack) -> do + a' <- unlabel a + b' <- unlabel b + + v <- label (labelOf a `lub` labelOf b) $ 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 + b' <- unlabel b + + v <- label (labelOf a `lub` labelOf b) $ 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" + return cfg{stack = v : stack, instrs} + + _ -> error "Missing or ill-typed operand(s) on the stack" + + -- Administrative instructions: + Taint l -> return cfg{instrs, progcn = l} + + _ -> error "instruction unknown" + +test1 :: LIO Lattice2 (Config Lattice2) +test1 = do + l1 <- label Low (V_I32 1) + l0 <- label Low (V_I32 0) + let config = Config [] [] [] [l1, l0] [Plain Drop, Plain Drop] Low + stepUntilFinal config + +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) +test3 = do + let config = Config [] [] [] [] [Plain $ I32_Const 6, Taint High, Plain $ I32_Const 7, Plain $ I32_RelOp Lt] Low + stepUntilFinal config + +sample :: LIO Lattice2 (Config Lattice2) -> IO () +sample ex = do + putStrLn "Running with state Low and clearance High" + + let state = LIOState Low High + y <- evalLIO ex state + + putStrLn "Final stack:" + print $ map showTCB y.stack + + return () - -- If the current instruction is 'Trapping', all following instructions are discared. - _ -> error "whelp" -- This function checks whether the configuration has reached a final state, i.e. whether the -- program has been executed to completion. -isFinalState :: Config -> Bool +isFinalState :: Label l => Config l -> Bool isFinalState cfg = case cfg.instrs of [] -> True -- If there are no more instructions to execute, we've reached a final state. @@ -157,22 +232,24 @@ isFinalState cfg = _ -> False -- This function will repeatedly apply the 'step' function until the program reaches a final state. -stepUntilFinal :: Config -> Config -stepUntilFinal cfg = +stepUntilFinal :: Label l => Config l -> LIO l (Config l) +stepUntilFinal cfg = do if isFinalState cfg - then cfg - else stepUntilFinal (step cfg) + then return cfg + else do + step' <- step cfg + stepUntilFinal step' -- This function creates an initial configuration and executes the given program to completion. -executeModule :: Module -> Config +{- executeModule :: Label l => Module l -> IO (Config l) executeModule m = let funcMap = fmap (\f -> (f.name, f)) m.funcs initialConfig = Config{funcs = funcMap, memory = m.initialMemory, locals = [], stack = [], instrs = [Plain (Call "main")]} - in - stepUntilFinal initialConfig + in let state = LIOState High High + in evalLIO (stepUntilFinal initialConfig) state -} -debug :: AdminInstr -> Config -> a -> a +debug :: Label l => AdminInstr l -> Config l -> a -> a debug instr cfg = - Debug.Trace.trace ("DEBUG: " ++ "\n\t(instr: " ++ show instr ++ ")\n\t(cfg: " ++ show cfg ++ ")\n") + Debug.Trace.trace ("DEBUG: " ++ "\n\t(instr: " ++ show instr ++ ")\n\t(stack: " ++ show (map showTCB cfg.stack) ++ ")\n") diff --git a/src/MiniWasm/Syntax.hs b/src/MiniWasm/Syntax.hs index 9d5f878..841c6e7 100644 --- a/src/MiniWasm/Syntax.hs +++ b/src/MiniWasm/Syntax.hs @@ -1,6 +1,8 @@ module MiniWasm.Syntax where import Data.Int(Int32, Int64) +import LIO.TCB +import LIO -- The type of Wasm values. -- MiniWasm only supports 32-bit and 64-bit integers. @@ -16,8 +18,16 @@ type FuncName = String -- The name of a function. -- These are all newtypes over '[ValueType]'. -- Their purpose is to make programs written in the AST look closer to actual Wasm programs. -- You can either pattern-match on the constructors, or use the .unwrap field to access the actual lists. -newtype Params = Params { unwrap ::[ValueType] } deriving (Show, Eq) -newtype Results = Results { unwrap :: [ValueType] } deriving (Show, Eq) +-- 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 Results l = Results { unwrap :: [Labeled l ValueType] } +instance Label l => Show (Results l) where + show (Results p) = show $ map showTCB p + newtype Locals = Locals { unwrap :: [ValueType] } deriving (Show, Eq) -- Numeric binary operators. @@ -40,7 +50,7 @@ data RelOp deriving (Show, Eq) -- MiniWasm instructions. -data Instr +data Instr l = Nop -- Do nothing. | Drop -- Drop the top-most value from the stack. | Unreachable -- This instruction traps when executed. Used to mark unreachable code paths. @@ -60,30 +70,28 @@ data Instr | I32_Load -- Load a value from the linear memory at the address popped from the stack, and push it onto the stack. | I32_Store -- Store a value at the specified adress in memory. Both the value and the address are popped from the stack. - | Block Params Results [Instr] -- Execute the list of instructions in a block with the specified block type. Branching to a block jumps to the end of the block. - | Loop Params Results [Instr] -- Execute the list of instructions in a loop with the specified block type. Branching to a loop jumps back to the beginning of the loop. + | Block (Params l) (Results l) [Instr l] -- Execute the list of instructions in a block with the specified block type. Branching to a block jumps to the end of the block. + | Loop (Params l) (Results l) [Instr l] -- Execute the list of instructions in a loop with the specified block type. Branching to a loop jumps back to the beginning of the loop. | Br LabelIndex -- Branch to the label with the specified index. Labels are indexed using DeBruijn indices, so the nearest label has index 0. | BrIf LabelIndex -- Pop an I32 from the stack, and branch to the specified label only if the value is non-zero. | Call FuncName -- Call the specified function. | Return -- Return from the current function. - deriving (Show, Eq) + deriving Show -- Function definitions. -data Func = +data Func l = Func { name :: FuncName -- The name of the function - , params :: Params -- The types of the function's parameters. - , results :: Results -- The types of the function's results. + , params :: Params l -- The types of the function's parameters. + , results :: Results l -- The types of the function's results. , locals :: Locals -- The types of the function's local variables. - , body :: [Instr] -- The body of the function. + , body :: [Instr l] -- The body of the function. } - deriving (Show, Eq) -- MiniWasm modules ("programs"). -data Module = +data Module l = Module { initialMemory :: [Int32] -- The initial contents of the module's linear memory. - , funcs :: [Func] -- The functions defined inside the module. + , funcs :: [Func l] -- The functions defined inside the module. } - deriving Show diff --git a/src/MiniWasm/TestCases/Programs.hs b/src/MiniWasm/TestCases/Programs.hs index 99a2e4f..5580bb9 100644 --- a/src/MiniWasm/TestCases/Programs.hs +++ b/src/MiniWasm/TestCases/Programs.hs @@ -1,251 +1,251 @@ module MiniWasm.TestCases.Programs where -import MiniWasm.Syntax -import MiniWasm.Execution -import MiniWasm.TestCases.SmallStep((~>)) +-- import MiniWasm.Syntax +-- import MiniWasm.Execution +-- import MiniWasm.TestCases.SmallStep((~>)) --- This file contains a few example MiniWasm modules, which also serve as test cases for the interpreter. --- You're free to modify them (or add new ones) to help you when solving the assignment. --- However, your solution will be graded only based on the original test cases, plus some test cases that are not present here. +-- -- This file contains a few example MiniWasm modules, which also serve as test cases for the interpreter. +-- -- You're free to modify them (or add new ones) to help you when solving the assignment. +-- -- However, your solution will be graded only based on the original test cases, plus some test cases that are not present here. --- If you're writing a new module, don't forget to add it to this list. --- It's a list of nested tuples, because it's going to be used with 'lookup' which expected a list of (key, value) pairs. -testPrograms :: [(String, (Module, ExpectedOutput))] -testPrograms = - [ "simpleAdd" ~> simpleAdd ~> ExpectStack [V_I32 6] - , "isEven" ~> isEven ~> ExpectStack [V_I32 0, V_I32 1] - , "factorial" ~> factorial ~> ExpectStack [V_I32 120] - , "factorial64" ~> factorial64 ~> ExpectStack [V_I64 120] - , "factorialRecursive" ~> factorialRecursive ~> ExpectStack [V_I32 720, V_I32 120] - , "memorySimple" ~> memorySimple ~> ExpectStack [V_I32 11, V_I32 10, V_I32 2, V_I32 1, V_I32 10] - , "localsSimple" ~> localsSimple ~> ExpectStack [V_I32 5, V_I32 0] - , "localsFunction" ~> localsFunction ~> ExpectStack [V_I32 5, V_I32 9, V_I32 0] +-- -- If you're writing a new module, don't forget to add it to this list. +-- -- It's a list of nested tuples, because it's going to be used with 'lookup' which expected a list of (key, value) pairs. +-- testPrograms :: [(String, (Module, ExpectedOutput))] +-- testPrograms = +-- [ "simpleAdd" ~> simpleAdd ~> ExpectStack [V_I32 6] +-- , "isEven" ~> isEven ~> ExpectStack [V_I32 0, V_I32 1] +-- , "factorial" ~> factorial ~> ExpectStack [V_I32 120] +-- , "factorial64" ~> factorial64 ~> ExpectStack [V_I64 120] +-- , "factorialRecursive" ~> factorialRecursive ~> ExpectStack [V_I32 720, V_I32 120] +-- , "memorySimple" ~> memorySimple ~> ExpectStack [V_I32 11, V_I32 10, V_I32 2, V_I32 1, V_I32 10] +-- , "localsSimple" ~> localsSimple ~> ExpectStack [V_I32 5, V_I32 0] +-- , "localsFunction" ~> localsFunction ~> ExpectStack [V_I32 5, V_I32 9, V_I32 0] - , "unreachable" ~> unreachable ~> ExpectTrap UnreachableExecuted - , "loadOutOfBounds" ~> loadOutOfBounds ~> ExpectTrap MemoryOutOfBounds - , "storeOutOfBounds" ~> storeOutOfBounds ~> ExpectTrap MemoryOutOfBounds - ] +-- , "unreachable" ~> unreachable ~> ExpectTrap UnreachableExecuted +-- , "loadOutOfBounds" ~> loadOutOfBounds ~> ExpectTrap MemoryOutOfBounds +-- , "storeOutOfBounds" ~> storeOutOfBounds ~> ExpectTrap MemoryOutOfBounds +-- ] -data ExpectedOutput - = ExpectStack [Value] -- Expect the program to succeed with the specified output stack. - | ExpectTrap TrapReason -- Expect the program to trap for the specified reason. +-- data ExpectedOutput +-- = ExpectStack [Value] -- Expect the program to succeed with the specified output stack. +-- | ExpectTrap TrapReason -- Expect the program to trap for the specified reason. -simpleAdd :: Module -simpleAdd = - Module - [] - [ Func "main" (Params []) (Results [I32]) (Locals []) - [ I32_Const 1 - , I32_Const 2 - , I32_Const 3 - , I32_BinOp Add - , I32_BinOp Add - ] - ] +-- simpleAdd :: Module +-- simpleAdd = +-- Module +-- [] +-- [ Func "main" (Params []) (Results [I32]) (Locals []) +-- [ I32_Const 1 +-- , I32_Const 2 +-- , I32_Const 3 +-- , I32_BinOp Add +-- , I32_BinOp Add +-- ] +-- ] -isEven :: Module -isEven = - Module - [] - [ Func "isEven" (Params [I32]) (Results [I32]) (Locals []) - [ LocalGet 0 - , I32_Const 2 - , I32_BinOp Rem +-- isEven :: Module +-- isEven = +-- Module +-- [] +-- [ Func "isEven" (Params [I32]) (Results [I32]) (Locals []) +-- [ LocalGet 0 +-- , I32_Const 2 +-- , I32_BinOp Rem - , I32_Const 0 - , I32_RelOp Eq - ] - , Func "main" (Params []) (Results [I32, I32]) (Locals []) - [ I32_Const 4 - , Call "isEven" +-- , I32_Const 0 +-- , I32_RelOp Eq +-- ] +-- , Func "main" (Params []) (Results [I32, I32]) (Locals []) +-- [ I32_Const 4 +-- , Call "isEven" - , I32_Const 7 - , Call "isEven" - ] - ] +-- , I32_Const 7 +-- , Call "isEven" +-- ] +-- ] -factorial :: Module -factorial = - Module - [] - [ Func "factorial" (Params [I32]) (Results [I32]) (Locals []) - [ I32_Const 1 - , Block (Params [I32]) (Results [I32]) - [ Loop (Params [I32]) (Results [I32]) - [ LocalGet 0 - , I32_Const 0 - , I32_RelOp Le - , BrIf 1 +-- factorial :: Module +-- factorial = +-- Module +-- [] +-- [ Func "factorial" (Params [I32]) (Results [I32]) (Locals []) +-- [ I32_Const 1 +-- , Block (Params [I32]) (Results [I32]) +-- [ Loop (Params [I32]) (Results [I32]) +-- [ LocalGet 0 +-- , I32_Const 0 +-- , I32_RelOp Le +-- , BrIf 1 - , LocalGet 0 - , LocalGet 0 - , I32_Const 1 - , I32_BinOp Sub - , LocalSet 0 - , I32_BinOp Mul +-- , LocalGet 0 +-- , LocalGet 0 +-- , I32_Const 1 +-- , I32_BinOp Sub +-- , LocalSet 0 +-- , I32_BinOp Mul - , Br 0 - ] - ] - ] - , Func "main" (Params []) (Results [I32]) (Locals []) - [ I32_Const 5 - , Call "factorial" - ] - ] +-- , Br 0 +-- ] +-- ] +-- ] +-- , Func "main" (Params []) (Results [I32]) (Locals []) +-- [ I32_Const 5 +-- , Call "factorial" +-- ] +-- ] --- Same as 'factorial', but with I64 everywhere -factorial64 :: Module -factorial64 = - Module - [] - [ Func "factorial" (Params [I64]) (Results [I64]) (Locals []) - [ I64_Const 1 - , Block (Params [I64]) (Results [I64]) - [ Loop (Params [I64]) (Results [I64]) - [ LocalGet 0 - , I64_Const 0 - , I64_RelOp Le - , BrIf 1 +-- -- Same as 'factorial', but with I64 everywhere +-- factorial64 :: Module +-- factorial64 = +-- Module +-- [] +-- [ Func "factorial" (Params [I64]) (Results [I64]) (Locals []) +-- [ I64_Const 1 +-- , Block (Params [I64]) (Results [I64]) +-- [ Loop (Params [I64]) (Results [I64]) +-- [ LocalGet 0 +-- , I64_Const 0 +-- , I64_RelOp Le +-- , BrIf 1 - , LocalGet 0 - , LocalGet 0 - , I64_Const 1 - , I64_BinOp Sub - , LocalSet 0 - , I64_BinOp Mul +-- , LocalGet 0 +-- , LocalGet 0 +-- , I64_Const 1 +-- , I64_BinOp Sub +-- , LocalSet 0 +-- , I64_BinOp Mul - , Br 0 - ] - ] - ] - , Func "main" (Params []) (Results [I64]) (Locals []) - [ I64_Const 5 - , Call "factorial" - ] - ] +-- , Br 0 +-- ] +-- ] +-- ] +-- , Func "main" (Params []) (Results [I64]) (Locals []) +-- [ I64_Const 5 +-- , Call "factorial" +-- ] +-- ] -factorialRecursive :: Module -factorialRecursive = - Module - [] - [ Func "factorial" (Params [I32]) (Results [I32]) (Locals []) - [ Block (Params []) (Results []) - [ LocalGet 0 - , I32_Const 0 - , I32_RelOp Le - , BrIf 0 +-- factorialRecursive :: Module +-- factorialRecursive = +-- Module +-- [] +-- [ Func "factorial" (Params [I32]) (Results [I32]) (Locals []) +-- [ Block (Params []) (Results []) +-- [ LocalGet 0 +-- , I32_Const 0 +-- , I32_RelOp Le +-- , BrIf 0 - , LocalGet 0 - , I32_Const 1 - , I32_BinOp Sub - , Call "factorial" +-- , LocalGet 0 +-- , I32_Const 1 +-- , I32_BinOp Sub +-- , Call "factorial" - , LocalGet 0 - , I32_BinOp Mul - , Return - ] - , I32_Const 1 - ] - , Func "main" (Params []) (Results [I32, I32]) (Locals []) - [ I32_Const 5 - , Call "factorial" +-- , LocalGet 0 +-- , I32_BinOp Mul +-- , Return +-- ] +-- , I32_Const 1 +-- ] +-- , Func "main" (Params []) (Results [I32, I32]) (Locals []) +-- [ I32_Const 5 +-- , Call "factorial" - , I32_Const 6 - , Call "factorial" - ] - ] +-- , I32_Const 6 +-- , Call "factorial" +-- ] +-- ] -localsSimple :: Module -localsSimple = - Module - [] - [ Func "main" (Params []) (Results [I32, I32]) (Locals [I32]) - [ LocalGet 0 +-- localsSimple :: Module +-- localsSimple = +-- Module +-- [] +-- [ Func "main" (Params []) (Results [I32, I32]) (Locals [I32]) +-- [ LocalGet 0 - , I32_Const 5 - , LocalSet 0 - , LocalGet 0 - ] - ] +-- , I32_Const 5 +-- , LocalSet 0 +-- , LocalGet 0 +-- ] +-- ] -localsFunction :: Module -localsFunction = - Module - [] - [ Func "f" (Params [I32]) (Results [I32]) (Locals [I32]) - [ LocalGet 0 - , I32_Const 1 - , I32_BinOp Sub +-- localsFunction :: Module +-- localsFunction = +-- Module +-- [] +-- [ Func "f" (Params [I32]) (Results [I32]) (Locals [I32]) +-- [ LocalGet 0 +-- , I32_Const 1 +-- , I32_BinOp Sub - , LocalSet 1 - , LocalGet 1 - ] +-- , LocalSet 1 +-- , LocalGet 1 +-- ] - , Func "main" (Params []) (Results [I32, I32, I32]) (Locals [I32]) - [ LocalGet 0 +-- , Func "main" (Params []) (Results [I32, I32, I32]) (Locals [I32]) +-- [ LocalGet 0 - , I32_Const 5 - , LocalSet 0 +-- , I32_Const 5 +-- , LocalSet 0 - , I32_Const 10 - , Call "f" +-- , I32_Const 10 +-- , Call "f" - , LocalGet 0 - ] - ] +-- , LocalGet 0 +-- ] +-- ] -memorySimple :: Module -memorySimple = - Module - [1 .. 10] - [ Func "main" (Params []) (Results [I32, I32, I32, I32, I32]) (Locals []) - [ MemSize +-- memorySimple :: Module +-- memorySimple = +-- Module +-- [1 .. 10] +-- [ Func "main" (Params []) (Results [I32, I32, I32, I32, I32]) (Locals []) +-- [ MemSize - , I32_Const 0 - , I32_Load +-- , I32_Const 0 +-- , I32_Load - , I32_Const 1 - , I32_Load +-- , I32_Const 1 +-- , I32_Load - , I32_Const 5 - , I32_Const 11 - , I32_Store +-- , I32_Const 5 +-- , I32_Const 11 +-- , I32_Store - , I32_Const 9 - , I32_Load +-- , I32_Const 9 +-- , I32_Load - , I32_Const 5 - , I32_Load - ] - ] +-- , I32_Const 5 +-- , I32_Load +-- ] +-- ] -unreachable :: Module -unreachable = - Module - [] - [ Func "main" (Params []) (Results [I32, I32, I32]) (Locals []) - [ Unreachable - ] - ] +-- unreachable :: Module +-- unreachable = +-- Module +-- [] +-- [ Func "main" (Params []) (Results [I32, I32, I32]) (Locals []) +-- [ Unreachable +-- ] +-- ] -loadOutOfBounds :: Module -loadOutOfBounds = - Module - [1, 2, 3] - [ Func "main" (Params []) (Results [I32]) (Locals []) - [ I32_Const 3 - , I32_Load - ] - ] +-- loadOutOfBounds :: Module +-- loadOutOfBounds = +-- Module +-- [1, 2, 3] +-- [ Func "main" (Params []) (Results [I32]) (Locals []) +-- [ I32_Const 3 +-- , I32_Load +-- ] +-- ] -storeOutOfBounds :: Module -storeOutOfBounds = - Module - [1, 2, 3] - [ Func "main" (Params []) (Results []) (Locals []) - [ I32_Const 3 - , I32_Const 0 - , I32_Store - ] - ] +-- storeOutOfBounds :: Module +-- storeOutOfBounds = +-- Module +-- [1, 2, 3] +-- [ Func "main" (Params []) (Results []) (Locals []) +-- [ I32_Const 3 +-- , I32_Const 0 +-- , I32_Store +-- ] +-- ] diff --git a/src/MiniWasm/TestCases/SmallStep.hs b/src/MiniWasm/TestCases/SmallStep.hs index 1468668..6255d4d 100644 --- a/src/MiniWasm/TestCases/SmallStep.hs +++ b/src/MiniWasm/TestCases/SmallStep.hs @@ -17,7 +17,7 @@ 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" @@ -45,7 +45,7 @@ smallStepTests = , Config [] [] [] [V_I64 3, V_I64 2] [Plain (I64_BinOp Add)] , Config [] [] [] [V_I64 5] [] ] - ] + ]-} {- , "LocalGet" ~> [ Config [] [] [V_I32 7] [] [Plain (LocalGet 0)] diff --git a/src/MiniWasm/Validation.hs b/src/MiniWasm/Validation.hs index 4d4bcf6..9fd2efe 100644 --- a/src/MiniWasm/Validation.hs +++ b/src/MiniWasm/Validation.hs @@ -4,6 +4,7 @@ import Data.Foldable(traverse_) import Data.List(nub) import MiniWasm.Syntax +import LIO -- This file implements a validation algorithm for MiniWasm. -- You don't need to read nor modify this file for the assignment, but skimming it @@ -82,7 +83,7 @@ data Context = , stack :: Stack } -validateInstr :: Context -> Instr -> Either ValidationError Stack +validateInstr :: Label l => Context -> Instr l -> Either ValidationError Stack validateInstr ctx instr = case instr of Nop -> Right ctx.stack @@ -159,13 +160,13 @@ validateInstr ctx instr = _ <- pop ctx.returnType ctx.stack return Any -validateInstrs :: Context -> [Instr] -> Either ValidationError Stack +validateInstrs :: Label l => Context -> [Instr l] -> Either ValidationError Stack validateInstrs ctx [] = Right ctx.stack validateInstrs ctx (instr : instrs) = do newStack <- validateInstr ctx instr validateInstrs ctx{stack = newStack} instrs -validateFunc :: [(FuncName, FuncType)] -> Func -> Either ValidationError () +validateFunc :: Label l => [(FuncName, FuncType)] -> Func l -> Either ValidationError () validateFunc funcTypes (Func name (Params params) (Results results) (Locals locals) body) = do let results' = reverse results @@ -175,7 +176,7 @@ validateFunc funcTypes (Func name (Params params) (Results results) (Locals loca stack <- validateInstrs ctx body popExact results' stack -validateModule :: Module -> Either ValidationError () +validateModule :: Label l => Module l -> Either ValidationError () validateModule m = let uniqueFuncs = nub $ fmap (\f -> f.name) m.funcs diff --git a/test/Main.hs b/test/Main.hs index c8f4ece..467a745 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -21,6 +21,7 @@ testSmallStep name cfgs = cfg' @=? step cfg go cfg' cfgs +{- testModule :: TestName -> Module -> ExpectedOutput -> TestTree testModule name m expectedOutput = testCase name $ do @@ -36,6 +37,7 @@ testModule name m expectedOutput = -- This case should never happen, unless you modify 'stepUntilFinal' or 'executeModule' _ -> assertFailure "Program is not in final state" +-} -- If you want to add a new test case, modify the 'testPrograms' list in the MiniWasm.TestCases.Programs module. testTree :: TestTree