-- |
-- Module      :  Cryptol.Symbolic.What4
-- Copyright   :  (c) 2013-2020 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ParallelListComp #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ViewPatterns #-}

module Cryptol.Symbolic.What4
 ( W4ProverConfig
 , defaultProver
 , proverNames
 , setupProver
 , satProve
 , satProveOffline
 , W4Exception(..)
 ) where

import Control.Applicative
import Control.Concurrent.Async
import Control.Concurrent.MVar
import Control.Monad.IO.Class
import Control.Monad (when, foldM, forM_, void)
import qualified Control.Exception as X
import System.IO (Handle, IOMode(..), withFile)
import Data.Time
import Data.IORef
import Data.List (intercalate, inits)
import Data.List.NonEmpty (NonEmpty(..))
import Data.Proxy
import qualified Data.Map as Map
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.List.NonEmpty as NE
import System.Exit

import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Base as M
import qualified Cryptol.ModuleSystem.Monad as M
import qualified Cryptol.ModuleSystem.Name as M

import qualified Cryptol.Backend.FloatHelpers as FH
import           Cryptol.Backend.What4

import qualified Cryptol.Eval as Eval
import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Value as Eval
import           Cryptol.Eval.Type (TValue)
import           Cryptol.Eval.What4

import           Cryptol.Parser.Position (emptyRange)
import           Cryptol.Symbolic
import           Cryptol.TypeCheck.AST
import           Cryptol.Utils.Logger(logPutStrLn,logPutStr,Logger)
import           Cryptol.Utils.Ident (preludeReferenceName, prelPrim, identText)

import qualified What4.Config as W4
import qualified What4.Interface as W4
import qualified What4.Expr.Builder as W4
import qualified What4.Expr.GroundEval as W4
import qualified What4.SatResult as W4
import qualified What4.SFloat as W4
import qualified What4.SWord as SW
import           What4.Solver
import qualified What4.Solver.Bitwuzla as W4
import qualified What4.Solver.Boolector as W4
import qualified What4.Solver.CVC4 as W4
import qualified What4.Solver.CVC5 as W4
import qualified What4.Solver.ExternalABC as W4
import qualified What4.Solver.Yices as W4
import qualified What4.Solver.Z3 as W4
import qualified What4.Solver.Adapter as W4
import qualified What4.Protocol.Online as W4
import qualified What4.Protocol.SMTLib2 as W4
import qualified What4.ProblemFeatures as W4

import qualified Data.BitVector.Sized as BV
import           Data.Parameterized.Nonce


import Prelude ()
import Prelude.Compat

data W4Exception
  = W4Ex X.SomeException
  | W4PortfolioFailure [ (Either X.SomeException (Maybe String, String)) ]

instance Show W4Exception where
  show :: W4Exception -> String
show (W4Ex SomeException
e) = SomeException -> String
forall e. Exception e => e -> String
X.displayException SomeException
e
  show (W4PortfolioFailure [Either SomeException (Maybe String, String)]
exs) =
       [String] -> String
