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

Lang.Crucible.Simulator.RegMap

Description

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

Synopsis

data RegEntry sym (tp :: CrucibleType) = RegEntry {
- regType :: !(TypeRepr tp)
- regValue :: !(RegValue sym tp)
}
muxRegEntry :: forall sym (tp :: CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegEntry sym tp)
newtype RegMap sym (ctx :: Ctx CrucibleType) = RegMap {
- regMap :: Assignment (RegEntry sym) ctx
}
regMapSize :: forall sym (ctx :: Ctx CrucibleType). RegMap sym ctx -> Size ctx
emptyRegMap :: RegMap sym (EmptyCtx :: Ctx CrucibleType)
reg :: forall (n :: Nat) sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType). Idx n ctx tp => RegMap sym ctx -> RegValue sym tp
regVal :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType). RegMap sym ctx -> Reg ctx tp -> RegValue sym tp
regVal' :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType). RegMap sym ctx -> Reg ctx tp -> RegEntry sym tp
assignReg :: forall (tp :: CrucibleType) sym (ctx :: Ctx CrucibleType). TypeRepr tp -> RegValue sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp)
assignReg' :: forall sym (tp :: CrucibleType) (ctx :: Ctx CrucibleType). RegEntry sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp)
appendRegs :: forall sym (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType). RegMap sym ctx -> RegMap sym ctx' -> RegMap sym (ctx <+> ctx')
takeRegs :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) sym. Size ctx -> Size ctx' -> RegMap sym (ctx <+> ctx') -> RegMap sym ctx
unconsReg :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType). RegMap sym (ctx ::> tp) -> (RegMap sym ctx, RegEntry sym tp)
muxRegForType :: forall sym (tp :: CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxReference :: forall sym (tp :: CrucibleType). IsSymInterface sym => sym -> ValMuxFn sym (ReferenceType tp)
eqReference :: forall sym (tp :: CrucibleType). IsSymInterface sym => sym -> RegValue sym (ReferenceType tp) -> RegValue sym (ReferenceType tp) -> IO (Pred sym)
pushBranchForType :: forall sym (tp :: CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> TypeRepr tp -> RegValue sym tp -> IO (RegValue sym tp)
abortBranchForType :: forall sym (tp :: CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> TypeRepr tp -> RegValue sym tp -> IO (RegValue sym tp)
pushBranchRegs :: forall sym (ctx :: Ctx CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> RegMap sym ctx -> IO (RegMap sym ctx)
abortBranchRegs :: forall sym (ctx :: Ctx CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> RegMap sym ctx -> IO (RegMap sym ctx)
pushBranchRegEntry :: forall sym (tp :: CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> RegEntry sym tp -> IO (RegEntry sym tp)
abortBranchRegEntry :: forall sym (tp :: CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> RegEntry sym tp -> IO (RegEntry sym tp)
mergeRegs :: forall sym (ctx :: Ctx CrucibleType). IsSymInterface sym => sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegMap sym ctx)
asSymExpr :: forall sym (tp :: CrucibleType) a. RegEntry sym tp -> (forall (bt :: BaseType). tp ~ BaseToType bt => SymExpr sym bt -> a) -> a -> a
module Lang.Crucible.Simulator.RegValue

Documentation

data RegEntry sym (tp :: CrucibleType) Source #

The value of a register.

Constructors

RegEntry
Fields regType :: !(TypeRepr tp) regValue :: !(RegValue sym tp)

muxRegEntry :: forall sym (tp :: CrucibleType). 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 :: forall sym (ctx :: Ctx CrucibleType). RegMap sym ctx -> Size ctx Source #

emptyRegMap :: RegMap sym (EmptyCtx :: Ctx CrucibleType) Source #

Create a new set of registers.

reg :: forall (n :: Nat) sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType). Idx n ctx tp => RegMap sym ctx -> RegValue sym tp Source #

regVal :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType). RegMap sym ctx -> Reg ctx tp -> RegValue sym tp Source #

regVal' :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType). RegMap sym ctx -> Reg ctx tp -> RegEntry sym tp Source #

assignReg :: forall (tp :: CrucibleType) sym (ctx :: Ctx CrucibleType). TypeRepr tp -> RegValue sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp) Source #

assignReg' :: forall sym (tp :: CrucibleType) (ctx :: Ctx CrucibleType). RegEntry sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp) Source #

appendRegs :: forall sym (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType). RegMap sym ctx -> RegMap sym ctx' -> RegMap sym (ctx <+> ctx') Source #

takeRegs :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) sym. Size ctx -> Size ctx' -> RegMap sym (ctx <+> ctx') -> RegMap sym ctx Source #

unconsReg :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType). RegMap sym (ctx ::> tp) -> (RegMap sym ctx, RegEntry sym tp) Source #

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

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

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

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

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

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

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

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

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

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

asSymExpr Source #

Arguments

:: forall sym (tp :: CrucibleType) a. RegEntry sym tp	RegEntry to examine
-> (forall (bt :: BaseType). 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