| Copyright | (c) Galois Inc 2015-2016 |
|---|---|
| License | BSD3 |
| Maintainer | Ryan Scott <rscott@galois.com>, Langston Barrett <langston@galois.com> |
| Stability | provisional |
| Safe Haskell | None |
| Language | Haskell2010 |
Lang.Crucible.Backend.Online
Description
A solver backend (IsSymBackend) that maintains an open connection to an
SMT solver (in contrast to Lang.Crucible.Backend.Simple).
The primary intended use-case is to prune unsatisfiable execution
traces during simulation using the execution feature provided by
Lang.Crucible.Simulator.PathSatisfiability. That execution feature is
parameterized over a function argument that can be instantiated with this
module's considerSatisfiability.
The online backend also allows override definitions access to a persistent SMT solver connection. This can be useful for some kinds of algorithms that benefit from quickly performing many small solver queries in a tight interaction loop.
The online backend is not currently used to dispatch proof obligations during symbolic execution, see GaloisInc/crucible#369, "Interleave proof with simulation".
Synopsis
- solverInteractionFile :: ConfigOption (BaseStringType Unicode)
- enableOnlineBackend :: ConfigOption BaseBoolType
- onlineBackendOptions :: forall solver scope (st :: Type -> Type) fs. OnlineSolver solver => OnlineBackend solver scope st fs -> [ConfigDesc]
- data OnlineBackend solver scope (st :: Type -> Type) fs
- withOnlineBackend :: forall solver m scope (st :: Type -> Type) fs a. (OnlineSolver solver, MonadIO m, MonadMask m) => ExprBuilder scope st fs -> ProblemFeatures -> (OnlineBackend solver scope st fs -> m a) -> m a
- newOnlineBackend :: forall solver scope (st :: Type -> Type) fs. OnlineSolver solver => ExprBuilder scope st fs -> ProblemFeatures -> IO (OnlineBackend solver scope st fs)
- checkSatisfiable :: SMTReadWriter solver => SolverProcess scope solver -> String -> BoolExpr scope -> IO (SatResult () ())
- checkSatisfiableWithModel :: SMTReadWriter solver => SolverProcess scope solver -> String -> BoolExpr scope -> (SatResult (GroundEvalFn scope) () -> IO a) -> IO a
- withSolverProcess :: forall solver scope (st :: Type -> Type) fs a. OnlineSolver solver => OnlineBackend solver scope st fs -> IO a -> (SolverProcess scope solver -> IO a) -> IO a
- resetSolverProcess :: forall solver scope (st :: Type -> Type) fs. OnlineSolver solver => OnlineBackend solver scope st fs -> IO ()
- restoreSolverState :: forall solver scope (st :: Type -> Type) fs. OnlineSolver solver => OnlineBackend solver scope st fs -> GoalCollector (CrucibleAssumptions (Expr scope)) (LabeledPred (BoolExpr scope) SimError) -> IO ()
- data UnsatFeatures
- unsatFeaturesToProblemFeatures :: UnsatFeatures -> ProblemFeatures
- data BranchResult
- considerSatisfiability :: forall solver scope (st :: Type -> Type) fs. OnlineSolver solver => OnlineBackend solver scope st fs -> Maybe ProgramLoc -> BoolExpr scope -> IO BranchResult
- type YicesOnlineBackend scope (st :: Type -> Type) fs = OnlineBackend Connection scope st fs
- withYicesOnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (YicesOnlineBackend scope st fs -> m a) -> m a
- type Z3OnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer Z3) scope st fs
- withZ3OnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (Z3OnlineBackend scope st fs -> m a) -> m a
- type BitwuzlaOnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer Bitwuzla) scope st fs
- withBitwuzlaOnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (BitwuzlaOnlineBackend scope st fs -> m a) -> m a
- type BoolectorOnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer Boolector) scope st fs
- withBoolectorOnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> (BoolectorOnlineBackend scope st fs -> m a) -> m a
- type CVC4OnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer CVC4) scope st fs
- withCVC4OnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (CVC4OnlineBackend scope st fs -> m a) -> m a
- type CVC5OnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer CVC5) scope st fs
- withCVC5OnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (CVC5OnlineBackend scope st fs -> m a) -> m a
- type STPOnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer STP) scope st fs
- withSTPOnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> (STPOnlineBackend scope st fs -> m a) -> m a
Configuration options
enableOnlineBackend :: ConfigOption BaseBoolType Source #
Option for enabling online solver interactions. Defaults to true. If disabled, operations requiring solver connections will be skipped.
onlineBackendOptions :: forall solver scope (st :: Type -> Type) fs. OnlineSolver solver => OnlineBackend solver scope st fs -> [ConfigDesc] Source #
OnlineBackend
data OnlineBackend solver scope (st :: Type -> Type) fs Source #
This represents the state of the backend along a given execution. It contains the current assertions and program location.
Instances
withOnlineBackend :: forall solver m scope (st :: Type -> Type) fs a. (OnlineSolver solver, MonadIO m, MonadMask m) => ExprBuilder scope st fs -> ProblemFeatures -> (OnlineBackend solver scope st fs -> m a) -> m a Source #
Do something with an online backend. The backend is only valid in the continuation.
Solver specific configuration options are not automatically installed by this operation.
newOnlineBackend :: forall solver scope (st :: Type -> Type) fs. OnlineSolver solver => ExprBuilder scope st fs -> ProblemFeatures -> IO (OnlineBackend solver scope st fs) Source #
checkSatisfiable :: SMTReadWriter solver => SolverProcess scope solver -> String -> BoolExpr scope -> IO (SatResult () ()) #
Check if the given formula is satisfiable in the current solver state, without requesting a model. This is done in a fresh frame, which is exited after the check call.
checkSatisfiableWithModel :: SMTReadWriter solver => SolverProcess scope solver -> String -> BoolExpr scope -> (SatResult (GroundEvalFn scope) () -> IO a) -> IO a #
Check if the formula is satisifiable in the current solver state. This is done in a fresh frame, which is exited after the continuation complets. The evaluation function can be used to query the model. The model is valid only in the given continuation.
Arguments
| :: forall solver scope (st :: Type -> Type) fs a. OnlineSolver solver | |
| => OnlineBackend solver scope st fs | |
| -> IO a | Default value to return if online features are disabled |
| -> (SolverProcess scope solver -> IO a) | |
| -> IO a |
Get the solver process. Starts the solver, if that hasn't
happened already and apply the given action.
If the enableOnlineBackend option is False, the action
is skipped instead, and the solver is not started.
resetSolverProcess :: forall solver scope (st :: Type -> Type) fs. OnlineSolver solver => OnlineBackend solver scope st fs -> IO () Source #
Shutdown any currently-active solver process.
A fresh solver process will be started on the
next call to getSolverProcess.
restoreSolverState :: forall solver scope (st :: Type -> Type) fs. OnlineSolver solver => OnlineBackend solver scope st fs -> GoalCollector (CrucibleAssumptions (Expr scope)) (LabeledPred (BoolExpr scope) SimError) -> IO () Source #
data UnsatFeatures Source #
Constructors
| NoUnsatFeatures | Do not compute unsat cores or assumptions |
| ProduceUnsatCores | Enable named assumptions and unsat-core computations |
| ProduceUnsatAssumptions | Enable check-with-assumptions commands and unsat-assumptions computations |
Branch satisfiability
data BranchResult Source #
Result of attempting to branch on a predicate.
Constructors
| IndeterminateBranchResult | The both branches of the predicate might be satisfiable (although satisfiablility of either branch is not guaranteed). |
| NoBranch !Bool | Commit to the branch where the given predicate is equal to the returned boolean. The opposite branch is unsatisfiable (although the given branch is not necessarily satisfiable). |
| UnsatisfiableContext | The context before considering the given predicate was already unsatisfiable. |
Instances
considerSatisfiability :: forall solver scope (st :: Type -> Type) fs. OnlineSolver solver => OnlineBackend solver scope st fs -> Maybe ProgramLoc -> BoolExpr scope -> IO BranchResult Source #
Backends for different solvers
Yices
type YicesOnlineBackend scope (st :: Type -> Type) fs = OnlineBackend Connection scope st fs Source #
withYicesOnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (YicesOnlineBackend scope st fs -> m a) -> m a Source #
Do something with a Yices online backend. The backend is only valid in the continuation.
The Yices configuration options will be automatically installed into the backend configuration object.
Z3
type Z3OnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer Z3) scope st fs Source #
withZ3OnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (Z3OnlineBackend scope st fs -> m a) -> m a Source #
Do something with a Z3 online backend. The backend is only valid in the continuation.
The Z3 configuration options will be automatically installed into the backend configuration object.
Bitwuzla
type BitwuzlaOnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer Bitwuzla) scope st fs Source #
withBitwuzlaOnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (BitwuzlaOnlineBackend scope st fs -> m a) -> m a Source #
Do something with a Bitwuzla online backend. The backend is only valid in the continuation.
The Bitwuzla configuration options will be automatically installed into the backend configuration object.
Boolector
type BoolectorOnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer Boolector) scope st fs Source #
withBoolectorOnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> (BoolectorOnlineBackend scope st fs -> m a) -> m a Source #
Do something with a Boolector online backend. The backend is only valid in the continuation.
The Boolector configuration options will be automatically installed into the backend configuration object.
CVC4
type CVC4OnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer CVC4) scope st fs Source #
withCVC4OnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (CVC4OnlineBackend scope st fs -> m a) -> m a Source #
Do something with a CVC4 online backend. The backend is only valid in the continuation.
The CVC4 configuration options will be automatically installed into the backend configuration object.
CVC5
type CVC5OnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer CVC5) scope st fs Source #
withCVC5OnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (CVC5OnlineBackend scope st fs -> m a) -> m a Source #
Do something with a CVC5 online backend. The backend is only valid in the continuation.
The CVC5 configuration options will be automatically installed into the backend configuration object.
STP
type STPOnlineBackend scope (st :: Type -> Type) fs = OnlineBackend (Writer STP) scope st fs Source #
withSTPOnlineBackend :: forall m scope (st :: Type -> Type) fs a. (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> (STPOnlineBackend scope st fs -> m a) -> m a Source #
Do something with a STP online backend. The backend is only valid in the continuation.
The STO configuration options will be automatically installed into the backend configuration object.