Copyright	(c) Galois Inc 2014
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Stability	provisional
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Simulator.RegMap

Description

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

Synopsis

data RegEntry sym tp = RegEntry {
- regType :: !(TypeRepr tp)
- regValue :: !(RegValue sym tp)
}
muxRegEntry :: IsSymInterface sym => sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegEntry sym tp)
newtype RegMap sym (ctx :: Ctx CrucibleType) = RegMap {
- regMap :: Assignment (RegEntry sym) ctx
}
regMapSize :: RegMap sym ctx -> Size ctx
emptyRegMap :: RegMap sym EmptyCtx
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 :: RegEntry sym tp -> (forall bt. tp ~ BaseToType bt => SymExpr sym bt -> a) -> a -> a
module Lang.Crucible.Simulator.RegValue

Documentation

data RegEntry sym tp Source #

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) Source #

Mux two register entries.

newtype RegMap sym (ctx :: Ctx CrucibleType) Source #

A set of registers in an execution frame.

Constructors

RegMap
Fields regMap :: Assignment (RegEntry sym) ctx

regMapSize :: RegMap sym ctx -> Size ctx Source #

emptyRegMap :: RegMap sym EmptyCtx Source #

Create a new set of registers.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

asSymExpr Source #

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