language-boogie-0.2: Interpreter and language infrastructure for Boogie.

Safe Haskell	None

Language.Boogie.Environment

Description

Execution state for the interpreter

Synopsis

Documentation

data MapRepr Source

Representation of a map value

Constructors

Source (Map [Value] Value)	Map that comes directly from a non-deterministic choice, possibly with some key-value pairs defined
Derived Ref (Map [Value] Value)	Map that is derived from another map by redefining values at some keys

Instances

Eq MapRepr
Ord MapRepr

emptyMap :: MapRepr Source

Representation of an empty map

stored :: MapRepr -> Map [Value] Value Source

Key-value pairs stored explicitly in a map representation

data Value Source

Run-time value

Constructors

IntValue Integer	Integer value
BoolValue Bool	Boolean value
CustomValue Id Int	Value of a user-defined type
MapValue MapRepr	Value of a map type: consists of an optional reference to the base map (if derived from base by updating) and key-value pairs that override base
Reference Ref	Reference to a map stored in the heap

Instances

Eq Value
Ord Value
Show Value

valueFromInteger :: Type -> Integer -> Value Source

valueFromInteger t n: value of type t with an integer code n

vnot :: Value -> Value Source

unValueBool :: Value -> Bool Source

unValueMap :: Value -> MapRepr Source

flattenMap :: Heap Value -> Ref -> (Ref, Map [Value] Value)Source

Source reference and key-value pairs of a reference in a heap

mapSource :: Heap Value -> Ref -> Ref Source

First component of flattenMap

mapValues :: Heap Value -> Ref -> Map [Value] Value Source

Second component of flattenMap

refIdTypeName :: [Char]Source

Dummy user-defined type used to differentiate map values

ucTypeName :: [Char]Source

Dummy user-defined type used to mark entities whose definitions are currently being evaluated

deepDeref :: Heap Value -> Value -> Value Source

deepDeref h v: Completely dereference value v given heap h (so that no references are left in v)

objectEq :: Heap Value -> Value -> Value -> Maybe Bool Source

objectEq h v1 v2: is v1 equal to v2 in the Boogie semantics? Nothing if cannot be determined.

mustAgree :: Ord k => Heap Value -> Map k Value -> Map k Value -> Bool Source

mustDisagree :: Ord k => Heap Value -> Map k Value -> Map k Value -> Bool Source

valueDoc :: Value -> Doc Source

Pretty-printed value

type Store = Map Id Value Source

Store: stores variable values at runtime

emptyStore :: Store Source

A store with no variables

functionConst :: [Char] -> [Char]Source

functionConst name : name of a map constant that corresponds function name (must be distinct from all global names)

userStore :: Heap Value -> Store -> Store Source

userStore heap store : store with all reference values completely dereferenced given heap, and all auxiliary values removed

storeDoc :: Store -> Doc Source

Pretty-printed store

data Memory Source

Memory: stores concrete values associated with names and references

Instances

Eq Memory
Show Memory

type StoreLens = SimpleLens Memory Store Source

Lens that selects a store from memory

memLocals :: Lens Memory Memory Store Store Source

memGlobals :: Lens Memory Memory Store Store Source

memOld :: Lens Memory Memory Store Store Source

memConstants :: Lens Memory Memory Store Store Source

memHeap :: Lens Memory Memory (Heap Value) (Heap Value)Source

emptyMemory :: Memory Source

Empty memory

visibleVariables :: Memory -> Store Source

Visible values of all identifiers in a memory (locals shadow globals)

memoryDoc :: Bool -> Memory -> Doc Source

memoryDoc debug mem : either user or debug representation of mem, depending on debug

data AbstractMemory Source

Abstract memory: stores constraints associated with names and references

amLocals :: Lens AbstractMemory AbstractMemory AbstractStore AbstractStore Source

amGlobals :: Lens AbstractMemory AbstractMemory AbstractStore AbstractStore Source

amHeap :: Lens AbstractMemory AbstractMemory (Map Ref ConstraintSet) (Map Ref ConstraintSet)Source

data Environment m Source

Execution state

envMemory :: forall m. Lens (Environment m) (Environment m) Memory Memory Source

envProcedures :: forall m. Lens (Environment m) (Environment m) (Map Id [PDef]) (Map Id [PDef])Source

envConstraints :: forall m. Lens (Environment m) (Environment m) AbstractMemory AbstractMemory Source

envTypeContext :: forall m. Lens (Environment m) (Environment m) Context Context Source

envGenerator :: forall m m. Lens (Environment m) (Environment m) (Generator m) (Generator m)Source

envCustomCount :: forall m. Lens (Environment m) (Environment m) (Map Id Int) (Map Id Int)Source

envQBound :: forall m. Lens (Environment m) (Environment m) (Maybe Integer) (Maybe Integer)Source

envInOld :: forall m. Lens (Environment m) (Environment m) Bool Bool Source

initEnv :: Context -> Generator m -> Maybe Integer -> Environment mSource

initEnv tc gen: Initial environment in a type context tc with a value generator gen

lookupProcedure :: Id -> Environment m -> [PDef]Source

lookupNameConstraints :: Id -> Environment m -> ConstraintSet Source

lookupMapConstraints :: Ref -> Environment m -> ConstraintSet Source

lookupCustomCount :: Id -> Environment m -> Int Source

addProcedureImpl :: Id -> PDef -> Environment m -> Environment mSource

addGlobalDefinition :: Id -> FDef -> Environment m -> Environment mSource

addMapDefinition :: Ref -> FDef -> Environment m -> Environment mSource

addMapConstraint :: Ref -> FDef -> Environment m -> Environment mSource

setCustomCount :: Id -> Int -> Environment m -> Environment mSource

withHeap :: (Heap Value -> (t, Heap Value)) -> Environment m -> (t, Environment m)Source