Copyright	(c) Galois Inc 2015-2016
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Stability	provisional
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Backend.Online

Contents

OnlineBackend

Description

The online backend maintains an open connection to an SMT solver that is used to prune unsatisfiable execution traces during simulation. At every symbolic branch point, the SMT solver is queried to determine if one or both symbolic branches are unsatisfiable. Only branches with satisfiable branch conditions are explored.

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.

Synopsis

data OnlineBackend solver scope st fs
withOnlineBackend :: (OnlineSolver solver, MonadIO m, MonadMask m) => ExprBuilder scope st fs -> ProblemFeatures -> (OnlineBackend solver scope st fs -> m a) -> m a
newOnlineBackend :: 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 :: OnlineSolver solver => OnlineBackend solver scope st fs -> IO a -> (SolverProcess scope solver -> IO a) -> IO a
resetSolverProcess :: OnlineSolver solver => OnlineBackend solver scope st fs -> IO ()
restoreSolverState :: OnlineSolver solver => OnlineBackend solver scope st fs -> GoalCollector (CrucibleAssumptions (Expr scope)) (LabeledPred (BoolExpr scope) SimError) -> IO ()
data UnsatFeatures
- = NoUnsatFeatures
- | ProduceUnsatCores
- | ProduceUnsatAssumptions
unsatFeaturesToProblemFeatures :: UnsatFeatures -> ProblemFeatures
solverInteractionFile :: ConfigOption (BaseStringType Unicode)
enableOnlineBackend :: ConfigOption BaseBoolType
onlineBackendOptions :: OnlineSolver solver => OnlineBackend solver scope st fs -> [ConfigDesc]
data BranchResult
- = IndeterminateBranchResult
- | NoBranch !Bool
- | UnsatisfiableContext
considerSatisfiability :: OnlineSolver solver => OnlineBackend solver scope st fs -> Maybe ProgramLoc -> BoolExpr scope -> IO BranchResult
type YicesOnlineBackend scope st fs = OnlineBackend Connection scope st fs
withYicesOnlineBackend :: (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (YicesOnlineBackend scope st fs -> m a) -> m a
type Z3OnlineBackend scope st fs = OnlineBackend (Writer Z3) scope st fs
withZ3OnlineBackend :: (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (Z3OnlineBackend scope st fs -> m a) -> m a
type BoolectorOnlineBackend scope st fs = OnlineBackend (Writer Boolector) scope st fs
withBoolectorOnlineBackend :: (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> (BoolectorOnlineBackend scope st fs -> m a) -> m a
type CVC4OnlineBackend scope st fs = OnlineBackend (Writer CVC4) scope st fs
withCVC4OnlineBackend :: (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (CVC4OnlineBackend scope st fs -> m a) -> m a
type CVC5OnlineBackend scope st fs = OnlineBackend (Writer CVC5) scope st fs
withCVC5OnlineBackend :: (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> UnsatFeatures -> ProblemFeatures -> (CVC5OnlineBackend scope st fs -> m a) -> m a
type STPOnlineBackend scope st fs = OnlineBackend (Writer STP) scope st fs
withSTPOnlineBackend :: (MonadIO m, MonadMask m) => ExprBuilder scope st fs -> (STPOnlineBackend scope st fs -> m a) -> m a

OnlineBackend

data OnlineBackend solver scope st fs Source #

This represents the state of the backend along a given execution. It contains the current assertions and program location.

Instances

Instances details

HasSymInterface (ExprBuilder t st fs) (OnlineBackend solver t st fs) Source #
Instance details Defined in Lang.Crucible.Backend.Online Methods backendGetSym :: OnlineBackend solver t st fs -> ExprBuilder t st fs Source #
(IsSymInterface (ExprBuilder scope st fs), OnlineSolver solver) => IsSymBackend (ExprBuilder scope st fs) (OnlineBackend solver scope st fs) Source #
Instance details Defined in Lang.Crucible.Backend.Online Methods pushAssumptionFrame :: OnlineBackend solver scope st fs -> IO FrameIdentifier Source # popAssumptionFrame :: OnlineBackend solver scope st fs -> FrameIdentifier -> IO (Assumptions (ExprBuilder scope st fs)) Source # popUntilAssumptionFrame :: OnlineBackend solver scope st fs -> FrameIdentifier -> IO () Source # popAssumptionFrameAndObligations :: OnlineBackend solver scope st fs -> FrameIdentifier -> IO (Assumptions (ExprBuilder scope st fs), ProofObligations (ExprBuilder scope st fs)) Source # addAssumption :: OnlineBackend solver scope st fs -> Assumption (ExprBuilder scope st fs) -> IO () Source # addAssumptions :: OnlineBackend solver scope st fs -> Assumptions (ExprBuilder scope st fs) -> IO () Source # getPathCondition :: OnlineBackend solver scope st fs -> IO (Pred (ExprBuilder scope st fs)) Source # collectAssumptions :: OnlineBackend solver scope st fs -> IO (Assumptions (ExprBuilder scope st fs)) Source # addProofObligation :: OnlineBackend solver scope st fs -> Assertion (ExprBuilder scope st fs) -> IO () Source # addDurableProofObligation :: OnlineBackend solver scope st fs -> Assertion (ExprBuilder scope st fs) -> IO () Source # getProofObligations :: OnlineBackend solver scope st fs -> IO (ProofObligations (ExprBuilder scope st fs)) Source # clearProofObligations :: OnlineBackend solver scope st fs -> IO () Source # saveAssumptionState :: OnlineBackend solver scope st fs -> IO (AssumptionState (ExprBuilder scope st fs)) Source # restoreAssumptionState :: OnlineBackend solver scope st fs -> AssumptionState (ExprBuilder scope st fs) -> IO () Source # resetAssumptionState :: OnlineBackend solver scope st fs -> IO () Source #

withOnlineBackend :: (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 :: 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.

withSolverProcess Source #

Arguments

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

unsatFeaturesToProblemFeatures :: UnsatFeatures -> ProblemFeatures Source #

Configuration options

solverInteractionFile :: ConfigOption (BaseStringType Unicode) Source #

enableOnlineBackend :: ConfigOption BaseBoolType Source #

Option for enabling online solver interactions. Defaults to true. If disabled, operations requiring solver connections will be skipped.

onlineBackendOptions :: OnlineSolver solver => OnlineBackend solver scope st fs -> [ConfigDesc] Source #

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

Instances details

Data BranchResult Source #
Instance details Defined in Lang.Crucible.Backend.Online Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BranchResult -> c BranchResult # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BranchResult # toConstr :: BranchResult -> Constr # dataTypeOf :: BranchResult -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BranchResult) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BranchResult) # gmapT :: (forall b. Data b => b -> b) -> BranchResult -> BranchResult # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BranchResult -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BranchResult -> r # gmapQ :: (forall d. Data d => d -> u) -> BranchResult -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BranchResult -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult #
Generic BranchResult Source #
Instance details Defined in Lang.Crucible.Backend.Online Associated Types type Rep BranchResult :: Type -> Type # Methods from :: BranchResult -> Rep BranchResult x # to :: Rep BranchResult x -> BranchResult #
Eq BranchResult Source #
Instance details Defined in Lang.Crucible.Backend.Online Methods (==) :: BranchResult -> BranchResult -> Bool # (/=) :: BranchResult -> BranchResult -> Bool #
Ord BranchResult Source #
Instance details Defined in Lang.Crucible.Backend.Online Methods compare :: BranchResult -> BranchResult -> Ordering # (<) :: BranchResult -> BranchResult -> Bool # (<=) :: BranchResult -> BranchResult -> Bool # (>) :: BranchResult -> BranchResult -> Bool # (>=) :: BranchResult -> BranchResult -> Bool # max :: BranchResult -> BranchResult -> BranchResult # min :: BranchResult -> BranchResult -> BranchResult #
type Rep BranchResult Source #
Instance details Defined in Lang.Crucible.Backend.Online type Rep BranchResult = D1 ('MetaData "BranchResult" "Lang.Crucible.Backend.Online" "crucible-0.7.1-BXyoRZbWPko2UikbrJsa4O" 'False) (C1 ('MetaCons "IndeterminateBranchResult" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NoBranch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)) :+: C1 ('MetaCons "UnsatisfiableContext" 'PrefixI 'False) (U1 :: Type -> Type)))

considerSatisfiability :: OnlineSolver solver => OnlineBackend solver scope st fs -> Maybe ProgramLoc -> BoolExpr scope -> IO BranchResult Source #

Yices

type YicesOnlineBackend scope st fs = OnlineBackend Connection scope st fs Source #

withYicesOnlineBackend :: (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.

n.b. the explicit forall allows the fs to be expressed as the first argument so that it can be dictated easily from the caller. Example:

withYicesOnlineBackend FloatRealRepr ng f'

Z3

type Z3OnlineBackend scope st fs = OnlineBackend (Writer Z3) scope st fs Source #

withZ3OnlineBackend :: (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.

n.b. the explicit forall allows the fs to be expressed as the first argument so that it can be dictated easily from the caller. Example:

withz3OnlineBackend FloatRealRepr ng f'

Boolector

type BoolectorOnlineBackend scope st fs = OnlineBackend (Writer Boolector) scope st fs Source #

withBoolectorOnlineBackend :: (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.

withBoolectorOnineBackend FloatRealRepr ng f'

CVC4

type CVC4OnlineBackend scope st fs = OnlineBackend (Writer CVC4) scope st fs Source #

withCVC4OnlineBackend :: (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.

n.b. the explicit forall allows the fs to be expressed as the first argument so that it can be dictated easily from the caller. Example:

withCVC4OnlineBackend FloatRealRepr ng f'

CVC5

type CVC5OnlineBackend scope st fs = OnlineBackend (Writer CVC5) scope st fs Source #

withCVC5OnlineBackend :: (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.

n.b. the explicit forall allows the fs to be expressed as the first argument so that it can be dictated easily from the caller. Example:

withCVC5OnlineBackend FloatRealRepr ng f'

STP

type STPOnlineBackend scope st fs = OnlineBackend (Writer STP) scope st fs Source #

withSTPOnlineBackend :: (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.

n.b. the explicit forall allows the fs to be expressed as the first argument so that it can be dictated easily from the caller. Example:

withSTPOnlineBackend FloatRealRepr ng f'