{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# Language RankNTypes, ImplicitParams, TypeApplications, MultiWayIf #-}
{-# Language OverloadedStrings, FlexibleContexts, ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
module Crux
( runSimulator
, postprocessSimResult
, loadOptions
, mkOutputConfig
, defaultOutputConfig
, SimulatorCallbacks(..)
, SimulatorHooks(..)
, RunnableState(..)
, pattern RunnableState
, Explainer
, CruxOptions(..)
, SomeOnlineSolver(..)
, Crux(..)
, module Crux.Config
, module Crux.Log
) where
import qualified Control.Exception as Ex
import Control.Lens
import Control.Monad ( unless, void, when )
import qualified Data.Aeson as JSON
import Data.Foldable
import Data.Functor.Contravariant ( (>$<) )
import Data.Functor.Contravariant.Divisible ( divide )
import Data.Generics.Product.Fields (field)
import Data.IORef
import Data.Maybe ( fromMaybe )
import qualified Data.Sequence as Seq
import Data.Text (Text)
import qualified Data.Text as T
import Data.Version (Version)
import Data.Void (Void)
import qualified Lumberjack as LJ
import Prettyprinter
import qualified System.Console.ANSI as AC
import System.Console.Terminal.Size (Window(Window), size)
import System.Directory (createDirectoryIfMissing)
import System.Exit (exitSuccess, ExitCode(..), exitFailure, exitWith)
import System.FilePath ((</>))
import System.IO ( Handle, hPutStr, stdout, stderr )
import Data.Parameterized.Classes
import Data.Parameterized.Nonce (newIONonceGenerator, NonceGenerator)
import Data.Parameterized.Some ( Some(..) )
import Lang.Crucible.Backend
import Lang.Crucible.Backend.Online
import qualified Lang.Crucible.Backend.Simple as CBS
import Lang.Crucible.CFG.Extension
import Lang.Crucible.Simulator
import Lang.Crucible.Simulator.BoundedExec
import Lang.Crucible.Simulator.BoundedRecursion
import Lang.Crucible.Simulator.PathSatisfiability
import Lang.Crucible.Simulator.PathSplitting
import Lang.Crucible.Simulator.PositionTracking
import Lang.Crucible.Simulator.Profiling
import Lang.Crucible.Types
import What4.Config (setOpt, getOptionSetting, verbosity, extendConfig)
import qualified What4.Expr as WE
import What4.FunctionName (FunctionName)
import What4.Interface (IsExprBuilder, getConfiguration)
import What4.InterpretedFloatingPoint (IsInterpretedFloatExprBuilder)
import What4.Protocol.Online (OnlineSolver)
import qualified What4.Solver as WS
import What4.Solver.CVC4 (cvc4Timeout)
import What4.Solver.CVC5 (cvc5Timeout)
import What4.Solver.Yices (yicesEnableMCSat, yicesGoalTimeout)
import What4.Solver.Z3 (z3Timeout)
import Crux.Config
import Crux.Config.Common
import Crux.Config.Doc
import qualified Crux.Config.Load as Cfg
import qualified Crux.Config.Solver as CCS
import Crux.FormatOut ( sayWhatFailedGoals, sayWhatResultStatus )
import Crux.Goal
import Crux.Log
import Crux.Log as Log
import Crux.Report
import Crux.Types
pattern RunnableState :: forall sym . () => forall ext personality . (IsSyntaxExtension ext) => ExecState (personality sym) sym ext (RegEntry sym UnitType) -> RunnableState sym
pattern $mRunnableState :: forall {r} {sym}.
RunnableState sym
-> (forall {ext} {personality :: * -> *}.
IsSyntaxExtension ext =>
ExecState (personality sym) sym ext (RegEntry sym UnitType) -> r)
-> ((# #) -> r)
-> r
$bRunnableState :: forall sym ext (personality :: * -> *).
IsSyntaxExtension ext =>
ExecState (personality sym) sym ext (RegEntry sym UnitType)
-> RunnableState sym
RunnableState es = RunnableStateWithExtensions es []
data RunnableState sym where
RunnableStateWithExtensions :: (IsSyntaxExtension ext)
=> ExecState (personality sym) sym ext (RegEntry sym UnitType)
-> [ExecutionFeature (personality sym) sym ext (RegEntry sym UnitType)]
-> RunnableState sym
newtype SimulatorCallbacks msgs r
= SimulatorCallbacks
{ forall msgs r.
SimulatorCallbacks msgs r
-> forall sym bak t (st :: * -> *) fs.
(IsSymBackend sym bak, Logs msgs, sym ~ ExprBuilder t st fs) =>
IO (SimulatorHooks sym bak t r)
getSimulatorCallbacks ::
forall sym bak t st fs.
( IsSymBackend sym bak
, Logs msgs
, sym ~ WE.ExprBuilder t st fs
) =>
IO (SimulatorHooks sym bak t r)
}
data SomeOnlineSolver sym bak where
SomeOnlineSolver :: ( sym ~ WE.ExprBuilder scope st fs
, bak ~ OnlineBackend solver scope st fs
, IsSymBackend sym bak
, OnlineSolver solver
) => bak -> SomeOnlineSolver sym bak
data SimulatorHooks sym bak t r =
SimulatorHooks
{ forall sym bak t r.
SimulatorHooks sym bak t r
-> bak
-> Maybe (SomeOnlineSolver sym bak)
-> IO (RunnableState sym)
setupHook :: bak -> Maybe (SomeOnlineSolver sym bak) -> IO (RunnableState sym)
, forall sym bak t r.
SimulatorHooks sym bak t r -> bak -> IO (Explainer sym t Void)
onErrorHook :: bak -> IO (Explainer sym t Void)
, forall sym bak t r.
SimulatorHooks sym bak t r -> bak -> CruxSimulationResult -> IO r
resultHook :: bak -> CruxSimulationResult -> IO r
}
postprocessSimResult ::
Logs msgs =>
Bool -> CruxOptions -> CruxSimulationResult -> IO ExitCode
postprocessSimResult :: forall msgs.
Logs msgs =>
Bool -> CruxOptions -> CruxSimulationResult -> IO ExitCode
postprocessSimResult Bool
showFailedGoals CruxOptions
opts CruxSimulationResult
res =
do
Bool -> CruxSimulationResult -> IO ()
forall msgs. Logs msgs => Bool -> CruxSimulationResult -> IO ()
logSimResult Bool
showFailedGoals CruxSimulationResult
res
CruxOptions -> CruxSimulationResult -> IO ()
generateReport CruxOptions
opts CruxSimulationResult
res
ExitCode -> IO ExitCode
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode -> IO ExitCode) -> ExitCode -> IO ExitCode
forall a b. (a -> b) -> a -> b
$! CruxSimulationResult -> ExitCode
computeExitCode CruxSimulationResult
res
loadOptions ::
SupportsCruxLogMessage msgs =>
(Maybe OutputOptions -> OutputConfig msgs) ->
Text ->
Version ->
Config opts ->
(Logs msgs => (CruxOptions, opts) -> IO a) ->
IO a
loadOptions :: forall msgs opts a.
SupportsCruxLogMessage msgs =>
(Maybe OutputOptions -> OutputConfig msgs)
-> Text
-> Version
-> Config opts
-> (Logs msgs => (CruxOptions, opts) -> IO a)
-> IO a
loadOptions Maybe OutputOptions -> OutputConfig msgs
mkOutCfg Text
nm Version
ver Config opts
config Logs msgs => (CruxOptions, opts) -> IO a
cont =
do let optSpec :: Config (CruxOptions, opts)
optSpec = Config CruxOptions -> Config opts -> Config (CruxOptions, opts)
forall a b. Config a -> Config b -> Config (a, b)
cfgJoin Config CruxOptions
cruxOptions Config opts
config
(ColorOptions
copts, Options (CruxOptions, opts)
opts) <- Text
-> Config (CruxOptions, opts)
-> IO (ColorOptions, Options (CruxOptions, opts))
forall opts. Text -> Config opts -> IO (ColorOptions, Options opts)
Cfg.loadConfig Text
nm Config (CruxOptions, opts)
optSpec
case Options (CruxOptions, opts)
opts of
Options (CruxOptions, opts)
Cfg.ShowHelp ->
do let ?outputConfig = Maybe OutputOptions -> OutputConfig msgs
mkOutCfg (OutputOptions -> Maybe OutputOptions
forall a. a -> Maybe a
Just (ColorOptions -> OutputOptions
defaultOutputOptions ColorOptions
copts))
Text -> Config (CruxOptions, opts) -> IO ()
forall msgs opts.
(Logs msgs, SupportsCruxLogMessage msgs) =>
Text -> Config opts -> IO ()
showHelp Text
nm Config (CruxOptions, opts)
optSpec
IO a
forall a. IO a
exitSuccess
Options (CruxOptions, opts)
Cfg.ShowVersion ->
do let ?outputConfig = Maybe OutputOptions -> OutputConfig msgs
mkOutCfg (OutputOptions -> Maybe OutputOptions
forall a. a -> Maybe a
Just (ColorOptions -> OutputOptions
defaultOutputOptions ColorOptions
copts))
Text -> Version -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
Text -> Version -> IO ()
showVersion Text
nm Version
ver
IO a
forall a. IO a
exitSuccess
Cfg.Options (CruxOptions
cruxWithoutColorOptions, opts
os) [FilePath]
files ->
do let crux :: CruxOptions
crux = ASetter CruxOptions CruxOptions ColorOptions ColorOptions
-> ColorOptions -> CruxOptions -> CruxOptions
forall s t a b. ASetter s t a b -> b -> s -> t
set (forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"outputOptions" ((OutputOptions -> Identity OutputOptions)
-> CruxOptions -> Identity CruxOptions)
-> ((ColorOptions -> Identity ColorOptions)
-> OutputOptions -> Identity OutputOptions)
-> ASetter CruxOptions CruxOptions ColorOptions ColorOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"colorOptions") ColorOptions
copts CruxOptions
cruxWithoutColorOptions
let ?outputConfig = Maybe OutputOptions -> OutputConfig msgs
mkOutCfg (OutputOptions -> Maybe OutputOptions
forall a. a -> Maybe a
Just (CruxOptions -> OutputOptions
outputOptions CruxOptions
crux))
CruxOptions
crux' <- CruxOptions -> IO CruxOptions
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
postprocessOptions CruxOptions
crux { inputFiles = files ++ inputFiles crux }
Logs msgs => (CruxOptions, opts) -> IO a
(CruxOptions, opts) -> IO a
cont (CruxOptions
crux', opts
os)
IO a -> (SomeException -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`Ex.catch` \(SomeException
e :: Ex.SomeException) ->
do let ?outputConfig = Maybe OutputOptions -> OutputConfig msgs
mkOutCfg Maybe OutputOptions
forall a. Maybe a
Nothing
case (SomeException -> Maybe ExitCode
forall e. Exception e => SomeException -> Maybe e
Ex.fromException SomeException
e :: Maybe ExitCode) of
Just ExitCode
exitCode -> ExitCode -> IO a
forall a. ExitCode -> IO a
exitWith ExitCode
exitCode
Maybe ExitCode
Nothing -> SomeException -> IO ()
forall msgs. Logs msgs => SomeException -> IO ()
logException SomeException
e IO () -> IO a -> IO a
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO a
forall a. IO a
exitFailure
showHelp ::
Logs msgs =>
SupportsCruxLogMessage msgs =>
Text -> Config opts -> IO ()
showHelp :: forall msgs opts.
(Logs msgs, SupportsCruxLogMessage msgs) =>
Text -> Config opts -> IO ()
showHelp Text
nm Config opts
cfg = do
Int
outWidth <- Int -> (Window Int -> Int) -> Maybe (Window Int) -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
80 (\(Window Int
_ Int
w) -> Int
w) (Maybe (Window Int) -> Int) -> IO (Maybe (Window Int)) -> IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (Maybe (Window Int))
forall n. Integral n => IO (Maybe (Window n))
size
let opts :: LayoutOptions
opts = PageWidth -> LayoutOptions
LayoutOptions (PageWidth -> LayoutOptions) -> PageWidth -> LayoutOptions
forall a b. (a -> b) -> a -> b
$ Int -> Double -> PageWidth
AvailablePerLine Int
outWidth Double
0.98
CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux (LogDoc -> CruxLogMessage
Log.Help (SimpleDocStream () -> LogDoc
LogDoc (LayoutOptions -> Doc () -> SimpleDocStream ()
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty LayoutOptions
opts (Text -> Config opts -> Doc ()
forall opts ann. Text -> Config opts -> Doc ann
configDocs Text
nm Config opts
cfg))))
showVersion ::
Logs msgs =>
SupportsCruxLogMessage msgs =>
Text -> Version -> IO ()
showVersion :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
Text -> Version -> IO ()
showVersion Text
nm Version
ver = CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux (Text -> Version -> CruxLogMessage
Log.Version Text
nm Version
ver)
mkOutputConfig ::
JSON.ToJSON msgs =>
(Handle, Bool) -> (Handle, Bool) ->
(msgs -> SayWhat) -> Maybe OutputOptions ->
OutputConfig msgs
mkOutputConfig :: forall msgs.
ToJSON msgs =>
(Handle, Bool)
-> (Handle, Bool)
-> (msgs -> SayWhat)
-> Maybe OutputOptions
-> OutputConfig msgs
mkOutputConfig (Handle
outHandle, Bool
outWantsColor) (Handle
errHandle, Bool
errWantsColor) msgs -> SayWhat
logMessageToSayWhat Maybe OutputOptions
opts =
let consensusBetween :: Bool -> Maybe Bool -> Bool
consensusBetween Bool
wants Maybe Bool
maybeRefuses = Bool
wants Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False Maybe Bool
maybeRefuses)
copts :: Maybe ColorOptions
copts = OutputOptions -> ColorOptions
colorOptions (OutputOptions -> ColorOptions)
-> Maybe OutputOptions -> Maybe ColorOptions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe OutputOptions
opts
outSpec :: (Handle, Bool)
outSpec = (Handle
outHandle, Bool -> Maybe Bool -> Bool
consensusBetween Bool
outWantsColor (ColorOptions -> Bool
Cfg.noColorsOut (ColorOptions -> Bool) -> Maybe ColorOptions -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ColorOptions
copts))
errSpec :: (Handle, Bool)
errSpec@(Handle
_, Bool
errShouldColor) = (Handle
errHandle, Bool -> Maybe Bool -> Bool
consensusBetween Bool
errWantsColor (ColorOptions -> Bool
Cfg.noColorsErr (ColorOptions -> Bool) -> Maybe ColorOptions -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ColorOptions
copts))
lgWhat :: LogAction IO SayWhat
lgWhat = let la :: LogAction IO SayWhat
la = (SayWhat -> IO ()) -> LogAction IO SayWhat
forall (m :: * -> *) msg. (msg -> m ()) -> LogAction m msg
LJ.LogAction ((SayWhat -> IO ()) -> LogAction IO SayWhat)
-> (SayWhat -> IO ()) -> LogAction IO SayWhat
forall a b. (a -> b) -> a -> b
$ (Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO ()
logToStd (Handle, Bool)
outSpec (Handle, Bool)
errSpec
baseline :: SayLevel
baseline = if Bool -> (OutputOptions -> Bool) -> Maybe OutputOptions -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Int -> Bool) -> (OutputOptions -> Int) -> OutputOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputOptions -> Int
simVerbose) Maybe OutputOptions
opts
then SayLevel
Noisily
else SayLevel
Simply
in if Bool
beQuiet
then SayLevel -> SayWhat -> SayWhat
logfltr SayLevel
OK (SayWhat -> SayWhat)
-> LogAction IO SayWhat -> LogAction IO SayWhat
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< LogAction IO SayWhat
la
else SayLevel -> SayWhat -> SayWhat
logfltr SayLevel
baseline (SayWhat -> SayWhat)
-> LogAction IO SayWhat -> LogAction IO SayWhat
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< LogAction IO SayWhat
la
beQuiet :: Bool
beQuiet = Bool -> (OutputOptions -> Bool) -> Maybe OutputOptions -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False OutputOptions -> Bool
quietMode Maybe OutputOptions
opts
logfltr :: SayLevel -> SayWhat -> SayWhat
logfltr SayLevel
allowed = \case
SayWhat
SayNothing -> SayWhat
SayNothing
w :: SayWhat
w@(SayWhat SayLevel
lvl Text
_ Text
_) -> if SayLevel
lvl SayLevel -> SayLevel -> Bool
forall a. Ord a => a -> a -> Bool
>= SayLevel
allowed then SayWhat
w else SayWhat
SayNothing
SayMore SayWhat
m1 SayWhat
m2 -> case (SayLevel -> SayWhat -> SayWhat
logfltr SayLevel
allowed SayWhat
m1, SayLevel -> SayWhat -> SayWhat
logfltr SayLevel
allowed SayWhat
m2) of
(SayWhat
SayNothing, SayWhat
SayNothing) -> SayWhat
SayNothing
(SayWhat
SayNothing, SayWhat
m) -> SayWhat
m
(SayWhat
m, SayWhat
SayNothing) -> SayWhat
m
(SayWhat
m1', SayWhat
m2') -> SayWhat -> SayWhat -> SayWhat
SayMore SayWhat
m1' SayWhat
m2'
printFails :: Bool
printFails = Bool -> (OutputOptions -> Bool) -> Maybe OutputOptions -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True OutputOptions -> Bool
printFailures Maybe OutputOptions
opts
printVars :: Bool
printVars = Bool -> (OutputOptions -> Bool) -> Maybe OutputOptions -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False OutputOptions -> Bool
printSymbolicVars Maybe OutputOptions
opts
lgGoal :: LogAction IO (Seq ProvedGoals)
lgGoal = Bool -> Bool -> Seq ProvedGoals -> SayWhat
sayWhatFailedGoals Bool
printFails Bool
printVars (Seq ProvedGoals -> SayWhat)
-> LogAction IO SayWhat -> LogAction IO (Seq ProvedGoals)
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< LogAction IO SayWhat
lgWhat
splitResults :: CruxSimulationResult -> (Seq ProvedGoals, CruxSimulationResult)
splitResults r :: CruxSimulationResult
r@(CruxSimulationResult ProgramCompleteness
_cmpl Seq (ProcessedGoals, ProvedGoals)
gls) = ((ProcessedGoals, ProvedGoals) -> ProvedGoals
forall a b. (a, b) -> b
snd ((ProcessedGoals, ProvedGoals) -> ProvedGoals)
-> Seq (ProcessedGoals, ProvedGoals) -> Seq ProvedGoals
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (ProcessedGoals, ProvedGoals)
gls, CruxSimulationResult
r)
in OutputConfig
{ _outputHandle :: Handle
_outputHandle = Handle
outHandle
, _quiet :: Bool
_quiet = Bool
beQuiet
, _logMsg :: LogAction IO msgs
_logMsg = msgs -> SayWhat
logMessageToSayWhat (msgs -> SayWhat) -> LogAction IO SayWhat -> LogAction IO msgs
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< LogAction IO SayWhat
lgWhat
, _logExc :: LogAction IO SomeException
_logExc = let seeRed :: IO ()
seeRed = Handle -> [SGR] -> IO ()
AC.hSetSGR Handle
errHandle
[ ConsoleIntensity -> SGR
AC.SetConsoleIntensity ConsoleIntensity
AC.BoldIntensity
, ConsoleLayer -> ColorIntensity -> Color -> SGR
AC.SetColor ConsoleLayer
AC.Foreground ColorIntensity
AC.Vivid Color
AC.Red]
seeCalm :: IO ()
seeCalm = Handle -> [SGR] -> IO ()
AC.hSetSGR Handle
errHandle [SGR
AC.Reset]
dispExc :: SomeException -> IO ()
dispExc = Handle -> FilePath -> IO ()
hPutStr Handle
errHandle (FilePath -> IO ())
-> (SomeException -> FilePath) -> SomeException -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> FilePath
forall e. Exception e => e -> FilePath
Ex.displayException
in if Bool
errShouldColor
then (SomeException -> IO ()) -> LogAction IO SomeException
forall (m :: * -> *) msg. (msg -> m ()) -> LogAction m msg
LJ.LogAction ((SomeException -> IO ()) -> LogAction IO SomeException)
-> (SomeException -> IO ()) -> LogAction IO SomeException
forall a b. (a -> b) -> a -> b
$ \SomeException
e -> IO () -> IO () -> IO () -> IO ()
forall a b c. IO a -> IO b -> IO c -> IO c
Ex.bracket_ IO ()
seeRed IO ()
seeCalm (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ SomeException -> IO ()
dispExc SomeException
e
else (SomeException -> IO ()) -> LogAction IO SomeException
forall (m :: * -> *) msg. (msg -> m ()) -> LogAction m msg
LJ.LogAction ((SomeException -> IO ()) -> LogAction IO SomeException)
-> (SomeException -> IO ()) -> LogAction IO SomeException
forall a b. (a -> b) -> a -> b
$ SomeException -> IO ()
dispExc
, _logSimResult :: Bool -> LogAction IO CruxSimulationResult
_logSimResult = \Bool
showDetails ->
if Bool
showDetails
then (CruxSimulationResult -> (Seq ProvedGoals, CruxSimulationResult))
-> LogAction IO (Seq ProvedGoals)
-> LogAction IO CruxSimulationResult
-> LogAction IO CruxSimulationResult
forall a b c.
(a -> (b, c)) -> LogAction IO b -> LogAction IO c -> LogAction IO a
forall (f :: * -> *) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide CruxSimulationResult -> (Seq ProvedGoals, CruxSimulationResult)
splitResults
LogAction IO (Seq ProvedGoals)
lgGoal
(CruxSimulationResult -> SayWhat
sayWhatResultStatus (CruxSimulationResult -> SayWhat)
-> LogAction IO SayWhat -> LogAction IO CruxSimulationResult
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< LogAction IO SayWhat
lgWhat)
else CruxSimulationResult -> SayWhat
sayWhatResultStatus (CruxSimulationResult -> SayWhat)
-> LogAction IO SayWhat -> LogAction IO CruxSimulationResult
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< LogAction IO SayWhat
lgWhat
, _logGoal :: LogAction IO ProvedGoals
_logGoal = ProvedGoals -> Seq ProvedGoals
forall a. a -> Seq a
Seq.singleton (ProvedGoals -> Seq ProvedGoals)
-> LogAction IO (Seq ProvedGoals) -> LogAction IO ProvedGoals
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< LogAction IO (Seq ProvedGoals)
lgGoal
}
defaultOutputConfig ::
JSON.ToJSON msgs =>
(msgs -> SayWhat) -> IO (Maybe OutputOptions -> OutputConfig msgs)
defaultOutputConfig :: forall msgs.
ToJSON msgs =>
(msgs -> SayWhat) -> IO (Maybe OutputOptions -> OutputConfig msgs)
defaultOutputConfig msgs -> SayWhat
logMessagesToSayWhat = do
Bool
outWantsColor <- Handle -> IO Bool
AC.hSupportsANSIColor Handle
stdout
Bool
errWantsColor <- Handle -> IO Bool
AC.hSupportsANSIColor Handle
stderr
(Maybe OutputOptions -> OutputConfig msgs)
-> IO (Maybe OutputOptions -> OutputConfig msgs)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Maybe OutputOptions -> OutputConfig msgs)
-> IO (Maybe OutputOptions -> OutputConfig msgs))
-> (Maybe OutputOptions -> OutputConfig msgs)
-> IO (Maybe OutputOptions -> OutputConfig msgs)
forall a b. (a -> b) -> a -> b
$ (Handle, Bool)
-> (Handle, Bool)
-> (msgs -> SayWhat)
-> Maybe OutputOptions
-> OutputConfig msgs
forall msgs.
ToJSON msgs =>
(Handle, Bool)
-> (Handle, Bool)
-> (msgs -> SayWhat)
-> Maybe OutputOptions
-> OutputConfig msgs
Crux.mkOutputConfig (Handle
stdout, Bool
outWantsColor) (Handle
stderr, Bool
errWantsColor) msgs -> SayWhat
logMessagesToSayWhat
withFloatRepr ::
CCS.HasDefaultFloatRepr solver =>
st s ->
CruxOptions ->
[solver] ->
(forall fm .
IsInterpretedFloatExprBuilder (WE.ExprBuilder s st (WE.Flags fm)) =>
WE.FloatModeRepr fm ->
IO a) ->
IO a
withFloatRepr :: forall solver (st :: * -> *) s a.
HasDefaultFloatRepr solver =>
st s
-> CruxOptions
-> [solver]
-> (forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> IO a)
-> IO a
withFloatRepr st s
st CruxOptions
cruxOpts [solver]
selectedSolvers forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> IO a
k =
case CruxOptions -> FilePath
floatMode CruxOptions
cruxOpts of
FilePath
"real" -> FloatModeRepr 'FloatReal -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> IO a
k FloatModeRepr 'FloatReal
WE.FloatRealRepr
FilePath
"ieee" -> FloatModeRepr 'FloatIEEE -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> IO a
k FloatModeRepr 'FloatIEEE
WE.FloatIEEERepr
FilePath
"uninterpreted" -> FloatModeRepr 'FloatUninterpreted -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> IO a
k FloatModeRepr 'FloatUninterpreted
WE.FloatUninterpretedRepr
FilePath
"default" -> case [solver]
selectedSolvers of
[solver
oneSolver] -> st s
-> solver
-> (forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> IO a)
-> IO a
forall solver (st :: * -> *) s a.
HasDefaultFloatRepr solver =>
st s
-> solver
-> (forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a)
-> a
forall (st :: * -> *) s a.
st s
-> solver
-> (forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a)
-> a
CCS.withDefaultFloatRepr st s
st solver
oneSolver FloatModeRepr fm -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> IO a
k
[solver]
_ -> FloatModeRepr 'FloatUninterpreted -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> IO a
k FloatModeRepr 'FloatUninterpreted
WE.FloatUninterpretedRepr
FilePath
fm -> FilePath -> IO a
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath
"Unknown floating point mode: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
fm FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"; expected one of [real|ieee|uninterpreted|default]")
withSelectedOnlineBackend :: forall msgs scope st a.
Logs msgs =>
SupportsCruxLogMessage msgs =>
CruxOptions ->
NonceGenerator IO scope ->
CCS.SolverOnline ->
Maybe String ->
st scope ->
(forall solver fm .
( OnlineSolver solver
, IsInterpretedFloatExprBuilder (WE.ExprBuilder scope st (WE.Flags fm))
) =>
(OnlineBackend solver scope st (WE.Flags fm) -> IO a)) ->
IO a
withSelectedOnlineBackend :: forall msgs scope (st :: * -> *) a.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions
-> NonceGenerator IO scope
-> SolverOnline
-> Maybe FilePath
-> st scope
-> (forall solver (fm :: FloatMode).
(OnlineSolver solver,
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm))) =>
OnlineBackend solver scope st (Flags fm) -> IO a)
-> IO a
withSelectedOnlineBackend CruxOptions
cruxOpts NonceGenerator IO scope
nonceGen SolverOnline
selectedSolver Maybe FilePath
maybeExplicitFloatMode st scope
initSt forall solver (fm :: FloatMode).
(OnlineSolver solver,
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm))) =>
OnlineBackend solver scope st (Flags fm) -> IO a
k =
case FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe (CruxOptions -> FilePath
floatMode CruxOptions
cruxOpts) Maybe FilePath
maybeExplicitFloatMode of
FilePath
"real" -> FloatModeRepr 'FloatReal -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm)) =>
FloatModeRepr fm -> IO a
withOnlineBackendFM FloatModeRepr 'FloatReal
WE.FloatRealRepr
FilePath
"ieee" -> FloatModeRepr 'FloatIEEE -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm)) =>
FloatModeRepr fm -> IO a
withOnlineBackendFM FloatModeRepr 'FloatIEEE
WE.FloatIEEERepr
FilePath
"uninterpreted" -> FloatModeRepr 'FloatUninterpreted -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm)) =>
FloatModeRepr fm -> IO a
withOnlineBackendFM FloatModeRepr 'FloatUninterpreted
WE.FloatUninterpretedRepr
FilePath
"default" ->
case SolverOnline
selectedSolver of
SolverOnline
CCS.Yices -> FloatModeRepr 'FloatReal -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm)) =>
FloatModeRepr fm -> IO a
withOnlineBackendFM FloatModeRepr 'FloatReal
WE.FloatRealRepr
SolverOnline
CCS.CVC4 -> FloatModeRepr 'FloatReal -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm)) =>
FloatModeRepr fm -> IO a
withOnlineBackendFM FloatModeRepr 'FloatReal
WE.FloatRealRepr
SolverOnline
CCS.CVC5 -> FloatModeRepr 'FloatReal -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm)) =>
FloatModeRepr fm -> IO a
withOnlineBackendFM FloatModeRepr 'FloatReal
WE.FloatRealRepr
SolverOnline
CCS.STP -> FloatModeRepr 'FloatReal -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm)) =>
FloatModeRepr fm -> IO a
withOnlineBackendFM FloatModeRepr 'FloatReal
WE.FloatRealRepr
SolverOnline
CCS.Z3 -> FloatModeRepr 'FloatIEEE -> IO a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm)) =>
FloatModeRepr fm -> IO a
withOnlineBackendFM FloatModeRepr 'FloatIEEE
WE.FloatIEEERepr
FilePath
fm -> FilePath -> IO a
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath
"Unknown floating point mode: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
fm FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"; expected one of [real|ieee|uninterpreted|default]")
where
withOnlineBackendFM ::
IsInterpretedFloatExprBuilder (WE.ExprBuilder scope st (WE.Flags fm)) =>
WE.FloatModeRepr fm ->
IO a
withOnlineBackendFM :: forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm)) =>
FloatModeRepr fm -> IO a
withOnlineBackendFM FloatModeRepr fm
fm =
do ExprBuilder scope st (Flags fm)
sym <- FloatModeRepr fm
-> st scope
-> NonceGenerator IO scope
-> IO (ExprBuilder scope st (Flags fm))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
WE.newExprBuilder FloatModeRepr fm
fm st scope
initSt NonceGenerator IO scope
nonceGen
CruxOptions
-> SolverOnline
-> ExprBuilder scope st (Flags fm)
-> (forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st (Flags fm) -> IO a)
-> IO a
forall msgs scope (st :: * -> *) fs a.
(Logs msgs, SupportsCruxLogMessage msgs,
IsInterpretedFloatExprBuilder (ExprBuilder scope st fs)) =>
CruxOptions
-> SolverOnline
-> ExprBuilder scope st fs
-> (forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO a)
-> IO a
withSelectedOnlineBackend' CruxOptions
cruxOpts SolverOnline
selectedSolver ExprBuilder scope st (Flags fm)
sym OnlineBackend solver scope st (Flags fm) -> IO a
forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st (Flags fm) -> IO a
forall solver (fm :: FloatMode).
(OnlineSolver solver,
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm))) =>
OnlineBackend solver scope st (Flags fm) -> IO a
k
withSelectedOnlineBackend' ::
Logs msgs =>
SupportsCruxLogMessage msgs =>
IsInterpretedFloatExprBuilder (WE.ExprBuilder scope st fs) =>
CruxOptions ->
CCS.SolverOnline ->
WE.ExprBuilder scope st fs ->
(forall solver.
OnlineSolver solver =>
(OnlineBackend solver scope st fs -> IO a)) ->
IO a
withSelectedOnlineBackend' :: forall msgs scope (st :: * -> *) fs a.
(Logs msgs, SupportsCruxLogMessage msgs,
IsInterpretedFloatExprBuilder (ExprBuilder scope st fs)) =>
CruxOptions
-> SolverOnline
-> ExprBuilder scope st fs
-> (forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO a)
-> IO a
withSelectedOnlineBackend' CruxOptions
cruxOpts SolverOnline
selectedSolver ExprBuilder scope st fs
sym forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO a
k =
let unsatCoreFeat :: UnsatFeatures
unsatCoreFeat | CruxOptions -> Bool
unsatCores CruxOptions
cruxOpts
, Bool -> Bool
not (CruxOptions -> Bool
yicesMCSat CruxOptions
cruxOpts) = UnsatFeatures
ProduceUnsatCores
| Bool
otherwise = UnsatFeatures
NoUnsatFeatures
extraFeatures :: ProblemFeatures
extraFeatures = CruxOptions -> ProblemFeatures
onlineProblemFeatures CruxOptions
cruxOpts
in case SolverOnline
selectedSolver of
SolverOnline
CCS.Yices -> ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (YicesOnlineBackend scope st fs -> IO a)
-> IO a
forall (m :: * -> *) scope (st :: * -> *) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (YicesOnlineBackend scope st fs -> m a)
-> m a
withYicesOnlineBackend ExprBuilder scope st fs
sym UnsatFeatures
unsatCoreFeat ProblemFeatures
extraFeatures ((YicesOnlineBackend scope st fs -> IO a) -> IO a)
-> (YicesOnlineBackend scope st fs -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \YicesOnlineBackend scope st fs
bak -> do
ExprBuilder scope st fs
-> ConfigOption BaseBoolType -> Bool -> IO ()
forall sym (t :: BaseType) a.
(IsExprBuilder sym, Opt t a) =>
sym -> ConfigOption t -> a -> IO ()
symCfg ExprBuilder scope st fs
sym ConfigOption BaseBoolType
yicesEnableMCSat (CruxOptions -> Bool
yicesMCSat CruxOptions
cruxOpts)
case CruxOptions -> Maybe DiffTime
goalTimeout CruxOptions
cruxOpts of
Just DiffTime
s -> ExprBuilder scope st fs
-> ConfigOption BaseIntegerType -> Integer -> IO ()
forall sym (t :: BaseType) a.
(IsExprBuilder sym, Opt t a) =>
sym -> ConfigOption t -> a -> IO ()
symCfg ExprBuilder scope st fs
sym ConfigOption BaseIntegerType
yicesGoalTimeout (DiffTime -> Integer
forall b. Integral b => DiffTime -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor DiffTime
s)
Maybe DiffTime
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
YicesOnlineBackend scope st fs -> IO a
forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO a
k YicesOnlineBackend scope st fs
bak
SolverOnline
CCS.CVC4 -> ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (CVC4OnlineBackend scope st fs -> IO a)
-> IO a
forall (m :: * -> *) scope (st :: * -> *) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (CVC4OnlineBackend scope st fs -> m a)
-> m a
withCVC4OnlineBackend ExprBuilder scope st fs
sym UnsatFeatures
unsatCoreFeat ProblemFeatures
extraFeatures ((CVC4OnlineBackend scope st fs -> IO a) -> IO a)
-> (CVC4OnlineBackend scope st fs -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \CVC4OnlineBackend scope st fs
bak -> do
case CruxOptions -> Maybe DiffTime
goalTimeout CruxOptions
cruxOpts of
Just DiffTime
s -> ExprBuilder scope st fs
-> ConfigOption BaseIntegerType -> Integer -> IO ()
forall sym (t :: BaseType) a.
(IsExprBuilder sym, Opt t a) =>
sym -> ConfigOption t -> a -> IO ()
symCfg ExprBuilder scope st fs
sym ConfigOption BaseIntegerType
cvc4Timeout (DiffTime -> Integer
forall b. Integral b => DiffTime -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (DiffTime
s DiffTime -> DiffTime -> DiffTime
forall a. Num a => a -> a -> a
* DiffTime
1000))
Maybe DiffTime
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
CVC4OnlineBackend scope st fs -> IO a
forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO a
k CVC4OnlineBackend scope st fs
bak
SolverOnline
CCS.CVC5 -> ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (CVC5OnlineBackend scope st fs -> IO a)
-> IO a
forall (m :: * -> *) scope (st :: * -> *) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (CVC5OnlineBackend scope st fs -> m a)
-> m a
withCVC5OnlineBackend ExprBuilder scope st fs
sym UnsatFeatures
unsatCoreFeat ProblemFeatures
extraFeatures ((CVC5OnlineBackend scope st fs -> IO a) -> IO a)
-> (CVC5OnlineBackend scope st fs -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \CVC5OnlineBackend scope st fs
bak -> do
case CruxOptions -> Maybe DiffTime
goalTimeout CruxOptions
cruxOpts of
Just DiffTime
s -> ExprBuilder scope st fs
-> ConfigOption BaseIntegerType -> Integer -> IO ()
forall sym (t :: BaseType) a.
(IsExprBuilder sym, Opt t a) =>
sym -> ConfigOption t -> a -> IO ()
symCfg ExprBuilder scope st fs
sym ConfigOption BaseIntegerType
cvc5Timeout (DiffTime -> Integer
forall b. Integral b => DiffTime -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (DiffTime
s DiffTime -> DiffTime -> DiffTime
forall a. Num a => a -> a -> a
* DiffTime
1000))
Maybe DiffTime
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
CVC5OnlineBackend scope st fs -> IO a
forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO a
k CVC5OnlineBackend scope st fs
bak
SolverOnline
CCS.Z3 -> ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (Z3OnlineBackend scope st fs -> IO a)
-> IO a
forall (m :: * -> *) scope (st :: * -> *) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (Z3OnlineBackend scope st fs -> m a)
-> m a
withZ3OnlineBackend ExprBuilder scope st fs
sym UnsatFeatures
unsatCoreFeat ProblemFeatures
extraFeatures ((Z3OnlineBackend scope st fs -> IO a) -> IO a)
-> (Z3OnlineBackend scope st fs -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \Z3OnlineBackend scope st fs
bak -> do
case CruxOptions -> Maybe DiffTime
goalTimeout CruxOptions
cruxOpts of
Just DiffTime
s -> ExprBuilder scope st fs
-> ConfigOption BaseIntegerType -> Integer -> IO ()
forall sym (t :: BaseType) a.
(IsExprBuilder sym, Opt t a) =>
sym -> ConfigOption t -> a -> IO ()
symCfg ExprBuilder scope st fs
sym ConfigOption BaseIntegerType
z3Timeout (DiffTime -> Integer
forall b. Integral b => DiffTime -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (DiffTime
s DiffTime -> DiffTime -> DiffTime
forall a. Num a => a -> a -> a
* DiffTime
1000))
Maybe DiffTime
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Z3OnlineBackend scope st fs -> IO a
forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO a
k Z3OnlineBackend scope st fs
bak
SolverOnline
CCS.STP -> do
case CruxOptions -> Maybe DiffTime
goalTimeout CruxOptions
cruxOpts of
Just DiffTime
_ -> CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux (FilePath -> CruxLogMessage
Log.UnsupportedTimeoutFor FilePath
"STP")
Maybe DiffTime
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
ExprBuilder scope st fs
-> (STPOnlineBackend scope st fs -> IO a) -> IO a
forall (m :: * -> *) scope (st :: * -> *) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> (STPOnlineBackend scope st fs -> m a) -> m a
withSTPOnlineBackend ExprBuilder scope st fs
sym STPOnlineBackend scope st fs -> IO a
forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO a
k
data ProfData sym = ProfData
{ forall sym. ProfData sym -> forall a. FunctionName -> IO a -> IO a
inFrame :: forall a. FunctionName -> IO a -> IO a
, forall sym. ProfData sym -> [GenericExecutionFeature sym]
profExecFeatures :: [GenericExecutionFeature sym]
, forall sym. ProfData sym -> IO ()
writeProf :: IO ()
}
noProfiling :: ProfData sym
noProfiling :: forall sym. ProfData sym
noProfiling = ProfData
{ inFrame :: forall a. FunctionName -> IO a -> IO a
inFrame = \FunctionName
_ IO a
x -> IO a
x
, profExecFeatures :: [GenericExecutionFeature sym]
profExecFeatures = []
, writeProf :: IO ()
writeProf = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
}
setupProfiling :: IsSymInterface sym => sym -> CruxOptions -> IO (ProfData sym)
setupProfiling :: forall sym.
IsSymInterface sym =>
sym -> CruxOptions -> IO (ProfData sym)
setupProfiling sym
sym CruxOptions
cruxOpts =
do ProfilingTable
tbl <- IO ProfilingTable
newProfilingTable
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CruxOptions -> Bool
profileSolver CruxOptions
cruxOpts) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
sym -> ProfilingTable -> IO ()
forall sym. IsSymInterface sym => sym -> ProfilingTable -> IO ()
startRecordingSolverEvents sym
sym ProfilingTable
tbl
let profSource :: FilePath
profSource = case CruxOptions -> [FilePath]
inputFiles CruxOptions
cruxOpts of
[FilePath
f] -> FilePath
f
[FilePath]
_ -> FilePath
"multiple files"
profOutFile :: FilePath
profOutFile = CruxOptions -> FilePath
outDir CruxOptions
cruxOpts FilePath -> FilePath -> FilePath
</> FilePath
"report_data.js"
saveProf :: ProfilingTable -> IO ()
saveProf = FilePath -> FilePath -> FilePath -> ProfilingTable -> IO ()
writeProfileReport FilePath
profOutFile FilePath
"crux profile" FilePath
profSource
profOpts :: ProfilingOptions
profOpts = ProfilingOptions
{ periodicProfileInterval :: NominalDiffTime
periodicProfileInterval = CruxOptions -> NominalDiffTime
profileOutputInterval CruxOptions
cruxOpts
, periodicProfileAction :: ProfilingTable -> IO ()
periodicProfileAction = ProfilingTable -> IO ()
saveProf
}
profFilt :: EventFilter
profFilt = EventFilter
{ recordProfiling :: Bool
recordProfiling = CruxOptions -> Bool
profileCrucibleFunctions CruxOptions
cruxOpts
, recordCoverage :: Bool
recordCoverage = CruxOptions -> Bool
branchCoverage CruxOptions
cruxOpts
}
[GenericExecutionFeature sym]
pfs <- Bool
-> IO (GenericExecutionFeature sym)
-> IO [GenericExecutionFeature sym]
forall sym.
Bool
-> IO (GenericExecutionFeature sym)
-> IO [GenericExecutionFeature sym]
execFeatureIf (CruxOptions -> Bool
profileCrucibleFunctions CruxOptions
cruxOpts Bool -> Bool -> Bool
|| CruxOptions -> Bool
branchCoverage CruxOptions
cruxOpts)
(ProfilingTable
-> EventFilter
-> Maybe ProfilingOptions
-> IO (GenericExecutionFeature sym)
forall sym.
ProfilingTable
-> EventFilter
-> Maybe ProfilingOptions
-> IO (GenericExecutionFeature sym)
profilingFeature ProfilingTable
tbl EventFilter
profFilt (ProfilingOptions -> Maybe ProfilingOptions
forall a. a -> Maybe a
Just ProfilingOptions
profOpts))
ProfData sym -> IO (ProfData sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProfData
{ inFrame :: forall a. FunctionName -> IO a -> IO a
inFrame = \FunctionName
str -> ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO a -> IO a
forall a.
ProfilingTable -> FunctionName -> Maybe ProgramLoc -> IO a -> IO a
inProfilingFrame ProfilingTable
tbl FunctionName
str Maybe ProgramLoc
forall a. Maybe a
Nothing
, profExecFeatures :: [GenericExecutionFeature sym]
profExecFeatures = [GenericExecutionFeature sym]
pfs
, writeProf :: IO ()
writeProf = ProfilingTable -> IO ()
saveProf ProfilingTable
tbl
}
execFeatureIf ::
Bool ->
IO (GenericExecutionFeature sym) ->
IO [GenericExecutionFeature sym]
execFeatureIf :: forall sym.
Bool
-> IO (GenericExecutionFeature sym)
-> IO [GenericExecutionFeature sym]
execFeatureIf Bool
b IO (GenericExecutionFeature sym)
m = if Bool
b then (GenericExecutionFeature sym
-> [GenericExecutionFeature sym] -> [GenericExecutionFeature sym]
forall a. a -> [a] -> [a]
:[]) (GenericExecutionFeature sym -> [GenericExecutionFeature sym])
-> IO (GenericExecutionFeature sym)
-> IO [GenericExecutionFeature sym]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (GenericExecutionFeature sym)
m else [GenericExecutionFeature sym] -> IO [GenericExecutionFeature sym]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
execFeatureMaybe ::
Maybe a ->
(a -> IO (GenericExecutionFeature sym)) ->
IO [GenericExecutionFeature sym]
execFeatureMaybe :: forall a sym.
Maybe a
-> (a -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym]
execFeatureMaybe Maybe a
mb a -> IO (GenericExecutionFeature sym)
m =
case Maybe a
mb of
Maybe a
Nothing -> [GenericExecutionFeature sym] -> IO [GenericExecutionFeature sym]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Just a
a -> (GenericExecutionFeature sym
-> [GenericExecutionFeature sym] -> [GenericExecutionFeature sym]
forall a. a -> [a] -> [a]
:[]) (GenericExecutionFeature sym -> [GenericExecutionFeature sym])
-> IO (GenericExecutionFeature sym)
-> IO [GenericExecutionFeature sym]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> IO (GenericExecutionFeature sym)
m a
a
setupSolver :: (IsExprBuilder sym, sym ~ WE.ExprBuilder t st fs) => CruxOptions -> Maybe FilePath -> sym -> IO ()
setupSolver :: forall sym t (st :: * -> *) fs.
(IsExprBuilder sym, sym ~ ExprBuilder t st fs) =>
CruxOptions -> Maybe FilePath -> sym -> IO ()
setupSolver CruxOptions
cruxOpts Maybe FilePath
mInteractionFile sym
sym = do
(Text -> IO ()) -> Maybe Text -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (sym -> ConfigOption (BaseStringType Unicode) -> Text -> IO ()
forall sym (t :: BaseType) a.
(IsExprBuilder sym, Opt t a) =>
sym -> ConfigOption t -> a -> IO ()
symCfg sym
sym ConfigOption (BaseStringType Unicode)
solverInteractionFile) ((FilePath -> Text) -> Maybe FilePath -> Maybe Text
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FilePath -> Text
T.pack Maybe FilePath
mInteractionFile)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CruxOptions -> Bool
hashConsing CruxOptions
cruxOpts) (ExprBuilder t st fs -> IO ()
forall t (st :: * -> *) fs. ExprBuilder t st fs -> IO ()
WE.startCaching sym
ExprBuilder t st fs
sym)
let outOpts :: OutputOptions
outOpts = CruxOptions -> OutputOptions
outputOptions CruxOptions
cruxOpts
sym -> ConfigOption BaseIntegerType -> Integer -> IO ()
forall sym (t :: BaseType) a.
(IsExprBuilder sym, Opt t a) =>
sym -> ConfigOption t -> a -> IO ()
symCfg sym
sym ConfigOption BaseIntegerType
verbosity (Integer -> IO ()) -> Integer -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ if OutputOptions -> Int
simVerbose OutputOptions
outOpts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
then OutputOptions -> Int
simVerbose OutputOptions
outOpts Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
else Int
0
setupExecutionFeatures :: IsSymBackend sym bak
=> CruxOptions
-> bak
-> Maybe (SomeOnlineSolver sym bak)
-> IO
([GenericExecutionFeature sym], ProfData sym)
setupExecutionFeatures :: forall sym bak.
IsSymBackend sym bak =>
CruxOptions
-> bak
-> Maybe (SomeOnlineSolver sym bak)
-> IO ([GenericExecutionFeature sym], ProfData sym)
setupExecutionFeatures CruxOptions
cruxOpts bak
bak Maybe (SomeOnlineSolver sym bak)
maybeOnline = do
let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
let profiling :: Bool
profiling = CruxOptions -> Bool
isProfiling CruxOptions
cruxOpts
ProfData sym
profInfo <- if Bool
profiling then sym -> CruxOptions -> IO (ProfData sym)
forall sym.
IsSymInterface sym =>
sym -> CruxOptions -> IO (ProfData sym)
setupProfiling sym
sym CruxOptions
cruxOpts
else ProfData sym -> IO (ProfData sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProfData sym
forall sym. ProfData sym
noProfiling
[GenericExecutionFeature sym]
tfs <- Maybe NominalDiffTime
-> (NominalDiffTime -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym]
forall a sym.
Maybe a
-> (a -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym]
execFeatureMaybe (CruxOptions -> Maybe NominalDiffTime
globalTimeout CruxOptions
cruxOpts) NominalDiffTime -> IO (GenericExecutionFeature sym)
forall sym. NominalDiffTime -> IO (GenericExecutionFeature sym)
timeoutFeature
[GenericExecutionFeature sym]
bfs <- Maybe Word64
-> (Word64 -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym]
forall a sym.
Maybe a
-> (a -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym]
execFeatureMaybe (CruxOptions -> Maybe Word64
loopBound CruxOptions
cruxOpts) ((Word64 -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym])
-> (Word64 -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym]
forall a b. (a -> b) -> a -> b
$ \Word64
i ->
(SomeHandle -> IO (Maybe Word64))
-> Bool -> IO (GenericExecutionFeature sym)
forall sym.
(SomeHandle -> IO (Maybe Word64))
-> Bool -> IO (GenericExecutionFeature sym)
boundedExecFeature (\SomeHandle
_ -> Maybe Word64 -> IO (Maybe Word64)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Word64 -> Maybe Word64
forall a. a -> Maybe a
Just Word64
i)) Bool
True
[GenericExecutionFeature sym]
rfs <- Maybe Word64
-> (Word64 -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym]
forall a sym.
Maybe a
-> (a -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym]
execFeatureMaybe (CruxOptions -> Maybe Word64
recursionBound CruxOptions
cruxOpts) ((Word64 -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym])
-> (Word64 -> IO (GenericExecutionFeature sym))
-> IO [GenericExecutionFeature sym]
forall a b. (a -> b) -> a -> b
$ \Word64
i ->
(SomeHandle -> IO (Maybe Word64))
-> Bool -> IO (GenericExecutionFeature sym)
forall sym.
(SomeHandle -> IO (Maybe Word64))
-> Bool -> IO (GenericExecutionFeature sym)
boundedRecursionFeature (\SomeHandle
_ -> Maybe Word64 -> IO (Maybe Word64)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Word64 -> Maybe Word64
forall a. a -> Maybe a
Just Word64
i)) Bool
True
[GenericExecutionFeature sym]
psat_fs <- case Maybe (SomeOnlineSolver sym bak)
maybeOnline of
Just (SomeOnlineSolver bak
_bak) ->
do OptionSetting BaseBoolType
enableOpt <- ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
enableOnlineBackend (sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration sym
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 (CruxOptions -> Bool
checkPathSat CruxOptions
cruxOpts)
Bool
-> IO (GenericExecutionFeature sym)
-> IO [GenericExecutionFeature sym]
forall sym.
Bool
-> IO (GenericExecutionFeature sym)
-> IO [GenericExecutionFeature sym]
execFeatureIf (CruxOptions -> Bool
checkPathSat CruxOptions
cruxOpts)
(IO (GenericExecutionFeature sym)
-> IO [GenericExecutionFeature sym])
-> IO (GenericExecutionFeature sym)
-> IO [GenericExecutionFeature sym]
forall a b. (a -> b) -> a -> b
$ sym
-> (Maybe ProgramLoc -> Pred sym -> IO BranchResult)
-> IO (GenericExecutionFeature sym)
forall sym.
IsSymInterface sym =>
sym
-> (Maybe ProgramLoc -> Pred sym -> IO BranchResult)
-> IO (GenericExecutionFeature sym)
pathSatisfiabilityFeature sym
sym (OnlineBackend solver scope st fs
-> Maybe ProgramLoc -> BoolExpr scope -> IO BranchResult
forall solver scope (st :: * -> *) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> Maybe ProgramLoc -> BoolExpr scope -> IO BranchResult
considerSatisfiability bak
OnlineBackend solver scope st fs
bak)
Maybe (SomeOnlineSolver sym bak)
Nothing -> [GenericExecutionFeature sym] -> IO [GenericExecutionFeature sym]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
GenericExecutionFeature sym
trackfs <- sym -> IO (GenericExecutionFeature sym)
forall sym.
IsSymInterface sym =>
sym -> IO (GenericExecutionFeature sym)
positionTrackingFeature sym
sym
([GenericExecutionFeature sym], ProfData sym)
-> IO ([GenericExecutionFeature sym], ProfData sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[GenericExecutionFeature sym]] -> [GenericExecutionFeature sym]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[GenericExecutionFeature sym]
tfs, ProfData sym -> [GenericExecutionFeature sym]
forall sym. ProfData sym -> [GenericExecutionFeature sym]
profExecFeatures ProfData sym
profInfo, [GenericExecutionFeature sym]
bfs, [GenericExecutionFeature sym]
rfs, [GenericExecutionFeature sym]
psat_fs, [GenericExecutionFeature sym
trackfs]], ProfData sym
profInfo)
withSolverAdapter :: CCS.SolverOffline -> (WS.SolverAdapter st -> a) -> a
withSolverAdapter :: forall (st :: * -> *) a.
SolverOffline -> (SolverAdapter st -> a) -> a
withSolverAdapter SolverOffline
solverOff SolverAdapter st -> a
k =
case SolverOffline
solverOff of
SolverOffline
CCS.Boolector -> SolverAdapter st -> a
k SolverAdapter st
forall (st :: * -> *). SolverAdapter st
WS.boolectorAdapter
SolverOffline
CCS.DReal -> SolverAdapter st -> a
k SolverAdapter st
forall (st :: * -> *). SolverAdapter st
WS.drealAdapter
CCS.SolverOnline SolverOnline
CCS.CVC4 -> SolverAdapter st -> a
k SolverAdapter st
forall (st :: * -> *). SolverAdapter st
WS.cvc4Adapter
CCS.SolverOnline SolverOnline
CCS.CVC5 -> SolverAdapter st -> a
k SolverAdapter st
forall (st :: * -> *). SolverAdapter st
WS.cvc5Adapter
CCS.SolverOnline SolverOnline
CCS.STP -> SolverAdapter st -> a
k SolverAdapter st
forall (st :: * -> *). SolverAdapter st
WS.stpAdapter
CCS.SolverOnline SolverOnline
CCS.Yices -> SolverAdapter st -> a
k SolverAdapter st
forall (st :: * -> *). SolverAdapter st
WS.yicesAdapter
CCS.SolverOnline SolverOnline
CCS.Z3 -> SolverAdapter st -> a
k SolverAdapter st
forall (st :: * -> *). SolverAdapter st
WS.z3Adapter
withSolverAdapters :: [CCS.SolverOffline] -> ([WS.SolverAdapter st] -> a) -> a
withSolverAdapters :: forall (st :: * -> *) a.
[SolverOffline] -> ([SolverAdapter st] -> a) -> a
withSolverAdapters [SolverOffline]
solverOffs [SolverAdapter st] -> a
k =
(SolverOffline
-> ([SolverAdapter st] -> a) -> [SolverAdapter st] -> a)
-> ([SolverAdapter st] -> a)
-> [SolverOffline]
-> [SolverAdapter st]
-> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SolverOffline
-> ([SolverAdapter st] -> a) -> [SolverAdapter st] -> a
forall {st :: * -> *} {a}.
SolverOffline
-> ([SolverAdapter st] -> a) -> [SolverAdapter st] -> a
go [SolverAdapter st] -> a
base [SolverOffline]
solverOffs ([SolverAdapter st] -> a) -> [SolverAdapter st] -> a
forall a b. (a -> b) -> a -> b
$ []
where
base :: [SolverAdapter st] -> a
base [SolverAdapter st]
adapters = [SolverAdapter st] -> a
k [SolverAdapter st]
adapters
go :: SolverOffline
-> ([SolverAdapter st] -> a) -> [SolverAdapter st] -> a
go SolverOffline
nextOff [SolverAdapter st] -> a
withAdapters [SolverAdapter st]
adapters = SolverOffline -> (SolverAdapter st -> a) -> a
forall (st :: * -> *) a.
SolverOffline -> (SolverAdapter st -> a) -> a
withSolverAdapter SolverOffline
nextOff (\SolverAdapter st
adapter -> [SolverAdapter st] -> a
withAdapters (SolverAdapter st
adapterSolverAdapter st -> [SolverAdapter st] -> [SolverAdapter st]
forall a. a -> [a] -> [a]
:[SolverAdapter st]
adapters))
runSimulator ::
Logs msgs =>
SupportsCruxLogMessage msgs =>
CruxOptions ->
SimulatorCallbacks msgs r ->
IO r
runSimulator :: forall msgs r.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> SimulatorCallbacks msgs r -> IO r
runSimulator CruxOptions
cruxOpts SimulatorCallbacks msgs r
simCallback = do
CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux ([FilePath] -> CruxLogMessage
Log.Checking (CruxOptions -> [FilePath]
inputFiles CruxOptions
cruxOpts))
Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True (CruxOptions -> FilePath
outDir CruxOptions
cruxOpts)
Some (NonceGenerator IO x
nonceGen :: NonceGenerator IO s) <- IO (Some (NonceGenerator IO))
newIONonceGenerator
case CruxOptions -> Either [FilePath] SolverConfig
CCS.parseSolverConfig CruxOptions
cruxOpts of
Right (CCS.SingleOnlineSolver SolverOnline
onSolver) ->
CruxOptions
-> NonceGenerator IO x
-> SolverOnline
-> Maybe FilePath
-> EmptyExprBuilderState x
-> (forall {solver} {fm :: FloatMode}.
(OnlineSolver solver,
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm))) =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r
forall msgs scope (st :: * -> *) a.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions
-> NonceGenerator IO scope
-> SolverOnline
-> Maybe FilePath
-> st scope
-> (forall solver (fm :: FloatMode).
(OnlineSolver solver,
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm))) =>
OnlineBackend solver scope st (Flags fm) -> IO a)
-> IO a
withSelectedOnlineBackend CruxOptions
cruxOpts NonceGenerator IO x
nonceGen SolverOnline
onSolver Maybe FilePath
forall a. Maybe a
Nothing EmptyExprBuilderState x
forall t. EmptyExprBuilderState t
WE.EmptyExprBuilderState ((forall {solver} {fm :: FloatMode}.
(OnlineSolver solver,
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm))) =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r)
-> (forall {solver} {fm :: FloatMode}.
(OnlineSolver solver,
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm))) =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r
forall a b. (a -> b) -> a -> b
$ \OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak -> do
let monline :: Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
monline = SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm))
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
forall a. a -> Maybe a
Just (OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm))
forall sym scope (st :: * -> *) fs bak solver.
(sym ~ ExprBuilder scope st fs,
bak ~ OnlineBackend solver scope st fs, IsSymBackend sym bak,
OnlineSolver solver) =>
bak -> SomeOnlineSolver sym bak
SomeOnlineSolver OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak)
CruxOptions
-> Maybe FilePath
-> ExprBuilder x EmptyExprBuilderState (Flags fm)
-> IO ()
forall sym t (st :: * -> *) fs.
(IsExprBuilder sym, sym ~ ExprBuilder t st fs) =>
CruxOptions -> Maybe FilePath -> sym -> IO ()
setupSolver CruxOptions
cruxOpts (CruxOptions -> Maybe FilePath
pathSatSolverOutput CruxOptions
cruxOpts) (OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> ExprBuilder x EmptyExprBuilderState (Flags fm)
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak)
([GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
execFeatures, ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
profInfo) <- CruxOptions
-> OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
-> IO
([GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))],
ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm)))
forall sym bak.
IsSymBackend sym bak =>
CruxOptions
-> bak
-> Maybe (SomeOnlineSolver sym bak)
-> IO ([GenericExecutionFeature sym], ProfData sym)
setupExecutionFeatures CruxOptions
cruxOpts OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
monline
CruxOptions
-> SimulatorCallbacks msgs r
-> OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> [GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
-> ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
-> ProverCallback (ExprBuilder x EmptyExprBuilderState (Flags fm))
-> IO r
forall sym bak r t (st :: * -> *) fs msgs.
(sym ~ ExprBuilder t st fs, IsSymBackend sym bak, Logs msgs,
SupportsCruxLogMessage msgs) =>
CruxOptions
-> SimulatorCallbacks msgs r
-> bak
-> [GenericExecutionFeature sym]
-> ProfData sym
-> Maybe (SomeOnlineSolver sym bak)
-> ProverCallback sym
-> IO r
doSimWithResults CruxOptions
cruxOpts SimulatorCallbacks msgs r
simCallback OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak [GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
execFeatures ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
profInfo Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
monline (OnlineBackend solver t EmptyExprBuilderState (Flags fm)
-> CruxOptions
-> SimContext
(personality (ExprBuilder x EmptyExprBuilderState (Flags fm)))
(ExprBuilder x EmptyExprBuilderState (Flags fm))
ext
-> (Maybe (GroundEvalFn t)
-> LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError
-> IO (Doc Void))
-> Maybe
(Goals
(CrucibleAssumptions
(SymExpr (ExprBuilder x EmptyExprBuilderState (Flags fm))))
(LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError))
-> IO
(ProcessedGoals,
Maybe
(Goals
(CrucibleAssumptions
(SymExpr (ExprBuilder x EmptyExprBuilderState (Flags fm))))
(LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError,
[ProgramLoc],
ProofResult (ExprBuilder x EmptyExprBuilderState (Flags fm)))))
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 solver x EmptyExprBuilderState (Flags fm)
OnlineBackend solver t EmptyExprBuilderState (Flags fm)
bak)
Right (CCS.OnlineSolverWithOfflineGoals SolverOnline
onSolver SolverOffline
offSolver) ->
CruxOptions
-> NonceGenerator IO x
-> SolverOnline
-> Maybe FilePath
-> EmptyExprBuilderState x
-> (forall {solver} {fm :: FloatMode}.
(OnlineSolver solver,
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm))) =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r
forall msgs scope (st :: * -> *) a.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions
-> NonceGenerator IO scope
-> SolverOnline
-> Maybe FilePath
-> st scope
-> (forall solver (fm :: FloatMode).
(OnlineSolver solver,
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm))) =>
OnlineBackend solver scope st (Flags fm) -> IO a)
-> IO a
withSelectedOnlineBackend CruxOptions
cruxOpts NonceGenerator IO x
nonceGen SolverOnline
onSolver Maybe FilePath
forall a. Maybe a
Nothing EmptyExprBuilderState x
forall t. EmptyExprBuilderState t
WE.EmptyExprBuilderState ((forall {solver} {fm :: FloatMode}.
(OnlineSolver solver,
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm))) =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r)
-> (forall {solver} {fm :: FloatMode}.
(OnlineSolver solver,
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm))) =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r
forall a b. (a -> b) -> a -> b
$ \OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak -> do
let monline :: Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
monline = SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm))
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
forall a. a -> Maybe a
Just (OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm))
forall sym scope (st :: * -> *) fs bak solver.
(sym ~ ExprBuilder scope st fs,
bak ~ OnlineBackend solver scope st fs, IsSymBackend sym bak,
OnlineSolver solver) =>
bak -> SomeOnlineSolver sym bak
SomeOnlineSolver OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak)
CruxOptions
-> Maybe FilePath
-> ExprBuilder x EmptyExprBuilderState (Flags fm)
-> IO ()
forall sym t (st :: * -> *) fs.
(IsExprBuilder sym, sym ~ ExprBuilder t st fs) =>
CruxOptions -> Maybe FilePath -> sym -> IO ()
setupSolver CruxOptions
cruxOpts (CruxOptions -> Maybe FilePath
pathSatSolverOutput CruxOptions
cruxOpts) (OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> ExprBuilder x EmptyExprBuilderState (Flags fm)
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak)
([GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
execFeatures, ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
profInfo) <- CruxOptions
-> OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
-> IO
([GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))],
ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm)))
forall sym bak.
IsSymBackend sym bak =>
CruxOptions
-> bak
-> Maybe (SomeOnlineSolver sym bak)
-> IO ([GenericExecutionFeature sym], ProfData sym)
setupExecutionFeatures CruxOptions
cruxOpts OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
monline
SolverOffline
-> (SolverAdapter EmptyExprBuilderState -> IO r) -> IO r
forall (st :: * -> *) a.
SolverOffline -> (SolverAdapter st -> a) -> a
withSolverAdapter SolverOffline
offSolver ((SolverAdapter EmptyExprBuilderState -> IO r) -> IO r)
-> (SolverAdapter EmptyExprBuilderState -> IO r) -> IO r
forall a b. (a -> b) -> a -> b
$ \SolverAdapter EmptyExprBuilderState
adapter -> do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SolverOnline -> SolverOffline -> Bool
CCS.sameSolver SolverOnline
onSolver SolverOffline
offSolver) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
[ConfigDesc] -> Config -> IO ()
extendConfig (SolverAdapter EmptyExprBuilderState -> [ConfigDesc]
forall (st :: * -> *). SolverAdapter st -> [ConfigDesc]
WS.solver_adapter_config_options SolverAdapter EmptyExprBuilderState
adapter) (ExprBuilder x EmptyExprBuilderState (Flags fm) -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration (OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> ExprBuilder x EmptyExprBuilderState (Flags fm)
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak))
CruxOptions
-> SimulatorCallbacks msgs r
-> OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> [GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
-> ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
-> ProverCallback (ExprBuilder x EmptyExprBuilderState (Flags fm))
-> IO r
forall sym bak r t (st :: * -> *) fs msgs.
(sym ~ ExprBuilder t st fs, IsSymBackend sym bak, Logs msgs,
SupportsCruxLogMessage msgs) =>
CruxOptions
-> SimulatorCallbacks msgs r
-> bak
-> [GenericExecutionFeature sym]
-> ProfData sym
-> Maybe (SomeOnlineSolver sym bak)
-> ProverCallback sym
-> IO r
doSimWithResults CruxOptions
cruxOpts SimulatorCallbacks msgs r
simCallback OnlineBackend solver x EmptyExprBuilderState (Flags fm)
bak [GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
execFeatures ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
profInfo Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
monline ([SolverAdapter EmptyExprBuilderState]
-> CruxOptions
-> SimContext
(personality (ExprBuilder x EmptyExprBuilderState (Flags fm)))
(ExprBuilder x EmptyExprBuilderState (Flags fm))
ext
-> (Maybe (GroundEvalFn t)
-> LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError
-> IO (Doc Void))
-> Maybe
(Goals
(CrucibleAssumptions
(SymExpr (ExprBuilder x EmptyExprBuilderState (Flags fm))))
(LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError))
-> IO
(ProcessedGoals,
Maybe
(Goals
(CrucibleAssumptions
(SymExpr (ExprBuilder x EmptyExprBuilderState (Flags fm))))
(LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError,
[ProgramLoc],
ProofResult (ExprBuilder x EmptyExprBuilderState (Flags fm)))))
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 EmptyExprBuilderState
adapter])
Right (CCS.OnlyOfflineSolvers [SolverOffline]
offSolvers) ->
EmptyExprBuilderState x
-> CruxOptions
-> [SolverOffline]
-> (forall {fm :: FloatMode}.
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm)) =>
FloatModeRepr fm -> IO r)
-> IO r
forall solver (st :: * -> *) s a.
HasDefaultFloatRepr solver =>
st s
-> CruxOptions
-> [solver]
-> (forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> IO a)
-> IO a
withFloatRepr (forall t. EmptyExprBuilderState t
WE.EmptyExprBuilderState @s) CruxOptions
cruxOpts [SolverOffline]
offSolvers ((forall {fm :: FloatMode}.
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm)) =>
FloatModeRepr fm -> IO r)
-> IO r)
-> (forall {fm :: FloatMode}.
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm)) =>
FloatModeRepr fm -> IO r)
-> IO r
forall a b. (a -> b) -> a -> b
$ \FloatModeRepr fm
floatRepr -> do
[SolverOffline]
-> ([SolverAdapter EmptyExprBuilderState] -> IO r) -> IO r
forall (st :: * -> *) a.
[SolverOffline] -> ([SolverAdapter st] -> a) -> a
withSolverAdapters [SolverOffline]
offSolvers (([SolverAdapter EmptyExprBuilderState] -> IO r) -> IO r)
-> ([SolverAdapter EmptyExprBuilderState] -> IO r) -> IO r
forall a b. (a -> b) -> a -> b
$ \[SolverAdapter EmptyExprBuilderState]
adapters -> do
ExprBuilder x EmptyExprBuilderState (Flags fm)
sym <- FloatModeRepr fm
-> EmptyExprBuilderState x
-> NonceGenerator IO x
-> IO (ExprBuilder x EmptyExprBuilderState (Flags fm))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
WE.newExprBuilder FloatModeRepr fm
floatRepr EmptyExprBuilderState x
forall t. EmptyExprBuilderState t
WE.EmptyExprBuilderState NonceGenerator IO x
nonceGen
SimpleBackend x EmptyExprBuilderState (Flags fm)
bak <- ExprBuilder x EmptyExprBuilderState (Flags fm)
-> IO (SimpleBackend x EmptyExprBuilderState (Flags fm))
forall t (st :: * -> *) fs.
ExprBuilder t st fs -> IO (SimpleBackend t st fs)
CBS.newSimpleBackend ExprBuilder x EmptyExprBuilderState (Flags fm)
sym
CruxOptions
-> Maybe FilePath
-> ExprBuilder x EmptyExprBuilderState (Flags fm)
-> IO ()
forall sym t (st :: * -> *) fs.
(IsExprBuilder sym, sym ~ ExprBuilder t st fs) =>
CruxOptions -> Maybe FilePath -> sym -> IO ()
setupSolver CruxOptions
cruxOpts Maybe FilePath
forall a. Maybe a
Nothing ExprBuilder x EmptyExprBuilderState (Flags fm)
sym
[ConfigDesc] -> Config -> IO ()
extendConfig (SolverAdapter EmptyExprBuilderState -> [ConfigDesc]
forall (st :: * -> *). SolverAdapter st -> [ConfigDesc]
WS.solver_adapter_config_options (SolverAdapter EmptyExprBuilderState -> [ConfigDesc])
-> [SolverAdapter EmptyExprBuilderState] -> [ConfigDesc]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [SolverAdapter EmptyExprBuilderState]
adapters) (ExprBuilder x EmptyExprBuilderState (Flags fm) -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder x EmptyExprBuilderState (Flags fm)
sym)
([GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
execFeatures, ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
profInfo) <- CruxOptions
-> SimpleBackend x EmptyExprBuilderState (Flags fm)
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(SimpleBackend x EmptyExprBuilderState (Flags fm)))
-> IO
([GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))],
ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm)))
forall sym bak.
IsSymBackend sym bak =>
CruxOptions
-> bak
-> Maybe (SomeOnlineSolver sym bak)
-> IO ([GenericExecutionFeature sym], ProfData sym)
setupExecutionFeatures CruxOptions
cruxOpts SimpleBackend x EmptyExprBuilderState (Flags fm)
bak Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(SimpleBackend x EmptyExprBuilderState (Flags fm)))
forall a. Maybe a
Nothing
CruxOptions
-> SimulatorCallbacks msgs r
-> SimpleBackend x EmptyExprBuilderState (Flags fm)
-> [GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
-> ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(SimpleBackend x EmptyExprBuilderState (Flags fm)))
-> ProverCallback (ExprBuilder x EmptyExprBuilderState (Flags fm))
-> IO r
forall sym bak r t (st :: * -> *) fs msgs.
(sym ~ ExprBuilder t st fs, IsSymBackend sym bak, Logs msgs,
SupportsCruxLogMessage msgs) =>
CruxOptions
-> SimulatorCallbacks msgs r
-> bak
-> [GenericExecutionFeature sym]
-> ProfData sym
-> Maybe (SomeOnlineSolver sym bak)
-> ProverCallback sym
-> IO r
doSimWithResults CruxOptions
cruxOpts SimulatorCallbacks msgs r
simCallback SimpleBackend x EmptyExprBuilderState (Flags fm)
bak [GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
execFeatures ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
profInfo Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(SimpleBackend x EmptyExprBuilderState (Flags fm)))
forall a. Maybe a
Nothing ([SolverAdapter EmptyExprBuilderState]
-> CruxOptions
-> SimContext
(personality (ExprBuilder x EmptyExprBuilderState (Flags fm)))
(ExprBuilder x EmptyExprBuilderState (Flags fm))
ext
-> (Maybe (GroundEvalFn t)
-> LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError
-> IO (Doc Void))
-> Maybe
(Goals
(CrucibleAssumptions
(SymExpr (ExprBuilder x EmptyExprBuilderState (Flags fm))))
(LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError))
-> IO
(ProcessedGoals,
Maybe
(Goals
(CrucibleAssumptions
(SymExpr (ExprBuilder x EmptyExprBuilderState (Flags fm))))
(LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError,
[ProgramLoc],
ProofResult (ExprBuilder x EmptyExprBuilderState (Flags fm)))))
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 EmptyExprBuilderState]
adapters)
Right (CCS.OnlineSolverWithSeparateOnlineGoals SolverOnline
pathSolver SolverOnline
goalSolver) ->
CruxOptions
-> NonceGenerator IO x
-> SolverOnline
-> Maybe FilePath
-> EmptyExprBuilderState x
-> (forall {solver} {fm :: FloatMode}.
(OnlineSolver solver,
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm))) =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r
forall msgs scope (st :: * -> *) a.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions
-> NonceGenerator IO scope
-> SolverOnline
-> Maybe FilePath
-> st scope
-> (forall solver (fm :: FloatMode).
(OnlineSolver solver,
IsInterpretedFloatExprBuilder (ExprBuilder scope st (Flags fm))) =>
OnlineBackend solver scope st (Flags fm) -> IO a)
-> IO a
withSelectedOnlineBackend CruxOptions
cruxOpts NonceGenerator IO x
nonceGen SolverOnline
pathSolver Maybe FilePath
forall a. Maybe a
Nothing EmptyExprBuilderState x
forall t. EmptyExprBuilderState t
WE.EmptyExprBuilderState ((forall {solver} {fm :: FloatMode}.
(OnlineSolver solver,
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm))) =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r)
-> (forall {solver} {fm :: FloatMode}.
(OnlineSolver solver,
IsInterpretedFloatExprBuilder
(ExprBuilder x EmptyExprBuilderState (Flags fm))) =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r
forall a b. (a -> b) -> a -> b
$ \OnlineBackend solver x EmptyExprBuilderState (Flags fm)
pathSatBak -> do
let sym :: ExprBuilder x EmptyExprBuilderState (Flags fm)
sym = OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> ExprBuilder x EmptyExprBuilderState (Flags fm)
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym OnlineBackend solver x EmptyExprBuilderState (Flags fm)
pathSatBak
CruxOptions
-> Maybe FilePath
-> ExprBuilder x EmptyExprBuilderState (Flags fm)
-> IO ()
forall sym t (st :: * -> *) fs.
(IsExprBuilder sym, sym ~ ExprBuilder t st fs) =>
CruxOptions -> Maybe FilePath -> sym -> IO ()
setupSolver CruxOptions
cruxOpts (CruxOptions -> Maybe FilePath
pathSatSolverOutput CruxOptions
cruxOpts) ExprBuilder x EmptyExprBuilderState (Flags fm)
sym
([GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
execFeatures, ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
profInfo) <- CruxOptions
-> OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
-> IO
([GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))],
ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm)))
forall sym bak.
IsSymBackend sym bak =>
CruxOptions
-> bak
-> Maybe (SomeOnlineSolver sym bak)
-> IO ([GenericExecutionFeature sym], ProfData sym)
setupExecutionFeatures CruxOptions
cruxOpts OnlineBackend solver x EmptyExprBuilderState (Flags fm)
pathSatBak (SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm))
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
forall a. a -> Maybe a
Just (OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm))
forall sym scope (st :: * -> *) fs bak solver.
(sym ~ ExprBuilder scope st fs,
bak ~ OnlineBackend solver scope st fs, IsSymBackend sym bak,
OnlineSolver solver) =>
bak -> SomeOnlineSolver sym bak
SomeOnlineSolver OnlineBackend solver x EmptyExprBuilderState (Flags fm)
pathSatBak))
CruxOptions
-> SolverOnline
-> ExprBuilder x EmptyExprBuilderState (Flags fm)
-> (forall {solver}.
OnlineSolver solver =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r
forall msgs scope (st :: * -> *) fs a.
(Logs msgs, SupportsCruxLogMessage msgs,
IsInterpretedFloatExprBuilder (ExprBuilder scope st fs)) =>
CruxOptions
-> SolverOnline
-> ExprBuilder scope st fs
-> (forall solver.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO a)
-> IO a
withSelectedOnlineBackend' CruxOptions
cruxOpts SolverOnline
goalSolver ExprBuilder x EmptyExprBuilderState (Flags fm)
sym ((forall {solver}.
OnlineSolver solver =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r)
-> (forall {solver}.
OnlineSolver solver =>
OnlineBackend solver x EmptyExprBuilderState (Flags fm) -> IO r)
-> IO r
forall a b. (a -> b) -> a -> b
$ \OnlineBackend solver x EmptyExprBuilderState (Flags fm)
goalBak -> do
CruxOptions
-> SimulatorCallbacks msgs r
-> OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> [GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
-> ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
-> ProverCallback (ExprBuilder x EmptyExprBuilderState (Flags fm))
-> IO r
forall sym bak r t (st :: * -> *) fs msgs.
(sym ~ ExprBuilder t st fs, IsSymBackend sym bak, Logs msgs,
SupportsCruxLogMessage msgs) =>
CruxOptions
-> SimulatorCallbacks msgs r
-> bak
-> [GenericExecutionFeature sym]
-> ProfData sym
-> Maybe (SomeOnlineSolver sym bak)
-> ProverCallback sym
-> IO r
doSimWithResults CruxOptions
cruxOpts SimulatorCallbacks msgs r
simCallback OnlineBackend solver x EmptyExprBuilderState (Flags fm)
pathSatBak [GenericExecutionFeature
(ExprBuilder x EmptyExprBuilderState (Flags fm))]
execFeatures ProfData (ExprBuilder x EmptyExprBuilderState (Flags fm))
profInfo (SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm))
-> Maybe
(SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm)))
forall a. a -> Maybe a
Just (OnlineBackend solver x EmptyExprBuilderState (Flags fm)
-> SomeOnlineSolver
(ExprBuilder x EmptyExprBuilderState (Flags fm))
(OnlineBackend solver x EmptyExprBuilderState (Flags fm))
forall sym scope (st :: * -> *) fs bak solver.
(sym ~ ExprBuilder scope st fs,
bak ~ OnlineBackend solver scope st fs, IsSymBackend sym bak,
OnlineSolver solver) =>
bak -> SomeOnlineSolver sym bak
SomeOnlineSolver OnlineBackend solver x EmptyExprBuilderState (Flags fm)
pathSatBak)) (OnlineBackend solver t EmptyExprBuilderState (Flags fm)
-> CruxOptions
-> SimContext
(personality (ExprBuilder x EmptyExprBuilderState (Flags fm)))
(ExprBuilder x EmptyExprBuilderState (Flags fm))
ext
-> (Maybe (GroundEvalFn t)
-> LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError
-> IO (Doc Void))
-> Maybe
(Goals
(CrucibleAssumptions
(SymExpr (ExprBuilder x EmptyExprBuilderState (Flags fm))))
(LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError))
-> IO
(ProcessedGoals,
Maybe
(Goals
(CrucibleAssumptions
(SymExpr (ExprBuilder x EmptyExprBuilderState (Flags fm))))
(LabeledPred
(SymExpr
(ExprBuilder x EmptyExprBuilderState (Flags fm)) BaseBoolType)
SimError,
[ProgramLoc],
ProofResult (ExprBuilder x EmptyExprBuilderState (Flags fm)))))
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 solver x EmptyExprBuilderState (Flags fm)
OnlineBackend solver t EmptyExprBuilderState (Flags fm)
goalBak)
Left [FilePath]
rsns -> FilePath -> IO r
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath
"Invalid solver configuration:\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unlines [FilePath]
rsns)
doSimWithResults ::
forall sym bak r t st fs msgs.
sym ~ WE.ExprBuilder t st fs =>
IsSymBackend sym bak =>
Logs msgs =>
SupportsCruxLogMessage msgs =>
CruxOptions ->
SimulatorCallbacks msgs r ->
bak ->
[GenericExecutionFeature sym] ->
ProfData sym ->
Maybe (SomeOnlineSolver sym bak) ->
ProverCallback sym
->
IO r
doSimWithResults :: forall sym bak r t (st :: * -> *) fs msgs.
(sym ~ ExprBuilder t st fs, IsSymBackend sym bak, Logs msgs,
SupportsCruxLogMessage msgs) =>
CruxOptions
-> SimulatorCallbacks msgs r
-> bak
-> [GenericExecutionFeature sym]
-> ProfData sym
-> Maybe (SomeOnlineSolver sym bak)
-> ProverCallback sym
-> IO r
doSimWithResults CruxOptions
cruxOpts SimulatorCallbacks msgs r
simCallback bak
bak [GenericExecutionFeature sym]
execFeatures ProfData sym
profInfo Maybe (SomeOnlineSolver sym bak)
monline ProverCallback sym
goalProver = do
IORef ProgramCompleteness
compRef <- ProgramCompleteness -> IO (IORef ProgramCompleteness)
forall a. a -> IO (IORef a)
newIORef ProgramCompleteness
ProgramComplete
IORef (Seq (ProcessedGoals, ProvedGoals))
glsRef <- Seq (ProcessedGoals, ProvedGoals)
-> IO (IORef (Seq (ProcessedGoals, ProvedGoals)))
forall a. a -> IO (IORef a)
newIORef Seq (ProcessedGoals, ProvedGoals)
forall a. Seq a
Seq.empty
FrameIdentifier
frm <- bak -> IO FrameIdentifier
forall sym bak. IsSymBackend sym bak => bak -> IO FrameIdentifier
pushAssumptionFrame bak
bak
SimulatorHooks bak -> Maybe (SomeOnlineSolver sym bak) -> IO (RunnableState sym)
setup bak -> IO (Explainer sym t Void)
onError bak -> CruxSimulationResult -> IO r
interpretResult <-
SimulatorCallbacks msgs r
-> forall sym bak t (st :: * -> *) fs.
(IsSymBackend sym bak, Logs msgs, sym ~ ExprBuilder t st fs) =>
IO (SimulatorHooks sym bak t r)
forall msgs r.
SimulatorCallbacks msgs r
-> forall sym bak t (st :: * -> *) fs.
(IsSymBackend sym bak, Logs msgs, sym ~ ExprBuilder t st fs) =>
IO (SimulatorHooks sym bak t r)
getSimulatorCallbacks SimulatorCallbacks msgs r
simCallback
ProfData sym -> forall a. FunctionName -> IO a -> IO a
forall sym. ProfData sym -> forall a. FunctionName -> IO a -> IO a
inFrame ProfData sym
profInfo FunctionName
"<Crux>" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
RunnableStateWithExtensions ExecState (personality sym) sym ext (RegEntry sym UnitType)
initSt [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
exts <- bak -> Maybe (SomeOnlineSolver sym bak) -> IO (RunnableState sym)
setup bak
bak Maybe (SomeOnlineSolver sym bak)
monline
Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void)
explainFailure <- bak -> IO (Explainer sym t Void)
onError bak
bak
case CruxOptions -> PathStrategy
pathStrategy CruxOptions
cruxOpts of
PathStrategy
AlwaysMergePaths ->
do ExecResult (personality sym) sym ext (RegEntry sym UnitType)
res <- [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
-> ExecState (personality sym) sym ext (RegEntry sym UnitType)
-> IO
(ExecResult (personality sym) sym ext (RegEntry sym UnitType))
forall p sym ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
[ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
executeCrucible ((GenericExecutionFeature sym
-> ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType))
-> [GenericExecutionFeature sym]
-> [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
forall a b. (a -> b) -> [a] -> [b]
map GenericExecutionFeature sym
-> ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)
forall sym ext p rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
GenericExecutionFeature sym -> ExecutionFeature p sym ext rtp
genericToExecutionFeature [GenericExecutionFeature sym]
execFeatures [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
-> [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
-> [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
forall a. [a] -> [a] -> [a]
++ [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
exts) ExecState (personality sym) sym ext (RegEntry sym UnitType)
initSt
IO Bool -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO Bool -> IO ()) -> IO Bool -> IO ()
forall a b. (a -> b) -> a -> b
$ IORef ProgramCompleteness
-> IORef (Seq (ProcessedGoals, ProvedGoals))
-> FrameIdentifier
-> (Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void))
-> Result personality (ExprBuilder t st fs)
-> IO Bool
forall (personality :: * -> *).
IORef ProgramCompleteness
-> IORef (Seq (ProcessedGoals, ProvedGoals))
-> FrameIdentifier
-> (Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void))
-> Result personality (ExprBuilder t st fs)
-> IO Bool
resultCont IORef ProgramCompleteness
compRef IORef (Seq (ProcessedGoals, ProvedGoals))
glsRef FrameIdentifier
frm Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void)
explainFailure (ExecResult
(personality (ExprBuilder t st fs))
(ExprBuilder t st fs)
ext
(RegEntry (ExprBuilder t st fs) UnitType)
-> Result personality (ExprBuilder t st fs)
forall (personality :: * -> *) sym ext.
ExecResult (personality sym) sym ext (RegEntry sym UnitType)
-> Result personality sym
Result ExecResult (personality sym) sym ext (RegEntry sym UnitType)
ExecResult
(personality (ExprBuilder t st fs))
(ExprBuilder t st fs)
ext
(RegEntry (ExprBuilder t st fs) UnitType)
res)
PathStrategy
SplitAndExploreDepthFirst ->
do (Word64
i,Seq (WorkItem (personality sym) sym ext (RegEntry sym UnitType))
ws) <- [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
-> ExecState (personality sym) sym ext (RegEntry sym UnitType)
-> (ExecResult (personality sym) sym ext (RegEntry sym UnitType)
-> IO Bool)
-> IO
(Word64,
Seq (WorkItem (personality sym) sym ext (RegEntry sym UnitType)))
forall p sym ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
[ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp
-> (ExecResult p sym ext rtp -> IO Bool)
-> IO (Word64, Seq (WorkItem p sym ext rtp))
executeCrucibleDFSPaths
((GenericExecutionFeature sym
-> ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType))
-> [GenericExecutionFeature sym]
-> [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
forall a b. (a -> b) -> [a] -> [b]
map GenericExecutionFeature sym
-> ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)
forall sym ext p rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
GenericExecutionFeature sym -> ExecutionFeature p sym ext rtp
genericToExecutionFeature [GenericExecutionFeature sym]
execFeatures [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
-> [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
-> [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
forall a. [a] -> [a] -> [a]
++ [ExecutionFeature
(personality sym) sym ext (RegEntry sym UnitType)]
exts)
ExecState (personality sym) sym ext (RegEntry sym UnitType)
initSt
(IORef ProgramCompleteness
-> IORef (Seq (ProcessedGoals, ProvedGoals))
-> FrameIdentifier
-> (Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void))
-> Result personality (ExprBuilder t st fs)
-> IO Bool
forall (personality :: * -> *).
IORef ProgramCompleteness
-> IORef (Seq (ProcessedGoals, ProvedGoals))
-> FrameIdentifier
-> (Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void))
-> Result personality (ExprBuilder t st fs)
-> IO Bool
resultCont IORef ProgramCompleteness
compRef IORef (Seq (ProcessedGoals, ProvedGoals))
glsRef FrameIdentifier
frm Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void)
explainFailure (Result personality (ExprBuilder t st fs) -> IO Bool)
-> (ExecResult (personality sym) sym ext (RegEntry sym UnitType)
-> Result personality (ExprBuilder t st fs))
-> ExecResult (personality sym) sym ext (RegEntry sym UnitType)
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecResult (personality sym) sym ext (RegEntry sym UnitType)
-> Result personality sym
ExecResult (personality sym) sym ext (RegEntry sym UnitType)
-> Result personality (ExprBuilder t st fs)
forall (personality :: * -> *) sym ext.
ExecResult (personality sym) sym ext (RegEntry sym UnitType)
-> Result personality sym
Result)
CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux (Word64 -> CruxLogMessage
Log.TotalPathsExplored Word64
i)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Seq (WorkItem (personality sym) sym ext (RegEntry sym UnitType))
-> Bool
forall a. Seq a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Seq (WorkItem (personality sym) sym ext (RegEntry sym UnitType))
ws) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux (Int -> CruxLogMessage
Log.PathsUnexplored (Seq (WorkItem (personality sym) sym ext (RegEntry sym UnitType))
-> Int
forall a. Seq a -> Int
Seq.length Seq (WorkItem (personality sym) sym ext (RegEntry sym UnitType))
ws))
CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
Log.SimulationComplete
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CruxOptions -> Bool
isProfiling CruxOptions
cruxOpts) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ ProfData sym -> IO ()
forall sym. ProfData sym -> IO ()
writeProf ProfData sym
profInfo
CruxSimulationResult
result <- ProgramCompleteness
-> Seq (ProcessedGoals, ProvedGoals) -> CruxSimulationResult
CruxSimulationResult (ProgramCompleteness
-> Seq (ProcessedGoals, ProvedGoals) -> CruxSimulationResult)
-> IO ProgramCompleteness
-> IO (Seq (ProcessedGoals, ProvedGoals) -> CruxSimulationResult)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef ProgramCompleteness -> IO ProgramCompleteness
forall a. IORef a -> IO a
readIORef IORef ProgramCompleteness
compRef IO (Seq (ProcessedGoals, ProvedGoals) -> CruxSimulationResult)
-> IO (Seq (ProcessedGoals, ProvedGoals))
-> IO CruxSimulationResult
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IORef (Seq (ProcessedGoals, ProvedGoals))
-> IO (Seq (ProcessedGoals, ProvedGoals))
forall a. IORef a -> IO a
readIORef IORef (Seq (ProcessedGoals, ProvedGoals))
glsRef
bak -> CruxSimulationResult -> IO r
interpretResult bak
bak CruxSimulationResult
result
where
failfast :: Bool
failfast = CruxOptions -> Bool
proofGoalsFailFast CruxOptions
cruxOpts
resultCont ::
IORef ProgramCompleteness
-> IORef (Seq.Seq (ProcessedGoals, ProvedGoals))
-> FrameIdentifier
-> (Maybe (WE.GroundEvalFn t) -> LabeledPred (WE.Expr t BaseBoolType) SimError -> IO (Doc Void))
-> Result personality (WE.ExprBuilder t st fs)
-> IO Bool
resultCont :: forall (personality :: * -> *).
IORef ProgramCompleteness
-> IORef (Seq (ProcessedGoals, ProvedGoals))
-> FrameIdentifier
-> (Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void))
-> Result personality (ExprBuilder t st fs)
-> IO Bool
resultCont IORef ProgramCompleteness
compRef IORef (Seq (ProcessedGoals, ProvedGoals))
glsRef FrameIdentifier
frm Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void)
explainFailure (Result ExecResult
(personality (ExprBuilder t st fs))
(ExprBuilder t st fs)
ext
(RegEntry (ExprBuilder t st fs) UnitType)
res) =
do Bool
timedOut <-
case ExecResult
(personality (ExprBuilder t st fs))
(ExprBuilder t st fs)
ext
(RegEntry (ExprBuilder t st fs) UnitType)
res of
TimeoutResult {} ->
do CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
Log.SimulationTimedOut
IORef ProgramCompleteness -> ProgramCompleteness -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef ProgramCompleteness
compRef ProgramCompleteness
ProgramIncomplete
Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
ExecResult
(personality (ExprBuilder t st fs))
(ExprBuilder t st fs)
ext
(RegEntry (ExprBuilder t st fs) UnitType)
_ -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
bak -> FrameIdentifier -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> FrameIdentifier -> IO ()
popUntilAssumptionFrame bak
bak FrameIdentifier
frm
let ctx :: SimContext
(personality (ExprBuilder t st fs)) (ExprBuilder t st fs) ext
ctx = ExecResult
(personality (ExprBuilder t st fs))
(ExprBuilder t st fs)
ext
(RegEntry (ExprBuilder t st fs) UnitType)
-> SimContext
(personality (ExprBuilder t st fs)) (ExprBuilder t st fs) ext
forall p sym ext r. ExecResult p sym ext r -> SimContext p sym ext
execResultContext ExecResult
(personality (ExprBuilder t st fs))
(ExprBuilder t st fs)
ext
(RegEntry (ExprBuilder t st fs) UnitType)
res
ProfData sym -> forall a. FunctionName -> IO a -> IO a
forall sym. ProfData sym -> forall a. FunctionName -> IO a -> IO a
inFrame ProfData sym
profInfo FunctionName
"<Prove Goals>" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
Maybe
(Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError))
todo <- bak
-> IO
(Maybe
(Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)))
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (ProofObligations sym)
getProofObligations bak
bak
CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux (CruxLogMessage -> IO ()) -> CruxLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$ [LogProofObligation] -> CruxLogMessage
Log.ProofObligations (ProofGoal
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)
-> LogProofObligation
ProofObligation (ExprBuilder t Any Any) -> LogProofObligation
forall t (st :: * -> *) fs.
ProofObligation (ExprBuilder t st fs) -> LogProofObligation
LogProofObligation (ProofGoal
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)
-> LogProofObligation)
-> [ProofGoal
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)]
-> [LogProofObligation]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ProofGoal
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)]
-> (Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)
-> [ProofGoal
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)])
-> Maybe
(Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError))
-> [ProofGoal
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)
-> [ProofGoal
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)]
forall asmp goal.
Monoid asmp =>
Goals asmp goal -> [ProofGoal asmp goal]
goalsToList Maybe
(Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError))
todo)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe
(Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError))
-> Bool
forall a. Maybe a -> Bool
isJust Maybe
(Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError))
todo) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
Log.AttemptingProvingVCs
(ProcessedGoals
nms, Maybe
(Goals
(CrucibleAssumptions (Expr t))
(LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
ProofResult (ExprBuilder t st fs)))
proved) <- 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)))
ProverCallback sym
goalProver CruxOptions
cruxOpts SimCtxt personality sym ext
SimContext
(personality (ExprBuilder t st fs)) (ExprBuilder t st fs) ext
ctx Explainer sym t Void
Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void)
explainFailure Maybe (Goals (Assumptions sym) (Assertion sym))
Maybe
(Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred
(SymExpr (ExprBuilder t st fs) BaseBoolType) SimError))
todo
Maybe ProvedGoals
mgt <- ExprBuilder t st fs
-> Maybe
(Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError,
[ProgramLoc], ProofResult (ExprBuilder t st fs)))
-> IO (Maybe ProvedGoals)
forall sym.
IsSymInterface sym =>
sym
-> Maybe
(Goals
(Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
-> IO (Maybe ProvedGoals)
provedGoalsTree (bak -> ExprBuilder t st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak) Maybe
(Goals
(CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
(LabeledPred (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError,
[ProgramLoc], ProofResult (ExprBuilder t st fs)))
Maybe
(Goals
(CrucibleAssumptions (Expr t))
(LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
ProofResult (ExprBuilder t st fs)))
proved
case Maybe ProvedGoals
mgt of
Maybe ProvedGoals
Nothing -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool
not Bool
timedOut)
Just ProvedGoals
gt ->
do IORef (Seq (ProcessedGoals, ProvedGoals))
-> (Seq (ProcessedGoals, ProvedGoals)
-> Seq (ProcessedGoals, ProvedGoals))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (Seq (ProcessedGoals, ProvedGoals))
glsRef (Seq (ProcessedGoals, ProvedGoals)
-> (ProcessedGoals, ProvedGoals)
-> Seq (ProcessedGoals, ProvedGoals)
forall a. Seq a -> a -> Seq a
Seq.|> (ProcessedGoals
nms,ProvedGoals
gt))
Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool
not (Bool
timedOut Bool -> Bool -> Bool
|| (Bool
failfast Bool -> Bool -> Bool
&& ProcessedGoals -> Integer
disprovedGoals ProcessedGoals
nms Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0)))
isProfiling :: CruxOptions -> Bool
isProfiling :: CruxOptions -> Bool
isProfiling CruxOptions
cruxOpts =
CruxOptions -> Bool
profileCrucibleFunctions CruxOptions
cruxOpts Bool -> Bool -> Bool
|| CruxOptions -> Bool
profileSolver CruxOptions
cruxOpts Bool -> Bool -> Bool
|| CruxOptions -> Bool
branchCoverage CruxOptions
cruxOpts
computeExitCode :: CruxSimulationResult -> ExitCode
computeExitCode :: CruxSimulationResult -> ExitCode
computeExitCode (CruxSimulationResult ProgramCompleteness
cmpl Seq (ProcessedGoals, ProvedGoals)
gls) = [ExitCode] -> ExitCode
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([ExitCode] -> ExitCode)
-> (Seq (ProcessedGoals, ProvedGoals) -> [ExitCode])
-> Seq (ProcessedGoals, ProvedGoals)
-> ExitCode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExitCode
baseExitCode -> [ExitCode] -> [ExitCode]
forall a. a -> [a] -> [a]
:) ([ExitCode] -> [ExitCode])
-> (Seq (ProcessedGoals, ProvedGoals) -> [ExitCode])
-> Seq (ProcessedGoals, ProvedGoals)
-> [ExitCode]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ProcessedGoals, ProvedGoals) -> ExitCode)
-> [(ProcessedGoals, ProvedGoals)] -> [ExitCode]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProcessedGoals, ProvedGoals) -> ExitCode
forall {b}. (ProcessedGoals, b) -> ExitCode
f ([(ProcessedGoals, ProvedGoals)] -> [ExitCode])
-> (Seq (ProcessedGoals, ProvedGoals)
-> [(ProcessedGoals, ProvedGoals)])
-> Seq (ProcessedGoals, ProvedGoals)
-> [ExitCode]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (ProcessedGoals, ProvedGoals)
-> [(ProcessedGoals, ProvedGoals)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Seq (ProcessedGoals, ProvedGoals) -> ExitCode)
-> Seq (ProcessedGoals, ProvedGoals) -> ExitCode
forall a b. (a -> b) -> a -> b
$ Seq (ProcessedGoals, ProvedGoals)
gls
where
base :: ExitCode
base = case ProgramCompleteness
cmpl of
ProgramCompleteness
ProgramComplete -> ExitCode
ExitSuccess
ProgramCompleteness
ProgramIncomplete -> Int -> ExitCode
ExitFailure Int
1
f :: (ProcessedGoals, b) -> ExitCode
f (ProcessedGoals
nms,b
_gl) =
let tot :: Integer
tot = ProcessedGoals -> Integer
totalProcessedGoals ProcessedGoals
nms
proved :: Integer
proved = ProcessedGoals -> Integer
provedGoals ProcessedGoals
nms
in if Integer
proved Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
tot then
ExitCode
ExitSuccess
else
Int -> ExitCode
ExitFailure Int
1