| Copyright | (c) Galois Inc 2014 |
|---|---|
| License | BSD3 |
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Stability | provisional |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.Simulator.RegValue
Description
RegValue is a type family that defines the runtime representation of crucible types.
Synopsis
- type family RegValue (sym :: Type) (tp :: CrucibleType) :: Type where ...
- class CanMux sym (tp :: CrucibleType) where
- newtype RegValue' sym tp = RV {}
- type MuxFn p v = p -> v -> v -> IO v
- data AnyValue sym where
- data FnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where
- 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
- fnValType :: FnVal sym args res -> TypeRepr (FunctionHandleType args res)
- newtype RolledType sym nm ctx = RolledType {
- unroll :: RegValue sym (UnrollType nm ctx)
- data SymSequence sym a where
- 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
- newtype VariantBranch sym tp = VB {}
- injectVariant :: IsExprBuilder sym => sym -> CtxRepr ctx -> Index ctx tp -> RegValue sym tp -> RegValue sym (VariantType ctx)
- type ValMuxFn sym tp = MuxFn (Pred sym) (RegValue sym tp)
- eqMergeFn :: (IsExprBuilder sym, Eq v) => sym -> String -> MuxFn p v
- 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))
- 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)
- muxHandle :: IsExpr (SymExpr sym) => sym -> Pred sym -> FnVal sym a r -> FnVal sym a r -> IO (FnVal sym a r)
Documentation
type family RegValue (sym :: Type) (tp :: CrucibleType) :: Type where ... Source #
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 Source #
A class for CrucibleTypes that have a
mux function.
Methods
Arguments
| :: sym | |
| -> p tp | Unused type to identify what is being merged. |
| -> ValMuxFn sym tp |
Instances
newtype RegValue' sym tp Source #
A newtype wrapper around RegValue. This is wrapper necessary because RegValue is a type family and, as such, cannot be partially applied.
Register values
data FnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where Source #
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 |
fnValType :: FnVal sym args res -> TypeRepr (FunctionHandleType args res) Source #
Extract the runtime representation of the type of the given FnVal
newtype RolledType sym nm ctx Source #
Constructors
| RolledType | |
Fields
| |
data SymSequence sym a where Source #
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) Source # | |
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) Source # | |
Defined in Lang.Crucible.Simulator.SymSequence | |
newtype VariantBranch sym tp Source #
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
eqMergeFn :: (IsExprBuilder sym, Eq v) => sym -> String -> MuxFn p v Source #
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) Source #
muxRecursive :: IsRecursiveType nm => (forall tp. TypeRepr tp -> ValMuxFn sym tp) -> SymbolRepr nm -> CtxRepr ctx -> ValMuxFn sym (RecursiveType nm ctx) Source #
muxStringMap :: IsExprBuilder sym => sym -> MuxFn (Pred sym) e -> MuxFn (Pred sym) (Map Text (PartExpr (Pred sym) e)) Source #
Merge to string maps together.
muxStruct :: (forall tp. TypeRepr tp -> ValMuxFn sym tp) -> CtxRepr ctx -> ValMuxFn sym (StructType ctx) Source #
muxVariant :: IsExprBuilder sym => sym -> (forall tp. TypeRepr tp -> ValMuxFn sym tp) -> CtxRepr ctx -> ValMuxFn sym (VariantType ctx) Source #
muxSymSequence :: sym -> Pred sym -> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a) Source #
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.