-- |
-- 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 :: SBVEval a -> m (SVal, a)
doSBVEval SBVEval a
m =
  (IO (SBVResult a) -> m (SBVResult a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SBVResult a) -> m (SBVResult a))
-> IO (SBVResult a) -> m (SBVResult a)
forall a b. (a -> b) -> a -> b
$ CallStack -> Eval (SBVResult a) -> IO (SBVResult a)
forall a. CallStack -> Eval a -> IO a
Eval.runEval CallStack
forall a. Monoid a => a
mempty (SBVEval a -> Eval (SBVResult a)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval SBVEval a
m)) m (SBVResult a) -> (SBVResult a -> m (SVal, a)) -> m (SVal, a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    SBVError EvalErrorEx
err -> IO (SVal, a) -> m (SVal, a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (EvalErrorEx -> IO (SVal, a)
forall e a. Exception e => e -> IO a
X.throwIO EvalErrorEx
err)
    SBVResult SVal
p a
x -> (SVal, a) -> m (SVal, a)
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
"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-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!" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Either SomeException (Maybe String, String) -> String)
-> [Either SomeException (Maybe String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Either SomeException (Maybe String, String) -> String
forall e. Exception e => Either e (Maybe String, String) -> String
f [Either SomeException (Maybe String, String)]
exs)
    where
    f :: Either e (Maybe String, String) -> String
f (Left e
e) = e -> String
forall e. Exception e => e -> String
X.displayException e
e
    f (Right (Maybe String
Nothing, String
msg)) = String
msg
    f (Right (Just String
nm, String
msg)) = String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg

instance X.Exception 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 = ((String, SMTConfig) -> String)
-> [(String, SMTConfig)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, SMTConfig) -> String
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 String -> [String] -> Bool
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
         [] -> Either String ([String], SBVProverConfig)
-> IO (Either String ([String], SBVProverConfig))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Either String ([String], SBVProverConfig)
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: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Solver] -> String
forall a. Show a => a -> String
show ((SMTConfig -> Solver) -> [SMTConfig] -> [Solver]
forall a b. (a -> b) -> [a] -> [b]
map (SMTSolver -> Solver
SBV.name (SMTSolver -> Solver)
-> (SMTConfig -> SMTSolver) -> SMTConfig -> Solver
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig -> SMTSolver
SBV.solver) [SMTConfig]
ps) in
               Either String ([String], SBVProverConfig)
-> IO (Either String ([String], SBVProverConfig))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([String], SBVProverConfig)
-> Either String ([String], SBVProverConfig)
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 String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"yices",String
"sbv-yices"] = SMTConfig
-> [String] -> IO (Either String ([String], SBVProverConfig))
forall a.
SMTConfig -> [String] -> IO (Either a ([String], SBVProverConfig))
tryCfgs SMTConfig
SBV.yices [String
"yices-smt2", String
"yices_smt2"]

  | Bool
otherwise =
    case String -> [(String, SMTConfig)] -> Maybe SMTConfig
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
nm [(String, SMTConfig)]
proverConfigs of
      Just SMTConfig
cfg -> SMTConfig
-> [String] -> IO (Either String ([String], SBVProverConfig))
forall a.
SMTConfig -> [String] -> IO (Either a ([String], SBVProverConfig))
tryCfgs SMTConfig
cfg []
      Maybe SMTConfig
