Commit 8a0672c2 authored by Katharina Brandl's avatar Katharina Brandl
Browse files

Tables and indirect calls + testcases.

parent 90b124ea
Pipeline #117921 passed with stages
in 72 minutes and 21 seconds
......@@ -15,7 +15,6 @@ import Control.Arrow.Transformer.Abstract.Except as AE
import Control.Arrow.Transformer.Concrete.Except as CE
import Control.Arrow.Transformer.Kleisli
import Control.Arrow.Transformer.Reader
--import Control.Arrow.Transformer.Stack
import Control.Arrow.Transformer.State
import Control.Arrow.Transformer.Value
import Control.Arrow.Transformer.Writer
......@@ -54,35 +53,23 @@ instance (Arrow c, Profunctor c, Functor f, ArrowMemory addr bytes c) => ArrowMe
(memstore (unlift a1) (unlift a2))-- >>^ moveIn
where moveIn (m, ey) = fmap ((,) m) ey
--deriving instance (Arrow c, ArrowMemory addr bytes c) => ArrowMemory addr bytes (StackT e c)
instance (Arrow c, ArrowMemory addr bytes c) => ArrowMemory addr bytes (StateT s c) where
type Join y (StateT s c) = Join (s,y) c
-- a1 :: StateT s c (bytes,x) y, a2 :: StateT s c x y
-- c1 :: c (s, (bytes,x)) (s,y), c2 :: c (s,x) (s,y)
-- memread :: c (bytes,x) y -> c x y -> c (m, (addr, Int, x)) (m,y)
-- memread on StateT :: StateT s c (bytes,x) y -> StateT s c x y -> StateT s c (m,(addr,Int,x)) (m,y)
-- StateT s c (m,(addr,bytes,x)) (m,y) has the form
-- StateT $ c (s,(m,(addr,Int,x))) (s,(m,y))
-- we need c (s, (m, (addr,Int,x))) (s, (m,y))
-- memread a1 a2 = lift $ proc (s, (m, (addr,i,x))) -> do
-- -- memread :: c (bytes,x) y -> c x y -> c (m, (addr, Int, x)) (m,y)
-- -- memread :: c (bytes,(s,x)) (s,y) -> c (s,x) (s,y) -> c (m, (addr, Int, (s,x))) (m, (s,y))
-- (newM, (newS,y)) <- memread (proc (bytes,(s,x)) -> unlift a1 -< (s, (bytes,x)))
-- (unlift a2)
-- -< (m, (addr,i,(s,x)))
-- returnA -< (newS, (newM, y))
--
-- memstore a1 a2 = lift $ proc (s, (m, (addr,bytes,x))) -> do
-- (newM, (newS,y)) <- memstore (unlift a1) (unlift a2) -< (m, (addr,bytes,(s,x)))
-- returnA -< (newS, (newM, y))
memread a1 a2 = lift $ proc (s, (ma,addr,i,x)) -> do
memread (proc (bytes,(s,x)) -> unlift a1 -< (s, (bytes,x)))
(unlift a2)
-< (ma,addr,i,(s,x))
memstore a1 a2 = lift $ proc (s, (ma,addr,bytes,x)) -> do
memstore (unlift a1) (unlift a2) -< (ma,addr,bytes,(s,x))
instance (Arrow c, ArrowMemory addr bytes c) => ArrowMemory addr bytes (ReaderT r c) where
type Join y (ReaderT r c) = Join y c
-- memread a1 a2 = lift $ proc (r, (m, (addr,i,x))) ->
-- memread (proc (bytes, (r,x)) -> unlift a1 -< (r, (bytes,x)))
-- (unlift a2)
-- -< (m, (addr,i,(r,x)))
-- memstore a1 a2 = lift $ proc (r, (m, (addr,bytes,x))) ->
-- memstore (unlift a1) (unlift a2) -< (m, (addr, bytes, (r,x)))
memread a1 a2 = lift $ proc (r, (ma,addr,i,x)) ->
memread (proc (bytes, (r,x)) -> unlift a1 -< (r, (bytes,x)))
(unlift a2)
-< (ma,addr,i,(r,x))
memstore a1 a2 = lift $ proc (r, (ma,addr,bytes,x)) ->
memstore (unlift a1) (unlift a2) -< (ma, addr, bytes, (r,x))
instance (ArrowMemory addr bytes c) => ArrowMemory addr bytes (WriterT r c) where
-- TODO
{-# LANGUAGE Arrows #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
......@@ -21,22 +22,36 @@ import Control.Arrow.Transformer.Writer
import Data.Profunctor
import GHC.Exts
class ArrowTable v c | c -> v where
type family JoinTable y (c :: * -> * -> *) :: Constraint
-- | readTable f g h (ta,ix,x)
-- | Lookup `ix` in table `ta` to retrieve the function address `fa`.
-- | Invokes `f (fa, x)` if all goes well.
-- | Invokes `g (ta,ix,x)` if `ix` is out of bounds.
-- | Invokes `h (ta,ix,x)` if `ix` cell is uninitialized.
readTable :: c (Int,x) y -> c (Int,v,x) y -> c (Int,v,x) y -> c (Int,v,x) y
readTable :: JoinTable y c => c (Int,x) y -> c (Int,v,x) y -> c (Int,v,x) y -> c (Int,v,x) y
deriving instance (ArrowTable v c) => ArrowTable v (ValueT val2 c)
deriving instance (Arrow c, Profunctor c, ArrowTable v c) => ArrowTable v (CE.ExceptT e c)
deriving instance (Arrow c, Profunctor c, ArrowTable v c) => ArrowTable v (AE.ExceptT e c)
instance (Arrow c, Profunctor c, Functor f, ArrowTable v c) => ArrowTable v (KleisliT f c) where
-- TODO
type JoinTable y (KleisliT f c) = JoinTable (f y) c
readTable f g h = lift $ readTable (unlift f) (unlift g) (unlift h)
instance (Arrow c, ArrowTable v c) => ArrowTable v (StateT s c) where
-- TODO
type JoinTable y (StateT s c) = JoinTable (s,y) c
readTable f g h = lift $ proc (s, (ta,ix,x)) ->
readTable (proc (i,(s,x)) -> unlift f -< (s,(i,x)))
(proc (i,v,(s,x)) -> unlift g -< (s,(i,v,x)))
(proc (i,v,(s,x)) -> unlift h -< (s,(i,v,x)))
-< (ta,ix,(s,x))
instance (Arrow c, ArrowTable v c) => ArrowTable v (ReaderT r c) where
-- TODO
type JoinTable y (ReaderT r c) = JoinTable y c
readTable f g h = lift $ proc (r,(ta,ix,x)) ->
readTable (proc (i,(r,x)) -> unlift f -< (r, (i,x)))
(proc (i,v,(r,x)) -> unlift g -< (r, (i,v,x)))
(proc (i,v,(r,x)) -> unlift h -< (r, (i,v,x)))
-< (ta,ix,(r,x))
instance (ArrowTable v c) => ArrowTable v (WriterT r c) where
-- TODO
......@@ -10,13 +10,14 @@
module Control.Arrow.Transformer.Abstract.Table where
import Abstract
import Data
import UnitAnalysisValue
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Except
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Fix hiding (filter)
import Control.Arrow.GlobalState
import Control.Arrow.Logger
import Control.Arrow.MemAddress
......@@ -33,26 +34,38 @@ import Control.Arrow.Table
import Control.Arrow.Trans
import Control.Arrow.WasmFrame
import Control.Arrow.Transformer.State
import Control.Arrow.Transformer.Reader
import Control.Category
import Control.Category (Category)
import Data.Maybe (catMaybes,isNothing)
import Data.Profunctor
import Data.Vector ((!), toList)
newtype TableT c x y = TableT (StateT Tables c x y)
import qualified Language.Wasm.Interpreter as Wasm
newtype TableT c x y = TableT (ReaderT Tables c x y)
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowLift,
ArrowFail e, ArrowExcept e, ArrowConst r, ArrowStore var' val', ArrowRun, ArrowFrame fd val,
ArrowStack st, ArrowReader r, ArrowStaticGlobalState val,
ArrowStack st, ArrowState s, ArrowStaticGlobalState val,
ArrowSerialize val dat valTy datDecTy datEncTy, ArrowJoin)
instance ArrowTrans TableT where
-- lift' :: c x y -> MemoryT v c x y
lift' a = TableT (lift' a)
instance ArrowTable Value (TableT c) where
-- TODO
instance (ArrowChoice c, Profunctor c) => ArrowTable Value (TableT c) where
type JoinTable y (TableT c) = ArrowComplete y c
readTable (TableT f) (TableT g) (TableT h) = TableT $ proc (ta,ix,x) -> do
(JoinVector tabs) <- ask -< ()
let (TableInst (Wasm.TableInstance _ tab)) = tabs ! ta
let tabList = toList tab
let funcs = catMaybes tabList
if any isNothing tabList
then (joinList1'' f -< (funcs,x)) <> (g -< (ta,ix,x)) <> (h -< (ta,ix,x))
else (joinList1'' f -< (funcs,x)) <> (g -< (ta,ix,x))
deriving instance (Arrow c, Profunctor c, ArrowComplete (Tables,y) c) => ArrowComplete y (TableT c)
deriving instance (Arrow c, Profunctor c, ArrowComplete y c) => ArrowComplete y (TableT c)
instance (ArrowLift c, ArrowFix (Underlying (TableT c) x y)) => ArrowFix (TableT c x y) where
type Fix (TableT c x y) = Fix (Underlying (TableT c) x y)
......@@ -35,6 +35,9 @@ import Control.Arrow.Transformer.State
import Control.Category
import Data.Profunctor
import Data.Vector as Vec
import qualified Language.Wasm.Interpreter as Wasm
newtype TableT c x y = TableT (StateT Tables c x y)
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowLift,
......@@ -42,8 +45,19 @@ newtype TableT c x y = TableT (StateT Tables c x y)
ArrowStack st, ArrowReader r, ArrowStaticGlobalState val,
ArrowSerialize val dat valTy datDecTy datEncTy)
instance ArrowTable Value (TableT c) where
-- TODO
instance (Profunctor c, ArrowChoice c) => ArrowTable Value (TableT c) where
type JoinTable y (TableT c) = ()
readTable (TableT f) (TableT g) (TableT h) = TableT $ proc (ta,i@(Value (Wasm.VI32 ix)),x) -> do
let ixI = fromIntegral ix
tabs <- get -< ()
let (TableInst (Wasm.TableInstance _ tab)) = tabs ! ta
if Vec.length tab <= ixI
then g -< (ta,i,x)
else do
let addr = tab ! ixI
case addr of
(Just a) -> f -< (a,x)
Nothing -> h -< (ta,i,x)
instance ArrowTrans TableT where
-- lift' :: c x y -> MemoryT v c x y
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
......@@ -5,6 +6,9 @@
module Data where
import Control.Arrow (ArrowChoice)
import Control.Arrow.Order(ArrowComplete,(<>))
import Control.Monad.State
import Data.Hashable
......@@ -72,6 +76,9 @@ data StaticGlobalState v = StaticGlobalState {
globalInstances :: Vector (GlobInst v)
} deriving (Show,Eq,Generic)
instance (Show v) => Pretty (StaticGlobalState v) where
pretty = viaShow
instance (PreOrd v) => PreOrd (StaticGlobalState v) where
(StaticGlobalState f1 g1) (StaticGlobalState f2 g2)
| f1 == f2 && Vec.length g1 == Vec.length g2 = Vec.all id $ Vec.zipWith () g1 g2
......@@ -299,6 +306,7 @@ convertInstruction i = case i of
Wasm.BrTable is i -> brTable is i
Wasm.Return -> return_
Wasm.Call i -> call i
Wasm.CallIndirect i -> callIndirect i
Wasm.Drop -> drop_
Wasm.Select -> select
Wasm.GetLocal i -> getLocal i
......@@ -382,6 +390,13 @@ data LoadType = L_I32 | L_I64 | L_F32 | L_F64 | L_I8S | L_I8U | L_I16S | L_I16U
data StoreType = S_I32 | S_I64 | S_F32 | S_F64 | S_I8 | S_I16
deriving Show
-- helper functions
joinList1'' :: (ArrowChoice c, ArrowComplete y c) => c (v,x) y -> c ([v],x) y
joinList1'' f = proc (vs,x) -> case vs of
[v] -> f -< (v,x)
(v:vss) -> (f -< (v,x)) <> (joinList1'' f -< (vss,x))
-- orphan instances
instance (Hashable v) => Hashable (Instruction v)
......
......@@ -168,7 +168,8 @@ invokeExported ::
Mem.Join () c,
JoinVal () c, Show v,
Fail.Join [v] c,
Fail.Join () c)
Fail.Join () c,
JoinTable () c)
=> c (Text, [v]) [v]
invokeExported = proc (funcName, args) -> do
(_, modInst) <- frameData -< () -- get the module instance
......@@ -185,7 +186,8 @@ invokeExternal ::
Mem.Join () c,
JoinVal () c, Show v,
Exc.Join () c,
Fail.Join () c)
Fail.Join () c,
JoinTable () c)
=> c (Int, [v]) [v]
invokeExternal = proc (funcAddr, args) ->
readFunction
......@@ -228,7 +230,8 @@ eval ::
JoinExc () c,
Mem.Join () c,
JoinVal () c, Show v,
Exc.Join () c)
Exc.Join () c,
JoinTable () c)
=> c [Instruction Natural] ()
eval = fix $ \eval' -> proc is -> do
--stack <- getStack -< ()
......@@ -271,7 +274,8 @@ evalControlInst ::
ArrowDynamicComponents v addr bytes exc e c,
JoinVal () c,
JoinExc () c,
Exc.Join () c)
Exc.Join () c,
JoinTable () c)
=> c [Instruction Natural] () -> c (Instruction Natural) ()
evalControlInst eval' = proc i -> case i of
Unreachable _ -> throw <<< exception -< Trap "Execution of unreachable instruction"
......
......@@ -115,10 +115,6 @@ mapList f = proc (as,x) -> do
b <- f -< (a,x)
returnA -< b:bs
joinList1'' :: (ArrowChoice c, ArrowComplete y c) => c (v,x) y -> c ([v],x) y
joinList1'' f = proc (vs,x) -> case vs of
[v] -> f -< (v,x)
(v:vss) -> (f -< (v,x)) <> (joinList1'' f -< (vss,x))
--joinList1'' f = proc (acc,bs) -> do
-- case bs of
-- [] -> returnA -< acc
......@@ -210,9 +206,18 @@ type Out = Terminating
Error
(Pow String)
(JoinVector Value,
(Tables,
--(Tables,
(StaticGlobalState Value,
Except (Exc Value) (JoinList Value, ())))))
Except (Exc Value) (JoinList Value, ()))))
type Result = Terminating
(Error
(Pow String)
(JoinVector Value,
--(Tables,
(StaticGlobalState Value,
Except (Exc Value) (JoinList Value, [Value]))))
invokeExported :: StaticGlobalState Value
-> Tables
......@@ -223,9 +228,9 @@ invokeExported :: StaticGlobalState Value
(Error
(Pow String)
(JoinVector Value,
(Tables,
--(Tables,
(StaticGlobalState Value,
Except (Exc Value) (JoinList Value, [Value])))))
Except (Exc Value) (JoinList Value, [Value]))))
invokeExported store tab modInst funcName args =
let ?cacheWidening = W.finite in
--let ?fixpointAlgorithm = Function.fix in -- TODO: we need something else here
......@@ -255,7 +260,7 @@ invokeExported store tab modInst funcName args =
isRecursive (_,(_,(_,(_,(_,(_,inst)))))) = case inst of
Loop {} : _ -> True
Call _ _ : _ -> True
CallIndirect _ _ : _ -> error "todo"
CallIndirect _ _ : _ -> True --error "todo"
_ -> False
p1 (locals,(_,(_,(stack,(la, instr))))) = --braces $ hsep (punctuate "," (pretty <$> toList stack))
hsep [pretty stack, pretty locals, pretty la, pretty instr]
......
......@@ -90,10 +90,15 @@ spec = do
let rs = map succResult results
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]
--
it "run test-mem" $ do
result <- runFunc "simple" "test-mem" [Value $ Wasm.VI32 42]
(succResult result) `shouldBe` [Value $ Wasm.VI32 43]
it "run test-call-indirect" $ do
result <- runFunc "simple" "test-call-indirect" []
--result `shouldSatisfy` (const False)
(succResult result) `shouldBe` [Value $ Wasm.VI32 0]
-- it "run test-br1" $ do
-- let path = "test/samples/simple.wast"
-- content <- LBS.readFile path
......
......@@ -5,7 +5,8 @@ module UnitSpec where
import Abstract (BaseValue(..))
import qualified Concrete as Concrete
import qualified ConcreteInterpreter as Concrete
import UnitAnalysis
import UnitAnalysis as U
import UnitAnalysisValue
import Soundness
import GenericInterpreter(Exc(..))
......@@ -50,14 +51,26 @@ readModule path = do
let Right validMod = validate m
return validMod
runFunc :: String -> String -> [Value] -> IO Result
runFunc modName funcName args = do
mod <- readModule ("test/samples/" ++ modName ++ ".wast")
Right (modInst, staticS, tabs) <- instantiateAbstract mod
return $ invokeExported staticS tabs modInst (pack funcName) args
succResult :: Result -> [Value]
succResult (Terminating (Success (_,(_,(Exc.Success (_,result)))))) = result
excResult :: Result -> Exc.Except (U.Exc Value) [Value]
excResult (Terminating (Success (_,(_,(Exc.Success (_,result)))))) = Exc.Success result
excResult (Terminating (Success (_,(_,(Exc.SuccessOrFail e (_,result)))))) = Exc.SuccessOrFail e result
excResult (Terminating (Success (_,(_,(Exc.Fail e))))) = Exc.Fail e
spec :: Spec
spec = do
it "" $ do
pending
--
-- it "run fact" $ do
it "run fact" $ do
result <- runFunc "fact" "fac-rec" [Value $ VI64 ()]
(succResult result) `shouldBe` [Value $ VI64 ()]
-- validMod <- readModule "test/samples/fact.wast"
-- Right (modInst, store) <- instantiate validMod
-- let (Success (_,(_,(Exc.Success (_,result))))) = term $ invokeExported store modInst (pack "fac-rec") [Value $ Lower $ VI64 ()]
......@@ -73,29 +86,25 @@ spec = do
---- putStrLn (show temp)
-- sound <- isSoundlyAbstracted validMod "fac-rec" args
-- sound `shouldBe` True
--
-- it "run test2" $ do
-- let path = "test/samples/simple.wast"
-- content <- LBS.readFile path
-- let Right m = parse content
-- let Right validMod = validate m
-- Right (modInst, store) <- instantiate validMod
-- let ((Success (_,(_,(Exc.Success (_,result)))))) = term $ invokeExported store modInst (pack "test2") []
-- result `shouldBe` [Value $ Lower $ VI32 ()]
--
--
-- it "run test-br3" $ do
-- let path = "test/samples/simple.wast"
-- content <- LBS.readFile path
-- let Right m = parse content
-- let Right validMod = validate m
-- Right (modInst, store) <- instantiate validMod
-- let ((Success (_,(_,(Exc.Success (_,result)))))) = term $ invokeExported store modInst (pack "test-br3") [Value $ Lower $ VI32 ()]
-- result `shouldBe` [Value $ Lower $ VI32 ()]
it "run test2" $ do
result <- runFunc "simple" "test2" []
(succResult result) `shouldBe` [Value $ VI32 ()]
it "run test-br3" $ do
result <- runFunc "simple" "test-br3" [Value $ VI32 ()]
(succResult result) `shouldBe` [Value $ VI32 ()]
-- let args = [[Concrete.Value $ Wasm.VI32 10]]
-- sound <- isSoundlyAbstracted validMod "test-br3" args
-- sound `shouldBe` True
--
it "run test-call-indirect" $ do
result <- runFunc "simple" "test-call-indirect" []
(excResult result) `shouldSatisfy` (\x -> case x of
(Exc.SuccessOrFail _ [Value (VI32 ())]) -> True
_ -> False)
-- it "run non-terminating" $ do
-- validMod <- readModule "test/samples/simple.wast"
-- Right (modInst, store) <- instantiate validMod
......
(module
(memory 1)
(table anyfunc
(elem
$noop
)
)
(type $out-i32 (func (result i32)))
;; Recursive factorial
(func (export "const") (param i32) (result i32)
(get_local 0)
......@@ -183,4 +192,8 @@
unreachable
)
)
(func (export "test-call-indirect") (result i32)
(call_indirect (type $out-i32) (i32.const 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