Commit 0a3dd5b6 authored by Katharina Brandl's avatar Katharina Brandl
Browse files

fixed soundess module

parent 6d84c6d2
Pipeline #130817 passed with stages
in 74 minutes and 48 seconds
......@@ -29,8 +29,8 @@ import Control.Arrow.Fix.ControlFlow
import Control.Arrow.Order
import Control.Arrow.Trans as Trans
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Except
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
......@@ -49,8 +49,8 @@ import Control.Arrow.Transformer.StaticGlobalState
import Control.Arrow.Transformer.Value
import Control.Arrow.Transformer.WasmFrame
import Data.Abstract.Error as Error
import Data.Abstract.Except
import Data.Abstract.MonotoneErrors (Errors)
import Data.Abstract.Terminating
import qualified Data.Abstract.Widening as W
import Data.Text.Lazy (Text)
......@@ -64,23 +64,21 @@ import Numeric.Natural (Natural)
type Value = Taint.Value Abs.Value
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,
(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,
(StaticGlobalState Value,
Except (Exc Value) (JoinList Value, [Value])))))
......@@ -92,7 +90,7 @@ invokeExported :: StaticGlobalState Value
-> [Abs.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
......@@ -110,17 +108,17 @@ 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
(CacheT Monotone In Out
(ControlFlowT (Instruction Natural)
(->)))))))))))))))))) (Text, [Value]) [Value]) (JoinVector $ Vec.empty,((0,modInst),(tab,(initialStore,([],(Generic.JumpTypes [],(funcName, P.map taint args)))))))
where
taint v = Taint.Value Tainted v
isRecursive (_,(_,(_,(_,(_,(_,inst)))))) = case inst of
isRecursive (_,(_,(_,(_,(_,(_,(_,inst))))))) = case inst of
Loop {} : _ -> True
Call _ _ : _ -> True
CallIndirect _ _ : _ -> True
......@@ -130,7 +128,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
instantiateTaint :: ValidModule -> IO (Either String (ModuleInstance, StaticGlobalState Value, Tables))
......
......@@ -91,7 +91,8 @@ instance (Hashable v, ArrowExcept (Abs.Exc (Value v)) c, ArrowChoice c) => IsExc
-- handleException = id
instance Arrow c => IsErr Abs.Err (ValueT (Value v) c) where
err = arr $ Abs.Err . Pow.singleton
--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)
......
......@@ -27,7 +27,6 @@ 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.LogError
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable
......
......@@ -34,7 +34,8 @@ 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)
--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
......@@ -49,7 +50,8 @@ instance (ArrowExcept (Exc Value) c, ArrowChoice c) => IsException (Exc Value) V
joinList1'' f -< (HashSet.toList excs,x)
instance Arrow c => IsErr Err (ValueT Value c) where
err = arr $ Err . Pow.singleton
--err = arr $ Err . Pow.singleton
err = arr id
newtype Value = Value (BaseValue () () () ()) deriving (Eq, Show, Hashable, PreOrd, Complete, Pretty)
......
......@@ -3,120 +3,127 @@
module Soundness where
import Abstract (BaseValue(..))
import qualified Abstract as Abstract
import qualified Concrete as Concrete
import qualified ConcreteInterpreter as Concrete
import Abstract as Abstract
import Concrete as Concrete
import ConcreteInterpreter as Concrete
import Data
import qualified GenericInterpreter as Generic
import qualified UnitAnalysis as UnitA
import UnitAnalysis as Abstract
import UnitAnalysisValue as Abstract
--import Control.Arrow.Transformer.Abstract.Stack (AbsList(..))
--import qualified Control.Arrow.Transformer.Abstract.WasmFrame as Frame
import qualified Data.Abstract.Error as AE
import Data.Abstract.Except (Except)
import qualified Data.Abstract.Except as Except
import Data.Abstract.FreeCompletion
import Data.Abstract.DiscretePowerset (Pow(..))
import Data.Abstract.MonotoneErrors (toSet)
import Data.Abstract.Terminating
import qualified Data.Concrete.Error as CE
import qualified Data.Concrete.Error as Concrete
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import Data.Order
import Data.Text.Lazy (pack)
import Data.Vector (Vector)
import qualified Data.Vector as Vec
import qualified Language.Wasm.Interpreter as Wasm
import Language.Wasm.Validate (ValidModule)
--type ConcResult = CE.Error
-- String
-- (Vector Concrete.Value,
-- (Concrete.GlobalState Concrete.Value,
-- CE.Error
-- (Generic.Exc Concrete.Value)
-- ([Concrete.Value], [Concrete.Value])))
--type AbsResult = (AE.Error
-- (Pow String)
-- (Frame.Vector UnitA.Value,
-- (FreeCompletion (Abstract.GlobalState UnitA.Value),
-- Except
-- (UnitA.Exc UnitA.Value)
-- (AbsList UnitA.Value, AbsList UnitA.Value))))
--
--alphaResult :: [ConcResult] -> AbsResult
--alphaResult = alphaError alphaString1
-- (alphaTuple alphaLocals1
-- (alphaTuple alphaGlobalState1
-- (alphaExcept1 alphaExc1
-- (alphaTuple alphaStack1 (AbsList . map alphaVal1)))))
--
--alphaValue :: [Concrete.Value] -> UnitA.Value
--alphaValue = foldr1 (⊔) . map alphaVal1 -- . HashSet.toList
--
--alphaVal1 :: Concrete.Value -> UnitA.Value
--alphaVal1 (Concrete.Value v) = UnitA.Value $ Lower $ case v of
-- Wasm.VI32 _ -> VI32 ()
-- Wasm.VI64 _ -> VI64 ()
-- Wasm.VF32 _ -> VF32 ()
-- Wasm.VF64 _ -> VF64 ()
--
--alphaTuple :: (concA -> absA) -> (concB -> absB) -> (concA,concB) -> (absA,absB)
--alphaTuple alphaA alphaB (a,b) = (alphaA a, alphaB b)
--
--alphaError :: (Complete absE, Complete absA) =>
-- (concE -> absE) -> (concA -> absA) -> [CE.Error concE concA] -> AE.Error absE absA
--alphaError alphaE alphaA = foldr1 (⊔) . map alphaError1 -- . HashSet.toList
-- where alphaError1 = either (AE.Fail . alphaE) (AE.Success . alphaA) . CE.toEither
--
--alphaString1 :: String -> Pow String
--alphaString1 = Pow . HashSet.singleton
--
--alphaLocals :: [Vector Concrete.Value] -> Frame.Vector UnitA.Value
--alphaLocals = foldr1 (⊔) . map alphaLocals1 -- . HashSet.toList
--alphaLocals1 :: Vector Concrete.Value -> Frame.Vector UnitA.Value
--alphaLocals1 = Frame.Vector . Vec.map alphaVal1
--
--alphaStack :: [[Concrete.Value]] -> AbsList UnitA.Value
--alphaStack = foldr1 (⊔) . map alphaStack1 -- . HashSet.toList
--alphaStack1 :: [Concrete.Value] -> AbsList UnitA.Value
--alphaStack1 = AbsList . map alphaVal1
--
--alphaGlobalState :: [Concrete.GlobalState Concrete.Value] -> FreeCompletion (Abstract.GlobalState UnitA.Value)
--alphaGlobalState = foldr1 (⊔) . map alphaGlobalState1 -- . HashSet.toList
--alphaGlobalState1 :: Concrete.GlobalState Concrete.Value
-- -> FreeCompletion (Abstract.GlobalState UnitA.Value)
--alphaGlobalState1 (Concrete.GlobalState f t _ g) = Lower $ Abstract.GlobalState f t (Vec.map alphaGlob g)
-- where alphaGlob (Concrete.GlobInst m v) = Lower $ Concrete.GlobInst m (alphaVal1 v)
--
--alphaExcept :: (Complete absE, Complete absA) =>
-- (concE -> absE) -> (concA -> absA) -> [CE.Error concE concA] -> Except absE absA
--alphaExcept alphaE alphaA = foldr1 (⊔) . map (alphaExcept1 alphaE alphaA) -- . HashSet.toList
--alphaExcept1 :: (concE -> absE) -> (concA -> absA) -> CE.Error concE concA -> Except absE absA
--alphaExcept1 alphaE alphaA = either (Except.Fail . alphaE) (Except.Success . alphaA) . CE.toEither
--
--alphaExc1 :: (Generic.Exc Concrete.Value) -> (UnitA.Exc UnitA.Value)
--alphaExc1 exc = UnitA.Exc $ HashSet.singleton $ convert exc
-- where convert (Generic.Jump i vs) = Generic.Jump i $ map alphaVal1 vs
-- convert (Generic.CallReturn vs) = Generic.CallReturn $ map alphaVal1 vs
-- convert (Generic.Trap s) = Generic.Trap s
--
--
--isSoundlyAbstracted :: ValidModule -> String -> [[Concrete.Value]] -> IO Bool
--isSoundlyAbstracted mod func argsList = do
-- Right (concModInst, concStore) <- Concrete.instantiate mod
-- Right (absModInst, absStore) <- UnitA.instantiate mod
-- let (AbsList absArgs) = foldr1 (⊔) $ (map (AbsList . map alphaVal1)) $ argsList
-- let concResults = map (snd . Concrete.invokeExported concStore concModInst (pack func)) argsList
-- let (Terminating temp) = UnitA.invokeExported absStore absModInst (pack func) absArgs
-- let absResult = resultToAbsList $ temp
-- return $ alphaResult concResults ⊑ absResult
--
-- where
-- resultToAbsList (AE.Success (locals, (state, (Except.Success (stack, vs))))) =
-- (AE.Success (locals, (state, (Except.Success (stack, (AbsList vs))))))
-- resultToAbsList (AE.Success (locals, (state, (Except.SuccessOrFail e (stack, vs))))) =
-- (AE.Success (locals, (state, (Except.SuccessOrFail e (stack, (AbsList vs))))))
-- resultToAbsList (AE.Success (locals, (state, (Except.Fail e)))) =
-- (AE.Success (locals, (state, (Except.Fail e))))
-- resultToAbsList (AE.Fail e) = AE.Fail e
type AbsResult = (Except (HashSet Err)
(Terminating
(JoinVector Abstract.Value,
(StaticGlobalState Abstract.Value,
Except (Exc Abstract.Value) (JoinList Abstract.Value, JoinList Abstract.Value)))))
convertAbsResult :: Abstract.Result -> AbsResult
convertAbsResult (_,(errs,Terminating (a, (gs, (Except.Success (stack,vals)))))) =
let errsSet = toSet errs in
if HashSet.null errsSet
then Except.Success (Terminating (a, (gs, (Except.Success (stack, JoinList vals)))))
else Except.SuccessOrFail errsSet (Terminating (a, (gs, (Except.Success (stack, JoinList vals)))))
convertAbsResult (_,(errs,Terminating (a, (gs, (Except.SuccessOrFail e (stack,vals)))))) =
let errsSet = toSet errs in
if HashSet.null errsSet
then Except.Success (Terminating (a, (gs, (Except.SuccessOrFail e (stack, JoinList vals)))))
else Except.SuccessOrFail errsSet (Terminating (a, (gs, (Except.SuccessOrFail e (stack, JoinList vals)))))
convertAbsResult (_,(errs,Terminating (a, (gs, Except.Fail e)))) =
let errsSet = toSet errs in
if HashSet.null errsSet
then Except.Success (Terminating (a, (gs, Except.Fail e)))
else Except.SuccessOrFail errsSet (Terminating (a, (gs, Except.Fail e)))
convertAbsResult (_,(errs,NonTerminating)) =
let errsSet = toSet errs in
if HashSet.null errsSet
then Except.Success NonTerminating
else Except.Fail errsSet
alphaResults :: [Concrete.Result] -> AbsResult
alphaResults = foldr1 () . map alphaResult
alphaResult :: Concrete.Result -> AbsResult
alphaResult = alphaError (alphaTerminating (alphaTuple
alphaVector
(alphaIgnoreFst (alphaIgnoreFst (alphaTuple
alphaGlobals
(alphaExcept (alphaTuple alphaJoinList alphaList)))))))
alphaTerminating :: (concA -> absA) -> concA -> Terminating absA
alphaTerminating alphaA = Terminating . alphaA
alphaVector :: JoinVector Concrete.Value -> JoinVector Abstract.Value
alphaVector (JoinVector v) = JoinVector $ Vec.map alphaVal v
alphaError :: (concA -> absA) -> Concrete.Error Generic.Err concA -> (Except (HashSet Generic.Err) absA)
alphaError alphaA = either
(\err -> Except.Fail $ HashSet.singleton err)
(\res -> Except.Success $ alphaA res)
. Concrete.toEither
alphaGlobals :: StaticGlobalState Concrete.Value -> StaticGlobalState Abstract.Value
alphaGlobals (StaticGlobalState f g) = StaticGlobalState f (Vec.map alphaGlob g)
alphaGlob :: GlobInst Concrete.Value -> GlobInst Abstract.Value
alphaGlob (GlobInst m v) = GlobInst m (alphaVal v)
alphaVal :: Concrete.Value -> Abstract.Value
alphaVal (Concrete.Value v) = Abstract.Value $ case v of
Wasm.VI32 _ -> VI32 ()
Wasm.VI64 _ -> VI64 ()
Wasm.VF32 _ -> VF32 ()
Wasm.VF64 _ -> VF64 ()
alphaTuple :: (concA -> absA) -> (concB -> absB) -> (concA,concB) -> (absA,absB)
alphaTuple alphaA alphaB (a,b) = (alphaA a, alphaB b)
alphaIgnoreFst :: (concB -> absB) -> (concA,concB) -> absB
alphaIgnoreFst alphaB (_,b) = alphaB b
alphaExcept :: (concA -> absA) -> Concrete.Error (Generic.Exc Concrete.Value) concA -> Except (Abstract.Exc Abstract.Value) absA
alphaExcept alphaA = either
(Except.Fail . alphaExc)
(Except.Success . alphaA)
. Concrete.toEither
alphaExc :: (Generic.Exc Concrete.Value) -> (Abstract.Exc Abstract.Value)
alphaExc exc = Abstract.Exc $ HashSet.singleton $ convert exc
where convert (Generic.Jump i vs) = Generic.Jump i $ map alphaVal vs
convert (Generic.CallReturn vs) = Generic.CallReturn $ map alphaVal vs
alphaJoinList :: JoinList Concrete.Value -> JoinList Abstract.Value
alphaJoinList (JoinList l) = alphaList l
alphaList :: [Concrete.Value] -> JoinList Abstract.Value
alphaList l = JoinList $ map alphaVal l
isSoundlyAbstracted :: ValidModule -> String -> [[Concrete.Value]] -> IO Bool
isSoundlyAbstracted valMod func argsList = do
-- instatiate the module
Right (concModInst, concState, concMem, concTab) <- instantiateConcrete valMod
Right (absModInst, absState, absTab) <- instantiateAbstract valMod
-- compute the abstract arguments
let (JoinList absArgs) = foldr1 () $ (map (JoinList . map alphaVal)) $ argsList
-- run concrete interpreter for each argument list
let concResults = map (Concrete.invokeExported concState concMem concTab concModInst (pack func)) argsList
-- run abstract interpreter with abstract argument list
let absResultRaw = Abstract.invokeExported absState absTab absModInst (pack func) absArgs
let absResult = convertAbsResult absResultRaw
-- check soundness
return $ alphaResults concResults absResult
......@@ -3,41 +3,20 @@
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.MonotoneErrors(toSet)
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
......@@ -46,7 +25,9 @@ main = hspec spec
term :: Terminating a -> a
term (Terminating a) = a
term _ = error "not defined"
getFunctionBody :: Function -> Expression
getFunctionBody (Function _ _ b) = b
readModule :: String -> IO ValidModule
......@@ -58,297 +39,63 @@ readModule path = do
runFunc :: String -> String -> [U.Value] -> IO Result
runFunc modName funcName args = do
mod <- readModule ("test/samples/" ++ modName ++ ".wast")
Right (modInst, staticS, tabs) <- instantiateTaint mod
m <- readModule ("test/samples/" ++ modName ++ ".wast")
Right (modInst, staticS, tabs) <- instantiateTaint m
return $ invokeExported staticS tabs modInst (pack funcName) args
succResult :: Result -> [Value]
succResult (_,(Terminating (Success (_,(_,(Exc.Success (_,result))))))) = result
succResult (_,(_,(Terminating (_,(_,(Exc.Success (_,result))))))) = result
succResult _ = error "not defined"
terminatedSucc :: Result -> Bool
terminatedSucc (_, (errs, Terminating (_,(_,(Exc.Success _))))) = HashSet.null (toSet errs)
terminatedSucc (_, (errs, NonTerminating)) = HashSet.null (toSet errs)
terminatedSucc _ = False
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
terminatedErr :: Result -> Bool
terminatedErr (_,(errs, NonTerminating)) = not $ HashSet.null (toSet errs)
terminatedErr _ = False
errResult :: Result -> Err
errResult (_,(Terminating (Fail x))) = x
terminatedMaybeErr :: Result -> Bool
terminatedMaybeErr (_,(errs, Terminating (_,(_,(Exc.Success _))))) = not $ HashSet.null (toSet errs)
terminatedMaybeErr _ = False
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 ()]
result `shouldSatisfy` terminatedSucc
(succResult result) `shouldBe` [taintValue Tainted (VI32 ())]
it "run noop" $ do
result <- runFunc "simple" "noop" []
result `shouldSatisfy` terminatedSucc
(succResult result) `shouldBe` [taintValue Untainted (VI32 ())]
it "run test2" $ do
result <- runFunc "simple" "test2" []
result `shouldSatisfy` terminatedSucc
(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 ())]
result `shouldSatisfy` terminatedMaybeErr
(succResult result) `shouldBe` [taintValue Taint.Top (VI32 ())]
it "test-mem2" $ do
result <- runFunc "simple" "test-mem2" []
result `shouldSatisfy` terminatedMaybeErr
(succResult result) `shouldBe` [taintValue Tainted (VI32 ())]
it "run fact" $ do
result <- runFunc "fact" "fac-rec" [U.Value $ VI64 ()]
let cfg = fst result
--putStrLn $ show cfg
result `shouldSatisfy` terminatedSucc
(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