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

Added JoinVal constraint to IsVal

parent 70a921aa
Pipeline #108613 passed with stages
in 72 minutes and 59 seconds
......@@ -59,7 +59,7 @@ data GlobalState v = GlobalState {
funcInstances :: Vector FuncInst,
tableInstances :: Vector TableInst,
globalInstances:: Vector (FreeCompletion (GlobInst v))
}
} deriving (Show)
instance (PreOrd v) => PreOrd (GlobalState v) where
s1 s2 = let gs1 = globalInstances s1 in
......
......@@ -54,6 +54,8 @@ toVal64 :: Word64 -> Value
toVal64 = Value . Wasm.VI64
instance (ArrowChoice c) => IsVal Value (ValueT Value c) where
type JoinVal y (ValueT Value c) = ()
i32const = proc w32 -> returnA -< Value $ Wasm.VI32 w32
i64const = proc w64 -> returnA -< Value $ Wasm.VI64 w64
iBinOp = proc (bs,op,Value v1,Value v2) ->
......
......@@ -109,35 +109,37 @@ withMemoryInstance f = proc (i,x) -> do
class Show v => IsVal v c | c -> v where
i32const :: c Word32 v
i64const :: c Word64 v
f32const :: c Float v
f64const :: c Double v
iUnOp :: c (BitSize, IUnOp, v) v
iBinOp :: c (BitSize, IBinOp, v, v) (Maybe v)
i32eqz :: c v v
i64eqz :: c v v
iRelOp :: c (BitSize, IRelOp, v, v) v
fUnOp :: c (BitSize, FUnOp, v) v
fBinOp :: c (BitSize, FBinOp, v, v) v
fRelOp :: c (BitSize, FRelOp, v, v) v
i32WrapI64 :: c v v
iTruncFU :: c (BitSize, BitSize, v) (Maybe v)
iTruncFS :: c (BitSize, BitSize, v) (Maybe v)
i64ExtendSI32 :: c v v
i64ExtendUI32 :: c v v
fConvertIU :: c (BitSize, BitSize, v) v
fConvertIS :: c (BitSize, BitSize, v) v
f32DemoteF64 :: c v v
f64PromoteF32 :: c v v
iReinterpretF :: c (BitSize, v) v
fReinterpretI :: c (BitSize, v) v
i32ifNeqz :: 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 :: c x y -> c x y -> c (v, [x], x) y
ifHasType :: c x y -> c x y -> c (v, ValueType, x) y
type family JoinVal y (c :: * -> * -> *) :: Constraint
i32const :: c Word32 v
i64const :: c Word64 v
f32const :: c Float v
f64const :: c Double v
iUnOp :: c (BitSize, IUnOp, v) v
iBinOp :: c (BitSize, IBinOp, v, v) (Maybe v)
i32eqz :: c v v
i64eqz :: c v v
iRelOp :: c (BitSize, IRelOp, v, v) v
fUnOp :: c (BitSize, FUnOp, v) v
fBinOp :: c (BitSize, FBinOp, v, v) v
fRelOp :: c (BitSize, FRelOp, v, v) v
i32WrapI64 :: c v v
iTruncFU :: c (BitSize, BitSize, v) (Maybe v)
iTruncFS :: c (BitSize, BitSize, v) (Maybe v)
i64ExtendSI32 :: c v v
i64ExtendUI32 :: c v v
fConvertIU :: c (BitSize, BitSize, v) v
fConvertIS :: c (BitSize, BitSize, v) v
f32DemoteF64 :: c v v
f64PromoteF32 :: c v v
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 :: 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
......@@ -152,7 +154,7 @@ invokeExported ::
ArrowExcept exc c, IsException exc v c, JoinExc () c, ArrowReader LabelArities c,
ArrowWasmMemory m addr bytes v c, --HostFunctionSupport addr bytes v c,
Mem.Join () c,
IsVal v c, Show v,
IsVal v c, JoinVal () c, Show v,
Exc.Join () c,
Fail.Join [v] c,
Fail.Join () c,
......@@ -178,7 +180,7 @@ invokeExternal ::
ArrowExcept exc c, IsException exc v c, JoinExc () c, ArrowReader LabelArities c,
ArrowWasmMemory m addr bytes v c, --HostFunctionSupport addr bytes v c,
Mem.Join () c,
IsVal v c, Show v,
IsVal v c, JoinVal () c, Show v,
Exc.Join () c,
Fail.Join () c,
ArrowFail e c,
......@@ -230,7 +232,7 @@ eval ::
ArrowExcept exc c, IsException exc v c, JoinExc () c, ArrowReader LabelArities c,
ArrowWasmMemory m addr bytes v c, --HostFunctionSupport addr bytes v c,
Mem.Join () c,
IsVal v c, Show v,
IsVal v c, JoinVal () c, Show v,
Exc.Join () c,
ArrowFix (c [Instruction Natural] ()),
ArrowLogger String c,
......@@ -276,7 +278,7 @@ evalControlInst ::
( ArrowChoice c, Profunctor c,
ArrowStack v c, -- operand stack of computation
ArrowDebuggableStack v c,
IsVal v c, -- needs to support value operations
IsVal v c, JoinVal () c, -- needs to support value operations
ArrowExcept exc c, IsException exc v c, JoinExc () c,
ArrowReader LabelArities c, -- return arity of nested labels
ArrowFrame FrameData v c, -- frame data and local variables
......@@ -451,7 +453,7 @@ localNoLabels f = proc x -> do
--r <- ask -< ()
local f -< (LabelArities{labels=[]}, x)
evalParametricInst :: (ArrowChoice c, Profunctor c, ArrowStack v c, IsVal v c)
evalParametricInst :: (ArrowChoice c, Profunctor c, ArrowStack v c, IsVal v c, JoinVal () c)
=> c (Instruction Natural) ()
evalParametricInst = proc i -> case i of
Drop -> const () ^<< pop -< ()
......
......@@ -47,7 +47,7 @@ import Control.Arrow.Transformer.Reader
import Control.Arrow.Transformer.Value
import Control.Arrow.Transformer.Abstract.WasmFrame
import Control.Category
import Control.Category (Category)
import Data.Abstract.FreeCompletion as FC
import Data.Abstract.Sign
......@@ -116,6 +116,8 @@ tailA f = proc () -> do
(a:as) -> returnA -< as
instance (ArrowChoice c) => IsVal Value (ValueT Value c) where
type JoinVal y (ValueT Value c) = ArrowComplete y (ValueT Value c)
i32const = proc _ -> returnA -< valueI32
i64const = proc _ -> returnA -< valueI64
f32const = proc _ -> returnA -< valueF32
......@@ -147,6 +149,7 @@ deriving instance ArrowComplete () c => ArrowComplete () (ValueT v c)
instance (ArrowChoice c) => IsException (Exc Value) Value (ValueT Value c) where
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)
......
......@@ -12,6 +12,7 @@ import qualified Data.ByteString.Lazy as LBS
import Data.Abstract.Error
import qualified Data.Abstract.Except as Exc
import Data.Abstract.FreeCompletion
import qualified Data.HashSet as HashSet
import Data.List (isInfixOf)
import Data.List.Singleton (singleton)
import qualified Data.Abstract.Powerset as Pow
......@@ -54,6 +55,80 @@ spec = do
Right (modInst, store) <- instantiate validMod
let (_, (Success (_,(_,(Exc.Success (_,result)))))) = invokeExported store modInst (pack "test-br3") [Value $ Lower $ VI32 ()]
result `shouldBe` [Value $ Lower $ VI32 ()]
it "run test-br-and-return" $ 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)))))) = invokeExported store modInst (pack "test-br-and-return") [Value $ Lower $ VI32 ()]
result `shouldBe` [Value $ Lower $ VI32 ()]
it "run test-unreachable" $ 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 (_, res)))))) = invokeExported store modInst (pack "test-unreachable") []
res `shouldBe` [Value $ Lower $ VI32 ()]
it "run test-unreachable2" $ 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 (_, res)))))) = invokeExported store modInst (pack "test-unreachable2") []
res `shouldBe` [Value $ Lower $ VI32 ()]
it "run test-unreachable3" $ 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 (_, res)))))) = invokeExported store modInst (pack "test-unreachable3") []
res `shouldBe` [Value $ Lower $ VI32 ()]
it "run test-unreachable4" $ 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.Fail (Exc e)))))) = invokeExported store modInst (pack "test-unreachable4") []
(HashSet.toList e) `shouldBe` [Trap "Execution of unreachable instruction"]
it "run test-unreachable5" $ 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 (_, res)))))) = invokeExported store modInst (pack "test-unreachable5") [Value $ Lower $ VI32 ()]
res `shouldBe` [Value $ Lower $ VI32 ()]
--(HashSet.toList e) `shouldBe` [Trap "Execution of unreachable instruction"]
it "run test-br-and-return3" $ 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 (_, res)))))) = invokeExported store modInst (pack "test-br-and-return3") [Value $ Lower $ VI32 ()]
res `shouldBe` [Value $ Lower $ VI32 ()]
it "run test-br-and-return2" $ 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 (_, res))))))= invokeExported store modInst (pack "test-br-and-return2") [Value $ Lower $ VI32 ()]
res `shouldBe` [Value $ Lower $ VI32 ()]
--result `shouldBe` [Value $ Lower $ VI32 ()]
-- it "run const" $ do
-- let path = "test/samples/simple.wast"
-- content <- LBS.readFile path
......
......@@ -62,4 +62,98 @@
)
)
(func (export "test-br-and-return") (param i32) (result i32)
(block (result i32)
(block (result i32)
(if (result i32) (i32.eq (get_local 0) (i32.const 0))
(then
i32.const 42
return
)
(else
i32.const 43
br 1
)
)
)
)
)
(func (export "test-unreachable") (result i32)
i32.const 42
return
unreachable
)
(func (export "test-unreachable2") (result i32)
(block (result i32)
i32.const 42
return
)
unreachable
)
(func (export "test-unreachable3") (result i32)
(block (result i32)
i32.const 42
br 1
)
unreachable
)
(func (export "test-unreachable4") (result i32)
(block (result i32)
i32.const 42
br 0
)
unreachable
)
(func (export "test-unreachable5") (param i32) (result i32)
(if (result i32) (i32.eq (get_local 0) (i32.const 0))
(then
i32.const 42
br 1
)
(else
i32.const 43
br 1
)
)
unreachable
)
(func (export "test-br-and-return3") (param i32) (result i32)
(block (result i32)
(if (result i32) (i32.eq (get_local 0) (i32.const 0))
(then
i32.const 42
br 1
)
(else
i32.const 43
br 1
)
)
unreachable
)
)
(func (export "test-br-and-return2") (param i32) (result i32)
(block (result i32)
(block (result i32)
(if (result i32) (i32.eq (get_local 0) (i32.const 0))
(then
i32.const 42
return
)
(else
i32.const 43
br 2
)
)
)
unreachable
)
)
)
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