diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -10,7 +10,7 @@ ## Dependencies * `ghc >= 8.0.1` -## Install +## Installation with Cabal `cabal install SSTG` ## As an API @@ -27,7 +27,7 @@ This can be extracted from Haskell source by performing a call to the function: ``` -mkTargetBindings :: FilePath -> FilePath -> IO [SSTG.Binding] +mkTargetBindings :: FilePath -> FilePath -> IO [Binding] mkTargetBinding proj src = ... ``` @@ -45,15 +45,48 @@ proj = path/to/stuff src = path/to/stuff/folder-one/source.hs ``` -The extracted `[SSTG.Binding]`, like almost everything in SSTG, is endowed with `Show, Equal, Read`. However, it is advised to use the pretty-print functions defined in `SSTG.Utils.Printing`. For instance: +The extracted `[Binding]`, like almost everything in SSTG, is endowed with `Show, Equal, Read`. However, it is advised to use the pretty-print functions defined in `SSTG.Utils.Printing`. For instance: ``` -pprBindingStr :: SSTG.Binding -> String +pprBindingStr :: Binding -> String ``` -#### Defunctionalizatoin +#### Defunctionalization +HEY KIDS YA EVER WANNA REASON ABOUT HIGHER-ORDER FUNCTIONS BUT YOUR SMT SOLVER AIN'T SMAHT ENOUGH??? CHECK OUT THIS [COOL WIKIPEDIA ARTICLE RIGHT HERE!!!][defunctionalization] +[defunctionalization]: https://en.wikipedia.org/wiki/Defunctionalization + #### Symbolic Execution +Symbolic execution is done by performin a series of graph reductions on a `State` until we reach some value form, or our `step_count` tick runs out, creating a form of bounded execution exploration. +To load a `State`, two functions can be used: +``` +data LoadResult = LoadOkay State | LoadGuess State [Binding] | LoadError String + +newtype Program = Program [Binding] + +loadState :: Program -> LoadResult + +loadStateEntry :: String -> Program -> LoadResult +``` +Next we have to fill out the flags for execution: +``` +data StepType = BFS | BFSLogged | DFS | DFSLogged + +data RunFlags = RunFlags { step_count :: Int + , step_type :: StepType + , dump_dir :: Maybe FilePath } +``` +Here `step_count` is the number of steps we may take, the `step_type` is currently only implemented for `BFS` and `BFSLogged`, the latter of which keeps track of every step taken, while `BFS` only returns the very last state. Note that `BFSLogged` is currently unoptimized because it is easy to implement that way :) + +Finally, to perform execution, the `execute` function is used: +``` +execute :: RunFlags -> State -> [([LiveState], [DeadState])] +``` +This yields a list of execution snapshots. The list is a singleton list if `BFS` or `DFS` is used, while multiple snapshots if the `BFSLogged` or `DFSLogged` is done. These can be then printed by using `pprLivesDeadsStr`: +``` +pprLivesDeadsStr :: ([LiveState], [DeadState]) -> String +``` + #### Constraint Solving To come. @@ -61,6 +94,6 @@ * Defunctionalization pre-processing * SMT integration -## Shortcommings +## Shortcomings * Uninterpreted function evaluations are abstracted as symbolic computations. This includes all functions defined in `Prelude` and those not defined in the scope of the target programs. * There might be bugs, who knows? :) diff --git a/SSTG.cabal b/SSTG.cabal --- a/SSTG.cabal +++ b/SSTG.cabal @@ -1,5 +1,5 @@ name: SSTG -version: 0.1.0.6 +version: 0.1.0.7 synopsis: STG Symbolic Execution description: Prototype of STG-based Symbolic Execution for Haskell. homepage: https://github.com/AntonXue/SSTG#readme @@ -21,13 +21,13 @@ , SSTG.Core.Translation.Haskell , SSTG.Core.Syntax , SSTG.Core.Syntax.Language - , SSTG.Core.Syntax.Typecheck + , SSTG.Core.Syntax.Typing , SSTG.Core.Execution , SSTG.Core.Execution.Engine - , SSTG.Core.Execution.Models , SSTG.Core.Execution.Naming , SSTG.Core.Execution.Rules , SSTG.Core.Execution.Stepping + , SSTG.Core.Execution.Support , SSTG.Utils , SSTG.Utils.Printing , SSTG.Utils.FileIO diff --git a/src/SSTG/Core/Execution.hs b/src/SSTG/Core/Execution.hs --- a/src/SSTG/Core/Execution.hs +++ b/src/SSTG/Core/Execution.hs @@ -1,15 +1,15 @@ -- | Export Module for SSTG.Core.Execution module SSTG.Core.Execution ( module SSTG.Core.Execution.Engine - , module SSTG.Core.Execution.Models , module SSTG.Core.Execution.Naming , module SSTG.Core.Execution.Rules , module SSTG.Core.Execution.Stepping + , module SSTG.Core.Execution.Support ) where import SSTG.Core.Execution.Engine -import SSTG.Core.Execution.Models import SSTG.Core.Execution.Naming import SSTG.Core.Execution.Rules import SSTG.Core.Execution.Stepping +import SSTG.Core.Execution.Support diff --git a/src/SSTG/Core/Execution/Engine.hs b/src/SSTG/Core/Execution/Engine.hs --- a/src/SSTG/Core/Execution/Engine.hs +++ b/src/SSTG/Core/Execution/Engine.hs @@ -10,9 +10,9 @@ ) where import SSTG.Core.Syntax -import SSTG.Core.Execution.Models import SSTG.Core.Execution.Naming import SSTG.Core.Execution.Stepping +import SSTG.Core.Execution.Support import qualified Data.Map as M diff --git a/src/SSTG/Core/Execution/Models.hs b/src/SSTG/Core/Execution/Models.hs deleted file mode 100644 --- a/src/SSTG/Core/Execution/Models.hs +++ /dev/null @@ -1,213 +0,0 @@ --- | Symbolic STG Execution Models -module SSTG.Core.Execution.Models - ( module SSTG.Core.Execution.Models - ) where - -import SSTG.Core.Syntax - -import qualified Data.Map as M - --- | Symbolic Transformation represents transformations applied to some --- State`(s). This is useful in allowing us to transfer from different actions --- within the engine. -newtype SymbolicT s a = SymbolicT { run :: s -> (s, a) } - --- | Functor instance of Symbolic Transformation. -instance Functor (SymbolicT s) where - fmap f st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 in (s1, f a1)) - --- | Applicative instance of Symbolic Transformation. -instance Applicative (SymbolicT s) where - pure a = SymbolicT (\s -> (s, a)) - sf <*> st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 - (s2, f2) = (run sf) s1 in (s2, f2 a1)) - --- | Monad instance of Symbolic Transformation. -instance Monad (SymbolicT s) where - return a = pure a - st >>= fs = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 - (s2, a2) = (run (fs a1)) s1 in (s2, a2)) - --- | `State` contains the information necessary to perform symbolic execution. --- Eval/Apply graph reduction semantics are used. -data State = State { state_status :: Status - , state_stack :: Stack - , state_heap :: Heap - , state_globals :: Globals - , state_code :: Code - , state_names :: [Name] - , state_paths :: PathCons - , state_links :: SymLinks - } deriving (Show, Eq, Read) - --- | Symbolic variables. The @Maybe (Expr, Locals)@ can be used to trace the --- source from which the symbolic variable was generated. For instance, this is --- useful during symbolic function application. -data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read) - --- | State status. -data Status = Status { steps :: Int - } deriving (Show, Eq, Read) - --- | Execution stack used in graph reduction semnatics. -newtype Stack = Stack [Frame] deriving (Show, Eq, Read) - --- | Frames of a stack. -data Frame = CaseFrame Var [Alt] Locals - | ApplyFrame [Atom] Locals - | UpdateFrame MemAddr - deriving (Show, Eq, Read) - --- | Memory address for things on the `Heap`. -newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord) - --- | A `Value` is something that we aim to reduce our current expression down --- into. `MemAddr` is a pointer to an object on the heap, such as `FunObj` or --- `ConObj`, which are "returned" from expression evaluation in this form. -data Value = LitVal Lit - | MemVal MemAddr - deriving (Show, Eq, Read) - --- | Locals binds a `Var`'s `Name` to its some `Value`. -newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read) - --- | Heaps map `MemAddr` to `HeapObj`, while keeping track of the last address --- that was allocated. This allows us to consistently allocate fresh addresses --- on the `Heap`. -data Heap = Heap (M.Map MemAddr HeapObj) MemAddr deriving (Show, Eq, Read) - --- | Heap objects. -data HeapObj = LitObj Lit - | SymObj Symbol - | ConObj DataCon [Value] - | FunObj [Var] Expr Locals - | Blackhole - deriving (Show, Eq, Read) - --- | Globals are statically loaded at the time when a `State` is loaded. --- However, because uninterpreted / out-of-scope variables are made symbolic --- at runtime, it can be modified during execution. -newtype Globals = Globals (M.Map Name Value) deriving (Show, Eq, Read) - --- | Evaluation of the current expression. We are either evaluating, or ready --- to return with some `Value`. -data Code = Evaluate Expr Locals - | Return Value - deriving (Show, Eq, Read) - --- | Path constraints. -type PathCons = [PathCond] - --- | Path conditions denote logical paths taken in program execution thus far. -data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool - deriving (Show, Eq, Read) - --- | Symbolic link tables helps keep track of what names went to what, what? -newtype SymLinks = SymLinks (M.Map Name Name) deriving (Show, Eq, Read) - --- Simple functions that require only the immediate data structure. - --- | A `Name`'s occurrence string. -nameOccStr :: Name -> String -nameOccStr (Name occ _ _ _) = occ - --- | Name's unique `Int` key. -nameUnique :: Name -> Int -nameUnique (Name _ _ _ unq) = unq - --- | Variable name. -varName :: Var -> Name -varName (Var name _) = name - --- | `MemAddr`'s `Int` value. -memAddrInt :: MemAddr -> Int -memAddrInt (MemAddr int) = int - --- | `Locals` lookup. -lookupLocals :: Var -> Locals -> Maybe Value -lookupLocals var (Locals lmap) = M.lookup (varName var) lmap - --- | `Locals` insertion. -insertLocals :: Var -> Value -> Locals -> Locals -insertLocals var val (Locals lmap) = Locals lmap' - where lmap' = M.insert (varName var) val lmap - --- | List insertion into `Locals`. -insertLocalsList :: [(Var, Value)] -> Locals -> Locals -insertLocalsList [] locals = locals -insertLocalsList ((var, val):vvs) locals = insertLocalsList vvs locals' - where locals' = insertLocals var val locals - --- | `Heap` lookup. -lookupHeap :: MemAddr -> Heap -> Maybe HeapObj -lookupHeap addr (Heap hmap _) = M.lookup addr hmap - --- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`. -allocHeap :: HeapObj -> Heap -> (Heap, MemAddr) -allocHeap hobj (Heap hmap prev) = (Heap hmap' addr, addr) - where addr = MemAddr ((memAddrInt prev) + 1) - hmap' = M.insert addr hobj hmap - --- | Allocate a list of `HeapObj` in a `Heap`, returning in the same order the --- `MemAddr` at which they have been allocated at. -allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr]) -allocHeapList [] heap = (heap, []) -allocHeapList (hobj:hobjs) heap = (heapf, addr : as) - where (heap', addr) = allocHeap hobj heap - (heapf, as) = allocHeapList hobjs heap' - --- | `Heap` direct insertion at a specific `MemAddr`. -insertHeap :: MemAddr -> HeapObj -> Heap -> Heap -insertHeap addr hobj (Heap hmap prev) = Heap hmap' prev - where hmap' = M.insert addr hobj hmap - --- | Insert a list of `HeapObj` at specified `MemAddr` locations. -insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap -insertHeapList [] heap = heap -insertHeapList ((addr, hobj):ahs) heap = insertHeapList ahs heap' - where heap' = insertHeap addr hobj heap - --- | `Globals` lookup. -lookupGlobals :: Var -> Globals -> Maybe Value -lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap - --- | `Globals` insertion. -insertGlobals :: Var -> Value -> Globals -> Globals -insertGlobals var val (Globals gmap) = Globals gmap' - where gmap' = M.insert (varName var) val gmap - --- | Insert a list of `Var` and `Value` pairs into `Globals`. This would --- typically occur for new symbolic variables created from uninterpreted / --- out-of-scope variables during runtime. -insertGlobalsList :: [(Var, Value)] -> Globals -> Globals -insertGlobalsList [] globals = globals -insertGlobalsList ((var, val):vvs) globals = insertGlobalsList vvs globals' - where globals' = insertGlobals var val globals - --- Complex functions that involve multiple data structures. - --- | `Value` lookup from the `Locals` first, then `Globals`. -lookupValue :: Var -> Locals -> Globals -> Maybe Value -lookupValue var locals globals = case lookupLocals var locals of - Nothing -> lookupGlobals var globals - mb_val -> mb_val - --- | `Heap` lookup. Returns the corresponding `MemAddr` and `HeapObj` if found. -vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj) -vlookupHeap var locals globals heap = do - val <- lookupValue var locals globals - case val of - LitVal _ -> Nothing - MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj) - --- | Type of `HeapObj` held at `MemAddr`, if found. -memAddrType :: MemAddr -> Heap -> Maybe Type -memAddrType addr heap = do - hobj <- lookupHeap addr heap - Just $ case hobj of - Blackhole -> Bottom - LitObj lit -> litType lit - SymObj (Symbol s _) -> varType s - ConObj dcon _ -> dataConType dcon - FunObj prms expr _ -> foldr FunTy (exprType expr) (map varType prms) - diff --git a/src/SSTG/Core/Execution/Naming.hs b/src/SSTG/Core/Execution/Naming.hs --- a/src/SSTG/Core/Execution/Naming.hs +++ b/src/SSTG/Core/Execution/Naming.hs @@ -9,7 +9,7 @@ ) where import SSTG.Core.Syntax -import SSTG.Core.Execution.Models +import SSTG.Core.Execution.Support import qualified Data.List as L import qualified Data.Map as M @@ -49,8 +49,8 @@ -- | `Name`s in the `Heap`. heapNames :: Heap -> [Name] -heapNames (Heap heap _) = concatMap (heapObjNames . snd) kvs - where kvs = M.toList heap +heapNames (Heap heap _) = concatMap (heapObjNames . snd) hlist + where hlist = M.toList heap -- | `Name`s in a `HeapObj`. heapObjNames :: HeapObj -> [Name] @@ -169,8 +169,8 @@ -- | `Name`s in a `SymLinks`. linksNames :: SymLinks -> [Name] -linksNames (SymLinks links) = concatMap (\(a, b) -> [a, b]) kvs - where kvs = M.toList links +linksNames (SymLinks links) = concatMap (\(a, b) -> [a, b]) slist + where slist = M.toList links -- | Create a fresh seed given any `Int`, a `String` seed, and a `Set` of -- `String`s that we do not want our new `String` to conflict with. The sole diff --git a/src/SSTG/Core/Execution/Rules.hs b/src/SSTG/Core/Execution/Rules.hs --- a/src/SSTG/Core/Execution/Rules.hs +++ b/src/SSTG/Core/Execution/Rules.hs @@ -6,8 +6,8 @@ ) where import SSTG.Core.Syntax -import SSTG.Core.Execution.Models import SSTG.Core.Execution.Naming +import SSTG.Core.Execution.Support -- | `Rule`s that are applied during STG reduction. data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt diff --git a/src/SSTG/Core/Execution/Stepping.hs b/src/SSTG/Core/Execution/Stepping.hs --- a/src/SSTG/Core/Execution/Stepping.hs +++ b/src/SSTG/Core/Execution/Stepping.hs @@ -8,8 +8,8 @@ , runBoundedDFSLogged ) where -import SSTG.Core.Execution.Models import SSTG.Core.Execution.Rules +import SSTG.Core.Execution.Support -- | A `State` that is not in value form yet, capable of being evaluated. A -- list of `Rule`s is kept to denote reduction history. diff --git a/src/SSTG/Core/Execution/Support.hs b/src/SSTG/Core/Execution/Support.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Execution/Support.hs @@ -0,0 +1,213 @@ +-- | Symbolic STG Execution Support Architecture +module SSTG.Core.Execution.Support + ( module SSTG.Core.Execution.Support + ) where + +import SSTG.Core.Syntax + +import qualified Data.Map as M + +-- | Symbolic Transformation represents transformations applied to some +-- State`(s). This is useful in allowing us to transfer from different actions +-- within the engine. +newtype SymbolicT s a = SymbolicT { run :: s -> (s, a) } + +-- | Functor instance of Symbolic Transformation. +instance Functor (SymbolicT s) where + fmap f st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 in (s1, f a1)) + +-- | Applicative instance of Symbolic Transformation. +instance Applicative (SymbolicT s) where + pure a = SymbolicT (\s -> (s, a)) + sf <*> st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 + (s2, f2) = (run sf) s1 in (s2, f2 a1)) + +-- | Monad instance of Symbolic Transformation. +instance Monad (SymbolicT s) where + return a = pure a + st >>= fs = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 + (s2, a2) = (run (fs a1)) s1 in (s2, a2)) + +-- | `State` contains the information necessary to perform symbolic execution. +-- Eval/Apply graph reduction semantics are used. +data State = State { state_status :: Status + , state_stack :: Stack + , state_heap :: Heap + , state_globals :: Globals + , state_code :: Code + , state_names :: [Name] + , state_paths :: PathCons + , state_links :: SymLinks + } deriving (Show, Eq, Read) + +-- | Symbolic variables. The @Maybe (Expr, Locals)@ can be used to trace the +-- source from which the symbolic variable was generated. For instance, this is +-- useful during symbolic function application. +data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read) + +-- | State status. +data Status = Status { steps :: Int + } deriving (Show, Eq, Read) + +-- | Execution stack used in graph reduction semnatics. +newtype Stack = Stack [Frame] deriving (Show, Eq, Read) + +-- | Frames of a stack. +data Frame = CaseFrame Var [Alt] Locals + | ApplyFrame [Atom] Locals + | UpdateFrame MemAddr + deriving (Show, Eq, Read) + +-- | Memory address for things on the `Heap`. +newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord) + +-- | A `Value` is something that we aim to reduce our current expression down +-- into. `MemAddr` is a pointer to an object on the heap, such as `FunObj` or +-- `ConObj`, which are "returned" from expression evaluation in this form. +data Value = LitVal Lit + | MemVal MemAddr + deriving (Show, Eq, Read) + +-- | Locals binds a `Var`'s `Name` to its some `Value`. +newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read) + +-- | Heaps map `MemAddr` to `HeapObj`, while keeping track of the last address +-- that was allocated. This allows us to consistently allocate fresh addresses +-- on the `Heap`. +data Heap = Heap (M.Map MemAddr HeapObj) MemAddr deriving (Show, Eq, Read) + +-- | Heap objects. +data HeapObj = LitObj Lit + | SymObj Symbol + | ConObj DataCon [Value] + | FunObj [Var] Expr Locals + | Blackhole + deriving (Show, Eq, Read) + +-- | Globals are statically loaded at the time when a `State` is loaded. +-- However, because uninterpreted / out-of-scope variables are made symbolic +-- at runtime, it can be modified during execution. +newtype Globals = Globals (M.Map Name Value) deriving (Show, Eq, Read) + +-- | Evaluation of the current expression. We are either evaluating, or ready +-- to return with some `Value`. +data Code = Evaluate Expr Locals + | Return Value + deriving (Show, Eq, Read) + +-- | Path constraints. +type PathCons = [PathCond] + +-- | Path conditions denote logical paths taken in program execution thus far. +data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool + deriving (Show, Eq, Read) + +-- | Symbolic link tables helps keep track of what names went to what, what? +newtype SymLinks = SymLinks (M.Map Name Name) deriving (Show, Eq, Read) + +-- Simple functions that require only the immediate data structure. + +-- | A `Name`'s occurrence string. +nameOccStr :: Name -> String +nameOccStr (Name occ _ _ _) = occ + +-- | Name's unique `Int` key. +nameUnique :: Name -> Int +nameUnique (Name _ _ _ unq) = unq + +-- | Variable name. +varName :: Var -> Name +varName (Var name _) = name + +-- | `MemAddr`'s `Int` value. +memAddrInt :: MemAddr -> Int +memAddrInt (MemAddr int) = int + +-- | `Locals` lookup. +lookupLocals :: Var -> Locals -> Maybe Value +lookupLocals var (Locals lmap) = M.lookup (varName var) lmap + +-- | `Locals` insertion. +insertLocals :: Var -> Value -> Locals -> Locals +insertLocals var val (Locals lmap) = Locals lmap' + where lmap' = M.insert (varName var) val lmap + +-- | List insertion into `Locals`. +insertLocalsList :: [(Var, Value)] -> Locals -> Locals +insertLocalsList [] locals = locals +insertLocalsList ((var, val):vvs) locals = insertLocalsList vvs locals' + where locals' = insertLocals var val locals + +-- | `Heap` lookup. +lookupHeap :: MemAddr -> Heap -> Maybe HeapObj +lookupHeap addr (Heap hmap _) = M.lookup addr hmap + +-- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`. +allocHeap :: HeapObj -> Heap -> (Heap, MemAddr) +allocHeap hobj (Heap hmap prev) = (Heap hmap' addr, addr) + where addr = MemAddr ((memAddrInt prev) + 1) + hmap' = M.insert addr hobj hmap + +-- | Allocate a list of `HeapObj` in a `Heap`, returning in the same order the +-- `MemAddr` at which they have been allocated at. +allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr]) +allocHeapList [] heap = (heap, []) +allocHeapList (hobj:hobjs) heap = (heapf, addr : as) + where (heap', addr) = allocHeap hobj heap + (heapf, as) = allocHeapList hobjs heap' + +-- | `Heap` direct insertion at a specific `MemAddr`. +insertHeap :: MemAddr -> HeapObj -> Heap -> Heap +insertHeap addr hobj (Heap hmap prev) = Heap hmap' prev + where hmap' = M.insert addr hobj hmap + +-- | Insert a list of `HeapObj` at specified `MemAddr` locations. +insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap +insertHeapList [] heap = heap +insertHeapList ((addr, hobj):ahs) heap = insertHeapList ahs heap' + where heap' = insertHeap addr hobj heap + +-- | `Globals` lookup. +lookupGlobals :: Var -> Globals -> Maybe Value +lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap + +-- | `Globals` insertion. +insertGlobals :: Var -> Value -> Globals -> Globals +insertGlobals var val (Globals gmap) = Globals gmap' + where gmap' = M.insert (varName var) val gmap + +-- | Insert a list of `Var` and `Value` pairs into `Globals`. This would +-- typically occur for new symbolic variables created from uninterpreted / +-- out-of-scope variables during runtime. +insertGlobalsList :: [(Var, Value)] -> Globals -> Globals +insertGlobalsList [] globals = globals +insertGlobalsList ((var, val):vvs) globals = insertGlobalsList vvs globals' + where globals' = insertGlobals var val globals + +-- Complex functions that involve multiple data structures. + +-- | `Value` lookup from the `Locals` first, then `Globals`. +lookupValue :: Var -> Locals -> Globals -> Maybe Value +lookupValue var locals globals = case lookupLocals var locals of + Nothing -> lookupGlobals var globals + mb_val -> mb_val + +-- | `Heap` lookup. Returns the corresponding `MemAddr` and `HeapObj` if found. +vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj) +vlookupHeap var locals globals heap = do + val <- lookupValue var locals globals + case val of + LitVal _ -> Nothing + MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj) + +-- | Type of `HeapObj` held at `MemAddr`, if found. +memAddrType :: MemAddr -> Heap -> Maybe Type +memAddrType addr heap = do + hobj <- lookupHeap addr heap + Just $ case hobj of + Blackhole -> Bottom + LitObj lit -> litType lit + SymObj (Symbol s _) -> varType s + ConObj dcon _ -> dataConType dcon + FunObj prms expr _ -> foldr FunTy (exprType expr) (map varType prms) + diff --git a/src/SSTG/Core/Syntax.hs b/src/SSTG/Core/Syntax.hs --- a/src/SSTG/Core/Syntax.hs +++ b/src/SSTG/Core/Syntax.hs @@ -1,9 +1,9 @@ -- | Export Module for SSTG.Syntax module SSTG.Core.Syntax ( module SSTG.Core.Syntax.Language - , module SSTG.Core.Syntax.Typecheck + , module SSTG.Core.Syntax.Typing ) where import SSTG.Core.Syntax.Language -import SSTG.Core.Syntax.Typecheck +import SSTG.Core.Syntax.Typing diff --git a/src/SSTG/Core/Syntax/Language.hs b/src/SSTG/Core/Syntax/Language.hs --- a/src/SSTG/Core/Syntax/Language.hs +++ b/src/SSTG/Core/Syntax/Language.hs @@ -22,7 +22,7 @@ type TyCon = GenTyCon Name type AlgTyRhs = GenAlgTyRhs Name --- | A Program is defined as a list of bindings. The @bnd@ is an identifier +-- | A `Program` is defined as a list of bindings. The @bnd@ is an identifier -- that determines a unique binder to the @var@. In practice, these are defined -- to be `Name` and `Var` respectively. newtype GenProgram bnd var = Program [GenBinding bnd var] diff --git a/src/SSTG/Core/Syntax/Typecheck.hs b/src/SSTG/Core/Syntax/Typecheck.hs deleted file mode 100644 --- a/src/SSTG/Core/Syntax/Typecheck.hs +++ /dev/null @@ -1,53 +0,0 @@ --- | Typing Module -module SSTG.Core.Syntax.Typecheck - ( module SSTG.Core.Syntax.Typecheck - ) where - -import SSTG.Core.Syntax.Language - --- | Variable type. -varType :: Var -> Type -varType (Var _ ty) = ty - --- | Literal type. -litType :: Lit -> Type -litType (MachChar _ ty) = ty -litType (MachStr _ ty) = ty -litType (MachInt _ ty) = ty -litType (MachWord _ ty) = ty -litType (MachFloat _ ty) = ty -litType (MachDouble _ ty) = ty -litType (MachNullAddr ty) = ty -litType (MachLabel _ _ ty) = ty -litType (BlankAddr) = Bottom -litType (AddrLit _) = Bottom -litType (SymLit var) = varType var -litType (SymLitEval pf args) = foldl AppTy (primFunType pf) (map litType args) - --- | Atom type. -atomType :: Atom -> Type -atomType (VarAtom var) = varType var -atomType (LitAtom lit) = litType lit - --- | Primitive function type. -primFunType :: PrimFun -> Type -primFunType (PrimFun _ ty) = ty - --- | Data constructor type denoted as a function. -dataConType :: DataCon -> Type -dataConType (DataCon _ ty tys) = foldr FunTy ty tys - --- | Alt type -altType :: Alt -> Type -altType (Alt _ _ expr) = exprType expr - --- | I wonder what this could possibly be? -exprType :: Expr -> Type -exprType (Atom atom) = atomType atom -exprType (PrimApp pf args) = foldl AppTy (primFunType pf) (map atomType args) -exprType (ConApp dc args) = foldl AppTy (dataConType dc) (map atomType args) -exprType (FunApp fun args) = foldl AppTy (varType fun) (map atomType args) -exprType (Let _ expr) = exprType expr -exprType (Case _ _ (a:_)) = altType a -exprType _ = Bottom - diff --git a/src/SSTG/Core/Syntax/Typing.hs b/src/SSTG/Core/Syntax/Typing.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Syntax/Typing.hs @@ -0,0 +1,53 @@ +-- | Typing Module +module SSTG.Core.Syntax.Typing + ( module SSTG.Core.Syntax.Typing + ) where + +import SSTG.Core.Syntax.Language + +-- | Variable type. +varType :: Var -> Type +varType (Var _ ty) = ty + +-- | Literal type. +litType :: Lit -> Type +litType (MachChar _ ty) = ty +litType (MachStr _ ty) = ty +litType (MachInt _ ty) = ty +litType (MachWord _ ty) = ty +litType (MachFloat _ ty) = ty +litType (MachDouble _ ty) = ty +litType (MachNullAddr ty) = ty +litType (MachLabel _ _ ty) = ty +litType (BlankAddr) = Bottom +litType (AddrLit _) = Bottom +litType (SymLit var) = varType var +litType (SymLitEval pf args) = foldl AppTy (primFunType pf) (map litType args) + +-- | Atom type. +atomType :: Atom -> Type +atomType (VarAtom var) = varType var +atomType (LitAtom lit) = litType lit + +-- | Primitive function type. +primFunType :: PrimFun -> Type +primFunType (PrimFun _ ty) = ty + +-- | Data constructor type denoted as a function. +dataConType :: DataCon -> Type +dataConType (DataCon _ ty tys) = foldr FunTy ty tys + +-- | Alt type +altType :: Alt -> Type +altType (Alt _ _ expr) = exprType expr + +-- | I wonder what this could possibly be? +exprType :: Expr -> Type +exprType (Atom atom) = atomType atom +exprType (PrimApp pf args) = foldl AppTy (primFunType pf) (map atomType args) +exprType (ConApp dc args) = foldl AppTy (dataConType dc) (map atomType args) +exprType (FunApp fun args) = foldl AppTy (varType fun) (map atomType args) +exprType (Let _ expr) = exprType expr +exprType (Case _ _ (a:_)) = altType a +exprType _ = Bottom + diff --git a/src/SSTG/Utils/FileIO.hs b/src/SSTG/Utils/FileIO.hs --- a/src/SSTG/Utils/FileIO.hs +++ b/src/SSTG/Utils/FileIO.hs @@ -5,8 +5,8 @@ , writePrettyState ) where -import SSTG.Core.Execution.Models import SSTG.Core.Execution.Stepping +import SSTG.Core.Execution.Support import SSTG.Utils.Printing import Text.Read