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

Lang.Crucible.Simulator.RegValue

Contents

Register values
Value mux functions
Equality

Description

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

Synopsis

type family RegValue sym (tp :: CrucibleType) where ...
class CanMux sym (tp :: CrucibleType) where
- muxReg :: sym -> p tp -> ValMuxFn sym tp
newtype RegValue' sym (tp :: CrucibleType) = RV {
- unRV :: RegValue sym tp
}
type MuxFn p v = p -> v -> v -> IO v
data AnyValue sym where
- AnyValue :: forall (tp :: CrucibleType) sym. TypeRepr tp -> RegValue sym tp -> AnyValue sym
data FnVal sym (args :: Ctx CrucibleType) (res :: CrucibleType) where
- ClosureFnVal :: forall sym (args :: Ctx CrucibleType) (tp :: CrucibleType) (res :: CrucibleType). !(FnVal sym (args ::> tp) res) -> !(TypeRepr tp) -> !(RegValue sym tp) -> FnVal sym args res
- VarargsFnVal :: forall (args1 :: Ctx CrucibleType) (res :: CrucibleType) (addlArgs :: Ctx CrucibleType) sym. !(FnHandle (args1 ::> VectorType AnyType) res) -> !(CtxRepr addlArgs) -> FnVal sym (args1 <+> addlArgs) res
- HandleFnVal :: forall (args :: Ctx CrucibleType) (res :: CrucibleType) sym. !(FnHandle args res) -> FnVal sym args res
fnValType :: forall sym (args :: Ctx CrucibleType) (res :: CrucibleType). FnVal sym args res -> TypeRepr (FunctionHandleType args res)
newtype RolledType sym (nm :: Symbol) (ctx :: Ctx CrucibleType) = RolledType {
- unroll :: RegValue sym (UnrollType nm ctx)
}
data SymSequence sym a where
- SymSequenceNil :: forall sym a. SymSequence sym a
- SymSequenceCons :: forall a sym. !(Nonce GlobalNonceGenerator a) -> a -> !(SymSequence sym a) -> SymSequence sym a
- SymSequenceAppend :: forall a sym. !(Nonce GlobalNonceGenerator a) -> !(SymSequence sym a) -> !(SymSequence sym a) -> SymSequence sym a
- SymSequenceMerge :: forall a sym. !(Nonce GlobalNonceGenerator a) -> !(Pred sym) -> !(SymSequence sym a) -> !(SymSequence sym a) -> SymSequence sym a
newtype VariantBranch sym (tp :: CrucibleType) = VB {
- unVB :: PartExpr (Pred sym) (RegValue sym tp)
}
injectVariant :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType). IsExprBuilder sym => sym -> CtxRepr ctx -> Index ctx tp -> RegValue sym tp -> RegValue sym (VariantType ctx)
type ValMuxFn sym (tp :: CrucibleType) = 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 :: forall (nm :: Symbol) sym (ctx :: Ctx CrucibleType). IsRecursiveType nm => (forall (tp :: CrucibleType). 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 sym (ctx :: Ctx CrucibleType). (forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp) -> CtxRepr ctx -> ValMuxFn sym (StructType ctx)
muxVariant :: forall sym (ctx :: Ctx CrucibleType). IsExprBuilder sym => sym -> (forall (tp :: CrucibleType). 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 :: forall sym (a :: Ctx CrucibleType) (r :: CrucibleType). IsExpr (SymExpr sym) => sym -> Pred sym -> FnVal sym a r -> FnVal sym a r -> IO (FnVal sym a r)
eqRegValue :: forall sym (tp :: CrucibleType). IsInterpretedFloatExprBuilder sym => sym -> TypeRepr tp -> RegValue sym tp -> RegValue sym tp -> IO (Pred sym)

Documentation

type family RegValue sym (tp :: CrucibleType) 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

muxReg Source #

Arguments

:: sym
-> p tp	Unused type to identify what is being merged.
-> ValMuxFn sym tp

Instances

Instances details

IsExprBuilder sym => CanMux sym BoolType Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p BoolType -> ValMuxFn sym BoolType Source #
IsSymInterface sym => CanMux sym CharType Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p CharType -> ValMuxFn sym CharType Source #
IsExprBuilder sym => CanMux sym ComplexRealType Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p ComplexRealType -> ValMuxFn sym ComplexRealType Source #
IsExprBuilder sym => CanMux sym IntegerType Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p IntegerType -> ValMuxFn sym IntegerType Source #
IsExprBuilder sym => CanMux sym NatType Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p NatType -> ValMuxFn sym NatType Source #
IsExprBuilder sym => CanMux sym RealValType Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p RealValType -> ValMuxFn sym RealValType Source #
CanMux sym UnitType Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p UnitType -> ValMuxFn sym UnitType Source #
IsInterpretedFloatExprBuilder sym => CanMux sym (FloatType fi) Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p (FloatType fi) -> ValMuxFn sym (FloatType fi) Source #
IsExprBuilder sym => CanMux sym (IEEEFloatType fpp) Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p (IEEEFloatType fpp) -> ValMuxFn sym (IEEEFloatType fpp) Source #
(IsExprBuilder sym, CanMux sym tp) => CanMux sym (MaybeType tp) Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p (MaybeType tp) -> ValMuxFn sym (MaybeType tp) Source #
IsExprBuilder sym => CanMux sym (StringType si) Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p (StringType si) -> ValMuxFn sym (StringType si) Source #
(IsSymInterface sym, CanMux sym tp) => CanMux sym (VectorType tp) Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p (VectorType tp) -> ValMuxFn sym (VectorType tp) Source #
IsExprBuilder sym => CanMux sym (FunctionHandleType a r) Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p (FunctionHandleType a r) -> ValMuxFn sym (FunctionHandleType a r) Source #
(IsExprBuilder sym, KnownNat w, KnownRepr BaseTypeRepr tp) => CanMux sym (WordMapType w tp) Source #
Instance details Defined in Lang.Crucible.Simulator.RegValue Methods muxReg :: sym -> p (WordMapType w tp) -> ValMuxFn sym (WordMapType w tp) Source #

newtype RegValue' sym (tp :: CrucibleType) Source #

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

Register values

data AnyValue sym where Source #

Constructors

AnyValue :: forall (tp :: CrucibleType) sym. TypeRepr tp -> RegValue sym tp -> AnyValue sym

data FnVal sym (args :: Ctx CrucibleType) (res :: CrucibleType) where Source #

Represents a function closure.

Constructors

ClosureFnVal :: forall sym (args :: Ctx CrucibleType) (tp :: CrucibleType) (res :: CrucibleType). !(FnVal sym (args ::> tp) res) -> !(TypeRepr tp) -> !(RegValue sym tp) -> FnVal sym args res
VarargsFnVal :: forall (args1 :: Ctx CrucibleType) (res :: CrucibleType) (addlArgs :: Ctx CrucibleType) sym. !(FnHandle (args1 ::> VectorType AnyType) res) -> !(CtxRepr addlArgs) -> FnVal sym (args1 <+> addlArgs) res
HandleFnVal :: forall (args :: Ctx CrucibleType) (res :: CrucibleType) sym. !(FnHandle args res) -> FnVal sym args res

Instances

Instances details

Show (FnVal sym a r) Source #
Instance details 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 :: forall sym (args :: Ctx CrucibleType) (res :: CrucibleType). FnVal sym args res -> TypeRepr (FunctionHandleType args res) Source #

Extract the runtime representation of the type of the given FnVal

newtype RolledType sym (nm :: Symbol) (ctx :: Ctx CrucibleType) Source #

Constructors

RolledType
Fields unroll :: RegValue sym (UnrollType nm ctx)

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 :: forall sym a. SymSequence sym a
SymSequenceCons :: forall a sym. !(Nonce GlobalNonceGenerator a) -> a -> !(SymSequence sym a) -> SymSequence sym a
SymSequenceAppend :: forall a sym. !(Nonce GlobalNonceGenerator a) -> !(SymSequence sym a) -> !(SymSequence sym a) -> SymSequence sym a
SymSequenceMerge :: forall a sym. !(Nonce GlobalNonceGenerator a) -> !(Pred sym) -> !(SymSequence sym a) -> !(SymSequence sym a) -> SymSequence sym a

Instances

Instances details

Eq (SymSequence sym a) Source #
Instance details 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 #
Instance details Defined in Lang.Crucible.Simulator.SymSequence Methods pretty :: SymSequence sym a -> Doc ann # prettyList :: [SymSequence sym a] -> Doc ann #

newtype VariantBranch sym (tp :: CrucibleType) Source #

Constructors

VB
Fields unVB :: PartExpr (Pred sym) (RegValue sym tp)

injectVariant Source #

Arguments

:: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType). 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 :: CrucibleType) = MuxFn (Pred sym) (RegValue sym tp) Source #

Version of MuxFn specialized to RegValue

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 :: forall (nm :: Symbol) sym (ctx :: Ctx CrucibleType). IsRecursiveType nm => (forall (tp :: CrucibleType). 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 sym (ctx :: Ctx CrucibleType). (forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp) -> CtxRepr ctx -> ValMuxFn sym (StructType ctx) Source #

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

muxVector :: IsExprBuilder sym => sym -> MuxFn p e -> MuxFn p (Vector e) 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.

muxHandle :: forall sym (a :: Ctx CrucibleType) (r :: CrucibleType). IsExpr (SymExpr sym) => sym -> Pred sym -> FnVal sym a r -> FnVal sym a r -> IO (FnVal sym a r) Source #

Equality

eqRegValue :: forall sym (tp :: CrucibleType). IsInterpretedFloatExprBuilder sym => sym -> TypeRepr tp -> RegValue sym tp -> RegValue sym tp -> IO (Pred sym) Source #

Equality of RegValues.

This is only supported for a few types, see #1582.