Lang.Crucible.Simulator.GlobalState

Documentation

data SymGlobalState (sym :: Type)

A map from global variables to their value.

emptyGlobals :: SymGlobalState sym

The empty set of global variable bindings.

newtype GlobalEntry (sym :: Type) (tp :: CrucibleType)

As a map element, type GlobalEntry sym tp models the contents of a GlobalVar, which is always defined.

Constructors

GlobalEntry

Fields

• globalEntryValue :: RegValue sym tp

insertGlobal :: GlobalVar tp -> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym

Set the value of a global in the state, or create a new global variable.

lookupGlobal :: GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)

Lookup a global variable in the state.

insertRef :: IsExprBuilder sym => sym -> RefCell tp -> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym

Set the value of a reference cell in the state.

lookupRef :: RefCell tp -> SymGlobalState sym -> PartExpr (Pred sym) (RegValue sym tp)

Look up the value of a reference cell in the state.

dropRef :: RefCell tp -> SymGlobalState sym -> SymGlobalState sym

Reset a reference cell to the uninitialized state. dropRef r is equivalent to updateRef r Unassigned.

updateRef :: RefCell tp -> PartExpr (Pred sym) (RegValue sym tp) -> SymGlobalState sym -> SymGlobalState sym

Write a partial value to a reference cell in the state.

globalPushBranch :: forall sym. IsSymInterface sym => sym -> IntrinsicTypes sym -> SymGlobalState sym -> IO (SymGlobalState sym)

Mark a branch point in the global state. Later calls to globalMuxFn will assume that the input states are identical up until the most recent branch point.

globalAbortBranch :: forall sym. IsSymInterface sym => sym -> IntrinsicTypes sym -> SymGlobalState sym -> IO (SymGlobalState sym)

Remove the most recent branch point marker, and thus cancel the effect of the most recent globalPushBranch.

globalMuxFn :: forall sym. IsSymInterface sym => sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (SymGlobalState sym)

Compute a symbolic if-then-else on two global states. The function assumes that the two states were identical up until the most recent branch point marked by globalPushBranch. This most recent branch point marker is also popped from the stack.