Commit bfb2e769 authored by Katharina Brandl's avatar Katharina Brandl
Browse files

small fixes and documentation

parent b2385129
Pipeline #136123 failed with stages
in 76 minutes and 53 seconds
......@@ -43,8 +43,7 @@ import qualified Data.Vector as Vec
import Data.Bits
import Language.Wasm.FloatUtils
import Language.Wasm.Interpreter (ModuleInstance)
import Language.Wasm.Interpreter (asInt32,asInt64,asWord32,asWord64,nearest,
import Language.Wasm.Interpreter (ModuleInstance, asInt32,asInt64,asWord32,asWord64,nearest,
floatFloor, doubleFloor, floatCeil, doubleCeil,
floatTrunc, doubleTrunc, zeroAwareMin, zeroAwareMax)
import qualified Language.Wasm.Interpreter as Wasm
......@@ -296,8 +295,8 @@ instance (ArrowChoice c, ArrowFail Err c, Fail.Join Value c) => IsVal Value (Val
(BS64, Wasm.VI64 val) -> returnA -< float64 $ wordToDouble val
_ -> returnA -< error "fReinterpretI: cannot apply operator to given argument."
listLookup sCont eCont = proc (Value v,xs,x) -> case v of
(Wasm.VI32 val) -> if (fromIntegral val) < length xs
then sCont -< xs !! (fromIntegral val)
(Wasm.VI32 val) -> if fromIntegral val < length xs
then sCont -< xs !! fromIntegral val
else eCont -< x
_ -> returnA -< error "listLookup: cannot apply operator to given arguments."
......@@ -306,9 +305,6 @@ instance (ArrowExcept (Exc Value) c) => IsException (Exc Value) Value (ValueT Va
exception = arr id
handleException = id
instance Arrow c => IsErr Err (ValueT Value c) where
err = arr id
type Result = (Error
Err
(JoinVector Value,
......
......@@ -53,9 +53,10 @@ import Text.Printf
import GHC.Generics
import GHC.Exts
-- the kind of exceptions that can be thrown
-- | the kind of exceptions that can be thrown
data Exc v = Jump Natural [v] | CallReturn [v] deriving (Show, Eq, Generic)
-- | unrecoverable errors
data Err = Trap String | InvocationError String deriving (Show, Eq, Generic)
instance Hashable v => Hashable (Exc v)
......@@ -66,31 +67,17 @@ class ArrowExcept exc c => IsException exc v c | c -> v where
exception :: c (Exc v) exc
handleException :: JoinExc y c => c (Exc v, x) y -> c (exc,x) y
class IsErr err c | c -> err where
err :: c Err err
-- | fail with a trap
trap :: (Fail.Join x c, ArrowFail Err c) => c String x
trap = proc s -> fail -< (Trap s)
trap :: (Fail.Join x c, ArrowFail err c, IsErr err c) => c String x
trap = proc s -> fail <<< err -< (Trap s)
-- | fail with an invocation error
invocationError :: (Fail.Join x c, ArrowFail Err c) => c String x
invocationError = proc s -> fail -< (InvocationError s)
invocationError :: (Fail.Join x c, ArrowFail err c, IsErr err c) => c String x
invocationError = proc s -> fail <<< err -< (InvocationError s)
-- stores a frame's static data (return arity and module instance)
-- | stores a frame's static data (return arity and module instance)
type FrameData = (Natural, ModuleInstance)
---- constraints to support (and call) host functions
--type HostFunctionSupport addr bytes v c = (ArrowApply c, ArrowGlobalState v m c, ArrowWasmMemory m addr bytes v c)
---- a host function is a function from a list of values (parameters) to a list of values (return values)
--newtype HostFunction v c = HostFunction (
-- forall addr bytes. HostFunctionSupport addr bytes v c => (c [v] [v]) )
--
--instance Show (HostFunction v c) where
-- show _ = "HostFunction"
type ArrowWasmMemory addr bytes sz v c =
( ArrowMemory addr bytes sz c,
ArrowEffectiveAddress v Natural addr c,
......@@ -110,11 +97,12 @@ type ArrowDynamicComponents v addr bytes sz exc e c =
ArrowWasmMemory addr bytes sz v c,
IsVal v c,
ArrowExcept exc c, IsException exc v c,
ArrowFail e c, IsErr e c,
ArrowFail Err c,
ArrowFix (c [Instruction Natural] ()),
?fixpointAlgorithm :: FixpointAlgorithm (Fix (c [Instruction Natural] ())))
-- | the language interface
class Show v => IsVal v c | c -> v where
type family JoinVal y (c :: * -> * -> *) :: Constraint
......@@ -142,14 +130,17 @@ class Show v => IsVal v c | c -> v where
iReinterpretF :: c (BitSize, v) v
fReinterpretI :: c (BitSize, v) v
i32ifNeqz :: (JoinVal y c) => c x y -> c x y -> c (v, x) y
-- | `listLookup f g (v, xs, x)`
-- | Looks up the `v`-th element in `xs` and passes it to `f`, or
-- | passes `x` to `g` if `v` is out of range of `xs`.
-- | listLookup f g (v, xs, x):
-- Looks up the `v`-th element in `xs` and passes it to `f`, or
-- passes `x` to `g` if `v` is out of range of `xs`.
listLookup :: (JoinVal y c) => c x y -> c x y -> c (v, [x], x) y
ifHasType :: c x y -> c x y -> c (v, ValueType, x) y
-- entry point to the generic interpreter
-- | entry point to the generic interpreter
--
-- invokes the function with the given name and the arguments
-- the module instance comes from ArrowFrame
-- ArrowGlobalState and ArrowWasmMemory are properly initialized
-- argument Text: name of the function to execute
......@@ -173,6 +164,7 @@ invokeExported = proc (funcName, args) -> do
Just (ExportInstance _ (ExternFunction addr)) -> invokeExternal -< (addr, args)
_ -> invocationError -< printf "Function with name %s was not found in module's exports" (show funcName)
-- | invokes function with the given static index and the arguments
invokeExternal ::
( ArrowChoice c,
ArrowStaticComponents v c, ArrowDynamicComponents v addr bytes sz exc e c,
......@@ -212,7 +204,7 @@ invokeExternal = proc (funcAddr, args) -> do
-< (args, paramTys)
f -< x
-- | evaluates the list of instructions in the context provided by arrow c
eval ::
( ArrowChoice c,
ArrowStaticComponents v c, ArrowDynamicComponents v addr bytes sz exc e c,
......@@ -297,7 +289,7 @@ invokeChecked ::
( ArrowChoice c,
ArrowStaticComponents v c,
IsVal v c, ArrowExcept exc c, IsException exc v c, JoinExc () c, Exc.Join () c, Fail.Join () c,
ArrowFail err c, IsErr err c)
ArrowFail Err c)
=> c [Instruction Natural] () -> c (Int, FuncType) ()
invokeChecked eval' = proc (addr, ftExpect) -> do
funcData@(ftActual,_,_) <- readFunction -< addr
......@@ -308,12 +300,13 @@ invokeChecked eval' = proc (addr, ftExpect) -> do
then f -< x
else trap -< printf "Mismatched function type in indirect call. Expected %s, actual %s." (show ftExpect) (show ftActual)
-- invoke function with code code within module instance funcModInst
-- the function execution can finish by different reasons:
-- - all instructions have been executed -> result are the top |resultTys| values on the stack
-- - the function calls return -> result are the top |resultTys| values on the stack
-- - the function produces a trap -> no result, trap is propagated
-- - TODO: what about break? Can we "break" to a function boundary? -> NO, only to block boundaries
-- | invoke function with code code within module instance funcModInst
--
-- the function execution can finish by different reasons:
--
-- * all instructions have been executed -> result are the top |resultTys| values on the stack
-- * the function calls return -> result are the top |resultTys| values on the stack
-- * the function produces a trap -> no result, trap is propagated
invoke ::
( ArrowChoice c, ArrowStack v c, ArrowJumpTypes c,
IsVal v c, ArrowFrame FrameData v c, ArrowExcept exc c, IsException exc v c, Exc.Join y c,
......@@ -327,7 +320,7 @@ invoke eval' = catch
result <- inNewFrame (localNoJumpTypes $ localFreshStack $ label eval' eval') -< ((rtLength, funcModInst), vs ++ zeros, (resultTys, code, []))
returnA -< result
)
(proc (_,e) -> handleException $
(proc (_,e) -> handleException
(proc (exc,_) -> case exc of
CallReturn vs -> do
pushn -< vs
......@@ -343,20 +336,19 @@ invoke eval' = catch
F32 -> f32const -< 0
F64 -> f64const -< 0
-- | jumps to the enclosing block with given index
branch :: (ArrowChoice c, ArrowExcept exc c, IsException exc v c, ArrowStack v c, ArrowJumpTypes c) => c Natural ()
branch = proc ix -> do
rt <- jumpType -< ix
vs <- popn -< fromIntegral $ length $ rt
vs <- popn -< fromIntegral $ length rt
throw <<< exception -< Jump ix vs
-- | Introduces a branching point `g` that can be jumped to from within `f`.
-- | When escalating jumps, all label-local operands must be popped from the stack.
-- | This implementation assumes that ArrowExcept discards label-local operands in ArrowStack upon throw.
-- When escalating jumps, all label-local operands must be popped from the stack.
-- This implementation assumes that ArrowExcept discards label-local operands in ArrowStack upon throw.
label :: (ArrowChoice c, ArrowExcept exc c, IsException exc v c, ArrowStack v c, ArrowJumpTypes c, Exc.Join z c,
ArrowStack v c, Show v, JoinExc z c)
=> c x z -> c y z -> c (ResultType, x, y) z
-- x: code to execute
-- y: continuation to execute after a break to the current label
label f g = catch
-- after executing f without a break we expect |rt| results on top of the stack
(proc (rt,x,_) -> do
......@@ -364,7 +356,7 @@ label f g = catch
returnA -< result
)
-- after a break the results are popped from the stack and passed back via exception e
(proc ((_,_,y),e) -> handleException $
(proc ((_,_,y),e) -> handleException
(proc (exc,y) -> case exc of
Jump 0 vs -> do
pushn -< vs
......@@ -433,12 +425,7 @@ memoryIndex = proc () -> do
(_,modInst) <- frameData -< ()
returnA -< memaddrs modInst ! 0
--withCurrentMemory :: (ArrowChoice c, ArrowGlobalState v m c, ArrowMemory addr bytes c, ArrowFrame FrameData v c) => c (m,x) (m,y) -> c x y
--withCurrentMemory f = proc x -> do
-- (_,modInst) <- frameData -< ()
-- let memAddr = memaddrs modInst ! 0
-- withMemoryInstance f -< (memAddr, x)
-- | loads byteSize bytes from memory and converts it to valType, the resulting value is pushed to the stack
load ::
( ArrowChoice c,
ArrowStaticComponents v c, ArrowDynamicComponents v addr bytes sz exc e c,
......@@ -456,6 +443,7 @@ load byteSize loadType valType = proc off -> do
(proc addr -> trap -< printf "Memory access out of bounds: Cannot read %d bytes at address %s in current memory" byteSize (show addr))
-< (memIndex, addr, byteSize, addr)
-- | stores a value into the memory, value and memory address are read from the stack
store ::
( ArrowChoice c,
ArrowStaticComponents v c, ArrowDynamicComponents v addr bytes sz exc e c,
......@@ -498,7 +486,7 @@ evalVariableInst = proc i -> case i of
evalNumericInst ::
( ArrowChoice c, ArrowStack v c, ArrowExcept exc c, IsException exc v c, IsVal v c, Show v, JoinVal v c,
Fail.Join v c, IsErr err c, ArrowFail err c)
Fail.Join v c, ArrowFail Err c)
=> c (Instruction Natural) v
evalNumericInst = proc i -> case i of
I32Const lit _ -> i32const -< lit
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
module Stack where
import Control.Category
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Except
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Trans
import Control.Arrow.Transformer.State
import Control.Arrow.Utils
import Data.Profunctor
import Data.Coerce
import Numeric.Natural (Natural)
class ArrowStack v c | c -> v where
push :: c v ()
pop :: c () v
peek :: c () v
ifEmpty :: c x y -> c x y -> c x y
localFreshStack :: c x y -> c x y
pop2 :: ArrowChoice c => c () (v, v)
pop2 = proc _ -> do
v2 <- pop -< ()
v1 <- pop -< ()
returnA -< (v1, v2)
popn :: ArrowChoice c => c Natural [v]
popn = proc n -> case n of
0 -> returnA -< []
_ -> do
v <- pop -< ()
vs <- popn -< n-1
returnA -< v:vs
pushn :: ArrowChoice c => c [v] ()
pushn = proc vs -> case vs of
[] -> returnA -< ()
v:vs' -> do
pushn -< vs'
push -< v
-- | Arrow transformer that adds a stack to a computation.
newtype StackT v c x y = StackT (StateT [v] c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowTrans,ArrowLift,ArrowRun,
ArrowConst r, ArrowReader r, ArrowFail e, ArrowExcept e, ArrowState [v])
-- | Execute a computation and only return the result value and store.
runStackT :: StackT v c x y -> c ([v], x) ([v], y)
runStackT = coerce
{-# INLINE runStackT #-}
-- | Execute a computation and only return the result value.
evalStackT :: (Profunctor c) => StackT v c x y -> c ([v], x) y
evalStackT f = rmap pi2 (runStackT f)
-- | Execute a computation and only return the result store.
execStackT :: (Profunctor c) => StackT v c x y -> c ([v], x) [v]
execStackT f = rmap pi1 (runStackT f)
instance (ArrowChoice c, Profunctor c) => ArrowStack v (StackT v c) where
push = StackT $ modify $ arr $ \(v,st) -> ((), v:st)
pop = StackT $ modify $ arr $ \((),v:st) -> (v, st)
peek = StackT $ get >>^ head
ifEmpty (StackT f) (StackT g) = StackT $ proc x -> do
st <- get -< ()
case st of
[] -> g -< x
_ -> f -< x
localFreshStack (StackT f) = StackT $ proc x -> do
st <- get -< ()
put -< []
y <- f -< x
put -< st
returnA -< y
pop2 = StackT $ modify $ arr $ \((),v2:v1:st) -> ((v1,v2), st)
popn = StackT $ modify $ arr $ \(n,st) -> splitAt (fromIntegral n) st
pushn = StackT $ modify $ arr $ \(st',st) -> ((),st'++st)
instance ArrowFix (Underlying (StackT v c) x y) => ArrowFix (StackT v c x y) where
type Fix (StackT v c x y) = Fix (Underlying (StackT v c) x y)--StackT v (Fix c ([v],x) ([v],y))
......@@ -15,12 +15,12 @@ import Prelude as P
import Abstract
import Data
import GenericInterpreter hiding (Exc,Err)
import GenericInterpreter hiding (Exc)
import qualified GenericInterpreter as Generic
import TaintAnalysisValue hiding (Value)
import qualified TaintAnalysisValue as Taint
import qualified UnitAnalysis as Abs
import UnitAnalysisValue(Exc(..),Err)
import UnitAnalysisValue(Exc(..))
import qualified UnitAnalysisValue as Abs
import Control.Arrow.Fix as Fix
......@@ -72,10 +72,10 @@ type In = (Errors Err,
(StaticGlobalState Value,
(JoinList Value, ([ResultType], [Instruction Natural])))))))
type Out = (Errors Err, (Terminating
type Out = (Errors Err, Terminating
(JoinVector Value,
(StaticGlobalState Value,
Except (Exc Value) (JoinList Value, ())))))
Except (Exc Value) (JoinList Value, ()))))
type Result = (CFG (Instruction Natural), (Errors Err,
......@@ -92,8 +92,6 @@ invokeExported :: StaticGlobalState Value
-> Result
invokeExported initialStore tab modInst funcName args =
let ?cacheWidening = (W.finite,W.finite) in
--let ?fixpointAlgorithm = Function.fix in -- TODO: we need something else here
--let algo = (trace p1 p2) . (Fix.filter isRecursive $ innermost) in
let algo = recordControlFlowGraph' getExpression . Fix.filter isRecursive innermost in
let ?fixpointAlgorithm = fixpointAlgorithm algo in
(\(cfg,(_,res)) -> (cfg,res)) $ Trans.run
......
......@@ -12,7 +12,7 @@
{-# OPTIONS_GHC -fno-warn-orphans #-}
module TaintAnalysisValue where
import GenericInterpreter hiding (Exc,Err)
import GenericInterpreter hiding (Exc)
import Data(joinList1'')
import qualified UnitAnalysisValue as Abs
......@@ -74,25 +74,12 @@ liftValueT1 :: (ValueT v c x y -> ValueT v c x' y') -> (ValueT (Value v) c x y -
liftValueT1 = coerce
{-# INLINE liftValueT1 #-}
--instance (ArrowExcept (Exc Value) c, ArrowChoice c) => IsException (Exc Value) (Value v) (ValueT (Value v) c) where
-- exception = proc (Exc (Value v)) ->
-- liftValueT exception -< (Exc v)
instance (Hashable v, ArrowExcept (Abs.Exc (Value v)) c, ArrowChoice c) => IsException (Abs.Exc (Value v)) (Value v) (ValueT (Value v) c) where
type JoinExc y (ValueT (Value v) c) = ArrowComplete y (ValueT (Value v) c)
exception = arr $ Abs.Exc . HashSet.singleton
handleException f = proc (Abs.Exc excs,x) ->
joinList1'' f -< (HashSet.toList excs,x)
--instance (ArrowExcept (Exc (Value v)) c) => IsException (Exc (Value v)) (Value v) (ValueT (Value v) c) where
-- type JoinExc y (ValueT (Value v) c) = ()
-- exception = arr id
-- handleException = id
instance Arrow c => IsErr Abs.Err (ValueT (Value v) c) where
--err = arr $ Abs.Err . Pow.singleton
err = arr id
instance (JoinVal v (ValueT v c), IsVal v (ValueT v c), ArrowChoice c) => IsVal (Value v) (ValueT (Value v) c) where
type JoinVal y (ValueT (Value v) c) = JoinVal y (ValueT v c)
......@@ -109,12 +96,6 @@ instance (JoinVal v (ValueT v c), IsVal v (ValueT v c), ArrowChoice c) => IsVal
v <- liftValueT iBinOp -< (bs,op,v1,v2)
returnA -< Value (t1 t2) v
-- iBinOp eCont sCont = proc (bs,op,Value t1 v1, Value t2 v2,x) ->
-- liftValueT (iBinOp
-- (proc (op,v1,v2,(t1,t2,_,x)) -> (unliftValueT eCont) -< (op,Value t1 v1,Value t2 v2,x))
-- (proc (v,(_,_,t,x)) -> (unliftValueT sCont) -< (Value t v,x)))
-- -< (bs,op,v1,v2,(t1,t2,t1 ⊔ t2,x))
iRelOp = proc (bs,op,Value t1 v1, Value t2 v2) -> do
v <- liftValueT iRelOp -< (bs,op,v1,v2)
returnA -< Value (t1 t2) v
......
......@@ -16,7 +16,7 @@ module UnitAnalysis where
import Abstract
import Data
import GenericInterpreter hiding (Exc,Err)
import GenericInterpreter hiding (Exc)
import qualified GenericInterpreter as Generic
import UnitAnalysisValue
......
......@@ -11,7 +11,7 @@ module UnitAnalysisValue where
import Abstract
import Data(joinList1'',Instruction)
import GenericInterpreter hiding (Exc,Err)
import GenericInterpreter hiding (Exc)
import qualified GenericInterpreter as Generic
import Control.Arrow
......@@ -33,9 +33,6 @@ import Text.Printf
newtype Exc v = Exc (HashSet (Generic.Exc v)) deriving (Eq, Show, Hashable, PreOrd, Complete)
--newtype Err = Err (Pow Generic.Err) deriving (Eq, Show, Hashable, PreOrd, Complete)
type Err = Generic.Err
instance (Show v) => Pretty (Exc v) where pretty = viaShow
instance (Show n) => Pretty (Instruction n) where pretty = viaShow
......@@ -44,14 +41,8 @@ instance (ArrowExcept (Exc Value) c, ArrowChoice c) => IsException (Exc Value) V
type JoinExc y (ValueT Value c) = ArrowComplete y (ValueT Value c)
exception = arr $ Exc . HashSet.singleton
handleException f = proc (Exc excs,x) -> do
--ys <- mapList f -< (HashSet.toList excs,x)
--joinList _j -< (_init,ys)
joinList1'' f -< (HashSet.toList excs,x)
instance Arrow c => IsErr Err (ValueT Value c) where
--err = arr $ Err . Pow.singleton
err = arr id
newtype Value = Value (BaseValue () () () ()) deriving (Eq, Show, Hashable, PreOrd, Complete, Pretty)
valueI32, valueI64, valueF32, valueF64 :: Value
......
......@@ -30,29 +30,29 @@ runFunc modName funcName args = do
return $ invokeExported staticS mems tabs modInst (pack funcName) args
succResult :: Result -> [Value]
succResult (Success (_,(_,(_,(_,(Success (_,result))))))) = result
succResult (Success (_,(_,(_,(_,Success (_,result)))))) = result
succResult _ = error "not defined"
spec :: Spec
spec = do
it "run noop" $ do
result <- runFunc "simple" "noop" []
(succResult result) `shouldBe` [Value $ Wasm.VI32 0]
succResult result `shouldBe` [Value $ Wasm.VI32 0]
it "run const" $ do
result <- runFunc "simple" "const" [Value $ Wasm.VI32 5]
(succResult result) `shouldBe` [Value $ Wasm.VI32 5]
succResult result `shouldBe` [Value $ Wasm.VI32 5]
it "run fac-rec" $ do
let params = map (singleton . Value . Wasm.VI64) [0 .. 8]
results <- mapM (runFunc "fact" "fac-rec") params
let rs = map succResult results
rs `shouldBe` (map (singleton . Value . Wasm.VI64) [1,1,2,6,24,120,720,5040,40320])
rs `shouldBe` map (singleton . Value . Wasm.VI64) [1,1,2,6,24,120,720,5040,40320]
it "run test-mem" $ do
result <- runFunc "simple" "test-mem" [Value $ Wasm.VI32 42]
(succResult result) `shouldBe` [Value $ Wasm.VI32 43]
succResult result `shouldBe` [Value $ Wasm.VI32 43]
it "run test-call-indirect" $ do
result <- runFunc "simple" "test-call-indirect" []
(succResult result) `shouldBe` [Value $ Wasm.VI32 0]
succResult result `shouldBe` [Value $ Wasm.VI32 0]
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment