Safe Haskell	Safe
Language	Haskell2010

SSTG.Core.Language.Support

Description

Symbolic STG Execution Support Architecture

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 #

fmap :: Functor f => forall a b. (a -> b) -> f a -> f b #

pure :: Applicative f => forall a. a -> f a #

Lift a value.

(<*>) :: Applicative f => forall a b. f (a -> b) -> f a -> f b #

Sequential application.

return :: Monad m => forall a. a -> m a #

Inject a value into the monadic type.

(>>=) :: Monad m => forall a b. m a -> (a -> m b) -> m b #

Sequentially compose two actions, passing any value produced by the first as an argument to the second.

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

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 status_id :: !Int status_parent :: !Int status_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 #

data Stack Source #

Execution stack used in graph reduction semnatics.

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 #

data MemAddr Source #

Memory address for things on the Heap.

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 #

data Locals Source #

Locals binds a Var's Name to its some 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.

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
AddrObj MemAddr
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 #

data 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.

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 #

data PathCons Source #

Path constraints are the conjunctive normal form of Constraints.

Instances

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

data Constraint Source #

Constraints denote logical paths taken in program execution thus far.

Constructors

Constraint (AltCon, [Var]) Expr Locals Bool

Instances

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

nameOccStr :: Name -> String Source #

A Name's occurrence string.

nameUnique :: Name -> Int Source #

Name imique Int.

varName :: Var -> Name Source #

Variable name.

null_addr :: MemAddr Source #

Null MemAddr.

addrInt :: MemAddr -> Int Source #

MemAddr's Int value.

init_status :: Status Source #

Initial Status.

incStatusSteps :: Status -> Status Source #

Increment Status steps.

updateStatusId :: Int -> Status -> Status Source #

Update the Status id.

empty_stack :: Stack Source #

Empty `Stack.

popStack :: Stack -> Maybe (Frame, Stack) Source #

Stack pop.

pushStack :: Frame -> Stack -> Stack Source #

Stack push.

stackToList :: Stack -> [Frame] Source #

Stack as list of Frames.

empty_locals :: Locals Source #

Empty Locals.

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.

localsToList :: Locals -> [(Name, Value)] Source #

Locals to key value pairs.

empty_heap :: Heap Source #

Empty Heap.

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.

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

Heap to key value pairs.

empty_globals :: Globals Source #

Empty Globals.

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.

globalsToList :: Globals -> [(Name, Value)] Source #

Globals to key value pairs.

empty_pathcons :: PathCons Source #

Empty PathCons.

insertPathCons :: Constraint -> PathCons -> PathCons Source #

PathCons insertion.

insertPathConsList :: [Constraint] -> PathCons -> PathCons Source #

Insert a list of Constraints into a PathCons.

pathconsToList :: PathCons -> [Constraint] Source #

PathCons to list of Constraints.

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.