diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs index 744ea359d..3ad8171c5 100644 --- a/crucible-cli/src/Lang/Crucible/CLI.hs +++ b/crucible-cli/src/Lang/Crucible/CLI.hs @@ -21,7 +21,7 @@ module Lang.Crucible.CLI ) where import Control.Monad - +import Control.Monad.Except (runExceptT) import Data.Foldable import Data.Map (Map) import Data.Text (Text) @@ -49,11 +49,13 @@ import Lang.Crucible.Syntax.SExpr import Lang.Crucible.Analysis.Postdom import Lang.Crucible.Backend -import Lang.Crucible.Backend.Prove (ProofResult(..), proveCurrentObligations) +import qualified Lang.Crucible.Backend.Prove as Prove import Lang.Crucible.Backend.Simple import Lang.Crucible.FunctionHandle import Lang.Crucible.Simulator import Lang.Crucible.Simulator.Profiling +import qualified Lang.Crucible.Utils.Seconds as Sec +import qualified Lang.Crucible.Utils.Timeout as CTO import What4.Config import What4.Interface (getConfiguration) @@ -181,12 +183,22 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks = getProofObligations bak >>= \case Nothing -> hPutStrLn outh "==== No proof obligations ====" Just {} -> hPutStrLn outh "==== Proof obligations ====" - proveCurrentObligations bak defaultLogData z3Adapter $ \goal res -> do - hPrint outh =<< ppProofObligation sym goal - case res of - Proved {} -> hPutStrLn outh "PROVED" - Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE" - Unknown {} -> hPutStrLn outh "UNKNOWN" + -- TODO: Make this timeout configurable via the CLI + let timeout = CTO.Timeout (Sec.secondsFromInt 5) + let prover = Prove.offlineProver timeout sym defaultLogData z3Adapter + let strat = Prove.ProofStrategy prover Prove.keepGoing + let ppResult = + \case + Prove.Proved {} -> "PROVED" + Prove.Disproved {} -> "COUNTEREXAMPLE" + Prove.Unknown {} -> "UNKNOWN" + let printer = Prove.ProofConsumer $ \goal res -> do + hPrint outh =<< ppProofObligation sym goal + hPutStrLn outh (ppResult res) + runExceptT (Prove.proveCurrentObligations bak strat printer) >>= + \case + Left CTO.TimedOut -> hPutStrLn outh "TIMEOUT" + Right () -> pure () _ -> hPutStrLn outh "No suitable main function found" diff --git a/crucible-symio/tests/TestMain.hs b/crucible-symio/tests/TestMain.hs index 24fc89b6a..67d7720fe 100644 --- a/crucible-symio/tests/TestMain.hs +++ b/crucible-symio/tests/TestMain.hs @@ -27,6 +27,7 @@ import GHC.TypeNats import Control.Lens ( (^.) ) import Control.Monad (foldM ) +import Control.Monad.Except (runExceptT) import Control.Monad.IO.Class (liftIO) import qualified Data.Map as Map import qualified Data.Parameterized.Context as Ctx @@ -51,6 +52,8 @@ import qualified Lang.Crucible.Simulator as CS import qualified Lang.Crucible.Simulator.OverrideSim as CSO import qualified Lang.Crucible.FunctionHandle as CFH import qualified Lang.Crucible.Simulator.GlobalState as CGS +import qualified Lang.Crucible.Utils.Seconds as Sec +import qualified Lang.Crucible.Utils.Timeout as CTO import qualified What4.Interface as W4 import qualified What4.Expr as WE @@ -134,7 +137,10 @@ runFSTest' bak (FSTest fsTest) = do putStrLn $ showF p T.assertFailure "Partial Result" - CB.proveCurrentObligations bak WSA.defaultLogData W4Y.yicesAdapter $ \obligation -> + let timeout = CTO.Timeout (Sec.secondsFromInt 5) + let prover = CB.offlineProver timeout sym WSA.defaultLogData W4Y.yicesAdapter + let strat = CB.ProofStrategy prover CB.failFast + merr <- runExceptT $ CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \obligation -> \case CB.Proved {} -> return () CB.Unknown {} -> T.assertFailure "Inconclusive" @@ -145,6 +151,9 @@ runFSTest' bak (FSTest fsTest) = do putStrLn (showF asmsPred) putStrLn (showF goalPred) T.assertFailure "Assertion Failure" + case merr of + Left CTO.TimedOut -> T.assertFailure "Timeout" + Right () -> pure () showAbortedResult :: CS.AbortedResult c d -> String showAbortedResult ar = case ar of diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs index 8e69a1628..a7bab5612 100644 --- a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs +++ b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs @@ -10,23 +10,24 @@ module Lang.Crucible.Syntax.Overrides ) where import Control.Lens hiding ((:>), Empty) -import Control.Monad (forM_) +import Control.Monad.Except (runExceptT) import Control.Monad.IO.Class import System.IO import Data.Parameterized.Context hiding (view) import What4.Expr.Builder -import What4.Interface import What4.ProgramLoc -import What4.SatResult import What4.Solver (LogData(..), defaultLogData) -import What4.Solver.Z3 (runZ3InOverride) +import What4.Solver.Z3 (z3Adapter) import Lang.Crucible.Backend +import qualified Lang.Crucible.Backend.Prove as CB import Lang.Crucible.Types import Lang.Crucible.FunctionHandle import Lang.Crucible.Simulator +import qualified Lang.Crucible.Utils.Seconds as Sec +import qualified Lang.Crucible.Utils.Timeout as CTO setupOverrides :: @@ -48,15 +49,20 @@ proveObligations = liftIO $ do hPutStrLn h "Attempting to prove all outstanding obligations!\n" - obls <- maybe [] goalsToList <$> getProofObligations bak - clearProofObligations bak + let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h + , logReason = "assertion proof" } + let timeout = CTO.Timeout (Sec.secondsFromInt 5) + let prover = CB.offlineProver timeout sym logData z3Adapter + let strat = CB.ProofStrategy prover CB.keepGoing + let ppResult o = + \case + CB.Proved {} -> unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg] + CB.Disproved {} -> unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg] + CB.Unknown {} -> unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg] + let printer = CB.ProofConsumer $ \o r -> hPutStrLn h (ppResult o r) + runExceptT (CB.proveCurrentObligations bak strat printer) >>= + \case + Left CTO.TimedOut -> hPutStrLn h "Proof timed out!" + Right () -> pure () - forM_ obls $ \o -> - do asms <- assumptionsPred sym (proofAssumptions o) - gl <- notPred sym (o ^. to proofGoal.labeledPred) - let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h - , logReason = "assertion proof" } - runZ3InOverride sym logData [asms,gl] $ \case - Unsat{} -> hPutStrLn h $ unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg] - Sat _mdl -> hPutStrLn h $ unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg] - Unknown -> hPutStrLn h $ unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg] + clearProofObligations bak diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal index c778eca6b..c786a4e23 100644 --- a/crucible/crucible.cabal +++ b/crucible/crucible.cabal @@ -44,6 +44,7 @@ common bldflags library import: bldflags build-depends: + async, base >= 4.13 && < 4.19, bimap, bv-sized >= 1.0.0 && < 1.1, @@ -129,6 +130,8 @@ library Lang.Crucible.Utils.MuxTree Lang.Crucible.Utils.PrettyPrint Lang.Crucible.Utils.RegRewrite + Lang.Crucible.Utils.Seconds + Lang.Crucible.Utils.Timeout Lang.Crucible.Utils.StateContT Lang.Crucible.Utils.Structural diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs index 01c14e85b..5e8193f3a 100644 --- a/crucible/src/Lang/Crucible/Backend/Prove.hs +++ b/crucible/src/Lang/Crucible/Backend/Prove.hs @@ -3,36 +3,139 @@ Module : Lang.Crucible.Backend.Prove Description : Proving goals under assumptions Copyright : (c) Galois, Inc 2024 License : BSD3 + +This module contains helpers to dispatch the proof obligations arising from +symbolic execution using SMT solvers. There are several dimensions of +configurability, encapsulated in a 'ProofStrategy': + +* Offline vs. online: Offline solvers ('offlineProver') are simpler to manage + and more easily parallelized, but starting processes adds overhead, and online + solvers ('onlineProver') can share state as assumptions are added. See the + top-level README for What4 for further discussion of this choice. +* Failing fast ('failFast') vs. keeping going ('keepGoing') +* Timeouts: Proving with timeouts ('offlineProveWithTimeout') vs. without + ('offlineProve') +* Parallelism: Not yet available via helpers in this module, but may be added to + a 'ProofStrategy' by clients. + +Once an appropriate strategy has been selected, it can be passed to entrypoints +such as 'proveObligations' to dispatch proof obligations. + +When proving a single goal, the overall approach is: + +* Gather all of the assumptions ('Assumptions') currently in scope (e.g., + from branch conditions). +* Negate the goal ('CB.Assertion') that we are trying to prove. +* Attempt to prove the conjunction of the assumptions and the negated goal. + +If this goal is satisfiable ('W4R.Sat'), then there exists a counterexample +that makes the original goal false, so we have disproven the goal. If the +negated goal is unsatisfiable ('W4R.Unsat'), on the other hand, then the +original goal is proven. + +Another way to think of this is as the negated material conditional +(implication) @not (assumptions -> assertion)@. This formula is equivalent +to @not ((not assumptions) and assertion)@, i.e., @assumptions and (not +assertion)@. -} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ScopedTypeVariables #-} module Lang.Crucible.Backend.Prove - ( ProofResult(..) - , proveGoal - , proveProofGoal + ( -- * Strategy + ProofResult(..) + , ProofConsumer(..) + , ProofStrategy(..) + -- ** Combiner + , SubgoalResult(..) + , Combiner(..) + , keepGoing + , failFast + -- ** Prover + , Prover(..) + -- *** Offline + , offlineProve + , offlineProveWithTimeout + , offlineProver + -- *** Online + , onlineProve + , onlineProver + -- * Proving goals , proveGoals , proveObligations , proveCurrentObligations ) where import Control.Lens ((^.)) -import Data.Functor.Const (Const(Const, getConst)) +import Control.Monad.Catch (MonadMask) +import Control.Monad.Error.Class (MonadError, liftEither) +import Control.Monad.IO.Class (MonadIO(liftIO)) +import qualified Control.Monad.Reader as Reader import qualified What4.Interface as W4 import qualified What4.Expr as WE -import qualified What4.Solver.Adapter as WSA +import qualified What4.Protocol.Online as WPO +import qualified What4.Protocol.SMTWriter as W4SMT import qualified What4.SatResult as W4R +import qualified What4.Solver.Adapter as WSA import qualified Lang.Crucible.Backend as CB import Lang.Crucible.Backend.Assumptions (Assumptions) -import Lang.Crucible.Backend.ProofGoals (traverseGoalsWithAssumptions) +import Lang.Crucible.Utils.Timeout (Timeout, TimedOut) +import qualified Lang.Crucible.Utils.Timeout as CTO + +-- | Local helper +consumeGoals :: + -- | Consume an 'Assuming' + (asmp -> a -> a) -> + -- | Consume a 'Prove' + (goal -> a) -> + -- | Consume a 'ProveConj' + (a -> a -> a) -> + CB.Goals asmp goal -> + a +consumeGoals onAssumption onGoal onConj = go + where + go (CB.Prove gl) = onGoal gl + go (CB.Assuming as gl) = onAssumption as (go gl) + go (CB.ProveConj g1 g2) = onConj (go g1) (go g2) + +-- | Local helper +consumeGoalsWithAssumptions :: + forall asmp goal a. + Monoid asmp => + -- | Consume a 'Prove' + (asmp -> goal -> a) -> + -- | Consume a 'ProveConj' + (a -> a -> a) -> + CB.Goals asmp goal -> + a +consumeGoalsWithAssumptions onGoal onConj goals = + Reader.runReader (go goals) mempty + where + go :: CB.Goals asmp goal -> Reader.Reader asmp a + go = + consumeGoals + (\asmp gl -> Reader.local (<> asmp) gl) + (\gl -> Reader.asks (\asmps -> onGoal asmps gl)) + (\g1 g2 -> onConj <$> g1 <*> g2) + +--------------------------------------------------------------------- +-- * Strategy -- | The result of attempting to prove a goal with an SMT solver. -- -- The constructors of this type correspond to those of 'W4R.SatResult'. +-- +-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder' +-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type) data ProofResult sym t = -- | The goal was proved. -- @@ -40,6 +143,12 @@ data ProofResult sym t Proved -- | The goal was disproved, and a model that falsifies it is available. -- + -- The 'WE.GroundEvalFn' is only available for use during the execution of + -- a 'ProofConsumer'. See 'WSA.SolverAdapter'. + -- + -- The @'Maybe' 'WE.ExprRangeBindings'@ are 'Just' when using + -- 'offlineProve' and 'Nothing' when using 'onlineProve'. + -- -- Corresponds to 'W4R.Sat'. | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t)) -- | The SMT solver returned \"unknown\". @@ -47,25 +156,107 @@ data ProofResult sym t -- Corresponds to 'W4R.Unknown'. | Unknown --- | Prove a single goal ('CB.Assertion') under the supplied 'Assumptions'. +-- | A 'ProofStrategy' dictates how results are proved. -- --- The overall approach is: +-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder' +-- * @m@ is the monad in which the 'Prover' and 'Combiner' run +-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type) +-- * @r@ is the return type of the eventual 'ProofConsumer' +data ProofStrategy sym m t r + = ProofStrategy + { -- | Generally 'offlineProver' or 'onlineProver' + stratProver :: {-# UNPACK #-} !(Prover sym m t r) + , stratCombine :: Combiner m r + } + +-- | A callback used to consume a 'ProofResult'. -- --- * Gather all of the assumptions ('Assumptions') currently in scope (e.g., --- from branch conditions). --- * Negate the goal ('CB.Assertion') that were are trying to prove. --- * Attempt to prove the conjunction of the assumptions and the negated goal. +-- If the result is 'Disproved', then this function must consume the +-- 'WE.GroundEvalFn' before returning. See 'WSA.SolverAdapter'. -- --- If this goal is satisfiable ('W4R.Sat'), then there exists a counterexample --- that makes the original goal false, so we have disproven the goal. If the --- negated goal is unsatisfiable ('W4R.Unsat'), on the other hand, then the --- original goal is proven. +-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder' +-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type) +-- * @r@ is the return type of the callback +newtype ProofConsumer sym t r + = ProofConsumer (CB.ProofObligation sym -> ProofResult sym t -> IO r) + +--------------------------------------------------------------------- +-- *** Combiner + +-- | Whether or not a subgoal was proved, together with the result from a +-- 'ProofConsumer'. +data SubgoalResult r + = SubgoalResult + { subgoalWasProved :: !Bool + , subgoalResult :: !r + } + deriving Functor + +-- | How to combine results of proofs, used as part of a 'ProofStrategy'. -- --- Another way to think of this is as the negated material conditional --- (implication) @not (assumptions -> assertion)@. This formula is equivalent --- to @not ((not assumptions) and assertion)@, i.e., @assumptions and (not --- assertion)@. -proveGoal :: +-- * @m@ is the monad in which the 'Prover' and 'Combiner' run +-- * @r@ is the return type of the eventual 'ProofConsumer' +newtype Combiner m r + = Combiner + { getCombiner :: + m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r) + } + +-- | Combine 'SubgoalResult's using the '<>' operator. Keep going when subgoals +-- fail. +keepGoing :: Monad m => Semigroup r => Combiner m r +keepGoing = Combiner $ \a1 a2 -> subgoalAnd <$> a1 <*> a2 + where + subgoalAnd :: + Semigroup r => + SubgoalResult r -> + SubgoalResult r -> + SubgoalResult r + subgoalAnd (SubgoalResult ok1 r1) (SubgoalResult ok2 r2) = + SubgoalResult (ok1 && ok2) (r1 <> r2) + +-- | Combine 'SubgoalResult's using the '<>' operator. After the first subgoal +-- fails, stop trying to prove further goals. +failFast :: Monad m => Semigroup r => Combiner m r +failFast = Combiner $ \sr1 sr2 -> do + SubgoalResult ok1 r1 <- sr1 + if ok1 + then do + SubgoalResult ok2 r2 <- sr2 + pure (SubgoalResult ok2 (r1 <> r2)) + else pure (SubgoalResult False r1) + +isProved :: ProofResult sym t -> Bool +isProved = + \case + Proved {} -> True + Disproved {} -> False + Unknown {} -> False + +--------------------------------------------------------------------- +-- ** Prover + +-- | A collection of functions used to prove goals as part of a 'ProofStrategy'. +data Prover sym m t r + = Prover + { -- | Prove a single goal under some 'Assumptions'. + proverProve :: + Assumptions sym -> + CB.Assertion sym -> + ProofConsumer sym t r -> + m (SubgoalResult r) + -- | Assume some 'Assumptions' in the scope of a subgoal. + , proverAssume :: + Assumptions sym -> + m (SubgoalResult r) -> + m (SubgoalResult r) + } + +--------------------------------------------------------------------- +-- *** Offline + +-- Not exported +offlineProveIO :: (sym ~ WE.ExprBuilder t st fs) => W4.IsSymExprBuilder sym => sym -> @@ -73,77 +264,192 @@ proveGoal :: WSA.SolverAdapter st -> Assumptions sym -> CB.Assertion sym -> - -- | Continuation to process the 'ProofResult'. - (CB.ProofObligation sym -> ProofResult sym t -> IO r) -> - IO r -proveGoal sym ld adapter asms goal k = do + ProofConsumer sym t r -> + IO (SubgoalResult r) +offlineProveIO sym ld adapter asmps goal (ProofConsumer k) = do let goalPred = goal ^. CB.labeledPred - asmsPred <- CB.assumptionsPred sym asms + asmsPred <- CB.assumptionsPred sym asmps notGoal <- W4.notPred sym goalPred - WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $ - k (CB.ProofGoal asms goal) . - \case - W4R.Sat (gfn, binds) -> Disproved gfn binds - W4R.Unsat () -> Proved - W4R.Unknown -> Unknown - --- | Prove a single 'CB.ProofGoal'. -proveProofGoal :: + WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $ \r -> + let r' = + case r of + W4R.Sat (gfn, binds) -> Disproved gfn binds + W4R.Unsat () -> Proved + W4R.Unknown -> Unknown + in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r' + +-- | Prove a goal using an \"offline\" solver (i.e., one process per goal). +-- +-- See 'offlineProveWithTimeout' for a version that integrates 'Timeout's. +-- +-- See the module-level documentation for further discussion of offline vs. +-- online solving. +offlineProve :: + MonadIO m => (sym ~ WE.ExprBuilder t st fs) => W4.IsSymExprBuilder sym => sym -> WSA.LogData -> WSA.SolverAdapter st -> - CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) -> - -- | Continuation to process the 'ProofResult'. - (CB.ProofObligation sym -> ProofResult sym t -> IO r) -> - IO r -proveProofGoal sym ld adapter (CB.ProofGoal asms goal) = - proveGoal sym ld adapter asms goal - --- | Prove a collection of 'CB.Goals'. -proveGoals :: - (Monoid m, sym ~ WE.ExprBuilder t st fs) => + Assumptions sym -> + CB.Assertion sym -> + ProofConsumer sym t r -> + m (SubgoalResult r) +offlineProve sym ld adapter asmps goal k = + liftIO (offlineProveIO sym ld adapter asmps goal k) + +-- | Prove a goal using an \"offline\" solver, with a timeout. +-- +-- See 'offlineProveWithTimeout' for a version without 'Timeout's. +-- +-- See the module-level documentation for further discussion of offline vs. +-- online solving. +offlineProveWithTimeout :: + MonadError TimedOut m => + MonadIO m => + (sym ~ WE.ExprBuilder t st fs) => W4.IsSymExprBuilder sym => + Timeout -> sym -> WSA.LogData -> WSA.SolverAdapter st -> - CB.Goals (CB.Assumptions sym) (CB.Assertion sym) -> - -- | Continuation to process each 'ProofResult'. - (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> - IO m -proveGoals sym ld adapter goals k = - getConst $ - traverseGoalsWithAssumptions - (\as g -> Const (proveGoal sym ld adapter as g k)) - goals + Assumptions sym -> + CB.Assertion sym -> + ProofConsumer sym t r -> + m (SubgoalResult r) +offlineProveWithTimeout to sym ld adapter asmps goal k = do + r <- liftIO (CTO.withTimeout to (offlineProveIO sym ld adapter asmps goal k)) + liftEither r --- | Prove a collection of 'CB.ProofObligations'. -proveObligations :: - (Monoid m, sym ~ WE.ExprBuilder t st fs) => +-- | Prove goals using 'offlineProveWithTimeout'. +-- +-- See the module-level documentation for further discussion of offline vs. +-- online solving. +offlineProver :: + MonadError TimedOut m => + MonadIO m => + (sym ~ WE.ExprBuilder t st fs) => + Timeout -> + W4.IsSymExprBuilder sym => sym -> WSA.LogData -> WSA.SolverAdapter st -> + Prover sym m t r +offlineProver to sym ld adapter = + Prover + { proverProve = offlineProveWithTimeout to sym ld adapter + , proverAssume = \_asmps a -> a + } + +--------------------------------------------------------------------- +-- *** Online + +-- | Prove a goal using an \"online\" solver (i.e., one process for all goals). +-- +-- See the module-level documentation for further discussion of offline vs. +-- online solving. +onlineProve :: + MonadIO m => + W4SMT.SMTReadWriter solver => + (sym ~ WE.ExprBuilder t st fs) => + W4.IsSymExprBuilder sym => + WPO.SolverProcess t solver -> + Assumptions sym -> + CB.Assertion sym -> + ProofConsumer sym t r -> + m (SubgoalResult r) +onlineProve sProc asmps goal (ProofConsumer k) = + liftIO $ WPO.checkSatisfiableWithModel sProc "prove" (goal ^. CB.labeledPred) $ \r -> + let r' = + case r of + W4R.Sat gfn -> Disproved gfn Nothing + W4R.Unsat () -> Proved + W4R.Unknown -> Unknown + in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r' + +-- | Add an assumption by @push@ing a new frame ('WPO.inNewFrame'). +onlineAssume :: + MonadIO m => + MonadMask m => + W4SMT.SMTReadWriter solver => + W4.IsSymExprBuilder sym => + (W4.SymExpr sym ~ WE.Expr t) => + sym -> + WPO.SolverProcess t solver -> + Assumptions sym -> + m r -> + m r +onlineAssume sym sProc asmps a = + WPO.inNewFrame sProc $ do + liftIO $ do + let conn = WPO.solverConn sProc + asmpsPred <- CB.assumptionsPred sym asmps + term <- W4SMT.mkFormula conn asmpsPred + W4SMT.assumeFormula conn term + pure () + a + +-- | Prove goals using 'onlineProve' and 'onlineAssume'. +-- +-- See the module-level documentation for further discussion of offline vs. +-- online solving. +onlineProver :: + MonadIO m => + MonadMask m => + W4SMT.SMTReadWriter solver => + (sym ~ WE.ExprBuilder t st fs) => + W4.IsSymExprBuilder sym => + sym -> + WPO.SolverProcess t solver -> + Prover sym m t r +onlineProver sym sProc = + Prover + { proverProve = onlineProve sProc + , proverAssume = onlineAssume sym sProc + } + +--------------------------------------------------------------------- +-- * Proving goals + +-- | Prove a collection of 'CB.Goals' using the specified 'ProofStrategy'. +proveGoals :: + Functor m => + ProofStrategy sym m t r -> + CB.Goals (CB.Assumptions sym) (CB.Assertion sym) -> + ProofConsumer sym t r -> + m r +proveGoals (ProofStrategy prover (Combiner comb)) goals k = + fmap subgoalResult $ + consumeGoalsWithAssumptions + (\asmps gl -> proverProve prover asmps gl k) + comb + goals + +-- | Prove a collection of 'CB.ProofObligations' using a 'ProofStrategy'. +proveObligations :: + Applicative m => + Monoid r => + (sym ~ WE.ExprBuilder t st fs) => + ProofStrategy sym m t r -> CB.ProofObligations sym -> - -- | Continuation to process each 'ProofResult'. - (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> - IO m -proveObligations sym ld adapter obligations k = + ProofConsumer sym t r -> + m r +proveObligations strat obligations k = case obligations of Nothing -> pure mempty - Just goals -> proveGoals sym ld adapter goals k + Just goals -> proveGoals strat goals k -- | Prove a the current collection of 'CB.ProofObligations' associated with the -- symbolic backend (retrieved via 'CB.getProofObligations'). proveCurrentObligations :: - (Monoid m, CB.IsSymBackend sym bak, sym ~ WE.ExprBuilder t st fs) => + MonadIO m => + Monoid r => + (sym ~ WE.ExprBuilder t st fs) => + CB.IsSymBackend sym bak => bak -> - WSA.LogData -> - WSA.SolverAdapter st -> - -- | Continuation to process each 'ProofResult'. - (CB.ProofObligation sym -> ProofResult sym t -> IO m) -> - IO m -proveCurrentObligations bak ld adapter k = do - obligations <- CB.getProofObligations bak - let sym = CB.backendGetSym bak - proveObligations sym ld adapter obligations k + ProofStrategy sym m t r -> + ProofConsumer sym t r -> + m r +proveCurrentObligations bak strat k = do + obligations <- liftIO (CB.getProofObligations bak) + proveObligations strat obligations k diff --git a/crucible/src/Lang/Crucible/Utils/Seconds.hs b/crucible/src/Lang/Crucible/Utils/Seconds.hs new file mode 100644 index 000000000..1350ce44b --- /dev/null +++ b/crucible/src/Lang/Crucible/Utils/Seconds.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +module Lang.Crucible.Utils.Seconds + ( Seconds + , secondsToInt + , secondsFromInt + , secondsToMicroseconds + ) where + +newtype Seconds = Seconds { secondsToInt :: Int } + deriving (Eq, Num, Ord, Show) + +-- | Inverse of 'secondsToInt' +secondsFromInt :: Int -> Seconds +secondsFromInt = Seconds + +secondsToMicroseconds :: Seconds -> Int +secondsToMicroseconds = (* 1000000) . secondsToInt diff --git a/crucible/src/Lang/Crucible/Utils/Timeout.hs b/crucible/src/Lang/Crucible/Utils/Timeout.hs new file mode 100644 index 000000000..42a70a108 --- /dev/null +++ b/crucible/src/Lang/Crucible/Utils/Timeout.hs @@ -0,0 +1,38 @@ +module Lang.Crucible.Utils.Timeout + ( Timeout(..) + , TimedOut(..) + , withTimeout + ) where + +import qualified Control.Concurrent as CC +import qualified Control.Concurrent.Async as CCA + +import qualified Lang.Crucible.Utils.Seconds as Secs + +-- | A timeout, in seconds. +newtype Timeout = Timeout { getTimeout :: Secs.Seconds } + deriving (Eq, Ord, Show) + +-- Private, not exported +timeoutToMicros :: Timeout -> Int +timeoutToMicros = Secs.secondsToMicroseconds . getTimeout + +-- | A task timed out. +data TimedOut = TimedOut + deriving Show + +-- | Execute a task with a timeout. +-- +-- Implemented via 'CCA.race', so re-throws exceptions that occur during the +-- task (if it completes before the timeout). +withTimeout :: + -- | Timeout duration (seconds) + Timeout -> + -- | Task to attempt + IO a -> + IO (Either TimedOut a) +withTimeout to task = do + let timeout = do + CC.threadDelay (timeoutToMicros to) + pure TimedOut + CCA.race timeout task