| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
SSTG.Core.Execution.Models
Description
Symbolic STG Execution Models
- newtype SymbolicT s a = SymbolicT {
- run :: s -> (s, a)
- 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
- data Symbol = Symbol Var (Maybe (Expr, Locals))
- data Status = Status {}
- newtype Stack = Stack [Frame]
- data Frame
- = CaseFrame Var [Alt] Locals
- | ApplyFrame [Atom] Locals
- | UpdateFrame MemAddr
- newtype MemAddr = MemAddr Int
- data Value
- newtype Locals = Locals (Map Name Value)
- data Heap = Heap (Map MemAddr HeapObj) MemAddr
- data HeapObj
- newtype Globals = Globals (Map Name Value)
- data Code
- type PathCons = [PathCond]
- data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool
- newtype SymLinks = SymLinks (Map Name Name)
- nameOccStr :: Name -> String
- nameUnique :: Name -> Int
- varName :: Var -> Name
- memAddrInt :: MemAddr -> Int
- lookupLocals :: Var -> Locals -> Maybe Value
- insertLocals :: Var -> Value -> Locals -> Locals
- insertLocalsList :: [(Var, Value)] -> Locals -> Locals
- lookupHeap :: MemAddr -> Heap -> Maybe HeapObj
- allocHeap :: HeapObj -> Heap -> (Heap, MemAddr)
- allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr])
- insertHeap :: MemAddr -> HeapObj -> Heap -> Heap
- insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap
- lookupGlobals :: Var -> Globals -> Maybe Value
- insertGlobals :: Var -> Value -> Globals -> Globals
- insertGlobalsList :: [(Var, Value)] -> Globals -> Globals
- lookupValue :: Var -> Locals -> Globals -> Maybe Value
- vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj)
- memAddrType :: MemAddr -> Heap -> Maybe Type
Documentation
newtype SymbolicT s a Source #
Symbolic Transformation We supply some state(s), it gives back those state(s) and some result.
Instances
| Monad (SymbolicT s) Source # | Monad instance of Symbolic Transformation Used for transitioning between different types of state manipulations. |
| Functor (SymbolicT s) Source # | Functor instance of Symbolic Transformation Apply transformations on the result. |
| Applicative (SymbolicT s) Source # | Applicative instance of Symbolic Transformation Can be used to chain together step-wise execution. |
State
Constructors
| State | |
Fields
| |
Symbolic
Status
Stack
Stack Frame
Constructors
| CaseFrame Var [Alt] Locals | |
| ApplyFrame [Atom] Locals | |
| UpdateFrame MemAddr |
Memory Address
Value
Locals
Heap
Heap Object
Globals
Evaluation State
Path Condition
Symbolic Link Table
nameOccStr :: Name -> String Source #
Name Occ String
nameUnique :: Name -> Int Source #
Name Unique
memAddrInt :: MemAddr -> Int Source #
Mem Addr Int