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

Added innermost fixpoint to abstract interpreter

parent 451f4902
Pipeline #111103 passed with stages
in 75 minutes and 23 seconds
......@@ -59,7 +59,9 @@ data GlobalState v = GlobalState {
funcInstances :: Vector FuncInst,
tableInstances :: Vector TableInst,
globalInstances:: Vector (FreeCompletion (GlobInst v))
} deriving (Show)
} deriving (Show,Eq,Generic)
instance (Hashable v) => Hashable (GlobalState v)
instance (PreOrd v) => PreOrd (GlobalState v) where
s1 s2 = let gs1 = globalInstances s1 in
......
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
module Concrete where
import Data.Abstract.FreeCompletion
import Data.Hashable
import Data.Order
import Data.Vector (Vector, (!), (//))
import qualified Data.Vector as Vec
......@@ -13,8 +15,12 @@ import Language.Wasm.Interpreter (ModuleInstance)
import qualified Language.Wasm.Interpreter as Wasm
import Language.Wasm.Structure hiding (exports, Const)
import GHC.Generics
newtype Value = Value Wasm.Value deriving (Show, Eq)
data Mut = Const | Mutable deriving (Show, Eq)
data Mut = Const | Mutable deriving (Show, Eq, Generic)
instance Hashable Mut
data GlobalState v = GlobalState {
funcInstances :: Vector FuncInst,
......@@ -40,11 +46,40 @@ data FuncInst =
| HostInst {
funcType :: FuncType
--hostCode :: HostFunction v c
} deriving (Show,Eq)
} deriving (Show,Eq, Generic)
newtype TableInst = TableInst Wasm.TableInstance deriving (Show,Eq)
instance (Hashable v) => Hashable (Vector v) where
hashWithSalt salt v = hashWithSalt salt (Vec.toList v)
instance Hashable MemArg
instance Hashable BitSize
instance Hashable IUnOp
instance Hashable IBinOp
instance Hashable IRelOp
instance Hashable FUnOp
instance Hashable FBinOp
instance Hashable FRelOp
instance Hashable Wasm.ExportInstance
deriving instance Generic Wasm.ExportInstance
instance Hashable Wasm.ExternalValue
deriving instance Generic Wasm.ExternalValue
instance (Hashable v) => Hashable (Instruction v)
instance Hashable ValueType
instance Hashable Function
instance Hashable FuncInst
instance Hashable FuncType
instance Hashable ModuleInstance
deriving instance Generic ModuleInstance
instance Hashable TableInst
instance Hashable Wasm.TableInstance
deriving instance Generic Wasm.TableInstance
instance Hashable Limit
newtype TableInst = TableInst Wasm.TableInstance deriving (Show,Eq,Generic)
data MemInst = MemInst (Maybe Word32) (Vector Word8) deriving (Show,Eq)
data GlobInst v = GlobInst Mut v deriving (Show, Eq)
data GlobInst v = GlobInst Mut v deriving (Show, Eq, Generic)
instance (Hashable v) => Hashable (GlobInst v)
instance (PreOrd v) => PreOrd (GlobInst v) where
(GlobInst m1 v1) (GlobInst m2 v2) = m1 == m2 && v1 v2
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
......@@ -30,13 +31,17 @@ import Control.Arrow.Utils hiding (zipWith, all)
import Control.Arrow.WasmFrame
import Control.Arrow.Writer
import Data.Hashable
import Data.Order
import Data.Profunctor
import Data.Coerce
import GHC.Generics
import GHC.Exts
newtype AbsList v = AbsList [v] deriving (Show,Eq)
newtype AbsList v = AbsList [v] deriving (Show,Eq,Generic)
instance (Hashable v) => Hashable (AbsList v)
instance (PreOrd v) => PreOrd (AbsList v) where
(AbsList v1) (AbsList v2) = all id $ zipWith () v1 v2
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
......@@ -8,6 +9,8 @@
module Control.Arrow.Transformer.Abstract.WasmFrame where
import Concrete
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Except
......@@ -26,12 +29,21 @@ import Control.Arrow.Transformer.State
import Control.Category hiding (id)
import Data.Hashable
import Data.Monoidal (shuffle1)
import Data.Order
import Data.Profunctor
import qualified Data.Vector as Vec
newtype Vector v = Vector (Vec.Vector v) deriving (Show,Eq)
import GHC.Generics
newtype Vector v = Vector (Vec.Vector v) deriving (Show,Eq,Generic)
instance (Hashable v) => Hashable (Vector v)
---- hashWithSalt salt (Vector v) = hashWithSalt salt (Vec.toList v)
--
--instance (Hashable v) => Hashable (Vec.Vector v) where
-- hashWithSalt salt v = hashWithSalt salt (Vec.toList v)
instance (PreOrd v) => PreOrd (Vector v) where
(Vector v1) (Vector v2) = all id $ Vec.zipWith () v1 v2
......
......@@ -73,7 +73,8 @@ class IsException exc v c | c -> v where
-- x ⊑ y | x == y = True
-- used for storing the return "arity" of nested labels
newtype LabelArities = LabelArities {labels :: [Natural]}
newtype LabelArities = LabelArities {labels :: [Natural]} deriving (Eq,Show,Generic)
instance Hashable LabelArities
-- stores a frame's static data (return arity and module instance)
type FrameData = (Natural, ModuleInstance)
......
......@@ -22,7 +22,8 @@ import Control.Arrow.Const
import Control.Arrow.Logger
import Control.Arrow.Except
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Fix as Fix
import Control.Arrow.Fix.Chaotic (innermost)
import Control.Arrow.MemAddress
import Control.Arrow.Memory
import Control.Arrow.MemSizable
......@@ -38,6 +39,11 @@ import Control.Arrow.WasmFrame
import Control.Arrow.Transformer.Abstract.Except
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable
import Control.Arrow.Transformer.Abstract.Fix.Component
import qualified Control.Arrow.Transformer.Abstract.Fix.Stack as Fix
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Arrow.Transformer.Abstract.DebuggableStack
import Control.Arrow.Transformer.Abstract.Logger
......@@ -52,6 +58,7 @@ import Control.Category (Category)
import Data.Abstract.FreeCompletion as FC
import Data.Abstract.Sign
import qualified Data.Abstract.Sign as S
import Data.Abstract.Terminating
import qualified Data.Function as Function
import Data.Hashable
import Data.HashSet as HashSet
......@@ -212,19 +219,35 @@ instance ArrowFix (Underlying (GlobalStateT v c) x y) => ArrowFix (GlobalStateT
deriving instance (ArrowComplete (FreeCompletion (GlobalState v), y) c) => ArrowComplete y (GlobalStateT v c)
type In = (Pow.Pow [String],
(Vector Value,
((Natural, ModuleInstance),
(FreeCompletion (GlobalState Value),
(AbsList Value, (LabelArities, [Instruction Natural]))))))
type Out = Terminating
(Pow.Pow [String],
Error
(Pow String)
(Vector Value,
(FreeCompletion (GlobalState Value),
Except (Exc Value) (AbsList Value, ()))))
invokeExported :: GlobalState Value
-> ModuleInstance
-> Text
-> [Value]
-> (Pow.Pow [String],
-> Terminating (Pow.Pow [String],
Error (Pow String)
(Vector Value,
(FreeCompletion (GlobalState Value),
Except (Exc Value)
(AbsList Value, [Value]))))
invokeExported store modInst funcName args =
let ?fixpointAlgorithm = Function.fix in -- TODO: we need something else here
Trans.run
let ?cacheWidening = error "todo" in
--let ?fixpointAlgorithm = Function.fix in -- TODO: we need something else here
let ?fixpointAlgorithm = fixpointAlgorithm $ Fix.filter isLoop $ innermost in
snd $ Trans.run
(Generic.invokeExported ::
ValueT Value
(ReaderT Generic.LabelArities
......@@ -234,7 +257,16 @@ invokeExported store modInst funcName args =
(FrameT FrameData Value
(ErrorT (Pow String)
(LoggerT String
(->)))))))) (Text, [Value]) [Value]) (Pow.singleton [],(Vector $ Vec.empty,((0,modInst),(Lower store,([],(Generic.LabelArities [],(funcName, args)))))))
(TerminatingT
(FixT
(ComponentT Component In
(Fix.StackT Fix.Stack In
(CacheT Cache In Out
(->))))))))))))) (Text, [Value]) [Value]) (Pow.singleton [],(Vector $ Vec.empty,((0,modInst),(Lower store,([],(Generic.LabelArities [],(funcName, args)))))))
where
isLoop (_,(_,(_,(_,(_,(_,inst)))))) = case inst of
Loop {} : _ -> True
_ -> False
instantiate :: ValidModule -> IO (Either String (ModuleInstance, GlobalState Value))
instantiate valMod = do
......
......@@ -18,6 +18,7 @@ import Data.Abstract.Except (Except)
import qualified Data.Abstract.Except as Except
import Data.Abstract.FreeCompletion
import Data.Abstract.DiscretePowerset (Pow(..))
import Data.Abstract.Terminating
import qualified Data.Concrete.Error as CE
import qualified Data.HashSet as HashSet
import Data.Order
......@@ -35,13 +36,13 @@ type ConcResult = CE.Error
CE.Error
(Generic.Exc Concrete.Value)
([Concrete.Value], [Concrete.Value])))
type AbsResult = AE.Error
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)))
(AbsList UnitA.Value, AbsList UnitA.Value))))
alphaResult :: [ConcResult] -> AbsResult
alphaResult = alphaError alphaString1
......@@ -107,7 +108,8 @@ isSoundlyAbstracted mod func argsList = do
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
let (Terminating temp) = UnitA.invokeExported absStore absModInst (pack func) absArgs
let absResult = resultToAbsList $ snd $ temp
return $ alphaResult concResults absResult
where
......
......@@ -15,6 +15,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.Terminating
import qualified Data.HashSet as HashSet
import Data.List (isInfixOf)
import Data.List.Singleton (singleton)
......@@ -34,6 +35,9 @@ import Test.Hspec
main :: IO ()
main = hspec spec
term :: Terminating a -> a
term (Terminating a) = a
getFunctionBody (Function _ _ b) = b
readModule :: String -> IO ValidModule
......@@ -49,10 +53,11 @@ spec = do
it "run noop" $ do
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") []
let (log, 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
......@@ -63,7 +68,7 @@ spec = do
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-br3") [Value $ Lower $ VI32 ()]
let (_, (Success (_,(_,(Exc.Success (_,result)))))) = term $ 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
......@@ -75,7 +80,7 @@ spec = do
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 ()]
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
......@@ -87,7 +92,7 @@ spec = do
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") []
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
......@@ -99,7 +104,7 @@ spec = do
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") []
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
......@@ -111,7 +116,7 @@ spec = do
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") []
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
......@@ -123,7 +128,7 @@ spec = do
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") []
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
......@@ -135,7 +140,7 @@ spec = do
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 ()]
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
......@@ -148,7 +153,7 @@ spec = do
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 ()]
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
......@@ -160,7 +165,7 @@ spec = do
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 ()]
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
......@@ -172,7 +177,7 @@ spec = do
-- let Right m = parse content
-- let Right validMod = validate m
-- Right (modInst, store) <- instantiate validMod
-- let (_,(Success (_,(_,(Success (_,result)))))) = invokeExported store modInst (pack "const") [Value $ Wasm.VI32 5]
-- 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
......@@ -181,7 +186,7 @@ spec = do
-- let Right m = parse content
-- let Right validMod = validate m
-- Right (modInst, store) <- instantiate validMod
-- let (_, (Success (_,(_,(Success (_,result1)))))) = invokeExported store modInst (pack "half-fac") [Value $ Wasm.VI32 0]
-- 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
......@@ -192,7 +197,7 @@ spec = do
-- --let halfFac64Code = (getFunctionBody . (!! 3) . functions . getModule) validMod
-- --putStrLn $ show validMod
-- Right (modInst, store) <- instantiate validMod
-- let (_, (Success (_,(_,(Success (_,result1)))))) = invokeExported store modInst (pack "half-fac-64") [Value $ Wasm.VI64 0]
-- 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 ""
......@@ -208,7 +213,7 @@ spec = do
-- --putStrLn ""
-- Right (modInst, store) <- instantiate validMod
-- let params = map (singleton . Value . Wasm.VI64) [0 .. 8]
-- let results = map (invokeExported store modInst (pack "fac-rec")) params
-- 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
......@@ -228,5 +233,5 @@ spec = do
-- let Right m = parse content
-- let Right validMod = validate m
-- Right (modInst, store) <- instantiate validMod
-- let (_, (Success (_,(_,(Success (_,result)))))) = invokeExported store modInst (pack "test-mem") [Value $ Wasm.VI32 42]
-- let (_, (Success (_,(_,(Success (_,result)))))) = term $ invokeExported store modInst (pack "test-mem") [Value $ Wasm.VI32 42]
-- result `shouldBe` [Value $ Wasm.VI32 43]
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