| Copyright | (c) Galois Inc 2024 |
|---|---|
| License | BSD3 |
| Maintainer | Langston Barrett <langston@galois.com> |
| Stability | provisional |
| Safe Haskell | None |
| Language | Haskell2010 |
Lang.Crucible.Concretize
Description
This module defines three different kinds of functions. In order of how much work they perform:
- Grounding functions (e.g.,
groundRegValue) take symbolic values (RegValues) and a model from an SMT solver (GroundEvalFn), and return the concrete value (ConcRegValue) that the symbolic value takes in the model. These functions can be used to report specific values that lead to violations of assertions, including safety assertions. - Concretization functions (e.g.,
concRegValue) request a model that is consistent with the current assumptions (e.g., path conditions) from the symbolic backend, and then ground a value in that model. These can be used to reduce the size and complexity of later queries to SMT solvers, at the cost of no longer being sound from a verification standpoint. - Unique concretization functions (e.g.,
uniquelyConcRegValue) do the same thing as concretization functions, but then check if the concrete value is the only possible value for the given symbolic expression in any model.
Synopsis
- type family ConcRegValue sym (tp :: CrucibleType) where ...
- newtype ConcRV' sym (tp :: CrucibleType) = ConcRV' {
- unConcRV' :: ConcRegValue sym tp
- asConcRegValue :: forall sym proxy (tp :: CrucibleType). IsExpr (SymExpr sym) => proxy sym -> TypeRepr tp -> RegValue sym tp -> Maybe (ConcRegValue sym tp)
- asConcRegEntry :: forall sym (tp :: CrucibleType). IsExpr (SymExpr sym) => RegEntry sym tp -> Maybe (ConcRegValue sym tp)
- asConcRegMap :: forall sym (tp :: Ctx CrucibleType). IsExpr (SymExpr sym) => RegMap sym tp -> Maybe (Assignment (ConcRV' sym) tp)
- data ConcAnyValue sym = ConcAnyValue (TypeRepr tp) (ConcRV' sym tp)
- type family ConcIntrinsic (nm :: Symbol) (ctx :: Ctx CrucibleType)
- newtype IntrinsicConcFn t (nm :: Symbol) = IntrinsicConcFn (forall sym (ctx :: Ctx CrucibleType). (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)
- groundRegValue :: forall sym t (tp :: CrucibleType). (SymExpr sym ~ Expr t, IsExprBuilder sym) => ConcCtx sym t -> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
- groundRegEntry :: forall sym t (tp :: CrucibleType). (SymExpr sym ~ Expr t, IsExprBuilder sym) => ConcCtx sym t -> RegEntry sym tp -> IO (ConcRegValue sym tp)
- groundRegMap :: forall sym t (tps :: Ctx CrucibleType). (SymExpr sym ~ Expr t, IsExprBuilder sym) => ConcCtx sym t -> RegMap sym tps -> IO (Assignment (ConcRV' sym) tps)
- concRegValue :: forall (tp :: CrucibleType) sym bak solver scope (st :: Type -> Type) fs. (IsSymBackend sym bak, sym ~ ExprBuilder scope st fs, SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) => bak -> MapF SymbolRepr (IntrinsicConcFn scope) -> TypeRepr tp -> RegValue sym tp -> IO (Either ConcretizationFailure (ConcRegValue sym tp))
- concRegEntry :: forall (tp :: CrucibleType) sym bak solver scope (st :: Type -> Type) fs. (IsSymBackend sym bak, sym ~ ExprBuilder scope st fs, SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) => bak -> MapF SymbolRepr (IntrinsicConcFn scope) -> RegEntry sym tp -> IO (Either ConcretizationFailure (ConcRegValue sym tp))
- concRegMap :: forall (tps :: Ctx CrucibleType) sym bak solver scope (st :: Type -> Type) fs. (IsSymBackend sym bak, sym ~ ExprBuilder scope st fs, SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) => bak -> MapF SymbolRepr (IntrinsicConcFn scope) -> RegMap sym tps -> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
- uniquelyConcRegValue :: forall (tp :: CrucibleType) sym bak solver scope (st :: Type -> Type) (fm :: FloatMode). (IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm), SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st (Flags fm), OnlineSolver solver) => bak -> FloatModeRepr fm -> MapF SymbolRepr (IntrinsicConcFn scope) -> MapF SymbolRepr IntrinsicConcToSymFn -> TypeRepr tp -> RegValue sym tp -> IO (Either UniqueConcretizationFailure (ConcRegValue sym tp))
- uniquelyConcRegEntry :: forall (tp :: CrucibleType) sym bak solver scope (st :: Type -> Type) (fm :: FloatMode). (IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm), SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st (Flags fm), OnlineSolver solver) => bak -> FloatModeRepr fm -> MapF SymbolRepr (IntrinsicConcFn scope) -> MapF SymbolRepr IntrinsicConcToSymFn -> RegEntry sym tp -> IO (Either UniqueConcretizationFailure (ConcRegValue sym tp))
- uniquelyConcRegMap :: forall (tps :: Ctx CrucibleType) sym bak solver scope (st :: Type -> Type) (fm :: FloatMode). (IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm), SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st (Flags fm), OnlineSolver solver) => bak -> FloatModeRepr fm -> MapF SymbolRepr (IntrinsicConcFn scope) -> MapF SymbolRepr IntrinsicConcToSymFn -> RegMap sym tps -> IO (Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps))
- newtype IntrinsicConcToSymFn (nm :: Symbol) = IntrinsicConcToSymFn (forall sym (ctx :: Ctx CrucibleType). IsExprBuilder sym => sym -> Assignment TypeRepr ctx -> ConcIntrinsic nm ctx -> IO (RegValue sym (IntrinsicType nm ctx)))
- concToSym :: forall sym scope (st :: Type -> Type) (fm :: FloatMode) (tp :: CrucibleType). 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 :: CrucibleType) where ... Source #
Defines the "concrete" interpretations of CrucibleType (as opposed
to the "symbolic" interpretations, which are defined by RegValue), as
returned by groundRegValue.
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 :: CrucibleType) Source #
Newtype to allow partial application of ConcRegValue.
Type families cannot appear partially applied.
Constructors
| ConcRV' | |
Fields
| |
asConcRegValue :: forall sym proxy (tp :: CrucibleType). IsExpr (SymExpr sym) => proxy sym -> TypeRepr tp -> RegValue sym tp -> Maybe (ConcRegValue sym tp) Source #
Check if a RegValue is actually concrete
asConcRegEntry :: forall sym (tp :: CrucibleType). IsExpr (SymExpr sym) => RegEntry sym tp -> Maybe (ConcRegValue sym tp) Source #
Check if a RegEntry is actually concrete
asConcRegMap :: forall sym (tp :: Ctx CrucibleType). IsExpr (SymExpr sym) => RegMap sym tp -> Maybe (Assignment (ConcRV' sym) tp) Source #
Check if a RegMap is actually concrete
data ConcAnyValue sym Source #
An AnyValue concretized by groundRegValue
Constructors
| ConcAnyValue (TypeRepr tp) (ConcRV' sym tp) |
type family ConcIntrinsic (nm :: Symbol) (ctx :: Ctx CrucibleType) Source #
Open type family for defining how intrinsics are concretized
newtype IntrinsicConcFn t (nm :: Symbol) Source #
Function for concretizing an intrinsic type
Constructors
| IntrinsicConcFn (forall sym (ctx :: Ctx CrucibleType). (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 groundRegValue
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
| |
Grounding
groundRegValue :: forall sym t (tp :: CrucibleType). (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.
groundRegEntry :: forall sym t (tp :: CrucibleType). (SymExpr sym ~ Expr t, IsExprBuilder sym) => ConcCtx sym t -> RegEntry sym tp -> IO (ConcRegValue sym tp) Source #
Like groundRegValue, but for RegEntry
groundRegMap :: forall sym t (tps :: Ctx CrucibleType). (SymExpr sym ~ Expr t, IsExprBuilder sym) => ConcCtx sym t -> RegMap sym tps -> IO (Assignment (ConcRV' sym) tps) Source #
Like groundRegEntry, but for a whole RegMap
Concretization
concRegValue :: forall (tp :: CrucibleType) sym bak solver scope (st :: Type -> Type) fs. (IsSymBackend sym bak, sym ~ ExprBuilder scope st fs, SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) => bak -> MapF SymbolRepr (IntrinsicConcFn scope) -> TypeRepr tp -> RegValue sym tp -> IO (Either ConcretizationFailure (ConcRegValue sym tp)) Source #
Generate a model and pick a feasible concrete value from it
concRegEntry :: forall (tp :: CrucibleType) sym bak solver scope (st :: Type -> Type) fs. (IsSymBackend sym bak, sym ~ ExprBuilder scope st fs, SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) => bak -> MapF SymbolRepr (IntrinsicConcFn scope) -> RegEntry sym tp -> IO (Either ConcretizationFailure (ConcRegValue sym tp)) Source #
Generate a model and pick a feasible concrete value from it
concRegMap :: forall (tps :: Ctx CrucibleType) sym bak solver scope (st :: Type -> Type) fs. (IsSymBackend sym bak, sym ~ ExprBuilder scope st fs, SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) => bak -> MapF SymbolRepr (IntrinsicConcFn scope) -> RegMap sym tps -> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps)) Source #
Like concRegValue, but for a whole RegMap
Unique concretization
uniquelyConcRegValue :: forall (tp :: CrucibleType) sym bak solver scope (st :: Type -> Type) (fm :: FloatMode). (IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm), SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st (Flags fm), OnlineSolver solver) => bak -> FloatModeRepr fm -> MapF SymbolRepr (IntrinsicConcFn scope) -> MapF SymbolRepr IntrinsicConcToSymFn -> TypeRepr tp -> RegValue sym tp -> IO (Either UniqueConcretizationFailure (ConcRegValue sym tp)) Source #
Generate a model and pick a feasible concrete value from it
uniquelyConcRegEntry :: forall (tp :: CrucibleType) sym bak solver scope (st :: Type -> Type) (fm :: FloatMode). (IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm), SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st (Flags fm), OnlineSolver solver) => bak -> FloatModeRepr fm -> MapF SymbolRepr (IntrinsicConcFn scope) -> MapF SymbolRepr IntrinsicConcToSymFn -> RegEntry sym tp -> IO (Either UniqueConcretizationFailure (ConcRegValue sym tp)) Source #
Generate a model and pick a feasible concrete value from it
uniquelyConcRegMap :: forall (tps :: Ctx CrucibleType) sym bak solver scope (st :: Type -> Type) (fm :: FloatMode). (IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm), SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st (Flags fm), OnlineSolver solver) => bak -> FloatModeRepr fm -> MapF SymbolRepr (IntrinsicConcFn scope) -> MapF SymbolRepr IntrinsicConcToSymFn -> RegMap sym tps -> IO (Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)) Source #
Like concRegValue, but for a whole RegMap
There and back again
newtype IntrinsicConcToSymFn (nm :: Symbol) Source #
Function for re-symbolizing an intrinsic type
Constructors
| IntrinsicConcToSymFn (forall sym (ctx :: Ctx CrucibleType). IsExprBuilder sym => sym -> Assignment TypeRepr ctx -> ConcIntrinsic nm ctx -> IO (RegValue sym (IntrinsicType nm ctx))) |
concToSym :: forall sym scope (st :: Type -> Type) (fm :: FloatMode) (tp :: CrucibleType). 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.