{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# Language ImplicitParams #-}
{-# Language MultiWayIf #-}
{-# Language PatternSynonyms #-}
{-# Language ScopedTypeVariables #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
{-# Language ViewPatterns #-}

module Crux.Goal where

import Control.Concurrent.Async (async, asyncThreadId, waitAnyCatch)
import Control.Exception (throwTo, SomeException, displayException)
import Control.Lens ((^.), view)

import Control.Monad (forM, forM_, unless, when)
import Data.Either (partitionEithers)
import Data.IORef
import Data.Maybe (fromMaybe)
import qualified Data.Map as Map
import qualified Data.Parameterized.Map as MapF
import qualified Data.Text as Text
import           Data.Void
import           Prettyprinter
import           System.Exit (ExitCode(ExitSuccess))
import           System.FilePath ((<.>), splitExtension)
import           System.IO (Handle, IOMode(..), withFile)
import qualified System.Timeout as ST

import What4.Interface (notPred, getConfiguration, IsExprBuilder)
import What4.Config (setOpt, getOptionSetting, Opt, ConfigOption)
import What4.ProgramLoc (ProgramLoc)
import What4.SatResult(SatResult(..))
import What4.Expr (ExprBuilder, GroundEvalFn(..), BoolExpr, GroundValueWrapper(..))
import What4.Protocol.Online( OnlineSolver, SolverProcess, inNewFrame, inNewFrame2Open
                            , inNewFrame2Close, solverEvalFuns, solverConn
                            , check, getUnsatCore, getAbducts )
import What4.Protocol.SMTWriter( SMTReadWriter, mkFormula, assumeFormulaWithFreshName
                               , assumeFormula, smtExprGroundEvalFn )
import qualified What4.Solver as WS
import Lang.Crucible.Backend
import Lang.Crucible.Backend.Online
        ( OnlineBackend, withSolverProcess, enableOnlineBackend, solverInteractionFile )
import Lang.Crucible.Simulator.SimError
        ( SimError(..), SimErrorReason(..) )
import Lang.Crucible.Simulator.ExecutionTree
        (ctxSymInterface)
import Lang.Crucible.Panic (panic)

import Crux.Types
import Crux.Model
import Crux.Log as Log
import Crux.Config.Common
import Crux.ProgressBar


symCfg :: (IsExprBuilder sym, Opt t a) => sym -> ConfigOption t -> a -> IO ()
symCfg :: forall sym (t :: BaseType) a.
(IsExprBuilder sym, Opt t a) =>
sym -> ConfigOption t -> a -> IO ()
symCfg sym
sym ConfigOption t
x a
y =
  do OptionSetting t
opt <- ConfigOption t -> Config -> IO (OptionSetting t)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption t
x (sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration sym
sym)
     [Doc Void]
_   <- OptionSetting t -> a -> IO [Doc Void]
forall (tp :: BaseType) a.
Opt tp a =>
OptionSetting tp -> a -> IO [Doc Void]
setOpt OptionSetting t
opt a
y
     () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()


-- | Simplify the proved goals.
provedGoalsTree :: forall sym.
  ( IsSymInterface sym
  ) =>
  sym ->
  Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)) ->
  IO (Maybe ProvedGoals)
provedGoalsTree :: forall sym.
IsSymInterface sym =>
sym
-> Maybe
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
-> IO (Maybe ProvedGoals)
provedGoalsTree sym
sym = (Goals
   (CrucibleAssumptions (SymExpr sym))
   (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
    ProofResult sym)
 -> IO ProvedGoals)
-> Maybe
     (Goals
        (CrucibleAssumptions (SymExpr sym))
        (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
         ProofResult sym))
-> IO (Maybe ProvedGoals)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (CrucibleAssumptions (SymExpr sym)
-> Goals
     (CrucibleAssumptions (SymExpr sym))
     (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
      ProofResult sym)
-> IO ProvedGoals
go CrucibleAssumptions (SymExpr sym)
forall a. Monoid a => a
mempty)
  where
  go :: Assumptions sym ->
        Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym) ->
        IO ProvedGoals
  go :: CrucibleAssumptions (SymExpr sym)
-> Goals
     (CrucibleAssumptions (SymExpr sym))
     (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
      ProofResult sym)
-> IO ProvedGoals
go CrucibleAssumptions (SymExpr sym)
asmps Goals
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
   ProofResult sym)
gs =
    case Goals
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
   ProofResult sym)
gs of
      Assuming CrucibleAssumptions (SymExpr sym)
as Goals
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
   ProofResult sym)
gs1 -> CrucibleAssumptions (SymExpr sym)
-> Goals
     (CrucibleAssumptions (SymExpr sym))
     (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
      ProofResult sym)
-> IO ProvedGoals
go (CrucibleAssumptions (SymExpr sym)
asmps CrucibleAssumptions (SymExpr sym)
-> CrucibleAssumptions (SymExpr sym)
-> CrucibleAssumptions (SymExpr sym)
forall a. Semigroup a => a -> a -> a
<> CrucibleAssumptions (SymExpr sym)
as) Goals
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
   ProofResult sym)
gs1
      Prove (LabeledPred (SymExpr sym BaseBoolType) SimError
p,[ProgramLoc]
locs,ProofResult sym
r) -> sym
-> CrucibleAssumptions (SymExpr sym)
-> LabeledPred (SymExpr sym BaseBoolType) SimError
-> [ProgramLoc]
-> ProofResult sym
-> IO ProvedGoals
forall sym.
IsSymInterface sym =>
sym
-> Assumptions sym
-> Assertion sym
-> [ProgramLoc]
-> ProofResult sym
-> IO ProvedGoals
proveToGoal sym
sym CrucibleAssumptions (SymExpr sym)
asmps LabeledPred (SymExpr sym BaseBoolType) SimError
p [ProgramLoc]
locs ProofResult sym
r
      ProveConj Goals
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
   ProofResult sym)
g1 Goals
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
   ProofResult sym)
g2 -> ProvedGoals -> ProvedGoals -> ProvedGoals
Branch (ProvedGoals -> ProvedGoals -> ProvedGoals)
-> IO ProvedGoals -> IO (ProvedGoals -> ProvedGoals)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CrucibleAssumptions (SymExpr sym)
-> Goals
     (CrucibleAssumptions (SymExpr sym))
     (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
      ProofResult sym)
-> IO ProvedGoals
go CrucibleAssumptions (SymExpr sym)
asmps Goals
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
   ProofResult sym)
g1 IO (ProvedGoals -> ProvedGoals) -> IO ProvedGoals -> IO ProvedGoals
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CrucibleAssumptions (SymExpr sym)
-> Goals
     (CrucibleAssumptions (SymExpr sym))
     (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
      ProofResult sym)
-> IO ProvedGoals
go CrucibleAssumptions (SymExpr sym)
asmps Goals
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (SymExpr sym BaseBoolType) SimError, [ProgramLoc],
   ProofResult sym)
g2

proveToGoal ::
  (IsSymInterface sym) =>
  sym ->
  Assumptions sym ->
  Assertion sym ->
  [ProgramLoc] ->
  ProofResult sym ->
  IO ProvedGoals
proveToGoal :: forall sym.
IsSymInterface sym =>
sym
-> Assumptions sym
-> Assertion sym
-> [ProgramLoc]
-> ProofResult sym
-> IO ProvedGoals
proveToGoal sym
sym Assumptions sym
allAsmps Assertion sym
p [ProgramLoc]
locs ProofResult sym
pr =
  case ProofResult sym
pr of
    NotProved Doc Void
ex Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
cex [String]
s ->
      do [CrucibleAssumption (SymExpr sym)]
as <- sym -> Assumptions sym -> IO [CrucibleAssumption (SymExpr sym)]
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO [Assumption sym]
flattenAssumptions sym
sym Assumptions sym
allAsmps
         ProvedGoals -> IO ProvedGoals
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([CrucibleAssumption (Const ())]
-> SimError
-> Doc Void
-> [ProgramLoc]
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProvedGoals
NotProvedGoal ((CrucibleAssumption (SymExpr sym) -> CrucibleAssumption (Const ()))
-> [CrucibleAssumption (SymExpr sym)]
-> [CrucibleAssumption (Const ())]
forall a b. (a -> b) -> [a] -> [b]
map CrucibleAssumption (SymExpr sym) -> CrucibleAssumption (Const ())
forall {e :: BaseType -> *}.
CrucibleAssumption e -> CrucibleAssumption (Const ())
showAsmp [CrucibleAssumption (SymExpr sym)]
as) (Assertion sym -> SimError
forall {pred} {a}. LabeledPred pred a -> a
showGoal Assertion sym
p) Doc Void
ex [ProgramLoc]
locs Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
cex [String]
s)
    Proved [Either (CrucibleAssumption (SymExpr sym)) (Assertion sym)]
xs ->
      case [Either (CrucibleAssumption (SymExpr sym)) (Assertion sym)]
-> ([CrucibleAssumption (SymExpr sym)], [Assertion sym])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (CrucibleAssumption (SymExpr sym)) (Assertion sym)]
xs of
        ([CrucibleAssumption (SymExpr sym)]
asmps, [])  -> ProvedGoals -> IO ProvedGoals
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([CrucibleAssumption (Const ())]
-> SimError -> [ProgramLoc] -> Bool -> ProvedGoals
ProvedGoal ((CrucibleAssumption (SymExpr sym) -> CrucibleAssumption (Const ()))
-> [CrucibleAssumption (SymExpr sym)]
-> [CrucibleAssumption (Const ())]
forall a b. (a -> b) -> [a] -> [b]
map CrucibleAssumption (SymExpr sym) -> CrucibleAssumption (Const ())
forall {e :: BaseType -> *}.
CrucibleAssumption e -> CrucibleAssumption (Const ())
showAsmp [CrucibleAssumption (SymExpr sym)]
asmps) (Assertion sym -> SimError
forall {pred} {a}. LabeledPred pred a -> a
showGoal Assertion sym
p) [ProgramLoc]
locs Bool
True)
        ([CrucibleAssumption (SymExpr sym)]
asmps, Assertion sym
_:[Assertion sym]
_) -> ProvedGoals -> IO ProvedGoals
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([CrucibleAssumption (Const ())]
-> SimError -> [ProgramLoc] -> Bool -> ProvedGoals
ProvedGoal ((CrucibleAssumption (SymExpr sym) -> CrucibleAssumption (Const ()))
-> [CrucibleAssumption (SymExpr sym)]
-> [CrucibleAssumption (Const ())]
forall a b. (a -> b) -> [a] -> [b]
map CrucibleAssumption (SymExpr sym) -> CrucibleAssumption (Const ())
forall {e :: BaseType -> *}.
CrucibleAssumption e -> CrucibleAssumption (Const ())
showAsmp [CrucibleAssumption (SymExpr sym)]
asmps) (Assertion sym -> SimError
forall {pred} {a}. LabeledPred pred a -> a
showGoal Assertion sym
p) [ProgramLoc]
locs Bool
False)

 where
 showAsmp :: CrucibleAssumption e -> CrucibleAssumption (Const ())
