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

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

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

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

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

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

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

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

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

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


import Prelude ()
import Prelude.Compat

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

instance Show W4Exception where
  show :: W4Exception -> String
show (W4Ex SomeException
e) = 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!"forall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map 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) = 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 forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ String
msg

instance X.Exception W4Exception

rethrowW4Exception :: IO a -> IO a
rethrowW4Exception :: forall a. IO a -> IO a
rethrowW4Exception IO a
m = 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 (forall e a. Exception e => e -> IO a
X.throwIO 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) <- forall e. Exception e => SomeException -> Maybe e
X.fromException SomeException
e = forall a. Maybe a
Nothing
    | Just ( Unsupported
_ :: Eval.Unsupported) <- forall e. Exception e => SomeException -> Maybe e
X.fromException SomeException
e = forall a. Maybe a
Nothing
    | Bool
otherwise = forall a. a -> Maybe a
Just SomeException
e

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


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


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

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

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

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

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

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

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

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

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

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

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

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

proverNames :: [String]
proverNames :: [String]
proverNames = forall a b. (a -> b) -> [a] -> [b]
map 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 =
  forall a. IO a -> IO a
rethrowW4Exception forall a b. (a -> b) -> a -> b
$
  case 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 " forall a. [a] -> [a] -> [a]
++ String
nm, String
"    " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SomeException
ex ]
         forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right ([String]
ws, W4ProverConfig
cfg))

    Just (W4Portfolio NonEmpty AnAdapter
ps) ->
      [AnAdapter] -> IO [AnAdapter]
filterAdapters (forall a. NonEmpty a -> [a]
NE.toList NonEmpty AnAdapter
ps) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
         [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (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: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ([AnAdapter] -> [String]
adapterNames (AnAdapter
pforall a. a -> [a] -> [a]
:[AnAdapter]
ps')) in
           forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right ([String
msg], NonEmpty AnAdapter -> W4ProverConfig
W4Portfolio (AnAdapter
pforall a. a -> [a] -> NonEmpty a
:|[AnAdapter]
ps')))

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

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

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

  filterAdapters :: [AnAdapter] -> IO [AnAdapter]
filterAdapters [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  filterAdapters (AnAdapter
p:[AnAdapter]
ps) =
    AnAdapter -> IO (Maybe SomeException)
tryAdapter AnAdapter
p 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
pforall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnAdapter] -> IO [AnAdapter]
filterAdapters [AnAdapter]
ps

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

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

  tryAdapter (AnOnlineAdapter String
_ ProblemFeatures
fs [ConfigDesc]
opts (Proxy s
_ :: Proxy s)) = IO (Maybe SomeException)
test forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just)
   where
    test :: IO (Maybe SomeException)
test =
      do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym <- forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
W4.newExprBuilder FloatModeRepr 'FloatIEEE
W4.FloatIEEERepr forall t. CryptolState t
CryptolState NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
         [ConfigDesc] -> Config -> IO ()
W4.extendConfig [ConfigDesc]
opts (forall sym. IsExprBuilder sym => sym -> Config
W4.getConfiguration ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym)
         (SolverProcess GlobalNonceGenerator s
proc :: W4.SolverProcess GlobalNonceGenerator s) <- forall solver scope (st :: * -> *) fs.
OnlineSolver solver =>
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope solver)
W4.startSolverProcess ProblemFeatures
fs forall a. Maybe a
Nothing ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym
         SatResult () ()
res <- forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> BoolExpr scope -> IO (SatResult () ())
W4.checkSatisfiable SolverProcess GlobalNonceGenerator s
proc String
"smoke test" (forall sym. IsExprBuilder sym => sym -> Pred sym
W4.falsePred ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
sym)
         case SatResult () ()
res of
           W4.Unsat () -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
           SatResult () ()
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"smoke test failed, expected UNSAT!"
         forall (f :: * -> *) a. Functor f => f a -> f ()
void (forall solver scope.
OnlineSolver solver =>
SolverProcess scope solver -> IO (ExitCode, Text)
W4.shutdownSolverProcess SolverProcess GlobalNonceGenerator s
proc)
         forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

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


data CryptolState t = CryptolState


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

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

what4FreshFns :: W4.IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym)
what4FreshFns :: forall sym. IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym)
what4FreshFns sym
sym =
  FreshVarFns
  { freshBitVar :: IO (SBit (What4 sym))
freshBitVar     = 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    = 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 = 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   = forall sym.
IsSymExprBuilder sym =>
sym -> Integer -> Integer -> IO (SFloat sym)
W4.fpFresh sym
sym
  }

-- | Simulate and manipulate query into a form suitable to be sent
-- to a solver.
prepareQuery ::
  W4.IsSymExprBuilder sym =>
  What4 sym ->
  ProverCommand ->
  M.ModuleT IO (Either String
                       ([FinType],[VarShape (What4 sym)],W4.Pred sym, W4.Pred sym)
               )
prepareQuery :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> ProverCommand
-> ModuleT
     IO
     (Either
        String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
prepareQuery What4 sym
sym ProverCommand { Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
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
.. } = do
  Map Name Newtype
ntEnv <- ModuleM (Map Name Newtype)
M.getNewtypes
  case QueryType -> Schema -> Either String [FinType]
predArgTypes QueryType
pcQueryType Schema
pcSchema of
    Left String
msg -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left String
msg)
    Right [FinType]
ts ->
      do [VarShape (What4 sym)]
args <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
Backend sym =>
FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar (forall sym. IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym)
what4FreshFns (forall sym. What4 sym -> sym
w4 What4 sym
sym))) [FinType]
ts)
         (Pred sym
safety,Pred sym
b) <- Map Name Newtype
-> [VarShape (What4 sym)] -> ModuleT IO (Pred sym, Pred sym)
simulate Map Name Newtype
ntEnv [VarShape (What4 sym)]
args
         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 forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred (forall sym. What4 sym -> sym
w4 What4 sym
sym) else Pred sym
safety

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

              forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                case QueryType
