Commit 6d84c6d2 authored by Katharina Brandl's avatar Katharina Brandl
Browse files

tests for taint analysis and different error transformer

parent d94988b3
Pipeline #130695 passed with stages
in 75 minutes and 53 seconds
......@@ -22,7 +22,7 @@ import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Reader
import Control.Arrow.Order (ArrowComplete(..))
import Control.Arrow.Order (ArrowComplete(..),ArrowJoin(..))
import Control.Arrow.Store as Store
import Control.Arrow.Except as Exc
import Control.Arrow.Transformer.State
......@@ -39,7 +39,7 @@ newtype LogErrorT e c x y = LogErrorT (StateT (Errors e) c x y)
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowLift, ArrowTrans,
ArrowConst r, ArrowReader r,
ArrowEnv var val, ArrowClosure expr cls, ArrowStore a b, ArrowLetRec var val,
ArrowExcept e', ArrowCallSite ctx)
ArrowExcept e', ArrowCallSite ctx, ArrowJoin)
runLogErrorT :: (Identifiable e, Profunctor c) => LogErrorT e c x y -> c x (Errors e, y)
runLogErrorT f = lmap (empty,) (unlift f)
......
......@@ -13,13 +13,14 @@ module TaintAnalysis where
import Prelude as P
import Abstract
import Data
import GenericInterpreter hiding (Exc,Err)
import qualified GenericInterpreter as Generic
import TaintAnalysisValue hiding (Value)
import qualified TaintAnalysisValue as Taint
import qualified UnitAnalysis as Abs
import UnitAnalysisValue(Exc(..),Err)
import Abstract
import Data
import TaintAnalysisValue
import qualified UnitAnalysisValue as Abs
import Control.Arrow.Fix as Fix
......@@ -56,31 +57,35 @@ import Data.Text.Lazy (Text)
import qualified Data.Vector as Vec
import Language.Wasm.Interpreter (ModuleInstance)
import qualified Language.Wasm.Interpreter as Wasm
import Language.Wasm.Validate (ValidModule)
import Numeric.Natural (Natural)
type In = (JoinVector (Value Abs.Value),
type Value = Taint.Value Abs.Value
type In = (JoinVector Value,
((Natural, ModuleInstance),
(Tables,
(StaticGlobalState (Value Abs.Value),
(JoinList (Value Abs.Value), (JumpTypes, [Instruction Natural]))))))
(StaticGlobalState Value,
(JoinList Value, (JumpTypes, [Instruction Natural]))))))
type Out = Terminating
(Error
Err
(JoinVector (Value Abs.Value),
(StaticGlobalState (Value Abs.Value),
Except (Exc (Value Abs.Value)) (JoinList (Value Abs.Value), ()))))
(JoinVector Value,
(StaticGlobalState Value,
Except (Exc Value) (JoinList Value, ()))))
type Result = (CFG (Instruction Natural), Terminating
(Error
Err
(JoinVector (Value Abs.Value),
(StaticGlobalState (Value Abs.Value),
Except (Exc (Value Abs.Value)) (JoinList (Value Abs.Value), [Value Abs.Value])))))
(JoinVector Value,
(StaticGlobalState Value,
Except (Exc Value) (JoinList Value, [Value])))))
invokeExported :: StaticGlobalState (Value Abs.Value)
invokeExported :: StaticGlobalState Value
-> Tables
-> ModuleInstance
-> Text
......@@ -94,17 +99,17 @@ invokeExported initialStore tab modInst funcName args =
let ?fixpointAlgorithm = fixpointAlgorithm algo in
(\(cfg,(_,res)) -> (cfg,res)) $ Trans.run
(Generic.invokeExported ::
ValueT (Value Abs.Value)
ValueT Value
(ReaderT Generic.JumpTypes
(StackT (Value Abs.Value)
(ExceptT (Exc (Value Abs.Value))
(StaticGlobalStateT (Value Abs.Value)
(StackT Value
(ExceptT (Exc Value)
(StaticGlobalStateT Value
(MemoryT
(MemAddressT
(SizeT (Value Abs.Value)
(SerializeT (Value Abs.Value)
(TableT (Value Abs.Value)
(FrameT FrameData (Value Abs.Value)
(SizeT Value
(SerializeT Value
(TableT Value
(FrameT FrameData Value
(ErrorT Err
(TerminatingT
(FixT
......@@ -112,9 +117,9 @@ invokeExported initialStore tab modInst funcName args =
(Fix.StackT Fix.Stack In
(CacheT Cache In Out
(ControlFlowT (Instruction Natural)
(->)))))))))))))))))) (Text, [Value Abs.Value]) [Value Abs.Value]) (JoinVector $ Vec.empty,((0,modInst),(tab,(initialStore,([],(Generic.JumpTypes [],(funcName, P.map taint args)))))))
(->)))))))))))))))))) (Text, [Value]) [Value]) (JoinVector $ Vec.empty,((0,modInst),(tab,(initialStore,([],(Generic.JumpTypes [],(funcName, P.map taint args)))))))
where
taint v = Value Tainted v
taint v = Taint.Value Tainted v
isRecursive (_,(_,(_,(_,(_,(_,inst)))))) = case inst of
Loop {} : _ -> True
Call _ _ : _ -> True
......@@ -128,4 +133,11 @@ invokeExported initialStore tab modInst funcName args =
getExpression (_,(_,(_,(_,(_,(_,exprs)))))) = case exprs of e:_ -> Just e; _ -> Nothing
deriving instance ArrowComplete (Value Abs.Value) c => ArrowComplete (Value Abs.Value) (ValueT Abs.Value c)
instantiateTaint :: ValidModule -> IO (Either String (ModuleInstance, StaticGlobalState Value, Tables))
instantiateTaint valMod = do res <- instantiate valMod (alpha Untainted) (\_ _ -> ()) TableInst
return $ fmap (\(m,s,_,tab) -> (m,s,JoinVector tab)) res
alpha :: Taint -> Wasm.Value -> Value
alpha t v = Taint.Value t (Abs.alpha v)
deriving instance ArrowComplete Value c => ArrowComplete Value (ValueT Abs.Value c)
......@@ -27,12 +27,19 @@ import qualified Data.Abstract.DiscretePowerset as Pow
import Data.Hashable
import Data.HashSet as HashSet
import Data.Order
import Data.Text.Prettyprint.Doc as Pretty
import GHC.Generics
import Data.Coerce (coerce)
data Taint = Tainted | Untainted | Top deriving (Eq, Show, Generic, Hashable)
data Value v = Value Taint v deriving (Eq, Show, Generic, Hashable)
instance Pretty Taint where
pretty = viaShow
instance (Show v) => Pretty (Value v) where
pretty = viaShow
instance PreOrd Taint where
_ Top = True
Tainted Tainted = True
......
......@@ -27,7 +27,8 @@ import Control.Arrow.Fix.ControlFlow
import Control.Arrow.Trans as Trans
import Control.Arrow.Transformer.Abstract.Except
import Control.Arrow.Transformer.Abstract.Error
--import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.LogError
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable
import Control.Arrow.Transformer.Abstract.Fix.Component
......@@ -48,8 +49,8 @@ import Control.Arrow.Transformer.WasmFrame
import Data.Abstract.Terminating
import Data.Abstract.Error as Error
import Data.Abstract.Except
import Data.Abstract.MonotoneErrors (Errors)
import qualified Data.Abstract.Widening as W
import Data.Text.Lazy (Text)
import qualified Data.Vector as Vec
......@@ -84,24 +85,22 @@ tailA f = proc () -> do
[] -> returnA -< error "tailA: cannot return the tail of an empty list"
type In = (JoinVector Value,
type In = (Errors Err,
(JoinVector Value,
((Natural, ModuleInstance),
(Tables,
(StaticGlobalState Value,
(JoinList Value, (JumpTypes, [Instruction Natural]))))))
(JoinList Value, (JumpTypes, [Instruction Natural])))))))
type Out = Terminating
(Error
Err
type Out = (Errors Err, (Terminating
(JoinVector Value,
--(Tables,
(StaticGlobalState Value,
Except (Exc Value) (JoinList Value, ()))))
Except (Exc Value) (JoinList Value, ())))))
type Result = (CFG (Instruction Natural), Terminating
(Error
Err
type Result = (CFG (Instruction Natural), (Errors Err,
Terminating
(JoinVector Value,
--(Tables,
(StaticGlobalState Value,
......@@ -114,7 +113,7 @@ invokeExported :: StaticGlobalState Value
-> [Value]
-> Result
invokeExported initialStore tab modInst funcName args =
let ?cacheWidening = W.finite in
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
......@@ -132,16 +131,16 @@ invokeExported initialStore tab modInst funcName args =
(SerializeT Value
(TableT Value
(FrameT FrameData Value
(ErrorT Err
(TerminatingT
(TerminatingT
(LogErrorT Err
(FixT
(ComponentT Component In
(Fix.StackT Fix.Stack In
(CacheT Cache In Out
(Fix.StackT Fix.Stack In
(CacheT Monotone In Out
(ControlFlowT (Instruction Natural)
(->)))))))))))))))))) (Text, [Value]) [Value]) (JoinVector $ Vec.empty,((0,modInst),(tab,(initialStore,([],(Generic.JumpTypes [],(funcName, args)))))))
where
isRecursive (_,(_,(_,(_,(_,(_,inst)))))) = case inst of
isRecursive (_,(_,(_,(_,(_,(_,(_,inst))))))) = case inst of
Loop {} : _ -> True
Call _ _ : _ -> True
CallIndirect _ _ : _ -> True --error "todo"
......@@ -151,7 +150,7 @@ invokeExported initialStore tab modInst funcName args =
-- p2 (Terminating (Error.Success (stack, (_,rest)))) = pretty rest
-- p2 x = pretty x
getExpression (_,(_,(_,(_,(_,(_,exprs)))))) = case exprs of e:_ -> Just e; _ -> Nothing
getExpression (_,(_,(_,(_,(_,(_,(_,exprs))))))) = case exprs of e:_ -> Just e; _ -> Nothing
instantiateAbstract :: ValidModule -> IO (Either String (ModuleInstance, StaticGlobalState Value, Tables))
instantiateAbstract valMod = do res <- instantiate valMod alpha (\_ _ -> ()) TableInst
......
{-# LANGUAGE OverloadedLists #-}
module TaintSpec where
import Abstract
import qualified Data as D
import Soundness
import TaintAnalysis
import TaintAnalysisValue (Taint(..))
import qualified TaintAnalysisValue as Taint
import UnitAnalysisValue (Exc,Err)
import qualified UnitAnalysisValue as U
--import GenericInterpreter(Exc(..),Err(..))
import GraphToDot
--import Control.Arrow.Transformer.Abstract.WasmFrame (Vector(..))
--import Control.Arrow.Transformer.Abstract.Stack (AbsList(..))
import qualified Data.ByteString.Lazy as LBS
import Data.Abstract.Error
import qualified Data.Abstract.Except as Exc
import Data.Abstract.FreeCompletion
import Data.Abstract.Terminating
import qualified Data.HashSet as HashSet
import Data.List (isInfixOf)
import Data.List.Singleton (singleton)
import qualified Data.Abstract.Powerset as Pow
import Data.Order
import Data.Text.Lazy (pack)
import Data.Text.Prettyprint.Doc
import Data.Vector(fromList,empty)
import qualified Data.Vector as Vec
import Language.Wasm
import Language.Wasm.Interpreter (ModuleInstance(..))
import qualified Language.Wasm.Interpreter as Wasm
import Language.Wasm.Structure
import Language.Wasm.Validate
import Numeric.Natural
import Test.Hspec
main :: IO ()
main = hspec spec
term :: Terminating a -> a
term (Terminating a) = a
getFunctionBody (Function _ _ b) = b
readModule :: String -> IO ValidModule
readModule path = do
content <- LBS.readFile path
let Right m = parse content
let Right validMod = validate m
return validMod
runFunc :: String -> String -> [U.Value] -> IO Result
runFunc modName funcName args = do
mod <- readModule ("test/samples/" ++ modName ++ ".wast")
Right (modInst, staticS, tabs) <- instantiateTaint mod
return $ invokeExported staticS tabs modInst (pack funcName) args
succResult :: Result -> [Value]
succResult (_,(Terminating (Success (_,(_,(Exc.Success (_,result))))))) = result
excResult :: Result -> Exc.Except (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
errResult :: Result -> Err
errResult (_,(Terminating (Fail x))) = x
taintValue :: Taint -> BaseValue () () () () -> Value
taintValue t bv = Taint.Value t $ U.Value bv
--fromTrap :: Err -> String
--fromTrap (Trap s) = s
spec :: Spec
spec = do
it "run const" $ do
result <- runFunc "simple" "const" [U.Value $ VI32 ()]
(succResult result) `shouldBe` [taintValue Tainted (VI32 ())]
it "run noop" $ do
result <- runFunc "simple" "noop" []
(succResult result) `shouldBe` [taintValue Untainted (VI32 ())]
it "run test2" $ do
result <- runFunc "simple" "test2" []
(succResult result) `shouldBe` [taintValue Untainted (VI32 ())]
it "test-mem" $ do
result <- runFunc "simple" "test-mem" [U.Value $ VI32 ()]
pending
--result `shouldSatisfy` (const False)
--(succResult result) `shouldBe` [taintValue Taint.Top (VI32 ())]
it "run fact" $ do
result <- runFunc "fact" "fac-rec" [U.Value $ VI64 ()]
let cfg = fst result
--putStrLn $ show cfg
(succResult result) `shouldBe` [taintValue Taint.Top (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 ()]
-- result `shouldBe` [Value $ Lower $ VI64 ()]
-- let args = [[Concrete.Value $ Wasm.VI64 1],[Concrete.Value $ Wasm.VI64 10]]
---- Right (concModInst, concStore) <- Concrete.instantiate validMod
---- Right (absModInst, absStore) <- instantiate validMod
---- let (AbsList absArgs) = foldr1 (⊔) $ (map (AbsList . map alphaVal1)) $ args
---- let concResults = map (snd . Concrete.invokeExported concStore concModInst (pack "fac-rec")) args
---- let (Terminating temp) = invokeExported absStore absModInst (pack "fac-rec") absArgs
---- --let absResult = resultToAbsList $ temp
---- putStrLn (show concResults)
---- putStrLn (show temp)
-- sound <- isSoundlyAbstracted validMod "fac-rec" args
-- sound `shouldBe` True
-- 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" []
-- pending
-- --errResult result `shouldSatisfy` const False
-- --(excResult result) `shouldSatisfy` (\x -> case x of
-- -- (Exc.SuccessOrFail _ [Value (VI32 ())]) -> True
-- -- _ -> False)
--
-- it "run test-unreachable" $ do
-- result <- runFunc "simple" "test-unreachable" []
-- let cfg = fst result
-- --putStrLn $ show cfg
-- (succResult result) `shouldBe` [Value $ VI32 ()]
--
-- it "print cfg" $ do
-- result <- runFunc "fact" "fac-rec" [Value $ VI64 ()]
-- let cfg = fst result
-- putStrLn (show cfg)
-- putStrLn $ graphToDot showForGraph cfg
-- pending
showForGraph :: D.Instruction Natural -> String
showForGraph (D.I32Const i _) = "I32Const " ++ (show i)
showForGraph (D.I64Const i _) = "I64Const " ++ (show i)
showForGraph (D.GetLocal n _) = "GetLocal " ++ (show n)
showForGraph (D.IRelOp bs op _) = "IRelOp " ++ (show bs) ++ " " ++ (show op)
showForGraph (D.IBinOp bs op _) = "IBinOp " ++ (show bs) ++ " " ++ (show op)
showForGraph (D.Call i _) = "Call " ++ (show i)
showForGraph (D.If t _ _ _) = "If " ++ (show t)
-- it "run non-terminating" $ do
-- validMod <- readModule "test/samples/simple.wast"
-- Right (modInst, store) <- instantiate validMod
-- let result = invokeExported store modInst (pack "non-terminating") []
-- result `shouldBe` NonTerminating
--
-- it "run maybe-non-terminating" $ do
-- validMod <- readModule "test/samples/simple.wast"
---- Right (modInst, store) <- instantiate validMod
---- let result = term $ invokeExported store modInst (pack "maybe-non-terminating") [Value $ Lower $ VI32 ()]
---- --result `shouldBe` [Value $ Lower $ VI32 ()]
---- result `shouldSatisfy` (const False)
-- let args = [[Concrete.Value $ Wasm.VI32 42]]
-- sound <- isSoundlyAbstracted validMod "maybe-non-terminating" args
-- sound `shouldBe` True
--
-- it "run noop" $ do
-- validMod <- readModule "test/samples/simple.wast"
-- Right (modInst, store) <- instantiate validMod
-- let (Success (locals,(Lower state,(Exc.Success (stack,result))))) = term $ invokeExported store modInst (pack "noop") []
-- locals `shouldBe` (Vector $ Vec.empty)
-- stack `shouldBe` []
-- result `shouldBe` [Value $ Lower $ VI32 ()]
--
-- let args = [[]]
-- sound <- isSoundlyAbstracted validMod "noop" args
-- sound `shouldBe` True
--
-- 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)))))) = term $ invokeExported store modInst (pack "test-br-and-return") [Value $ Lower $ VI32 ()]
-- result `shouldBe` [Value $ Lower $ VI32 ()]
-- let args = [[Concrete.Value $ Wasm.VI32 10]]
-- sound <- isSoundlyAbstracted validMod "test-br-and-return" args
-- sound `shouldBe` True
--
-- 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)))))) = term $ invokeExported store modInst (pack "test-unreachable") []
-- res `shouldBe` [Value $ Lower $ VI32 ()]
-- let args = [[]]
-- sound <- isSoundlyAbstracted validMod "test-unreachable" args
-- sound `shouldBe` True
--
-- 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)))))) = term $ invokeExported store modInst (pack "test-unreachable2") []
-- res `shouldBe` [Value $ Lower $ VI32 ()]
-- let args = [[]]
-- sound <- isSoundlyAbstracted validMod "test-unreachable2" args
-- sound `shouldBe` True
--
-- 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)))))) = term $ invokeExported store modInst (pack "test-unreachable3") []
-- res `shouldBe` [Value $ Lower $ VI32 ()]
-- let args = [[]]
-- sound <- isSoundlyAbstracted validMod "test-unreachable3" args
-- sound `shouldBe` True
--
-- 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)))))) = term $ invokeExported store modInst (pack "test-unreachable4") []
-- (HashSet.toList e) `shouldBe` [Trap "Execution of unreachable instruction"]
-- let args = [[]]
-- sound <- isSoundlyAbstracted validMod "test-unreachable4" args
-- sound `shouldBe` True
--
-- 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)))))) = term $ invokeExported store modInst (pack "test-unreachable5") [Value $ Lower $ VI32 ()]
-- res `shouldBe` [Value $ Lower $ VI32 ()]
-- let args = [[Concrete.Value $ Wasm.VI32 10]]
-- sound <- isSoundlyAbstracted validMod "test-unreachable5" args
-- sound `shouldBe` True
-- --(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)))))) = term $ invokeExported store modInst (pack "test-br-and-return3") [Value $ Lower $ VI32 ()]
-- res `shouldBe` [Value $ Lower $ VI32 ()]
-- let args = [[Concrete.Value $ Wasm.VI32 10]]
-- sound <- isSoundlyAbstracted validMod "test-br-and-return3" args
-- sound `shouldBe` True
--
-- 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))))))= term $ invokeExported store modInst (pack "test-br-and-return2") [Value $ Lower $ VI32 ()]
-- res `shouldBe` [Value $ Lower $ VI32 ()]
-- let args = [[Concrete.Value $ Wasm.VI32 10]]
-- sound <- isSoundlyAbstracted validMod "test-br-and-return2" args
-- sound `shouldBe` True
-- --result `shouldBe` [Value $ Lower $ VI32 ()]
---- it "run const" $ 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 (_,(_,(Success (_,result)))))) = term $ invokeExported store modInst (pack "const") [Value $ Wasm.VI32 5]
---- result `shouldBe` [Value $ Wasm.VI32 5]
----
---- it "run half-fact" $ 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 (_,(_,(Success (_,result1)))))) = term $ invokeExported store modInst (pack "half-fac") [Value $ Wasm.VI32 0]
---- result1 `shouldBe` [Value $ Wasm.VI32 1]
----
---- it "run half-fact-64" $ do
---- let path = "test/samples/simple.wast"
---- content <- LBS.readFile path
---- let Right m = parse content
---- let Right validMod = validate m
---- --let halfFac64Code = (getFunctionBody . (!! 3) . functions . getModule) validMod
---- --putStrLn $ show validMod
---- Right (modInst, store) <- instantiate validMod
---- let (_, (Success (_,(_,(Success (_,result1)))))) = term $ invokeExported store modInst (pack "half-fac-64") [Value $ Wasm.VI64 0]
---- result1 `shouldBe` [Value $ Wasm.VI64 1]
---- --mapM_ (putStrLn . show) halfFac64Code
---- --putStrLn ""
---- --mapM_ putStrLn (reverse logs)
----
---- it "run fac-rec" $ do
---- let path = "test/samples/fact.wast"
---- content <- LBS.readFile path
---- let Right m = parse content
---- let Right validMod = validate m
---- --let facCode = (getFunctionBody . (!! 0) . functions . getModule) validMod
---- --mapM_ (putStrLn . show) facCode
---- --putStrLn ""
---- Right (modInst, store) <- instantiate validMod
---- let params = map (singleton . Value . Wasm.VI64) [0 .. 8]
---- let results = map (term $ invokeExported store modInst (pack "fac-rec")) params
---- let rs = map (\(_,Success (_,(_,(Success (_,r))))) -> r) results
---- --let logs = zip [0 ..] ls
---- --mapM_ printLogs logs
---- rs `shouldBe` (map (singleton . Value . Wasm.VI64) [1,1,2,6,24,120,720,5040,40320])
----
---- --where
---- -- printLogs (n,ls) = do
---- -- putStrLn $ show n
---- -- mapM_ putStrLn ((reverse . filter (\x -> isInfixOf "before returning" x ||
---- -- isInfixOf "readFunction" x ||
---- -- isInfixOf "invoke" x)) ls)
---- -- putStrLn ""
----
---- it "run test-mem" $ 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 (_,(_,(Success (_,result)))))) = term $ invokeExported store modInst (pack "test-mem") [Value $ Wasm.VI32 42]
---- result `shouldBe` [Value $ Wasm.VI32 43]
......@@ -19,6 +19,7 @@ import qualified Data.ByteString.Lazy as LBS
import Data.Abstract.Error
import qualified Data.Abstract.Except as Exc
import Data.Abstract.FreeCompletion
import Data.Abstract.MonotoneErrors(toSet)
import Data.Abstract.Terminating
import qualified Data.HashSet as HashSet
import Data.List (isInfixOf)
......@@ -62,15 +63,27 @@ runFunc modName funcName args = do