showAsmp CrucibleAssumption e
x = CrucibleAssumption e -> CrucibleAssumption (Const ())
forall {e :: BaseType -> *}.
CrucibleAssumption e -> CrucibleAssumption (Const ())
forgetAssumption CrucibleAssumption e
x
 showGoal :: LabeledPred pred a -> a
showGoal LabeledPred pred a
x = LabeledPred pred a
xLabeledPred pred a -> Getting a (LabeledPred pred a) a -> a
forall s a. s -> Getting a s a -> a
^.Getting a (LabeledPred pred a) a
forall pred msg msg' (f :: * -> *).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg


countGoals :: Goals a b -> Int
countGoals :: forall a b. Goals a b -> Int
countGoals Goals a b
gs =
  case Goals a b
gs of
    Assuming a
_ Goals a b
gs1  -> Goals a b -> Int
forall a b. Goals a b -> Int
countGoals Goals a b
gs1
    Prove b
_         -> Int
1
    ProveConj Goals a b
g1 Goals a b
g2 -> Goals a b -> Int
forall a b. Goals a b -> Int
countGoals Goals a b
g1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Goals a b -> Int
forall a b. Goals a b -> Int
countGoals Goals a b
g2

isResourceExhausted :: LabeledPred p SimError -> Bool
isResourceExhausted :: forall p. LabeledPred p SimError -> Bool
isResourceExhausted (Getting SimError (LabeledPred p SimError) SimError
-> LabeledPred p SimError -> SimError
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting SimError (LabeledPred p SimError) SimError
forall pred msg msg' (f :: * -> *).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg -> SimError ProgramLoc
_ (ResourceExhausted String
_)) = Bool
True
isResourceExhausted LabeledPred p SimError
_ = Bool
False

updateProcessedGoals ::
  LabeledPred p SimError ->
  ProofResult a ->
  ProcessedGoals ->
  ProcessedGoals
updateProcessedGoals :: forall p a.
LabeledPred p SimError
-> ProofResult a -> ProcessedGoals -> ProcessedGoals
updateProcessedGoals LabeledPred p SimError
_ (Proved [Either (Assumption a) (Assertion a)]
_) ProcessedGoals
pgs =
  ProcessedGoals
pgs{ totalProcessedGoals = 1 + totalProcessedGoals pgs
     , provedGoals = 1 + provedGoals pgs
     }

updateProcessedGoals LabeledPred p SimError
res (NotProved Doc Void
_ Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
_ [String]
_) ProcessedGoals
pgs | LabeledPred p SimError -> Bool
forall p. LabeledPred p SimError -> Bool
isResourceExhausted LabeledPred p SimError
res =
  ProcessedGoals
pgs{ totalProcessedGoals = 1 + totalProcessedGoals pgs
     , incompleteGoals = 1 + incompleteGoals pgs
     }

updateProcessedGoals LabeledPred p SimError
_ (NotProved Doc Void
_ (Just (ModelView, [CrucibleEvent GroundValueWrapper])
_) [String]
_) ProcessedGoals
pgs =
  ProcessedGoals
pgs{ totalProcessedGoals = 1 + totalProcessedGoals pgs
     , disprovedGoals = 1 + disprovedGoals pgs
     }

updateProcessedGoals LabeledPred p SimError
_ (NotProved Doc Void
_ Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
Nothing [String]
_) ProcessedGoals
pgs =
  ProcessedGoals
pgs{ totalProcessedGoals = 1 + totalProcessedGoals pgs }

-- | A function that can be used to generate a pretty explanation of a
-- simulation error.

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

-- | 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.
proveGoalsOffline :: forall st sym p t fs personality msgs.
  ( sym ~ ExprBuilder t st fs
  , Logs msgs
  , SupportsCruxLogMessage msgs
  ) =>
  [WS.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)))
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)))
proveGoalsOffline [SolverAdapter st]
_adapter CruxOptions
_opts SimCtxt personality sym p
_ctx Maybe (GroundEvalFn t) -> Assertion sym -> IO (Doc Void)
_explainFailure Maybe (Goals (Assumptions sym) (Assertion sym))
Nothing = (ProcessedGoals,
 Maybe
   (Goals
      (CrucibleAssumptions (Expr t))
      (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
       ProofResult (ExprBuilder t st fs))))
-> IO
     (ProcessedGoals,
      Maybe
        (Goals
           (CrucibleAssumptions (Expr t))
           (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
            ProofResult (ExprBuilder t st fs))))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Integer -> Integer -> Integer -> ProcessedGoals
ProcessedGoals Integer
0 Integer
0 Integer
0 Integer
0, Maybe
  (Goals
     (CrucibleAssumptions (Expr t))
     (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
      ProofResult (ExprBuilder t st fs)))
forall a. Maybe a
Nothing)
proveGoalsOffline [SolverAdapter st]
adapters CruxOptions
opts SimCtxt personality sym p
ctx Maybe (GroundEvalFn t) -> Assertion sym -> IO (Doc Void)
explainFailure (Just Goals (Assumptions sym) (Assertion sym)
gs0) = do
  IORef ProcessedGoals
