Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
.
UnsatResult [Either (Assumption sym) (Assertion sym)] [ProgramLoc] | |
SatResult (Doc Void) [CrucibleEvent GroundValueWrapper] | |
UnknownResult (Doc Void) [ProgramLoc] |