Lang.Crucible.Simulator.RegMap

Register maps hold the values of registers at simulation/run time.

Documentation

data RegEntry sym tp

The value of a register.

Constructors

RegEntry

Fields

• regType :: !(TypeRepr tp)
• regValue :: !(RegValue sym tp)

muxRegEntry :: IsSymInterface sym => sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegEntry sym tp)

Mux two register entries.

newtype RegMap sym (ctx :: Ctx CrucibleType)

A set of registers in an execution frame.

Constructors

RegMap

Fields

• regMap :: Assignment (RegEntry sym) ctx

regMapSize :: RegMap sym ctx -> Size ctx

emptyRegMap :: RegMap sym EmptyCtx

Create a new set of registers.

reg :: forall n sym ctx tp. Idx n ctx tp => RegMap sym ctx -> RegValue sym tp

regVal :: RegMap sym ctx -> Reg ctx tp -> RegValue sym tp

regVal' :: RegMap sym ctx -> Reg ctx tp -> RegEntry sym tp

assignReg :: TypeRepr tp -> RegValue sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp)

assignReg' :: RegEntry sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp)

appendRegs :: RegMap sym ctx -> RegMap sym ctx' -> RegMap sym (ctx <+> ctx')

takeRegs :: Size ctx -> Size ctx' -> RegMap sym (ctx <+> ctx') -> RegMap sym ctx

unconsReg :: RegMap sym (ctx ::> tp) -> (RegMap sym ctx, RegEntry sym tp)

muxRegForType :: forall sym tp. IsSymInterface sym => sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp

muxReference :: IsSymInterface sym => sym -> ValMuxFn sym (ReferenceType tp)

eqReference :: IsSymInterface sym => sym -> RegValue sym (ReferenceType tp) -> RegValue sym (ReferenceType tp) -> IO (Pred sym)

pushBranchForType :: forall sym tp. IsSymInterface sym => sym -> IntrinsicTypes sym -> TypeRepr tp -> RegValue sym tp -> IO (RegValue sym tp)

abortBranchForType :: forall sym tp. IsSymInterface sym => sym -> IntrinsicTypes sym -> TypeRepr tp -> RegValue sym tp -> IO (RegValue sym tp)

pushBranchRegs :: forall sym ctx. IsSymInterface sym => sym -> IntrinsicTypes sym -> RegMap sym ctx -> IO (RegMap sym ctx)

abortBranchRegs :: forall sym ctx. IsSymInterface sym => sym -> IntrinsicTypes sym -> RegMap sym ctx -> IO (RegMap sym ctx)

pushBranchRegEntry :: IsSymInterface sym => sym -> IntrinsicTypes sym -> RegEntry sym tp -> IO (RegEntry sym tp)

abortBranchRegEntry :: IsSymInterface sym => sym -> IntrinsicTypes sym -> RegEntry sym tp -> IO (RegEntry sym tp)

mergeRegs :: IsSymInterface sym => sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegMap sym ctx)

asSymExpr

Arguments

:: RegEntry sym tp

RegEntry to examine

-> (forall bt. tp ~ BaseToType bt => SymExpr sym bt -> a)

calculate final value when the register is a SymExpr

-> a

final value to use if the register entry is not a SymExpr

-> a

module Lang.Crucible.Simulator.RegValue