goalNum <- ProcessedGoals -> IO (IORef ProcessedGoals)
forall a. a -> IO (IORef a)
newIORef (Integer -> Integer -> Integer -> Integer -> ProcessedGoals
ProcessedGoals Integer
0 Integer
0 Integer
0 Integer
0)
  (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end,IO ()
finish) <- Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError)
-> IO (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
forall msgs asmp ast.
(Logs msgs, SupportsCruxLogMessage msgs) =>
Goals asmp ast
-> IO (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
proverMilestoneCallbacks Goals (Assumptions sym) (Assertion sym)
Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError)
gs0
  Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
gs <- SupportsCruxLogMessage msgs =>
(ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> IORef ProcessedGoals
-> Assumptions sym
-> Goals (Assumptions sym) (Assertion sym)
-> IO
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
(ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> IORef ProcessedGoals
-> Assumptions sym
-> Goals (Assumptions sym) (Assertion sym)
-> IO
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) IORef ProcessedGoals
goalNum Assumptions sym
CrucibleAssumptions (Expr t)
forall a. Monoid a => a
mempty Goals (Assumptions sym) (Assertion sym)
gs0
  ProcessedGoals
nms <- IORef ProcessedGoals -> IO ProcessedGoals
forall a. IORef a -> IO a
readIORef IORef ProcessedGoals
goalNum
  IO ()
finish
  (ProcessedGoals,
 Maybe
   (Goals
      (CrucibleAssumptions (Expr t))
      (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
       ProofResult (ExprBuilder t st fs))))
-> IO
     (ProcessedGoals,
      Maybe
        (Goals
           (CrucibleAssumptions (Expr t))
           (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
            ProofResult (ExprBuilder t st fs))))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProcessedGoals
nms, Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
-> Maybe
     (Goals
        (CrucibleAssumptions (Expr t))
        (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
         ProofResult (ExprBuilder t st fs)))
forall a. a -> Maybe a
Just Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
gs)

  where
    sym :: sym
sym = SimCtxt personality sym p
ctxSimCtxt personality sym p
-> Getting sym (SimCtxt personality sym p) sym -> sym
forall s a. s -> Getting a s a -> a
^.Getting sym (SimCtxt personality sym p) sym
forall p sym ext (f :: * -> *).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface

    failfast :: Bool
failfast = CruxOptions -> Bool
proofGoalsFailFast CruxOptions
opts

    go :: SupportsCruxLogMessage msgs
       => (ProverMilestoneStartGoal, ProverMilestoneEndGoal)
       -> IORef ProcessedGoals
       -> Assumptions sym
       -> Goals (Assumptions sym) (Assertion sym)
       -> IO (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
    go :: SupportsCruxLogMessage msgs =>
(ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> IORef ProcessedGoals
-> Assumptions sym
-> Goals (Assumptions sym) (Assertion sym)
-> IO
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) IORef ProcessedGoals
goalNum Assumptions sym
assumptionsInScope Goals (Assumptions sym) (Assertion sym)
gs =
      case Goals (Assumptions sym) (Assertion sym)
gs of
        Assuming Assumptions sym
ps Goals (Assumptions sym) (Assertion sym)
gs1 -> do
          Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
res <- SupportsCruxLogMessage msgs =>
(ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> IORef ProcessedGoals
-> Assumptions sym
-> Goals (Assumptions sym) (Assertion sym)
-> IO
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
(ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> IORef ProcessedGoals
-> Assumptions sym
-> Goals (Assumptions sym) (Assertion sym)
-> IO
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) IORef ProcessedGoals
goalNum (Assumptions sym
CrucibleAssumptions (Expr t)
assumptionsInScope CrucibleAssumptions (Expr t)
-> CrucibleAssumptions (Expr t) -> CrucibleAssumptions (Expr t)
forall a. Semigroup a => a -> a -> a
<> Assumptions sym
CrucibleAssumptions (Expr t)
ps) Goals (Assumptions sym) (Assertion sym)
gs1
          Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
-> IO
     (Goals
        (CrucibleAssumptions (Expr t))
        (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
         ProofResult (ExprBuilder t st fs)))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CrucibleAssumptions (Expr t)
-> Goals
     (CrucibleAssumptions (Expr t))
     (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
      ProofResult (ExprBuilder t st fs))
-> Goals
     (CrucibleAssumptions (Expr t))
     (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
      ProofResult (ExprBuilder t st fs))
forall asmp goal. asmp -> Goals asmp goal -> Goals asmp goal
Assuming Assumptions sym
CrucibleAssumptions (Expr t)
ps Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
res)

        ProveConj Goals (Assumptions sym) (Assertion sym)
g1 Goals (Assumptions sym) (Assertion sym)
g2 -> do
          Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
g1' <- SupportsCruxLogMessage msgs =>
(ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> IORef ProcessedGoals
-> Assumptions sym
-> Goals (Assumptions sym) (Assertion sym)
-> IO
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
(ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> IORef ProcessedGoals
-> Assumptions sym
-> Goals (Assumptions sym) (Assertion sym)
-> IO
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) IORef ProcessedGoals
goalNum Assumptions sym
assumptionsInScope Goals (Assumptions sym) (Assertion sym)
g1
          Integer
numDisproved <- ProcessedGoals -> Integer
disprovedGoals (ProcessedGoals -> Integer) -> IO ProcessedGoals -> IO Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef ProcessedGoals -> IO ProcessedGoals
forall a. IORef a -> IO a
readIORef IORef ProcessedGoals
goalNum
          if Bool
failfast Bool -> Bool -> Bool
&& Integer
numDisproved Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0
            then Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
-> IO
     (Goals
        (CrucibleAssumptions (Expr t))
        (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
         ProofResult (ExprBuilder t st fs)))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
g1'
            else Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
-> Goals
     (CrucibleAssumptions (Expr t))
     (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
      ProofResult (ExprBuilder t st fs))
-> Goals
     (CrucibleAssumptions (Expr t))
     (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
      ProofResult (ExprBuilder t st fs))
forall asmp goal.
Goals asmp goal -> Goals asmp goal -> Goals asmp goal
ProveConj Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult (ExprBuilder t st fs))
g1' (Goals
   (CrucibleAssumptions (Expr t))
   (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
    ProofResult (ExprBuilder t st fs))
 -> Goals
      (CrucibleAssumptions (Expr t))
      (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
       ProofResult (ExprBuilder t st fs)))
-> IO
     (Goals
        (CrucibleAssumptions (Expr t))
        (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
         ProofResult (ExprBuilder t st fs)))
-> IO
     (Goals
        (CrucibleAssumptions (Expr t))
        (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
         ProofResult (ExprBuilder t st fs)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SupportsCruxLogMessage msgs =>
(ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> IORef ProcessedGoals
-> Assumptions sym
-> Goals (Assumptions sym) (Assertion sym)
-> IO
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
(ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> IORef ProcessedGoals
-> Assumptions sym
-> Goals (Assumptions sym) (Assertion sym)
-> IO
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) IORef ProcessedGoals
goalNum Assumptions sym
assumptionsInScope Goals (Assumptions sym) (Assertion sym)
g2

        Prove Assertion sym
p -> do
          Integer
goalNumber <- ProcessedGoals -> Integer
totalProcessedGoals (ProcessedGoals -> Integer) -> IO ProcessedGoals -> IO Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef ProcessedGoals -> IO ProcessedGoals
forall a. IORef a -> IO a
readIORef IORef ProcessedGoals
goalNum
          ProverMilestoneStartGoal
start Integer
goalNumber

          -- Conjoin all of the in-scope assumptions, the goal, then negate and
          -- check sat with the adapter
          Expr t BaseBoolType
assumptions <- sym -> Assumptions sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred sym
sym Assumptions sym
assumptionsInScope
          Expr t BaseBoolType
goal <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (Assertion sym
LabeledPred (Expr t BaseBoolType) SimError
p LabeledPred (Expr t BaseBoolType) SimError
-> Getting
     (Expr t BaseBoolType)
     (LabeledPred (Expr t BaseBoolType) SimError)
     (Expr t BaseBoolType)
-> Expr t BaseBoolType
forall s a. s -> Getting a s a -> a
^. Getting
  (Expr t BaseBoolType)
  (LabeledPred (Expr t BaseBoolType) SimError)
  (Expr t BaseBoolType)
forall pred msg pred' (f :: * -> *).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred)

          Either [SomeException] (Maybe ([ProgramLoc], ProofResult sym))
res <- Maybe DiffTime
-> [SolverAdapter st]
-> (SolverAdapter st -> IO ([ProgramLoc], ProofResult sym))
-> IO
     (Either [SomeException] (Maybe ([ProgramLoc], ProofResult sym)))
forall a b (s :: * -> *) time.
RealFrac time =>
Maybe time
-> [SolverAdapter s]
-> (SolverAdapter s -> IO (b, ProofResult a))
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
dispatchSolversOnGoalAsync (CruxOptions -> Maybe DiffTime
goalTimeout CruxOptions
opts) [SolverAdapter st]
adapters
                           (Assertion sym
-> Assumptions sym
-> Expr t BaseBoolType
-> Expr t BaseBoolType
-> Integer
-> SolverAdapter st
-> IO ([ProgramLoc], ProofResult sym)
runOneSolver Assertion sym
p Assumptions sym
assumptionsInScope Expr t BaseBoolType
assumptions Expr t BaseBoolType
goal Integer
goalNumber)
          ProverMilestoneStartGoal
end Integer
goalNumber
          case Either [SomeException] (Maybe ([ProgramLoc], ProofResult sym))
res of
            Right Maybe ([ProgramLoc], ProofResult sym)
Nothing -> do
              let details :: ProofResult sym
details = Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
forall sym.
Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
NotProved Doc Void
"(timeout)" Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
forall a. Maybe a
Nothing []
              let locs :: [ProgramLoc]
locs = CrucibleAssumptions (Expr t) -> [ProgramLoc]
forall (e :: BaseType -> *). CrucibleAssumptions e -> [ProgramLoc]
assumptionsTopLevelLocs Assumptions sym
CrucibleAssumptions (Expr t)
assumptionsInScope
              IORef ProcessedGoals -> (ProcessedGoals -> ProcessedGoals) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef ProcessedGoals
goalNum (LabeledPred (Expr t BaseBoolType) SimError
-> ProofResult Any -> ProcessedGoals -> ProcessedGoals
forall p a.
LabeledPred p SimError
-> ProofResult a -> ProcessedGoals -> ProcessedGoals
updateProcessedGoals Assertion sym
LabeledPred (Expr t BaseBoolType) SimError
p ProofResult Any
forall {sym}. ProofResult sym
details)
              Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult sym)
-> IO
     (Goals
        (CrucibleAssumptions (Expr t))
        (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
         ProofResult sym))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
 ProofResult sym)
-> Goals
     (CrucibleAssumptions (Expr t))
     (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
      ProofResult sym)
forall asmp goal. goal -> Goals asmp goal
Prove (Assertion sym
LabeledPred (Expr t BaseBoolType) SimError
p, [ProgramLoc]
locs, ProofResult sym
forall {sym}. ProofResult sym
details))

            Right (Just ([ProgramLoc]
locs,ProofResult sym
details)) -> do
              IORef ProcessedGoals -> (ProcessedGoals -> ProcessedGoals) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef ProcessedGoals
goalNum (LabeledPred (Expr t BaseBoolType) SimError
-> ProofResult sym -> ProcessedGoals -> ProcessedGoals
forall p a.
LabeledPred p SimError
-> ProofResult a -> ProcessedGoals -> ProcessedGoals
updateProcessedGoals Assertion sym
LabeledPred (Expr t BaseBoolType) SimError
p ProofResult sym
details)
              case ProofResult sym
details of
                NotProved Doc Void
_ (Just (ModelView, [CrucibleEvent GroundValueWrapper])
_) [String]
_ ->
                  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
failfast Bool -> Bool -> Bool
&& Bool -> Bool
not (LabeledPred (Expr t BaseBoolType) SimError -> Bool
forall p. LabeledPred p SimError -> Bool
isResourceExhausted Assertion sym
LabeledPred (Expr t BaseBoolType) SimError
p)) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
                    CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
Log.FoundCounterExample
                ProofResult sym
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Goals
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
   ProofResult sym)
-> IO
     (Goals
        (CrucibleAssumptions (Expr t))
        (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
         ProofResult sym))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
 ProofResult sym)
-> Goals
     (CrucibleAssumptions (Expr t))
     (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
      ProofResult sym)
forall asmp goal. goal -> Goals asmp goal
Prove (Assertion sym
LabeledPred (Expr t BaseBoolType) SimError
p, [ProgramLoc]
locs, ProofResult sym
details))
            Left [SomeException]
es -> do
              IORef ProcessedGoals -> (ProcessedGoals -> ProcessedGoals) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef ProcessedGoals
goalNum (LabeledPred (Expr t BaseBoolType) SimError
-> ProofResult Any -> ProcessedGoals -> ProcessedGoals
forall p a.
LabeledPred p SimError
-> ProofResult a -> ProcessedGoals -> ProcessedGoals
updateProcessedGoals Assertion sym
LabeledPred (Expr t BaseBoolType) SimError
p (Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult Any
forall sym.
Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
NotProved Doc Void
forall a. Monoid a => a
mempty Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
forall a. Maybe a
Nothing []))
              let allExceptions :: String
allExceptions = [String] -> String
unlines (SomeException -> String
forall e. Exception e => e -> String
displayException (SomeException -> String) -> [SomeException] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SomeException]
es)
              String
-> IO
     (Goals
        (CrucibleAssumptions (Expr t))
        (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
         ProofResult sym))
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
allExceptions

    runOneSolver :: Assertion sym
                 -> Assumptions sym
                 -> BoolExpr t
                 -> BoolExpr t
                 -> Integer
                 -> WS.SolverAdapter st
                 -> IO ([ProgramLoc], ProofResult sym)
    runOneSolver :: Assertion sym
-> Assumptions sym
-> Expr t BaseBoolType
-> Expr t BaseBoolType
-> Integer
-> SolverAdapter st
-> IO ([ProgramLoc], ProofResult sym)
runOneSolver Assertion sym
p Assumptions sym
assumptionsInScope Expr t BaseBoolType
assumptions Expr t BaseBoolType
goal Integer
goalNumber SolverAdapter st
adapter =
      -- Create a file to a single offline solver interaction, assuming the user
      -- has selected this option. A single Crux session might invoke an offline
      -- solver multiple times, so each file has unique suffixes to indicate the
      -- goal number and which solver in particular was used to solve the goal.
      -- (Recall that a Crux user can choose multiple offline solvers, so it is
      -- important to indicate which solver was picked for each goal.)
      Maybe String
-> (Maybe Handle -> IO ([ProgramLoc], ProofResult sym))
-> IO ([ProgramLoc], ProofResult sym)
forall r. Maybe String -> (Maybe Handle -> IO r) -> IO r
withMaybeOfflineSolverOutputHandle (CruxOptions -> Maybe String
offlineSolverOutput CruxOptions
opts) ((Maybe Handle -> IO ([ProgramLoc], ProofResult sym))
 -> IO ([ProgramLoc], ProofResult sym))
-> (Maybe Handle -> IO ([ProgramLoc], ProofResult sym))
-> IO ([ProgramLoc], ProofResult sym)
forall a b. (a -> b) -> a -> b
$ \Maybe Handle
mbLogHandle ->
      let logData :: LogData
logData = LogData
WS.defaultLogData { WS.logHandle = mbLogHandle } in
      SolverAdapter st
-> forall t fs a.
   ExprBuilder t st fs
   -> LogData
   -> [BoolExpr t]
   -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
       -> IO a)
   -> IO a
