Crux.Goal

Documentation

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)

Simplify the proved goals.

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)

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)))

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)))

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.

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

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)))

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

Like inNewFrame, but specifically for frame 2. This is used for the purpose of generating abducts.

data SMTResult sym

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]