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

{-# 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)

-- External interface ----------------------------------------------------------

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

-- | The names of all the solvers supported by SBV
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))

    -- special case, we search for two different yices binaries
  | 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

-- | Select the appropriate solver or solvers from the given prover command,
--   and invoke those solvers on the given symbolic value.
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


-- | Prepare a symbolic query by symbolically simulating the expression found in
--   the @ProverQuery@.  The result will either be an error or a list of the types
--   of the symbolic inputs and the symbolic value to supply to the solver.
--
--   Note that the difference between sat and prove queries is reflected later
--   in `runProver` where we call different SBV methods depending on the mode,
--   so we do _not_ negate the goal here.  Moreover, assumptions are added
--   using conjunction for sat queries and implication for prove queries.
--
--   For safety properties, we want to add them as an additional goal
--   when we do prove queries, and an additional assumption when we do
--   sat queries.  In both cases, the safety property is combined with
--   the main goal via a conjunction.
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

     -- The `addAsm` function is used to combine assumptions that
     -- arise from the types of symbolic variables (e.g. Z n values
     -- are assumed to be integers in the range `0 <= x < n`) with
     -- the main content of the query.  We use conjunction or implication
     -- depending on the type of query.
     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

                 -- Compute the symbolic inputs, and any domain constraints needed
                 -- according to their types.
                 [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)
                 -- Run the main symbolic computation.  First we populate the
                 -- evaluation environment, then we compute the value, finally
                 -- we apply it to the symbolic inputs.
                 (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)

                 -- Ignore the safety condition if the flag is set and we are not
                 -- doing a safety query
                 let safety' :: SVal
safety' = case QueryType
pcQueryType of
                                 QueryType
SafetyQuery -> SVal
safety
                                 QueryType
_ | Bool
pcIgnoreSafety -> SVal
SBV.svTrue
                                   | Bool
otherwise -> SVal
safety

                 -- "observe" the value of the safety predicate.  This makes its value
                 -- avaliable in the resulting model.
                 forall a. SymVal a => String -> SBV a -> Symbolic ()
SBV.sObserve String
"safety" (forall a. SVal -> SBV a
SBV.SBV SVal
safety' :: SBV.SBV Bool)

                 -- read any definitional relations that were asserted
                 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)))

-- | Turn the SMT results from SBV into a @ProverResult@ that is ready for the Cryptol REPL.
--   There may be more than one result if we made a multi-sat query.
processResults ::
  ProverCommand ->
  [FinType] {- ^ Types of the symbolic inputs -} ->
  [SBV.SMTResult] {- ^ Results from the solver -} ->
  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
       -- allSat can return more than one as long as
       -- they're satisfiable
       (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

       -- prove should only have one counterexample
       [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

       -- prove returns only one
       [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)

       -- unsat returns empty
       [] -> 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)

       -- otherwise something is wrong
       [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)
                    -- sbv-10.0.0 removes the `allSatHasPrefixExistentials` field
#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
    -- It's a bit fragile, but the value of the safety predicate seems
    -- to always be the first value in the model assignment list.
    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)


-- | Execute a symbolic ':prove' or ':sat' command.
--
--   This command returns a pair: the first element is the name of the
--   solver that completes the given query (if any) along with the result
--   of executing the query.
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)

-- | Execute a symbolic ':prove' or ':sat' command when the prover is
--   set to offline.  This only prepares the SMT input file for the
--   solver and does not actually invoke the solver.
--
--   This method returns either an error message or the text of
--   the SMT input file corresponding to the given prover command.
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

-- | Given concrete values from the solver and a collection of finite types,
--   reconstruct Cryptol concrete values, and return any unused solver
--   values.
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'

-- | Parse a single value of a finite type by consuming some number of
--   solver values.  The parsed Cryptol values is returned along with
--   any solver values not consumed.
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
   )
   -- XXX: NOT IMPLEMENTED


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 () -- TODO
  }