forall (st :: * -> *).
SolverAdapter st
-> forall t fs a.
   ExprBuilder t st fs
   -> LogData
   -> [BoolExpr t]
   -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
       -> IO a)
   -> IO a
WS.solver_adapter_check_sat SolverAdapter st
adapter (SimCtxt personality sym p
ctx SimCtxt personality sym p
-> Getting
     (ExprBuilder t st fs)
     (SimCtxt personality sym p)
     (ExprBuilder t st fs)
-> ExprBuilder t st fs
forall s a. s -> Getting a s a -> a
^. Getting
  (ExprBuilder t st fs)
  (SimCtxt personality sym p)
  (ExprBuilder t st fs)
(ExprBuilder t st fs
 -> Const (ExprBuilder t st fs) (ExprBuilder t st fs))
-> SimContext (personality sym) (ExprBuilder t st fs) p
-> Const
     (ExprBuilder t st fs)
     (SimContext (personality sym) (ExprBuilder t st fs) p)
forall p sym ext (f :: * -> *).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface) LogData
logData [Expr t BaseBoolType
assumptions, Expr t BaseBoolType
goal] ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
  -> IO ([ProgramLoc], ProofResult sym))
 -> IO ([ProgramLoc], ProofResult sym))
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO ([ProgramLoc], ProofResult sym))
-> IO ([ProgramLoc], ProofResult sym)
forall a b. (a -> b) -> a -> b
$ \SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
satRes ->
        case SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
satRes of
          Unsat ()
_ -> do
            -- NOTE: We don't have an easy way to get an unsat core here
            -- because we don't have a solver connection.
            [CrucibleAssumption (Expr t)]
as <- sym -> Assumptions sym -> IO [Assumption sym]
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO [Assumption sym]
flattenAssumptions sym
sym Assumptions sym
assumptionsInScope
            let core :: [Either
   (CrucibleAssumption (Expr t))
   (LabeledPred (Expr t BaseBoolType) SimError)]
core = (CrucibleAssumption (Expr t)
 -> Either
      (CrucibleAssumption (Expr t))
      (LabeledPred (Expr t BaseBoolType) SimError))
-> [CrucibleAssumption (Expr t)]
-> [Either
      (CrucibleAssumption (Expr t))
      (LabeledPred (Expr t BaseBoolType) SimError)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CrucibleAssumption (Expr t)
-> Either
     (CrucibleAssumption (Expr t))
     (LabeledPred (Expr t BaseBoolType) SimError)
forall a b. a -> Either a b
Left [CrucibleAssumption (Expr t)]
as [Either
   (CrucibleAssumption (Expr t))
   (LabeledPred (Expr t BaseBoolType) SimError)]
-> [Either
      (CrucibleAssumption (Expr t))
      (LabeledPred (Expr t BaseBoolType) SimError)]
-> [Either
      (CrucibleAssumption (Expr t))
      (LabeledPred (Expr t BaseBoolType) SimError)]
forall a. [a] -> [a] -> [a]
++ [ LabeledPred (Expr t BaseBoolType) SimError
-> Either
     (CrucibleAssumption (Expr t))
     (LabeledPred (Expr t BaseBoolType) SimError)
forall a b. b -> Either a b
Right Assertion sym
LabeledPred (Expr t BaseBoolType) SimError
p ]
            let locs :: [ProgramLoc]
locs = CrucibleAssumptions (Expr t) -> [ProgramLoc]
forall (e :: BaseType -> *). CrucibleAssumptions e -> [ProgramLoc]
assumptionsTopLevelLocs Assumptions sym
CrucibleAssumptions (Expr t)
assumptionsInScope
            ([ProgramLoc], ProofResult sym)
-> IO ([ProgramLoc], ProofResult sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProgramLoc]
locs, [Either (Assumption sym) (Assertion sym)] -> ProofResult sym
forall sym.
[Either (Assumption sym) (Assertion sym)] -> ProofResult sym
Proved [Either (Assumption sym) (Assertion sym)]
[Either
   (CrucibleAssumption (Expr t))
   (LabeledPred (Expr t BaseBoolType) SimError)]
core)
          Sat (GroundEvalFn t
evalFn, Maybe (ExprRangeBindings t)
_) -> do
            [CrucibleEvent GroundValueWrapper]
evs  <- (forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp))
-> CrucibleAssumptions (Expr t)
-> IO [CrucibleEvent GroundValueWrapper]
forall (e :: BaseType -> *).
IsExpr e =>
(forall (tp :: BaseType). e tp -> IO (GroundValue tp))
-> CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper]
concretizeEvents (GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
groundEval GroundEvalFn t
evalFn) Assumptions sym
CrucibleAssumptions (Expr t)
assumptionsInScope
            let vals :: ModelView
vals = [CrucibleEvent GroundValueWrapper] -> ModelView
evalModelFromEvents [CrucibleEvent GroundValueWrapper]
evs
            Doc Void
explain <- Maybe (GroundEvalFn t) -> Assertion sym -> IO (Doc Void)
explainFailure (GroundEvalFn t -> Maybe (GroundEvalFn t)
forall a. a -> Maybe a
Just GroundEvalFn t
evalFn) Assertion sym
p
            let locs :: [ProgramLoc]
locs = (CrucibleEvent GroundValueWrapper -> ProgramLoc)
-> [CrucibleEvent GroundValueWrapper] -> [ProgramLoc]
forall a b. (a -> b) -> [a] -> [b]
map CrucibleEvent GroundValueWrapper -> ProgramLoc
forall (e :: BaseType -> *). CrucibleEvent e -> ProgramLoc
eventLoc [CrucibleEvent GroundValueWrapper]
evs
            ([ProgramLoc], ProofResult sym)
-> IO ([ProgramLoc], ProofResult sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProgramLoc]
locs, Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
forall sym.
Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
NotProved Doc Void
explain ((ModelView, [CrucibleEvent GroundValueWrapper])
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
forall a. a -> Maybe a
Just (ModelView
vals,[CrucibleEvent GroundValueWrapper]
evs)) [])
          SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
Unknown -> do
            Doc Void
explain <- Maybe (GroundEvalFn t) -> Assertion sym -> IO (Doc Void)
explainFailure Maybe (GroundEvalFn t)
forall a. Maybe a
Nothing Assertion sym
p
            let locs :: [ProgramLoc]
locs = CrucibleAssumptions (Expr t) -> [ProgramLoc]
forall (e :: BaseType -> *). CrucibleAssumptions e -> [ProgramLoc]
assumptionsTopLevelLocs Assumptions sym
CrucibleAssumptions (Expr t)
assumptionsInScope
            ([ProgramLoc], ProofResult sym)
-> IO ([ProgramLoc], ProofResult sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProgramLoc]
locs, Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
forall sym.
Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
NotProved Doc Void
explain Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
forall a. Maybe a
Nothing [])
      where
        -- Create a handle for a file based on the template. For instance, if
        -- the template is @solver-output.smt2@, then create a file named
        -- @solver-output-<goal number>-<solver name>.smt2@.
        withOfflineSolverOutputHandle :: FilePath -> (Handle -> IO r) -> IO r
        withOfflineSolverOutputHandle :: forall r. String -> (Handle -> IO r) -> IO r
withOfflineSolverOutputHandle String
template Handle -> IO r
k =
          let (String
templateName, String
templateExt) = String -> (String, String)
splitExtension String
template
              fileName :: String
fileName = String
templateName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
goalNumber
                                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SolverAdapter st -> String
forall (st :: * -> *). SolverAdapter st -> String
WS.solver_adapter_name SolverAdapter st
adapter
                                     String -> String -> String
<.> String
templateExt in
          String -> IOMode -> (Handle -> IO r) -> IO r
forall r. String -> IOMode -> (Handle -> IO r) -> IO r
withFile String
fileName IOMode
WriteMode Handle -> IO r
k

        -- Lift @withOfflineSolverOutputHandle@ to a @Maybe FilePath@ argument.
        withMaybeOfflineSolverOutputHandle ::
          Maybe FilePath -> (Maybe Handle -> IO r) -> IO r
        withMaybeOfflineSolverOutputHandle :: forall r. Maybe String -> (Maybe Handle -> IO r) -> IO r
withMaybeOfflineSolverOutputHandle Maybe String
mbTemplate Maybe Handle -> IO r
k =
          case Maybe String
mbTemplate of
            Just String
template -> String -> (Handle -> IO r) -> IO r
forall r. String -> (Handle -> IO r) -> IO r
withOfflineSolverOutputHandle String
template (Maybe Handle -> IO r
k (Maybe Handle -> IO r)
-> (Handle -> Maybe Handle) -> Handle -> IO r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> Maybe Handle
forall a. a -> Maybe a
Just)
            Maybe String
Nothing       -> Maybe Handle -> IO r
k Maybe Handle
forall a. Maybe a
Nothing

evalModelFromEvents :: [CrucibleEvent GroundValueWrapper] -> ModelView
evalModelFromEvents :: [CrucibleEvent GroundValueWrapper] -> ModelView
evalModelFromEvents [CrucibleEvent GroundValueWrapper]
evs = MapF BaseTypeRepr Vals -> ModelView
ModelView ((MapF BaseTypeRepr Vals
 -> CrucibleEvent GroundValueWrapper -> MapF BaseTypeRepr Vals)
-> MapF BaseTypeRepr Vals
-> [CrucibleEvent GroundValueWrapper]
-> MapF BaseTypeRepr Vals
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl MapF BaseTypeRepr Vals
-> CrucibleEvent GroundValueWrapper -> MapF BaseTypeRepr Vals
f (ModelView -> MapF BaseTypeRepr Vals
modelVals ModelView
emptyModelView) [CrucibleEvent GroundValueWrapper]
evs)
 where
   f :: MapF BaseTypeRepr Vals
-> CrucibleEvent GroundValueWrapper -> MapF BaseTypeRepr Vals
f MapF BaseTypeRepr Vals
m (CreateVariableEvent ProgramLoc
loc String
nm BaseTypeRepr tp
tpr (GVW GroundValue tp
v)) = (Vals tp -> Vals tp -> Vals tp)
-> BaseTypeRepr tp
-> Vals tp
-> MapF BaseTypeRepr Vals
-> MapF BaseTypeRepr Vals
forall {v} (k :: v -> *) (a :: v -> *) (tp :: v).
OrdF k =>
(a tp -> a tp -> a tp) -> k tp -> a tp -> MapF k a -> MapF k a
MapF.insertWith Vals tp -> Vals tp -> Vals tp
forall {ty :: BaseType} {ty :: BaseType} {ty :: BaseType}.
(GroundValue ty ~ GroundValue ty,
 GroundValue ty ~ GroundValue ty) =>
