| Copyright | (c) Galois Inc 2014-2022 |
|---|---|
| License | BSD3 |
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.Backend
Description
This module provides an interface that symbolic backends must provide for interacting with the symbolic simulator.
Compared to the solver connections provided by What4, Crucible backends provide
a facility for managing an assumption stack (see AssumptionStack). Note
that these backends are layered on top of the ExprBuilder;
the solver choice is still up to the user. The
SimpleBackend is designed to be used with an
offline solver connection, while the
OnlineBackend is designed to be used with an
online solver.
The AssumptionStack tracks the assumptions that are in scope for each
assertion, accounting for the branching and merging structure of programs. The
symbolic simulator manages the AssumptionStack. After symbolic simulation
completes, the caller should traverse the AssumptionStack (or use
combinators like proofGoalsToList) to discharge the resulting proof
obligations with a solver backend.
Synopsis
- class (IsSymInterface sym, HasSymInterface sym bak) => IsSymBackend sym bak | bak -> sym where
- pushAssumptionFrame :: bak -> IO FrameIdentifier
- popAssumptionFrame :: bak -> FrameIdentifier -> IO (Assumptions sym)
- popUntilAssumptionFrame :: bak -> FrameIdentifier -> IO ()
- popAssumptionFrameAndObligations :: bak -> FrameIdentifier -> IO (Assumptions sym, ProofObligations sym)
- addAssumption :: bak -> Assumption sym -> IO ()
- addAssumptions :: bak -> Assumptions sym -> IO ()
- getPathCondition :: bak -> IO (Pred sym)
- collectAssumptions :: bak -> IO (Assumptions sym)
- addProofObligation :: bak -> Assertion sym -> IO ()
- addDurableProofObligation :: bak -> Assertion sym -> IO ()
- getProofObligations :: bak -> IO (ProofObligations sym)
- clearProofObligations :: bak -> IO ()
- saveAssumptionState :: bak -> IO (AssumptionState sym)
- restoreAssumptionState :: bak -> AssumptionState sym -> IO ()
- resetAssumptionState :: bak -> IO ()
- type IsSymInterface sym = (IsSymExprBuilder sym, IsInterpretedFloatSymExprBuilder sym)
- class HasSymInterface sym bak | bak -> sym where
- backendGetSym :: bak -> sym
- data SomeBackend sym = forall bak.IsSymBackend sym bak => SomeBackend bak
- data CrucibleAssumption (e :: BaseType -> Type)
- data CrucibleEvent (e :: BaseType -> Type) where
- CreateVariableEvent :: ProgramLoc -> String -> BaseTypeRepr tp -> e tp -> CrucibleEvent e
- LocationReachedEvent :: ProgramLoc -> CrucibleEvent e
- data CrucibleAssumptions (e :: BaseType -> Type) where
- SingleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e
- SingleEvent :: CrucibleEvent e -> CrucibleAssumptions e
- ManyAssumptions :: Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
- MergeAssumptions :: e BaseBoolType -> CrucibleAssumptions e -> CrucibleAssumptions e -> CrucibleAssumptions e
- type Assumption sym = CrucibleAssumption (SymExpr sym)
- type Assertion sym = LabeledPred (Pred sym) SimError
- type Assumptions sym = CrucibleAssumptions (SymExpr sym)
- concretizeEvents :: IsExpr e => (forall tp. e tp -> IO (GroundValue tp)) -> CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper]
- ppEvent :: IsExpr e => CrucibleEvent e -> Doc ann
- singleEvent :: CrucibleEvent e -> CrucibleAssumptions e
- singleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e
- trivialAssumption :: IsExpr e => CrucibleAssumption e -> Bool
- impossibleAssumption :: IsExpr e => CrucibleAssumption e -> Maybe AbortExecReason
- ppAssumption :: (forall tp. e tp -> Doc ann) -> CrucibleAssumption e -> Doc ann
- assumptionLoc :: CrucibleAssumption e -> ProgramLoc
- eventLoc :: CrucibleEvent e -> ProgramLoc
- mergeAssumptions :: IsExprBuilder sym => sym -> Pred sym -> Assumptions sym -> Assumptions sym -> IO (Assumptions sym)
- assumptionPred :: CrucibleAssumption e -> e BaseBoolType
- forgetAssumption :: CrucibleAssumption e -> CrucibleAssumption (Const ())
- assumptionsPred :: IsExprBuilder sym => sym -> Assumptions sym -> IO (Pred sym)
- flattenAssumptions :: IsExprBuilder sym => sym -> Assumptions sym -> IO [Assumption sym]
- assumptionsTopLevelLocs :: CrucibleAssumptions e -> [ProgramLoc]
- type ProofObligation sym = ProofGoal (Assumptions sym) (Assertion sym)
- type ProofObligations sym = Maybe (Goals (Assumptions sym) (Assertion sym))
- type AssumptionState sym = GoalCollector (Assumptions sym) (Assertion sym)
- assert :: IsSymBackend sym bak => bak -> Pred sym -> SimErrorReason -> IO ()
- data LabeledPred pred msg = LabeledPred {
- _labeledPred :: !pred
- _labeledPredMsg :: !msg
- labeledPred :: forall pred msg pred' f. Functor f => (pred -> f pred') -> LabeledPred pred msg -> f (LabeledPred pred' msg)
- labeledPredMsg :: forall pred msg msg' f. Functor f => (msg -> f msg') -> LabeledPred pred msg -> f (LabeledPred pred msg')
- data AssumptionStack asmp ast
- data FrameIdentifier
- data ProofGoal asmp goal = ProofGoal {
- proofAssumptions :: asmp
- proofGoal :: goal
- data Goals asmp goal
- goalsToList :: Monoid asmp => Goals asmp goal -> [ProofGoal asmp goal]
- data AbortExecReason
- abortExecBecause :: AbortExecReason -> IO a
- ppAbortExecReason :: AbortExecReason -> Doc ann
- throwUnsupported :: (IsExprBuilder sym, MonadIO m, HasCallStack) => sym -> String -> m a
- addAssertion :: IsSymBackend sym bak => bak -> Assertion sym -> IO ()
- addDurableAssertion :: IsSymBackend sym bak => bak -> Assertion sym -> IO ()
- addAssertionM :: IsSymBackend sym bak => bak -> IO (Pred sym) -> SimErrorReason -> IO ()
- addFailedAssertion :: IsSymBackend sym bak => bak -> SimErrorReason -> IO a
- assertIsInteger :: IsSymBackend sym bak => bak -> SymReal sym -> SimErrorReason -> IO ()
- readPartExpr :: IsSymBackend sym bak => bak -> PartExpr (Pred sym) v -> SimErrorReason -> IO v
- ppProofObligation :: IsExprBuilder sym => sym -> ProofObligation sym -> IO (Doc ann)
- backendOptions :: [ConfigDesc]
- assertThenAssumeConfigOption :: ConfigOption BaseBoolType
Documentation
class (IsSymInterface sym, HasSymInterface sym bak) => IsSymBackend sym bak | bak -> sym where Source #
This class provides operations that interact with the symbolic simulator. It allows for logical assumptions/assertions to be added to the current path condition, and allows queries to be asked about branch conditions.
The bak type contains all the datastructures necessary to
maintain the current program path conditions, and keep track of
assumptions and assertions made during program execution. The sym
type is expected to satisfy the IsSymInterface constraints, which
provide access to the What4 expression language. A sym is uniquely
determined by a bak.
Minimal complete definition
pushAssumptionFrame, popAssumptionFrame, popUntilAssumptionFrame, popAssumptionFrameAndObligations, addAssumption, addAssumptions, getPathCondition, collectAssumptions, addDurableProofObligation, getProofObligations, clearProofObligations, saveAssumptionState, restoreAssumptionState
Methods
pushAssumptionFrame :: bak -> IO FrameIdentifier Source #
Push a new assumption frame onto the stack. Assumptions and assertions made will now be associated with this frame on the stack until a new frame is pushed onto the stack, or until this one is popped.
popAssumptionFrame :: bak -> FrameIdentifier -> IO (Assumptions sym) Source #
Pop an assumption frame from the stack. The collected assumptions in this frame are returned. Pops are required to be well-bracketed with pushes. In particular, if the given frame identifier is not the identifier of the top frame on the stack, an error will be raised.
popUntilAssumptionFrame :: bak -> FrameIdentifier -> IO () Source #
Pop all assumption frames up to and including the frame with the given frame identifier. This operation will panic if the named frame does not exist on the stack.
popAssumptionFrameAndObligations :: bak -> FrameIdentifier -> IO (Assumptions sym, ProofObligations sym) Source #
Pop an assumption frame from the stack. The collected assummptions in this frame are returned, along with any proof obligations that were incurred while the frame was active. Pops are required to be well-bracketed with pushes. In particular, if the given frame identifier is not the identifier of the top frame on the stack, an error will be raised.
addAssumption :: bak -> Assumption sym -> IO () Source #
Add an assumption to the current state.
addAssumptions :: bak -> Assumptions sym -> IO () Source #
Add a collection of assumptions to the current state.
getPathCondition :: bak -> IO (Pred sym) Source #
Get the current path condition as a predicate. This consists of the conjunction of all the assumptions currently in scope.
collectAssumptions :: bak -> IO (Assumptions sym) Source #
Collect all the assumptions currently in scope
addProofObligation :: bak -> Assertion sym -> IO () Source #
Add a new proof obligation to the system.
The proof may use the current path condition and assumptions. Note
that this *DOES NOT* add the goal as an assumption. See also
addAssertion. Also note that predicates that concretely evaluate
to True will be silently discarded. See addDurableProofObligation
to avoid discarding goals.
addDurableProofObligation :: bak -> Assertion sym -> IO () Source #
Add a new proof obligation to the system which will persist
throughout symbolic execution even if it is concretely valid.
The proof may use the current path condition and assumptions. Note
that this *DOES NOT* add the goal as an assumption. See also
addDurableAssertion.
getProofObligations :: bak -> IO (ProofObligations sym) Source #
Get the collection of proof obligations.
clearProofObligations :: bak -> IO () Source #
Forget the current collection of proof obligations.
Presumably, we've already used getProofObligations to save them
somewhere else.
saveAssumptionState :: bak -> IO (AssumptionState sym) Source #
Create a snapshot of the current assumption state, that may later be restored. This is useful for supporting control-flow patterns that don't neatly fit into the stack push/pop model.
restoreAssumptionState :: bak -> AssumptionState sym -> IO () Source #
Restore the assumption state to a previous snapshot.
resetAssumptionState :: bak -> IO () Source #
Reset the assumption state to a fresh, blank state
Instances
type IsSymInterface sym = (IsSymExprBuilder sym, IsInterpretedFloatSymExprBuilder sym) Source #
class HasSymInterface sym bak | bak -> sym where Source #
Class for backend type that can retrieve sym values.
This is separate from IsSymBackend specifically to avoid
the need for additional class constraints on the backendGetSym
operation, which is occasionally useful.
Methods
backendGetSym :: bak -> sym Source #
Retrive the symbolic expression builder corresponding to this simulator backend.
Instances
| HasSymInterface (ExprBuilder t st fs) (SimpleBackend t st fs) Source # | |
Defined in Lang.Crucible.Backend.Simple Methods backendGetSym :: SimpleBackend t st fs -> ExprBuilder t st fs Source # | |
| HasSymInterface (ExprBuilder t st fs) (OnlineBackend solver t st fs) Source # | |
Defined in Lang.Crucible.Backend.Online Methods backendGetSym :: OnlineBackend solver t st fs -> ExprBuilder t st fs Source # | |
data SomeBackend sym Source #
Constructors
| forall bak.IsSymBackend sym bak => SomeBackend bak |
Assumption management
data CrucibleAssumption (e :: BaseType -> Type) Source #
This type describes assumptions made at some point during program execution.
Constructors
| GenericAssumption ProgramLoc String (e BaseBoolType) | An unstructured description of the source of an assumption. |
| BranchCondition ProgramLoc (Maybe ProgramLoc) (e BaseBoolType) | This arose because we want to explore a specific path. The first location is the location of the branch predicate. The second one is the location of the branch target. |
| AssumingNoError SimError (e BaseBoolType) | An assumption justified by a proof of the impossibility of a certain simulator error. |
data CrucibleEvent (e :: BaseType -> Type) where Source #
This type describes events we can track during program execution.
Constructors
| CreateVariableEvent | This event describes the creation of a symbolic variable. |
Fields
| |
| LocationReachedEvent :: ProgramLoc -> CrucibleEvent e | This event describes reaching a particular program location. |
data CrucibleAssumptions (e :: BaseType -> Type) where Source #
This type tracks both logical assumptions and program events that are relevant when evaluating proof obligations arising from simulation.
Constructors
| SingleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e | |
| SingleEvent :: CrucibleEvent e -> CrucibleAssumptions e | |
| ManyAssumptions :: Seq (CrucibleAssumptions e) -> CrucibleAssumptions e | |
| MergeAssumptions | |
Fields
| |
Instances
| Monoid (CrucibleAssumptions e) Source # | |
Defined in Lang.Crucible.Backend Methods mempty :: CrucibleAssumptions e # mappend :: CrucibleAssumptions e -> CrucibleAssumptions e -> CrucibleAssumptions e # mconcat :: [CrucibleAssumptions e] -> CrucibleAssumptions e # | |
| Semigroup (CrucibleAssumptions e) Source # | |
Defined in Lang.Crucible.Backend Methods (<>) :: CrucibleAssumptions e -> CrucibleAssumptions e -> CrucibleAssumptions e # sconcat :: NonEmpty (CrucibleAssumptions e) -> CrucibleAssumptions e # stimes :: Integral b => b -> CrucibleAssumptions e -> CrucibleAssumptions e # | |
type Assumption sym = CrucibleAssumption (SymExpr sym) Source #
type Assumptions sym = CrucibleAssumptions (SymExpr sym) Source #
concretizeEvents :: IsExpr e => (forall tp. e tp -> IO (GroundValue tp)) -> CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper] Source #
Given a ground evaluation function, compute a linear, ground-valued sequence of events corresponding to this program run.
singleEvent :: CrucibleEvent e -> CrucibleAssumptions e Source #
trivialAssumption :: IsExpr e => CrucibleAssumption e -> Bool Source #
Check if an assumption is trivial (always true)
impossibleAssumption :: IsExpr e => CrucibleAssumption e -> Maybe AbortExecReason Source #
If an assumption is clearly impossible, return an abort reason that can be used to unwind the execution of this branch.
ppAssumption :: (forall tp. e tp -> Doc ann) -> CrucibleAssumption e -> Doc ann Source #
assumptionLoc :: CrucibleAssumption e -> ProgramLoc Source #
Return the program location associated with an assumption
eventLoc :: CrucibleEvent e -> ProgramLoc Source #
Return the program location associated with an event
mergeAssumptions :: IsExprBuilder sym => sym -> Pred sym -> Assumptions sym -> Assumptions sym -> IO (Assumptions sym) Source #
Merge the assumptions collected from the branches of a conditional.
assumptionPred :: CrucibleAssumption e -> e BaseBoolType Source #
Get the predicate associated with this assumption
forgetAssumption :: CrucibleAssumption e -> CrucibleAssumption (Const ()) Source #
assumptionsPred :: IsExprBuilder sym => sym -> Assumptions sym -> IO (Pred sym) Source #
Compute the logical predicate corresponding to this collection of assumptions.
flattenAssumptions :: IsExprBuilder sym => sym -> Assumptions sym -> IO [Assumption sym] Source #
Given a CrucibleAssumptions structure, flatten all the muxed assumptions into
a flat sequence of assumptions that have been appropriately weakened.
Note, once these assumptions have been flattened, their order might no longer
strictly correspond to any concrete program run.
assumptionsTopLevelLocs :: CrucibleAssumptions e -> [ProgramLoc] Source #
Collect the program locations of all assumptions and
events that did not occur in the context of a symbolic branch.
These are locations that every program path represented by
this CrucibleAssumptions structure must have passed through.
type ProofObligation sym = ProofGoal (Assumptions sym) (Assertion sym) Source #
type ProofObligations sym = Maybe (Goals (Assumptions sym) (Assertion sym)) Source #
type AssumptionState sym = GoalCollector (Assumptions sym) (Assertion sym) Source #
assert :: IsSymBackend sym bak => bak -> Pred sym -> SimErrorReason -> IO () Source #
Add a proof obligation using the current program location. Afterwards, assume the given fact.
Reexports
data LabeledPred pred msg #
Information about an assertion that was previously made.
Constructors
| LabeledPred | |
Fields
| |
Instances
| Bifoldable LabeledPred | |
Defined in What4.LabeledPred Methods bifold :: Monoid m => LabeledPred m m -> m # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> LabeledPred a b -> m # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> LabeledPred a b -> c # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> LabeledPred a b -> c # | |
| Bifunctor LabeledPred | |
Defined in What4.LabeledPred Methods bimap :: (a -> b) -> (c -> d) -> LabeledPred a c -> LabeledPred b d # first :: (a -> b) -> LabeledPred a c -> LabeledPred b c # second :: (b -> c) -> LabeledPred a b -> LabeledPred a c # | |
| Bitraversable LabeledPred | |
Defined in What4.LabeledPred Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> LabeledPred a b -> f (LabeledPred c d) # | |
| Eq2 LabeledPred | |
Defined in What4.LabeledPred Methods liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> LabeledPred a c -> LabeledPred b d -> Bool # | |
| Ord2 LabeledPred | |
Defined in What4.LabeledPred Methods liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> LabeledPred a c -> LabeledPred b d -> Ordering # | |
| Show2 LabeledPred | |
Defined in What4.LabeledPred | |
| Generic1 (LabeledPred pred :: Type -> Type) | |
Defined in What4.LabeledPred Associated Types type Rep1 (LabeledPred pred) :: k -> Type # Methods from1 :: forall (a :: k). LabeledPred pred a -> Rep1 (LabeledPred pred) a # to1 :: forall (a :: k). Rep1 (LabeledPred pred) a -> LabeledPred pred a # | |
| Foldable (LabeledPred pred) | |
Defined in What4.LabeledPred Methods fold :: Monoid m => LabeledPred pred m -> m # foldMap :: Monoid m => (a -> m) -> LabeledPred pred a -> m # foldMap' :: Monoid m => (a -> m) -> LabeledPred pred a -> m # foldr :: (a -> b -> b) -> b -> LabeledPred pred a -> b # foldr' :: (a -> b -> b) -> b -> LabeledPred pred a -> b # foldl :: (b -> a -> b) -> b -> LabeledPred pred a -> b # foldl' :: (b -> a -> b) -> b -> LabeledPred pred a -> b # foldr1 :: (a -> a -> a) -> LabeledPred pred a -> a # foldl1 :: (a -> a -> a) -> LabeledPred pred a -> a # toList :: LabeledPred pred a -> [a] # null :: LabeledPred pred a -> Bool # length :: LabeledPred pred a -> Int # elem :: Eq a => a -> LabeledPred pred a -> Bool # maximum :: Ord a => LabeledPred pred a -> a # minimum :: Ord a => LabeledPred pred a -> a # sum :: Num a => LabeledPred pred a -> a # product :: Num a => LabeledPred pred a -> a # | |
| Eq pred => Eq1 (LabeledPred pred) | |
Defined in What4.LabeledPred Methods liftEq :: (a -> b -> Bool) -> LabeledPred pred a -> LabeledPred pred b -> Bool # | |
| Ord pred => Ord1 (LabeledPred pred) | |
Defined in What4.LabeledPred Methods liftCompare :: (a -> b -> Ordering) -> LabeledPred pred a -> LabeledPred pred b -> Ordering # | |
| Show pred => Show1 (LabeledPred pred) | |
Defined in What4.LabeledPred Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> LabeledPred pred a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [LabeledPred pred a] -> ShowS # | |
| Traversable (LabeledPred pred) | |
Defined in What4.LabeledPred Methods traverse :: Applicative f => (a -> f b) -> LabeledPred pred a -> f (LabeledPred pred b) # sequenceA :: Applicative f => LabeledPred pred (f a) -> f (LabeledPred pred a) # mapM :: Monad m => (a -> m b) -> LabeledPred pred a -> m (LabeledPred pred b) # sequence :: Monad m => LabeledPred pred (m a) -> m (LabeledPred pred a) # | |
| Functor (LabeledPred pred) | |
Defined in What4.LabeledPred Methods fmap :: (a -> b) -> LabeledPred pred a -> LabeledPred pred b # (<$) :: a -> LabeledPred pred b -> LabeledPred pred a # | |
| (Data pred, Data msg) => Data (LabeledPred pred msg) | |
Defined in What4.LabeledPred Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LabeledPred pred msg -> c (LabeledPred pred msg) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LabeledPred pred msg) # toConstr :: LabeledPred pred msg -> Constr # dataTypeOf :: LabeledPred pred msg -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LabeledPred pred msg)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LabeledPred pred msg)) # gmapT :: (forall b. Data b => b -> b) -> LabeledPred pred msg -> LabeledPred pred msg # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r # gmapQ :: (forall d. Data d => d -> u) -> LabeledPred pred msg -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LabeledPred pred msg -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LabeledPred pred msg -> m (LabeledPred pred msg) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LabeledPred pred msg -> m (LabeledPred pred msg) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LabeledPred pred msg -> m (LabeledPred pred msg) # | |
| Generic (LabeledPred pred msg) | |
Defined in What4.LabeledPred Associated Types type Rep (LabeledPred pred msg) :: Type -> Type # Methods from :: LabeledPred pred msg -> Rep (LabeledPred pred msg) x # to :: Rep (LabeledPred pred msg) x -> LabeledPred pred msg # | |
| (Show pred, Show msg) => Show (LabeledPred pred msg) | |
Defined in What4.LabeledPred Methods showsPrec :: Int -> LabeledPred pred msg -> ShowS # show :: LabeledPred pred msg -> String # showList :: [LabeledPred pred msg] -> ShowS # | |
| (Eq pred, Eq msg) => Eq (LabeledPred pred msg) | |
Defined in What4.LabeledPred Methods (==) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool # (/=) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool # | |
| (Ord pred, Ord msg) => Ord (LabeledPred pred msg) | |
Defined in What4.LabeledPred Methods compare :: LabeledPred pred msg -> LabeledPred pred msg -> Ordering # (<) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool # (<=) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool # (>) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool # (>=) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool # max :: LabeledPred pred msg -> LabeledPred pred msg -> LabeledPred pred msg # min :: LabeledPred pred msg -> LabeledPred pred msg -> LabeledPred pred msg # | |
| type Rep1 (LabeledPred pred :: Type -> Type) | |
Defined in What4.LabeledPred type Rep1 (LabeledPred pred :: Type -> Type) = D1 ('MetaData "LabeledPred" "What4.LabeledPred" "what4-1.5.1-6GimHtONvd1LMJIg4FyjIh" 'False) (C1 ('MetaCons "LabeledPred" 'PrefixI 'True) (S1 ('MetaSel ('Just "_labeledPred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 pred) :*: S1 ('MetaSel ('Just "_labeledPredMsg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) Par1)) | |
| type Rep (LabeledPred pred msg) | |
Defined in What4.LabeledPred type Rep (LabeledPred pred msg) = D1 ('MetaData "LabeledPred" "What4.LabeledPred" "what4-1.5.1-6GimHtONvd1LMJIg4FyjIh" 'False) (C1 ('MetaCons "LabeledPred" 'PrefixI 'True) (S1 ('MetaSel ('Just "_labeledPred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 pred) :*: S1 ('MetaSel ('Just "_labeledPredMsg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 msg))) | |
labeledPred :: forall pred msg pred' f. Functor f => (pred -> f pred') -> LabeledPred pred msg -> f (LabeledPred pred' msg) #
Predicate that was asserted.
labeledPredMsg :: forall pred msg msg' f. Functor f => (msg -> f msg') -> LabeledPred pred msg -> f (LabeledPred pred msg') #
Message added when assumption/assertion was made.
data AssumptionStack asmp ast Source #
An assumption stack is a data structure for tracking logical assumptions and proof obligations. Assumptions can be added to the current stack frame, and stack frames may be pushed (to remember a previous state) or popped to restore a previous state.
data FrameIdentifier Source #
A FrameIdentifier is a value that identifies an
an assumption frame. These are expected to be unique
when a new frame is pushed onto the stack. This is
primarily a debugging aid, to ensure that stack management
remains well-bracketed.
Instances
| Eq FrameIdentifier Source # | |
Defined in Lang.Crucible.Backend.ProofGoals Methods (==) :: FrameIdentifier -> FrameIdentifier -> Bool # (/=) :: FrameIdentifier -> FrameIdentifier -> Bool # | |
| Ord FrameIdentifier Source # | |
Defined in Lang.Crucible.Backend.ProofGoals Methods compare :: FrameIdentifier -> FrameIdentifier -> Ordering # (<) :: FrameIdentifier -> FrameIdentifier -> Bool # (<=) :: FrameIdentifier -> FrameIdentifier -> Bool # (>) :: FrameIdentifier -> FrameIdentifier -> Bool # (>=) :: FrameIdentifier -> FrameIdentifier -> Bool # max :: FrameIdentifier -> FrameIdentifier -> FrameIdentifier # min :: FrameIdentifier -> FrameIdentifier -> FrameIdentifier # | |
data ProofGoal asmp goal Source #
A proof goal consists of a collection of assumptions that were in scope when an assertion was made, together with the given assertion.
Constructors
| ProofGoal | |
Fields
| |
A collection of goals, which can represent shared assumptions.
goalsToList :: Monoid asmp => Goals asmp goal -> [ProofGoal asmp goal] Source #
Render the tree of goals as a list instead, duplicating shared assumptions over each goal as necessary.
Aborting execution
data AbortExecReason Source #
This is used to signal that current execution path is infeasible.
Constructors
| InfeasibleBranch ProgramLoc | We have discovered that the currently-executing branch is infeasible. The given program location describes the point at which infeasibility was discovered. |
| AssertionFailure SimError | An assertion concretely failed. |
| VariantOptionsExhausted ProgramLoc | We tried all possible cases for a variant, and now we should do something else. |
| EarlyExit ProgramLoc | We invoked a function which ends the current thread of execution
(e.g., |
Instances
| Exception AbortExecReason Source # | |
Defined in Lang.Crucible.Backend Methods toException :: AbortExecReason -> SomeException # | |
| Show AbortExecReason Source # | |
Defined in Lang.Crucible.Backend Methods showsPrec :: Int -> AbortExecReason -> ShowS # show :: AbortExecReason -> String # showList :: [AbortExecReason] -> ShowS # | |
abortExecBecause :: AbortExecReason -> IO a Source #
Throw an exception, thus aborting the current execution path.
ppAbortExecReason :: AbortExecReason -> Doc ann Source #
Utilities
throwUnsupported :: (IsExprBuilder sym, MonadIO m, HasCallStack) => sym -> String -> m a Source #
addAssertion :: IsSymBackend sym bak => bak -> Assertion sym -> IO () Source #
Add a proof obligation for the given predicate, and then assume it (when the assertThenAssume option is true). Note that assuming the prediate might cause the current execution path to abort, if we happened to assume something that is obviously false.
addDurableAssertion :: IsSymBackend sym bak => bak -> Assertion sym -> IO () Source #
Add a durable proof obligation for the given predicate, and then assume it (when the assertThenAssume option is true). Note that assuming the prediate might cause the current execution path to abort, if we happened to assume something that is obviously false.
addAssertionM :: IsSymBackend sym bak => bak -> IO (Pred sym) -> SimErrorReason -> IO () Source #
Run the given action to compute a predicate, and assert it.
addFailedAssertion :: IsSymBackend sym bak => bak -> SimErrorReason -> IO a Source #
Add a proof obligation for False. This always aborts execution of the current path, because after asserting false, we get to assume it, and so there is no need to check anything after. This is why the resulting IO computation can have the fully polymorphic type.
assertIsInteger :: IsSymBackend sym bak => bak -> SymReal sym -> SimErrorReason -> IO () Source #
Assert that the given real-valued expression is an integer.
readPartExpr :: IsSymBackend sym bak => bak -> PartExpr (Pred sym) v -> SimErrorReason -> IO v Source #
Given a partial expression, assert that it is defined and return the underlying value.
ppProofObligation :: IsExprBuilder sym => sym -> ProofObligation sym -> IO (Doc ann) Source #
backendOptions :: [ConfigDesc] Source #