| Copyright | (c) Galois Inc 2024 |
|---|---|
| License | BSD3 |
| Maintainer | Langston Barrett <langston@galois.com> |
| Stability | provisional |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.Concretize
Contents
Description
This module defines concRegValue, a function that takes a RegValue (i.e.,
a symbolic value), and a model from the SMT solver (GroundEvalFn), and
returns the concrete value that the symbolic value takes in the model.
This can be used to report specific values that lead to violations of assertions, including safety assertions.
Synopsis
- type family ConcRegValue sym tp where ...
- newtype ConcRV' sym tp = ConcRV' {
- unConcRV' :: ConcRegValue sym tp
- data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRV' sym tp)
- type family ConcIntrinsic nm ctx
- newtype IntrinsicConcFn t nm = IntrinsicConcFn (forall sym ctx. SymExpr sym ~ Expr t => IsExprBuilder sym => ConcCtx sym t -> Assignment TypeRepr ctx -> Intrinsic sym nm ctx -> IO (ConcRegValue sym (IntrinsicType nm ctx)))
- data ConcCtx sym t = ConcCtx {
- model :: GroundEvalFn t
- intrinsicConcFuns :: MapF SymbolRepr (IntrinsicConcFn t)
- concRegValue :: SymExpr sym ~ Expr t => IsExprBuilder sym => ConcCtx sym t -> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
- concRegEntry :: SymExpr sym ~ Expr t => IsExprBuilder sym => ConcCtx sym t -> RegEntry sym tp -> IO (ConcRegValue sym tp)
- concRegMap :: SymExpr sym ~ Expr t => IsExprBuilder sym => ConcCtx sym t -> RegMap sym tps -> IO (Assignment (ConcRV' sym) tps)
- newtype IntrinsicConcToSymFn nm = IntrinsicConcToSymFn (forall sym ctx. IsExprBuilder sym => sym -> Assignment TypeRepr ctx -> ConcIntrinsic nm ctx -> IO (RegValue sym (IntrinsicType nm ctx)))
- concToSym :: sym ~ ExprBuilder scope st (Flags fm) => sym -> MapF SymbolRepr IntrinsicConcToSymFn -> FloatModeRepr fm -> TypeRepr tp -> ConcRegValue sym tp -> IO (RegValue sym tp)
Documentation
type family ConcRegValue sym tp where ... Source #
Defines the "concrete" interpretations of CrucibleType (as opposed
to the "symbolic" interpretations, which are defined by RegValue), as
returned by concRegValue.
Unlike What4's GroundValue, this type family is parameterized
by sym, the symbolic backend. This is because Crucible makes use of
"interpreted" floating point numbers (SymInterpretedFloatType). What4's
SymFloat always uses an IEEE-754 interpretation of symbolic floats, whereas
SymInterpretedFloatType can use IEEE-754, real numbers, or uninterpreted
functions depending on how the symbolic backend is configured.
Equations
| ConcRegValue sym (BaseToType bt) = GroundValue bt | |
| ConcRegValue sym (FloatType fi) = GroundValue (SymInterpretedFloatType sym fi) | |
| ConcRegValue sym AnyType = ConcAnyValue sym | |
| ConcRegValue sym UnitType = () | |
| ConcRegValue sym NatType = Integer | |
| ConcRegValue sym CharType = Word16 | |
| ConcRegValue sym (FunctionHandleType a r) = ConcFnVal sym a r | |
| ConcRegValue sym (MaybeType tp) = Maybe (ConcRegValue sym tp) | |
| ConcRegValue sym (VectorType tp) = Vector (ConcRV' sym tp) | |
| ConcRegValue sym (SequenceType tp) = Seq (ConcRV' sym tp) | |
| ConcRegValue sym (StructType ctx) = Assignment (ConcRV' sym) ctx | |
| ConcRegValue sym (VariantType ctx) = Assignment (ConcVariantBranch sym) ctx | |
| ConcRegValue sym (ReferenceType tp) = NonEmpty (RefCell tp) | |
| ConcRegValue sym (WordMapType w tp) = () | |
| ConcRegValue sym (RecursiveType nm ctx) = ConcRegValue sym (UnrollType nm ctx) | |
| ConcRegValue sym (IntrinsicType nm ctx) = ConcIntrinsic nm ctx | |
| ConcRegValue sym (StringMapType tp) = Map Text (ConcRV' sym tp) |
newtype ConcRV' sym tp Source #
Newtype to allow partial application of ConcRegValue.
Type families cannot appear partially applied.
Constructors
| ConcRV' | |
Fields
| |
data ConcAnyValue sym Source #
An AnyValue concretized by concRegValue
Constructors
| forall tp. ConcAnyValue (TypeRepr tp) (ConcRV' sym tp) |
type family ConcIntrinsic nm ctx Source #
Open type family for defining how intrinsics are concretized
newtype IntrinsicConcFn t nm Source #
Function for concretizing an intrinsic type
Constructors
| IntrinsicConcFn (forall sym ctx. SymExpr sym ~ Expr t => IsExprBuilder sym => ConcCtx sym t -> Assignment TypeRepr ctx -> Intrinsic sym nm ctx -> IO (ConcRegValue sym (IntrinsicType nm ctx))) |
Context needed for concRegValue
The t parameter matches that on GroundEvalFn and Expr, namely, it
is a phantom type brand used to relate nonces to a specific nonce generator
(similar to the s parameter of the ST monad). It also appears as the
first argument to ExprBuilder.
Constructors
| ConcCtx | |
Fields
| |
concRegValue :: SymExpr sym ~ Expr t => IsExprBuilder sym => ConcCtx sym t -> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp) Source #
Pick a feasible concrete value from the model
This function does not attempt to "normalize" variants nor mux trees in any way. If the model reports that multiple branches of a variant or mux tree are plausible, then multiple branches might be included in the result.
concRegEntry :: SymExpr sym ~ Expr t => IsExprBuilder sym => ConcCtx sym t -> RegEntry sym tp -> IO (ConcRegValue sym tp) Source #
Like concRegValue, but for RegEntry
concRegMap :: SymExpr sym ~ Expr t => IsExprBuilder sym => ConcCtx sym t -> RegMap sym tps -> IO (Assignment (ConcRV' sym) tps) Source #
Like concRegEntry, but for a whole RegMap
There and back again
newtype IntrinsicConcToSymFn nm Source #
Function for re-symbolizing an intrinsic type
Constructors
| IntrinsicConcToSymFn (forall sym ctx. IsExprBuilder sym => sym -> Assignment TypeRepr ctx -> ConcIntrinsic nm ctx -> IO (RegValue sym (IntrinsicType nm ctx))) |
concToSym :: sym ~ ExprBuilder scope st (Flags fm) => sym -> MapF SymbolRepr IntrinsicConcToSymFn -> FloatModeRepr fm -> TypeRepr tp -> ConcRegValue sym tp -> IO (RegValue sym tp) Source #
Inject a ConcRegValue back into a RegValue.