{-# 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 ()
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 }
type Explainer sym t ann = Maybe (GroundEvalFn t)
-> LPred sym SimError
-> IO (Doc ann)
type ProverCallback sym =
forall ext personality t st fs.
(sym ~ ExprBuilder t st fs) =>
CruxOptions ->
SimCtxt personality sym ext ->
Explainer sym t Void ->
Maybe (Goals (Assumptions sym) (Assertion sym)) ->
IO (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)))
proveGoalsOffline :: forall st sym p t fs personality msgs.
( sym ~ ExprBuilder t st fs
, Logs msgs
, SupportsCruxLogMessage msgs
) =>
[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
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 =
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
[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
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
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
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
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
)
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
(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))
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)
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
(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
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
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
case Goals
(CrucibleAssumptions (Expr s)) (LabeledPred (BoolExpr s) SimError)
gs of
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
$
do let p :: BoolExpr s
p = CrucibleAssumption (Expr s) -> BoolExpr s
forall (e :: BaseType -> *). CrucibleAssumption e -> e BaseBoolType
assumptionPred CrucibleAssumption (Expr s)
asm
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
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)
Prove LabeledPred (BoolExpr s) SimError
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
gn
ProverMilestoneStartGoal
start Integer
goalNumber
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)
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
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 () ->
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
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
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
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)
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)))
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)
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))
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
data SMTResult sym
= UnsatResult [Either (Assumption sym) (Assertion sym)]
[ProgramLoc]
| SatResult (Doc Void)
[CrucibleEvent GroundValueWrapper]
| UnknownResult (Doc Void)
[ProgramLoc]