Nothing  -> Either String ([String], SBVProverConfig)
-> IO (Either String ([String], SBVProverConfig))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Either String ([String], SBVProverConfig)
forall a b. a -> Either a b
Left (String
"unknown solver name: " String -> ShowS
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 Either a ([String], SBVProverConfig)
-> IO (Either a ([String], SBVProverConfig))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([String], SBVProverConfig) -> Either a ([String], SBVProverConfig)
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
       Either a ([String], SBVProverConfig)
-> IO (Either a ([String], SBVProverConfig))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([String], SBVProverConfig) -> Either a ([String], SBVProverConfig)
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: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
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 =
  (Either ModuleError ((Maybe String, ProverResult), ModuleEnv),
 [ModuleWarning])
-> IO
     (Either ModuleError ((Maybe String, ProverResult), ModuleEnv),
      [ModuleWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return (((Maybe String, ProverResult), ModuleEnv)
-> Either ModuleError ((Maybe String, ProverResult), ModuleEnv)
forall a b. b -> Either a b
Right ((Maybe String
forall a. Maybe a
Nothing, String -> ProverResult
ProverError String
msg), ModuleInput IO -> ModuleEnv
forall (m :: * -> *). ModuleInput m -> ModuleEnv
M.minpModuleEnv ModuleInput IO
minp), [])


isFailedResult :: [SBV.SMTResult] -> Maybe String
isFailedResult :: [SMTResult] -> Maybe String
isFailedResult [] = String -> Maybe String
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  -> String -> Maybe String
forall a. a -> Maybe a
Just (String
"Solver returned UNKNOWN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTReasonUnknown -> String
forall a. Show a => a -> String
show SMTReasonUnknown
rsn)
    SBV.ProofError SMTConfig
_ [String]
ms Maybe SMTResult
_ -> String -> Maybe String
forall a. a -> Maybe a
Just ([String] -> String
unlines (String
"Solver error" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ms))
    SMTResult
_ -> Maybe String
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 :: 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
   Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
     String -> IO ()
lPutStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Trying proof with " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                               Solver -> String
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

   Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
     String -> IO ()
lPutStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Got result from " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                               Solver -> String
forall a. Show a => a -> String
show (SMTSolver -> Solver
SBV.name (SMTConfig -> SMTSolver
SBV.solver SMTConfig
prover))
   (Maybe String, [SMTResult]) -> IO (Maybe String, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just (Solver -> String
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 :: 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 <- (IO (Maybe String, [SMTResult])
 -> IO (Async (Maybe String, [SMTResult])))
-> [IO (Maybe String, [SMTResult])]
-> IO [Async (Maybe String, [SMTResult])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM IO (Maybe String, [SMTResult])
-> IO (Async (Maybe String, [SMTResult]))
forall a. IO a -> IO (Async a)
async [ ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO res)
-> (res -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
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 [] = SBVPortfolioException -> IO (Maybe String, [SMTResult])
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) <- [Async (Maybe String, [SMTResult])]
-> IO
     (Async (Maybe String, [SMTResult]),
      Either SomeException (Maybe String, [SMTResult]))
forall a. [Async a] -> IO (Async a, Either SomeException a)
waitAnyCatch [Async (Maybe String, [SMTResult])]
as
      let others :: [Async (Maybe String, [SMTResult])]
others = (Async (Maybe String, [SMTResult]) -> Bool)
-> [Async (Maybe String, [SMTResult])]
-> [Async (Maybe String, [SMTResult])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Async (Maybe String, [SMTResult])
-> Async (Maybe String, [SMTResult]) -> Bool
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 (SomeException -> Either SomeException (Maybe String, String)
forall a b. a -> Either a b
Left SomeException
exEither SomeException (Maybe String, String)
-> [Either SomeException (Maybe String, String)]
-> [Either SomeException (Maybe String, String)]
forall a. a -> [a] -> [a]
:[Either SomeException (Maybe String, String)]
exs) [Async (Maybe String, [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 ((Maybe String, String)
-> Either SomeException (Maybe String, String)
forall a b. b -> Either a b
Right (Maybe String
nm, String
msg) Either SomeException (Maybe String, String)
-> [Either SomeException (Maybe String, String)]
-> [Either SomeException (Maybe String, String)]
forall a. a -> [a] -> [a]
: [Either SomeException (Maybe String, String)]
exs) [Async (Maybe String, [SMTResult])]
others
          | Bool
otherwise ->
              do [Async (Maybe String, [SMTResult])]
-> (Async (Maybe String, [SMTResult]) -> IO ()) -> IO ()
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 -> ThreadId -> ExitCode -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
X.throwTo (Async (Maybe String, [SMTResult]) -> ThreadId
forall a. Async a -> ThreadId
asyncThreadId Async (Maybe String, [SMTResult])
a) ExitCode
ExitSuccess)
                 (Maybe String, [SMTResult]) -> IO (Maybe String, [SMTResult])
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) -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n
                     SatQuery SatNum
AllSat -> Maybe Int
forall a. Maybe a
Nothing
                     QueryType
ProveQuery -> Maybe Int
forall a. Maybe a
Nothing
                     QueryType
SafetyQuery -> Maybe Int
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  -> ProverCommand
-> (String -> IO ())
-> [SMTConfig]
-> (SMTConfig -> Symbolic SVal -> IO ThmResult)
-> (ThmResult -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
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 -> ProverCommand
-> (String -> IO ())
-> [SMTConfig]
-> (SMTConfig -> Symbolic SVal -> IO ThmResult)
-> (ThmResult -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
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) -> ProverCommand
-> (String -> IO ())
-> [SMTConfig]
-> (SMTConfig -> Symbolic SVal -> IO SatResult)
-> (SatResult -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
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
_ -> (Maybe String, [SMTResult]) -> IO (Maybe String, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
forall a. Maybe a
Nothing,
                   [SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
SBV.ProofError SMTConfig
p
                     [String
":sat with option prover=any requires option satNum=1"]
                     Maybe SMTResult
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  -> ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO ThmResult)
-> (ThmResult -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
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 -> ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO ThmResult)
-> (ThmResult -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
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) -> ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO SatResult)
-> (SatResult -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
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
_           -> ProverCommand
-> (String -> IO ())
-> SMTConfig
-> (SMTConfig -> Symbolic SVal -> IO AllSatResult)
-> (AllSatResult -> [SMTResult])
-> Symbolic SVal
-> IO (Maybe String, [SMTResult])
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, Module
m) <- Bool -> ImportSource -> ModuleM (ModulePath, Module)
M.loadModuleFrom Bool
True (ModName -> ImportSource
M.FromModule ModName
preludeReferenceName)
              let decls :: [DeclGroup]
decls = Module -> [DeclGroup]
mDecls Module
m
              let nms :: [Name]
nms = (Name, IfaceDecl) -> Name
forall a b. (a, b) -> a
fst ((Name, IfaceDecl) -> Name) -> [(Name, IfaceDecl)] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name IfaceDecl -> [(Name, IfaceDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList (IfaceDecls -> Map Name IfaceDecl
M.ifDecls (Iface -> IfaceDecls
M.ifPublic (Module -> Iface
M.genIface Module
m)))
              let ds :: Map PrimIdent Expr
ds = [(PrimIdent, Expr)] -> Map PrimIdent Expr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Text -> PrimIdent
prelPrim (Ident -> Text
identText (Name -> Ident
M.nameIdent Name
nm)), Expr -> [DeclGroup] -> Expr
EWhere (Name -> Expr
EVar Name
nm) [DeclGroup]
decls) | Name
nm <- [Name]
nms ]
              Map PrimIdent Expr -> ModuleT IO (Map PrimIdent Expr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map PrimIdent Expr
ds

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

     Bool
callStacks <- ModuleT IO Bool
forall (m :: * -> *). Monad m => ModuleT m Bool
M.getCallStacks
     let ?callStacks = 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 -> Either String ([FinType], Symbolic SVal)
-> ModuleT IO (Either String ([FinType], Symbolic SVal))
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String ([FinType], Symbolic SVal)
forall a b. a -> Either a b
Left String
msg)
       Right [FinType]
ts -> IO (Either String ([FinType], Symbolic SVal))
-> ModuleT IO (Either String ([FinType], Symbolic SVal))
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
M.io (IO (Either String ([FinType], Symbolic SVal))
 -> ModuleT IO (Either String ([FinType], Symbolic SVal)))
-> IO (Either String ([FinType], Symbolic SVal))
-> ModuleT IO (Either String ([FinType], Symbolic SVal))
forall a b. (a -> b) -> a -> b
$
         do Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Logger -> String -> IO ()
logPutStrLn (EvalOpts -> Logger
Eval.evalLogger EvalOpts
evo) String
"Simulating..."
            Either String ([FinType], Symbolic SVal)
-> IO (Either String ([FinType], Symbolic SVal))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String ([FinType], Symbolic SVal)
 -> IO (Either String ([FinType], Symbolic SVal)))
-> Either String ([FinType], Symbolic SVal)
-> IO (Either String ([FinType], Symbolic SVal))
forall a b. (a -> b) -> a -> b
$ ([FinType], Symbolic SVal)
-> Either String ([FinType], Symbolic SVal)
forall a b. b -> Either a b
Right (([FinType], Symbolic SVal)
 -> Either String ([FinType], Symbolic SVal))
-> ([FinType], Symbolic SVal)
-> Either String ([FinType], Symbolic SVal)
forall a b. (a -> b) -> a -> b
$ ([FinType]
ts,
              do State
sbvState <- SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
SBV.symbolicEnv
                 MVar State
stateMVar <- IO (MVar State) -> SymbolicT IO (MVar State)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (State -> IO (MVar State)
forall a. a -> IO (MVar a)
newMVar State
sbvState)
                 MVar SVal
defRelsVar <- IO (MVar SVal) -> SymbolicT IO (MVar SVal)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (SVal -> IO (MVar SVal)
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 = \i -> (Right <$> Map.lookup i tbl) <|>
                                       (Left <$> Map.lookup i ds)
                 let ?range = emptyRange

                 -- Compute the symbolic inputs, and any domain constraints needed
                 -- according to their types.
                 [SBVEval (GenValue SBV)]
args <- (VarShape SBV -> SBVEval (GenValue SBV))
-> [VarShape SBV] -> [SBVEval (GenValue SBV)]
forall a b. (a -> b) -> [a] -> [b]
map (GenValue SBV -> SBVEval (GenValue SBV)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue SBV -> SBVEval (GenValue SBV))
-> (VarShape SBV -> GenValue SBV)
-> VarShape SBV
-> SBVEval (GenValue SBV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV -> VarShape SBV -> GenValue SBV
forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue SBV
sym) ([VarShape SBV] -> [SBVEval (GenValue SBV)])
-> SymbolicT IO [VarShape SBV]
-> SymbolicT IO [SBVEval (GenValue SBV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                     IO [VarShape SBV] -> SymbolicT IO [VarShape SBV]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ((FinType -> IO (VarShape SBV)) -> [FinType] -> IO [VarShape SBV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FreshVarFns SBV -> FinType -> IO (VarShape SBV)
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) <- SBVEval SVal -> SymbolicT IO (SVal, SVal)
forall (m :: * -> *) a. MonadIO m => SBVEval a -> m (SVal, a)
doSBVEval (SBVEval SVal -> SymbolicT IO (SVal, SVal))
-> SBVEval SVal -> SymbolicT IO (SVal, SVal)
forall a b. (a -> b) -> a -> b
$
                     do GenEvalEnv SBV
env <- SBV -> [DeclGroup] -> GenEvalEnv SBV -> SEval SBV (GenEvalEnv SBV)
forall sym.
EvalPrims sym =>
sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
Eval.evalDecls SBV
sym [DeclGroup]
extDgs (GenEvalEnv SBV -> SBVEval (GenEvalEnv SBV))
-> SBVEval (GenEvalEnv SBV) -> SBVEval (GenEvalEnv SBV)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                                 SBV
-> Map Name Newtype -> GenEvalEnv SBV -> SEval SBV (GenEvalEnv SBV)
forall sym.
EvalPrims sym =>
sym
-> Map Name Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
Eval.evalNewtypeDecls SBV
sym Map Name Newtype
ntEnv GenEvalEnv SBV
forall a. Monoid a => a
mempty
                        GenValue SBV
v <- SBV -> GenEvalEnv SBV -> Expr -> SEval SBV (GenValue SBV)
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 <- (GenValue SBV -> SBVEval (GenValue SBV) -> SBVEval (GenValue SBV))
-> GenValue SBV
-> [SBVEval (GenValue SBV)]
-> SBVEval (GenValue SBV)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (SBV
-> GenValue SBV
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
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 GenValue SBV -> SEval SBV ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
Eval.forceValue GenValue SBV
appliedVal
                               SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure SVal
SBV.svTrue
                          QueryType
_ -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue SBV -> SBit SBV
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.
                 String -> SBV Bool -> Symbolic ()
forall a. SymVal a => String -> SBV a -> Symbolic ()
SBV.sObserve String
"safety" (SVal -> SBV Bool
forall a. SVal -> SBV a
SBV.SBV SVal
safety' :: SBV.SBV Bool)

                 -- read any definitional relations that were asserted
                 SVal
defRels <- IO SVal -> Symbolic SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (MVar SVal -> IO SVal
forall a. MVar a -> IO a
readMVar MVar SVal
defRelsVar)

                 SVal -> Symbolic SVal
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 <- ((Bool, [(TValue, Expr, Value)]) -> [(TValue, Expr, Value)])
-> [(Bool, [(TValue, Expr, Value)])] -> [[(TValue, Expr, Value)]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, [(TValue, Expr, Value)]) -> [(TValue, Expr, Value)]
forall a b. (a, b) -> b
snd ([(Bool, [(TValue, Expr, Value)])] -> [[(TValue, Expr, Value)]])
-> ModuleT IO [(Bool, [(TValue, Expr, Value)])]
-> ModuleT IO [[(TValue, Expr, Value)]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SMTResult -> ModuleT IO (Bool, [(TValue, Expr, Value)]))
-> [SMTResult] -> ModuleT IO [(Bool, [(TValue, Expr, Value)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PrimMap -> SMTResult -> ModuleT IO (Bool, [(TValue, Expr, Value)])
forall (m :: * -> *).
Monad m =>
PrimMap -> SMTResult -> m (Bool, [(TValue, Expr, Value)])
mkTevs PrimMap
prims) [SMTResult]
results
         ProverResult -> ModuleT IO ProverResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ProverResult -> ModuleT IO ProverResult)
-> ProverResult -> ModuleT IO ProverResult
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) <- PrimMap -> SMTResult -> ModuleT IO (Bool, [(TValue, Expr, Value)])
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
         ProverResult -> ModuleT IO ProverResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ProverResult -> ModuleT IO ProverResult)
-> ProverResult -> ModuleT IO ProverResult
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 {}] ->
         ProverResult -> ModuleT IO ProverResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ProverResult -> ModuleT IO ProverResult)
-> ProverResult -> ModuleT IO ProverResult
forall a b. (a -> b) -> a -> b
$ [TValue] -> ProverResult
ThmResult (FinType -> TValue
unFinType (FinType -> TValue) -> [FinType] -> [TValue]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinType]
ts)

       -- unsat returns empty
       [] -> ProverResult -> ModuleT IO ProverResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ProverResult -> ModuleT IO ProverResult)
-> ProverResult -> ModuleT IO ProverResult
forall a b. (a -> b) -> a -> b
$ [TValue] -> ProverResult
ThmResult (FinType -> TValue
unFinType (FinType -> TValue) -> [FinType] -> [TValue]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinType]
ts)

       -- otherwise something is wrong
       [SMTResult]
_ -> ProverResult -> ModuleT IO ProverResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ProverResult -> ModuleT IO ProverResult)
-> ProverResult -> ModuleT IO ProverResult
forall a b. (a -> b) -> a -> b
$ String -> ProverResult
ProverError ([SMTResult] -> String
rshow [SMTResult]
results)
#if MIN_VERSION_sbv(8,8,0)
              where rshow :: [SMTResult] -> String
rshow | Bool
isSat = AllSatResult -> String
forall a. Show a => a -> String
show (AllSatResult -> String)
-> ([SMTResult] -> AllSatResult) -> [SMTResult] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Bool -> Bool -> Bool -> [SMTResult] -> AllSatResult
SBV.AllSatResult Bool
False Bool
False Bool
False Bool
False)
#else
              where rshow | isSat = show .  SBV.AllSatResult . (False,False,False,)
#endif
                          | Bool
otherwise = ThmResult -> String
forall a. Show a => a -> String
show (ThmResult -> String)
-> ([SMTResult] -> ThmResult) -> [SMTResult] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTResult -> ThmResult
SBV.ThmResult (SMTResult -> ThmResult)
-> ([SMTResult] -> SMTResult) -> [SMTResult] -> ThmResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SMTResult] -> SMTResult
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 Right (Bool
_, (CV
safetyCV : [CV]
cvs)) = SMTResult -> Either String (Bool, [CV])
SBV.getModelAssignment SMTResult
result
        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
    (Bool, [(TValue, Expr, Value)])
-> m (Bool, [(TValue, Expr, Value)])
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 =
  (String -> ModuleCmd (Maybe String, ProverResult))
-> ModuleCmd (Maybe String, ProverResult)
-> ModuleCmd (Maybe String, ProverResult)
forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack String -> ModuleCmd (Maybe String, ProverResult)
proverError (ModuleCmd (Maybe String, ProverResult)
 -> ModuleCmd (Maybe String, ProverResult))
-> ModuleCmd (Maybe String, ProverResult)
-> ModuleCmd (Maybe String, ProverResult)
forall a b. (a -> b) -> a -> b
$ \ModuleInput IO
minp ->
  ModuleInput IO
-> ModuleM (Maybe String, ProverResult)
-> IO
     (Either ModuleError ((Maybe String, ProverResult), ModuleEnv),
      [ModuleWarning])
forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM ModuleInput IO
minp (ModuleM (Maybe String, ProverResult)
 -> IO
      (Either ModuleError ((Maybe String, ProverResult), ModuleEnv),
       [ModuleWarning]))
-> ModuleM (Maybe String, ProverResult)
-> IO
     (Either ModuleError ((Maybe String, ProverResult), ModuleEnv),
      [ModuleWarning])
forall a b. (a -> b) -> a -> b
$ do
  EvalOpts
evo <- IO EvalOpts -> ModuleT IO EvalOpts
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (ModuleInput IO -> IO EvalOpts
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 ModuleT IO (Either String ([FinType], Symbolic SVal))
-> (Either String ([FinType], Symbolic SVal)
    -> ModuleM (Maybe String, ProverResult))
-> ModuleM (Maybe String, ProverResult)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left String
msg -> (Maybe String, ProverResult)
-> ModuleM (Maybe String, ProverResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
forall a. Maybe a
Nothing, String -> ProverResult
ProverError String
msg)
    Right ([FinType]
ts, Symbolic SVal
q) ->
      do (Maybe String
firstProver, [SMTResult]
results) <- IO (Maybe String, [SMTResult])
-> ModuleT IO (Maybe String, [SMTResult])
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
         (Maybe String, ProverResult)
-> ModuleM (Maybe String, ProverResult)
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
..} =
  (String -> ModuleCmd (Either String String))
-> ModuleCmd (Either String String)
-> ModuleCmd (Either String String)
forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack (\String
msg ModuleInput IO
minp -> (Either ModuleError (Either String String, ModuleEnv),
 [ModuleWarning])
-> IO
     (Either ModuleError (Either String String, ModuleEnv),
      [ModuleWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Either String String, ModuleEnv)
-> Either ModuleError (Either String String, ModuleEnv)
forall a b. b -> Either a b
Right (String -> Either String String
forall a b. a -> Either a b
Left String
msg, ModuleInput IO -> ModuleEnv
forall (m :: * -> *). ModuleInput m -> ModuleEnv
M.minpModuleEnv ModuleInput IO
minp), [])) (ModuleCmd (Either String String)
 -> ModuleCmd (Either String String))
-> ModuleCmd (Either String String)
-> ModuleCmd (Either String String)
forall a b. (a -> b) -> a -> b
$
  \ModuleInput IO
minp -> ModuleInput IO
-> ModuleM (Either String String)
-> IO
     (Either ModuleError (Either String String, ModuleEnv),
      [ModuleWarning])
forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM ModuleInput IO
minp (ModuleM (Either String String)
 -> IO
      (Either ModuleError (Either String String, ModuleEnv),
       [ModuleWarning]))
-> ModuleM (Either String String)
-> IO
     (Either ModuleError (Either String String, ModuleEnv),
      [ModuleWarning])
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
        EvalOpts
evo <- IO EvalOpts -> ModuleT IO EvalOpts
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (ModuleInput IO -> IO EvalOpts
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 ModuleT IO (Either String ([FinType], Symbolic SVal))
-> (Either String ([FinType], Symbolic SVal)
    -> ModuleM (Either String String))
-> ModuleM (Either String String)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Left String
msg -> Either String String -> ModuleM (Either String String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String String
forall a b. a -> Either a b
Left String
msg)
          Right ([FinType]
_ts, Symbolic SVal
q) -> String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String)
-> ModuleT IO String -> ModuleM (Either String String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String -> ModuleT IO String
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
M.io (Bool -> Symbolic SVal -> IO String
SBV.generateSMTBenchmark Bool
isSat Symbolic SVal
q)

protectStack :: (String -> M.ModuleCmd a)
             -> M.ModuleCmd a
             -> M.ModuleCmd a
protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack String -> ModuleCmd a
mkErr ModuleCmd a
cmd ModuleInput IO
modEnv =
  (AsyncException -> Maybe ())
-> IO (ModuleRes a) -> (() -> IO (ModuleRes a)) -> IO (ModuleRes a)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
X.catchJust AsyncException -> Maybe ()
isOverflow (ModuleCmd a
cmd ModuleInput IO
modEnv) () -> IO (ModuleRes a)
handler
  where isOverflow :: AsyncException -> Maybe ()
isOverflow AsyncException
X.StackOverflow = () -> Maybe ()
forall a. a -> Maybe a
Just ()
        isOverflow AsyncException
_               = Maybe ()
forall a. Maybe a
Nothing
        msg :: String
msg = String
"Symbolic evaluation failed to terminate."
        handler :: () -> IO (ModuleRes a)
handler () = String -> ModuleCmd a
mkErr String
msg 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 VarShape Concrete -> [VarShape Concrete] -> [VarShape Concrete]
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 [] = String -> [String] -> (VarShape Concrete, [CV])
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Symbolic.parseValue" [ String
"empty FTBit" ]
parseValue FinType
FTBit (CV
cv : [CV]
cvs) = (SBit Concrete -> VarShape Concrete
forall sym. SBit sym -> VarShape sym
VarBit (CV -> Bool
SBV.cvToBool CV
cv), [CV]
cvs)
parseValue FinType
FTInteger [CV]
cvs =
  case Kind -> [CV] -> Maybe (Integer, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
SBV.genParse Kind
SBV.KUnbounded [CV]
cvs of
    Just (Integer
x, [CV]
cvs') -> (SInteger Concrete -> VarShape Concrete
forall sym. SInteger sym -> VarShape sym
VarInteger Integer
SInteger Concrete
x, [CV]
cvs')
    Maybe (Integer, [CV])
Nothing        -> String -> [String] -> (VarShape Concrete, [CV])
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 =
  (VarShape Concrete, [CV])
-> Maybe (VarShape Concrete, [CV]) -> (VarShape Concrete, [CV])
forall a. a -> Maybe a -> a
fromMaybe (String -> [String] -> (VarShape Concrete, [CV])
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Symbolic.parseValue" [String
"no rational"]) (Maybe (VarShape Concrete, [CV]) -> (VarShape Concrete, [CV]))
-> Maybe (VarShape Concrete, [CV]) -> (VarShape Concrete, [CV])
forall a b. (a -> b) -> a -> b
$
  do (Integer
n,[CV]
cvs')  <- Kind -> [CV] -> Maybe (Integer, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
SBV.genParse Kind
SBV.KUnbounded [CV]
cvs
     (Integer
d,[CV]
cvs'') <- Kind -> [CV] -> Maybe (Integer, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
SBV.genParse Kind
SBV.KUnbounded [CV]
cvs'
     (VarShape Concrete, [CV]) -> Maybe (VarShape Concrete, [CV])
forall (m :: * -> *) a. Monad m => a -> m a
return (SInteger Concrete -> SInteger Concrete -> VarShape Concrete
forall sym. SInteger sym -> SInteger sym -> VarShape sym
VarRational Integer
SInteger Concrete
n Integer
SInteger Concrete
d, [CV]
cvs'')
parseValue (FTSeq Integer
0 FinType
FTBit) [CV]
cvs = (SWord Concrete -> VarShape Concrete
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 Kind -> [CV] -> Maybe (Integer, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
SBV.genParse (Bool -> Int -> Kind
SBV.KBounded Bool
False (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)) [CV]
cvs of
    Just (Integer
x, [CV]
cvs') -> (SWord Concrete -> VarShape Concrete
forall sym. SWord sym -> VarShape sym
VarWord (Integer -> Integer -> BV
Concrete.mkBv (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
n) Integer
x), [CV]
cvs')
    Maybe (Integer, [CV])
Nothing -> String -> [String] -> (VarShape Concrete, [CV])
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Symbolic.parseValue" [String
"no bitvector"]
parseValue (FTSeq Integer
n FinType
t) [CV]
cvs = (Integer -> [VarShape Concrete] -> VarShape Concrete
forall sym. Integer -> [VarShape sym] -> VarShape sym
VarFinSeq (Integer -> Integer
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 (Int -> FinType -> [FinType]
forall a. Int -> a -> [a]
replicate (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) FinType
t) [CV]
cvs
parseValue (FTTuple [FinType]
ts) [CV]
cvs = ([VarShape Concrete] -> VarShape Concrete
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 = (RecordMap Ident (VarShape Concrete) -> VarShape Concrete
forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
VarRecord RecordMap Ident (VarShape Concrete)
r', [CV]
cvs')
  where ([Ident]
ns, [FinType]
ts)   = [(Ident, FinType)] -> ([Ident], [FinType])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Ident, FinType)] -> ([Ident], [FinType]))
-> [(Ident, FinType)] -> ([Ident], [FinType])
forall a b. (a -> b) -> a -> b
$ RecordMap Ident FinType -> [(Ident, FinType)]
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         = [Ident] -> [VarShape Concrete] -> [(Ident, VarShape Concrete)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
ns [VarShape Concrete]
vs
        r' :: RecordMap Ident (VarShape Concrete)
r'         = [Ident]
-> [(Ident, VarShape Concrete)]
-> RecordMap Ident (VarShape Concrete)
forall a b. (Show a, Ord a) => [a] -> [(a, b)] -> RecordMap a b
recordFromFieldsWithDisplay (RecordMap Ident FinType -> [Ident]
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 =
   (SFloat Concrete -> VarShape Concrete
forall sym. SFloat sym -> VarShape sym
VarFloat BF :: Integer -> Integer -> BigFloat -> BF
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 -> () -> IO ()
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 -> () -> IO ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
     SVal -> IO SVal
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 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = SVal -> IO SVal
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 (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
w)

sbvFreshFns :: SBV -> FreshVarFns SBV
sbvFreshFns :: SBV -> FreshVarFns SBV
sbvFreshFns SBV
sym =
  FreshVarFns :: forall sym.
IO (SBit sym)
-> (Integer -> IO (SWord sym))
-> (Maybe Integer -> Maybe Integer -> IO (SInteger sym))
-> (Integer -> Integer -> IO (SFloat sym))
-> FreshVarFns sym
FreshVarFns
  { freshBitVar :: IO (SBit 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
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- TODO
  }