binops
This commit is contained in:
parent
78b8e9ab07
commit
3024cd2ca1
@ -29,7 +29,7 @@ library
|
|||||||
hs-source-dirs: src
|
hs-source-dirs: src
|
||||||
exposed-modules:
|
exposed-modules:
|
||||||
MiniWasm.Syntax
|
MiniWasm.Syntax
|
||||||
MiniWasm.Validation
|
--MiniWasm.Validation
|
||||||
MiniWasm.Execution
|
MiniWasm.Execution
|
||||||
MiniWasm.TestCases.SmallStep
|
MiniWasm.TestCases.SmallStep
|
||||||
MiniWasm.TestCases.Programs
|
MiniWasm.TestCases.Programs
|
||||||
|
@ -8,10 +8,12 @@
|
|||||||
module MiniWasm.Execution where
|
module MiniWasm.Execution where
|
||||||
|
|
||||||
import Data.Int (Int32, Int64)
|
import Data.Int (Int32, Int64)
|
||||||
|
import LIO
|
||||||
import Data.Maybe (fromJust)
|
import Data.Maybe (fromJust)
|
||||||
|
|
||||||
import Debug.Trace qualified
|
import Debug.Trace qualified
|
||||||
import MiniWasm.Syntax
|
import MiniWasm.Syntax
|
||||||
|
import LIO.TCB
|
||||||
|
|
||||||
-- Wasm values
|
-- Wasm values
|
||||||
data Value
|
data Value
|
||||||
@ -19,6 +21,23 @@ data Value
|
|||||||
| V_I64 Int64
|
| V_I64 Int64
|
||||||
deriving (Show, Eq)
|
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:
|
-- Helper functions to manipulate MiniWasm values:
|
||||||
|
|
||||||
-- Gives the default value for each MiniWasm type.
|
-- Gives the default value for each MiniWasm type.
|
||||||
@ -60,6 +79,10 @@ _ !? _ = Nothing
|
|||||||
|
|
||||||
infixl 9 !? -- Same as !!
|
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.
|
-- 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.
|
-- You can use this when interpreting the I32_Store and LocalSet instructions.
|
||||||
updateAt :: Int -> a -> [a] -> Maybe [a]
|
updateAt :: Int -> a -> [a] -> Maybe [a]
|
||||||
@ -70,21 +93,21 @@ updateAt n a (a' : as)
|
|||||||
updateAt n a [] = Nothing
|
updateAt n a [] = Nothing
|
||||||
|
|
||||||
-- Administrative instructions.
|
-- Administrative instructions.
|
||||||
data AdminInstr
|
data AdminInstr l
|
||||||
= Plain Instr -- Regular instruction.
|
= Plain (Instr l) -- Regular instruction.
|
||||||
| -- Label frame.
|
| -- Label frame.
|
||||||
Label
|
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.
|
{ 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.
|
, 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.
|
| -- Function call frame.
|
||||||
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.
|
{ 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 :: [Value] -- The local variables of this function call.
|
||||||
, innerStack :: [Value] -- The inner stack 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:
|
| -- New administrative instructions:
|
||||||
-- Our interpreter implements control flow slightly differently from the
|
-- Our interpreter implements control flow slightly differently from the
|
||||||
@ -95,61 +118,113 @@ data AdminInstr
|
|||||||
Trapping TrapReason -- The program is trapping.
|
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 :: [Value]} -- The program is branching to label 'target' with args 'values'.
|
||||||
| Returning {results :: [Value]} -- The program is returning 'results' from a function.
|
| 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.
|
-- Reasons for which the program can trap.
|
||||||
data TrapReason
|
data TrapReason
|
||||||
= UnreachableExecuted -- An 'Unreachable' instruction was executed.
|
= UnreachableExecuted -- An 'Unreachable' instruction was executed.
|
||||||
| MemoryOutOfBounds -- A memory load or store was out of bounds.
|
| MemoryOutOfBounds -- A memory load or store was out of bounds.
|
||||||
deriving (Show, Eq)
|
deriving Show
|
||||||
|
|
||||||
-- Configurations
|
-- Configurations
|
||||||
--
|
--
|
||||||
-- The configuration represents the state of a running MiniWasm program.
|
-- The configuration represents the state of a running MiniWasm program.
|
||||||
-- For simplicity, we use an _explicit_ value stack in our interpreter:
|
-- For simplicity, we use an _explicit_ value stack in our interpreter:
|
||||||
-- instructions push/pop values from this stack.
|
-- instructions push/pop values from this stack.
|
||||||
data Config = Config
|
data Config l = Config
|
||||||
{ funcs :: [(FuncName, Func)] -- Function lookup map. You can use the 'lookup' function to find a function by its name.
|
{ funcs :: [(FuncName, Func l)] -- Function lookup map. You can use the 'lookup' function to find a function by its name.
|
||||||
, memory :: [Int32] -- Linear memory.
|
, memory :: [Int32] -- Linear memory.
|
||||||
, locals :: [Value] -- Local variables.
|
, locals :: [Labeled l Value] -- Local variables.
|
||||||
, stack :: [Value] -- Explicit value stack.
|
, stack :: [Labeled l Value] -- Explicit value stack.
|
||||||
, instrs :: [AdminInstr] -- Next instructions to be executed.
|
, instrs :: [AdminInstr l] -- Next instructions to be executed.
|
||||||
|
, progcn :: l
|
||||||
}
|
}
|
||||||
deriving (Show, Eq)
|
|
||||||
|
|
||||||
-- The small-step evaluation function.
|
-- The small-step evaluation function.
|
||||||
--
|
--
|
||||||
-- Replace the TODO stubs in this function with your code.
|
-- Replace the TODO stubs in this function with your code.
|
||||||
step :: Config -> Config
|
step :: Label l => Config l -> LIO l (Config l)
|
||||||
step cfg =
|
step cfg = do
|
||||||
case cfg.instrs of
|
case cfg.instrs of
|
||||||
[] -> 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 $
|
||||||
case instr of
|
case instr of
|
||||||
Plain instr ->
|
Plain instr ->
|
||||||
case (instr, cfg.stack) of
|
case (instr, cfg.stack) of
|
||||||
(Nop, _) -> cfg{instrs} -- Evaluating Nop does nothing, so just update the list of remaining instructions.
|
(Nop, _) -> return 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.
|
(Drop, _ : stack) -> return cfg{stack, instrs} -- Evaluating Drop just pops and discards the top value from the stack.
|
||||||
(Unreachable, _) -> cfg{instrs = [Trapping UnreachableExecuted]}
|
(Unreachable, _) -> return cfg{instrs = [Trapping UnreachableExecuted]}
|
||||||
(I32_Const i, stack) -> cfg{stack = V_I32 i : stack, instrs}
|
(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.
|
-- 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, V_I32 b : V_I32 a : stack) -> cfg{stack = V_I32 (evalBinOp op a b) : stack, instrs}
|
(I32_BinOp op, b : a : stack) -> do
|
||||||
(I32_RelOp op, V_I32 b : V_I32 a : stack) -> cfg{stack = boolToI32 (evalRelOp op a b) : stack, instrs}
|
a' <- unlabel a
|
||||||
(I64_Const i, stack) -> cfg{stack = V_I64 i : stack, instrs}
|
b' <- unlabel b
|
||||||
(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}
|
v <- label (labelOf a `lub` labelOf b) $ case (a', b') of
|
||||||
_ -> error "Missing or ill-typed operand(s) on the stack"
|
(V_I32 a'', V_I32 b'') -> V_I32 $ evalBinOp op a'' b''
|
||||||
-- Administrative instructions:
|
(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
|
-- This function checks whether the configuration has reached a final state, i.e. whether the
|
||||||
-- program has been executed to completion.
|
-- program has been executed to completion.
|
||||||
isFinalState :: Config -> Bool
|
isFinalState :: Label l => Config l -> Bool
|
||||||
isFinalState cfg =
|
isFinalState cfg =
|
||||||
case cfg.instrs of
|
case cfg.instrs of
|
||||||
[] -> True -- If there are no more instructions to execute, we've reached a final state.
|
[] -> True -- If there are no more instructions to execute, we've reached a final state.
|
||||||
@ -157,22 +232,24 @@ isFinalState cfg =
|
|||||||
_ -> False
|
_ -> False
|
||||||
|
|
||||||
-- This function will repeatedly apply the 'step' function until the program reaches a final state.
|
-- This function will repeatedly apply the 'step' function until the program reaches a final state.
|
||||||
stepUntilFinal :: Config -> Config
|
stepUntilFinal :: Label l => Config l -> LIO l (Config l)
|
||||||
stepUntilFinal cfg =
|
stepUntilFinal cfg = do
|
||||||
if isFinalState cfg
|
if isFinalState cfg
|
||||||
then cfg
|
then return cfg
|
||||||
else stepUntilFinal (step cfg)
|
else do
|
||||||
|
step' <- step cfg
|
||||||
|
stepUntilFinal step'
|
||||||
|
|
||||||
-- This function creates an initial configuration and executes the given program to completion.
|
-- 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 =
|
executeModule m =
|
||||||
let
|
let
|
||||||
funcMap = fmap (\f -> (f.name, f)) m.funcs
|
funcMap = fmap (\f -> (f.name, f)) m.funcs
|
||||||
initialConfig =
|
initialConfig =
|
||||||
Config{funcs = funcMap, memory = m.initialMemory, locals = [], stack = [], instrs = [Plain (Call "main")]}
|
Config{funcs = funcMap, memory = m.initialMemory, locals = [], stack = [], instrs = [Plain (Call "main")]}
|
||||||
in
|
in let state = LIOState High High
|
||||||
stepUntilFinal initialConfig
|
in evalLIO (stepUntilFinal initialConfig) state -}
|
||||||
|
|
||||||
debug :: AdminInstr -> Config -> a -> a
|
debug :: Label l => AdminInstr l -> Config l -> a -> a
|
||||||
debug instr cfg =
|
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")
|
||||||
|
@ -1,6 +1,8 @@
|
|||||||
module MiniWasm.Syntax where
|
module MiniWasm.Syntax where
|
||||||
|
|
||||||
import Data.Int(Int32, Int64)
|
import Data.Int(Int32, Int64)
|
||||||
|
import LIO.TCB
|
||||||
|
import LIO
|
||||||
|
|
||||||
-- The type of Wasm values.
|
-- The type of Wasm values.
|
||||||
-- MiniWasm only supports 32-bit and 64-bit integers.
|
-- 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]'.
|
-- These are all newtypes over '[ValueType]'.
|
||||||
-- Their purpose is to make programs written in the AST look closer to actual Wasm programs.
|
-- 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.
|
-- 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)
|
-- Labeled l
|
||||||
newtype Results = Results { unwrap :: [ValueType] } deriving (Show, Eq)
|
-- 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)
|
newtype Locals = Locals { unwrap :: [ValueType] } deriving (Show, Eq)
|
||||||
|
|
||||||
-- Numeric binary operators.
|
-- Numeric binary operators.
|
||||||
@ -40,7 +50,7 @@ data RelOp
|
|||||||
deriving (Show, Eq)
|
deriving (Show, Eq)
|
||||||
|
|
||||||
-- MiniWasm instructions.
|
-- MiniWasm instructions.
|
||||||
data Instr
|
data Instr l
|
||||||
= Nop -- Do nothing.
|
= Nop -- Do nothing.
|
||||||
| Drop -- Drop the top-most value from the stack.
|
| Drop -- Drop the top-most value from the stack.
|
||||||
| Unreachable -- This instruction traps when executed. Used to mark unreachable code paths.
|
| 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_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.
|
| 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.
|
| 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 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.
|
| 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.
|
| 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.
|
| 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.
|
| Call FuncName -- Call the specified function.
|
||||||
| Return -- Return from the current function.
|
| Return -- Return from the current function.
|
||||||
deriving (Show, Eq)
|
deriving Show
|
||||||
|
|
||||||
-- Function definitions.
|
-- Function definitions.
|
||||||
data Func =
|
data Func l =
|
||||||
Func
|
Func
|
||||||
{ name :: FuncName -- The name of the function
|
{ name :: FuncName -- The name of the function
|
||||||
, params :: Params -- The types of the function's parameters.
|
, params :: Params l -- The types of the function's parameters.
|
||||||
, results :: Results -- The types of the function's results.
|
, results :: Results l -- The types of the function's results.
|
||||||
, locals :: Locals -- The types of the function's local variables.
|
, 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").
|
-- MiniWasm modules ("programs").
|
||||||
data Module =
|
data Module l =
|
||||||
Module
|
Module
|
||||||
{ initialMemory :: [Int32] -- The initial contents of the module's linear memory.
|
{ 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
|
|
||||||
|
@ -1,251 +1,251 @@
|
|||||||
module MiniWasm.TestCases.Programs where
|
module MiniWasm.TestCases.Programs where
|
||||||
|
|
||||||
import MiniWasm.Syntax
|
-- import MiniWasm.Syntax
|
||||||
import MiniWasm.Execution
|
-- import MiniWasm.Execution
|
||||||
import MiniWasm.TestCases.SmallStep((~>))
|
-- import MiniWasm.TestCases.SmallStep((~>))
|
||||||
|
|
||||||
-- This file contains a few example MiniWasm modules, which also serve as test cases for the interpreter.
|
-- -- 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.
|
-- -- 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.
|
-- -- 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.
|
-- -- 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.
|
-- -- 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 :: [(String, (Module, ExpectedOutput))]
|
||||||
testPrograms =
|
-- testPrograms =
|
||||||
[ "simpleAdd" ~> simpleAdd ~> ExpectStack [V_I32 6]
|
-- [ "simpleAdd" ~> simpleAdd ~> ExpectStack [V_I32 6]
|
||||||
, "isEven" ~> isEven ~> ExpectStack [V_I32 0, V_I32 1]
|
-- , "isEven" ~> isEven ~> ExpectStack [V_I32 0, V_I32 1]
|
||||||
, "factorial" ~> factorial ~> ExpectStack [V_I32 120]
|
-- , "factorial" ~> factorial ~> ExpectStack [V_I32 120]
|
||||||
, "factorial64" ~> factorial64 ~> ExpectStack [V_I64 120]
|
-- , "factorial64" ~> factorial64 ~> ExpectStack [V_I64 120]
|
||||||
, "factorialRecursive" ~> factorialRecursive ~> ExpectStack [V_I32 720, V_I32 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]
|
-- , "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]
|
-- , "localsSimple" ~> localsSimple ~> ExpectStack [V_I32 5, V_I32 0]
|
||||||
, "localsFunction" ~> localsFunction ~> ExpectStack [V_I32 5, V_I32 9, V_I32 0]
|
-- , "localsFunction" ~> localsFunction ~> ExpectStack [V_I32 5, V_I32 9, V_I32 0]
|
||||||
|
|
||||||
, "unreachable" ~> unreachable ~> ExpectTrap UnreachableExecuted
|
-- , "unreachable" ~> unreachable ~> ExpectTrap UnreachableExecuted
|
||||||
, "loadOutOfBounds" ~> loadOutOfBounds ~> ExpectTrap MemoryOutOfBounds
|
-- , "loadOutOfBounds" ~> loadOutOfBounds ~> ExpectTrap MemoryOutOfBounds
|
||||||
, "storeOutOfBounds" ~> storeOutOfBounds ~> ExpectTrap MemoryOutOfBounds
|
-- , "storeOutOfBounds" ~> storeOutOfBounds ~> ExpectTrap MemoryOutOfBounds
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
data ExpectedOutput
|
-- data ExpectedOutput
|
||||||
= ExpectStack [Value] -- Expect the program to succeed with the specified output stack.
|
-- = ExpectStack [Value] -- Expect the program to succeed with the specified output stack.
|
||||||
| ExpectTrap TrapReason -- Expect the program to trap for the specified reason.
|
-- | ExpectTrap TrapReason -- Expect the program to trap for the specified reason.
|
||||||
|
|
||||||
simpleAdd :: Module
|
-- simpleAdd :: Module
|
||||||
simpleAdd =
|
-- simpleAdd =
|
||||||
Module
|
-- Module
|
||||||
[]
|
-- []
|
||||||
[ Func "main" (Params []) (Results [I32]) (Locals [])
|
-- [ Func "main" (Params []) (Results [I32]) (Locals [])
|
||||||
[ I32_Const 1
|
-- [ I32_Const 1
|
||||||
, I32_Const 2
|
-- , I32_Const 2
|
||||||
, I32_Const 3
|
-- , I32_Const 3
|
||||||
, I32_BinOp Add
|
-- , I32_BinOp Add
|
||||||
, I32_BinOp Add
|
-- , I32_BinOp Add
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
isEven :: Module
|
-- isEven :: Module
|
||||||
isEven =
|
-- isEven =
|
||||||
Module
|
-- Module
|
||||||
[]
|
-- []
|
||||||
[ Func "isEven" (Params [I32]) (Results [I32]) (Locals [])
|
-- [ Func "isEven" (Params [I32]) (Results [I32]) (Locals [])
|
||||||
[ LocalGet 0
|
-- [ LocalGet 0
|
||||||
, I32_Const 2
|
-- , I32_Const 2
|
||||||
, I32_BinOp Rem
|
-- , I32_BinOp Rem
|
||||||
|
|
||||||
, I32_Const 0
|
-- , I32_Const 0
|
||||||
, I32_RelOp Eq
|
-- , I32_RelOp Eq
|
||||||
]
|
-- ]
|
||||||
, Func "main" (Params []) (Results [I32, I32]) (Locals [])
|
-- , Func "main" (Params []) (Results [I32, I32]) (Locals [])
|
||||||
[ I32_Const 4
|
-- [ I32_Const 4
|
||||||
, Call "isEven"
|
-- , Call "isEven"
|
||||||
|
|
||||||
, I32_Const 7
|
-- , I32_Const 7
|
||||||
, Call "isEven"
|
-- , Call "isEven"
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
factorial :: Module
|
-- factorial :: Module
|
||||||
factorial =
|
-- factorial =
|
||||||
Module
|
-- Module
|
||||||
[]
|
-- []
|
||||||
[ Func "factorial" (Params [I32]) (Results [I32]) (Locals [])
|
-- [ Func "factorial" (Params [I32]) (Results [I32]) (Locals [])
|
||||||
[ I32_Const 1
|
-- [ I32_Const 1
|
||||||
, Block (Params [I32]) (Results [I32])
|
-- , Block (Params [I32]) (Results [I32])
|
||||||
[ Loop (Params [I32]) (Results [I32])
|
-- [ Loop (Params [I32]) (Results [I32])
|
||||||
[ LocalGet 0
|
-- [ LocalGet 0
|
||||||
, I32_Const 0
|
-- , I32_Const 0
|
||||||
, I32_RelOp Le
|
-- , I32_RelOp Le
|
||||||
, BrIf 1
|
-- , BrIf 1
|
||||||
|
|
||||||
, LocalGet 0
|
-- , LocalGet 0
|
||||||
, LocalGet 0
|
-- , LocalGet 0
|
||||||
, I32_Const 1
|
-- , I32_Const 1
|
||||||
, I32_BinOp Sub
|
-- , I32_BinOp Sub
|
||||||
, LocalSet 0
|
-- , LocalSet 0
|
||||||
, I32_BinOp Mul
|
-- , I32_BinOp Mul
|
||||||
|
|
||||||
, Br 0
|
-- , Br 0
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
, Func "main" (Params []) (Results [I32]) (Locals [])
|
-- , Func "main" (Params []) (Results [I32]) (Locals [])
|
||||||
[ I32_Const 5
|
-- [ I32_Const 5
|
||||||
, Call "factorial"
|
-- , Call "factorial"
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
-- Same as 'factorial', but with I64 everywhere
|
-- -- Same as 'factorial', but with I64 everywhere
|
||||||
factorial64 :: Module
|
-- factorial64 :: Module
|
||||||
factorial64 =
|
-- factorial64 =
|
||||||
Module
|
-- Module
|
||||||
[]
|
-- []
|
||||||
[ Func "factorial" (Params [I64]) (Results [I64]) (Locals [])
|
-- [ Func "factorial" (Params [I64]) (Results [I64]) (Locals [])
|
||||||
[ I64_Const 1
|
-- [ I64_Const 1
|
||||||
, Block (Params [I64]) (Results [I64])
|
-- , Block (Params [I64]) (Results [I64])
|
||||||
[ Loop (Params [I64]) (Results [I64])
|
-- [ Loop (Params [I64]) (Results [I64])
|
||||||
[ LocalGet 0
|
-- [ LocalGet 0
|
||||||
, I64_Const 0
|
-- , I64_Const 0
|
||||||
, I64_RelOp Le
|
-- , I64_RelOp Le
|
||||||
, BrIf 1
|
-- , BrIf 1
|
||||||
|
|
||||||
, LocalGet 0
|
-- , LocalGet 0
|
||||||
, LocalGet 0
|
-- , LocalGet 0
|
||||||
, I64_Const 1
|
-- , I64_Const 1
|
||||||
, I64_BinOp Sub
|
-- , I64_BinOp Sub
|
||||||
, LocalSet 0
|
-- , LocalSet 0
|
||||||
, I64_BinOp Mul
|
-- , I64_BinOp Mul
|
||||||
|
|
||||||
, Br 0
|
-- , Br 0
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
, Func "main" (Params []) (Results [I64]) (Locals [])
|
-- , Func "main" (Params []) (Results [I64]) (Locals [])
|
||||||
[ I64_Const 5
|
-- [ I64_Const 5
|
||||||
, Call "factorial"
|
-- , Call "factorial"
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
factorialRecursive :: Module
|
-- factorialRecursive :: Module
|
||||||
factorialRecursive =
|
-- factorialRecursive =
|
||||||
Module
|
-- Module
|
||||||
[]
|
-- []
|
||||||
[ Func "factorial" (Params [I32]) (Results [I32]) (Locals [])
|
-- [ Func "factorial" (Params [I32]) (Results [I32]) (Locals [])
|
||||||
[ Block (Params []) (Results [])
|
-- [ Block (Params []) (Results [])
|
||||||
[ LocalGet 0
|
-- [ LocalGet 0
|
||||||
, I32_Const 0
|
-- , I32_Const 0
|
||||||
, I32_RelOp Le
|
-- , I32_RelOp Le
|
||||||
, BrIf 0
|
-- , BrIf 0
|
||||||
|
|
||||||
, LocalGet 0
|
-- , LocalGet 0
|
||||||
, I32_Const 1
|
-- , I32_Const 1
|
||||||
, I32_BinOp Sub
|
-- , I32_BinOp Sub
|
||||||
, Call "factorial"
|
-- , Call "factorial"
|
||||||
|
|
||||||
, LocalGet 0
|
-- , LocalGet 0
|
||||||
, I32_BinOp Mul
|
-- , I32_BinOp Mul
|
||||||
, Return
|
-- , Return
|
||||||
]
|
-- ]
|
||||||
, I32_Const 1
|
-- , I32_Const 1
|
||||||
]
|
-- ]
|
||||||
, Func "main" (Params []) (Results [I32, I32]) (Locals [])
|
-- , Func "main" (Params []) (Results [I32, I32]) (Locals [])
|
||||||
[ I32_Const 5
|
-- [ I32_Const 5
|
||||||
, Call "factorial"
|
-- , Call "factorial"
|
||||||
|
|
||||||
, I32_Const 6
|
-- , I32_Const 6
|
||||||
, Call "factorial"
|
-- , Call "factorial"
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
localsSimple :: Module
|
-- localsSimple :: Module
|
||||||
localsSimple =
|
-- localsSimple =
|
||||||
Module
|
-- Module
|
||||||
[]
|
-- []
|
||||||
[ Func "main" (Params []) (Results [I32, I32]) (Locals [I32])
|
-- [ Func "main" (Params []) (Results [I32, I32]) (Locals [I32])
|
||||||
[ LocalGet 0
|
-- [ LocalGet 0
|
||||||
|
|
||||||
, I32_Const 5
|
-- , I32_Const 5
|
||||||
, LocalSet 0
|
-- , LocalSet 0
|
||||||
, LocalGet 0
|
-- , LocalGet 0
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
localsFunction :: Module
|
-- localsFunction :: Module
|
||||||
localsFunction =
|
-- localsFunction =
|
||||||
Module
|
-- Module
|
||||||
[]
|
-- []
|
||||||
[ Func "f" (Params [I32]) (Results [I32]) (Locals [I32])
|
-- [ Func "f" (Params [I32]) (Results [I32]) (Locals [I32])
|
||||||
[ LocalGet 0
|
-- [ LocalGet 0
|
||||||
, I32_Const 1
|
-- , I32_Const 1
|
||||||
, I32_BinOp Sub
|
-- , I32_BinOp Sub
|
||||||
|
|
||||||
, LocalSet 1
|
-- , LocalSet 1
|
||||||
, LocalGet 1
|
-- , LocalGet 1
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
, Func "main" (Params []) (Results [I32, I32, I32]) (Locals [I32])
|
-- , Func "main" (Params []) (Results [I32, I32, I32]) (Locals [I32])
|
||||||
[ LocalGet 0
|
-- [ LocalGet 0
|
||||||
|
|
||||||
, I32_Const 5
|
-- , I32_Const 5
|
||||||
, LocalSet 0
|
-- , LocalSet 0
|
||||||
|
|
||||||
, I32_Const 10
|
-- , I32_Const 10
|
||||||
, Call "f"
|
-- , Call "f"
|
||||||
|
|
||||||
, LocalGet 0
|
-- , LocalGet 0
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
memorySimple :: Module
|
-- memorySimple :: Module
|
||||||
memorySimple =
|
-- memorySimple =
|
||||||
Module
|
-- Module
|
||||||
[1 .. 10]
|
-- [1 .. 10]
|
||||||
[ Func "main" (Params []) (Results [I32, I32, I32, I32, I32]) (Locals [])
|
-- [ Func "main" (Params []) (Results [I32, I32, I32, I32, I32]) (Locals [])
|
||||||
[ MemSize
|
-- [ MemSize
|
||||||
|
|
||||||
, I32_Const 0
|
-- , I32_Const 0
|
||||||
, I32_Load
|
-- , I32_Load
|
||||||
|
|
||||||
, I32_Const 1
|
-- , I32_Const 1
|
||||||
, I32_Load
|
-- , I32_Load
|
||||||
|
|
||||||
, I32_Const 5
|
-- , I32_Const 5
|
||||||
, I32_Const 11
|
-- , I32_Const 11
|
||||||
, I32_Store
|
-- , I32_Store
|
||||||
|
|
||||||
, I32_Const 9
|
-- , I32_Const 9
|
||||||
, I32_Load
|
-- , I32_Load
|
||||||
|
|
||||||
, I32_Const 5
|
-- , I32_Const 5
|
||||||
, I32_Load
|
-- , I32_Load
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
unreachable :: Module
|
-- unreachable :: Module
|
||||||
unreachable =
|
-- unreachable =
|
||||||
Module
|
-- Module
|
||||||
[]
|
-- []
|
||||||
[ Func "main" (Params []) (Results [I32, I32, I32]) (Locals [])
|
-- [ Func "main" (Params []) (Results [I32, I32, I32]) (Locals [])
|
||||||
[ Unreachable
|
-- [ Unreachable
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
loadOutOfBounds :: Module
|
-- loadOutOfBounds :: Module
|
||||||
loadOutOfBounds =
|
-- loadOutOfBounds =
|
||||||
Module
|
-- Module
|
||||||
[1, 2, 3]
|
-- [1, 2, 3]
|
||||||
[ Func "main" (Params []) (Results [I32]) (Locals [])
|
-- [ Func "main" (Params []) (Results [I32]) (Locals [])
|
||||||
[ I32_Const 3
|
-- [ I32_Const 3
|
||||||
, I32_Load
|
-- , I32_Load
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
|
||||||
storeOutOfBounds :: Module
|
-- storeOutOfBounds :: Module
|
||||||
storeOutOfBounds =
|
-- storeOutOfBounds =
|
||||||
Module
|
-- Module
|
||||||
[1, 2, 3]
|
-- [1, 2, 3]
|
||||||
[ Func "main" (Params []) (Results []) (Locals [])
|
-- [ Func "main" (Params []) (Results []) (Locals [])
|
||||||
[ I32_Const 3
|
-- [ I32_Const 3
|
||||||
, I32_Const 0
|
-- , I32_Const 0
|
||||||
, I32_Store
|
-- , I32_Store
|
||||||
]
|
-- ]
|
||||||
]
|
-- ]
|
||||||
|
@ -17,7 +17,7 @@ infixr 5 ~>
|
|||||||
-- You can add your own or modify them, but be careful: Unlike the full program tests, these Configs
|
-- 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
|
-- 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".
|
-- unhelpful error like "ill-typed operands on the stack".
|
||||||
|
{-
|
||||||
smallStepTests :: [(String, [Config])]
|
smallStepTests :: [(String, [Config])]
|
||||||
smallStepTests =
|
smallStepTests =
|
||||||
[ "Nop"
|
[ "Nop"
|
||||||
@ -45,7 +45,7 @@ smallStepTests =
|
|||||||
, Config [] [] [] [V_I64 3, V_I64 2] [Plain (I64_BinOp Add)]
|
, Config [] [] [] [V_I64 3, V_I64 2] [Plain (I64_BinOp Add)]
|
||||||
, Config [] [] [] [V_I64 5] []
|
, Config [] [] [] [V_I64 5] []
|
||||||
]
|
]
|
||||||
]
|
]-}
|
||||||
{-
|
{-
|
||||||
, "LocalGet"
|
, "LocalGet"
|
||||||
~> [ Config [] [] [V_I32 7] [] [Plain (LocalGet 0)]
|
~> [ Config [] [] [V_I32 7] [] [Plain (LocalGet 0)]
|
||||||
|
@ -4,6 +4,7 @@ import Data.Foldable(traverse_)
|
|||||||
import Data.List(nub)
|
import Data.List(nub)
|
||||||
|
|
||||||
import MiniWasm.Syntax
|
import MiniWasm.Syntax
|
||||||
|
import LIO
|
||||||
|
|
||||||
-- This file implements a validation algorithm for MiniWasm.
|
-- This file implements a validation algorithm for MiniWasm.
|
||||||
-- You don't need to read nor modify this file for the assignment, but skimming it
|
-- You don't need to read nor modify this file for the assignment, but skimming it
|
||||||
@ -82,7 +83,7 @@ data Context =
|
|||||||
, stack :: Stack
|
, stack :: Stack
|
||||||
}
|
}
|
||||||
|
|
||||||
validateInstr :: Context -> Instr -> Either ValidationError Stack
|
validateInstr :: Label l => Context -> Instr l -> Either ValidationError Stack
|
||||||
validateInstr ctx instr =
|
validateInstr ctx instr =
|
||||||
case instr of
|
case instr of
|
||||||
Nop -> Right ctx.stack
|
Nop -> Right ctx.stack
|
||||||
@ -159,13 +160,13 @@ validateInstr ctx instr =
|
|||||||
_ <- pop ctx.returnType ctx.stack
|
_ <- pop ctx.returnType ctx.stack
|
||||||
return Any
|
return Any
|
||||||
|
|
||||||
validateInstrs :: Context -> [Instr] -> Either ValidationError Stack
|
validateInstrs :: Label l => Context -> [Instr l] -> Either ValidationError Stack
|
||||||
validateInstrs ctx [] = Right ctx.stack
|
validateInstrs ctx [] = Right ctx.stack
|
||||||
validateInstrs ctx (instr : instrs) = do
|
validateInstrs ctx (instr : instrs) = do
|
||||||
newStack <- validateInstr ctx instr
|
newStack <- validateInstr ctx instr
|
||||||
validateInstrs ctx{stack = newStack} instrs
|
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
|
validateFunc funcTypes (Func name (Params params) (Results results) (Locals locals) body) = do
|
||||||
let
|
let
|
||||||
results' = reverse results
|
results' = reverse results
|
||||||
@ -175,7 +176,7 @@ validateFunc funcTypes (Func name (Params params) (Results results) (Locals loca
|
|||||||
stack <- validateInstrs ctx body
|
stack <- validateInstrs ctx body
|
||||||
popExact results' stack
|
popExact results' stack
|
||||||
|
|
||||||
validateModule :: Module -> Either ValidationError ()
|
validateModule :: Label l => Module l -> Either ValidationError ()
|
||||||
validateModule m =
|
validateModule m =
|
||||||
let
|
let
|
||||||
uniqueFuncs = nub $ fmap (\f -> f.name) m.funcs
|
uniqueFuncs = nub $ fmap (\f -> f.name) m.funcs
|
||||||
|
@ -21,6 +21,7 @@ testSmallStep name cfgs =
|
|||||||
cfg' @=? step cfg
|
cfg' @=? step cfg
|
||||||
go cfg' cfgs
|
go cfg' cfgs
|
||||||
|
|
||||||
|
{-
|
||||||
testModule :: TestName -> Module -> ExpectedOutput -> TestTree
|
testModule :: TestName -> Module -> ExpectedOutput -> TestTree
|
||||||
testModule name m expectedOutput =
|
testModule name m expectedOutput =
|
||||||
testCase name $ do
|
testCase name $ do
|
||||||
@ -36,6 +37,7 @@ testModule name m expectedOutput =
|
|||||||
|
|
||||||
-- This case should never happen, unless you modify 'stepUntilFinal' or 'executeModule'
|
-- This case should never happen, unless you modify 'stepUntilFinal' or 'executeModule'
|
||||||
_ -> assertFailure "Program is not in final state"
|
_ -> 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.
|
-- If you want to add a new test case, modify the 'testPrograms' list in the MiniWasm.TestCases.Programs module.
|
||||||
testTree :: TestTree
|
testTree :: TestTree
|
||||||
|
Loading…
x
Reference in New Issue
Block a user