Vals ty -> Vals ty -> Vals ty
jn BaseTypeRepr tp
tpr ([Entry (GroundValue tp)] -> Vals tp
forall (ty :: BaseType). [Entry (GroundValue ty)] -> Vals ty
Vals [String -> ProgramLoc -> GroundValue tp -> Entry (GroundValue tp)
forall a. String -> ProgramLoc -> a -> Entry a
Entry String
nm ProgramLoc
loc GroundValue tp
v]) MapF BaseTypeRepr Vals
m
   f MapF BaseTypeRepr Vals
m CrucibleEvent GroundValueWrapper
_ = MapF BaseTypeRepr Vals
m

   jn :: Vals ty -> Vals ty -> Vals ty
jn (Vals [Entry (GroundValue ty)]
new) (Vals [Entry (GroundValue ty)]
old) = [Entry (GroundValue ty)] -> Vals ty
forall (ty :: BaseType). [Entry (GroundValue ty)] -> Vals ty
Vals ([Entry (GroundValue ty)]
[Entry (GroundValue ty)]
old[Entry (GroundValue ty)]
-> [Entry (GroundValue ty)] -> [Entry (GroundValue ty)]
forall a. [a] -> [a] -> [a]
++[Entry (GroundValue ty)]
[Entry (GroundValue ty)]
new)

dispatchSolversOnGoalAsync :: forall a b s time.
                              (RealFrac time)
                           => Maybe time
                           -> [WS.SolverAdapter s]
                           -> (WS.SolverAdapter s -> IO (b,ProofResult a))
                           -> IO (Either [SomeException] (Maybe (b,ProofResult a)))
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)))
dispatchSolversOnGoalAsync Maybe time
mtimeoutSeconds [SolverAdapter s]
adapters SolverAdapter s -> IO (b, ProofResult a)
withAdapter = do
  [Async (b, ProofResult a)]
