{-# 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 -- for the export list
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 []

-- | A crucible @ExecState@ that is ready to be passed into the simulator.
--   This will usually, but not necessarily, be an @InitialState@.
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

-- | Individual crux tools will generally call the @runSimulator@ combinator to
--   handle the nitty-gritty of setting up and running the simulator. Tools
--   provide @SimulatorCallbacks@ to hook into the simulation process at three
--   points:
--
--   * Before simulation begins, to set up global variables, register override
--     functions, construct the initial program entry point, and generally do
--     any necessary language-specific setup (i.e., to produce a 'RunnableState')
--   * When simulation ends with an assertion failure ('Explainer')
--   * When simulation ends, regardless of the outcome, to interpret the results.
--
--   All of these callbacks have access to the symbolic backend.
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)
    }


-- | A GADT to capture the online solver constraints when we need them
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

-- | See 'SimulatorCallbacks'
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
    }

-- | Given the result of a simulation and proof run, report the overall
--   status, generate user-consumable reports and compute the exit code.
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 -- print goals that failed and overall result
     Bool -> CruxSimulationResult -> IO ()
forall msgs. Logs msgs => Bool -> CruxSimulationResult -> IO ()
logSimResult Bool
showFailedGoals CruxSimulationResult
res

     -- Generate report
     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


-- | Load crux generic and the provided options, and provide them to
--   the given continuation.
--
--   IMPORTANT:  This processes options like @help@ and @version@, which
--   just print something and exit, so this function may never call
--   its continuation.
loadOptions ::
  SupportsCruxLogMessage msgs =>
  (Maybe OutputOptions -> OutputConfig msgs) ->
  Text {- ^ Name -} ->
  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
  -- Ideally, this would be done in the log handler.  We will soon try to change
  -- the logging mechanism so thaat it prefers 'Doc' over 'Text' so that layout
  -- decisions can be delayed to the log handlers.
  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)


-- | Create an OutputConfig for Crux, based on an indication of whether colored
-- output should be used, the normal and error output handles, and the parsed
-- CruxOptions.
--
-- If no CruxOptions are available (i.e. Nothing, as used in the preliminary
-- portions of loadOptions), then a default output stance is applied; the
-- default stance is described along with the individual option below.
--
-- The following CruxOptions affect the generated OutputConfig:
--
--  * noColorsErr    (default stance: False when the error handle supports
--    colors, as reported by System.Console.ANSI.hSupportsANSIColor)
--  * noColorsOut    (default stance: False when the output handle supports
--    colors, as reported by System.Console.ANSI.hSupportsANSIColor)
--  * printFailures  (default stance: True)
--  * quietMode      (default stance: False)
--  * simVerbose     (default stance: False)
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
                   -- TODO simVerbose may not be the best setting to use here...
                   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


--------------------------------------------------------------------------------

-- | For a given configuration, compute the 'FloatModeRepr'
--
-- Note that this needs to be CPS-ed because of the type parameter to the float
-- mode.  Also note that we can't use this function in
-- 'withSelectedOnlineBackend', unfortunately, because that function requires a
-- 'IsInterpretedFloatExprBuilder' constraint that we don't seem to have a way
-- to capture in this CPS-ed style.
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]")

-- | Parse through the options structure to determine which online backend to
-- instantiate (including the chosen floating point mode).
--
-- The choice of solver is provided as a separate argument (the
-- 'CCS.SolverOnline').  This function dispatches primarily on floating point
-- mode.  An explicit floating point mode can be provided if it has to match
-- another solver that has already started.  This code is slightly complicated
-- and duplicated because it is very hard to quantify over 'FloatModeRepr's in
-- such a way that captures the necessary 'IsInterpretedFloatExprBuilder'
-- constraints.
withSelectedOnlineBackend :: forall msgs scope st a.
  Logs msgs =>
  SupportsCruxLogMessage msgs =>
  CruxOptions ->
  NonceGenerator IO scope ->
  CCS.SolverOnline ->
  Maybe String ->
  st scope ->
  -- The string is an optional explicitly-requested float mode that supersedes the choice in
  -- the configuration (probably due to using two different online connections)
  (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
       -- We don't have a timeout option for STP
       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


-- | Common setup for all solver connections
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)

  -- Turn on hash-consing, if enabled
  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
  -- The simulator verbosity is one less than our verbosity.
  -- In this way, we can say things, without the simulator also
  -- being verbose
  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

-- | Common code for initializing all of the requested execution features
--
-- This function is a bit funny because one feature, path satisfiability
-- checking, requires on online solver while the others do not.  In order to
-- maximally reuse code, we pass in the necessary online constraints as an extra
-- argument when we have them available (i.e., when we build an online solver)
-- and elide them otherwise.
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
  -- Setup profiling
  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

  -- Global timeout
  [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

  -- Loop bound
  [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 {- side cond: yes -}

  -- Recursion bound
  [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 {- side cond: yes -}

  -- Check path satisfiability
  [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 []

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

-- | Select the What4 solver adapter for the user's solver choice (used for
-- offline solvers)
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))

-- | Parse through all of the user-provided options and start up the verification process
--
-- This figures out which solvers need to be run, and in which modes.  It takes
-- as arguments some of the results of common setup code.  It also tries to
-- minimize code duplication between the different verification paths (e.g.,
-- online vs offline solving).
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
          -- We have to add the configuration options from the solver adapter,
          -- since they weren't included in the symbolic backend configuration
          -- with the initial setup of the online solver (since it could have
          -- been a different solver)
          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
          -- Since we have a bare SimpleBackend here, we have to initialize it
          -- with the options taken from the solver adapter (e.g., solver path)
          [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) ->
      -- This case is probably the most complicated because it needs two
      -- separate online solvers.  The two must agree on the floating point
      -- mode.
      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)


-- | Core invocation of the symbolic execution engine
--
-- This is separated out so that we don't have to duplicate the code sequence in
-- 'runSimulator'.  The strategy used to ultimately discharge proof obligations
-- is a parameter to allow this code to use either an online or offline solver
-- connection.
--
-- The main work in this function is setting up appropriate solver frames and
-- traversing the goals tree, as well as handling some reporting.
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
    {- ^ The function to use to prove goals; this is intended to be
         one of 'proveGoalsOffline' or 'proveGoalsOnline' -} ->
  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
    -- perform tool-specific setup
    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

    -- execute the simulator
    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