Safe Haskell	Safe
Language	Haskell2010

SSTG.Core.Execution.Models

Description

Symbolic STG Execution Models

Synopsis

Documentation

newtype SymbolicT s a Source #

Symbolic Transformation represents transformations applied to some State`(s). This is useful in allowing us to transfer from different actions within the engine.

Constructors

SymbolicT
Fields run :: s -> (s, a)

Instances

Monad (SymbolicT s) Source #	Monad instance of Symbolic Transformation.
Methods (>>=) :: SymbolicT s a -> (a -> SymbolicT s b) -> SymbolicT s b # (>>) :: SymbolicT s a -> SymbolicT s b -> SymbolicT s b # return :: a -> SymbolicT s a # fail :: String -> SymbolicT s a #
Functor (SymbolicT s) Source #	Functor instance of Symbolic Transformation.
Methods fmap :: (a -> b) -> SymbolicT s a -> SymbolicT s b # (<$) :: a -> SymbolicT s b -> SymbolicT s a #
Applicative (SymbolicT s) Source #	Applicative instance of Symbolic Transformation.
Methods pure :: a -> SymbolicT s a # (<>) :: SymbolicT s (a -> b) -> SymbolicT s a -> SymbolicT s b # (>) :: SymbolicT s a -> SymbolicT s b -> SymbolicT s b # (<*) :: SymbolicT s a -> SymbolicT s b -> SymbolicT s a #

data State Source #

State contains the information necessary to perform symbolic execution. Eval/Apply graph reduction semantics are used.

Constructors

State
Fields state_status :: Status state_stack :: Stack state_heap :: Heap state_globals :: Globals state_code :: Code state_names :: [Name] state_paths :: PathCons state_links :: SymLinks

Instances

Eq State Source #
Methods (==) :: State -> State -> Bool # (/=) :: State -> State -> Bool #
Read State Source #
Methods readsPrec :: Int -> ReadS State # readList :: ReadS [State] # readPrec :: ReadPrec State # readListPrec :: ReadPrec [State] #
Show State Source #
Methods showsPrec :: Int -> State -> ShowS # show :: State -> String # showList :: [State] -> ShowS #

data Symbol Source #

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.

Constructors

Symbol Var (Maybe (Expr, Locals))

Instances

Eq Symbol Source #
Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
Read Symbol Source #
Methods readsPrec :: Int -> ReadS Symbol # readList :: ReadS [Symbol] # readPrec :: ReadPrec Symbol # readListPrec :: ReadPrec [Symbol] #
Show Symbol Source #
Methods showsPrec :: Int -> Symbol -> ShowS # show :: Symbol -> String # showList :: [Symbol] -> ShowS #

data Status Source #

State status.

Constructors

Status
Fields steps :: Int

Instances

Eq Status Source #
Methods (==) :: Status -> Status -> Bool # (/=) :: Status -> Status -> Bool #
Read Status Source #
Methods readsPrec :: Int -> ReadS Status # readList :: ReadS [Status] # readPrec :: ReadPrec Status # readListPrec :: ReadPrec [Status] #
Show Status Source #
Methods showsPrec :: Int -> Status -> ShowS # show :: Status -> String # showList :: [Status] -> ShowS #

newtype Stack Source #

Execution stack used in graph reduction semnatics.

Constructors

Stack [Frame]

Instances

Eq Stack Source #
Methods (==) :: Stack -> Stack -> Bool # (/=) :: Stack -> Stack -> Bool #
Read Stack Source #
Methods readsPrec :: Int -> ReadS Stack # readList :: ReadS [Stack] # readPrec :: ReadPrec Stack # readListPrec :: ReadPrec [Stack] #
Show Stack Source #
Methods showsPrec :: Int -> Stack -> ShowS # show :: Stack -> String # showList :: [Stack] -> ShowS #

data Frame Source #

Frames of a stack.

Constructors

CaseFrame Var [Alt] Locals
ApplyFrame [Atom] Locals
UpdateFrame MemAddr

Instances

Eq Frame Source #
Methods (==) :: Frame -> Frame -> Bool # (/=) :: Frame -> Frame -> Bool #
Read Frame Source #
Methods readsPrec :: Int -> ReadS Frame # readList :: ReadS [Frame] # readPrec :: ReadPrec Frame # readListPrec :: ReadPrec [Frame] #
Show Frame Source #
Methods showsPrec :: Int -> Frame -> ShowS # show :: Frame -> String # showList :: [Frame] -> ShowS #

newtype MemAddr Source #

Memory address for things on the Heap.

Constructors

MemAddr Int

Instances

Eq MemAddr Source #
Methods (==) :: MemAddr -> MemAddr -> Bool # (/=) :: MemAddr -> MemAddr -> Bool #
Ord MemAddr Source #
Methods compare :: MemAddr -> MemAddr -> Ordering # (<) :: MemAddr -> MemAddr -> Bool # (<=) :: MemAddr -> MemAddr -> Bool # (>) :: MemAddr -> MemAddr -> Bool # (>=) :: MemAddr -> MemAddr -> Bool # max :: MemAddr -> MemAddr -> MemAddr # min :: MemAddr -> MemAddr -> MemAddr #
Read MemAddr Source #
Methods readsPrec :: Int -> ReadS MemAddr # readList :: ReadS [MemAddr] # readPrec :: ReadPrec MemAddr # readListPrec :: ReadPrec [MemAddr] #
Show MemAddr Source #
Methods showsPrec :: Int -> MemAddr -> ShowS # show :: MemAddr -> String # showList :: [MemAddr] -> ShowS #

data Value Source #

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.

Constructors

LitVal Lit
MemVal MemAddr

Instances

Eq Value Source #
Methods (==) :: Value -> Value -> Bool # (/=) :: Value -> Value -> Bool #
Read Value Source #
Methods readsPrec :: Int -> ReadS Value # readList :: ReadS [Value] # readPrec :: ReadPrec Value # readListPrec :: ReadPrec [Value] #
Show Value Source #
Methods showsPrec :: Int -> Value -> ShowS # show :: Value -> String # showList :: [Value] -> ShowS #

newtype Locals Source #

Locals binds a Var's Name to its some Value.

Constructors

Locals (Map Name Value)

Instances

Eq Locals Source #
Methods (==) :: Locals -> Locals -> Bool # (/=) :: Locals -> Locals -> Bool #
Read Locals Source #
Methods readsPrec :: Int -> ReadS Locals # readList :: ReadS [Locals] # readPrec :: ReadPrec Locals # readListPrec :: ReadPrec [Locals] #
Show Locals Source #
Methods showsPrec :: Int -> Locals -> ShowS # show :: Locals -> String # showList :: [Locals] -> ShowS #

data Heap Source #

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.

Constructors

Heap (Map MemAddr HeapObj) MemAddr

Instances

Eq Heap Source #
Methods (==) :: Heap -> Heap -> Bool # (/=) :: Heap -> Heap -> Bool #
Read Heap Source #
Methods readsPrec :: Int -> ReadS Heap # readList :: ReadS [Heap] # readPrec :: ReadPrec Heap # readListPrec :: ReadPrec [Heap] #
Show Heap Source #
Methods showsPrec :: Int -> Heap -> ShowS # show :: Heap -> String # showList :: [Heap] -> ShowS #

data HeapObj Source #

Heap objects.

Constructors

LitObj Lit
SymObj Symbol
ConObj DataCon [Value]
FunObj [Var] Expr Locals
Blackhole

Instances

Eq HeapObj Source #
Methods (==) :: HeapObj -> HeapObj -> Bool # (/=) :: HeapObj -> HeapObj -> Bool #
Read HeapObj Source #
Methods readsPrec :: Int -> ReadS HeapObj # readList :: ReadS [HeapObj] # readPrec :: ReadPrec HeapObj # readListPrec :: ReadPrec [HeapObj] #
Show HeapObj Source #
Methods showsPrec :: Int -> HeapObj -> ShowS # show :: HeapObj -> String # showList :: [HeapObj] -> ShowS #

newtype Globals Source #

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.

Constructors

Globals (Map Name Value)

Instances

Eq Globals Source #
Methods (==) :: Globals -> Globals -> Bool # (/=) :: Globals -> Globals -> Bool #
Read Globals Source #
Methods readsPrec :: Int -> ReadS Globals # readList :: ReadS [Globals] # readPrec :: ReadPrec Globals # readListPrec :: ReadPrec [Globals] #
Show Globals Source #
Methods showsPrec :: Int -> Globals -> ShowS # show :: Globals -> String # showList :: [Globals] -> ShowS #

data Code Source #

Evaluation of the current expression. We are either evaluating, or ready to return with some Value.

Constructors

Evaluate Expr Locals
Return Value

Instances

Eq Code Source #
Methods (==) :: Code -> Code -> Bool # (/=) :: Code -> Code -> Bool #
Read Code Source #
Methods readsPrec :: Int -> ReadS Code # readList :: ReadS [Code] # readPrec :: ReadPrec Code # readListPrec :: ReadPrec [Code] #
Show Code Source #
Methods showsPrec :: Int -> Code -> ShowS # show :: Code -> String # showList :: [Code] -> ShowS #

type PathCons = [PathCond] Source #

Path constraints.

data PathCond Source #

Path conditions denote logical paths taken in program execution thus far.

Constructors

PathCond (AltCon, [Var]) Expr Locals Bool

Instances

Eq PathCond Source #
Methods (==) :: PathCond -> PathCond -> Bool # (/=) :: PathCond -> PathCond -> Bool #
Read PathCond Source #
Methods readsPrec :: Int -> ReadS PathCond # readList :: ReadS [PathCond] # readPrec :: ReadPrec PathCond # readListPrec :: ReadPrec [PathCond] #
Show PathCond Source #
Methods showsPrec :: Int -> PathCond -> ShowS # show :: PathCond -> String # showList :: [PathCond] -> ShowS #

newtype SymLinks Source #

Symbolic link tables helps keep track of what names went to what, what?

Constructors

SymLinks (Map Name Name)

Instances

Eq SymLinks Source #
Methods (==) :: SymLinks -> SymLinks -> Bool # (/=) :: SymLinks -> SymLinks -> Bool #
Read SymLinks Source #
Methods readsPrec :: Int -> ReadS SymLinks # readList :: ReadS [SymLinks] # readPrec :: ReadPrec SymLinks # readListPrec :: ReadPrec [SymLinks] #
Show SymLinks Source #
Methods showsPrec :: Int -> SymLinks -> ShowS # show :: SymLinks -> String # showList :: [SymLinks] -> ShowS #

nameOccStr :: Name -> String Source #

A Name's occurrence string.

nameUnique :: Name -> Int Source #

Name's unique Int key.

varName :: Var -> Name Source #

Variable name.

memAddrInt :: MemAddr -> Int Source #

MemAddr's Int value.

lookupLocals :: Var -> Locals -> Maybe Value Source #

Locals lookup.

insertLocals :: Var -> Value -> Locals -> Locals Source #

Locals insertion.

insertLocalsList :: [(Var, Value)] -> Locals -> Locals Source #

List insertion into Locals.

lookupHeap :: MemAddr -> Heap -> Maybe HeapObj Source #

Heap lookup.

allocHeap :: HeapObj -> Heap -> (Heap, MemAddr) Source #

Heap allocation. Updates the last MemAddr kept in the Heap.

allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr]) Source #

Allocate a list of HeapObj in a Heap, returning in the same order the MemAddr at which they have been allocated at.

insertHeap :: MemAddr -> HeapObj -> Heap -> Heap Source #

Heap direct insertion at a specific MemAddr.

insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap Source #

Insert a list of HeapObj at specified MemAddr locations.

lookupGlobals :: Var -> Globals -> Maybe Value Source #

Globals lookup.

insertGlobals :: Var -> Value -> Globals -> Globals Source #

Globals insertion.

insertGlobalsList :: [(Var, Value)] -> Globals -> Globals Source #

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.

lookupValue :: Var -> Locals -> Globals -> Maybe Value Source #

Value lookup from the Locals first, then Globals.

vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj) Source #

Heap lookup. Returns the corresponding MemAddr and HeapObj if found.

memAddrType :: MemAddr -> Heap -> Maybe Type Source #

Type of HeapObj held at MemAddr, if found.