unlines (String
"All solveres in the portfolio failed!"String -> [String] -> [String]
forall a. a -> [a] -> [a]
:(Either SomeException (Maybe String, String) -> String)
-> [Either SomeException (Maybe String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Either SomeException (Maybe String, String) -> String
forall {e}.
Exception e =>
Either e (Maybe String, String) -> String
f [Either SomeException (Maybe String, String)]
exs)
    where
    f :: Either e (Maybe String, String) -> String
f (Left e
e) = e -> String
forall e. Exception e => e -> String
X.displayException e
e
    f (Right (Maybe String
Nothing, String
msg)) = String
msg
    f (Right (Just String
nm, String
msg)) = String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg

instance X.Exception W4Exception

rethrowW4Exception :: IO a -> IO a
rethrowW4Exception :: forall a. IO a -> IO a
rethrowW4Exception IO a
m = (SomeException -> Maybe SomeException)
-> IO a -> (SomeException -> IO a) -> IO a
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
X.catchJust SomeException -> Maybe SomeException
f IO a
m (W4Exception -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (W4Exception -> IO a)
-> (SomeException -> W4Exception) -> SomeException -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> W4Exception
W4Ex)
  where
  f :: SomeException -> Maybe SomeException
f SomeException
e
    | Just ( AsyncException
_ :: X.AsyncException) <- SomeException -> Maybe AsyncException
forall e. Exception e => SomeException -> Maybe e
X.fromException SomeException
e = Maybe SomeException
forall a. Maybe a
Nothing
    | Just ( Unsupported
_ :: Eval.Unsupported) <- SomeException -> Maybe Unsupported
forall e. Exception e => SomeException -> Maybe e
X.fromException SomeException
e = Maybe SomeException
forall a. Maybe a
Nothing
    | Bool
otherwise = SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just SomeException
e

protectStack :: (String -> M.ModuleCmd a)
             -> M.ModuleCmd a
             -> M.ModuleCmd a
protectStack :: forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack String -> ModuleCmd a
mkErr ModuleCmd a
cmd ModuleInput IO
modEnv =
  IO (ModuleRes a) -> IO (ModuleRes a)
forall a. IO a -> IO a
rethrowW4Exception (IO (ModuleRes a) -> IO (ModuleRes a))
-> IO (ModuleRes a) -> IO (ModuleRes a)
forall a b. (a -> b) -> a -> b
$
  (AsyncException -> Maybe ())
-> IO (ModuleRes a) -> (() -> IO (ModuleRes a)) -> IO (ModuleRes a)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
X.catchJust AsyncException -> Maybe ()
isOverflow (ModuleCmd a
cmd ModuleInput IO
modEnv) () -> IO (ModuleRes a)
handler
  where isOverflow :: AsyncException -> Maybe ()
isOverflow AsyncException
X.StackOverflow = () -> Maybe ()
forall a. a -> Maybe a
Just ()
        isOverflow AsyncException
_               = Maybe ()
forall a. Maybe a
Nothing
        msg :: String
msg = String
"Symbolic evaluation failed to terminate."
        handler :: () -> IO (ModuleRes a)
handler () = String -> ModuleCmd a
mkErr String
msg ModuleInput IO
modEnv


-- | Returns definitions, together with the value and it safety predicate.
doW4Eval ::
  (W4.IsExprBuilder sym, MonadIO m) =>
  sym -> W4Eval sym a -> m (W4.Pred sym, a)
doW4Eval :: forall sym (m :: * -> *) a.
(IsExprBuilder sym, MonadIO m) =>
sym -> W4Eval sym a -> m (Pred sym, a)
doW4Eval sym
sym W4Eval sym a
m =
  do W4Result sym a
res <- IO (W4Result sym a) -> m (W4Result sym a)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (W4Result sym a) -> m (W4Result sym a))
-> IO (W4Result sym a) -> m (W4Result sym a)
forall a b. (a -> b) -> a -> b
$ CallStack -> Eval (W4Result sym a) -> IO (W4Result sym a)
forall a. CallStack -> Eval a -> IO a
Eval.runEval CallStack
forall a. Monoid a => a
mempty (W4Eval sym a -> sym -> Eval (W4Result sym a)
forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval W4Eval sym a
m sym
sym)
     case W4Result sym a
res of
       W4Error EvalErrorEx
err  -> IO (Pred sym, a) -> m (Pred sym, a)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (EvalErrorEx -> IO (Pred sym, a)
forall e a. Exception e => e -> IO a
X.throwIO EvalErrorEx
err)
       W4Result Pred sym
p a
x -> (Pred sym, a) -> m (Pred sym, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred sym
p,a
x)

-- | Wraps a 'W4.ConfigOption' to provide a consistent interface for setting
--   solver goal timeouts (see 'configTimeoutMilliSeconds', 'configTimeoutSeconds', 'setConfigTimeout').
data ConfigTimeout = 
        ConfigTimeout 
          (W4.ConfigOption W4.BaseIntegerType)
          -- | Translate a 'W4.SolverGoalTimeout' into the integer backing this config option.
          (W4.SolverGoalTimeout -> Integer)

-- | Construct a 'ConfigTimeout' from a 'W4.ConfigOption', where the given
--   option configures a solver-specific timeout measured in milliseconds.
configTimeoutMilliSeconds :: W4.ConfigOption W4.BaseIntegerType -> ConfigTimeout
configTimeoutMilliSeconds :: ConfigOption BaseIntegerType -> ConfigTimeout
configTimeoutMilliSeconds ConfigOption BaseIntegerType
opt = ConfigOption BaseIntegerType
-> (SolverGoalTimeout -> Integer) -> ConfigTimeout
ConfigTimeout ConfigOption BaseIntegerType
opt SolverGoalTimeout -> Integer
W4.getGoalTimeoutInMilliSeconds

-- | Construct a 'ConfigTimeout' from a 'W4.ConfigOption', where the given
--   option configures a solver-specific timeout measured in seconds. 
--   Rounds up to at least 1 second when setting a non-zero timeout 
--   (see 'W4.getGoalTimeoutInSeconds').
configTimeoutSeconds :: W4.ConfigOption W4.BaseIntegerType -> ConfigTimeout
configTimeoutSeconds :: ConfigOption BaseIntegerType -> ConfigTimeout
configTimeoutSeconds ConfigOption BaseIntegerType
opt = ConfigOption BaseIntegerType
-> (SolverGoalTimeout -> Integer) -> ConfigTimeout
ConfigTimeout ConfigOption BaseIntegerType
opt SolverGoalTimeout -> Integer
W4.getGoalTimeoutInSeconds

setConfigTimeout :: 
  W4.IsExprBuilder sym =>
  ConfigTimeout ->
  W4.SolverGoalTimeout ->
  sym ->
  IO ()
setConfigTimeout :: forall sym.
IsExprBuilder sym =>
ConfigTimeout -> SolverGoalTimeout -> sym -> IO ()
setConfigTimeout (ConfigTimeout ConfigOption BaseIntegerType
opt SolverGoalTimeout -> Integer
toOpt) SolverGoalTimeout
t sym
sym = 
  do OptionSetting BaseIntegerType
optSetting <- ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
W4.getOptionSetting ConfigOption BaseIntegerType
opt (sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
W4.getConfiguration sym
sym)
     OptionSetResult
_ <- OptionSetting BaseIntegerType -> Integer -> IO OptionSetResult
forall (tp :: BaseType) a.
Opt tp a =>
OptionSetting tp -> a -> IO OptionSetResult
W4.trySetOpt OptionSetting BaseIntegerType
optSetting (SolverGoalTimeout -> Integer
toOpt SolverGoalTimeout
t)
     () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

data AnAdapter
  = AnAdapter (forall st. SolverAdapter st)
  | forall s. W4.OnlineSolver s =>
     AnOnlineAdapter
       String
       W4.ProblemFeatures
       [W4.ConfigDesc]
       ConfigTimeout
       (Proxy s)

data W4ProverConfig
  = W4ProverConfig AnAdapter
  | W4OfflineConfig
  | W4Portfolio (NonEmpty AnAdapter)

adapters :: W4ProverConfig -> [AnAdapter]
adapters :: W4ProverConfig -> [AnAdapter]
adapters W4ProverConfig
cfg = case W4ProverConfig
cfg of
  W4ProverConfig AnAdapter
adpt -> [AnAdapter
adpt]
  W4ProverConfig
W4OfflineConfig -> []
  W4Portfolio NonEmpty AnAdapter
adpts -> NonEmpty AnAdapter -> [AnAdapter]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty AnAdapter
adpts

proverConfigs :: [(String, W4ProverConfig)]
proverConfigs :: [(String, W4ProverConfig)]
proverConfigs =
  [ (String
"w4-cvc4"      , AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
cvc4OnlineAdapter)
  , (String
"w4-cvc5"      , AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
cvc5OnlineAdapter)
  , (String
"w4-yices"     , AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
yicesOnlineAdapter)
  , (String
"w4-z3"        , AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
z3OnlineAdapter)
  , (String
"w4-bitwuzla"  , AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
bitwuzlaOnlineAdapter)
  , (String
"w4-boolector" , AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
boolectorOnlineAdapter)

  , (String
"w4-abc"       , AnAdapter -> W4ProverConfig
W4ProverConfig ((forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter SolverAdapter st
forall (st :: * -> *). SolverAdapter st
W4.externalABCAdapter))

  , (String
"w4-offline"   , W4ProverConfig
W4OfflineConfig )
  , (String
"w4-any"       , W4ProverConfig
allSolvers)
  ]

z3OnlineAdapter :: AnAdapter
z3OnlineAdapter :: AnAdapter
z3OnlineAdapter =
  String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy (Writer Z3)
-> AnAdapter
forall s.
OnlineSolver s =>
String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy s
-> AnAdapter
AnOnlineAdapter String
"Z3" ProblemFeatures
W4.z3Features [ConfigDesc]
W4.z3Options (ConfigOption BaseIntegerType -> ConfigTimeout
configTimeoutMilliSeconds ConfigOption BaseIntegerType
W4.z3Timeout)
         (Proxy (Writer Z3)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (W4.Writer W4.Z3))

yicesOnlineAdapter :: AnAdapter
yicesOnlineAdapter :: AnAdapter
yicesOnlineAdapter =
  String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy Connection
-> AnAdapter
forall s.
OnlineSolver s =>
String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy s
-> AnAdapter
AnOnlineAdapter String
"Yices" ProblemFeatures
W4.yicesDefaultFeatures [ConfigDesc]
W4.yicesOptions (ConfigOption BaseIntegerType -> ConfigTimeout
configTimeoutSeconds ConfigOption BaseIntegerType
W4.yicesGoalTimeout)
         (Proxy Connection
forall {k} (t :: k). Proxy t
Proxy :: Proxy W4.Connection)

cvc4OnlineAdapter :: AnAdapter
cvc4OnlineAdapter :: AnAdapter
cvc4OnlineAdapter =
  String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy (Writer CVC4)
-> AnAdapter
forall s.
OnlineSolver s =>
String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy s
-> AnAdapter
AnOnlineAdapter String
"CVC4" ProblemFeatures
W4.cvc4Features [ConfigDesc]
W4.cvc4Options (ConfigOption BaseIntegerType -> ConfigTimeout
configTimeoutMilliSeconds ConfigOption BaseIntegerType
W4.cvc4Timeout)
         (Proxy (Writer CVC4)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (W4.Writer W4.CVC4))

cvc5OnlineAdapter :: AnAdapter
cvc5OnlineAdapter :: AnAdapter
cvc5OnlineAdapter =
  String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy (Writer CVC5)
-> AnAdapter
forall s.
OnlineSolver s =>
String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy s
-> AnAdapter
AnOnlineAdapter String
"CVC5" ProblemFeatures
W4.cvc5Features [ConfigDesc]
W4.cvc5Options (ConfigOption BaseIntegerType -> ConfigTimeout
configTimeoutMilliSeconds ConfigOption BaseIntegerType
W4.cvc5Timeout)
         (Proxy (Writer CVC5)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (W4.Writer W4.CVC5))

bitwuzlaOnlineAdapter :: AnAdapter
bitwuzlaOnlineAdapter :: AnAdapter
bitwuzlaOnlineAdapter =
  String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy (Writer Bitwuzla)
-> AnAdapter
forall s.
OnlineSolver s =>
String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy s
-> AnAdapter
AnOnlineAdapter String
"Bitwuzla" ProblemFeatures
W4.bitwuzlaFeatures [ConfigDesc]
W4.bitwuzlaOptions (ConfigOption BaseIntegerType -> ConfigTimeout
configTimeoutMilliSeconds ConfigOption BaseIntegerType
W4.bitwuzlaTimeout)
         (Proxy (Writer Bitwuzla)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (W4.Writer W4.Bitwuzla))

boolectorOnlineAdapter :: AnAdapter
boolectorOnlineAdapter :: AnAdapter
boolectorOnlineAdapter =
  String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy (Writer Boolector)
-> AnAdapter
forall s.
OnlineSolver s =>
String
-> ProblemFeatures
-> [ConfigDesc]
-> ConfigTimeout
-> Proxy s
-> AnAdapter
AnOnlineAdapter String
"Boolector" ProblemFeatures
W4.boolectorFeatures [ConfigDesc]
W4.boolectorOptions (ConfigOption BaseIntegerType -> ConfigTimeout
configTimeoutMilliSeconds ConfigOption BaseIntegerType
W4.boolectorTimeout)
         (Proxy (Writer Boolector)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (W4.Writer W4.Boolector))

allSolvers :: W4ProverConfig
allSolvers :: W4ProverConfig
allSolvers = NonEmpty AnAdapter -> W4ProverConfig
W4Portfolio
  (NonEmpty AnAdapter -> W4ProverConfig)
-> NonEmpty AnAdapter -> W4ProverConfig
forall a b. (a -> b) -> a -> b
$ AnAdapter
z3OnlineAdapter AnAdapter -> [AnAdapter] -> NonEmpty AnAdapter
forall a. a -> [a] -> NonEmpty a
:|
  [ AnAdapter
cvc4OnlineAdapter
  , AnAdapter
cvc5OnlineAdapter
  , AnAdapter
bitwuzlaOnlineAdapter
  , AnAdapter
boolectorOnlineAdapter
  , AnAdapter
yicesOnlineAdapter
  , (forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter SolverAdapter st
forall (st :: * -> *). SolverAdapter st
W4.externalABCAdapter
  ]

defaultProver :: W4ProverConfig
defaultProver :: W4ProverConfig
defaultProver = AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
z3OnlineAdapter

proverNames :: [String]
proverNames :: [String]
proverNames = ((String, W4ProverConfig) -> String)
-> [(String, W4ProverConfig)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, W4ProverConfig) -> String
forall a b. (a, b) -> a
fst [(String, W4ProverConfig)]
proverConfigs

setupProver :: String -> IO (Either String ([String], W4ProverConfig))
setupProver :: String -> IO (Either String ([String], W4ProverConfig))
setupProver String
nm =
  IO (Either String ([String], W4ProverConfig))
-> IO (Either String ([String], W4ProverConfig))
forall a. IO a -> IO a
rethrowW4Exception (IO (Either String ([String], W4ProverConfig))
 -> IO (Either String ([String], W4ProverConfig)))
-> IO (Either String ([String], W4ProverConfig))
-> IO (Either String ([String], W4ProverConfig))
forall a b. (a -> b) -> a -> b
$
  case String -> [(String, W4ProverConfig)] -> Maybe W4ProverConfig
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
nm [(String, W4ProverConfig)]
proverConfigs of
    Just cfg :: W4ProverConfig
cfg@(W4ProverConfig AnAdapter
p) ->
      do Maybe SomeException
st <- AnAdapter -> IO (Maybe SomeException)
tryAdapter AnAdapter
p
         let ws :: [String]
ws = case Maybe SomeException
st of
                    Maybe SomeException
Nothing -> []
                    Just SomeException
ex -> [ String
"Warning: solver interaction failed with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm, String
"    " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SomeException -> String
forall a. Show a => a -> String
show SomeException
ex ]
         Either String ([String], W4ProverConfig)
-> IO (Either String ([String], W4ProverConfig))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([String], W4ProverConfig)
-> Either String ([String], W4ProverConfig)
forall a b. b -> Either a b
Right ([String]
ws, W4ProverConfig
cfg))

    Just (W4Portfolio NonEmpty AnAdapter
ps) ->
      [AnAdapter] -> IO [AnAdapter]
filterAdapters (NonEmpty AnAdapter -> [AnAdapter]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty AnAdapter
ps) IO [AnAdapter]
-> ([AnAdapter] -> IO (Either String ([String], W4ProverConfig)))
-> IO (Either String ([String], W4ProverConfig))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
         [] -> Either String ([String], W4ProverConfig)
-> IO (Either String ([String], W4ProverConfig))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Either String ([String], W4ProverConfig)
forall a b. a -> Either a b
Left String
"What4 could not communicate with any provers!")
         (AnAdapter
p:[AnAdapter]
ps') ->
           let msg :: String
msg = String
"What4 found the following solvers: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show ([AnAdapter] -> [String]
adapterNames (AnAdapter
pAnAdapter -> [AnAdapter] -> [AnAdapter]
forall a. a -> [a] -> [a]
:[AnAdapter]
ps')) in
           Either String ([String], W4ProverConfig)
-> IO (Either String ([String], W4ProverConfig))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([String], W4ProverConfig)
-> Either String ([String], W4ProverConfig)
forall a b. b -> Either a b
Right ([String
msg], NonEmpty AnAdapter -> W4ProverConfig
W4Portfolio (AnAdapter
pAnAdapter -> [AnAdapter] -> NonEmpty AnAdapter
forall a. a -> [a] -> NonEmpty a
:|[AnAdapter]
ps')))

    Just W4ProverConfig
W4OfflineConfig -> Either String ([String], W4ProverConfig)
-> IO (Either String ([String], W4ProverConfig))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([String], W4ProverConfig)
-> Either String ([String], W4ProverConfig)
forall a b. b -> Either a b
Right ([], W4ProverConfig
W4OfflineConfig))

    Maybe W4ProverConfig
Nothing -> Either String ([String], W4ProverConfig)
-> IO (Either String ([String], W4ProverConfig))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Either String ([String], W4ProverConfig)
forall a b. a -> Either a b
Left (String
"unknown solver name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm))

  where
  adapterNames :: [AnAdapter] -> [String]
adapterNames [] = []
  adapterNames (AnAdapter forall (st :: * -> *). SolverAdapter st
adpt : [AnAdapter]
ps) =
    SolverAdapter Any -> String
forall (st :: * -> *). SolverAdapter st -> String
solver_adapter_name SolverAdapter Any
forall (st :: * -> *). SolverAdapter st
adpt String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [AnAdapter] -> [String]
adapterNames [AnAdapter]
ps
  adapterNames (AnOnlineAdapter String
n ProblemFeatures
_ [ConfigDesc]
_ ConfigTimeout
_ Proxy s
_ : [AnAdapter]
ps) =
    String
n String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [AnAdapter] -> [String]
adapterNames [AnAdapter]
ps

  filterAdapters :: [AnAdapter] -> IO [AnAdapter]
filterAdapters [] = [AnAdapter] -> IO [AnAdapter]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  filterAdapters (AnAdapter
p:[AnAdapter]
ps) =
    AnAdapter -> IO (Maybe SomeException)
tryAdapter AnAdapter
p IO (Maybe SomeException)
-> (Maybe SomeException -> IO [AnAdapter]) -> IO [AnAdapter]
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just SomeException
_err -> [AnAdapter] -> IO [AnAdapter]
filterAdapters [AnAdapter]
ps
      Maybe SomeException
Nothing   -> (AnAdapter
pAnAdapter -> [AnAdapter] -> [AnAdapter]
forall a. a -> [a] -> [a]
:) ([AnAdapter] -> [AnAdapter]) -> IO [AnAdapter] -> IO [AnAdapter]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnAdapter] -> IO [AnAdapter]
filterAdapters [AnAdapter]
ps

  tryAdapter :: AnAdapter -> IO (Maybe X.SomeException)

  tryAdapter :: AnAdapter -> IO (Maybe SomeException)
tryAdapter (AnAdapter forall (st :: * -> *). SolverAdapter st
adpt) =
     do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym <- FloatModeRepr 'FloatIEEE
-> CryptolState GlobalNonceGenerator
-> NonceGenerator IO GlobalNonceGenerator
-> IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
W4.newExprBuilder FloatModeRepr 'FloatIEEE
W4.FloatIEEERepr CryptolState GlobalNonceGenerator
forall t. CryptolState t
CryptolState NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
        [ConfigDesc] -> Config -> IO ()
W4.extendConfig (SolverAdapter Any -> [ConfigDesc]
forall (st :: * -> *). SolverAdapter st -> [ConfigDesc]
W4.solver_adapter_config_options SolverAdapter Any
forall (st :: * -> *). SolverAdapter st
adpt) (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> Config
forall sym. IsExprBuilder sym => sym -> Config
W4.getConfiguration ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym)
        ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> SolverAdapter CryptolState -> IO (Maybe SomeException)
forall t (st :: * -> *) fs.
ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException)
W4.smokeTest ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym SolverAdapter CryptolState
forall (st :: * -> *). SolverAdapter st
adpt

  tryAdapter (AnOnlineAdapter String
_ ProblemFeatures
fs [ConfigDesc]
opts ConfigTimeout
_ (Proxy s
_ :: Proxy s)) = IO (Maybe SomeException)
test IO (Maybe SomeException)
-> (SomeException -> IO (Maybe SomeException))
-> IO (Maybe SomeException)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` (Maybe SomeException -> IO (Maybe SomeException)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe SomeException -> IO (Maybe SomeException))
-> (SomeException -> Maybe SomeException)
-> SomeException
-> IO (Maybe SomeException)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just)
   where
    test :: IO (Maybe SomeException)
test =
      do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym <- FloatModeRepr 'FloatIEEE
-> CryptolState GlobalNonceGenerator
-> NonceGenerator IO GlobalNonceGenerator
-> IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
W4.newExprBuilder FloatModeRepr 'FloatIEEE
W4.FloatIEEERepr CryptolState GlobalNonceGenerator
forall t. CryptolState t
CryptolState NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
         [ConfigDesc] -> Config -> IO ()
W4.extendConfig [ConfigDesc]
opts (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> Config
forall sym. IsExprBuilder sym => sym -> Config
W4.getConfiguration ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym)

         (SolverProcess GlobalNonceGenerator s
proc :: W4.SolverProcess GlobalNonceGenerator s) <- ProblemFeatures
-> Maybe Handle
-> ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> IO (SolverProcess GlobalNonceGenerator s)
forall solver scope (st :: * -> *) fs.
OnlineSolver solver =>
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope solver)
forall scope (st :: * -> *) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope s)
W4.startSolverProcess ProblemFeatures
fs Maybe Handle
forall a. Maybe a
Nothing ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym
         SatResult () ()
res <- SolverProcess GlobalNonceGenerator s
-> String -> BoolExpr GlobalNonceGenerator -> IO (SatResult () ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> BoolExpr scope -> IO (SatResult () ())
W4.checkSatisfiable SolverProcess GlobalNonceGenerator s
proc String
"smoke test" (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> Pred
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.falsePred ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym)
         case SatResult () ()
res of
           W4.Unsat () -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           SatResult () ()
_ -> String -> IO ()
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"smoke test failed, expected UNSAT!"
         IO (ExitCode, Text) -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (SolverProcess GlobalNonceGenerator s -> IO (ExitCode, Text)
forall scope. SolverProcess scope s -> IO (ExitCode, Text)
forall solver scope.
OnlineSolver solver =>
SolverProcess scope solver -> IO (ExitCode, Text)
W4.shutdownSolverProcess SolverProcess GlobalNonceGenerator s
proc)
         Maybe SomeException -> IO (Maybe SomeException)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SomeException
forall a. Maybe a
Nothing

proverError :: String -> M.ModuleCmd (Maybe String, ProverResult)
proverError :: String -> ModuleCmd (Maybe String, ProverResult)
proverError String
msg ModuleInput IO
minp =
  ModuleRes (Maybe String, ProverResult)
-> IO (ModuleRes (Maybe String, ProverResult))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Maybe String, ProverResult), ModuleEnv)
-> Either ModuleError ((Maybe String, ProverResult), ModuleEnv)
forall a b. b -> Either a b
Right ((Maybe String
forall a. Maybe a
Nothing, String -> ProverResult
ProverError String
msg), ModuleInput IO -> ModuleEnv
forall (m :: * -> *). ModuleInput m -> ModuleEnv
M.minpModuleEnv ModuleInput IO
minp), [])


data CryptolState t = CryptolState


setupAdapterOptions :: W4ProverConfig -> W4.ExprBuilder t CryptolState fs -> IO ()
setupAdapterOptions :: forall t fs.
W4ProverConfig -> ExprBuilder t CryptolState fs -> IO ()
setupAdapterOptions W4ProverConfig
cfg ExprBuilder t CryptolState fs
sym =
   case W4ProverConfig
cfg of
     W4ProverConfig AnAdapter
p -> AnAdapter -> IO ()
setupAnAdapter AnAdapter
p
     W4Portfolio NonEmpty AnAdapter
ps -> (AnAdapter -> IO ()) -> NonEmpty AnAdapter -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ AnAdapter -> IO ()
setupAnAdapter NonEmpty AnAdapter
ps
     W4ProverConfig
W4OfflineConfig -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  where
  setupAnAdapter :: AnAdapter -> IO ()
setupAnAdapter (AnAdapter forall (st :: * -> *). SolverAdapter st
adpt) =
    [ConfigDesc] -> Config -> IO ()
W4.extendConfig (SolverAdapter Any -> [ConfigDesc]
forall (st :: * -> *). SolverAdapter st -> [ConfigDesc]
W4.solver_adapter_config_options SolverAdapter Any
forall (st :: * -> *). SolverAdapter st
adpt) (ExprBuilder t CryptolState fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
W4.getConfiguration ExprBuilder t CryptolState fs
sym)
  setupAnAdapter (AnOnlineAdapter String
_n ProblemFeatures
_fs [ConfigDesc]
opts ConfigTimeout
_ Proxy s
_p) =
    [ConfigDesc] -> Config -> IO ()
W4.extendConfig [ConfigDesc]
opts (ExprBuilder t CryptolState fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
W4.getConfiguration ExprBuilder t CryptolState fs
sym)

what4FreshFns :: W4.IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym)
what4FreshFns :: forall sym. IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym)
what4FreshFns sym
sym =
  FreshVarFns
  { freshBitVar :: IO (SBit (What4 sym))
freshBitVar     = sym
-> SolverSymbol
-> BaseTypeRepr 'BaseBoolType
-> IO (SymExpr sym 'BaseBoolType)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
W4.freshConstant sym
sym SolverSymbol
W4.emptySymbol BaseTypeRepr 'BaseBoolType
W4.BaseBoolRepr
  , freshWordVar :: Integer -> IO (SWord (What4 sym))
freshWordVar    = sym -> SolverSymbol -> Integer -> IO (SWord sym)
forall sym.
IsSymExprBuilder sym =>
sym -> SolverSymbol -> Integer -> IO (SWord sym)
SW.freshBV sym
sym SolverSymbol
W4.emptySymbol
  , freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger (What4 sym))
freshIntegerVar = sym
-> SolverSymbol
-> Maybe Integer
-> Maybe Integer
-> IO (SymInteger sym)
forall sym.
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Maybe Integer
-> Maybe Integer
-> IO (SymInteger sym)
W4.freshBoundedInt sym
sym SolverSymbol
W4.emptySymbol
  , freshFloatVar :: Integer -> Integer -> IO (SFloat (What4 sym))
freshFloatVar   = sym -> Integer -> Integer -> IO (SFloat sym)
forall sym.
IsSymExprBuilder sym =>
sym -> Integer -> Integer -> IO (SFloat sym)
W4.fpFresh sym
sym
  }

-- | Simulate and manipulate query into a form suitable to be sent
-- to a solver.
prepareQuery ::
  W4.IsSymExprBuilder sym =>
  What4 sym ->
  ProverCommand ->
  M.ModuleT IO (Either String
                       ([FinType],[VarShape (What4 sym)],W4.Pred sym, W4.Pred sym)
               )
prepareQuery :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> ProverCommand
-> ModuleT
     IO
     (Either
        String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
prepareQuery What4 sym
sym ProverCommand { Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcQueryType :: QueryType
pcProverName :: String
pcVerbose :: Bool
pcValidate :: Bool
pcProverStats :: IORef ProverStats
pcExtraDecls :: [DeclGroup]
pcSmtFile :: Maybe String
pcExpr :: Expr
pcSchema :: Schema
pcIgnoreSafety :: Bool
pcQueryType :: ProverCommand -> QueryType
pcProverName :: ProverCommand -> String
pcVerbose :: ProverCommand -> Bool
pcValidate :: ProverCommand -> Bool
pcProverStats :: ProverCommand -> IORef ProverStats
pcExtraDecls :: ProverCommand -> [DeclGroup]
pcSmtFile :: ProverCommand -> Maybe String
pcExpr :: ProverCommand -> Expr
pcSchema :: ProverCommand -> Schema
pcIgnoreSafety :: ProverCommand -> Bool
.. } = do
  Map Name NominalType
ntEnv <- ModuleM (Map Name NominalType)
M.getNominalTypes
  case QueryType -> Schema -> Either String [FinType]
predArgTypes QueryType
pcQueryType Schema
pcSchema of
    Left String
msg -> Either
  String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
-> ModuleT
     IO
     (Either
        String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
-> Either
     String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
forall a b. a -> Either a b
Left String
msg)
    Right [FinType]
ts ->
      do [VarShape (What4 sym)]
args <- IO [VarShape (What4 sym)] -> ModuleT IO [VarShape (What4 sym)]
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ((FinType -> IO (VarShape (What4 sym)))
-> [FinType] -> IO [VarShape (What4 sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FreshVarFns (What4 sym) -> FinType -> IO (VarShape (What4 sym))
forall sym.
Backend sym =>
FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar (sym -> FreshVarFns (What4 sym)
forall sym. IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym)
what4FreshFns (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym))) [FinType]
ts)
         (Pred sym
safety,Pred sym
b) <- Map Name NominalType
-> [VarShape (What4 sym)] -> ModuleT IO (Pred sym, Pred sym)
simulate Map Name NominalType
ntEnv [VarShape (What4 sym)]
args
         IO
  (Either
     String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
-> ModuleT
     IO
     (Either
        String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
           do -- Ignore the safety condition if the flag is set
              let safety' :: Pred sym
safety' = if Bool
pcIgnoreSafety then sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) else Pred sym
safety

              Pred sym
defs <- MVar (Pred sym) -> IO (Pred sym)
forall a. MVar a -> IO a
readMVar (What4 sym -> MVar (Pred sym)
forall sym. What4 sym -> MVar (Pred sym)
w4defs What4 sym
sym)

              ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
-> Either
     String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
forall a b. b -> Either a b
Right (([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
 -> Either
      String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
-> IO ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
-> IO
     (Either
        String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                case QueryType
pcQueryType of
                  QueryType
ProveQuery ->
                    do Pred sym
q <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
safety' Pred sym
b
                       Pred sym
q' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
defs Pred sym
q
                       ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
-> IO ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([FinType]
ts,[VarShape (What4 sym)]
args,Pred sym
safety',Pred sym
q')

                  QueryType
SafetyQuery ->
                    do Pred sym
q <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
safety
                       Pred sym
q' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
defs Pred sym
q
                       ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
-> IO ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([FinType]
ts,[VarShape (What4 sym)]
args,Pred sym
safety,Pred sym
q')

                  SatQuery SatNum
_ ->
                    do Pred sym
q <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
safety' Pred sym
b
                       Pred sym
q' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
defs Pred sym
q
                       ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
-> IO ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([FinType]
ts,[VarShape (What4 sym)]
args,Pred sym
safety',Pred sym
q')
  where
  simulate :: Map Name NominalType
-> [VarShape (What4 sym)] -> ModuleT IO (Pred sym, Pred sym)
simulate Map Name NominalType
ntEnv [VarShape (What4 sym)]
args =
    do let lPutStrLn :: String -> ModuleM ()
lPutStrLn = (Logger -> String -> IO ()) -> String -> ModuleM ()
forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
M.withLogger Logger -> String -> IO ()
logPutStrLn
       Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose (String -> ModuleM ()
lPutStrLn String
"Simulating...")

       Map PrimIdent Expr
ds <- do (ModulePath
_mp, TCTopEntity
ent) <- Bool -> ImportSource -> ModuleM (ModulePath, TCTopEntity)
M.loadModuleFrom Bool
True (ModName -> ImportSource
M.FromModule ModName
preludeReferenceName)
                let m :: Module
m = TCTopEntity -> Module
tcTopEntityToModule TCTopEntity
ent
                let decls :: [DeclGroup]
decls = Module -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls Module
m
                let nms :: [Name]
nms = (Name, IfaceDecl) -> Name
forall a b. (a, b) -> a
fst ((Name, IfaceDecl) -> Name) -> [(Name, IfaceDecl)] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name IfaceDecl -> [(Name, IfaceDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList (IfaceDecls -> Map Name IfaceDecl
M.ifDecls (IfaceG ModName -> IfaceDecls
forall name. IfaceG name -> IfaceDecls
M.ifDefines (Module -> IfaceG ModName
forall name. ModuleG name -> IfaceG name
M.genIface Module
m)))
                let ds :: Map PrimIdent Expr
ds = [(PrimIdent, Expr)] -> Map PrimIdent Expr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Text -> PrimIdent
prelPrim (Ident -> Text
identText (Name -> Ident
M.nameIdent Name
nm)), Expr -> [DeclGroup] -> Expr
EWhere (Name -> Expr
EVar Name
nm) [DeclGroup]
decls) | Name
nm <- [Name]
nms ]
                Map PrimIdent Expr -> ModuleT IO (Map PrimIdent Expr)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map PrimIdent Expr
ds

       IO EvalOpts
getEOpts <- ModuleM (IO EvalOpts)
M.getEvalOptsAction
       let tbl :: Map PrimIdent (Prim (What4 sym))
tbl = What4 sym -> IO EvalOpts -> Map PrimIdent (Prim (What4 sym))
forall sym.
IsSymExprBuilder sym =>
What4 sym -> IO EvalOpts -> Map PrimIdent (Prim (What4 sym))
primTable What4 sym
sym IO EvalOpts
getEOpts
       let ?evalPrim = \PrimIdent
i -> (Prim (What4 sym) -> Either Expr (Prim (What4 sym))
forall a b. b -> Either a b
Right (Prim (What4 sym) -> Either Expr (Prim (What4 sym)))
-> Maybe (Prim (What4 sym))
-> Maybe (Either Expr (Prim (What4 sym)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimIdent
-> Map PrimIdent (Prim (What4 sym)) -> Maybe (Prim (What4 sym))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent (Prim (What4 sym))
tbl) Maybe (Either Expr (Prim (What4 sym)))
-> Maybe (Either Expr (Prim (What4 sym)))
-> Maybe (Either Expr (Prim (What4 sym)))
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                             (Expr -> Either Expr (Prim (What4 sym))
forall a b. a -> Either a b
Left (Expr -> Either Expr (Prim (What4 sym)))
-> Maybe Expr -> Maybe (Either Expr (Prim (What4 sym)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimIdent -> Map PrimIdent Expr -> Maybe Expr
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent Expr
ds)
       let ?range = ?range::Range
Range
emptyRange
       Bool
callStacks <- ModuleT IO Bool
forall (m :: * -> *). Monad m => ModuleT m Bool
M.getCallStacks
       let ?callStacks = ?callStacks::Bool
Bool
callStacks

       ModuleEnv
modEnv <- ModuleT IO ModuleEnv
forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
M.getModuleEnv
       let extDgs :: [DeclGroup]
extDgs = ModuleEnv -> [DeclGroup]
M.allDeclGroups ModuleEnv
modEnv [DeclGroup] -> [DeclGroup] -> [DeclGroup]
forall a. [a] -> [a] -> [a]
++ [DeclGroup]
pcExtraDecls

       sym -> W4Eval sym (Pred sym) -> ModuleT IO (Pred sym, Pred sym)
forall sym (m :: * -> *) a.
(IsExprBuilder sym, MonadIO m) =>
sym -> W4Eval sym a -> m (Pred sym, a)
doW4Eval (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym)
         do GenEvalEnv (What4 sym)
env <- What4 sym
-> [DeclGroup]
-> GenEvalEnv (What4 sym)
-> SEval (What4 sym) (GenEvalEnv (What4 sym))
forall sym.
EvalPrims sym =>
sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
Eval.evalDecls What4 sym
sym [DeclGroup]
extDgs (GenEvalEnv (What4 sym) -> W4Eval sym (GenEvalEnv (What4 sym)))
-> W4Eval sym (GenEvalEnv (What4 sym))
-> W4Eval sym (GenEvalEnv (What4 sym))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                     What4 sym
-> Map Name NominalType
-> GenEvalEnv (What4 sym)
-> SEval (What4 sym) (GenEvalEnv (What4 sym))
forall sym.
EvalPrims sym =>
sym
-> Map Name NominalType
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
Eval.evalNominalDecls What4 sym
sym Map Name NominalType
ntEnv GenEvalEnv (What4 sym)
forall a. Monoid a => a
mempty

            GenValue (What4 sym)
v   <- What4 sym
-> GenEvalEnv (What4 sym)
-> Expr
-> SEval (What4 sym) (GenValue (What4 sym))
forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
Eval.evalExpr  What4 sym
sym GenEvalEnv (What4 sym)
env    Expr
pcExpr
            GenValue (What4 sym)
appliedVal <-
              (GenValue (What4 sym)
 -> W4Eval sym (GenValue (What4 sym))
 -> W4Eval sym (GenValue (What4 sym)))
-> GenValue (What4 sym)
-> [W4Eval sym (GenValue (What4 sym))]
-> W4Eval sym (GenValue (What4 sym))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (What4 sym
-> GenValue (What4 sym)
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
Eval.fromVFun What4 sym
sym) GenValue (What4 sym)
v ((VarShape (What4 sym) -> W4Eval sym (GenValue (What4 sym)))
-> [VarShape (What4 sym)] -> [W4Eval sym (GenValue (What4 sym))]
forall a b. (a -> b) -> [a] -> [b]
map (GenValue (What4 sym) -> W4Eval sym (GenValue (What4 sym))
forall a. a -> W4Eval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue (What4 sym) -> W4Eval sym (GenValue (What4 sym)))
-> (VarShape (What4 sym) -> GenValue (What4 sym))
-> VarShape (What4 sym)
-> W4Eval sym (GenValue (What4 sym))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. What4 sym -> VarShape (What4 sym) -> GenValue (What4 sym)
forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue What4 sym
sym) [VarShape (What4 sym)]
args)

            case QueryType
pcQueryType of
              QueryType
SafetyQuery ->
                do GenValue (What4 sym) -> SEval (What4 sym) ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
Eval.forceValue GenValue (What4 sym)
appliedVal
                   Pred sym -> W4Eval sym (Pred sym)
forall a. a -> W4Eval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym))

              QueryType
_ -> Pred sym -> W4Eval sym (Pred sym)
forall a. a -> W4Eval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue (What4 sym) -> SBit (What4 sym)
forall sym. Backend sym => GenValue sym -> SBit sym
Eval.fromVBit GenValue (What4 sym)
appliedVal)


satProve ::
  W4ProverConfig ->
  Bool {- ^ hash consing -} ->
  Bool {- ^ warn on uninterpreted functions -} ->
  Int {- ^ timeout milliseconds -} ->
  ProverCommand ->
  M.ModuleCmd (Maybe String, ProverResult)

satProve :: W4ProverConfig
-> Bool
-> Bool
-> Int
-> ProverCommand
-> ModuleCmd (Maybe String, ProverResult)
satProve W4ProverConfig
solverCfg Bool
hashConsing Bool
warnUninterp Int
timeoutMs pc :: ProverCommand
pc@ProverCommand {Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcQueryType :: ProverCommand -> QueryType
pcProverName :: ProverCommand -> String
pcVerbose :: ProverCommand -> Bool
pcValidate :: ProverCommand -> Bool
pcProverStats :: ProverCommand -> IORef ProverStats
pcExtraDecls :: ProverCommand -> [DeclGroup]
pcSmtFile :: ProverCommand -> Maybe String
pcExpr :: ProverCommand -> Expr
pcSchema :: ProverCommand -> Schema
pcIgnoreSafety :: ProverCommand -> Bool
pcQueryType :: QueryType
pcProverName :: String
pcVerbose :: Bool
pcValidate :: Bool
pcProverStats :: IORef ProverStats
pcExtraDecls :: [DeclGroup]
pcSmtFile :: Maybe String
pcExpr :: Expr
pcSchema :: Schema
pcIgnoreSafety :: Bool
..} =
  (String -> ModuleCmd (Maybe String, ProverResult))
-> ModuleCmd (Maybe String, ProverResult)
-> ModuleCmd (Maybe String, ProverResult)
forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack String -> ModuleCmd (Maybe String, ProverResult)
proverError \ModuleInput IO
modIn ->
  ModuleInput IO
-> ModuleM (Maybe String, ProverResult)
-> IO (ModuleRes (Maybe String, ProverResult))
forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM ModuleInput IO
modIn
  do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym   <- IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> ModuleT
     IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
makeSym
     MVar (BoolExpr GlobalNonceGenerator)
defVar  <- IO (MVar (BoolExpr GlobalNonceGenerator))
-> ModuleT IO (MVar (BoolExpr GlobalNonceGenerator))
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (BoolExpr GlobalNonceGenerator
-> IO (MVar (BoolExpr GlobalNonceGenerator))
forall a. a -> IO (MVar a)
newMVar (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> Pred
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym))
     MVar
  (What4FunCache
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
funVar  <- IO
  (MVar
     (What4FunCache
        (ExprBuilder
           GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
-> ModuleT
     IO
     (MVar
        (What4FunCache
           (ExprBuilder
              GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (What4FunCache
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> IO
     (MVar
        (What4FunCache
           (ExprBuilder
              GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
forall a. a -> IO (MVar a)
newMVar What4FunCache
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall a. Monoid a => a
mempty)
     MVar (Set Text)
uninterpWarnVar <- IO (MVar (Set Text)) -> ModuleT IO (MVar (Set Text))
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Set Text -> IO (MVar (Set Text))
forall a. a -> IO (MVar a)
newMVar Set Text
forall a. Monoid a => a
mempty)
     let sym :: What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym = ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> MVar
     (Pred
        (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
-> MVar
     (What4FunCache
        (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
-> MVar (Set Text)
-> What4
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall sym.
sym
-> MVar (Pred sym)
-> MVar (What4FunCache sym)
-> MVar (Set Text)
-> What4 sym
What4 ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym MVar
  (Pred
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
MVar (BoolExpr GlobalNonceGenerator)
defVar MVar
  (What4FunCache
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
funVar MVar (Set Text)
uninterpWarnVar
     LogData
logData <- (Logger -> () -> IO LogData) -> () -> ModuleM LogData
forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
M.withLogger Logger -> () -> IO LogData
forall {f :: * -> *}. Applicative f => Logger -> () -> f LogData
doLog ()
     UTCTime
start   <- IO UTCTime -> ModuleT IO UTCTime
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO UTCTime
getCurrentTime
     Either
  String
  ([FinType],
   [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
   BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
query   <- What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> ProverCommand
-> ModuleT
     IO
     (Either
        String
        ([FinType],
         [VarShape
            (What4
               (ExprBuilder
                  GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
         Pred
           (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)),
         Pred
           (ExprBuilder
              GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
forall sym.
IsSymExprBuilder sym =>
What4 sym
-> ProverCommand
-> ModuleT
     IO
     (Either
        String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
prepareQuery What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym ProverCommand { Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcQueryType :: QueryType
pcProverName :: String
pcVerbose :: Bool
pcValidate :: Bool
pcProverStats :: IORef ProverStats
pcExtraDecls :: [DeclGroup]
pcSmtFile :: Maybe String
pcExpr :: Expr
pcSchema :: Schema
pcIgnoreSafety :: Bool
pcQueryType :: QueryType
pcProverName :: String
pcVerbose :: Bool
pcValidate :: Bool
pcProverStats :: IORef ProverStats
pcExtraDecls :: [DeclGroup]
pcSmtFile :: Maybe String
pcExpr :: Expr
pcSchema :: Schema
pcIgnoreSafety :: Bool
.. }
     PrimMap
primMap <- ModuleM PrimMap
M.getPrimMap
     Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
warnUninterp
       ((Logger -> Set Text -> IO ()) -> Set Text -> ModuleM ()
forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
M.withLogger Logger -> Set Text -> IO ()
printUninterpWarn (Set Text -> ModuleM ()) -> ModuleT IO (Set Text) -> ModuleM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (Set Text) -> ModuleT IO (Set Text)
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (MVar (Set Text) -> IO (Set Text)
forall a. MVar a -> IO a
readMVar MVar (Set Text)
uninterpWarnVar))
     IO (Maybe String, ProverResult)
-> ModuleM (Maybe String, ProverResult)
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
       do (Maybe String, ProverResult)
result <- What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> LogData
-> PrimMap
-> Either
     String
     ([FinType],
      [VarShape
         (What4
            (ExprBuilder
               GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
      BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
-> IO (Maybe String, ProverResult)
runProver What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym LogData
logData PrimMap
primMap Either
  String
  ([FinType],
   [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
   BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
query
          UTCTime
end <- IO UTCTime
getCurrentTime
          IORef ProverStats -> ProverStats -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef ProverStats
pcProverStats (UTCTime -> UTCTime -> ProverStats
diffUTCTime UTCTime
end UTCTime
start)
          (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String, ProverResult)
result
  where
  makeSym :: IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
makeSym =
    do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym <- FloatModeRepr 'FloatIEEE
-> CryptolState GlobalNonceGenerator
-> NonceGenerator IO GlobalNonceGenerator
-> IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
W4.newExprBuilder FloatModeRepr 'FloatIEEE
W4.FloatIEEERepr
                                  CryptolState GlobalNonceGenerator
forall t. CryptolState t
CryptolState
                                  NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
       W4ProverConfig
-> ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> IO ()
forall t fs.
W4ProverConfig -> ExprBuilder t CryptolState fs -> IO ()
setupAdapterOptions W4ProverConfig
solverCfg ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym
       Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
hashConsing (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> IO ()
forall t (st :: * -> *) fs. ExprBuilder t st fs -> IO ()
W4.startCaching ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym)
       Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
timeoutMs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (W4ProverConfig
-> Integer
-> ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> IO ()
forall sym.
IsExprBuilder sym =>
W4ProverConfig -> Integer -> sym -> IO ()
setTimeout W4ProverConfig
solverCfg (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
timeoutMs) ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym)
       ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym

  doLog :: Logger -> () -> f LogData
doLog Logger
lg () =
    LogData -> f LogData
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    LogData
defaultLogData
      { logCallbackVerbose = \Int
i String
msg -> Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2) (Logger -> String -> IO ()
logPutStrLn Logger
lg String
msg)
      , logReason = "solver query"
      }

  runProver :: What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> LogData
-> PrimMap
-> Either
     String
     ([FinType],
      [VarShape
         (What4
            (ExprBuilder
               GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
      BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
-> IO (Maybe String, ProverResult)
runProver What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym LogData
logData PrimMap
primMap Either
  String
  ([FinType],
   [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
   BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
q =
    case Either
  String
  ([FinType],
   [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
   BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
q of
      Left String
msg -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe String
forall a. Maybe a
Nothing, String -> ProverResult
ProverError String
msg)
      Right ([FinType]
ts,[VarShape
   (What4
      (ExprBuilder
         GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
args,BoolExpr GlobalNonceGenerator
safety,BoolExpr GlobalNonceGenerator
query) ->
        case QueryType
pcQueryType of
          QueryType
ProveQuery ->
            What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
-> Maybe
     (Pred
        (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
-> Pred
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> IO (Maybe String, ProverResult)
forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
singleQuery What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym W4ProverConfig
solverCfg ProverCommand
pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape
   (What4
      (ExprBuilder
         GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
args (BoolExpr GlobalNonceGenerator
-> Maybe (BoolExpr GlobalNonceGenerator)
forall a. a -> Maybe a
Just BoolExpr GlobalNonceGenerator
safety) Pred
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
BoolExpr GlobalNonceGenerator
query

          QueryType
SafetyQuery ->
            What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
-> Maybe
     (Pred
        (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
-> Pred
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> IO (Maybe String, ProverResult)
forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
singleQuery What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym W4ProverConfig
solverCfg ProverCommand
pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape
   (What4
      (ExprBuilder
         GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
args (BoolExpr GlobalNonceGenerator
-> Maybe (BoolExpr GlobalNonceGenerator)
forall a. a -> Maybe a
Just BoolExpr GlobalNonceGenerator
safety) Pred
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
BoolExpr GlobalNonceGenerator
query

          SatQuery SatNum
num ->
            What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
-> Pred
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> SatNum
-> IO (Maybe String, ProverResult)
forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Pred sym
-> SatNum
-> IO (Maybe String, ProverResult)
multiSATQuery What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym W4ProverConfig
solverCfg ProverCommand
pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape
   (What4
      (ExprBuilder
         GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
args Pred
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
BoolExpr GlobalNonceGenerator
query SatNum
num

printUninterpWarn :: Logger -> Set Text -> IO ()
printUninterpWarn :: Logger -> Set Text -> IO ()
printUninterpWarn Logger
lg Set Text
uninterpWarns =
  case Set Text -> [Text]
forall a. Set a -> [a]
Set.toList Set Text
uninterpWarns of
    []  -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    [Text
x] -> Logger -> String -> IO ()
logPutStrLn Logger
lg (String
"[Warning] Uninterpreted functions used to represent " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" operations.")
    [Text]
xs  -> Logger -> String -> IO ()
logPutStr Logger
lg (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
             [ String
"[Warning] Uninterpreted functions used to represent the following operations:"
             , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
Text.unpack [Text]
xs) ]

satProveOffline ::
  Bool {- ^ hash consing -} ->
  Bool {- ^ warn on uninterpreted functions -} ->
  ProverCommand ->
  ((Handle -> IO ()) -> IO ()) ->
  M.ModuleCmd (Maybe String)

satProveOffline :: Bool
-> Bool
-> ProverCommand
-> ((Handle -> IO ()) -> IO ())
-> ModuleCmd (Maybe String)
satProveOffline Bool
hashConsing Bool
warnUninterp ProverCommand{ Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcQueryType :: ProverCommand -> QueryType
pcProverName :: ProverCommand -> String
pcVerbose :: ProverCommand -> Bool
pcValidate :: ProverCommand -> Bool
pcProverStats :: ProverCommand -> IORef ProverStats
pcExtraDecls :: ProverCommand -> [DeclGroup]
pcSmtFile :: ProverCommand -> Maybe String
pcExpr :: ProverCommand -> Expr
pcSchema :: ProverCommand -> Schema
pcIgnoreSafety :: ProverCommand -> Bool
pcQueryType :: QueryType
pcProverName :: String
pcVerbose :: Bool
pcValidate :: Bool
pcProverStats :: IORef ProverStats
pcExtraDecls :: [DeclGroup]
pcSmtFile :: Maybe String
pcExpr :: Expr
pcSchema :: Schema
pcIgnoreSafety :: Bool
.. } (Handle -> IO ()) -> IO ()
outputContinuation =

  (String -> ModuleCmd (Maybe String))
-> ModuleCmd (Maybe String) -> ModuleCmd (Maybe String)
forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack String -> ModuleCmd (Maybe String)
forall {f :: * -> *} {a} {m :: * -> *} {a} {a}.
Applicative f =>
a -> ModuleInput m -> f (Either a (Maybe a, ModuleEnv), [a])
onError \ModuleInput IO
modIn ->
  ModuleInput IO
-> ModuleM (Maybe String)
-> IO
     (Either ModuleError (Maybe String, ModuleEnv), [ModuleWarning])
forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM ModuleInput IO
modIn
   do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym <- IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> ModuleT
     IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
makeSym
      MVar (BoolExpr GlobalNonceGenerator)
defVar  <- IO (MVar (BoolExpr GlobalNonceGenerator))
-> ModuleT IO (MVar (BoolExpr GlobalNonceGenerator))
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (BoolExpr GlobalNonceGenerator
-> IO (MVar (BoolExpr GlobalNonceGenerator))
forall a. a -> IO (MVar a)
newMVar (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> Pred
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym))
      MVar
  (What4FunCache
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
funVar  <- IO
  (MVar
     (What4FunCache
        (ExprBuilder
           GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
-> ModuleT
     IO
     (MVar
        (What4FunCache
           (ExprBuilder
              GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (What4FunCache
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> IO
     (MVar
        (What4FunCache
           (ExprBuilder
              GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
forall a. a -> IO (MVar a)
newMVar What4FunCache
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall a. Monoid a => a
mempty)
      MVar (Set Text)
uninterpWarnVar <- IO (MVar (Set Text)) -> ModuleT IO (MVar (Set Text))
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Set Text -> IO (MVar (Set Text))
forall a. a -> IO (MVar a)
newMVar Set Text
forall a. Monoid a => a
mempty)
      let sym :: What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym = ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> MVar
     (Pred
        (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
-> MVar
     (What4FunCache
        (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
-> MVar (Set Text)
-> What4
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall sym.
sym
-> MVar (Pred sym)
-> MVar (What4FunCache sym)
-> MVar (Set Text)
-> What4 sym
What4 ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym MVar
  (Pred
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
MVar (BoolExpr GlobalNonceGenerator)
defVar MVar
  (What4FunCache
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
funVar MVar (Set Text)
uninterpWarnVar
      Either
  String
  ([FinType],
   [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
   BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
ok  <- What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> ProverCommand
-> ModuleT
     IO
     (Either
        String
        ([FinType],
         [VarShape
            (What4
               (ExprBuilder
                  GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
         Pred
           (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)),
         Pred
           (ExprBuilder
              GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))))
forall sym.
IsSymExprBuilder sym =>
What4 sym
-> ProverCommand
-> ModuleT
     IO
     (Either
        String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
prepareQuery What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym ProverCommand { Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcQueryType :: QueryType
pcProverName :: String
pcVerbose :: Bool
pcValidate :: Bool
pcProverStats :: IORef ProverStats
pcExtraDecls :: [DeclGroup]
pcSmtFile :: Maybe String
pcExpr :: Expr
pcSchema :: Schema
pcIgnoreSafety :: Bool
pcQueryType :: QueryType
pcProverName :: String
pcVerbose :: Bool
pcValidate :: Bool
pcProverStats :: IORef ProverStats
pcExtraDecls :: [DeclGroup]
pcSmtFile :: Maybe String
pcExpr :: Expr
pcSchema :: Schema
pcIgnoreSafety :: Bool
.. }
      Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
warnUninterp
        ((Logger -> Set Text -> IO ()) -> Set Text -> ModuleM ()
forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
M.withLogger Logger -> Set Text -> IO ()
printUninterpWarn (Set Text -> ModuleM ()) -> ModuleT IO (Set Text) -> ModuleM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (Set Text) -> ModuleT IO (Set Text)
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (MVar (Set Text) -> IO (Set Text)
forall a. MVar a -> IO a
readMVar MVar (Set Text)
uninterpWarnVar))
      IO (Maybe String) -> ModuleM (Maybe String)
forall a. IO a -> ModuleT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
        case Either
  String
  ([FinType],
   [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
   BoolExpr GlobalNonceGenerator, BoolExpr GlobalNonceGenerator)
ok of
          Left String
msg -> Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
msg)
          Right ([FinType]
_ts,[VarShape
   (What4
      (ExprBuilder
         GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
_args,BoolExpr GlobalNonceGenerator
_safety,BoolExpr GlobalNonceGenerator
query) ->
            do (Handle -> IO ()) -> IO ()
outputContinuation (\Handle
hdl -> ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> Handle -> [BoolExpr GlobalNonceGenerator] -> IO ()
forall t (st :: * -> *) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
W4.writeZ3SMT2File ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym Handle
hdl [BoolExpr GlobalNonceGenerator
query])
               Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
  where
  makeSym :: IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
makeSym =
    do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym <- FloatModeRepr 'FloatIEEE
-> CryptolState GlobalNonceGenerator
-> NonceGenerator IO GlobalNonceGenerator
-> IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
W4.newExprBuilder FloatModeRepr 'FloatIEEE
W4.FloatIEEERepr CryptolState GlobalNonceGenerator
forall t. CryptolState t
CryptolState NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
       [ConfigDesc] -> Config -> IO ()
W4.extendConfig [ConfigDesc]
W4.z3Options (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> Config
forall sym. IsExprBuilder sym => sym -> Config
W4.getConfiguration ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym)
       Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
hashConsing (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> IO ()
forall t (st :: * -> *) fs. ExprBuilder t st fs -> IO ()
W4.startCaching ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym)
       ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym

  onError :: a -> ModuleInput m -> f (Either a (Maybe a, ModuleEnv), [a])
onError a
msg ModuleInput m
minp = (Either a (Maybe a, ModuleEnv), [a])
-> f (Either a (Maybe a, ModuleEnv), [a])
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Maybe a, ModuleEnv) -> Either a (Maybe a, ModuleEnv)
forall a b. b -> Either a b
Right (a -> Maybe a
forall a. a -> Maybe a
Just a
msg, ModuleInput m -> ModuleEnv
forall (m :: * -> *). ModuleInput m -> ModuleEnv
M.minpModuleEnv ModuleInput m
minp), [])


{-
decSatNum :: SatNum -> SatNum
decSatNum (SomeSat n) | n > 0 = SomeSat (n-1)
decSatNum n = n
-}


multiSATQuery :: forall sym t fm.
  sym ~ W4.ExprBuilder t CryptolState fm =>
  What4 sym ->
  W4ProverConfig ->
  ProverCommand ->
  PrimMap ->
  W4.LogData ->
  [FinType] ->
  [VarShape (What4 sym)] ->
  W4.Pred sym ->
  SatNum ->
  IO (Maybe String, ProverResult)

multiSATQuery :: forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Pred sym
-> SatNum
-> IO (Maybe String, ProverResult)
multiSATQuery What4 sym
sym W4ProverConfig
solverCfg ProverCommand
pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape (What4 sym)]
args Pred sym
query (SomeSat Int
n) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 =
  What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
singleQuery What4 sym
sym W4ProverConfig
solverCfg ProverCommand
pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape (What4 sym)]
args Maybe (Pred sym)
Maybe (Expr t 'BaseBoolType)
forall a. Maybe a
Nothing Pred sym
query

multiSATQuery What4 sym
_sym W4ProverConfig
W4OfflineConfig ProverCommand
_pc PrimMap
_primMap LogData
_logData [FinType]
_ts [VarShape (What4 sym)]
_args Pred sym
_query SatNum
_satNum =
  String -> IO (Maybe String, ProverResult)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"What4 offline solver cannot be used for multi-SAT queries"

multiSATQuery What4 sym
_sym (W4Portfolio NonEmpty AnAdapter
_) ProverCommand
_pc PrimMap
_primMap LogData
_logData [FinType]
_ts [VarShape (What4 sym)]
_args Pred sym
_query SatNum
_satNum =
  String -> IO (Maybe String, ProverResult)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"What4 portfolio solver cannot be used for multi-SAT queries"

multiSATQuery What4 sym
_sym (W4ProverConfig (AnAdapter forall (st :: * -> *). SolverAdapter st
adpt)) ProverCommand
_pc PrimMap
_primMap LogData
_logData [FinType]
_ts [VarShape (What4 sym)]
_args Pred sym
_query SatNum
_satNum =
  String -> IO (Maybe String, ProverResult)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Solver " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SolverAdapter Any -> String
forall (st :: * -> *). SolverAdapter st -> String
solver_adapter_name SolverAdapter Any
forall (st :: * -> *). SolverAdapter st
adpt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" does not support incremental solving and " String -> ShowS
forall a. [a] -> [a] -> [a]
++
        String
"cannot be used for multi-SAT queries.")

multiSATQuery What4 sym
sym (W4ProverConfig (AnOnlineAdapter String
nm ProblemFeatures
fs [ConfigDesc]
_opts ConfigTimeout
_ (Proxy s
_ :: Proxy s)))
               ProverCommand{Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcQueryType :: ProverCommand -> QueryType
pcProverName :: ProverCommand -> String
pcVerbose :: ProverCommand -> Bool
pcValidate :: ProverCommand -> Bool
pcProverStats :: ProverCommand -> IORef ProverStats
pcExtraDecls :: ProverCommand -> [DeclGroup]
pcSmtFile :: ProverCommand -> Maybe String
pcExpr :: ProverCommand -> Expr
pcSchema :: ProverCommand -> Schema
pcIgnoreSafety :: ProverCommand -> Bool
pcQueryType :: QueryType
pcProverName :: String
pcVerbose :: Bool
pcValidate :: Bool
pcProverStats :: IORef ProverStats
pcExtraDecls :: [DeclGroup]
pcSmtFile :: Maybe String
pcExpr :: Expr
pcSchema :: Schema
pcIgnoreSafety :: Bool
..} PrimMap
primMap LogData
_logData [FinType]
ts [VarShape (What4 sym)]
args Pred sym
query SatNum
satNum0 =
    Maybe String
-> IOMode
-> (Maybe Handle -> IO (Maybe String, ProverResult))
-> IO (Maybe String, ProverResult)
forall r. Maybe String -> IOMode -> (Maybe Handle -> IO r) -> IO r
withMaybeFile Maybe String
pcSmtFile IOMode
WriteMode ((Maybe Handle -> IO (Maybe String, ProverResult))
 -> IO (Maybe String, ProverResult))
-> (Maybe Handle -> IO (Maybe String, ProverResult))
-> IO (Maybe String, ProverResult)
forall a b. (a -> b) -> a -> b
$ \Maybe Handle
smtFileHdl ->
    IO (SolverProcess t s)
-> (SolverProcess t s -> IO ())
-> (SolverProcess t s -> IO (Maybe String, ProverResult))
-> IO (Maybe String, ProverResult)
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
X.bracket
      (ProblemFeatures
-> Maybe Handle
-> ExprBuilder t CryptolState fm
-> IO (SolverProcess t s)
forall solver scope (st :: * -> *) fs.
OnlineSolver solver =>
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope solver)
forall scope (st :: * -> *) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope s)
W4.startSolverProcess ProblemFeatures
fs Maybe Handle
smtFileHdl (What4 (ExprBuilder t CryptolState fm)
-> ExprBuilder t CryptolState fm
forall sym. What4 sym -> sym
w4 What4 sym
What4 (ExprBuilder t CryptolState fm)
sym))
      (IO (ExitCode, Text) -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO (ExitCode, Text) -> IO ())
-> (SolverProcess t s -> IO (ExitCode, Text))
-> SolverProcess t s
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverProcess t s -> IO (ExitCode, Text)
forall scope. SolverProcess scope s -> IO (ExitCode, Text)
forall solver scope.
OnlineSolver solver =>
SolverProcess scope solver -> IO (ExitCode, Text)
W4.shutdownSolverProcess)
      (\ (SolverProcess t s
proc :: W4.SolverProcess t s) ->
        do WriterConn t s -> Expr t 'BaseBoolType -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
W4.assume (SolverProcess t s -> WriterConn t s
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
W4.solverConn SolverProcess t s
proc) Pred sym
Expr t 'BaseBoolType
query
           SatResult (GroundEvalFn t) ()
res <- SolverProcess t s -> String -> IO (SatResult (GroundEvalFn t) ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
W4.checkAndGetModel SolverProcess t s
proc String
"query"
           case SatResult (GroundEvalFn t) ()
res of
             SatResult (GroundEvalFn t) ()
W4.Unknown -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
nm, String -> ProverResult
ProverError String
"Solver returned UNKNOWN")
             W4.Unsat ()
_ -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
nm, [TValue] -> ProverResult
ThmResult ((FinType -> TValue) -> [FinType] -> [TValue]
forall a b. (a -> b) -> [a] -> [b]
map FinType -> TValue
unFinType [FinType]
ts))
             W4.Sat GroundEvalFn t
evalFn ->
               do [VarShape Concrete]
xs <- (VarShape (What4 (ExprBuilder t CryptolState fm))
 -> IO (VarShape Concrete))
-> [VarShape (What4 (ExprBuilder t CryptolState fm))]
-> IO [VarShape Concrete]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
forall t fm.
GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
varShapeToConcrete GroundEvalFn t
evalFn) [VarShape (What4 sym)]
[VarShape (What4 (ExprBuilder t CryptolState fm))]
args
                  let mdl :: [(TValue, Expr, Value)]
mdl = PrimMap
-> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
computeModel PrimMap
primMap [FinType]
ts [VarShape Concrete]
xs
                  -- NB, we flatten these shapes to make sure that we can split
                  -- our search across all of the atomic variables
                  let vs :: [VarShape (What4 sym)]
vs = [VarShape (What4 sym)]
-> [VarShape (What4 sym)] -> [VarShape (What4 sym)]
forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
flattenShapes [VarShape (What4 sym)]
args []
                  let cs :: [VarShape Concrete]
cs = [VarShape Concrete] -> [VarShape Concrete] -> [VarShape Concrete]
forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
flattenShapes [VarShape Concrete]
xs []
                  Models
mdls <- SatNum -> MultiSat () -> IO Models
forall a. SatNum -> MultiSat a -> IO Models
runMultiSat SatNum
satNum0 (MultiSat () -> IO Models) -> MultiSat () -> IO Models
forall a b. (a -> b) -> a -> b
$
                            do [(TValue, Expr, Value)] -> MultiSat ()
yield [(TValue, Expr, Value)]
mdl
                               SolverProcess t s
-> [VarShape (What4 sym)] -> [VarShape Concrete] -> MultiSat ()
computeMoreModels SolverProcess t s
proc [VarShape (What4 sym)]
vs [VarShape Concrete]
cs
                  (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
nm, Models -> ProverResult
AllSatResult Models
mdls))

  where
  -- This search procedure uses incremental solving and push/pop to split on the concrete
  -- values of variables, while also helping to prevent the accumulation of unhelpful
  -- lemmas in the solver state.  This algorithm is basically taken from:
  --   http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations
  computeMoreModels ::
    W4.SolverProcess t s ->
    [VarShape (What4 sym)] ->
    [VarShape Concrete.Concrete] ->
    MultiSat ()
  computeMoreModels :: SolverProcess t s
-> [VarShape (What4 sym)] -> [VarShape Concrete] -> MultiSat ()
computeMoreModels SolverProcess t s
proc [VarShape (What4 sym)]
vs [VarShape Concrete]
cs =
    -- Enumerate all the ways to split up the current model
    [([(VarShape (What4 sym), VarShape Concrete)],
  VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
-> (([(VarShape (What4 sym), VarShape Concrete)],
     VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])
    -> MultiSat ())
-> MultiSat ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([VarShape (What4 sym)]
-> [VarShape Concrete]
-> [([(VarShape (What4 sym), VarShape Concrete)],
     VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
forall sym.
[VarShape (What4 sym)]
-> [VarShape Concrete]
-> [([(VarShape (What4 sym), VarShape Concrete)],
     VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
computeSplits [VarShape (What4 sym)]
vs [VarShape Concrete]
cs) ((([(VarShape (What4 sym), VarShape Concrete)],
   VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])
  -> MultiSat ())
 -> MultiSat ())
-> (([(VarShape (What4 sym), VarShape Concrete)],
     VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])
    -> MultiSat ())
-> MultiSat ()
forall a b. (a -> b) -> a -> b
$ \ ([(VarShape (What4 sym), VarShape Concrete)]
prefix, VarShape (What4 sym)
vi, VarShape Concrete
ci, [VarShape (What4 sym)]
suffix) ->
      do -- open a new solver frame
         IO () -> MultiSat ()
forall a. IO a -> MultiSat a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> MultiSat ()) -> IO () -> MultiSat ()
forall a b. (a -> b) -> a -> b
$ SolverProcess t s -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
W4.push SolverProcess t s
proc
         -- force the selected pair to be different
         IO () -> MultiSat ()
forall a. IO a -> MultiSat a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> MultiSat ()) -> IO () -> MultiSat ()
forall a b. (a -> b) -> a -> b
$ WriterConn t s -> Expr t 'BaseBoolType -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
W4.assume (SolverProcess t s -> WriterConn t s
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
W4.solverConn SolverProcess t s
proc) (Expr t 'BaseBoolType -> IO ())
-> IO (Expr t 'BaseBoolType) -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) (Expr t 'BaseBoolType -> IO (Expr t 'BaseBoolType))
-> IO (Expr t 'BaseBoolType) -> IO (Expr t 'BaseBoolType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< What4 sym
-> VarShape (What4 sym) -> VarShape Concrete -> IO (Pred sym)
forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> VarShape (What4 sym) -> VarShape Concrete -> IO (Pred sym)
computeModelPred What4 sym
sym VarShape (What4 sym)
vi VarShape Concrete
ci
         -- force the prefix values to be the same
         IO () -> MultiSat ()
forall a. IO a -> MultiSat a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> MultiSat ()) -> IO () -> MultiSat ()
forall a b. (a -> b) -> a -> b
$ [(VarShape (What4 sym), VarShape Concrete)]
-> ((VarShape (What4 sym), VarShape Concrete) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(VarShape (What4 sym), VarShape Concrete)]
prefix (((VarShape (What4 sym), VarShape Concrete) -> IO ()) -> IO ())
-> ((VarShape (What4 sym), VarShape Concrete) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(VarShape (What4 sym)
v,VarShape Concrete
c) ->
           WriterConn t s -> Expr t 'BaseBoolType -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
W4.assume (SolverProcess t s -> WriterConn t s
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
W4.solverConn SolverProcess t s
proc) (Expr t 'BaseBoolType -> IO ())
-> IO (Expr t 'BaseBoolType) -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< What4 sym
-> VarShape (What4 sym) -> VarShape Concrete -> IO (Pred sym)
forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> VarShape (What4 sym) -> VarShape Concrete -> IO (Pred sym)
computeModelPred What4 sym
sym VarShape (What4 sym)
v VarShape Concrete
c
         -- under these assumptions, find all the remaining models
         SolverProcess t s -> [VarShape (What4 sym)] -> MultiSat ()
findMoreModels SolverProcess t s
proc (VarShape (What4 sym)
viVarShape (What4 sym)
-> [VarShape (What4 sym)] -> [VarShape (What4 sym)]
forall a. a -> [a] -> [a]
:[VarShape (What4 sym)]
suffix)
         -- pop the current assumption frame
         IO () -> MultiSat ()
forall a. IO a -> MultiSat a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> MultiSat ()) -> IO () -> MultiSat ()
forall a b. (a -> b) -> a -> b
$ SolverProcess t s -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
W4.pop SolverProcess t s
proc

  findMoreModels ::
    W4.SolverProcess t s ->
    [VarShape (What4 sym)] ->
    MultiSat ()
  findMoreModels :: SolverProcess t s -> [VarShape (What4 sym)] -> MultiSat ()
findMoreModels SolverProcess t s
proc [VarShape (What4 sym)]
vs =
    -- see if our current assumptions are consistent
    do SatResult (GroundEvalFn t) ()
res <- IO (SatResult (GroundEvalFn t) ())
-> MultiSat (SatResult (GroundEvalFn t) ())
forall a. IO a -> MultiSat a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (SolverProcess t s -> String -> IO (SatResult (GroundEvalFn t) ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
W4.checkAndGetModel SolverProcess t s
proc String
"find model")
       case SatResult (GroundEvalFn t) ()
res of
         -- if the solver gets stuck, drop all the way out and stop search
         SatResult (GroundEvalFn t) ()
W4.Unknown -> MultiSat ()
forall a. MultiSat a
done
         -- if our assumptions are already unsatisfiable, stop search and return
         W4.Unsat ()
_ -> () -> MultiSat ()
forall a. a -> MultiSat a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         W4.Sat GroundEvalFn t
evalFn ->
           -- We found a model.  Record it and then use it to split the remaining
           -- search variables some more.
           do [VarShape Concrete]
xs <- IO [VarShape Concrete] -> MultiSat [VarShape Concrete]
forall a. IO a -> MultiSat a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ((VarShape (What4 (ExprBuilder t CryptolState fm))
 -> IO (VarShape Concrete))
-> [VarShape (What4 (ExprBuilder t CryptolState fm))]
-> IO [VarShape Concrete]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
forall t fm.
GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
varShapeToConcrete GroundEvalFn t
evalFn) [VarShape (What4 sym)]
[VarShape (What4 (ExprBuilder t CryptolState fm))]
args)
              [(TValue, Expr, Value)] -> MultiSat ()
yield (PrimMap
-> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
computeModel PrimMap
primMap [FinType]
ts [VarShape Concrete]
xs)
              [VarShape Concrete]
cs <- IO [VarShape Concrete] -> MultiSat [VarShape Concrete]
forall a. IO a -> MultiSat a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ((VarShape (What4 (ExprBuilder t CryptolState fm))
 -> IO (VarShape Concrete))
-> [VarShape (What4 (ExprBuilder t CryptolState fm))]
-> IO [VarShape Concrete]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
forall t fm.
GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
varShapeToConcrete GroundEvalFn t
evalFn) [VarShape (What4 sym)]
[VarShape (What4 (ExprBuilder t CryptolState fm))]
vs)
              SolverProcess t s
-> [VarShape (What4 sym)] -> [VarShape Concrete] -> MultiSat ()
computeMoreModels SolverProcess t s
proc [VarShape (What4 sym)]
vs [VarShape Concrete]
cs

-- == Support operations for multi-SAT ==
type Models = [[(TValue, Expr, Concrete.Value)]]

newtype MultiSat a =
  MultiSat { forall a.
MultiSat a
-> Models
-> SatNum
-> (a -> Models -> SatNum -> IO Models)
-> IO Models
unMultiSat ::  Models -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models }

instance Functor MultiSat where
  fmap :: forall a b. (a -> b) -> MultiSat a -> MultiSat b
fmap a -> b
f MultiSat a
m = (Models
 -> SatNum -> (b -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat b
forall a.
(Models
 -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat a
MultiSat (\Models
ms SatNum
satNum b -> Models -> SatNum -> IO Models
k -> MultiSat a
-> Models
-> SatNum
-> (a -> Models -> SatNum -> IO Models)
-> IO Models
forall a.
MultiSat a
-> Models
-> SatNum
-> (a -> Models -> SatNum -> IO Models)
-> IO Models
unMultiSat MultiSat a
m Models
ms SatNum
satNum (b -> Models -> SatNum -> IO Models
k (b -> Models -> SatNum -> IO Models)
-> (a -> b) -> a -> Models -> SatNum -> IO Models
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f))

instance Applicative MultiSat where
  pure :: forall a. a -> MultiSat a
pure a
x = (Models
 -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat a
forall a.
(Models
 -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat a
MultiSat (\Models
ms SatNum
satNum a -> Models -> SatNum -> IO Models
k -> a -> Models -> SatNum -> IO Models
k a
x Models
ms SatNum
satNum)
  MultiSat (a -> b)
mf <*> :: forall a b. MultiSat (a -> b) -> MultiSat a -> MultiSat b
<*> MultiSat a
mx = MultiSat (a -> b)
mf MultiSat (a -> b) -> ((a -> b) -> MultiSat b) -> MultiSat b
forall a b. MultiSat a -> (a -> MultiSat b) -> MultiSat b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a -> b
f -> (a -> b) -> MultiSat a -> MultiSat b
forall a b. (a -> b) -> MultiSat a -> MultiSat b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f MultiSat a
mx

instance Monad MultiSat where
  MultiSat a
m >>= :: forall a b. MultiSat a -> (a -> MultiSat b) -> MultiSat b
>>= a -> MultiSat b
f = (Models
 -> SatNum -> (b -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat b
forall a.
(Models
 -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat a
MultiSat (\Models
ms SatNum
satNum b -> Models -> SatNum -> IO Models
k -> MultiSat a
-> Models
-> SatNum
-> (a -> Models -> SatNum -> IO Models)
-> IO Models
forall a.
MultiSat a
-> Models
-> SatNum
-> (a -> Models -> SatNum -> IO Models)
-> IO Models
unMultiSat MultiSat a
m Models
ms SatNum
satNum (\a
x Models
ms' SatNum
satNum' -> MultiSat b
-> Models
-> SatNum
-> (b -> Models -> SatNum -> IO Models)
-> IO Models
forall a.
MultiSat a
-> Models
-> SatNum
-> (a -> Models -> SatNum -> IO Models)
-> IO Models
unMultiSat (a -> MultiSat b
f a
x) Models
ms' SatNum
satNum' b -> Models -> SatNum -> IO Models
k))

instance MonadIO MultiSat where
  liftIO :: forall a. IO a -> MultiSat a
liftIO IO a
m = (Models
 -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat a
forall a.
(Models
 -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat a
MultiSat (\Models
ms SatNum
satNum a -> Models -> SatNum -> IO Models
k -> do a
x <- IO a
m; a -> Models -> SatNum -> IO Models
k a
x Models
ms SatNum
satNum)

runMultiSat :: SatNum -> MultiSat a -> IO Models
runMultiSat :: forall a. SatNum -> MultiSat a -> IO Models
runMultiSat SatNum
satNum MultiSat a
m = Models -> Models
forall a. [a] -> [a]
reverse (Models -> Models) -> IO Models -> IO Models
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MultiSat a
-> Models
-> SatNum
-> (a -> Models -> SatNum -> IO Models)
-> IO Models
forall a.
MultiSat a
-> Models
-> SatNum
-> (a -> Models -> SatNum -> IO Models)
-> IO Models
unMultiSat MultiSat a
m [] SatNum
satNum (\a
_ Models
ms SatNum
_ -> Models -> IO Models
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Models
ms)

done :: MultiSat a
done :: forall a. MultiSat a
done = (Models
 -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat a
forall a.
(Models
 -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat a
MultiSat (\Models
ms SatNum
_satNum a -> Models -> SatNum -> IO Models
_k -> Models -> IO Models
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Models
ms)

yield :: [(TValue, Expr, Concrete.Value)] -> MultiSat ()
yield :: [(TValue, Expr, Value)] -> MultiSat ()
yield [(TValue, Expr, Value)]
mdl = (Models
 -> SatNum -> (() -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat ()
forall a.
(Models
 -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models)
-> MultiSat a
MultiSat (\Models
ms SatNum
satNum () -> Models -> SatNum -> IO Models
k ->
  case SatNum
satNum of
    SomeSat Int
n
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 -> () -> Models -> SatNum -> IO Models
k () ([(TValue, Expr, Value)]
mdl[(TValue, Expr, Value)] -> Models -> Models
forall a. a -> [a] -> [a]
:Models
ms) (Int -> SatNum
SomeSat (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
      | Bool
otherwise -> Models -> IO Models
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TValue, Expr, Value)]
mdl[(TValue, Expr, Value)] -> Models -> Models
forall a. a -> [a] -> [a]
:Models
ms)
    SatNum
_ -> () -> Models -> SatNum -> IO Models
k () ([(TValue, Expr, Value)]
mdl[(TValue, Expr, Value)] -> Models -> Models
forall a. a -> [a] -> [a]
:Models
ms) SatNum
satNum)

-- Compute all the ways to split a sequences of variables
-- and concrete values for those variables.  Each element
-- of the list consists of a prefix of (varaible,value)
-- pairs whose values we will fix, a single (varaible,value)
-- pair that we will force to be different, and a list of
-- additional unconstrained variables.
computeSplits ::
  [VarShape (What4 sym)] ->
  [VarShape Concrete.Concrete] ->
  [ ( [(VarShape (What4 sym), VarShape Concrete.Concrete)]
    , VarShape (What4 sym)
    , VarShape Concrete.Concrete
    , [VarShape (What4 sym)]
    )
  ]
computeSplits :: forall sym.
[VarShape (What4 sym)]
-> [VarShape Concrete]
-> [([(VarShape (What4 sym), VarShape Concrete)],
     VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
computeSplits [VarShape (What4 sym)]
vs [VarShape Concrete]
cs = [([(VarShape (What4 sym), VarShape Concrete)],
  VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
-> [([(VarShape (What4 sym), VarShape Concrete)],
     VarShape (What4 sym), VarShape Concrete, [VarShape (What4 sym)])]
forall a. [a] -> [a]
reverse
  [ ([(VarShape (What4 sym), VarShape Concrete)]
prefix, VarShape (What4 sym)
v, VarShape Concrete
c, [VarShape (What4 sym)]
tl)
  | [(VarShape (What4 sym), VarShape Concrete)]
prefix <- [(VarShape (What4 sym), VarShape Concrete)]
-> [[(VarShape (What4 sym), VarShape Concrete)]]
forall a. [a] -> [[a]]
inits ([VarShape (What4 sym)]
-> [VarShape Concrete]
-> [(VarShape (What4 sym), VarShape Concrete)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VarShape (What4 sym)]
vs [VarShape Concrete]
cs)
  | VarShape (What4 sym)
v      <- [VarShape (What4 sym)]
vs
  | VarShape Concrete
c      <- [VarShape Concrete]
cs
  | [VarShape (What4 sym)]
tl     <- NonEmpty [VarShape (What4 sym)] -> [[VarShape (What4 sym)]]
forall a. NonEmpty a -> [a]
NE.tail ([VarShape (What4 sym)] -> NonEmpty [VarShape (What4 sym)]
forall (f :: * -> *) a. Foldable f => f a -> NonEmpty [a]
NE.tails [VarShape (What4 sym)]
vs)
  ]
-- == END Support operations for multi-SAT ==

singleQuery ::
  sym ~ W4.ExprBuilder t CryptolState fm =>
  What4 sym ->
  W4ProverConfig ->
  ProverCommand ->
  PrimMap ->
  W4.LogData ->
  [FinType] ->
  [VarShape (What4 sym)] ->
  Maybe (W4.Pred sym) {- ^ optional safety predicate.  Nothing = SAT query -} ->
  W4.Pred sym ->
  IO (Maybe String, ProverResult)

singleQuery :: forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
singleQuery What4 sym
_ W4ProverConfig
W4OfflineConfig ProverCommand
_pc PrimMap
_primMap LogData
_logData [FinType]
_ts [VarShape (What4 sym)]
_args Maybe (Pred sym)
_msafe Pred sym
_query =
  -- this shouldn't happen...
  String -> IO (Maybe String, ProverResult)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"What4 offline solver cannot be used for direct queries"

singleQuery What4 sym
sym (W4Portfolio NonEmpty AnAdapter
ps) ProverCommand
pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape (What4 sym)]
args Maybe (Pred sym)
msafe Pred sym
query =
  do [Async (Maybe String, ProverResult)]
as <- (IO (Maybe String, ProverResult)
 -> IO (Async (Maybe String, ProverResult)))
-> [IO (Maybe String, ProverResult)]
-> IO [Async (Maybe String, ProverResult)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM IO (Maybe String, ProverResult)
-> IO (Async (Maybe String, ProverResult))
forall a. IO a -> IO (Async a)
async [ What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
singleQuery What4 sym
sym (AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
p) ProverCommand
pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape (What4 sym)]
args Maybe (Pred sym)
msafe Pred sym
query
                      | AnAdapter
p <- NonEmpty AnAdapter -> [AnAdapter]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty AnAdapter
ps
                      ]
     [Either SomeException (Maybe String, String)]
-> [Async (Maybe String, ProverResult)]
-> IO (Maybe String, ProverResult)
waitForResults [] [Async (Maybe String, ProverResult)]
as

 where
 waitForResults :: [Either SomeException (Maybe String, String)]
-> [Async (Maybe String, ProverResult)]
-> IO (Maybe String, ProverResult)
waitForResults [Either SomeException (Maybe String, String)]
exs [] = W4Exception -> IO (Maybe String, ProverResult)
forall e a. Exception e => e -> IO a
X.throwIO ([Either SomeException (Maybe String, String)] -> W4Exception
W4PortfolioFailure [Either SomeException (Maybe String, String)]
exs)
 waitForResults [Either SomeException (Maybe String, String)]
exs [Async (Maybe String, ProverResult)]
as =
   do (Async (Maybe String, ProverResult)
winner, Either SomeException (Maybe String, ProverResult)
result) <- [Async (Maybe String, ProverResult)]
-> IO
     (Async (Maybe String, ProverResult),
      Either SomeException (Maybe String, ProverResult))
forall a. [Async a] -> IO (Async a, Either SomeException a)
waitAnyCatch [Async (Maybe String, ProverResult)]
as
      let others :: [Async (Maybe String, ProverResult)]
others = (Async (Maybe String, ProverResult) -> Bool)
-> [Async (Maybe String, ProverResult)]
-> [Async (Maybe String, ProverResult)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Async (Maybe String, ProverResult)
-> Async (Maybe String, ProverResult) -> Bool
forall a. Eq a => a -> a -> Bool
/= Async (Maybe String, ProverResult)
winner) [Async (Maybe String, ProverResult)]
as
      case Either SomeException (Maybe String, ProverResult)
result of
        Left SomeException
ex ->
          [Either SomeException (Maybe String, String)]
-> [Async (Maybe String, ProverResult)]
-> IO (Maybe String, ProverResult)
waitForResults (SomeException -> Either SomeException (Maybe String, String)
forall a b. a -> Either a b
Left SomeException
exEither SomeException (Maybe String, String)
-> [Either SomeException (Maybe String, String)]
-> [Either SomeException (Maybe String, String)]
forall a. a -> [a] -> [a]
:[Either SomeException (Maybe String, String)]
exs) [Async (Maybe String, ProverResult)]
others
        Right (Maybe String
nm, ProverError String
err) ->
          [Either SomeException (Maybe String, String)]
-> [Async (Maybe String, ProverResult)]
-> IO (Maybe String, ProverResult)
waitForResults ((Maybe String, String)
-> Either SomeException (Maybe String, String)
forall a b. b -> Either a b
Right (Maybe String
nm,String
err) Either SomeException (Maybe String, String)
-> [Either SomeException (Maybe String, String)]
-> [Either SomeException (Maybe String, String)]
forall a. a -> [a] -> [a]
: [Either SomeException (Maybe String, String)]
exs) [Async (Maybe String, ProverResult)]
others
        Right (Maybe String, ProverResult)
r ->
          do [Async (Maybe String, ProverResult)]
-> (Async (Maybe String, ProverResult) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Async (Maybe String, ProverResult)]
others (\Async (Maybe String, ProverResult)
a -> ThreadId -> ExitCode -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
X.throwTo (Async (Maybe String, ProverResult) -> ThreadId
forall a. Async a -> ThreadId
asyncThreadId Async (Maybe String, ProverResult)
a) ExitCode
ExitSuccess)
             (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String, ProverResult)
r

singleQuery What4 sym
sym (W4ProverConfig (AnAdapter forall (st :: * -> *). SolverAdapter st
adpt)) ProverCommand
_pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape (What4 sym)]
args Maybe (Pred sym)
msafe Pred sym
query =
  do ProverResult
pres <- SolverAdapter CryptolState
-> forall t fs a.
   ExprBuilder t CryptolState fs
   -> LogData
   -> [BoolExpr t]
   -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
       -> IO a)
   -> IO a
forall (st :: * -> *).
SolverAdapter st
-> forall t fs a.
   ExprBuilder t st fs
   -> LogData
   -> [BoolExpr t]
   -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
       -> IO a)
   -> IO a
W4.solver_adapter_check_sat SolverAdapter CryptolState
forall (st :: * -> *). SolverAdapter st
adpt (What4 (ExprBuilder t CryptolState fm)
-> ExprBuilder t CryptolState fm
forall sym. What4 sym -> sym
w4 What4 sym
What4 (ExprBuilder t CryptolState fm)
sym) LogData
logData [Pred sym
BoolExpr t
query] ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
  -> IO ProverResult)
 -> IO ProverResult)
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO ProverResult)
-> IO ProverResult
forall a b. (a -> b) -> a -> b
$ \SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
res ->
         case SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
res of
           SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
W4.Unknown -> ProverResult -> IO ProverResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> ProverResult
ProverError String
"Solver returned UNKNOWN")
           W4.Unsat ()
_ -> ProverResult -> IO ProverResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TValue] -> ProverResult
ThmResult ((FinType -> TValue) -> [FinType] -> [TValue]
forall a b. (a -> b) -> [a] -> [b]
map FinType -> TValue
unFinType [FinType]
ts))
           W4.Sat (GroundEvalFn t
evalFn,Maybe (ExprRangeBindings t)
_) ->
             do [VarShape Concrete]
xs <- (VarShape (What4 (ExprBuilder t CryptolState fm))
 -> IO (VarShape Concrete))
-> [VarShape (What4 (ExprBuilder t CryptolState fm))]
-> IO [VarShape Concrete]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
forall t fm.
GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
varShapeToConcrete GroundEvalFn t
evalFn) [VarShape (What4 sym)]
[VarShape (What4 (ExprBuilder t CryptolState fm))]
args
                let model :: [(TValue, Expr, Value)]
model = PrimMap
-> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
computeModel PrimMap
primMap [FinType]
ts [VarShape Concrete]
xs
                case Maybe (Pred sym)
msafe of
                  Just Pred sym
s ->
                    do Bool
s' <- GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn Pred sym
BoolExpr t
s
                       let cexType :: CounterExampleType
cexType = if Bool
s' then CounterExampleType
PredicateFalsified else CounterExampleType
SafetyViolation
                       ProverResult -> IO ProverResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CounterExampleType -> [(TValue, Expr, Value)] -> ProverResult
CounterExample CounterExampleType
cexType [(TValue, Expr, Value)]
model)
                  Maybe (Pred sym)
Nothing -> ProverResult -> IO ProverResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Models -> ProverResult
AllSatResult [ [(TValue, Expr, Value)]
model ])

     (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just (SolverAdapter Any -> String
forall (st :: * -> *). SolverAdapter st -> String
W4.solver_adapter_name SolverAdapter Any
forall (st :: * -> *). SolverAdapter st
adpt), ProverResult
pres)

singleQuery What4 sym
sym (W4ProverConfig (AnOnlineAdapter String
nm ProblemFeatures
fs [ConfigDesc]
_opts ConfigTimeout
_ (Proxy s
_ :: Proxy s)))
              ProverCommand{Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcQueryType :: ProverCommand -> QueryType
pcProverName :: ProverCommand -> String
pcVerbose :: ProverCommand -> Bool
pcValidate :: ProverCommand -> Bool
pcProverStats :: ProverCommand -> IORef ProverStats
pcExtraDecls :: ProverCommand -> [DeclGroup]
pcSmtFile :: ProverCommand -> Maybe String
pcExpr :: ProverCommand -> Expr
pcSchema :: ProverCommand -> Schema
pcIgnoreSafety :: ProverCommand -> Bool
pcQueryType :: QueryType
pcProverName :: String
pcVerbose :: Bool
pcValidate :: Bool
pcProverStats :: IORef ProverStats
pcExtraDecls :: [DeclGroup]
pcSmtFile :: Maybe String
pcExpr :: Expr
pcSchema :: Schema
pcIgnoreSafety :: Bool
..} PrimMap
primMap LogData
_logData [FinType]
ts [VarShape (What4 sym)]
args Maybe (Pred sym)
msafe Pred sym
query =
  Maybe String
-> IOMode
-> (Maybe Handle -> IO (Maybe String, ProverResult))
-> IO (Maybe String, ProverResult)
forall r. Maybe String -> IOMode -> (Maybe Handle -> IO r) -> IO r
withMaybeFile Maybe String
pcSmtFile IOMode
WriteMode ((Maybe Handle -> IO (Maybe String, ProverResult))
 -> IO (Maybe String, ProverResult))
-> (Maybe Handle -> IO (Maybe String, ProverResult))
-> IO (Maybe String, ProverResult)
forall a b. (a -> b) -> a -> b
$ \Maybe Handle
smtFileHdl ->
  IO (SolverProcess t s)
-> (SolverProcess t s -> IO ())
-> (SolverProcess t s -> IO (Maybe String, ProverResult))
-> IO (Maybe String, ProverResult)
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
X.bracket
    (ProblemFeatures
-> Maybe Handle
-> ExprBuilder t CryptolState fm
-> IO (SolverProcess t s)
forall solver scope (st :: * -> *) fs.
OnlineSolver solver =>
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope solver)
forall scope (st :: * -> *) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope s)
W4.startSolverProcess ProblemFeatures
fs Maybe Handle
smtFileHdl (What4 (ExprBuilder t CryptolState fm)
-> ExprBuilder t CryptolState fm
forall sym. What4 sym -> sym
w4 What4 sym
What4 (ExprBuilder t CryptolState fm)
sym))
    (IO (ExitCode, Text) -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO (ExitCode, Text) -> IO ())
-> (SolverProcess t s -> IO (ExitCode, Text))
-> SolverProcess t s
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverProcess t s -> IO (ExitCode, Text)
forall scope. SolverProcess scope s -> IO (ExitCode, Text)
forall solver scope.
OnlineSolver solver =>
SolverProcess scope solver -> IO (ExitCode, Text)
W4.shutdownSolverProcess)
    (\ (SolverProcess t s
proc :: W4.SolverProcess t s) ->
        do WriterConn t s -> BoolExpr t -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
W4.assume (SolverProcess t s -> WriterConn t s
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
W4.solverConn SolverProcess t s
proc) Pred sym
BoolExpr t
query
           SatResult (GroundEvalFn t) ()
res <- SolverProcess t s -> String -> IO (SatResult (GroundEvalFn t) ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
W4.checkAndGetModel SolverProcess t s
proc String
"query"
           case SatResult (GroundEvalFn t) ()
res of
             SatResult (GroundEvalFn t) ()
W4.Unknown -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
nm, String -> ProverResult
ProverError String
"Solver returned UNKNOWN")
             W4.Unsat ()
_ -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
nm, [TValue] -> ProverResult
ThmResult ((FinType -> TValue) -> [FinType] -> [TValue]
forall a b. (a -> b) -> [a] -> [b]
map FinType -> TValue
unFinType [FinType]
ts))
             W4.Sat GroundEvalFn t
evalFn ->
               do [VarShape Concrete]
xs <- (VarShape (What4 (ExprBuilder t CryptolState fm))
 -> IO (VarShape Concrete))
-> [VarShape (What4 (ExprBuilder t CryptolState fm))]
-> IO [VarShape Concrete]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
forall t fm.
GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
varShapeToConcrete GroundEvalFn t
evalFn) [VarShape (What4 sym)]
[VarShape (What4 (ExprBuilder t CryptolState fm))]
args
                  let model :: [(TValue, Expr, Value)]
model = PrimMap
-> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
computeModel PrimMap
primMap [FinType]
ts [VarShape Concrete]
xs
                  case Maybe (Pred sym)
msafe of
                    Just Pred sym
s ->
                      do Bool
s' <- GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn Pred sym
BoolExpr t
s
                         let cexType :: CounterExampleType
cexType = if Bool
s' then CounterExampleType
PredicateFalsified else CounterExampleType
SafetyViolation
                         (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
nm, CounterExampleType -> [(TValue, Expr, Value)] -> ProverResult
CounterExample CounterExampleType
cexType [(TValue, Expr, Value)]
model)
                    Maybe (Pred sym)
Nothing -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
nm, Models -> ProverResult
AllSatResult [ [(TValue, Expr, Value)]
model ])
    )


-- | Like 'withFile', but lifted to work over 'Maybe'.
withMaybeFile :: Maybe FilePath -> IOMode -> (Maybe Handle -> IO r) -> IO r
withMaybeFile :: forall r. Maybe String -> IOMode -> (Maybe Handle -> IO r) -> IO r
withMaybeFile Maybe String
mbFP IOMode
mode Maybe Handle -> IO r
action =
  case Maybe String
mbFP of
    Just String
fp -> String -> IOMode -> (Handle -> IO r) -> IO r
forall r. String -> IOMode -> (Handle -> IO r) -> IO r
withFile String
fp IOMode
mode (Maybe Handle -> IO r
action (Maybe Handle -> IO r)
-> (Handle -> Maybe Handle) -> Handle -> IO r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> Maybe Handle
forall a. a -> Maybe a
Just)
    Maybe String
Nothing -> Maybe Handle -> IO r
action Maybe Handle
forall a. Maybe a
Nothing

computeModelPred ::
  sym ~ W4.ExprBuilder t CryptolState fm =>
  What4 sym ->
  VarShape (What4 sym) ->
  VarShape Concrete.Concrete ->
  IO (W4.Pred sym)
computeModelPred :: forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> VarShape (What4 sym) -> VarShape Concrete -> IO (Pred sym)
computeModelPred What4 sym
sym VarShape (What4 sym)
v VarShape Concrete
c =
  (Expr t 'BaseBoolType, Expr t 'BaseBoolType)
-> Expr t 'BaseBoolType
forall a b. (a, b) -> b
snd ((Expr t 'BaseBoolType, Expr t 'BaseBoolType)
 -> Expr t 'BaseBoolType)
-> IO (Expr t 'BaseBoolType, Expr t 'BaseBoolType)
-> IO (Expr t 'BaseBoolType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> W4Eval sym (Expr t 'BaseBoolType)
-> IO (SymExpr sym 'BaseBoolType, Expr t 'BaseBoolType)
forall sym (m :: * -> *) a.
(IsExprBuilder sym, MonadIO m) =>
sym -> W4Eval sym a -> m (Pred sym, a)
doW4Eval (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) (What4 sym
-> (VarShape (What4 sym), VarShape Concrete)
-> SEval (What4 sym) (SBit (What4 sym))
forall sym.
Backend sym =>
sym -> (VarShape sym, VarShape Concrete) -> SEval sym (SBit sym)
varModelPred What4 sym
sym (VarShape (What4 sym)
v, VarShape Concrete
c))

varShapeToConcrete ::
  W4.GroundEvalFn t ->
  VarShape (What4 (W4.ExprBuilder t CryptolState fm)) ->
  IO (VarShape Concrete.Concrete)
varShapeToConcrete :: forall t fm.
GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
varShapeToConcrete GroundEvalFn t
evalFn VarShape (What4 (ExprBuilder t CryptolState fm))
v =
  case VarShape (What4 (ExprBuilder t CryptolState fm))
v of
    VarBit SBit (What4 (ExprBuilder t CryptolState fm))
b -> Bool -> VarShape Concrete
SBit Concrete -> VarShape Concrete
forall sym. SBit sym -> VarShape sym
VarBit (Bool -> VarShape Concrete) -> IO Bool -> IO (VarShape Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn Expr t 'BaseBoolType
SBit (What4 (ExprBuilder t CryptolState fm))
b
    VarInteger SInteger (What4 (ExprBuilder t CryptolState fm))
i -> Integer -> VarShape Concrete
SInteger Concrete -> VarShape Concrete
forall sym. SInteger sym -> VarShape sym
VarInteger (Integer -> VarShape Concrete)
-> IO Integer -> IO (VarShape Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn Expr t BaseIntegerType
SInteger (What4 (ExprBuilder t CryptolState fm))
i
    VarRational SInteger (What4 (ExprBuilder t CryptolState fm))
n SInteger (What4 (ExprBuilder t CryptolState fm))
d -> Integer -> Integer -> VarShape Concrete
SInteger Concrete -> SInteger Concrete -> VarShape Concrete
forall sym. SInteger sym -> SInteger sym -> VarShape sym
VarRational (Integer -> Integer -> VarShape Concrete)
-> IO Integer -> IO (Integer -> VarShape Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn Expr t BaseIntegerType
SInteger (What4 (ExprBuilder t CryptolState fm))
n IO (Integer -> VarShape Concrete)
-> IO Integer -> IO (VarShape Concrete)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn Expr t BaseIntegerType
SInteger (What4 (ExprBuilder t CryptolState fm))
d
    VarWord SWord (ExprBuilder t CryptolState fm)
SWord (What4 (ExprBuilder t CryptolState fm))
SW.ZBV -> VarShape Concrete -> IO (VarShape Concrete)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord Concrete -> VarShape Concrete
forall sym. SWord sym -> VarShape sym
VarWord (Integer -> Integer -> BV
Concrete.mkBv Integer
0 Integer
0))
    VarWord (SW.DBV SymBV (ExprBuilder t CryptolState fm) w
x) ->
      let w :: Integer
w = NatRepr w -> Integer
forall (n :: Natural). NatRepr n -> Integer
W4.intValue (Expr t (BaseBVType w) -> NatRepr w
forall (w :: Natural). Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> *) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV (ExprBuilder t CryptolState fm) w
Expr t (BaseBVType w)
x)
       in SWord Concrete -> VarShape Concrete
BV -> VarShape Concrete
forall sym. SWord sym -> VarShape sym
VarWord (BV -> VarShape Concrete)
-> (BV w -> BV) -> BV w -> VarShape Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BV
Concrete.mkBv Integer
w (Integer -> BV) -> (BV w -> Integer) -> BV w -> BV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned (BV w -> VarShape Concrete) -> IO (BV w) -> IO (VarShape Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn SymBV (ExprBuilder t CryptolState fm) w
Expr t (BaseBVType w)
x
    VarFloat fv :: SFloat (What4 (ExprBuilder t CryptolState fm))
fv@(W4.SFloat SymFloat (ExprBuilder t CryptolState fm) fpp
f) ->
      let (Integer
e,Integer
p) = SFloat (ExprBuilder t CryptolState fm) -> (Integer, Integer)
forall sym. SFloat sym -> (Integer, Integer)
W4.fpSize SFloat (ExprBuilder t CryptolState fm)
SFloat (What4 (ExprBuilder t CryptolState fm))
fv
       in BF -> VarShape Concrete
SFloat Concrete -> VarShape Concrete
forall sym. SFloat sym -> VarShape sym
VarFloat (BF -> VarShape Concrete)
-> (BigFloat -> BF) -> BigFloat -> VarShape Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BigFloat -> BF
FH.BF Integer
e Integer
p (BigFloat -> VarShape Concrete)
-> IO BigFloat -> IO (VarShape Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn SymFloat (ExprBuilder t CryptolState fm) fpp
Expr t (BaseFloatType fpp)
f
    VarFinSeq Integer
n [VarShape (What4 (ExprBuilder t CryptolState fm))]
vs ->
      Integer -> [VarShape Concrete] -> VarShape Concrete
forall sym. Integer -> [VarShape sym] -> VarShape sym
VarFinSeq Integer
n ([VarShape Concrete] -> VarShape Concrete)
-> IO [VarShape Concrete] -> IO (VarShape Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarShape (What4 (ExprBuilder t CryptolState fm))
 -> IO (VarShape Concrete))
-> [VarShape (What4 (ExprBuilder t CryptolState fm))]
-> IO [VarShape Concrete]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
forall t fm.
GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
varShapeToConcrete GroundEvalFn t
evalFn) [VarShape (What4 (ExprBuilder t CryptolState fm))]
vs
    VarTuple [VarShape (What4 (ExprBuilder t CryptolState fm))]
vs ->
      [VarShape Concrete] -> VarShape Concrete
forall sym. [VarShape sym] -> VarShape sym
VarTuple ([VarShape Concrete] -> VarShape Concrete)
-> IO [VarShape Concrete] -> IO (VarShape Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarShape (What4 (ExprBuilder t CryptolState fm))
 -> IO (VarShape Concrete))
-> [VarShape (What4 (ExprBuilder t CryptolState fm))]
-> IO [VarShape Concrete]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
forall t fm.
GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
varShapeToConcrete GroundEvalFn t
evalFn) [VarShape (What4 (ExprBuilder t CryptolState fm))]
vs
    VarRecord RecordMap Ident (VarShape (What4 (ExprBuilder t CryptolState fm)))
fs ->
      RecordMap Ident (VarShape Concrete) -> VarShape Concrete
forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
VarRecord (RecordMap Ident (VarShape Concrete) -> VarShape Concrete)
-> IO (RecordMap Ident (VarShape Concrete))
-> IO (VarShape Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarShape (What4 (ExprBuilder t CryptolState fm))
 -> IO (VarShape Concrete))
-> RecordMap
     Ident (VarShape (What4 (ExprBuilder t CryptolState fm)))
-> IO (RecordMap Ident (VarShape Concrete))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
traverse (GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
forall t fm.
GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
varShapeToConcrete GroundEvalFn t
evalFn) RecordMap Ident (VarShape (What4 (ExprBuilder t CryptolState fm)))
fs
    VarEnum SInteger (What4 (ExprBuilder t CryptolState fm))
tag Vector (ConInfo (VarShape (What4 (ExprBuilder t CryptolState fm))))
cons ->
      Integer
-> Vector (ConInfo (VarShape Concrete)) -> VarShape Concrete
SInteger Concrete
-> Vector (ConInfo (VarShape Concrete)) -> VarShape Concrete
forall sym.
SInteger sym -> Vector (ConInfo (VarShape sym)) -> VarShape sym
VarEnum (Integer
 -> Vector (ConInfo (VarShape Concrete)) -> VarShape Concrete)
-> IO Integer
-> IO (Vector (ConInfo (VarShape Concrete)) -> VarShape Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn Expr t BaseIntegerType
SInteger (What4 (ExprBuilder t CryptolState fm))
tag
              IO (Vector (ConInfo (VarShape Concrete)) -> VarShape Concrete)
-> IO (Vector (ConInfo (VarShape Concrete)))
-> IO (VarShape Concrete)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ConInfo (VarShape (What4 (ExprBuilder t CryptolState fm)))
 -> IO (ConInfo (VarShape Concrete)))
-> Vector
     (ConInfo (VarShape (What4 (ExprBuilder t CryptolState fm))))
-> IO (Vector (ConInfo (VarShape Concrete)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ((VarShape (What4 (ExprBuilder t CryptolState fm))
 -> IO (VarShape Concrete))
-> ConInfo (VarShape (What4 (ExprBuilder t CryptolState fm)))
-> IO (ConInfo (VarShape Concrete))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ConInfo a -> f (ConInfo b)
traverse (GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
forall t fm.
GroundEvalFn t
-> VarShape (What4 (ExprBuilder t CryptolState fm))
-> IO (VarShape Concrete)
varShapeToConcrete GroundEvalFn t
evalFn)) Vector (ConInfo (VarShape (What4 (ExprBuilder t CryptolState fm))))
cons

setAdapterTimeout :: 
  W4.IsExprBuilder sym =>
  AnAdapter ->
  W4.SolverGoalTimeout ->
  sym ->
  IO ()
setAdapterTimeout :: forall sym.
IsExprBuilder sym =>
AnAdapter -> SolverGoalTimeout -> sym -> IO ()
setAdapterTimeout (AnAdapter forall (st :: * -> *). SolverAdapter st
_) SolverGoalTimeout
_timeout sym
_sym =
  () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- NOTE: this is only externalABC at the moment, which has no timeout option
setAdapterTimeout (AnOnlineAdapter String
_ ProblemFeatures
_ [ConfigDesc]
_ ConfigTimeout
cfgTimeout Proxy s
_) SolverGoalTimeout
timeout sym
sym =
  ConfigTimeout -> SolverGoalTimeout -> sym -> IO ()
forall sym.
IsExprBuilder sym =>
ConfigTimeout -> SolverGoalTimeout -> sym -> IO ()
setConfigTimeout ConfigTimeout
cfgTimeout SolverGoalTimeout
timeout sym
sym

setTimeout ::
  W4.IsExprBuilder sym =>
  W4ProverConfig ->
  Integer {- ^ timeout in seconds -} ->
  sym ->
  IO ()
setTimeout :: forall sym.
IsExprBuilder sym =>
W4ProverConfig -> Integer -> sym -> IO ()
setTimeout W4ProverConfig
cfg Integer
s sym
sym = [AnAdapter] -> (AnAdapter -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (W4ProverConfig -> [AnAdapter]
adapters W4ProverConfig
cfg) ((AnAdapter -> IO ()) -> IO ()) -> (AnAdapter -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \AnAdapter
adpt ->
  AnAdapter -> SolverGoalTimeout -> sym -> IO ()
forall sym.
IsExprBuilder sym =>
AnAdapter -> SolverGoalTimeout -> sym -> IO ()
setAdapterTimeout AnAdapter
adpt (Integer -> SolverGoalTimeout
W4.SolverGoalTimeout (Integer
1000 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
s)) sym
sym