| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Crux.Goal
Synopsis
- symCfg :: (IsExprBuilder sym, Opt t a) => sym -> ConfigOption t -> a -> IO ()
- provedGoalsTree :: forall sym. IsSymInterface sym => sym -> Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)) -> IO (Maybe ProvedGoals)
- proveToGoal :: IsSymInterface sym => sym -> Assumptions sym -> Assertion sym -> [ProgramLoc] -> ProofResult sym -> IO ProvedGoals
- countGoals :: Goals a b -> Int
- isResourceExhausted :: LabeledPred p SimError -> Bool
- updateProcessedGoals :: LabeledPred p SimError -> ProofResult a -> ProcessedGoals -> ProcessedGoals
- type Explainer sym t ann = Maybe (GroundEvalFn t) -> LPred sym SimError -> IO (Doc ann)
- type ProverCallback sym = forall ext personality t st fs. sym ~ ExprBuilder t st fs => CruxOptions -> SimCtxt personality sym ext -> Explainer sym t Void -> Maybe (Goals (Assumptions sym) (Assertion sym)) -> IO (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)))
- proveGoalsOffline :: forall st sym p t fs personality msgs. (sym ~ ExprBuilder t st fs, Logs msgs, SupportsCruxLogMessage msgs) => [SolverAdapter st] -> CruxOptions -> SimCtxt personality sym p -> (Maybe (GroundEvalFn t) -> Assertion sym -> IO (Doc Void)) -> Maybe (Goals (Assumptions sym) (Assertion sym)) -> IO (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)))
- evalModelFromEvents :: [CrucibleEvent GroundValueWrapper] -> ModelView
- dispatchSolversOnGoalAsync :: forall a b s time. RealFrac time => Maybe time -> [SolverAdapter s] -> (SolverAdapter s -> IO (b, ProofResult a)) -> IO (Either [SomeException] (Maybe (b, ProofResult a)))
- proverMilestoneCallbacks :: Logs msgs => SupportsCruxLogMessage msgs => Goals asmp ast -> IO ProverMilestoneCallbacks
- proveGoalsOnline :: forall sym personality p msgs goalSolver s st fs. (sym ~ ExprBuilder s st fs, OnlineSolver goalSolver, Logs msgs, SupportsCruxLogMessage msgs) => OnlineBackend goalSolver s st fs -> CruxOptions -> SimCtxt personality sym p -> (Maybe (GroundEvalFn s) -> Assertion sym -> IO (Doc Void)) -> Maybe (Goals (Assumptions sym) (Assertion sym)) -> IO (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)))
- inNewFrame2 :: SMTReadWriter solver => SolverProcess scope solver -> IO a -> IO a
- data SMTResult sym
- = UnsatResult [Either (Assumption sym) (Assertion sym)] [ProgramLoc]
- | SatResult (Doc Void) [CrucibleEvent GroundValueWrapper]
- | UnknownResult (Doc Void) [ProgramLoc]
Documentation
symCfg :: (IsExprBuilder sym, Opt t a) => sym -> ConfigOption t -> a -> IO () Source #
provedGoalsTree :: forall sym. IsSymInterface sym => sym -> Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)) -> IO (Maybe ProvedGoals) Source #
Simplify the proved goals.
proveToGoal :: IsSymInterface sym => sym -> Assumptions sym -> Assertion sym -> [ProgramLoc] -> ProofResult sym -> IO ProvedGoals Source #
countGoals :: Goals a b -> Int Source #
isResourceExhausted :: LabeledPred p SimError -> Bool Source #
updateProcessedGoals :: LabeledPred p SimError -> ProofResult a -> ProcessedGoals -> ProcessedGoals Source #
type Explainer sym t ann = Maybe (GroundEvalFn t) -> LPred sym SimError -> IO (Doc ann) Source #
A function that can be used to generate a pretty explanation of a simulation error.
type ProverCallback sym = forall ext personality t st fs. sym ~ ExprBuilder t st fs => CruxOptions -> SimCtxt personality sym ext -> Explainer sym t Void -> Maybe (Goals (Assumptions sym) (Assertion sym)) -> IO (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) Source #
proveGoalsOffline :: forall st sym p t fs personality msgs. (sym ~ ExprBuilder t st fs, Logs msgs, SupportsCruxLogMessage msgs) => [SolverAdapter st] -> CruxOptions -> SimCtxt personality sym p -> (Maybe (GroundEvalFn t) -> Assertion sym -> IO (Doc Void)) -> Maybe (Goals (Assumptions sym) (Assertion sym)) -> IO (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) Source #
Discharge a tree of proof obligations (Goals) by using a non-online solver
This function traverses the Goals tree while keeping track of a collection
of assumptions in scope for each goal. For each proof goal encountered in
the tree, it creates a fresh solver connection using the provided solver
adapter.
This is in contrast to proveGoalsOnline, which uses an online solver
connection with scoped assumption frames. This function allows using a wider
variety of solvers (i.e., ones that don't have support for online solving)
and would in principle enable parallel goal evaluation (though the tree
structure makes that a bit trickier, it isn't too hard).
Note that this function uses the same symbolic backend (ExprBuilder) as the
symbolic execution phase, which should not be a problem.
dispatchSolversOnGoalAsync :: forall a b s time. RealFrac time => Maybe time -> [SolverAdapter s] -> (SolverAdapter s -> IO (b, ProofResult a)) -> IO (Either [SomeException] (Maybe (b, ProofResult a))) Source #
proverMilestoneCallbacks :: Logs msgs => SupportsCruxLogMessage msgs => Goals asmp ast -> IO ProverMilestoneCallbacks Source #
Returns three actions, called respectively when the proving process for a goal is started, when it is ended, and when the final goal is solved. These handlers should handle all necessary output / notifications to external observers, based on the run options.
proveGoalsOnline :: forall sym personality p msgs goalSolver s st fs. (sym ~ ExprBuilder s st fs, OnlineSolver goalSolver, Logs msgs, SupportsCruxLogMessage msgs) => OnlineBackend goalSolver s st fs -> CruxOptions -> SimCtxt personality sym p -> (Maybe (GroundEvalFn s) -> Assertion sym -> IO (Doc Void)) -> Maybe (Goals (Assumptions sym) (Assertion sym)) -> IO (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) Source #
Prove a collection of goals. The result is a goal tree, where each goal is annotated with the outcome of the proof.
NOTE: This function takes an explicit symbolic backend as an argument, even
though the symbolic backend used for symbolic execution is available in the
SimCtxt. We do that so that we can use separate solvers for path
satisfiability checking and goal discharge.
inNewFrame2 :: SMTReadWriter solver => SolverProcess scope solver -> IO a -> IO a Source #
Like inNewFrame, but specifically for frame 2. This is used for the
purpose of generating abducts.
An intermediate data structure used in proveGoalsOnline. This can be
thought of as a halfway point between a SMTResult and a ProofResult.
Constructors
| UnsatResult [Either (Assumption sym) (Assertion sym)] [ProgramLoc] | |
| SatResult (Doc Void) [CrucibleEvent GroundValueWrapper] | |
| UnknownResult (Doc Void) [ProgramLoc] |