-- |
-- 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 ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# 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_)
import qualified Control.Exception as X
import System.IO (Handle)
import Data.Time
import Data.IORef
import Data.List (intercalate)
import Data.List.NonEmpty (NonEmpty(..))
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.Backend.What4.SFloat as W4

import qualified Cryptol.Eval as Eval
import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Value as Eval
import           Cryptol.Eval.What4
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.SWord as SW
import           What4.Solver
import qualified What4.Solver.Adapter 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 :: 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 :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack String -> ModuleCmd a
mkErr ModuleCmd a
cmd (EvalOpts, String -> IO ByteString, ModuleEnv)
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 (EvalOpts, String -> IO ByteString, ModuleEnv)
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 (EvalOpts, String -> IO ByteString, ModuleEnv)
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 :: 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 (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
$ Eval (W4Result sym a) -> IO (W4Result sym a)
forall a. Eval a -> IO a
Eval.runEval (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 EvalError
err  -> IO (Pred sym, a) -> m (Pred sym, a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (EvalError -> IO (Pred sym, a)
forall e a. Exception e => e -> IO a
X.throwIO EvalError
err)
       W4Result Pred sym
p a
x -> (Pred sym, a) -> m (Pred sym, a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred sym
p,a
x)


data AnAdapter = AnAdapter (forall st. SolverAdapter st)

data W4ProverConfig
  = W4ProverConfig AnAdapter
  | W4Portfolio (NonEmpty AnAdapter)

proverConfigs :: [(String, W4ProverConfig)]
proverConfigs :: [(String, W4ProverConfig)]
proverConfigs =
  [ (String
"w4-cvc4"     , AnAdapter -> W4ProverConfig
W4ProverConfig ((forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter forall (st :: * -> *). SolverAdapter st
cvc4Adapter) )
  , (String
"w4-yices"    , AnAdapter -> W4ProverConfig
W4ProverConfig ((forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter forall (st :: * -> *). SolverAdapter st
yicesAdapter) )
  , (String
"w4-z3"       , AnAdapter -> W4ProverConfig
W4ProverConfig ((forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter forall (st :: * -> *). SolverAdapter st
z3Adapter) )
  , (String
"w4-boolector", AnAdapter -> W4ProverConfig
W4ProverConfig ((forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter forall (st :: * -> *). SolverAdapter st
boolectorAdapter) )
  , (String
"w4-offline"  , AnAdapter -> W4ProverConfig
W4ProverConfig ((forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter forall (st :: * -> *). SolverAdapter st
z3Adapter) )
  , (String
"w4-any"      , W4ProverConfig
allSolvers)
  ]

allSolvers :: W4ProverConfig
allSolvers :: W4ProverConfig
allSolvers = NonEmpty AnAdapter -> W4ProverConfig
W4Portfolio
  (NonEmpty AnAdapter -> W4ProverConfig)
-> NonEmpty AnAdapter -> W4ProverConfig
forall a b. (a -> b) -> a -> b
$ (forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter forall (st :: * -> *). SolverAdapter st
z3Adapter AnAdapter -> [AnAdapter] -> NonEmpty AnAdapter
forall a. a -> [a] -> NonEmpty a
:|
  [ (forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter forall (st :: * -> *). SolverAdapter st
cvc4Adapter
  , (forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter forall (st :: * -> *). SolverAdapter st
boolectorAdapter
  , (forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter forall (st :: * -> *). SolverAdapter st
yicesAdapter
  ]

defaultProver :: W4ProverConfig
defaultProver :: W4ProverConfig
defaultProver = AnAdapter -> W4ProverConfig
W4ProverConfig ((forall (st :: * -> *). SolverAdapter st) -> AnAdapter
AnAdapter forall (st :: * -> *). SolverAdapter st
z3Adapter)

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 (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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
         [] -> Either String ([String], W4ProverConfig)
-> IO (Either String ([String], W4ProverConfig))
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 (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')))

    Maybe W4ProverConfig
Nothing -> Either String ([String], W4ProverConfig)
-> IO (Either String ([String], W4ProverConfig))
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

  filterAdapters :: [AnAdapter] -> IO [AnAdapter]
filterAdapters [] = [AnAdapter] -> IO [AnAdapter]
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 (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 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



proverError :: String -> M.ModuleCmd (Maybe String, ProverResult)
proverError :: String -> ModuleCmd (Maybe String, ProverResult)
proverError String
msg (EvalOpts
_, String -> IO ByteString
_, ModuleEnv
modEnv) =
  (Either ModuleError ((Maybe String, ProverResult), ModuleEnv),
 [ModuleWarning])
-> IO
     (Either ModuleError ((Maybe String, ProverResult), ModuleEnv),
      [ModuleWarning])
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), ModuleEnv
modEnv), [])


data CryptolState t = CryptolState


setupAdapterOptions :: W4ProverConfig -> W4.ExprBuilder t CryptolState fs -> IO ()
setupAdapterOptions :: 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

  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)


what4FreshFns :: W4.IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym)
what4FreshFns :: sym -> FreshVarFns (What4 sym)
what4FreshFns sym
sym =
  FreshVarFns :: forall sym.
IO (SBit sym)
-> (Integer -> IO (SWord sym))
-> (Maybe Integer -> Maybe Integer -> IO (SInteger sym))
-> (Integer -> Integer -> IO (SFloat sym))
-> FreshVarFns 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)
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 :: 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
pcIgnoreSafety :: ProverCommand -> Bool
pcSchema :: ProverCommand -> Schema
pcExpr :: ProverCommand -> Expr
pcSmtFile :: ProverCommand -> Maybe String
pcExtraDecls :: ProverCommand -> [DeclGroup]
pcProverStats :: ProverCommand -> IORef ProverStats
pcValidate :: ProverCommand -> Bool
pcVerbose :: ProverCommand -> Bool
pcProverName :: ProverCommand -> String
pcQueryType :: ProverCommand -> QueryType
pcIgnoreSafety :: Bool
pcSchema :: Schema
pcExpr :: Expr
pcSmtFile :: Maybe String
pcExtraDecls :: [DeclGroup]
pcProverStats :: IORef ProverStats
pcValidate :: Bool
pcVerbose :: Bool
pcProverName :: String
pcQueryType :: QueryType
.. } =
  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 (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 (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)
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) <- [VarShape (What4 sym)] -> ModuleT IO (Pred sym, Pred sym)
simulate [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 (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 (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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure ([FinType]
ts,[VarShape (What4 sym)]
args,Pred sym
safety',Pred sym
q')
  where
  simulate :: [VarShape (What4 sym)] -> ModuleT IO (Pred sym, Pred sym)
simulate [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, Module
m) <- Bool -> ImportSource -> ModuleM (ModulePath, Module)
M.loadModuleFrom Bool
True (ModName -> ImportSource
M.FromModule ModName
preludeReferenceName)
                let decls :: [DeclGroup]
decls = Module -> [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 (Iface -> IfaceDecls
M.ifPublic (Module -> Iface
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 (f :: * -> *) a. Applicative f => a -> f a
pure Map PrimIdent Expr
ds

       let tbl :: Map PrimIdent (Value sym)
tbl = What4 sym -> Map PrimIdent (Value sym)
forall sym.
IsSymExprBuilder sym =>
What4 sym -> Map PrimIdent (Value sym)
primTable What4 sym
sym
       let ?evalPrim = \i -> (Right <$> Map.lookup i tbl) <|>
                             (Left <$> Map.lookup i ds)

       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)
forall a. Monoid a => a
mempty
            Value sym
v   <- What4 sym
-> GenEvalEnv (What4 sym) -> Expr -> SEval (What4 sym) (Value sym)
forall sym.
EvalPrims sym =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
Eval.evalExpr  What4 sym
sym GenEvalEnv (What4 sym)
env    Expr
pcExpr
            Value sym
appliedVal <-
              (Value sym -> W4Eval sym (Value sym) -> W4Eval sym (Value sym))
-> Value sym -> [W4Eval sym (Value sym)] -> W4Eval sym (Value sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Value sym -> W4Eval sym (Value sym) -> W4Eval sym (Value sym)
forall sym.
GenValue sym
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
Eval.fromVFun Value sym
v ((VarShape (What4 sym) -> W4Eval sym (Value sym))
-> [VarShape (What4 sym)] -> [W4Eval sym (Value sym)]
forall a b. (a -> b) -> [a] -> [b]
map (Value sym -> W4Eval sym (Value sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value sym -> W4Eval sym (Value sym))
-> (VarShape (What4 sym) -> Value sym)
-> VarShape (What4 sym)
-> W4Eval sym (Value sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. What4 sym -> VarShape (What4 sym) -> Value 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 Value sym -> SEval (What4 sym) ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
Eval.forceValue Value sym
appliedVal
                   Pred sym -> W4Eval sym (Pred sym)
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 (f :: * -> *) a. Applicative f => a -> f a
pure (Value sym -> SBit (What4 sym)
forall sym. GenValue sym -> SBit sym
Eval.fromVBit Value sym
appliedVal)


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

satProve :: W4ProverConfig
-> Bool
-> Bool
-> ProverCommand
-> ModuleCmd (Maybe String, ProverResult)
satProve W4ProverConfig
solverCfg Bool
hashConsing Bool
warnUninterp ProverCommand {Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcIgnoreSafety :: Bool
pcSchema :: Schema
pcExpr :: Expr
pcSmtFile :: Maybe String
pcExtraDecls :: [DeclGroup]
pcProverStats :: IORef ProverStats
pcValidate :: Bool
pcVerbose :: Bool
pcProverName :: String
pcQueryType :: QueryType
pcIgnoreSafety :: ProverCommand -> Bool
pcSchema :: ProverCommand -> Schema
pcExpr :: ProverCommand -> Expr
pcSmtFile :: ProverCommand -> Maybe String
pcExtraDecls :: ProverCommand -> [DeclGroup]
pcProverStats :: ProverCommand -> IORef ProverStats
pcValidate :: ProverCommand -> Bool
pcVerbose :: ProverCommand -> Bool
pcProverName :: ProverCommand -> String
pcQueryType :: ProverCommand -> QueryType
..} =
  (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 \(EvalOpts
evo, String -> IO ByteString
byteReader, ModuleEnv
modEnv) ->
  (EvalOpts, String -> IO ByteString, ModuleEnv)
-> ModuleM (Maybe String, ProverResult)
-> IO
     (Either ModuleError ((Maybe String, ProverResult), ModuleEnv),
      [ModuleWarning])
forall a.
(EvalOpts, String -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM (EvalOpts
evo, String -> IO ByteString
byteReader, ModuleEnv
modEnv)
  do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym   <- IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> ModuleT
     IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
makeSym
     MVar (Expr GlobalNonceGenerator 'BaseBoolType)
defVar  <- IO (MVar (Expr GlobalNonceGenerator 'BaseBoolType))
-> ModuleT IO (MVar (Expr GlobalNonceGenerator 'BaseBoolType))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Expr GlobalNonceGenerator 'BaseBoolType
-> IO (MVar (Expr GlobalNonceGenerator 'BaseBoolType))
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 (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 (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 (Expr GlobalNonceGenerator 'BaseBoolType)
MVar
  (Pred
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
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 (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO UTCTime
getCurrentTime
     Either
  String
  ([FinType],
   [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
   Expr GlobalNonceGenerator 'BaseBoolType,
   Expr GlobalNonceGenerator 'BaseBoolType)
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 :: QueryType
-> String
-> Bool
-> Bool
-> IORef ProverStats
-> [DeclGroup]
-> Maybe String
-> Expr
-> Schema
-> Bool
-> ProverCommand
ProverCommand { Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcIgnoreSafety :: Bool
pcSchema :: Schema
pcExpr :: Expr
pcSmtFile :: Maybe String
pcExtraDecls :: [DeclGroup]
pcProverStats :: IORef ProverStats
pcValidate :: Bool
pcVerbose :: Bool
pcProverName :: String
pcQueryType :: QueryType
pcIgnoreSafety :: Bool
pcSchema :: Schema
pcExpr :: Expr
pcSmtFile :: Maybe String
pcExtraDecls :: [DeclGroup]
pcProverStats :: IORef ProverStats
pcValidate :: Bool
pcVerbose :: Bool
pcProverName :: String
pcQueryType :: QueryType
.. }
     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 (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 (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)))],
      Expr GlobalNonceGenerator 'BaseBoolType,
      Expr GlobalNonceGenerator 'BaseBoolType)
-> 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)))],
   Expr GlobalNonceGenerator 'BaseBoolType,
   Expr GlobalNonceGenerator 'BaseBoolType)
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 (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)
       ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
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 (f :: * -> *) a. Applicative f => a -> f a
pure
    LogData
defaultLogData
      { logCallbackVerbose :: Int -> String -> IO ()
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 :: String
logReason = String
"solver query"
      }

  runProver :: What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> LogData
-> PrimMap
-> Either
     String
     ([FinType],
      [VarShape
         (What4
            (ExprBuilder
               GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
      Expr GlobalNonceGenerator 'BaseBoolType,
      Expr GlobalNonceGenerator 'BaseBoolType)
-> 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)))],
   Expr GlobalNonceGenerator 'BaseBoolType,
   Expr GlobalNonceGenerator 'BaseBoolType)
q =
    case Either
  String
  ([FinType],
   [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
   Expr GlobalNonceGenerator 'BaseBoolType,
   Expr GlobalNonceGenerator 'BaseBoolType)
q of
      Left String
msg -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
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,Expr GlobalNonceGenerator 'BaseBoolType
safety,Expr GlobalNonceGenerator 'BaseBoolType
query) ->
        case QueryType
pcQueryType of
          QueryType
ProveQuery ->
            What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> W4ProverConfig
-> 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
-> 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 PrimMap
primMap LogData
logData [FinType]
ts [VarShape
   (What4
      (ExprBuilder
         GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
args
                                                          (Expr GlobalNonceGenerator 'BaseBoolType
-> Maybe (Expr GlobalNonceGenerator 'BaseBoolType)
forall a. a -> Maybe a
Just Expr GlobalNonceGenerator 'BaseBoolType
safety) Expr GlobalNonceGenerator 'BaseBoolType
Pred
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
query

          QueryType
SafetyQuery ->
            What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> W4ProverConfig
-> 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
-> 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 PrimMap
primMap LogData
logData [FinType]
ts [VarShape
   (What4
      (ExprBuilder
         GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
args
                                                          (Expr GlobalNonceGenerator 'BaseBoolType
-> Maybe (Expr GlobalNonceGenerator 'BaseBoolType)
forall a. a -> Maybe a
Just Expr GlobalNonceGenerator 'BaseBoolType
safety) Expr GlobalNonceGenerator 'BaseBoolType
Pred
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
query

          SatQuery SatNum
num ->
            What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> W4ProverConfig
-> 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
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Pred sym
-> SatNum
-> IO (Maybe String, ProverResult)
multiSATQuery What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym W4ProverConfig
solverCfg PrimMap
primMap LogData
logData [FinType]
ts [VarShape
   (What4
      (ExprBuilder
         GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
args
                                                            Expr GlobalNonceGenerator 'BaseBoolType
Pred
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
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 (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 ::
  W4ProverConfig ->
  Bool {- ^ hash consing -} ->
  Bool {- ^ warn on uninterpreted functions -} ->
  ProverCommand ->
  ((Handle -> IO ()) -> IO ()) ->
  M.ModuleCmd (Maybe String)

satProveOffline :: W4ProverConfig
-> Bool
-> Bool
-> ProverCommand
-> ((Handle -> IO ()) -> IO ())
-> ModuleCmd (Maybe String)
satProveOffline (W4Portfolio (AnAdapter
p:|[AnAdapter]
_)) Bool
hashConsing Bool
warnUninterp ProverCommand
cmd (Handle -> IO ()) -> IO ()
outputContinuation =
  W4ProverConfig
-> Bool
-> Bool
-> ProverCommand
-> ((Handle -> IO ()) -> IO ())
-> ModuleCmd (Maybe String)
satProveOffline (AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
p) Bool
hashConsing Bool
warnUninterp ProverCommand
cmd (Handle -> IO ()) -> IO ()
outputContinuation

satProveOffline (W4ProverConfig (AnAdapter forall (st :: * -> *). SolverAdapter st
adpt)) Bool
hashConsing Bool
warnUninterp ProverCommand {Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcIgnoreSafety :: Bool
pcSchema :: Schema
pcExpr :: Expr
pcSmtFile :: Maybe String
pcExtraDecls :: [DeclGroup]
pcProverStats :: IORef ProverStats
pcValidate :: Bool
pcVerbose :: Bool
pcProverName :: String
pcQueryType :: QueryType
pcIgnoreSafety :: ProverCommand -> Bool
pcSchema :: ProverCommand -> Schema
pcExpr :: ProverCommand -> Expr
pcSmtFile :: ProverCommand -> Maybe String
pcExtraDecls :: ProverCommand -> [DeclGroup]
pcProverStats :: ProverCommand -> IORef ProverStats
pcValidate :: ProverCommand -> Bool
pcVerbose :: ProverCommand -> Bool
pcProverName :: ProverCommand -> String
pcQueryType :: ProverCommand -> QueryType
..} (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 a b b a a.
Applicative f =>
a -> (a, b, b) -> f (Either a (Maybe a, b), [a])
onError \(EvalOpts
evo,String -> IO ByteString
byteReader,ModuleEnv
modEnv) ->
  (EvalOpts, String -> IO ByteString, ModuleEnv)
-> ModuleM (Maybe String)
-> IO
     (Either ModuleError (Maybe String, ModuleEnv), [ModuleWarning])
forall a.
(EvalOpts, String -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM (EvalOpts
evo,String -> IO ByteString
byteReader,ModuleEnv
modEnv)
   do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym <- IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
-> ModuleT
     IO
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
makeSym
      MVar (Expr GlobalNonceGenerator 'BaseBoolType)
defVar  <- IO (MVar (Expr GlobalNonceGenerator 'BaseBoolType))
-> ModuleT IO (MVar (Expr GlobalNonceGenerator 'BaseBoolType))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Expr GlobalNonceGenerator 'BaseBoolType
-> IO (MVar (Expr GlobalNonceGenerator 'BaseBoolType))
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 (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 (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 (Expr GlobalNonceGenerator 'BaseBoolType)
MVar
  (Pred
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
defVar MVar
  (What4FunCache
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
funVar MVar (Set Text)
uninterpWarnVar
      Either
  String
  ([FinType],
   [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
   Expr GlobalNonceGenerator 'BaseBoolType,
   Expr GlobalNonceGenerator 'BaseBoolType)
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 :: QueryType
-> String
-> Bool
-> Bool
-> IORef ProverStats
-> [DeclGroup]
-> Maybe String
-> Expr
-> Schema
-> Bool
-> ProverCommand
ProverCommand { Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
pcIgnoreSafety :: Bool
pcSchema :: Schema
pcExpr :: Expr
pcSmtFile :: Maybe String
pcExtraDecls :: [DeclGroup]
pcProverStats :: IORef ProverStats
pcValidate :: Bool
pcVerbose :: Bool
pcProverName :: String
pcQueryType :: QueryType
pcIgnoreSafety :: Bool
pcSchema :: Schema
pcExpr :: Expr
pcSmtFile :: Maybe String
pcExtraDecls :: [DeclGroup]
pcProverStats :: IORef ProverStats
pcValidate :: Bool
pcVerbose :: Bool
pcProverName :: String
pcQueryType :: QueryType
.. }
      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 (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 (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
        case Either
  String
  ([FinType],
   [VarShape
      (What4
         (ExprBuilder
            GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))],
   Expr GlobalNonceGenerator 'BaseBoolType,
   Expr GlobalNonceGenerator 'BaseBoolType)
ok of
          Left String
msg -> Maybe String -> IO (Maybe String)
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,Expr GlobalNonceGenerator 'BaseBoolType
_safety,Expr GlobalNonceGenerator 'BaseBoolType
query) ->
            do (Handle -> IO ()) -> IO ()
outputContinuation
                  (\Handle
hdl -> SolverAdapter CryptolState
-> ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
-> Handle
-> [Expr GlobalNonceGenerator 'BaseBoolType]
-> IO ()
forall (st :: * -> *).
SolverAdapter st
-> forall t fs.
   ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 SolverAdapter CryptolState
forall (st :: * -> *). SolverAdapter st
adpt ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym Handle
hdl [Expr GlobalNonceGenerator 'BaseBoolType
query])
               Maybe String -> IO (Maybe String)
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 (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)
       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 (f :: * -> *) a. Applicative f => a -> f a
pure ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym

  onError :: a -> (a, b, b) -> f (Either a (Maybe a, b), [a])
onError a
msg (a
_,b
_,b
modEnv) = (Either a (Maybe a, b), [a]) -> f (Either a (Maybe a, b), [a])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Maybe a, b) -> Either a (Maybe a, b)
forall a b. b -> Either a b
Right (a -> Maybe a
forall a. a -> Maybe a
Just a
msg, b
modEnv), [])


decSatNum :: SatNum -> SatNum
decSatNum :: SatNum -> SatNum
decSatNum (SomeSat Int
n) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Int -> SatNum
SomeSat (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
decSatNum SatNum
n = SatNum
n


multiSATQuery ::
  sym ~ W4.ExprBuilder t CryptolState fm =>
  What4 sym ->
  W4ProverConfig ->
  PrimMap ->
  W4.LogData ->
  [FinType] ->
  [VarShape (What4 sym)] ->
  W4.Pred sym ->
  SatNum ->
  IO (Maybe String, ProverResult)
multiSATQuery :: What4 sym
-> W4ProverConfig
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Pred sym
-> SatNum
-> IO (Maybe String, ProverResult)
multiSATQuery What4 sym
sym W4ProverConfig
solverCfg 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
-> 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
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
singleQuery What4 sym
sym W4ProverConfig
solverCfg PrimMap
primMap LogData
logData [FinType]
ts [VarShape (What4 sym)]
args Maybe (Pred sym)
forall a. Maybe a
Nothing Pred sym
query

multiSATQuery What4 sym
_sym (W4Portfolio NonEmpty AnAdapter
_) PrimMap
_primMap LogData
_logData [FinType]
_ts [VarShape (What4 sym)]
_args Pred sym
_query SatNum
_satNum =
  String -> IO (Maybe String, ProverResult)
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)) PrimMap
primMap LogData
logData [FinType]
ts [VarShape (What4 sym)]
args Pred sym
query SatNum
satNum0 =
  do Either ProverResult ([(Type, Expr, Value)], BoolExpr t)
pres <- SolverAdapter CryptolState
-> ExprBuilder t CryptolState fm
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO (Either ProverResult ([(Type, Expr, Value)], BoolExpr t)))
-> IO (Either ProverResult ([(Type, Expr, Value)], BoolExpr t))
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 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) LogData
logData [BoolExpr t
Pred sym
query] ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
  -> IO (Either ProverResult ([(Type, Expr, Value)], BoolExpr t)))
 -> IO (Either ProverResult ([(Type, Expr, Value)], BoolExpr t)))
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO (Either ProverResult ([(Type, Expr, Value)], BoolExpr t)))
-> IO (Either ProverResult ([(Type, Expr, Value)], BoolExpr t))
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 -> Either ProverResult ([(Type, Expr, Value)], BoolExpr t)
-> IO (Either ProverResult ([(Type, Expr, Value)], BoolExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (ProverResult
-> Either ProverResult ([(Type, Expr, Value)], BoolExpr t)
forall a b. a -> Either a b
Left (String -> ProverResult
ProverError String
"Solver returned UNKNOWN"))
           W4.Unsat ()
_ -> Either ProverResult ([(Type, Expr, Value)], BoolExpr t)
-> IO (Either ProverResult ([(Type, Expr, Value)], BoolExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (ProverResult
-> Either ProverResult ([(Type, Expr, Value)], BoolExpr t)
forall a b. a -> Either a b
Left ([Type] -> ProverResult
ThmResult ((FinType -> Type) -> [FinType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map FinType -> Type
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)
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 :: [(Type, Expr, Value)]
model = PrimMap
-> [FinType] -> [VarShape Concrete] -> [(Type, Expr, Value)]
computeModel PrimMap
primMap [FinType]
ts [VarShape Concrete]
xs
                BoolExpr t
blockingPred <- 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)
computeBlockingPred What4 sym
sym [VarShape (What4 sym)]
args [VarShape Concrete]
xs
                Either ProverResult ([(Type, Expr, Value)], BoolExpr t)
-> IO (Either ProverResult ([(Type, Expr, Value)], BoolExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (([(Type, Expr, Value)], BoolExpr t)
-> Either ProverResult ([(Type, Expr, Value)], BoolExpr t)
forall a b. b -> Either a b
Right ([(Type, Expr, Value)]
model, BoolExpr t
blockingPred))

     case Either ProverResult ([(Type, Expr, Value)], BoolExpr t)
pres of
       Left ProverResult
res -> (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just (SolverAdapter Any -> String
forall (st :: * -> *). SolverAdapter st -> String
solver_adapter_name SolverAdapter Any
forall (st :: * -> *). SolverAdapter st
adpt), ProverResult
res)
       Right ([(Type, Expr, Value)]
mdl,BoolExpr t
block) ->
         do [[(Type, Expr, Value)]]
mdls <- ([(Type, Expr, Value)]
mdl[(Type, Expr, Value)]
-> [[(Type, Expr, Value)]] -> [[(Type, Expr, Value)]]
forall a. a -> [a] -> [a]
:) ([[(Type, Expr, Value)]] -> [[(Type, Expr, Value)]])
-> IO [[(Type, Expr, Value)]] -> IO [[(Type, Expr, Value)]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BoolExpr t] -> SatNum -> IO [[(Type, Expr, Value)]]
computeMoreModels [BoolExpr t
block,BoolExpr t
Pred sym
query] (SatNum -> SatNum
decSatNum SatNum
satNum0)
            (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
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
solver_adapter_name SolverAdapter Any
forall (st :: * -> *). SolverAdapter st
adpt), [[(Type, Expr, Value)]] -> ProverResult
AllSatResult [[(Type, Expr, Value)]]
mdls)

  where

  computeMoreModels :: [BoolExpr t] -> SatNum -> IO [[(Type, Expr, Value)]]
computeMoreModels [BoolExpr t]
_qs (SomeSat Int
n) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [[(Type, Expr, Value)]] -> IO [[(Type, Expr, Value)]]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- should never happen...
  computeMoreModels [BoolExpr t]
qs (SomeSat Int
n) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = -- final model
    SolverAdapter CryptolState
-> ExprBuilder t CryptolState fm
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO [[(Type, Expr, Value)]])
-> IO [[(Type, Expr, Value)]]
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 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) LogData
logData [BoolExpr t]
qs ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
  -> IO [[(Type, Expr, Value)]])
 -> IO [[(Type, Expr, Value)]])
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO [[(Type, Expr, Value)]])
-> IO [[(Type, Expr, Value)]]
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 -> [[(Type, Expr, Value)]] -> IO [[(Type, Expr, Value)]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
           W4.Unsat ()
_ -> [[(Type, Expr, Value)]] -> IO [[(Type, Expr, Value)]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
           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)
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 :: [(Type, Expr, Value)]
model = PrimMap
-> [FinType] -> [VarShape Concrete] -> [(Type, Expr, Value)]
computeModel PrimMap
primMap [FinType]
ts [VarShape Concrete]
xs
                [[(Type, Expr, Value)]] -> IO [[(Type, Expr, Value)]]
forall (m :: * -> *) a. Monad m => a -> m a
return [[(Type, Expr, Value)]
model]

  computeMoreModels [BoolExpr t]
qs SatNum
satNum =
    do Maybe ([(Type, Expr, Value)], BoolExpr t)
pres <- SolverAdapter CryptolState
-> ExprBuilder t CryptolState fm
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO (Maybe ([(Type, Expr, Value)], BoolExpr t)))
-> IO (Maybe ([(Type, Expr, Value)], BoolExpr t))
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 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) LogData
logData [BoolExpr t]
qs ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
  -> IO (Maybe ([(Type, Expr, Value)], BoolExpr t)))
 -> IO (Maybe ([(Type, Expr, Value)], BoolExpr t)))
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO (Maybe ([(Type, Expr, Value)], BoolExpr t)))
-> IO (Maybe ([(Type, Expr, Value)], BoolExpr t))
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 -> Maybe ([(Type, Expr, Value)], BoolExpr t)
-> IO (Maybe ([(Type, Expr, Value)], BoolExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(Type, Expr, Value)], BoolExpr t)
forall a. Maybe a
Nothing
           W4.Unsat ()
_ -> Maybe ([(Type, Expr, Value)], BoolExpr t)
-> IO (Maybe ([(Type, Expr, Value)], BoolExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(Type, Expr, Value)], BoolExpr t)
forall a. Maybe a
Nothing
           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)
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 :: [(Type, Expr, Value)]
model = PrimMap
-> [FinType] -> [VarShape Concrete] -> [(Type, Expr, Value)]
computeModel PrimMap
primMap [FinType]
ts [VarShape Concrete]
xs
                BoolExpr t
blockingPred <- 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)
computeBlockingPred What4 sym
sym [VarShape (What4 sym)]
args [VarShape Concrete]
xs
                Maybe ([(Type, Expr, Value)], BoolExpr t)
-> IO (Maybe ([(Type, Expr, Value)], BoolExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (([(Type, Expr, Value)], BoolExpr t)
-> Maybe ([(Type, Expr, Value)], BoolExpr t)
forall a. a -> Maybe a
Just ([(Type, Expr, Value)]
model, BoolExpr t
blockingPred))

       case Maybe ([(Type, Expr, Value)], BoolExpr t)
pres of
         Maybe ([(Type, Expr, Value)], BoolExpr t)
Nothing -> [[(Type, Expr, Value)]] -> IO [[(Type, Expr, Value)]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
         Just ([(Type, Expr, Value)]
mdl, BoolExpr t
block) ->
           ([(Type, Expr, Value)]
mdl[(Type, Expr, Value)]
-> [[(Type, Expr, Value)]] -> [[(Type, Expr, Value)]]
forall a. a -> [a] -> [a]
:) ([[(Type, Expr, Value)]] -> [[(Type, Expr, Value)]])
-> IO [[(Type, Expr, Value)]] -> IO [[(Type, Expr, Value)]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BoolExpr t] -> SatNum -> IO [[(Type, Expr, Value)]]
computeMoreModels (BoolExpr t
blockBoolExpr t -> [BoolExpr t] -> [BoolExpr t]
forall a. a -> [a] -> [a]
:[BoolExpr t]
qs) (SatNum -> SatNum
decSatNum SatNum
satNum)

singleQuery ::
  sym ~ W4.ExprBuilder t CryptolState fm =>
  What4 sym ->
  W4ProverConfig ->
  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 :: What4 sym
-> W4ProverConfig
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
singleQuery What4 sym
sym (W4Portfolio NonEmpty AnAdapter
ps) 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)
mapM IO (Maybe String, ProverResult)
-> IO (Async (Maybe String, ProverResult))
forall a. IO a -> IO (Async a)
async [ What4 sym
-> W4ProverConfig
-> 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
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
singleQuery What4 sym
sym (AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
p) 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 (m :: * -> *) a. Monad m => a -> m a
return (Maybe String, ProverResult)
r

singleQuery What4 sym
sym (W4ProverConfig (AnAdapter forall (st :: * -> *). SolverAdapter st
adpt)) PrimMap
primMap LogData
logData [FinType]
ts [VarShape (What4 sym)]
args Maybe (Pred sym)
msafe Pred sym
query =
  do ProverResult
pres <- SolverAdapter CryptolState
-> ExprBuilder t CryptolState fm
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO ProverResult)
-> IO ProverResult
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 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) LogData
logData [BoolExpr t
Pred sym
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 (m :: * -> *) a. Monad m => a -> m a
return (String -> ProverResult
ProverError String
"Solver returned UNKNOWN")
           W4.Unsat ()
_ -> ProverResult -> IO ProverResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> ProverResult
ThmResult ((FinType -> Type) -> [FinType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map FinType -> Type
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)
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 :: [(Type, Expr, Value)]
model = PrimMap
-> [FinType] -> [VarShape Concrete] -> [(Type, 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 -> BoolExpr t -> IO (GroundValue 'BaseBoolType)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn BoolExpr t
Pred sym
s
                       let cexType :: CounterExampleType
cexType = if Bool
s' then CounterExampleType
PredicateFalsified else CounterExampleType
SafetyViolation
                       ProverResult -> IO ProverResult
forall (m :: * -> *) a. Monad m => a -> m a
return (CounterExampleType -> [(Type, Expr, Value)] -> ProverResult
CounterExample CounterExampleType
cexType [(Type, Expr, Value)]
model)
                  Maybe (Pred sym)
Nothing -> ProverResult -> IO ProverResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([[(Type, Expr, Value)]] -> ProverResult
AllSatResult [ [(Type, Expr, Value)]
model ])

     (Maybe String, ProverResult) -> IO (Maybe String, ProverResult)
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)


computeBlockingPred ::
  sym ~ W4.ExprBuilder t CryptolState fm =>
  What4 sym ->
  [VarShape (What4 sym)] ->
  [VarShape Concrete.Concrete] ->
  IO (W4.Pred sym)
computeBlockingPred :: What4 sym
-> [VarShape (What4 sym)] -> [VarShape Concrete] -> IO (Pred sym)
computeBlockingPred What4 sym
sym [VarShape (What4 sym)]
vs [VarShape Concrete]
xs =
  do (Expr t 'BaseBoolType, Expr t 'BaseBoolType)
res <- sym
-> W4Eval sym (Expr t 'BaseBoolType)
-> IO (Pred sym, 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)
modelPred What4 sym
sym [VarShape (What4 sym)]
vs [VarShape Concrete]
xs)
     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, Expr t 'BaseBoolType)
-> Expr t 'BaseBoolType
forall a b. (a, b) -> b
snd (Expr t 'BaseBoolType, Expr t 'BaseBoolType)
res)

varShapeToConcrete ::
  W4.GroundEvalFn t ->
  VarShape (What4 (W4.ExprBuilder t CryptolState fm)) ->
  IO (VarShape Concrete.Concrete)
varShapeToConcrete :: 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
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
-> Expr t 'BaseBoolType -> IO (GroundValue 'BaseBoolType)
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
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
-> Expr t BaseIntegerType -> IO (GroundValue BaseIntegerType)
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
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
-> Expr t BaseIntegerType -> IO (GroundValue BaseIntegerType)
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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GroundEvalFn t
-> Expr t BaseIntegerType -> IO (GroundValue BaseIntegerType)
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 (What4 (ExprBuilder t CryptolState fm))
SW.ZBV -> VarShape Concrete -> IO (VarShape Concrete)
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 x) ->
      let w :: Integer
w = NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
W4.intValue (Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> *) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth Expr t (BaseBVType w)
SymBV (ExprBuilder t CryptolState fm) w
x)
       in 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 :: Nat). 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
-> Expr t (BaseBVType w) -> IO (GroundValue (BaseBVType w))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn Expr t (BaseBVType w)
SymBV (ExprBuilder t CryptolState fm) w
x
    VarFloat fv :: SFloat (What4 (ExprBuilder t CryptolState fm))
fv@(W4.SFloat f) ->
      do 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
         BF -> VarShape Concrete
forall sym. SFloat sym -> VarShape sym
VarFloat (BF -> VarShape Concrete)
-> (BV (FloatPrecisionBits fpp) -> BF)
-> BV (FloatPrecisionBits fpp)
-> VarShape Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer -> BF
FH.floatFromBits Integer
e Integer
p (Integer -> BF)
-> (BV (FloatPrecisionBits fpp) -> Integer)
-> BV (FloatPrecisionBits fpp)
-> BF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV (FloatPrecisionBits fpp) -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV (FloatPrecisionBits fpp) -> VarShape Concrete)
-> IO (BV (FloatPrecisionBits fpp)) -> IO (VarShape Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseFloatType fpp)
-> IO (GroundValue (BaseFloatType fpp))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
W4.groundEval GroundEvalFn t
evalFn Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t CryptolState fm) 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)
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)
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)
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