pcQueryType of
                  QueryType
ProveQuery ->
                    do Pred sym
q <- forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
safety' Pred sym
b
                       Pred sym
q' <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
defs Pred sym
q
                       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 <- forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
safety
                       Pred sym
q' <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
defs Pred sym
q
                       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 <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
safety' Pred sym
b
                       Pred sym
q' <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
defs Pred sym
q
                       forall (f :: * -> *) a. Applicative f => a -> f a
pure ([FinType]
ts,[VarShape (What4 sym)]
args,Pred sym
safety',Pred sym
q')
  where
  simulate :: Map Name Newtype
-> [VarShape (What4 sym)] -> ModuleT IO (Pred sym, Pred sym)
simulate Map Name Newtype
ntEnv [VarShape (What4 sym)]
args =
    do let lPutStrLn :: String -> ModuleM ()
lPutStrLn = forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
M.withLogger Logger -> String -> IO ()
logPutStrLn
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose (String -> ModuleM ()
lPutStrLn String
"Simulating...")

       Map PrimIdent Expr
ds <- do (ModulePath
_mp, TCTopEntity
ent) <- Bool -> ImportSource -> ModuleM (ModulePath, TCTopEntity)
M.loadModuleFrom Bool
True (ModName -> ImportSource
M.FromModule ModName
preludeReferenceName)
                let m :: Module
m = TCTopEntity -> Module
tcTopEntityToModule TCTopEntity
ent
                let decls :: [DeclGroup]
decls = forall mname. ModuleG mname -> [DeclGroup]
mDecls Module
m
                let nms :: [Name]
nms = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Map k a -> [(k, a)]
Map.toList (IfaceDecls -> Map Name IfaceDecl
M.ifDecls (forall name. IfaceG name -> IfaceDecls
M.ifDefines (forall name. ModuleG name -> IfaceG name
M.genIface Module
m)))
                let ds :: Map PrimIdent Expr
ds = 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 ]
                forall (f :: * -> *) a. Applicative f => a -> f a
pure Map PrimIdent Expr
ds

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

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

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

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

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

              QueryType
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. GenValue sym -> SBit sym
Eval.fromVBit GenValue (What4 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 pc :: ProverCommand
pc@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
..} =
  forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack String -> ModuleCmd (Maybe String, ProverResult)
proverError \ModuleInput IO
modIn ->
  forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM ModuleInput IO
modIn
  do ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym   <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
makeSym
     MVar (Expr GlobalNonceGenerator 'BaseBoolType)
defVar  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. a -> IO (MVar a)
newMVar (forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym))
     MVar
  (What4FunCache
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
funVar  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. a -> IO (MVar a)
newMVar forall a. Monoid a => a
mempty)
     MVar (Set Text)
uninterpWarnVar <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. a -> IO (MVar a)
newMVar forall a. Monoid a => a
mempty)
     let sym :: What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym = 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)
defVar MVar
  (What4FunCache
     (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))