asyncs <- [SolverAdapter s]
-> (SolverAdapter s -> IO (Async (b, ProofResult a)))
-> IO [Async (b, ProofResult a)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [SolverAdapter s]
adapters (IO (b, ProofResult a) -> IO (Async (b, ProofResult a))
forall a. IO a -> IO (Async a)
async (IO (b, ProofResult a) -> IO (Async (b, ProofResult a)))
-> (SolverAdapter s -> IO (b, ProofResult a))
-> SolverAdapter s
-> IO (Async (b, ProofResult a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverAdapter s -> IO (b, ProofResult a)
withAdapter)
  [Async (b, ProofResult a)]
-> [SomeException]
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
await [Async (b, ProofResult a)]
asyncs []
  where
    await :: [Async (b, ProofResult a)]
-> [SomeException]
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
await [] [SomeException]
es = Either [SomeException] (Maybe (b, ProofResult a))
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [SomeException] (Maybe (b, ProofResult a))
 -> IO (Either [SomeException] (Maybe (b, ProofResult a))))
-> Either [SomeException] (Maybe (b, ProofResult a))
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
forall a b. (a -> b) -> a -> b
$ [SomeException]
-> Either [SomeException] (Maybe (b, ProofResult a))
forall a b. a -> Either a b
Left [SomeException]
es
    await [Async (b, ProofResult a)]
as [SomeException]
es = do
      Maybe
  (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
mresult <- IO
  (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
-> IO
     (Maybe
        (Async (b, ProofResult a),
         Either SomeException (b, ProofResult a)))
withTimeout (IO
   (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
 -> IO
      (Maybe
         (Async (b, ProofResult a),
          Either SomeException (b, ProofResult a))))
-> IO
     (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
-> IO
     (Maybe
        (Async (b, ProofResult a),
         Either SomeException (b, ProofResult a)))
forall a b. (a -> b) -> a -> b
$ [Async (b, ProofResult a)]
-> IO
     (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
forall a. [Async a] -> IO (Async a, Either SomeException a)
waitAnyCatch [Async (b, ProofResult a)]
as
      case Maybe
  (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
mresult of
        Just (Async (b, ProofResult a)
a, Either SomeException (b, ProofResult a)
result) -> do
          let as' :: [Async (b, ProofResult a)]
as' = (Async (b, ProofResult a) -> Bool)
-> [Async (b, ProofResult a)] -> [Async (b, ProofResult a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Async (b, ProofResult a) -> Async (b, ProofResult a) -> Bool
forall a. Eq a => a -> a -> Bool
/= Async (b, ProofResult a)
a) [Async (b, ProofResult a)]
as
          case Either SomeException (b, ProofResult a)
result of
            Left  SomeException
exc ->
              [Async (b, ProofResult a)]
-> [SomeException]
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
await [Async (b, ProofResult a)]
as' (SomeException
exc SomeException -> [SomeException] -> [SomeException]
forall a. a -> [a] -> [a]
: [SomeException]
es)
            Right (b
x, r :: ProofResult a
r@(Proved [Either (Assumption a) (Assertion a)]
_)) -> do
              (Async (b, ProofResult a) -> IO ())
-> [Async (b, ProofResult a)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Async (b, ProofResult a) -> IO ()
forall {a}. Async a -> IO ()
kill [Async (b, ProofResult a)]
as'
              Either [SomeException] (Maybe (b, ProofResult a))
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [SomeException] (Maybe (b, ProofResult a))
 -> IO (Either [SomeException] (Maybe (b, ProofResult a))))
-> Either [SomeException] (Maybe (b, ProofResult a))
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
forall a b. (a -> b) -> a -> b
$ Maybe (b, ProofResult a)
-> Either [SomeException] (Maybe (b, ProofResult a))
forall a b. b -> Either a b
Right ((b, ProofResult a) -> Maybe (b, ProofResult a)
forall a. a -> Maybe a
Just (b
x,ProofResult a
r))
            Right (b
x,r :: ProofResult a
r@(NotProved Doc Void
_ (Just (ModelView, [CrucibleEvent GroundValueWrapper])
_) [String]
_)) -> do
              (Async (b, ProofResult a) -> IO ())
-> [Async (b, ProofResult a)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Async (b, ProofResult a) -> IO ()
forall {a}. Async a -> IO ()
kill [Async (b, ProofResult a)]
as'
              Either [SomeException] (Maybe (b, ProofResult a))
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [SomeException] (Maybe (b, ProofResult a))
 -> IO (Either [SomeException] (Maybe (b, ProofResult a))))
-> Either [SomeException] (Maybe (b, ProofResult a))
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
forall a b. (a -> b) -> a -> b
$ Maybe (b, ProofResult a)
-> Either [SomeException] (Maybe (b, ProofResult a))
forall a b. b -> Either a b
Right ((b, ProofResult a) -> Maybe (b, ProofResult a)
forall a. a -> Maybe a
Just (b
x,ProofResult a
r))
            Right (b, ProofResult a)
_ ->
              [Async (b, ProofResult a)]
-> [SomeException]
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
await [Async (b, ProofResult a)]
as' [SomeException]
es
        Maybe
  (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
Nothing -> do
          (Async (b, ProofResult a) -> IO ())
-> [Async (b, ProofResult a)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Async (b, ProofResult a) -> IO ()
forall {a}. Async a -> IO ()
kill [Async (b, ProofResult a)]
as
          Either [SomeException] (Maybe (b, ProofResult a))
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [SomeException] (Maybe (b, ProofResult a))
 -> IO (Either [SomeException] (Maybe (b, ProofResult a))))
-> Either [SomeException] (Maybe (b, ProofResult a))
-> IO (Either [SomeException] (Maybe (b, ProofResult a)))
forall a b. (a -> b) -> a -> b
$ Maybe (b, ProofResult a)
-> Either [SomeException] (Maybe (b, ProofResult a))
forall a b. b -> Either a b
Right (Maybe (b, ProofResult a)
 -> Either [SomeException] (Maybe (b, ProofResult a)))
-> Maybe (b, ProofResult a)
-> Either [SomeException] (Maybe (b, ProofResult a))
forall a b. (a -> b) -> a -> b
$ Maybe (b, ProofResult a)
forall a. Maybe a
Nothing

    withTimeout :: IO
  (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
-> IO
     (Maybe
        (Async (b, ProofResult a),
         Either SomeException (b, ProofResult a)))
withTimeout IO
  (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
action
      | Just time
seconds <- Maybe time
mtimeoutSeconds = Int
-> IO
     (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
-> IO
     (Maybe
        (Async (b, ProofResult a),
         Either SomeException (b, ProofResult a)))
forall a. Int -> IO a -> IO (Maybe a)
ST.timeout (time -> Int
forall b. Integral b => time -> b
forall a b. (RealFrac a, Integral b) => a -> b
round time
seconds Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1000000) IO
  (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
action
      | Bool
otherwise = (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
-> Maybe
     (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
forall a. a -> Maybe a
Just ((Async (b, ProofResult a),
  Either SomeException (b, ProofResult a))
 -> Maybe
      (Async (b, ProofResult a),
       Either SomeException (b, ProofResult a)))
-> IO
     (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
-> IO
     (Maybe
        (Async (b, ProofResult a),
         Either SomeException (b, ProofResult a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO
  (Async (b, ProofResult a), Either SomeException (b, ProofResult a))
action

    -- `cancel` from async blocks until the canceled thread has terminated.
    kill :: Async a -> IO ()
kill Async a
a = ThreadId -> ExitCode -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
throwTo (Async a -> ThreadId
forall a. Async a -> ThreadId
asyncThreadId Async a
a) ExitCode
ExitSuccess


-- | 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.
proverMilestoneCallbacks ::
  Log.Logs msgs =>
  Log.SupportsCruxLogMessage msgs =>
  Goals asmp ast -> IO ProverMilestoneCallbacks
proverMilestoneCallbacks :: forall msgs asmp ast.
(Logs msgs, SupportsCruxLogMessage msgs) =>
Goals asmp ast
-> IO (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
proverMilestoneCallbacks Goals asmp ast
goals = do
  (ProverMilestoneStartGoal
start, ProverMilestoneStartGoal
end, IO ()
finish) <-
    if Getting Bool (OutputConfig msgs) Bool -> OutputConfig msgs -> Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Bool (OutputConfig msgs) Bool
forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Bool -> f Bool) -> OutputConfig msgs -> f (OutputConfig msgs)
quiet Logs msgs
OutputConfig msgs
?outputConfig then
      (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
-> IO (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
silentProverMilestoneCallbacks
    else
      String
-> Int
-> IO (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
prepStatus String
"Checking: " (Goals asmp ast -> Int
forall a b. Goals a b -> Int
countGoals Goals asmp ast
goals)
  (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
-> IO (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( ProverMilestoneStartGoal
start ProverMilestoneStartGoal
-> ProverMilestoneStartGoal -> ProverMilestoneStartGoal
forall a. Semigroup a => a -> a -> a
<> CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux (CruxLogMessage -> IO ())
-> (Integer -> CruxLogMessage) -> ProverMilestoneStartGoal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CruxLogMessage
Log.StartedGoal
    , ProverMilestoneStartGoal
end ProverMilestoneStartGoal
-> ProverMilestoneStartGoal -> ProverMilestoneStartGoal
forall a. Semigroup a => a -> a -> a
<> CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux (CruxLogMessage -> IO ())
-> (Integer -> CruxLogMessage) -> ProverMilestoneStartGoal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CruxLogMessage
Log.EndedGoal
    , IO ()
finish
    )


-- | 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.
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)))
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)))
proveGoalsOnline OnlineBackend goalSolver s st fs
_ CruxOptions
_opts SimCtxt personality sym p
_ctxt Maybe (GroundEvalFn s) -> Assertion sym -> IO (Doc Void)
_explainFailure Maybe (Goals (Assumptions sym) (Assertion sym))
Nothing =
     (ProcessedGoals,
 Maybe
   (Goals
      (CrucibleAssumptions (Expr s))
      (LabeledPred (BoolExpr s) SimError, [ProgramLoc],
       ProofResult (ExprBuilder s st fs))))
-> IO
     (ProcessedGoals,
      Maybe
        (Goals
           (CrucibleAssumptions (Expr s))
           (LabeledPred (BoolExpr s) SimError, [ProgramLoc],
            ProofResult (ExprBuilder s st fs))))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Integer -> Integer -> Integer -> ProcessedGoals
ProcessedGoals Integer
0 Integer
0 Integer
0 Integer
0, Maybe
  (Goals
     (CrucibleAssumptions (Expr s))
     (LabeledPred (BoolExpr s) SimError, [ProgramLoc],
      ProofResult (ExprBuilder s st fs)))
forall a. Maybe a
Nothing)

proveGoalsOnline OnlineBackend goalSolver s st fs
bak CruxOptions
opts SimCtxt personality sym p
_ctxt Maybe (GroundEvalFn s) -> Assertion sym -> IO (Doc Void)
explainFailure (Just Goals (Assumptions sym) (Assertion sym)
gs0) =
  do
     -- send solver interactions to the correct file
     (Text -> IO ()) -> Maybe Text -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ExprBuilder s st fs
-> ConfigOption (BaseStringType Unicode) -> Text -> IO ()
forall sym (t :: BaseType) a.
(IsExprBuilder sym, Opt t a) =>
sym -> ConfigOption t -> a -> IO ()
symCfg ExprBuilder s st fs
sym ConfigOption (BaseStringType Unicode)
solverInteractionFile) ((String -> Text) -> Maybe String -> Maybe Text
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Text
Text.pack (CruxOptions -> Maybe String
onlineSolverOutput CruxOptions
opts))
     -- initial goal count
     IORef ProcessedGoals
goalNum <- ProcessedGoals -> IO (IORef ProcessedGoals)
forall a. a -> IO (IORef a)
newIORef (Integer -> Integer -> Integer -> Integer -> ProcessedGoals
ProcessedGoals Integer
0 Integer
0 Integer
0 Integer
0)
     -- nameMap is a mutable ref to a map from Text to Either (Assumption sym) (Assertion sym)
     IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap <- Map
  Text
  (Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
-> IO
     (IORef
        (Map
           Text
           (Either
              (CrucibleAssumption (Expr s))
              (LabeledPred (BoolExpr s) SimError))))
forall a. a -> IO (IORef a)
newIORef Map
  Text
  (Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
forall k a. Map k a
Map.empty
     Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CruxOptions -> Bool
unsatCores CruxOptions
opts Bool -> Bool -> Bool
&& CruxOptions -> Bool
yicesMCSat CruxOptions
opts) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
       CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
Log.SkippingUnsatCoresBecauseMCSatEnabled
     -- callbacks for starting a goal, ending a goal, and finishing all goals
     (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end,IO ()
finish) <- Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
-> IO (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
forall msgs asmp ast.
(Logs msgs, SupportsCruxLogMessage msgs) =>
Goals asmp ast
-> IO (ProverMilestoneStartGoal, ProverMilestoneStartGoal, IO ())
proverMilestoneCallbacks Goals (Assumptions sym) (Assertion sym)
Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
gs0
     -- make sure online features are enabled
     OptionSetting BaseBoolType
enableOpt <- ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
enableOnlineBackend (ExprBuilder s st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder s st fs
sym)
     [Doc Void]
_ <- OptionSetting BaseBoolType -> Bool -> IO [Doc Void]
forall (tp :: BaseType) a.
Opt tp a =>
OptionSetting tp -> a -> IO [Doc Void]
setOpt OptionSetting BaseBoolType
enableOpt Bool
True
     -- @go@ traverses a proof tree, processing/solving each goal as it traverses it.
     -- It also updates goal count and nameMap
     Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
res <- OnlineBackend goalSolver s st fs
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
-> (SolverProcess s goalSolver
    -> IO
         (Goals
            (CrucibleAssumptions (Expr s))
            (LabeledPred (BoolExpr s) SimError, [ProgramLoc],
             ProofResult sym)))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall solver scope (st :: * -> *) fs a.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> IO a -> (SolverProcess scope solver -> IO a) -> IO a
withSolverProcess OnlineBackend goalSolver s st fs
bak (String
-> [String]
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall a. HasCallStack => String -> [String] -> a
panic String
"proveGoalsOnline" [String
"Online solving not enabled!"]) ((SolverProcess s goalSolver
  -> IO
       (Goals
          (CrucibleAssumptions (Expr s))
          (LabeledPred (BoolExpr s) SimError, [ProgramLoc],
           ProofResult sym)))
 -> IO
      (Goals
         (CrucibleAssumptions (Expr s))
         (LabeledPred (BoolExpr s) SimError, [ProgramLoc],
          ProofResult sym)))
-> (SolverProcess s goalSolver
    -> IO
         (Goals
            (CrucibleAssumptions (Expr s))
            (LabeledPred (BoolExpr s) SimError, [ProgramLoc],
             ProofResult sym)))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall a b. (a -> b) -> a -> b
$ \SolverProcess s goalSolver
sp ->
              SolverProcess s goalSolver
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall (m :: * -> *) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
inNewFrame SolverProcess s goalSolver
sp ((ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> SolverProcess s goalSolver
-> CrucibleAssumptions (Expr s)
-> IORef ProcessedGoals
-> Goals
     (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
-> IORef
     (Map
        Text
        (Either
           (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) SolverProcess s goalSolver
sp CrucibleAssumptions (Expr s)
forall a. Monoid a => a
mempty IORef ProcessedGoals
goalNum Goals (Assumptions sym) (Assertion sym)
Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
gs0 IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap)
     ProcessedGoals
nms <- IORef ProcessedGoals -> IO ProcessedGoals
forall a. IORef a -> IO a
readIORef IORef ProcessedGoals
goalNum
     IO ()
finish
     (ProcessedGoals,
 Maybe
   (Goals
      (CrucibleAssumptions (Expr s))
      (LabeledPred (BoolExpr s) SimError, [ProgramLoc],
       ProofResult sym)))
-> IO
     (ProcessedGoals,
      Maybe
        (Goals
           (CrucibleAssumptions (Expr s))
           (LabeledPred (BoolExpr s) SimError, [ProgramLoc],
            ProofResult sym)))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProcessedGoals
nms, Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
-> Maybe
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall a. a -> Maybe a
Just Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
res)

  where
  sym :: ExprBuilder s st fs
sym = OnlineBackend goalSolver s st fs -> ExprBuilder s st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym OnlineBackend goalSolver s st fs
bak

  bindName :: k -> a -> IORef (Map k a) -> IO ()
bindName k
nm a
p IORef (Map k a)
nameMap = IORef (Map k a) -> (Map k a -> Map k a) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (Map k a)
nameMap (k -> a -> Map k a -> Map k a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
nm a
p)

  hasUnsatCores :: Bool
hasUnsatCores = CruxOptions -> Bool
unsatCores CruxOptions
opts Bool -> Bool -> Bool
&& Bool -> Bool
not (CruxOptions -> Bool
yicesMCSat CruxOptions
opts)

  howManyAbducts :: Word64
howManyAbducts = Word64 -> Maybe Word64 -> Word64
forall a. a -> Maybe a -> a
fromMaybe Word64
0 (CruxOptions -> Maybe Word64
getNAbducts CruxOptions
opts)

  usingAbducts :: Bool
usingAbducts = Word64
howManyAbducts Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
0

  failfast :: Bool
failfast = CruxOptions -> Bool
proofGoalsFailFast CruxOptions
opts

  go :: (ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> SolverProcess s goalSolver
-> CrucibleAssumptions (Expr s)
-> IORef ProcessedGoals
-> Goals
     (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
-> IORef
     (Map
        Text
        (Either
           (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) SolverProcess s goalSolver
sp CrucibleAssumptions (Expr s)
assumptionsInScope IORef ProcessedGoals
gn Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
gs IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap = do
    -- traverse goal tree
    case Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
gs of
      -- case: assumption in context for all the contained goals
      Assuming CrucibleAssumptions (Expr s)
asms Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
gs1 ->
        do [CrucibleAssumption (Expr s)]
ps <- ExprBuilder s st fs
-> Assumptions (ExprBuilder s st fs)
-> IO [Assumption (ExprBuilder s st fs)]
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO [Assumption sym]
flattenAssumptions ExprBuilder s st fs
sym Assumptions (ExprBuilder s st fs)
CrucibleAssumptions (Expr s)
asms
           [CrucibleAssumption (Expr s)]
-> (CrucibleAssumption (Expr s) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [CrucibleAssumption (Expr s)]
ps ((CrucibleAssumption (Expr s) -> IO ()) -> IO ())
-> (CrucibleAssumption (Expr s) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \CrucibleAssumption (Expr s)
asm ->
             Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (CrucibleAssumption (Expr s) -> Bool
forall (e :: BaseType -> *).
IsExpr e =>
CrucibleAssumption e -> Bool
trivialAssumption CrucibleAssumption (Expr s)
asm) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
               -- extract predicate from assumption
               do let p :: BoolExpr s
p = CrucibleAssumption (Expr s) -> BoolExpr s
forall (e :: BaseType -> *). CrucibleAssumption e -> e BaseBoolType
assumptionPred CrucibleAssumption (Expr s)
asm
                  -- create formula, assert to SMT solver, create new name and add to nameMap
                  Text
nm <- Term goalSolver -> IO Text
doAssume (Term goalSolver -> IO Text) -> IO (Term goalSolver) -> IO Text
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< WriterConn s goalSolver -> BoolExpr s -> IO (Term goalSolver)
forall h t.
SMTWriter h =>
WriterConn t h -> BoolExpr t -> IO (Term h)
mkFormula WriterConn s goalSolver
conn BoolExpr s
p
                  Text
-> Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)
-> IORef
     (Map
        Text
        (Either
           (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
-> IO ()
forall {k} {a}. Ord k => k -> a -> IORef (Map k a) -> IO ()
bindName Text
nm (CrucibleAssumption (Expr s)
-> Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)
forall a b. a -> Either a b
Left CrucibleAssumption (Expr s)
asm) IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap
           -- recursive call
           Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
res <- (ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> SolverProcess s goalSolver
-> CrucibleAssumptions (Expr s)
-> IORef ProcessedGoals
-> Goals
     (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
-> IORef
     (Map
        Text
        (Either
           (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) SolverProcess s goalSolver
sp (CrucibleAssumptions (Expr s)
assumptionsInScope CrucibleAssumptions (Expr s)
-> CrucibleAssumptions (Expr s) -> CrucibleAssumptions (Expr s)
forall a. Semigroup a => a -> a -> a
<> CrucibleAssumptions (Expr s)
asms) IORef ProcessedGoals
gn Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
gs1 IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap
           Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CrucibleAssumptions (Expr s)
-> Goals
     (CrucibleAssumptions (Expr s))
     (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
-> Goals
     (CrucibleAssumptions (Expr s))
     (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
forall asmp goal. asmp -> Goals asmp goal -> Goals asmp goal
Assuming ([CrucibleAssumptions (Expr s)] -> CrucibleAssumptions (Expr s)
forall a. Monoid a => [a] -> a
mconcat ((CrucibleAssumption (Expr s) -> CrucibleAssumptions (Expr s))
-> [CrucibleAssumption (Expr s)] -> [CrucibleAssumptions (Expr s)]
forall a b. (a -> b) -> [a] -> [b]
map CrucibleAssumption (Expr s) -> CrucibleAssumptions (Expr s)
forall (e :: BaseType -> *).
CrucibleAssumption e -> CrucibleAssumptions e
singleAssumption [CrucibleAssumption (Expr s)]
ps)) Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
res)
      -- case: proof obligation in the context of all previously-made assumptions
      Prove LabeledPred (BoolExpr s) SimError
p ->
        -- number of processed goals gives goal number to prove
        do Integer
goalNumber <- ProcessedGoals -> Integer
totalProcessedGoals (ProcessedGoals -> Integer) -> IO ProcessedGoals -> IO Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef ProcessedGoals -> IO ProcessedGoals
forall a. IORef a -> IO a
readIORef IORef ProcessedGoals
gn
           ProverMilestoneStartGoal
start Integer
goalNumber
           -- negate goal, create formula
           Term goalSolver
t <- WriterConn s goalSolver -> BoolExpr s -> IO (Term goalSolver)
forall h t.
SMTWriter h =>
WriterConn t h -> BoolExpr t -> IO (Term h)
mkFormula WriterConn s goalSolver
conn (BoolExpr s -> IO (Term goalSolver))
-> IO (BoolExpr s) -> IO (Term goalSolver)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder s st fs
-> Pred (ExprBuilder s st fs) -> IO (Pred (ExprBuilder s st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred ExprBuilder s st fs
sym (LabeledPred (BoolExpr s) SimError
p LabeledPred (BoolExpr s) SimError
-> Getting
     (BoolExpr s) (LabeledPred (BoolExpr s) SimError) (BoolExpr s)
-> BoolExpr s
forall s a. s -> Getting a s a -> a
^. Getting
  (BoolExpr s) (LabeledPred (BoolExpr s) SimError) (BoolExpr s)
forall pred msg pred' (f :: * -> *).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred)
           -- assert formula to SMT solver, create new name and add to nameMap.
           -- This is done in a new assertion frame if abduction is turned on since
           -- this assertion would need to be removed before asking for abducts
           let inNewFrame2ForAbducts :: IO (SMTResult sym) -> IO (SMTResult sym)
inNewFrame2ForAbducts =
                 if Bool
usingAbducts then SolverProcess s goalSolver
-> IO (SMTResult sym) -> IO (SMTResult sym)
forall solver scope a.
SMTReadWriter solver =>
SolverProcess scope solver -> IO a -> IO a
inNewFrame2 SolverProcess s goalSolver
sp else IO (SMTResult sym) -> IO (SMTResult sym)
forall a. a -> a
id
           SMTResult sym
ret <- IO (SMTResult sym) -> IO (SMTResult sym)
inNewFrame2ForAbducts (IO (SMTResult sym) -> IO (SMTResult sym))
-> IO (SMTResult sym) -> IO (SMTResult sym)
forall a b. (a -> b) -> a -> b
$ do
             Text
nm <- Term goalSolver -> IO Text
doAssume Term goalSolver
t
             Text
-> Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)
-> IORef
     (Map
        Text
        (Either
           (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
-> IO ()
forall {k} {a}. Ord k => k -> a -> IORef (Map k a) -> IO ()
bindName Text
nm (LabeledPred (BoolExpr s) SimError
-> Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)
forall a b. b -> Either a b
Right LabeledPred (BoolExpr s) SimError
p) IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap
             -- check-sat with SMT solver, pattern match on result
             SatResult () ()
res <- SolverProcess s goalSolver -> String -> IO (SatResult () ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> String -> IO (SatResult () ())
check SolverProcess s goalSolver
sp String
"proof"
             case SatResult () ()
res of
               Unsat () ->
                 -- build unsat core, which is the entire assertion set by default
                 do Map
  Text
  (Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
namemap <- IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
-> IO
     (Map
        Text
        (Either
           (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
forall a. IORef a -> IO a
readIORef IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap
                    [Either
   (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)]
core <- if Bool
hasUnsatCores then
                               (Text
 -> Either
      (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
-> [Text]
-> [Either
      (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)]
forall a b. (a -> b) -> [a] -> [b]
map (Map
  Text
  (Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
-> Text
-> Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)
forall {k} {a}. (Show k, Ord k) => Map k a -> k -> a
lookupnm Map
  Text
  (Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
namemap) ([Text]
 -> [Either
       (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)])
-> IO [Text]
-> IO
     [Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SolverProcess s goalSolver -> IO [Text]
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO [Text]
getUnsatCore SolverProcess s goalSolver
sp
                            -- default unsat core: entire assertion set
                            else [Either
   (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)]
-> IO
     [Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map
  Text
  (Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
-> [Either
      (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)]
forall k a. Map k a -> [a]
Map.elems Map
  Text
  (Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
namemap)
                    let locs :: [ProgramLoc]
locs = CrucibleAssumptions (Expr s) -> [ProgramLoc]
forall (e :: BaseType -> *). CrucibleAssumptions e -> [ProgramLoc]
assumptionsTopLevelLocs CrucibleAssumptions (Expr s)
assumptionsInScope
                    SMTResult sym -> IO (SMTResult sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTResult sym -> IO (SMTResult sym))
-> SMTResult sym -> IO (SMTResult sym)
forall a b. (a -> b) -> a -> b
$ [Either (Assumption sym) (Assertion sym)]
-> [ProgramLoc] -> SMTResult sym
forall sym.
[Either (Assumption sym) (Assertion sym)]
-> [ProgramLoc] -> SMTResult sym
UnsatResult [Either (Assumption sym) (Assertion sym)]
[Either
   (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)]
core [ProgramLoc]
locs
               Sat ()  ->
                 do -- evaluate counter-example
                    GroundEvalFn s
f <- WriterConn s goalSolver
-> SMTEvalFunctions goalSolver -> IO (GroundEvalFn s)
forall t h.
SMTWriter h =>
WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
smtExprGroundEvalFn WriterConn s goalSolver
conn (SolverProcess s goalSolver -> SMTEvalFunctions goalSolver
forall scope solver.
SolverProcess scope solver -> SMTEvalFunctions solver
solverEvalFuns SolverProcess s goalSolver
sp)
                    [CrucibleEvent GroundValueWrapper]
evs <- (forall (tp :: BaseType). Expr s tp -> IO (GroundValue tp))
-> CrucibleAssumptions (Expr s)
-> IO [CrucibleEvent GroundValueWrapper]
forall (e :: BaseType -> *).
IsExpr e =>
(forall (tp :: BaseType). e tp -> IO (GroundValue tp))
-> CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper]
concretizeEvents (GroundEvalFn s
-> forall (tp :: BaseType). Expr s tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
groundEval GroundEvalFn s
f) CrucibleAssumptions (Expr s)
assumptionsInScope
                    Doc Void
explain <- Maybe (GroundEvalFn s) -> Assertion sym -> IO (Doc Void)
explainFailure (GroundEvalFn s -> Maybe (GroundEvalFn s)
forall a. a -> Maybe a
Just GroundEvalFn s
f) Assertion sym
LabeledPred (BoolExpr s) SimError
p
                    SMTResult sym -> IO (SMTResult sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTResult sym -> IO (SMTResult sym))
-> SMTResult sym -> IO (SMTResult sym)
forall a b. (a -> b) -> a -> b
$ Doc Void -> [CrucibleEvent GroundValueWrapper] -> SMTResult sym
forall sym.
Doc Void -> [CrucibleEvent GroundValueWrapper] -> SMTResult sym
SatResult Doc Void
explain [CrucibleEvent GroundValueWrapper]
evs
               SatResult () ()
Unknown ->
                 do Doc Void
explain <- Maybe (GroundEvalFn s) -> Assertion sym -> IO (Doc Void)
explainFailure Maybe (GroundEvalFn s)
forall a. Maybe a
Nothing Assertion sym
LabeledPred (BoolExpr s) SimError
p
                    let locs :: [ProgramLoc]
locs = CrucibleAssumptions (Expr s) -> [ProgramLoc]
forall (e :: BaseType -> *). CrucibleAssumptions e -> [ProgramLoc]
assumptionsTopLevelLocs CrucibleAssumptions (Expr s)
assumptionsInScope
                    SMTResult sym -> IO (SMTResult sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTResult sym -> IO (SMTResult sym))
-> SMTResult sym -> IO (SMTResult sym)
forall a b. (a -> b) -> a -> b
$ Doc Void -> [ProgramLoc] -> SMTResult sym
forall sym. Doc Void -> [ProgramLoc] -> SMTResult sym
UnknownResult Doc Void
explain [ProgramLoc]
locs
           ProverMilestoneStartGoal
end Integer
goalNumber
           LabeledPred (BoolExpr s) SimError
-> SMTResult sym
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall asmp.
LabeledPred (BoolExpr s) SimError
-> SMTResult sym
-> IO
     (Goals
        asmp
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
smtResultToGoals LabeledPred (BoolExpr s) SimError
p SMTResult sym
ret
      -- case: conjunction of goals
      ProveConj Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
g1 Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
g2 ->
        do Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
g1' <- SolverProcess s goalSolver
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall (m :: * -> *) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
inNewFrame SolverProcess s goalSolver
sp ((ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> SolverProcess s goalSolver
-> CrucibleAssumptions (Expr s)
-> IORef ProcessedGoals
-> Goals
     (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
-> IORef
     (Map
        Text
        (Either
           (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) SolverProcess s goalSolver
sp CrucibleAssumptions (Expr s)
assumptionsInScope IORef ProcessedGoals
gn Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
g1 IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap)
           -- NB, we don't need 'inNewFrame' here because
           --  we don't need to back up to this point again.
           if Bool
failfast then
             do Integer
numDisproved <- ProcessedGoals -> Integer
disprovedGoals (ProcessedGoals -> Integer) -> IO ProcessedGoals -> IO Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef ProcessedGoals -> IO ProcessedGoals
forall a. IORef a -> IO a
readIORef IORef ProcessedGoals
gn
                if Integer
numDisproved Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then
                  Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
g1'
                else
                  Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
-> Goals
     (CrucibleAssumptions (Expr s))
     (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
-> Goals
     (CrucibleAssumptions (Expr s))
     (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
forall asmp goal.
Goals asmp goal -> Goals asmp goal -> Goals asmp goal
ProveConj Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
g1' (Goals
   (CrucibleAssumptions (Expr s))
   (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
 -> Goals
      (CrucibleAssumptions (Expr s))
      (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> SolverProcess s goalSolver
-> CrucibleAssumptions (Expr s)
-> IORef ProcessedGoals
-> Goals
     (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
-> IORef
     (Map
        Text
        (Either
           (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) SolverProcess s goalSolver
sp CrucibleAssumptions (Expr s)
assumptionsInScope IORef ProcessedGoals
gn Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
g2 IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap
           else
             Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
-> Goals
     (CrucibleAssumptions (Expr s))
     (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
-> Goals
     (CrucibleAssumptions (Expr s))
     (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
forall asmp goal.
Goals asmp goal -> Goals asmp goal -> Goals asmp goal
ProveConj Goals
  (CrucibleAssumptions (Expr s))
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
g1' (Goals
   (CrucibleAssumptions (Expr s))
   (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
 -> Goals
      (CrucibleAssumptions (Expr s))
      (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ProverMilestoneStartGoal, ProverMilestoneStartGoal)
-> SolverProcess s goalSolver
-> CrucibleAssumptions (Expr s)
-> IORef ProcessedGoals
-> Goals
     (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
-> IORef
     (Map
        Text
        (Either
           (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
-> IO
     (Goals
        (CrucibleAssumptions (Expr s))
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
go (ProverMilestoneStartGoal
start,ProverMilestoneStartGoal
end) SolverProcess s goalSolver
sp CrucibleAssumptions (Expr s)
assumptionsInScope IORef ProcessedGoals
gn Goals
  (CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
g2 IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap

    where
    conn :: WriterConn s goalSolver
conn = SolverProcess s goalSolver -> WriterConn s goalSolver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess s goalSolver
sp

    lookupnm :: Map k a -> k -> a
lookupnm Map k a
namemap k
x =
      a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Named predicate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" not found!")
                (k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
x Map k a
namemap)

    doAssume :: Term goalSolver -> IO Text
doAssume Term goalSolver
formula = do
      Map
  Text
  (Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
namemap <- IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
-> IO
     (Map
        Text
        (Either
           (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
forall a. IORef a -> IO a
readIORef IORef
  (Map
     Text
     (Either
        (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError)))
nameMap
      if Bool
hasUnsatCores
      then WriterConn s goalSolver -> Term goalSolver -> IO Text
forall h t. SMTWriter h => WriterConn t h -> Term h -> IO Text
assumeFormulaWithFreshName WriterConn s goalSolver
conn Term goalSolver
formula
      else WriterConn s goalSolver -> Term goalSolver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Term h -> IO ()
assumeFormula WriterConn s goalSolver
conn Term goalSolver
formula IO () -> IO Text -> IO Text
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Text -> IO Text
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Text
Text.pack (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Map
  Text
  (Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
-> Int
forall k a. Map k a -> Int
Map.size Map
  Text
  (Either
     (CrucibleAssumption (Expr s)) (LabeledPred (BoolExpr s) SimError))
namemap)))

    -- Convert an 'SMTResult' to a 'ProofResult'. This function should be
    -- called /after/ 'inNewFrame2' so that the abducts can be queried properly
    -- in the SatResult case.
    smtResultToGoals :: LabeledPred (BoolExpr s) SimError
                     -> SMTResult sym
                     -> IO ( Goals asmp (LabeledPred (BoolExpr s) SimError
                           , [ProgramLoc]
                           , ProofResult sym)
                           )
    smtResultToGoals :: forall asmp.
LabeledPred (BoolExpr s) SimError
-> SMTResult sym
-> IO
     (Goals
        asmp
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
smtResultToGoals LabeledPred (BoolExpr s) SimError
p SMTResult sym
smtRes = do
      ([ProgramLoc]
locs, ProofResult sym
gt) <- case SMTResult sym
smtRes of
        UnsatResult [Either (Assumption sym) (Assertion sym)]
core [ProgramLoc]
locs -> do
          let pr :: ProofResult sym
pr = [Either (Assumption sym) (Assertion sym)] -> ProofResult sym
forall sym.
[Either (Assumption sym) (Assertion sym)] -> ProofResult sym
Proved [Either (Assumption sym) (Assertion sym)]
core
          ([ProgramLoc], ProofResult sym)
-> IO ([ProgramLoc], ProofResult sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProgramLoc]
locs, ProofResult sym
pr)
        SatResult Doc Void
explain [CrucibleEvent GroundValueWrapper]
evs -> do
          let vals :: ModelView
vals = [CrucibleEvent GroundValueWrapper] -> ModelView
evalModelFromEvents [CrucibleEvent GroundValueWrapper]
evs
          [String]
abds <- if Bool
usingAbducts then
                    SolverProcess s goalSolver
-> Int -> Text -> BoolExpr s -> IO [String]
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> Int -> Text -> BoolExpr scope -> IO [String]
getAbducts SolverProcess s goalSolver
sp (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
howManyAbducts) Text
"abd" (LabeledPred (BoolExpr s) SimError
p LabeledPred (BoolExpr s) SimError
-> Getting
     (BoolExpr s) (LabeledPred (BoolExpr s) SimError) (BoolExpr s)
-> BoolExpr s
forall s a. s -> Getting a s a -> a
^. Getting
  (BoolExpr s) (LabeledPred (BoolExpr s) SimError) (BoolExpr s)
forall pred msg pred' (f :: * -> *).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred)
                  else
                    [String] -> IO [String]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
          let gt :: ProofResult sym
gt = Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
forall sym.
Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
NotProved Doc Void
explain ((ModelView, [CrucibleEvent GroundValueWrapper])
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
forall a. a -> Maybe a
Just (ModelView
vals,[CrucibleEvent GroundValueWrapper]
evs)) [String]
abds
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
failfast Bool -> Bool -> Bool
&& Bool -> Bool
not (LabeledPred (BoolExpr s) SimError -> Bool
forall p. LabeledPred p SimError -> Bool
isResourceExhausted LabeledPred (BoolExpr s) SimError
p)) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
            CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
Log.FoundCounterExample
          let locs :: [ProgramLoc]
locs = (CrucibleEvent GroundValueWrapper -> ProgramLoc)
-> [CrucibleEvent GroundValueWrapper] -> [ProgramLoc]
forall a b. (a -> b) -> [a] -> [b]
map CrucibleEvent GroundValueWrapper -> ProgramLoc
forall (e :: BaseType -> *). CrucibleEvent e -> ProgramLoc
eventLoc [CrucibleEvent GroundValueWrapper]
evs
          ([ProgramLoc], ProofResult sym)
-> IO ([ProgramLoc], ProofResult sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProgramLoc]
locs, ProofResult sym
gt)
        UnknownResult Doc Void
explain [ProgramLoc]
locs -> do
          let gt :: ProofResult sym
gt = Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
forall sym.
Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> [String]
-> ProofResult sym
NotProved Doc Void
explain Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
forall a. Maybe a
Nothing []
          ([ProgramLoc], ProofResult sym)
-> IO ([ProgramLoc], ProofResult sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProgramLoc]
locs, ProofResult sym
gt)

      -- update goal count
      IORef ProcessedGoals -> (ProcessedGoals -> ProcessedGoals) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef ProcessedGoals
gn (LabeledPred (BoolExpr s) SimError
-> ProofResult sym -> ProcessedGoals -> ProcessedGoals
forall p a.
LabeledPred p SimError
-> ProofResult a -> ProcessedGoals -> ProcessedGoals
updateProcessedGoals LabeledPred (BoolExpr s) SimError
p ProofResult sym
gt)
      Goals
  asmp
  (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
-> IO
     (Goals
        asmp
        (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
-> Goals
     asmp
     (LabeledPred (BoolExpr s) SimError, [ProgramLoc], ProofResult sym)
forall asmp goal. goal -> Goals asmp goal
Prove (LabeledPred (BoolExpr s) SimError
p, [ProgramLoc]
locs, ProofResult sym
gt))

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

-- TODO: Upstream this to @what4@ (Issue what4#218).
inNewFrame2 :: SMTReadWriter solver => SolverProcess scope solver -> IO a -> IO a
inNewFrame2 :: forall solver scope a.
SMTReadWriter solver =>
SolverProcess scope solver -> IO a -> IO a
inNewFrame2 SolverProcess scope solver
sp IO a
action = do
  SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
inNewFrame2Open SolverProcess scope solver
sp
  a
val <- IO a
action
  SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
inNewFrame2Close SolverProcess scope solver
sp
  a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
val

-- | An intermediate data structure used in 'proveGoalsOnline'. This can be
-- thought of as a halfway point between a 'SatResult' and a 'ProofResult'.
data SMTResult sym
  = UnsatResult [Either (Assumption sym) (Assertion sym)]
                [ProgramLoc]
  | SatResult (Doc Void)
              [CrucibleEvent GroundValueWrapper]
  | UnknownResult (Doc Void)
                  [ProgramLoc]