{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Symbolic.SBV
( SBVProverConfig
, defaultProver
, proverNames
, setupProver
, satProve
, satProveOffline
, SBVPortfolioException(..)
) where
import Control.Applicative
import Control.Concurrent.Async
import Control.Concurrent.MVar
import Control.Monad.IO.Class
import Control.Monad (when, foldM, forM_)
import Data.Maybe (fromMaybe)
import qualified Data.Map as Map
import qualified Control.Exception as X
import System.Exit (ExitCode(ExitSuccess))
import LibBF(bfNaN)
import qualified Data.SBV as SBV (sObserve, symbolicEnv)
import qualified Data.SBV.Internals as SBV (SBV(..))
import qualified Data.SBV.Dynamic as SBV
import Data.SBV (Timing(SaveTiming))
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 Cryptol.Backend.SBV
import qualified Cryptol.Backend.FloatHelpers as FH
import qualified Cryptol.Eval as Eval
import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Value as Eval
import Cryptol.Eval.SBV
import Cryptol.Parser.Position (emptyRange)
import Cryptol.Symbolic
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Ident (preludeReferenceName, prelPrim, identText)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Logger(logPutStrLn)
import Cryptol.Utils.RecordMap
import Prelude ()
import Prelude.Compat
doSBVEval :: MonadIO m => SBVEval a -> m (SBV.SVal, a)
doSBVEval :: forall (m :: * -> *) a. MonadIO m => SBVEval a -> m (SVal, a)
doSBVEval SBVEval a
m =
(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 a. SBVEval a -> Eval (SBVResult a)
sbvEval SBVEval a
m)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
SBVError EvalErrorEx
err -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall e a. Exception e => e -> IO a
X.throwIO EvalErrorEx
err)
SBVResult SVal
p a
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal
p, a
x)
proverConfigs :: [(String, SBV.SMTConfig)]
proverConfigs :: [(String, SMTConfig)]
proverConfigs =
[ (String
"cvc4" , SMTConfig
SBV.cvc4 )
, (String
"cvc5" , SMTConfig
SBV.cvc5 )
, (String
"yices" , SMTConfig
SBV.yices )
, (String
"z3" , SMTConfig
SBV.z3 )
, (String
"boolector", SMTConfig
SBV.boolector)
, (String
"mathsat" , SMTConfig
SBV.mathSAT )
, (String
"abc" , SMTConfig
SBV.abc )
, (String
"offline" , SMTConfig
SBV.defaultSMTCfg )
, (String
"any" , SMTConfig
SBV.defaultSMTCfg )
, (String
"sbv-cvc4" , SMTConfig
SBV.cvc4 )
, (String
"sbv-cvc5" , SMTConfig
SBV.cvc5 )
, (String
"sbv-yices" , SMTConfig
SBV.yices )
, (String
"sbv-z3" , SMTConfig
SBV.z3 )
, (String
"sbv-boolector", SMTConfig
SBV.boolector)
, (String
"sbv-mathsat" , SMTConfig
SBV.mathSAT )
, (String
"sbv-abc" , SMTConfig
SBV.abc )
, (String
"sbv-offline" , SMTConfig
SBV.defaultSMTCfg )
, (String
"sbv-any" , SMTConfig
SBV.defaultSMTCfg )
]
newtype SBVPortfolioException
= SBVPortfolioException [Either X.SomeException (Maybe String,String)]
instance Show SBVPortfolioException where
show :: SBVPortfolioException -> String
show (SBVPortfolioException [Either SomeException (Maybe String, String)]
exs) =
[String] -> String
unlines (String
"All solvers 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 SBVPortfolioException
data SBVProverConfig
= SBVPortfolio [SBV.SMTConfig]
| SBVProverConfig SBV.SMTConfig
defaultProver :: SBVProverConfig
defaultProver :: SBVProverConfig
defaultProver = SMTConfig -> SBVProverConfig
SBVProverConfig SMTConfig
SBV.z3
proverNames :: [String]
proverNames :: [String]
proverNames = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(String, SMTConfig)]
proverConfigs
setupProver :: String -> IO (Either String ([String], SBVProverConfig))
setupProver :: String -> IO (Either String ([String], SBVProverConfig))
setupProver String
nm
| String
nm forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"any",String
"sbv-any"] =
#if MIN_VERSION_sbv(8,9,0)
do [SMTConfig]
ps <- IO [SMTConfig]
SBV.getAvailableSolvers
#else
do ps <- SBV.sbvAvailableSolvers
#endif
case [SMTConfig]
ps of
[] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left String
"SBV could not find any provers")
[SMTConfig]
_ -> let msg :: String
msg = String
"SBV found the following solvers: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map (SMTSolver -> Solver
SBV.name forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig -> SMTSolver
SBV.solver) [SMTConfig]
ps) in
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right ([String
msg], [SMTConfig] -> SBVProverConfig
SBVPortfolio [SMTConfig]
ps))
| String
nm forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"yices",String
"sbv-yices"] = forall {a}.
SMTConfig -> [String] -> IO (Either a ([String], SBVProverConfig))
tryCfgs SMTConfig
SBV.yices [String
"yices-smt2", String
"yices_smt2"]
| Bool
otherwise =
case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
nm [(String, SMTConfig)]
proverConfigs of
Just SMTConfig
cfg -> forall {a}.
SMTConfig -> [String] -> IO (Either a ([String], SBVProverConfig))
tryCfgs SMTConfig
cfg []
Maybe SMTConfig
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
tryCfgs :: SMTConfig -> [String] -> IO (Either a ([String], SBVProverConfig))
tryCfgs SMTConfig
cfg (String
e:[String]
es) =
do let cfg' :: SMTConfig
cfg' = SMTConfig
cfg{ solver :: SMTSolver
SBV.solver = (SMTConfig -> SMTSolver
SBV.solver SMTConfig
cfg){ executable :: String
SBV.executable = String
e } }
Bool
ok <- SMTConfig -> IO Bool
SBV.sbvCheckSolverInstallation SMTConfig
cfg'
if Bool
ok then forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right ([], SMTConfig -> SBVProverConfig
SBVProverConfig SMTConfig
cfg')) else SMTConfig -> [String] -> IO (Either a ([String], SBVProverConfig))
tryCfgs SMTConfig
cfg [String]
es
tryCfgs SMTConfig
cfg [] =
do Bool
ok <- SMTConfig -> IO Bool
SBV.sbvCheckSolverInstallation SMTConfig
cfg
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (Bool -> [String]
ws Bool
ok, SMTConfig -> SBVProverConfig
SBVProverConfig SMTConfig
cfg))
ws :: Bool -> [String]
ws Bool
ok = if Bool
ok then [] else [String]
notFound
notFound :: [String]
notFound = [String
"Warning: " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" installation not found"]
satSMTResults :: SBV.SatResult -> [SBV.SMTResult]
satSMTResults :: SatResult -> [SMTResult]
satSMTResults (SBV.SatResult SMTResult
r) = [SMTResult
r]
allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult]
#if MIN_VERSION_sbv(8,8,0)
allSatSMTResults :: AllSatResult -> [SMTResult]
allSatSMTResults (SBV.AllSatResult {allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
rs}) = [SMTResult]
rs
#else
allSatSMTResults (SBV.AllSatResult (_, _, _, rs)) = rs
#endif
thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult]
thmSMTResults :: ThmResult -> [SMTResult]
thmSMTResults (SBV.ThmResult SMTResult
r) = [SMTResult
r]
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), [])
isFailedResult :: [SBV.SMTResult] -> Maybe String
isFailedResult :: [SMTResult] -> Maybe String
isFailedResult [] = forall a. a -> Maybe a
Just String
"Solver returned no results!"
isFailedResult (SMTResult
r:[SMTResult]
_) =
case SMTResult
r of
SBV.Unknown SMTConfig
_cfg SMTReasonUnknown
rsn -> forall a. a -> Maybe a
Just (String
"Solver returned UNKNOWN " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SMTReasonUnknown
rsn)
SBV.ProofError SMTConfig
_ [String]
ms Maybe SMTResult
_ -> forall a. a -> Maybe a
Just ([String] -> String
unlines (String
"Solver error" forall a. a -> [a] -> [a]
: [String]
ms))
SMTResult
_ -> forall a. Maybe a
Nothing
runSingleProver ::
ProverCommand ->
(String -> IO ()) ->
SBV.SMTConfig ->
(SBV.SMTConfig -> SBV.Symbolic SBV.SVal -> IO res) ->
(res -> [SBV.SMTResult]) ->
SBV.Symbolic SBV.SVal ->
IO (Maybe String, [SBV.SMTResult])
runSingleProver :: forall res.
ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runSingleProver 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
..} String -> IO ()
lPutStrLn SMTConfig
prover SMTConfig -> Symbolic SVal -> IO res
callSolver res -> [SMTResult]
processResult Symbolic SVal
e = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose forall a b. (a -> b) -> a -> b
$
String -> IO ()
lPutStrLn forall a b. (a -> b) -> a -> b
$ String
"Trying proof with " forall a. [a] -> [a] -> [a]
++
forall a. Show a => a -> String
show (SMTSolver -> Solver
SBV.name (SMTConfig -> SMTSolver
SBV.solver SMTConfig
prover))
res
res <- SMTConfig -> Symbolic SVal -> IO res
callSolver SMTConfig
prover Symbolic SVal
e
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose forall a b. (a -> b) -> a -> b
$
String -> IO ()
lPutStrLn forall a b. (a -> b) -> a -> b
$ String
"Got result from " forall a. [a] -> [a] -> [a]
++
forall a. Show a => a -> String
show (SMTSolver -> Solver
SBV.name (SMTConfig -> SMTSolver
SBV.solver SMTConfig
prover))
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (forall a. Show a => a -> String
show (SMTSolver -> Solver
SBV.name (SMTConfig -> SMTSolver
SBV.solver SMTConfig
prover))), res -> [SMTResult]
processResult res
res)
runMultiProvers ::
ProverCommand ->
(String -> IO ()) ->
[SBV.SMTConfig] ->
(SBV.SMTConfig -> SBV.Symbolic SBV.SVal -> IO res) ->
(res -> [SBV.SMTResult]) ->
SBV.Symbolic SBV.SVal ->
IO (Maybe String, [SBV.SMTResult])
runMultiProvers :: forall res.
ProverCommand
-> (String -> IO ())
-> [SMTConfig]
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runMultiProvers ProverCommand
pc String -> IO ()
lPutStrLn [SMTConfig]
provers SMTConfig -> Symbolic SVal -> IO res
callSolver res -> [SMTResult]
processResult Symbolic SVal
e = do
[Async (Maybe String, [SMTResult])]
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 res.
ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runSingleProver ProverCommand
pc String -> IO ()
lPutStrLn SMTConfig
p SMTConfig -> Symbolic SVal -> IO res
callSolver res -> [SMTResult]
processResult Symbolic SVal
e
| SMTConfig
p <- [SMTConfig]
provers
]
[Either SomeException (Maybe String, String)]
-> [Async (Maybe String, [SMTResult])]
-> IO (Maybe String, [SMTResult])
waitForResults [] [Async (Maybe String, [SMTResult])]
as
where
waitForResults :: [Either SomeException (Maybe String, String)]
-> [Async (Maybe String, [SMTResult])]
-> IO (Maybe String, [SMTResult])
waitForResults [Either SomeException (Maybe String, String)]
exs [] = forall a e. Exception e => e -> a
X.throw ([Either SomeException (Maybe String, String)]
-> SBVPortfolioException
SBVPortfolioException [Either SomeException (Maybe String, String)]
exs)
waitForResults [Either SomeException (Maybe String, String)]
exs [Async (Maybe String, [SMTResult])]
as =
do (Async (Maybe String, [SMTResult])
winner, Either SomeException (Maybe String, [SMTResult])
result) <- forall a. [Async a] -> IO (Async a, Either SomeException a)
waitAnyCatch [Async (Maybe String, [SMTResult])]
as
let others :: [Async (Maybe String, [SMTResult])]
others = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Async (Maybe String, [SMTResult])
winner) [Async (Maybe String, [SMTResult])]
as
case Either SomeException (Maybe String, [SMTResult])
result of
Left SomeException
ex ->
[Either SomeException (Maybe String, String)]
-> [Async (Maybe String, [SMTResult])]
-> IO (Maybe String, [SMTResult])
waitForResults (forall a b. a -> Either a b
Left SomeException
exforall a. a -> [a] -> [a]
:[Either SomeException (Maybe String, String)]
exs) [Async (Maybe String, [SMTResult])]
others
Right r :: (Maybe String, [SMTResult])
r@(Maybe String
nm, [SMTResult]
rs)
| Just String
msg <- [SMTResult] -> Maybe String
isFailedResult [SMTResult]
rs ->
[Either SomeException (Maybe String, String)]
-> [Async (Maybe String, [SMTResult])]
-> IO (Maybe String, [SMTResult])
waitForResults (forall a b. b -> Either a b
Right (Maybe String
nm, String
msg) forall a. a -> [a] -> [a]
: [Either SomeException (Maybe String, String)]
exs) [Async (Maybe String, [SMTResult])]
others
| Bool
otherwise ->
do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Async (Maybe String, [SMTResult])]
others (\Async (Maybe String, [SMTResult])
a -> forall e. Exception e => ThreadId -> e -> IO ()
X.throwTo (forall a. Async a -> ThreadId
asyncThreadId Async (Maybe String, [SMTResult])
a) ExitCode
ExitSuccess)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String, [SMTResult])
r
runProver ::
SBVProverConfig ->
ProverCommand ->
(String -> IO ()) ->
SBV.Symbolic SBV.SVal ->
IO (Maybe String, [SBV.SMTResult])
runProver :: SBVProverConfig
-> ProverCommand
-> (String -> IO ())
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runProver SBVProverConfig
proverConfig 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
..} String -> IO ()
lPutStrLn Symbolic SVal
x =
do let mSatNum :: Maybe Int
mSatNum = case QueryType
pcQueryType of
SatQuery (SomeSat Int
n) -> forall a. a -> Maybe a
Just Int
n
SatQuery SatNum
AllSat -> forall a. Maybe a
Nothing
QueryType
ProveQuery -> forall a. Maybe a
Nothing
QueryType
SafetyQuery -> forall a. Maybe a
Nothing
case SBVProverConfig
proverConfig of
SBVPortfolio [SMTConfig]
ps ->
let ps' :: [SMTConfig]
ps' = [ SMTConfig
p { transcript :: Maybe String
SBV.transcript = Maybe String
pcSmtFile
, timing :: Timing
SBV.timing = IORef ProverStats -> Timing
SaveTiming IORef ProverStats
pcProverStats
, verbose :: Bool
SBV.verbose = Bool
pcVerbose
, validateModel :: Bool
SBV.validateModel = Bool
pcValidate
}
| SMTConfig
p <- [SMTConfig]
ps
] in
case QueryType
pcQueryType of
QueryType
ProveQuery -> forall res.
ProverCommand
-> (String -> IO ())
-> [SMTConfig]
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runMultiProvers ProverCommand
pc String -> IO ()
lPutStrLn [SMTConfig]
ps' SMTConfig -> Symbolic SVal -> IO ThmResult
SBV.proveWith ThmResult -> [SMTResult]
thmSMTResults Symbolic SVal
x
QueryType
SafetyQuery -> forall res.
ProverCommand
-> (String -> IO ())
-> [SMTConfig]
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runMultiProvers ProverCommand
pc String -> IO ()
lPutStrLn [SMTConfig]
ps' SMTConfig -> Symbolic SVal -> IO ThmResult
SBV.proveWith ThmResult -> [SMTResult]
thmSMTResults Symbolic SVal
x
SatQuery (SomeSat Int
1) -> forall res.
ProverCommand
-> (String -> IO ())
-> [SMTConfig]
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runMultiProvers ProverCommand
pc String -> IO ()
lPutStrLn [SMTConfig]
ps' SMTConfig -> Symbolic SVal -> IO SatResult
SBV.satWith SatResult -> [SMTResult]
satSMTResults Symbolic SVal
x
QueryType
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing,
[SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
SBV.ProofError SMTConfig
p
[String
":sat with option prover=any requires option satNum=1"]
forall a. Maybe a
Nothing
| SMTConfig
p <- [SMTConfig]
ps])
SBVProverConfig SMTConfig
p ->
let p' :: SMTConfig
p' = SMTConfig
p { transcript :: Maybe String
SBV.transcript = Maybe String
pcSmtFile
, allSatMaxModelCount :: Maybe Int
SBV.allSatMaxModelCount = Maybe Int
mSatNum
, timing :: Timing
SBV.timing = IORef ProverStats -> Timing
SaveTiming IORef ProverStats
pcProverStats
, verbose :: Bool
SBV.verbose = Bool
pcVerbose
, validateModel :: Bool
SBV.validateModel = Bool
pcValidate
} in
case QueryType
pcQueryType of
QueryType
ProveQuery -> forall res.
ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runSingleProver ProverCommand
pc String -> IO ()
lPutStrLn SMTConfig
p' SMTConfig -> Symbolic SVal -> IO ThmResult
SBV.proveWith ThmResult -> [SMTResult]
thmSMTResults Symbolic SVal
x
QueryType
SafetyQuery -> forall res.
ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runSingleProver ProverCommand
pc String -> IO ()
lPutStrLn SMTConfig
p' SMTConfig -> Symbolic SVal -> IO ThmResult
SBV.proveWith ThmResult -> [SMTResult]
thmSMTResults Symbolic SVal
x
SatQuery (SomeSat Int
1) -> forall res.
ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runSingleProver ProverCommand
pc String -> IO ()
lPutStrLn SMTConfig
p' SMTConfig -> Symbolic SVal -> IO SatResult
SBV.satWith SatResult -> [SMTResult]
satSMTResults Symbolic SVal
x
SatQuery SatNum
_ -> forall res.
ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runSingleProver ProverCommand
pc String -> IO ()
lPutStrLn SMTConfig
p' SMTConfig -> Symbolic SVal -> IO AllSatResult
SBV.allSatWith AllSatResult -> [SMTResult]
allSatSMTResults Symbolic SVal
x
prepareQuery ::
Eval.EvalOpts ->
ProverCommand ->
M.ModuleT IO (Either String ([FinType], SBV.Symbolic SBV.SVal))
prepareQuery :: EvalOpts
-> ProverCommand
-> ModuleT IO (Either String ([FinType], Symbolic SVal))
prepareQuery EvalOpts
evo 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
..} =
do 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
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
Bool
callStacks <- forall (m :: * -> *). Monad m => ModuleT m Bool
M.getCallStacks
let ?callStacks = Bool
callStacks
IO EvalOpts
getEOpts <- ModuleM (IO EvalOpts)
M.getEvalOptsAction
Map Name Newtype
ntEnv <- ModuleM (Map Name Newtype)
M.getNewtypes
let addAsm :: SVal -> SVal -> SVal
addAsm = case QueryType
pcQueryType of
QueryType
ProveQuery -> \SVal
x SVal
y -> SVal -> SVal -> SVal
SBV.svOr (SVal -> SVal
SBV.svNot SVal
x) SVal
y
QueryType
SafetyQuery -> \SVal
x SVal
y -> SVal -> SVal -> SVal
SBV.svOr (SVal -> SVal
SBV.svNot SVal
x) SVal
y
SatQuery SatNum
_ -> \SVal
x SVal
y -> SVal -> SVal -> SVal
SBV.svAnd SVal
x SVal
y
case QueryType -> Schema -> Either String [FinType]
predArgTypes QueryType
pcQueryType Schema
pcSchema of
Left String
msg -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left String
msg)
Right [FinType]
ts -> forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
M.io forall a b. (a -> b) -> a -> b
$
do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose forall a b. (a -> b) -> a -> b
$ Logger -> String -> IO ()
logPutStrLn (EvalOpts -> Logger
Eval.evalLogger EvalOpts
evo) String
"Simulating..."
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ ([FinType]
ts,
do State
sbvState <- forall (m :: * -> *). MonadSymbolic m => m State
SBV.symbolicEnv
MVar State
stateMVar <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. a -> IO (MVar a)
newMVar State
sbvState)
MVar SVal
defRelsVar <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. a -> IO (MVar a)
newMVar SVal
SBV.svTrue)
let sym :: SBV
sym = MVar State -> MVar SVal -> SBV
SBV MVar State
stateMVar MVar SVal
defRelsVar
let tbl :: Map PrimIdent (Prim SBV)
tbl = SBV -> IO EvalOpts -> Map PrimIdent (Prim SBV)
primTable SBV
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 SBV)
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
[SBVEval (GenValue SBV)]
args <- 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 SBV
sym) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
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 (SBV -> FreshVarFns SBV
sbvFreshFns SBV
sym)) [FinType]
ts)
(SVal
safety,SVal
b) <- forall (m :: * -> *) a. MonadIO m => SBVEval a -> m (SVal, a)
doSBVEval forall a b. (a -> b) -> a -> b
$
do GenEvalEnv SBV
env <- forall sym.
EvalPrims sym =>
sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
Eval.evalDecls SBV
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 SBV
sym Map Name Newtype
ntEnv forall a. Monoid a => a
mempty
GenValue SBV
v <- forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
Eval.evalExpr SBV
sym GenEvalEnv SBV
env Expr
pcExpr
GenValue SBV
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 SBV
sym) GenValue SBV
v [SBVEval (GenValue SBV)]
args
case QueryType
pcQueryType of
QueryType
SafetyQuery ->
do forall sym. Backend sym => GenValue sym -> SEval sym ()
Eval.forceValue GenValue SBV
appliedVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure SVal
SBV.svTrue
QueryType
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. GenValue sym -> SBit sym
Eval.fromVBit GenValue SBV
appliedVal)
let safety' :: SVal
safety' = case QueryType
pcQueryType of
QueryType
SafetyQuery -> SVal
safety
QueryType
_ | Bool
pcIgnoreSafety -> SVal
SBV.svTrue
| Bool
otherwise -> SVal
safety
forall a. SymVal a => String -> SBV a -> Symbolic ()
SBV.sObserve String
"safety" (forall a. SVal -> SBV a
SBV.SBV SVal
safety' :: SBV.SBV Bool)
SVal
defRels <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. MVar a -> IO a
readMVar MVar SVal
defRelsVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (SVal -> SVal -> SVal
addAsm SVal
defRels (SVal -> SVal -> SVal
SBV.svAnd SVal
safety' SVal
b)))
processResults ::
ProverCommand ->
[FinType] ->
[SBV.SMTResult] ->
M.ModuleT IO ProverResult
processResults :: ProverCommand
-> [FinType] -> [SMTResult] -> ModuleT IO ProverResult
processResults 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
..} [FinType]
ts [SMTResult]
results =
do let isSat :: Bool
isSat = case QueryType
pcQueryType of
QueryType
ProveQuery -> Bool
False
QueryType
SafetyQuery -> Bool
False
SatQuery SatNum
_ -> Bool
True
PrimMap
prims <- ModuleM PrimMap
M.getPrimMap
case [SMTResult]
results of
(SBV.Satisfiable {} : [SMTResult]
_) | Bool
isSat -> do
[[(TValue, Expr, Value)]]
tevss <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd 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 {m :: * -> *}.
Monad m =>
PrimMap -> SMTResult -> m (Bool, [(TValue, Expr, Value)])
mkTevs PrimMap
prims) [SMTResult]
results
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [[(TValue, Expr, Value)]] -> ProverResult
AllSatResult [[(TValue, Expr, Value)]]
tevss
[r :: SMTResult
r@SBV.Satisfiable{}] -> do
(Bool
safety, [(TValue, Expr, Value)]
res) <- forall {m :: * -> *}.
Monad m =>
PrimMap -> SMTResult -> m (Bool, [(TValue, Expr, Value)])
mkTevs PrimMap
prims SMTResult
r
let cexType :: CounterExampleType
cexType = if Bool
safety then CounterExampleType
PredicateFalsified else CounterExampleType
SafetyViolation
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CounterExampleType -> [(TValue, Expr, Value)] -> ProverResult
CounterExample CounterExampleType
cexType [(TValue, Expr, Value)]
res
[SBV.Unsatisfiable {}] ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [TValue] -> ProverResult
ThmResult (FinType -> TValue
unFinType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinType]
ts)
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [TValue] -> ProverResult
ThmResult (FinType -> TValue
unFinType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinType]
ts)
[SMTResult]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> ProverResult
ProverError ([SMTResult] -> String
rshow [SMTResult]
results)
#if MIN_VERSION_sbv(10,0,0)
where rshow :: [SMTResult] -> String
rshow | Bool
isSat = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Bool -> Bool -> [SMTResult] -> AllSatResult
SBV.AllSatResult Bool
False Bool
False Bool
False)
#elif MIN_VERSION_sbv(8,8,0)
where rshow | isSat = show . (SBV.AllSatResult False False False False)
#else
where rshow | isSat = show . SBV.AllSatResult . (False,False,False,)
#endif
| Bool
otherwise = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTResult -> ThmResult
SBV.ThmResult forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head
where
mkTevs :: PrimMap -> SMTResult -> m (Bool, [(TValue, Expr, Value)])
mkTevs PrimMap
prims SMTResult
result = do
let (CV
safetyCV, [CV]
cvs) =
case SMTResult -> Either String (Bool, [CV])
SBV.getModelAssignment SMTResult
result of
Right (Bool
_, (CV
safetyCV' : [CV]
cvs')) -> (CV
safetyCV', [CV]
cvs')
Either String (Bool, [CV])
_ -> forall a. HasCallStack => String -> a
error String
"processResults: SBV.getModelAssignment failure"
safety :: Bool
safety = CV -> Bool
SBV.cvToBool CV
safetyCV
([VarShape Concrete]
vs, [CV]
_) = [FinType] -> [CV] -> ([VarShape Concrete], [CV])
parseValues [FinType]
ts [CV]
cvs
mdl :: [(TValue, Expr, Value)]
mdl = PrimMap
-> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
computeModel PrimMap
prims [FinType]
ts [VarShape Concrete]
vs
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
safety, [(TValue, Expr, Value)]
mdl)
satProve :: SBVProverConfig -> ProverCommand -> M.ModuleCmd (Maybe String, ProverResult)
satProve :: SBVProverConfig
-> ProverCommand -> ModuleCmd (Maybe String, ProverResult)
satProve SBVProverConfig
proverCfg ProverCommand
pc =
forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack String -> ModuleCmd (Maybe String, ProverResult)
proverError forall a b. (a -> b) -> a -> b
$ \ModuleInput IO
minp ->
forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM ModuleInput IO
minp forall a b. (a -> b) -> a -> b
$ do
EvalOpts
evo <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall (m :: * -> *). ModuleInput m -> m EvalOpts
M.minpEvalOpts ModuleInput IO
minp)
let lPutStrLn :: String -> IO ()
lPutStrLn = Logger -> String -> IO ()
logPutStrLn (EvalOpts -> Logger
Eval.evalLogger EvalOpts
evo)
EvalOpts
-> ProverCommand
-> ModuleT IO (Either String ([FinType], Symbolic SVal))
prepareQuery EvalOpts
evo ProverCommand
pc forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left String
msg -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, String -> ProverResult
ProverError String
msg)
Right ([FinType]
ts, Symbolic SVal
q) ->
do (Maybe String
firstProver, [SMTResult]
results) <- forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
M.io (SBVProverConfig
-> ProverCommand
-> (String -> IO ())
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
runProver SBVProverConfig
proverCfg ProverCommand
pc String -> IO ()
lPutStrLn Symbolic SVal
q)
ProverResult
esatexprs <- ProverCommand
-> [FinType] -> [SMTResult] -> ModuleT IO ProverResult
processResults ProverCommand
pc [FinType]
ts [SMTResult]
results
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
firstProver, ProverResult
esatexprs)
satProveOffline :: SBVProverConfig -> ProverCommand -> M.ModuleCmd (Either String String)
satProveOffline :: SBVProverConfig
-> ProverCommand -> ModuleCmd (Either String String)
satProveOffline SBVProverConfig
_proverCfg 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
msg ModuleInput IO
minp -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (forall a b. a -> Either a b
Left String
msg, forall (m :: * -> *). ModuleInput m -> ModuleEnv
M.minpModuleEnv ModuleInput IO
minp), [])) forall a b. (a -> b) -> a -> b
$
\ModuleInput IO
minp -> forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM ModuleInput IO
minp forall a b. (a -> b) -> a -> b
$
do let isSat :: Bool
isSat = case QueryType
pcQueryType of
QueryType
ProveQuery -> Bool
False
QueryType
SafetyQuery -> Bool
False
SatQuery SatNum
_ -> Bool
True
#if MIN_VERSION_sbv(10,0,0)
generateSMTBenchmark :: Symbolic SVal -> IO String
generateSMTBenchmark
| Bool
isSat = Symbolic SVal -> IO String
SBV.generateSMTBenchmarkSat
| Bool
otherwise = Symbolic SVal -> IO String
SBV.generateSMTBenchmarkProof
#else
generateSMTBenchmark = SBV.generateSMTBenchmark isSat
#endif
EvalOpts
evo <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall (m :: * -> *). ModuleInput m -> m EvalOpts
M.minpEvalOpts ModuleInput IO
minp)
EvalOpts
-> ProverCommand
-> ModuleT IO (Either String ([FinType], Symbolic SVal))
prepareQuery EvalOpts
evo ProverCommand
pc forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left String
msg -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left String
msg)
Right ([FinType]
_ts, Symbolic SVal
q) -> forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
M.io (Symbolic SVal -> IO String
generateSMTBenchmark Symbolic SVal
q)
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 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
parseValues :: [FinType] -> [SBV.CV] -> ([VarShape Concrete.Concrete], [SBV.CV])
parseValues :: [FinType] -> [CV] -> ([VarShape Concrete], [CV])
parseValues [] [CV]
cvs = ([], [CV]
cvs)
parseValues (FinType
t : [FinType]
ts) [CV]
cvs = (VarShape Concrete
v forall a. a -> [a] -> [a]
: [VarShape Concrete]
vs, [CV]
cvs'')
where (VarShape Concrete
v, [CV]
cvs') = FinType -> [CV] -> (VarShape Concrete, [CV])
parseValue FinType
t [CV]
cvs
([VarShape Concrete]
vs, [CV]
cvs'') = [FinType] -> [CV] -> ([VarShape Concrete], [CV])
parseValues [FinType]
ts [CV]
cvs'
parseValue :: FinType -> [SBV.CV] -> (VarShape Concrete.Concrete, [SBV.CV])
parseValue :: FinType -> [CV] -> (VarShape Concrete, [CV])
parseValue FinType
FTBit [] = forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Symbolic.parseValue" [ String
"empty FTBit" ]
parseValue FinType
FTBit (CV
cv : [CV]
cvs) = (forall sym. SBit sym -> VarShape sym
VarBit (CV -> Bool
SBV.cvToBool CV
cv), [CV]
cvs)
parseValue FinType
FTInteger [CV]
cvs =
case forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
SBV.genParse Kind
SBV.KUnbounded [CV]
cvs of
Just (Integer
x, [CV]
cvs') -> (forall sym. SInteger sym -> VarShape sym
VarInteger Integer
x, [CV]
cvs')
Maybe (Integer, [CV])
Nothing -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Symbolic.parseValue" [ String
"no integer" ]
parseValue (FTIntMod Integer
_) [CV]
cvs = FinType -> [CV] -> (VarShape Concrete, [CV])
parseValue FinType
FTInteger [CV]
cvs
parseValue FinType
FTRational [CV]
cvs =
forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Symbolic.parseValue" [String
"no rational"]) forall a b. (a -> b) -> a -> b
$
do (Integer
n,[CV]
cvs') <- forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
SBV.genParse Kind
SBV.KUnbounded [CV]
cvs
(Integer
d,[CV]
cvs'') <- forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
SBV.genParse Kind
SBV.KUnbounded [CV]
cvs'
forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym. SInteger sym -> SInteger sym -> VarShape sym
VarRational Integer
n Integer
d, [CV]
cvs'')
parseValue (FTSeq Integer
0 FinType
FTBit) [CV]
cvs = (forall sym. SWord sym -> VarShape sym
VarWord (Integer -> Integer -> BV
Concrete.mkBv Integer
0 Integer
0), [CV]
cvs)
parseValue (FTSeq Integer
n FinType
FTBit) [CV]
cvs =
case forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
SBV.genParse (Bool -> Int -> Kind
SBV.KBounded Bool
False (forall a. Num a => Integer -> a
fromInteger Integer
n)) [CV]
cvs of
Just (Integer
x, [CV]
cvs') -> (forall sym. SWord sym -> VarShape sym
VarWord (Integer -> Integer -> BV
Concrete.mkBv (forall a. Integral a => a -> Integer
toInteger Integer
n) Integer
x), [CV]
cvs')
Maybe (Integer, [CV])
Nothing -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Symbolic.parseValue" [String
"no bitvector"]
parseValue (FTSeq Integer
n FinType
t) [CV]
cvs = (forall sym. Integer -> [VarShape sym] -> VarShape sym
VarFinSeq (forall a. Integral a => a -> Integer
toInteger Integer
n) [VarShape Concrete]
vs, [CV]
cvs')
where ([VarShape Concrete]
vs, [CV]
cvs') = [FinType] -> [CV] -> ([VarShape Concrete], [CV])
parseValues (forall a. Int -> a -> [a]
replicate (forall a. Num a => Integer -> a
fromInteger Integer
n) FinType
t) [CV]
cvs
parseValue (FTTuple [FinType]
ts) [CV]
cvs = (forall sym. [VarShape sym] -> VarShape sym
VarTuple [VarShape Concrete]
vs, [CV]
cvs')
where ([VarShape Concrete]
vs, [CV]
cvs') = [FinType] -> [CV] -> ([VarShape Concrete], [CV])
parseValues [FinType]
ts [CV]
cvs
parseValue (FTRecord RecordMap Ident FinType
r) [CV]
cvs = (forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
VarRecord RecordMap Ident (VarShape Concrete)
r', [CV]
cvs')
where ([Ident]
ns, [FinType]
ts) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident FinType
r
([VarShape Concrete]
vs, [CV]
cvs') = [FinType] -> [CV] -> ([VarShape Concrete], [CV])
parseValues [FinType]
ts [CV]
cvs
fs :: [(Ident, VarShape Concrete)]
fs = forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
ns [VarShape Concrete]
vs
r' :: RecordMap Ident (VarShape Concrete)
r' = forall a b. (Show a, Ord a) => [a] -> [(a, b)] -> RecordMap a b
recordFromFieldsWithDisplay (forall a b. RecordMap a b -> [a]
displayOrder RecordMap Ident FinType
r) [(Ident, VarShape Concrete)]
fs
parseValue (FTNewtype Newtype
_ [Either Nat' TValue]
_ RecordMap Ident FinType
r) [CV]
cvs = FinType -> [CV] -> (VarShape Concrete, [CV])
parseValue (RecordMap Ident FinType -> FinType
FTRecord RecordMap Ident FinType
r) [CV]
cvs
parseValue (FTFloat Integer
e Integer
p) [CV]
cvs =
(forall sym. SFloat sym -> VarShape sym
VarFloat FH.BF { bfValue :: BigFloat
FH.bfValue = BigFloat
bfNaN
, bfExpWidth :: Integer
FH.bfExpWidth = Integer
e
, bfPrecWidth :: Integer
FH.bfPrecWidth = Integer
p
}
, [CV]
cvs
)
freshBoundedInt :: SBV -> Maybe Integer -> Maybe Integer -> IO SBV.SVal
freshBoundedInt :: SBV -> Maybe Integer -> Maybe Integer -> IO SVal
freshBoundedInt SBV
sym Maybe Integer
lo Maybe Integer
hi =
do SVal
x <- SBV -> IO (SInteger SBV)
freshSInteger_ SBV
sym
case Maybe Integer
lo of
Just Integer
l -> SBV -> SVal -> IO ()
addDefEqn SBV
sym (SVal -> SVal -> SVal
SBV.svLessEq (Kind -> Integer -> SVal
SBV.svInteger Kind
SBV.KUnbounded Integer
l) SVal
x)
Maybe Integer
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
case Maybe Integer
hi of
Just Integer
h -> SBV -> SVal -> IO ()
addDefEqn SBV
sym (SVal -> SVal -> SVal
SBV.svLessEq SVal
x (Kind -> Integer -> SVal
SBV.svInteger Kind
SBV.KUnbounded Integer
h))
Maybe Integer
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
forall (m :: * -> *) a. Monad m => a -> m a
return SVal
x
freshBitvector :: SBV -> Integer -> IO SBV.SVal
freshBitvector :: SBV -> Integer -> IO SVal
freshBitvector SBV
sym Integer
w
| Integer
w forall a. Eq a => a -> a -> Bool
== Integer
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind -> Integer -> SVal
SBV.svInteger (Bool -> Int -> Kind
SBV.KBounded Bool
False Int
0) Integer
0)
| Bool
otherwise = SBV -> Int -> IO (SWord SBV)
freshBV_ SBV
sym (forall a. Num a => Integer -> a
fromInteger Integer
w)
sbvFreshFns :: SBV -> FreshVarFns SBV
sbvFreshFns :: SBV -> FreshVarFns SBV
sbvFreshFns SBV
sym =
FreshVarFns
{ freshBitVar :: IO (SBit SBV)
freshBitVar = SBV -> IO (SBit SBV)
freshSBool_ SBV
sym
, freshWordVar :: Integer -> IO (SWord SBV)
freshWordVar = SBV -> Integer -> IO SVal
freshBitvector SBV
sym
, freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger SBV)
freshIntegerVar = SBV -> Maybe Integer -> Maybe Integer -> IO SVal
freshBoundedInt SBV
sym
, freshFloatVar :: Integer -> Integer -> IO (SFloat SBV)
freshFloatVar = \Integer
_ Integer
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
}