funVar MVar (Set Text)
uninterpWarnVar
     LogData
logData <- forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
M.withLogger forall {f :: * -> *}. Applicative f => Logger -> () -> f LogData
doLog ()
     UTCTime
start   <- 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   <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> ProverCommand
-> ModuleT
     IO
     (Either
        String ([FinType], [VarShape (What4 sym)], Pred sym, Pred sym))
prepareQuery What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym ProverCommand { Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
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
     forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
warnUninterp
       (forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
M.withLogger Logger -> Set Text -> IO ()
printUninterpWarn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. MVar a -> IO a
readMVar MVar (Set Text)
uninterpWarnVar))
     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
          forall a. IORef a -> a -> IO ()
writeIORef IORef ProverStats
pcProverStats (UTCTime -> UTCTime -> ProverStats
diffUTCTime UTCTime
end UTCTime
start)
          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 <- forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
W4.newExprBuilder FloatModeRepr 'FloatIEEE
W4.FloatIEEERepr
                                  forall t. CryptolState t
CryptolState
                                  NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
       forall t fs.
W4ProverConfig -> ExprBuilder t CryptolState fs -> IO ()
setupAdapterOptions W4ProverConfig
solverCfg ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
hashConsing (forall t (st :: * -> *) fs. ExprBuilder t st fs -> IO ()
W4.startCaching ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym)
       forall (f :: * -> *) a. Applicative f => a -> f a
pure ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)
w4sym

  doLog :: Logger -> () -> f LogData
doLog Logger
lg () =
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
    LogData
defaultLogData
      { logCallbackVerbose :: Int -> String -> IO ()
logCallbackVerbose = \Int
i String
msg -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 ->
            forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
singleQuery What4
  (ExprBuilder GlobalNonceGenerator CryptolState (Flags 'FloatIEEE))
sym W4ProverConfig
solverCfg ProverCommand
pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape
   (What4
      (ExprBuilder
         GlobalNonceGenerator CryptolState (Flags 'FloatIEEE)))]
args (forall a. a -> Maybe a
Just Expr GlobalNonceGenerator 'BaseBoolType
safety) Expr GlobalNonceGenerator 'BaseBoolType
query

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

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

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

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

satProveOffline :: Bool
-> Bool
-> ProverCommand
-> ((Handle -> IO ()) -> IO ())
-> ModuleCmd (Maybe String)
satProveOffline Bool
hashConsing Bool
warnUninterp ProverCommand{ Bool
String
[DeclGroup]
Maybe String
IORef ProverStats
Schema
Expr
QueryType
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 =

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

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


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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

singleQuery What4 sym
sym (W4Portfolio NonEmpty AnAdapter
ps) ProverCommand
pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape (What4 sym)]
args Maybe (Pred sym)
msafe Pred sym
query =
  do [Async (Maybe String, ProverResult)]
as <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. IO a -> IO (Async a)
async [ forall sym t fm.
(sym ~ ExprBuilder t CryptolState fm) =>
What4 sym
-> W4ProverConfig
-> ProverCommand
-> PrimMap
-> LogData
-> [FinType]
-> [VarShape (What4 sym)]
-> Maybe (Pred sym)
-> Pred sym
-> IO (Maybe String, ProverResult)
singleQuery What4 sym
sym (AnAdapter -> W4ProverConfig
W4ProverConfig AnAdapter
p) ProverCommand
pc PrimMap
primMap LogData
logData [FinType]
ts [VarShape (What4 sym)]
args Maybe (Pred sym)
msafe Pred sym
query
                      | AnAdapter
p <- 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 [] = 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) <- forall a. [Async a] -> IO (Async a, Either SomeException a)
waitAnyCatch [Async (Maybe String, ProverResult)]
as
      let others :: [Async (Maybe String, ProverResult)]
others = forall a. (a -> Bool) -> [a] -> [a]
filter (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 (forall a b. a -> Either a b
Left SomeException
exforall 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 (forall a b. b -> Either a b
Right (Maybe String
nm,String
err) forall a. a -> [a] -> [a]
: [Either SomeException (Maybe String, String)]
exs) [Async (Maybe String, ProverResult)]
others
        Right (Maybe String, ProverResult)
r ->
          do 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 -> forall e. Exception e => ThreadId -> e -> IO ()
X.throwTo (forall a. Async a -> ThreadId
asyncThreadId Async (Maybe String, ProverResult)
a) ExitCode
ExitSuccess)
             forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String, ProverResult)
r

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

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

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


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

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

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