{-# 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
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
}
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
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 ->
Bool ->
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 ->
Bool ->
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), [])
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
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
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 =
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
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
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
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
SolverProcess t s -> [VarShape (What4 sym)] -> MultiSat ()
findMoreModels SolverProcess t s
proc (VarShape (What4 sym)
viforall a. a -> [a] -> [a]
:[VarShape (What4 sym)]
suffix)
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 =
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
SatResult (GroundEvalFn t) ()
W4.Unknown -> forall a. MultiSat a
done
W4.Unsat ()
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
W4.Sat GroundEvalFn t
evalFn ->
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
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)
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)
]
singleQuery ::
sym ~ W4.ExprBuilder t CryptolState fm =>
What4 sym ->
W4ProverConfig ->
ProverCommand ->
PrimMap ->
W4.LogData ->
[FinType] ->
[VarShape (What4 sym)] ->
Maybe (W4.Pred sym) ->
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 =
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 ])
)
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