Lang.Crucible.Simulator.RegValue

RegValue is a type family that defines the runtime representation of crucible types.

Documentation

type family RegValue (sym :: Type) (tp :: CrucibleType) :: Type where ...

Maps register types to the runtime representation.

Equations

RegValue sym (BaseToType bt) = SymExpr sym bt

RegValue sym (FloatType fi) = SymInterpretedFloat sym fi

RegValue sym AnyType = AnyValue sym

RegValue sym UnitType = ()

RegValue sym NatType = SymNat sym

RegValue sym CharType = Word16

RegValue sym (FunctionHandleType a r) = FnVal sym a r

RegValue sym (MaybeType tp) = PartExpr (Pred sym) (RegValue sym tp)

RegValue sym (VectorType tp) = Vector (RegValue sym tp)

RegValue sym (SequenceType tp) = SymSequence sym (RegValue sym tp)

RegValue sym (StructType ctx) = Assignment (RegValue' sym) ctx

RegValue sym (VariantType ctx) = Assignment (VariantBranch sym) ctx

RegValue sym (ReferenceType tp) = MuxTree sym (RefCell tp)

RegValue sym (WordMapType w tp) = WordMap sym w tp

RegValue sym (RecursiveType nm ctx) = RolledType sym nm ctx

RegValue sym (IntrinsicType nm ctx) = Intrinsic sym nm ctx

RegValue sym (StringMapType tp) = Map Text (PartExpr (Pred sym) (RegValue sym tp))

class CanMux sym (tp :: CrucibleType) where

A class for CrucibleTypes that have a mux function.

Methods

muxReg

Arguments

:: sym

-> p tp

Unused type to identify what is being merged.

-> ValMuxFn sym tp

Instances

IsExprBuilder sym => CanMux sym BoolType

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p BoolType -> ValMuxFn sym BoolType

IsSymInterface sym => CanMux sym CharType

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p CharType -> ValMuxFn sym CharType

IsExprBuilder sym => CanMux sym ComplexRealType

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p ComplexRealType -> ValMuxFn sym ComplexRealType

IsExprBuilder sym => CanMux sym IntegerType

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p IntegerType -> ValMuxFn sym IntegerType

IsExprBuilder sym => CanMux sym NatType

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p NatType -> ValMuxFn sym NatType

IsExprBuilder sym => CanMux sym RealValType

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p RealValType -> ValMuxFn sym RealValType

CanMux sym UnitType

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p UnitType -> ValMuxFn sym UnitType

IsInterpretedFloatExprBuilder sym => CanMux sym (FloatType fi)

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p (FloatType fi) -> ValMuxFn sym (FloatType fi)

IsExprBuilder sym => CanMux sym (IEEEFloatType fpp)

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p (IEEEFloatType fpp) -> ValMuxFn sym (IEEEFloatType fpp)

(IsExprBuilder sym, CanMux sym tp) => CanMux sym (MaybeType tp)

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p (MaybeType tp) -> ValMuxFn sym (MaybeType tp)

IsExprBuilder sym => CanMux sym (StringType si)

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p (StringType si) -> ValMuxFn sym (StringType si)

(IsSymInterface sym, CanMux sym tp) => CanMux sym (VectorType tp)

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p (VectorType tp) -> ValMuxFn sym (VectorType tp)

IsExprBuilder sym => CanMux sym (FunctionHandleType a r)

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p (FunctionHandleType a r) -> ValMuxFn sym (FunctionHandleType a r)

(IsExprBuilder sym, KnownNat w, KnownRepr BaseTypeRepr tp) => CanMux sym (WordMapType w tp)

Defined in Lang.Crucible.Simulator.RegValue

Methods

muxReg :: sym -> p (WordMapType w tp) -> ValMuxFn sym (WordMapType w tp)

newtype RegValue' sym tp

A newtype wrapper around RegValue. This is wrapper necessary because RegValue is a type family and, as such, cannot be partially applied.

Constructors

RV

Fields

• unRV :: RegValue sym tp

type MuxFn p v = p -> v -> v -> IO v

Register values

data AnyValue sym where

Constructors

AnyValue :: TypeRepr tp -> RegValue sym tp -> AnyValue sym

data FnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where

Represents a function closure.

Constructors

ClosureFnVal :: !(FnVal sym (args ::> tp) ret) -> !(TypeRepr tp) -> !(RegValue sym tp) -> FnVal sym args ret

VarargsFnVal :: !(FnHandle (args ::> VectorType AnyType) ret) -> !(CtxRepr addlArgs) -> FnVal sym (args <+> addlArgs) ret

HandleFnVal :: !(FnHandle a r) -> FnVal sym a r

Instances

Show (FnVal sym a r)

Defined in Lang.Crucible.Simulator.RegValue

Methods

showsPrec :: Int -> FnVal sym a r -> ShowS

show :: FnVal sym a r -> String

showList :: [FnVal sym a r] -> ShowS

fnValType :: FnVal sym args res -> TypeRepr (FunctionHandleType args res)

Extract the runtime representation of the type of the given FnVal

newtype RolledType sym nm ctx

Constructors

RolledType

Fields

• unroll :: RegValue sym (UnrollType nm ctx)

data SymSequence sym a where

A symbolic sequence of values supporting efficent merge operations. Semantically, these are essentially cons-lists, and designed to support access from the front only. Nodes carry nonce values that allow DAG-based traversal, which efficently supports the common case where merged nodes share a common sublist.

Constructors

SymSequenceNil :: SymSequence sym a

SymSequenceCons :: !(Nonce GlobalNonceGenerator a) -> a -> !(SymSequence sym a) -> SymSequence sym a

SymSequenceAppend :: !(Nonce GlobalNonceGenerator a) -> !(SymSequence sym a) -> !(SymSequence sym a) -> SymSequence sym a

SymSequenceMerge :: !(Nonce GlobalNonceGenerator a) -> !(Pred sym) -> !(SymSequence sym a) -> !(SymSequence sym a) -> SymSequence sym a

Instances

Eq (SymSequence sym a)

Defined in Lang.Crucible.Simulator.SymSequence

Methods

(==) :: SymSequence sym a -> SymSequence sym a -> Bool

(/=) :: SymSequence sym a -> SymSequence sym a -> Bool

(IsExpr (SymExpr sym), Pretty a) => Pretty (SymSequence sym a)

Defined in Lang.Crucible.Simulator.SymSequence

Methods

pretty :: SymSequence sym a -> Doc ann

prettyList :: [SymSequence sym a] -> Doc ann

newtype VariantBranch sym tp

Constructors

VB

Fields

• unVB :: PartExpr (Pred sym) (RegValue sym tp)

injectVariant

Arguments

:: IsExprBuilder sym

=> sym

symbolic backend

-> CtxRepr ctx

Types of the variant branches

-> Index ctx tp

Which branch

-> RegValue sym tp

The value to inject

-> RegValue sym (VariantType ctx)

Construct a VariantType value by identifying which branch of the variant to construct, and providing a value of the correct type.

Value mux functions

type ValMuxFn sym tp = MuxFn (Pred sym) (RegValue sym tp)

Version of MuxFn specialized to RegValue

eqMergeFn :: (IsExprBuilder sym, Eq v) => sym -> String -> MuxFn p v

Merge function that checks if two values are equal, and fails if they are not.

mergePartExpr :: IsExprBuilder sym => sym -> (Pred sym -> v -> v -> IO v) -> Pred sym -> PartExpr (Pred sym) v -> PartExpr (Pred sym) v -> IO (PartExpr (Pred sym) v)

muxRecursive :: IsRecursiveType nm => (forall tp. TypeRepr tp -> ValMuxFn sym tp) -> SymbolRepr nm -> CtxRepr ctx -> ValMuxFn sym (RecursiveType nm ctx)

muxStringMap :: IsExprBuilder sym => sym -> MuxFn (Pred sym) e -> MuxFn (Pred sym) (Map Text (PartExpr (Pred sym) e))

Merge to string maps together.

muxStruct :: (forall tp. TypeRepr tp -> ValMuxFn sym tp) -> CtxRepr ctx -> ValMuxFn sym (StructType ctx)

muxVariant :: IsExprBuilder sym => sym -> (forall tp. TypeRepr tp -> ValMuxFn sym tp) -> CtxRepr ctx -> ValMuxFn sym (VariantType ctx)

muxVector :: IsExprBuilder sym => sym -> MuxFn p e -> MuxFn p (Vector e)

muxSymSequence :: sym -> Pred sym -> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)

Compute an ifthenelse on symbolic sequences. This will simply produce an internal merge node except in the special case where the then and else branches are sytactically identical.

muxHandle :: IsExpr (SymExpr sym) => sym -> Pred sym -> FnVal sym a r -> FnVal sym a r -> IO (FnVal sym a r)