Commit 451f4902 authored by Katharina Brandl's avatar Katharina Brandl
Browse files

Testing of sound approximation of UnitAnalysis

parent b9e3cde4
Pipeline #109099 passed with stages
in 75 minutes and 55 seconds
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
module Soundness where
import Abstract (BaseValue(..))
import qualified Abstract as Abstract
import qualified Concrete as Concrete
import qualified ConcreteInterpreter as Concrete
import qualified GenericInterpreter as Generic
import qualified UnitAnalysis as UnitA
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 qualified Data.Concrete.Error as CE
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 absResult = resultToAbsList $ snd $ UnitA.invokeExported absStore absModInst (pack func) absArgs
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
......@@ -3,7 +3,10 @@
module UnitSpec where
import Abstract (BaseValue(..))
import qualified Concrete as Concrete
import qualified ConcreteInterpreter as Concrete
import UnitAnalysis
import Soundness
import GenericInterpreter(Exc(..))
import Control.Arrow.Transformer.Abstract.WasmFrame (Vector(..))
......@@ -33,19 +36,26 @@ main = hspec spec
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
spec :: Spec
spec = do
it "run noop" $ do
let path = "test/samples/simple.wast"
content <- LBS.readFile path
let Right m = parse content
let Right validMod = validate m
validMod <- readModule "test/samples/simple.wast"
Right (modInst, store) <- instantiate validMod
let (log, Success (locals,(Lower state,(Exc.Success (stack,result))))) = invokeExported store modInst (pack "noop") []
locals `shouldBe` (Vector $ Vec.empty)
stack `shouldBe` []
result `shouldBe` [Value $ Lower $ VI32 ()]
--result `shouldBe` [Value $ Wasm.VI32 0]
let args = [[]]
sound <- isSoundlyAbstracted validMod "noop" args
sound `shouldBe` True
it "run test-br3" $ do
let path = "test/samples/simple.wast"
......@@ -55,6 +65,9 @@ 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 ()]
let args = [[Concrete.Value $ Wasm.VI32 10]]
sound <- isSoundlyAbstracted validMod "test-br3" args
sound `shouldBe` True
it "run test-br-and-return" $ do
let path = "test/samples/simple.wast"
......@@ -64,6 +77,9 @@ spec = do
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 ()]
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"
......@@ -73,6 +89,9 @@ spec = do
Right (modInst, store) <- instantiate validMod
let (_, (Success (_,(_,(Exc.Success (_, res)))))) = 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"
......@@ -82,6 +101,9 @@ spec = do
Right (modInst, store) <- instantiate validMod
let (_, (Success (_,(_,(Exc.Success (_, res)))))) = 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"
......@@ -91,6 +113,9 @@ spec = do
Right (modInst, store) <- instantiate validMod
let (_, (Success (_,(_,(Exc.Success (_, res)))))) = 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"
......@@ -100,6 +125,9 @@ spec = do
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"]
let args = [[]]
sound <- isSoundlyAbstracted validMod "test-unreachable4" args
sound `shouldBe` True
it "run test-unreachable5" $ do
let path = "test/samples/simple.wast"
......@@ -109,6 +137,9 @@ spec = do
Right (modInst, store) <- instantiate validMod
let (_, (Success (_,(_,(Exc.Success (_, res)))))) = 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
......@@ -119,6 +150,9 @@ spec = do
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 ()]
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"
......@@ -128,6 +162,9 @@ spec = do
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 ()]
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"
......
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