{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Symbolic where
import Control.Monad.IO.Class
import Control.Monad (replicateM, when, zipWithM, foldM)
import Control.Monad.Writer (WriterT, runWriterT, tell, lift)
import Data.List (intercalate, genericLength)
import Data.IORef(IORef)
import qualified Control.Exception as X
import qualified Data.SBV.Dynamic as SBV
import Data.SBV (Timing(SaveTiming))
import Data.SBV.Internals (showTDiff)
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 Cryptol.Symbolic.Prims
import Cryptol.Symbolic.Value
import qualified Cryptol.Eval as Eval
import qualified Cryptol.Eval.Monad as Eval
import qualified Cryptol.Eval.Type as Eval
import qualified Cryptol.Eval.Value as Eval
import Cryptol.Eval.Env (GenEvalEnv(..))
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Ident (Ident)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Logger(logPutStrLn)
import Prelude ()
import Prelude.Compat
import Data.Time (NominalDiffTime)
type EvalEnv = GenEvalEnv SBool SWord
proverConfigs :: [(String, SBV.SMTConfig)]
proverConfigs :: [(String, SMTConfig)]
proverConfigs =
[ ("cvc4" , SMTConfig
SBV.cvc4 )
, ("yices" , SMTConfig
SBV.yices )
, ("z3" , SMTConfig
SBV.z3 )
, ("boolector", SMTConfig
SBV.boolector)
, ("mathsat" , SMTConfig
SBV.mathSAT )
, ("abc" , SMTConfig
SBV.abc )
, ("offline" , SMTConfig
SBV.defaultSMTCfg )
, ("any" , SMTConfig
SBV.defaultSMTCfg )
]
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
lookupProver :: String -> SBV.SMTConfig
lookupProver :: String -> SMTConfig
lookupProver s :: String
s =
case String -> [(String, SMTConfig)] -> Maybe SMTConfig
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
s [(String, SMTConfig)]
proverConfigs of
Just cfg :: SMTConfig
cfg -> SMTConfig
cfg
Nothing -> String -> [String] -> SMTConfig
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.Symbolic" [ "invalid prover: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s ]
type SatResult = [(Type, Expr, Eval.Value)]
data SatNum = AllSat | SomeSat Int
deriving (Int -> SatNum -> String -> String
[SatNum] -> String -> String
SatNum -> String
(Int -> SatNum -> String -> String)
-> (SatNum -> String)
-> ([SatNum] -> String -> String)
-> Show SatNum
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [SatNum] -> String -> String
$cshowList :: [SatNum] -> String -> String
show :: SatNum -> String
$cshow :: SatNum -> String
showsPrec :: Int -> SatNum -> String -> String
$cshowsPrec :: Int -> SatNum -> String -> String
Show)
data QueryType = SatQuery SatNum | ProveQuery
deriving (Int -> QueryType -> String -> String
[QueryType] -> String -> String
QueryType -> String
(Int -> QueryType -> String -> String)
-> (QueryType -> String)
-> ([QueryType] -> String -> String)
-> Show QueryType
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [QueryType] -> String -> String
$cshowList :: [QueryType] -> String -> String
show :: QueryType -> String
$cshow :: QueryType -> String
showsPrec :: Int -> QueryType -> String -> String
$cshowsPrec :: Int -> QueryType -> String -> String
Show)
data ProverCommand = ProverCommand {
ProverCommand -> QueryType
pcQueryType :: QueryType
, ProverCommand -> String
pcProverName :: String
, ProverCommand -> Bool
pcVerbose :: Bool
, ProverCommand -> Bool
pcValidate :: Bool
, ProverCommand -> IORef ProverStats
pcProverStats :: !(IORef ProverStats)
, :: [DeclGroup]
, ProverCommand -> Maybe String
pcSmtFile :: Maybe FilePath
, ProverCommand -> Expr
pcExpr :: Expr
, ProverCommand -> Schema
pcSchema :: Schema
}
type ProverStats = NominalDiffTime
data ProverResult = AllSatResult [SatResult]
| ThmResult [Type]
| EmptyResult
| ProverError String
satSMTResults :: SBV.SatResult -> [SBV.SMTResult]
satSMTResults :: SatResult -> [SMTResult]
satSMTResults (SBV.SatResult r :: SMTResult
r) = [SMTResult
r]
allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult]
allSatSMTResults :: AllSatResult -> [SMTResult]
allSatSMTResults (SBV.AllSatResult (_, _, _, rs :: [SMTResult]
rs)) = [SMTResult]
rs
thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult]
thmSMTResults :: ThmResult -> [SMTResult]
thmSMTResults (SBV.ThmResult r :: SMTResult
r) = [SMTResult
r]
proverError :: String -> M.ModuleCmd (Maybe SBV.Solver, ProverResult)
proverError :: String -> ModuleCmd (Maybe Solver, ProverResult)
proverError msg :: String
msg (_,modEnv :: ModuleEnv
modEnv) =
(Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv),
[ModuleWarning])
-> IO
(Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv),
[ModuleWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return (((Maybe Solver, ProverResult), ModuleEnv)
-> Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv)
forall a b. b -> Either a b
Right ((Maybe Solver
forall a. Maybe a
Nothing, String -> ProverResult
ProverError String
msg), ModuleEnv
modEnv), [])
satProve :: ProverCommand -> M.ModuleCmd (Maybe SBV.Solver, ProverResult)
satProve :: ProverCommand -> ModuleCmd (Maybe Solver, ProverResult)
satProve ProverCommand {..} =
(String -> ModuleCmd (Maybe Solver, ProverResult))
-> ModuleCmd (Maybe Solver, ProverResult)
-> ModuleCmd (Maybe Solver, ProverResult)
forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack String -> ModuleCmd (Maybe Solver, ProverResult)
proverError (ModuleCmd (Maybe Solver, ProverResult)
-> ModuleCmd (Maybe Solver, ProverResult))
-> ModuleCmd (Maybe Solver, ProverResult)
-> ModuleCmd (Maybe Solver, ProverResult)
forall a b. (a -> b) -> a -> b
$ \(evo :: EvalOpts
evo,modEnv :: ModuleEnv
modEnv) ->
(EvalOpts, ModuleEnv)
-> ModuleM (Maybe Solver, ProverResult)
-> IO
(Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv),
[ModuleWarning])
forall a.
(EvalOpts, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM (EvalOpts
evo,ModuleEnv
modEnv) (ModuleM (Maybe Solver, ProverResult)
-> IO
(Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv),
[ModuleWarning]))
-> ModuleM (Maybe Solver, ProverResult)
-> IO
(Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv),
[ModuleWarning])
forall a b. (a -> b) -> a -> b
$ do
let (isSat :: Bool
isSat, mSatNum :: Maybe Int
mSatNum) = case QueryType
pcQueryType of
ProveQuery -> (Bool
False, Maybe Int
forall a. Maybe a
Nothing)
SatQuery sn :: SatNum
sn -> case SatNum
sn of
SomeSat n :: Int
n -> (Bool
True, Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n)
AllSat -> (Bool
True, Maybe Int
forall a. Maybe a
Nothing)
let extDgs :: [DeclGroup]
extDgs = ModuleEnv -> [DeclGroup]
allDeclGroups ModuleEnv
modEnv [DeclGroup] -> [DeclGroup] -> [DeclGroup]
forall a. [a] -> [a] -> [a]
++ [DeclGroup]
pcExtraDecls
[SMTConfig]
provers <-
case String
pcProverName of
"any" -> IO [SMTConfig] -> ModuleT IO [SMTConfig]
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
M.io IO [SMTConfig]
SBV.sbvAvailableSolvers
_ -> [SMTConfig] -> ModuleT IO [SMTConfig]
forall (m :: * -> *) a. Monad m => a -> m a
return [(String -> SMTConfig
lookupProver String
pcProverName) { transcript :: Maybe String
SBV.transcript = Maybe String
pcSmtFile
, allSatMaxModelCount :: Maybe Int
SBV.allSatMaxModelCount = Maybe Int
mSatNum
}]
let provers' :: [SMTConfig]
provers' = [ SMTConfig
p { 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]
provers ]
let tyFn :: FinType -> WriterT [SBool] Symbolic Value
tyFn = if Bool
isSat then FinType -> WriterT [SBool] Symbolic Value
existsFinType else FinType -> WriterT [SBool] Symbolic Value
forallFinType
let lPutStrLn :: String -> ModuleM ()
lPutStrLn = (Logger -> String -> IO ()) -> String -> ModuleM ()
forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
M.withLogger Logger -> String -> IO ()
logPutStrLn
let doEval :: MonadIO m => Eval.Eval a -> m a
doEval :: Eval a -> m a
doEval m :: Eval a
m = IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$ EvalOpts -> Eval a -> IO a
forall a. EvalOpts -> Eval a -> IO a
Eval.runEval EvalOpts
evo Eval a
m
let runProver :: (SMTConfig -> t -> IO t)
-> (t -> [SMTResult])
-> t
-> ModuleT IO (Maybe Solver, [SMTResult])
runProver fn :: SMTConfig -> t -> IO t
fn tag :: t -> [SMTResult]
tag e :: t
e = do
case [SMTConfig]
provers of
[prover :: SMTConfig
prover] -> do
Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
forall a b. (a -> b) -> a -> b
$
String -> ModuleM ()
lPutStrLn (String -> ModuleM ()) -> String -> ModuleM ()
forall a b. (a -> b) -> a -> b
$ "Trying proof with " String -> String -> String
forall a. [a] -> [a] -> [a]
++
Solver -> String
forall a. Show a => a -> String
show (SMTSolver -> Solver
SBV.name (SMTConfig -> SMTSolver
SBV.solver SMTConfig
prover))
t
res <- IO t -> ModuleT IO t
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
M.io (SMTConfig -> t -> IO t
fn SMTConfig
prover t
e)
Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
forall a b. (a -> b) -> a -> b
$
String -> ModuleM ()
lPutStrLn (String -> ModuleM ()) -> String -> ModuleM ()
forall a b. (a -> b) -> a -> b
$ "Got result from " String -> String -> String
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 Solver, [SMTResult])
-> ModuleT IO (Maybe Solver, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Solver -> Maybe Solver
forall a. a -> Maybe a
Just (SMTSolver -> Solver
SBV.name (SMTConfig -> SMTSolver
SBV.solver SMTConfig
prover)), t -> [SMTResult]
tag t
res)
_ ->
(Maybe Solver, [SMTResult])
-> ModuleT IO (Maybe Solver, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return ( Maybe Solver
forall a. Maybe a
Nothing
, [ SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
SBV.ProofError
SMTConfig
prover
[":sat with option prover=any requires option satNum=1"]
Maybe SMTResult
forall a. Maybe a
Nothing
| SMTConfig
prover <- [SMTConfig]
provers ]
)
runProvers :: ([SMTConfig] -> t -> IO (a, ProverStats, t))
-> (t -> b) -> t -> ModuleT IO (Maybe a, b)
runProvers fn :: [SMTConfig] -> t -> IO (a, ProverStats, t)
fn tag :: t -> b
tag e :: t
e = do
Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
forall a b. (a -> b) -> a -> b
$
String -> ModuleM ()
lPutStrLn (String -> ModuleM ()) -> String -> ModuleM ()
forall a b. (a -> b) -> a -> b
$ "Trying proof with " String -> String -> String
forall a. [a] -> [a] -> [a]
++
String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ((SMTConfig -> String) -> [SMTConfig] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Solver -> String
forall a. Show a => a -> String
show (Solver -> String) -> (SMTConfig -> Solver) -> SMTConfig -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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]
provers)
(firstProver :: a
firstProver, timeElapsed :: ProverStats
timeElapsed, res :: t
res) <- IO (a, ProverStats, t) -> ModuleT IO (a, ProverStats, t)
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
M.io ([SMTConfig] -> t -> IO (a, ProverStats, t)
fn [SMTConfig]
provers' t
e)
Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
forall a b. (a -> b) -> a -> b
$
String -> ModuleM ()
lPutStrLn (String -> ModuleM ()) -> String -> ModuleM ()
forall a b. (a -> b) -> a -> b
$ "Got result from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
firstProver String -> String -> String
forall a. [a] -> [a] -> [a]
++
", time: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ProverStats -> String
showTDiff ProverStats
timeElapsed
(Maybe a, b) -> ModuleT IO (Maybe a, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Maybe a
forall a. a -> Maybe a
Just a
firstProver, t -> b
tag t
res)
let runFn :: Symbolic SBool -> ModuleT IO (Maybe Solver, [SMTResult])
runFn = case QueryType
pcQueryType of
ProveQuery -> ([SMTConfig]
-> Symbolic SBool -> IO (Solver, ProverStats, ThmResult))
-> (ThmResult -> [SMTResult])
-> Symbolic SBool
-> ModuleT IO (Maybe Solver, [SMTResult])
forall a t t b.
Show a =>
([SMTConfig] -> t -> IO (a, ProverStats, t))
-> (t -> b) -> t -> ModuleT IO (Maybe a, b)
runProvers [SMTConfig]
-> Symbolic SBool -> IO (Solver, ProverStats, ThmResult)
SBV.proveWithAny ThmResult -> [SMTResult]
thmSMTResults
SatQuery sn :: SatNum
sn -> case SatNum
sn of
SomeSat 1 -> ([SMTConfig]
-> Symbolic SBool -> IO (Solver, ProverStats, SatResult))
-> (SatResult -> [SMTResult])
-> Symbolic SBool
-> ModuleT IO (Maybe Solver, [SMTResult])
forall a t t b.
Show a =>
([SMTConfig] -> t -> IO (a, ProverStats, t))
-> (t -> b) -> t -> ModuleT IO (Maybe a, b)
runProvers [SMTConfig]
-> Symbolic SBool -> IO (Solver, ProverStats, SatResult)
SBV.satWithAny SatResult -> [SMTResult]
satSMTResults
_ -> (SMTConfig -> Symbolic SBool -> IO AllSatResult)
-> (AllSatResult -> [SMTResult])
-> Symbolic SBool
-> ModuleT IO (Maybe Solver, [SMTResult])
forall t t.
(SMTConfig -> t -> IO t)
-> (t -> [SMTResult])
-> t
-> ModuleT IO (Maybe Solver, [SMTResult])
runProver SMTConfig -> Symbolic SBool -> IO AllSatResult
SBV.allSatWith AllSatResult -> [SMTResult]
allSatSMTResults
let addAsm :: SBool -> SBool -> SBool
addAsm = case QueryType
pcQueryType of
ProveQuery -> \x :: SBool
x y :: SBool
y -> SBool -> SBool -> SBool
SBV.svOr (SBool -> SBool
SBV.svNot SBool
x) SBool
y
SatQuery _ -> \x :: SBool
x y :: SBool
y -> SBool -> SBool -> SBool
SBV.svAnd SBool
x SBool
y
case Schema -> Either String [FinType]
predArgTypes Schema
pcSchema of
Left msg :: String
msg -> (Maybe Solver, ProverResult)
-> ModuleM (Maybe Solver, ProverResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Solver
forall a. Maybe a
Nothing, String -> ProverResult
ProverError String
msg)
Right ts :: [FinType]
ts -> do Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pcVerbose (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
forall a b. (a -> b) -> a -> b
$ String -> ModuleM ()
lPutStrLn "Simulating..."
Value
v <- Eval Value -> ModuleT IO Value
forall (m :: * -> *) a. MonadIO m => Eval a -> m a
doEval (Eval Value -> ModuleT IO Value) -> Eval Value -> ModuleT IO Value
forall a b. (a -> b) -> a -> b
$ do GenEvalEnv SBool SBool SBool
env <- [DeclGroup]
-> GenEvalEnv SBool SBool SBool
-> Eval (GenEvalEnv SBool SBool SBool)
forall b w i.
EvalPrims b w i =>
[DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
Eval.evalDecls [DeclGroup]
extDgs GenEvalEnv SBool SBool SBool
forall a. Monoid a => a
mempty
GenEvalEnv SBool SBool SBool -> Expr -> Eval Value
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
Eval.evalExpr GenEvalEnv SBool SBool SBool
env Expr
pcExpr
PrimMap
prims <- ModuleM PrimMap
M.getPrimMap
(Maybe Solver, [SMTResult])
runRes <- Symbolic SBool -> ModuleT IO (Maybe Solver, [SMTResult])
runFn (Symbolic SBool -> ModuleT IO (Maybe Solver, [SMTResult]))
-> Symbolic SBool -> ModuleT IO (Maybe Solver, [SMTResult])
forall a b. (a -> b) -> a -> b
$ do
(args :: [Value]
args, asms :: [SBool]
asms) <- WriterT [SBool] Symbolic [Value] -> Symbolic ([Value], [SBool])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT ((FinType -> WriterT [SBool] Symbolic Value)
-> [FinType] -> WriterT [SBool] Symbolic [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM FinType -> WriterT [SBool] Symbolic Value
tyFn [FinType]
ts)
SBool
b <- Eval SBool -> Symbolic SBool
forall (m :: * -> *) a. MonadIO m => Eval a -> m a
doEval (Value -> SBool
forall b w i. GenValue b w i -> b
fromVBit (Value -> SBool) -> Eval Value -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(Value -> Eval Value -> Eval Value)
-> Value -> [Eval Value] -> Eval Value
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Value -> Eval Value -> Eval Value
forall b w i.
GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
fromVFun Value
v ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
Eval.ready [Value]
args))
SBool -> Symbolic SBool
forall (m :: * -> *) a. Monad m => a -> m a
return ((SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SBool -> SBool -> SBool
addAsm SBool
b [SBool]
asms)
let (firstProver :: Maybe Solver
firstProver, results :: [SMTResult]
results) = (Maybe Solver, [SMTResult])
runRes
ProverResult
esatexprs <- case [SMTResult]
results of
(SBV.Satisfiable {} : _) -> do
[[(Type, Expr, Value)]]
tevss <- (SMTResult -> ModuleT IO [(Type, Expr, Value)])
-> [SMTResult] -> ModuleT IO [[(Type, Expr, Value)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SMTResult -> ModuleT IO [(Type, Expr, Value)]
forall (m :: * -> *).
MonadIO m =>
SMTResult -> m [(Type, Expr, Value)]
mkTevs [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
$ [[(Type, Expr, Value)]] -> ProverResult
AllSatResult [[(Type, Expr, Value)]]
tevss
where
mkTevs :: SMTResult -> m [(Type, Expr, Value)]
mkTevs result :: SMTResult
result = do
let Right (_, cvs :: [CV]
cvs) = SMTResult -> Either String (Bool, [CV])
SBV.getModelAssignment SMTResult
result
(vs :: [Value]
vs, _) = [FinType] -> [CV] -> ([Value], [CV])
parseValues [FinType]
ts [CV]
cvs
sattys :: [Type]
sattys = FinType -> Type
unFinType (FinType -> Type) -> [FinType] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinType]
ts
[Maybe Expr]
satexprs <-
Eval [Maybe Expr] -> m [Maybe Expr]
forall (m :: * -> *) a. MonadIO m => Eval a -> m a
doEval ((Type -> Value -> Eval (Maybe Expr))
-> [Type] -> [Value] -> Eval [Maybe Expr]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (PrimMap -> Type -> Value -> Eval (Maybe Expr)
Eval.toExpr PrimMap
prims) [Type]
sattys [Value]
vs)
case [Type] -> [Expr] -> [Value] -> [(Type, Expr, Value)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Type]
sattys ([Expr] -> [Value] -> [(Type, Expr, Value)])
-> Maybe [Expr] -> Maybe ([Value] -> [(Type, Expr, Value)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Maybe Expr] -> Maybe [Expr]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe Expr]
satexprs) Maybe ([Value] -> [(Type, Expr, Value)])
-> Maybe [Value] -> Maybe [(Type, Expr, Value)]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Value] -> Maybe [Value]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
vs of
Nothing ->
String -> [String] -> m [(Type, Expr, Value)]
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.Symbolic.sat"
[ "unable to make assignment into expression" ]
Just tevs :: [(Type, Expr, Value)]
tevs -> [(Type, Expr, Value)] -> m [(Type, Expr, Value)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Type, Expr, Value)] -> m [(Type, Expr, Value)])
-> [(Type, Expr, Value)] -> m [(Type, Expr, Value)]
forall a b. (a -> b) -> a -> b
$ [(Type, Expr, Value)]
tevs
[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
$ [Type] -> ProverResult
ThmResult (FinType -> Type
unFinType (FinType -> Type) -> [FinType] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinType]
ts)
[] -> 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
$ [Type] -> ProverResult
ThmResult (FinType -> Type
unFinType (FinType -> Type) -> [FinType] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinType]
ts)
_ -> 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)
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, [SMTResult]) -> AllSatResult
SBV.AllSatResult ((Bool, Bool, Bool, [SMTResult]) -> AllSatResult)
-> ([SMTResult] -> (Bool, Bool, Bool, [SMTResult]))
-> [SMTResult]
-> AllSatResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool
False,Bool
False,Bool
False,)
| 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
(Maybe Solver, ProverResult)
-> ModuleM (Maybe Solver, ProverResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Solver
firstProver, ProverResult
esatexprs)
satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String)
satProveOffline :: ProverCommand -> ModuleCmd (Either String String)
satProveOffline ProverCommand {..} =
(String -> ModuleCmd (Either String String))
-> ModuleCmd (Either String String)
-> ModuleCmd (Either String String)
forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack (\msg :: String
msg (_,modEnv :: ModuleEnv
modEnv) -> (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, ModuleEnv
modEnv), [])) (ModuleCmd (Either String String)
-> ModuleCmd (Either String String))
-> ModuleCmd (Either String String)
-> ModuleCmd (Either String String)
forall a b. (a -> b) -> a -> b
$
\(evOpts :: EvalOpts
evOpts,modEnv :: ModuleEnv
modEnv) -> do
let isSat :: Bool
isSat = case QueryType
pcQueryType of
ProveQuery -> Bool
False
SatQuery _ -> Bool
True
let extDgs :: [DeclGroup]
extDgs = ModuleEnv -> [DeclGroup]
allDeclGroups ModuleEnv
modEnv [DeclGroup] -> [DeclGroup] -> [DeclGroup]
forall a. [a] -> [a] -> [a]
++ [DeclGroup]
pcExtraDecls
let tyFn :: FinType -> WriterT [SBool] Symbolic Value
tyFn = if Bool
isSat then FinType -> WriterT [SBool] Symbolic Value
existsFinType else FinType -> WriterT [SBool] Symbolic Value
forallFinType
let addAsm :: SBool -> SBool -> SBool
addAsm = if Bool
isSat then SBool -> SBool -> SBool
SBV.svAnd else \x :: SBool
x y :: SBool
y -> SBool -> SBool -> SBool
SBV.svOr (SBool -> SBool
SBV.svNot SBool
x) SBool
y
case Schema -> Either String [FinType]
predArgTypes Schema
pcSchema of
Left msg :: String
msg -> (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, ModuleEnv
modEnv), [])
Right ts :: [FinType]
ts ->
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
evOpts) "Simulating..."
Value
v <- IO Value -> IO Value
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Value -> IO Value) -> IO Value -> IO Value
forall a b. (a -> b) -> a -> b
$ EvalOpts -> Eval Value -> IO Value
forall a. EvalOpts -> Eval a -> IO a
Eval.runEval EvalOpts
evOpts (Eval Value -> IO Value) -> Eval Value -> IO Value
forall a b. (a -> b) -> a -> b
$
do GenEvalEnv SBool SBool SBool
env <- [DeclGroup]
-> GenEvalEnv SBool SBool SBool
-> Eval (GenEvalEnv SBool SBool SBool)
forall b w i.
EvalPrims b w i =>
[DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
Eval.evalDecls [DeclGroup]
extDgs GenEvalEnv SBool SBool SBool
forall a. Monoid a => a
mempty
GenEvalEnv SBool SBool SBool -> Expr -> Eval Value
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
Eval.evalExpr GenEvalEnv SBool SBool SBool
env Expr
pcExpr
String
smtlib <- Bool -> Symbolic SBool -> IO String
SBV.generateSMTBenchmark Bool
isSat (Symbolic SBool -> IO String) -> Symbolic SBool -> IO String
forall a b. (a -> b) -> a -> b
$ do
(args :: [Value]
args, asms :: [SBool]
asms) <- WriterT [SBool] Symbolic [Value] -> Symbolic ([Value], [SBool])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT ((FinType -> WriterT [SBool] Symbolic Value)
-> [FinType] -> WriterT [SBool] Symbolic [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM FinType -> WriterT [SBool] Symbolic Value
tyFn [FinType]
ts)
SBool
b <- IO SBool -> Symbolic SBool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBool -> Symbolic SBool) -> IO SBool -> Symbolic SBool
forall a b. (a -> b) -> a -> b
$ EvalOpts -> Eval SBool -> IO SBool
forall a. EvalOpts -> Eval a -> IO a
Eval.runEval EvalOpts
evOpts
(Value -> SBool
forall b w i. GenValue b w i -> b
fromVBit (Value -> SBool) -> Eval Value -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Eval Value -> Eval Value)
-> Value -> [Eval Value] -> Eval Value
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Value -> Eval Value -> Eval Value
forall b w i.
GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
fromVFun Value
v ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
Eval.ready [Value]
args))
SBool -> Symbolic SBool
forall (m :: * -> *) a. Monad m => a -> m a
return ((SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SBool -> SBool -> SBool
addAsm SBool
b [SBool]
asms)
(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. b -> Either a b
Right String
smtlib, ModuleEnv
modEnv), [])
protectStack :: (String -> M.ModuleCmd a)
-> M.ModuleCmd a
-> M.ModuleCmd a
protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
protectStack mkErr :: String -> ModuleCmd a
mkErr cmd :: ModuleCmd a
cmd modEnv :: (EvalOpts, ModuleEnv)
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 (EvalOpts, ModuleEnv)
modEnv) () -> IO (ModuleRes a)
handler
where isOverflow :: AsyncException -> Maybe ()
isOverflow X.StackOverflow = () -> Maybe ()
forall a. a -> Maybe a
Just ()
isOverflow _ = Maybe ()
forall a. Maybe a
Nothing
msg :: String
msg = "Symbolic evaluation failed to terminate."
handler :: () -> IO (ModuleRes a)
handler () = String -> ModuleCmd a
mkErr String
msg (EvalOpts, ModuleEnv)
modEnv
parseValues :: [FinType] -> [SBV.CV] -> ([Eval.Value], [SBV.CV])
parseValues :: [FinType] -> [CV] -> ([Value], [CV])
parseValues [] cvs :: [CV]
cvs = ([], [CV]
cvs)
parseValues (t :: FinType
t : ts :: [FinType]
ts) cvs :: [CV]
cvs = (Value
v Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: [Value]
vs, [CV]
cvs'')
where (v :: Value
v, cvs' :: [CV]
cvs') = FinType -> [CV] -> (Value, [CV])
parseValue FinType
t [CV]
cvs
(vs :: [Value]
vs, cvs'' :: [CV]
cvs'') = [FinType] -> [CV] -> ([Value], [CV])
parseValues [FinType]
ts [CV]
cvs'
parseValue :: FinType -> [SBV.CV] -> (Eval.Value, [SBV.CV])
parseValue :: FinType -> [CV] -> (Value, [CV])
parseValue FTBit [] = String -> [String] -> (Value, [CV])
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ]
parseValue FTBit (cv :: CV
cv : cvs :: [CV]
cvs) = (Bool -> Value
forall b w i. b -> GenValue b w i
Eval.VBit (CV -> Bool
SBV.cvToBool CV
cv), [CV]
cvs)
parseValue FTInteger cvs :: [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 (x :: Integer
x, cvs' :: [CV]
cvs') -> (Integer -> Value
forall b w i. i -> GenValue b w i
Eval.VInteger Integer
x, [CV]
cvs')
Nothing -> String -> [String] -> (Value, [CV])
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.Symbolic.parseValue" [ "no integer" ]
parseValue (FTIntMod _) cvs :: [CV]
cvs = FinType -> [CV] -> (Value, [CV])
parseValue FinType
FTInteger [CV]
cvs
parseValue (FTSeq 0 FTBit) cvs :: [CV]
cvs = (Integer -> Integer -> Value
forall b w i. BitWord b w i => Integer -> Integer -> GenValue b w i
Eval.word 0 0, [CV]
cvs)
parseValue (FTSeq n :: Int
n FTBit) cvs :: [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 Int
n) [CV]
cvs of
Just (x :: Integer
x, cvs' :: [CV]
cvs') -> (Integer -> Integer -> Value
forall b w i. BitWord b w i => Integer -> Integer -> GenValue b w i
Eval.word (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n) Integer
x, [CV]
cvs')
Nothing -> (Integer -> Eval (WordValue Bool BV Integer) -> Value
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord ([Value] -> Integer
forall i a. Num i => [a] -> i
genericLength [Value]
vs) (Eval (WordValue Bool BV Integer) -> Value)
-> Eval (WordValue Bool BV Integer) -> Value
forall a b. (a -> b) -> a -> b
$ WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer))
-> WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer)
forall a b. (a -> b) -> a -> b
$ BV -> WordValue Bool BV Integer
forall b w i. w -> WordValue b w i
Eval.WordVal (BV -> WordValue Bool BV Integer)
-> BV -> WordValue Bool BV Integer
forall a b. (a -> b) -> a -> b
$
[Bool] -> BV
forall b w i. BitWord b w i => [b] -> w
Eval.packWord ((Value -> Bool) -> [Value] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Bool
forall b w i. GenValue b w i -> b
fromVBit [Value]
vs), [CV]
cvs')
where (vs :: [Value]
vs, cvs' :: [CV]
cvs') = [FinType] -> [CV] -> ([Value], [CV])
parseValues (Int -> FinType -> [FinType]
forall a. Int -> a -> [a]
replicate Int
n FinType
FTBit) [CV]
cvs
parseValue (FTSeq n :: Int
n t :: FinType
t) cvs :: [CV]
cvs =
(Integer -> SeqMap Bool BV Integer -> Value
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
Eval.VSeq (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n) (SeqMap Bool BV Integer -> Value)
-> SeqMap Bool BV Integer -> Value
forall a b. (a -> b) -> a -> b
$ [Eval Value] -> SeqMap Bool BV Integer
forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
Eval.finiteSeqMap ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
Eval.ready [Value]
vs)
, [CV]
cvs'
)
where (vs :: [Value]
vs, cvs' :: [CV]
cvs') = [FinType] -> [CV] -> ([Value], [CV])
parseValues (Int -> FinType -> [FinType]
forall a. Int -> a -> [a]
replicate Int
n FinType
t) [CV]
cvs
parseValue (FTTuple ts :: [FinType]
ts) cvs :: [CV]
cvs = ([Eval Value] -> Value
forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
Eval.VTuple ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
Eval.ready [Value]
vs), [CV]
cvs')
where (vs :: [Value]
vs, cvs' :: [CV]
cvs') = [FinType] -> [CV] -> ([Value], [CV])
parseValues [FinType]
ts [CV]
cvs
parseValue (FTRecord fs :: [(Ident, FinType)]
fs) cvs :: [CV]
cvs = ([(Ident, Eval Value)] -> Value
forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
Eval.VRecord ([Ident] -> [Eval Value] -> [(Ident, Eval Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
ns ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
Eval.ready [Value]
vs)), [CV]
cvs')
where (ns :: [Ident]
ns, ts :: [FinType]
ts) = [(Ident, FinType)] -> ([Ident], [FinType])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Ident, FinType)]
fs
(vs :: [Value]
vs, cvs' :: [CV]
cvs') = [FinType] -> [CV] -> ([Value], [CV])
parseValues [FinType]
ts [CV]
cvs
allDeclGroups :: M.ModuleEnv -> [DeclGroup]
allDeclGroups :: ModuleEnv -> [DeclGroup]
allDeclGroups = (Module -> [DeclGroup]) -> [Module] -> [DeclGroup]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Module -> [DeclGroup]
mDecls ([Module] -> [DeclGroup])
-> (ModuleEnv -> [Module]) -> ModuleEnv -> [DeclGroup]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleEnv -> [Module]
M.loadedNonParamModules
data FinType
= FTBit
| FTInteger
| FTIntMod Integer
| FTSeq Int FinType
| FTTuple [FinType]
| FTRecord [(Ident, FinType)]
numType :: Integer -> Maybe Int
numType :: Integer -> Maybe Int
numType n :: Integer
n
| 0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n Bool -> Bool -> Bool
&& Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int) = Int -> Maybe Int
forall a. a -> Maybe a
Just (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)
| Bool
otherwise = Maybe Int
forall a. Maybe a
Nothing
finType :: TValue -> Maybe FinType
finType :: TValue -> Maybe FinType
finType ty :: TValue
ty =
case TValue
ty of
Eval.TVBit -> FinType -> Maybe FinType
forall a. a -> Maybe a
Just FinType
FTBit
Eval.TVInteger -> FinType -> Maybe FinType
forall a. a -> Maybe a
Just FinType
FTInteger
Eval.TVIntMod n :: Integer
n -> FinType -> Maybe FinType
forall a. a -> Maybe a
Just (Integer -> FinType
FTIntMod Integer
n)
Eval.TVSeq n :: Integer
n t :: TValue
t -> Int -> FinType -> FinType
FTSeq (Int -> FinType -> FinType)
-> Maybe Int -> Maybe (FinType -> FinType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Maybe Int
numType Integer
n Maybe (FinType -> FinType) -> Maybe FinType -> Maybe FinType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TValue -> Maybe FinType
finType TValue
t
Eval.TVTuple ts :: [TValue]
ts -> [FinType] -> FinType
FTTuple ([FinType] -> FinType) -> Maybe [FinType] -> Maybe FinType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TValue -> Maybe FinType) -> [TValue] -> Maybe [FinType]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse TValue -> Maybe FinType
finType [TValue]
ts
Eval.TVRec fields :: [(Ident, TValue)]
fields -> [(Ident, FinType)] -> FinType
FTRecord ([(Ident, FinType)] -> FinType)
-> Maybe [(Ident, FinType)] -> Maybe FinType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Ident, TValue) -> Maybe (Ident, FinType))
-> [(Ident, TValue)] -> Maybe [(Ident, FinType)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((TValue -> Maybe FinType)
-> (Ident, TValue) -> Maybe (Ident, FinType)
forall (f :: * -> *) a b t.
Functor f =>
(a -> f b) -> (t, a) -> f (t, b)
traverseSnd TValue -> Maybe FinType
finType) [(Ident, TValue)]
fields
Eval.TVAbstract {} -> Maybe FinType
forall a. Maybe a
Nothing
_ -> Maybe FinType
forall a. Maybe a
Nothing
unFinType :: FinType -> Type
unFinType :: FinType -> Type
unFinType fty :: FinType
fty =
case FinType
fty of
FTBit -> Type
tBit
FTInteger -> Type
tInteger
FTIntMod n :: Integer
n -> Type -> Type
tIntMod (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n)
FTSeq l :: Int
l ety :: FinType
ety -> Type -> Type -> Type
tSeq (Int -> Type
forall a. Integral a => a -> Type
tNum Int
l) (FinType -> Type
unFinType FinType
ety)
FTTuple ftys :: [FinType]
ftys -> [Type] -> Type
tTuple (FinType -> Type
unFinType (FinType -> Type) -> [FinType] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinType]
ftys)
FTRecord fs :: [(Ident, FinType)]
fs -> [(Ident, Type)] -> Type
tRec ([Ident] -> [Type] -> [(Ident, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
fns [Type]
tys)
where
fns :: [Ident]
fns = (Ident, FinType) -> Ident
forall a b. (a, b) -> a
fst ((Ident, FinType) -> Ident) -> [(Ident, FinType)] -> [Ident]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Ident, FinType)]
fs
tys :: [Type]
tys = FinType -> Type
unFinType (FinType -> Type)
-> ((Ident, FinType) -> FinType) -> (Ident, FinType) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident, FinType) -> FinType
forall a b. (a, b) -> b
snd ((Ident, FinType) -> Type) -> [(Ident, FinType)] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Ident, FinType)]
fs
predArgTypes :: Schema -> Either String [FinType]
predArgTypes :: Schema -> Either String [FinType]
predArgTypes schema :: Schema
schema@(Forall ts :: [TParam]
ts ps :: [Type]
ps ty :: Type
ty)
| [TParam] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TParam]
ts Bool -> Bool -> Bool
&& [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
ps =
case TValue -> Maybe [FinType]
go (TValue -> Maybe [FinType])
-> Either Nat' TValue -> Either Nat' (Maybe [FinType])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (HasCallStack => TypeEnv -> Type -> Either Nat' TValue
TypeEnv -> Type -> Either Nat' TValue
Eval.evalType TypeEnv
forall a. Monoid a => a
mempty Type
ty) of
Right (Just fts :: [FinType]
fts) -> [FinType] -> Either String [FinType]
forall a b. b -> Either a b
Right [FinType]
fts
_ -> String -> Either String [FinType]
forall a b. a -> Either a b
Left (String -> Either String [FinType])
-> String -> Either String [FinType]
forall a b. (a -> b) -> a -> b
$ "Not a valid predicate type:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
schema)
| Bool
otherwise = String -> Either String [FinType]
forall a b. a -> Either a b
Left (String -> Either String [FinType])
-> String -> Either String [FinType]
forall a b. (a -> b) -> a -> b
$ "Not a monomorphic type:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
schema)
where
go :: TValue -> Maybe [FinType]
go :: TValue -> Maybe [FinType]
go Eval.TVBit = [FinType] -> Maybe [FinType]
forall a. a -> Maybe a
Just []
go (Eval.TVFun ty1 :: TValue
ty1 ty2 :: TValue
ty2) = (:) (FinType -> [FinType] -> [FinType])
-> Maybe FinType -> Maybe ([FinType] -> [FinType])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TValue -> Maybe FinType
finType TValue
ty1 Maybe ([FinType] -> [FinType])
-> Maybe [FinType] -> Maybe [FinType]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TValue -> Maybe [FinType]
go TValue
ty2
go _ = Maybe [FinType]
forall a. Maybe a
Nothing
inBoundsIntMod :: Integer -> SInteger -> SBool
inBoundsIntMod :: Integer -> SBool -> SBool
inBoundsIntMod n :: Integer
n x :: SBool
x =
SBool -> SBool -> SBool
SBV.svAnd (SBool -> SBool -> SBool
SBV.svLessEq (Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
Eval.integerLit 0) SBool
x) (SBool -> SBool -> SBool
SBV.svLessThan SBool
x (Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
Eval.integerLit Integer
n))
forallFinType :: FinType -> WriterT [SBool] SBV.Symbolic Value
forallFinType :: FinType -> WriterT [SBool] Symbolic Value
forallFinType ty :: FinType
ty =
case FinType
ty of
FTBit -> SBool -> Value
forall b w i. b -> GenValue b w i
VBit (SBool -> Value)
-> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Symbolic SBool
forallSBool_
FTInteger -> SBool -> Value
forall b w i. i -> GenValue b w i
VInteger (SBool -> Value)
-> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Symbolic SBool
forallSInteger_
FTIntMod n :: Integer
n -> do SBool
x <- Symbolic SBool -> WriterT [SBool] Symbolic SBool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Symbolic SBool
forallSInteger_
[SBool] -> WriterT [SBool] Symbolic ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Integer -> SBool -> SBool
inBoundsIntMod Integer
n SBool
x]
Value -> WriterT [SBool] Symbolic Value
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> Value
forall b w i. i -> GenValue b w i
VInteger SBool
x)
FTSeq 0 FTBit -> Value -> WriterT [SBool] Symbolic Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> WriterT [SBool] Symbolic Value)
-> Value -> WriterT [SBool] Symbolic Value
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Value
forall b w i. BitWord b w i => Integer -> Integer -> GenValue b w i
Eval.word 0 0
FTSeq n :: Int
n FTBit -> Integer -> Eval (WordValue SBool SBool SBool) -> Value
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n) (Eval (WordValue SBool SBool SBool) -> Value)
-> (SBool -> Eval (WordValue SBool SBool SBool)) -> SBool -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> (SBool -> WordValue SBool SBool SBool)
-> SBool
-> Eval (WordValue SBool SBool SBool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBool -> WordValue SBool SBool SBool
forall b w i. w -> WordValue b w i
Eval.WordVal (SBool -> Value)
-> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Int -> Symbolic SBool
forallBV_ Int
n)
FTSeq n :: Int
n t :: FinType
t -> do [Value]
vs <- Int
-> WriterT [SBool] Symbolic Value
-> WriterT [SBool] Symbolic [Value]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (FinType -> WriterT [SBool] Symbolic Value
forallFinType FinType
t)
Value -> WriterT [SBool] Symbolic Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> WriterT [SBool] Symbolic Value)
-> Value -> WriterT [SBool] Symbolic Value
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap SBool SBool SBool -> Value
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n) (SeqMap SBool SBool SBool -> Value)
-> SeqMap SBool SBool SBool -> Value
forall a b. (a -> b) -> a -> b
$ [Eval Value] -> SeqMap SBool SBool SBool
forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
Eval.finiteSeqMap ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
Eval.ready [Value]
vs)
FTTuple ts :: [FinType]
ts -> [Eval Value] -> Value
forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
VTuple ([Eval Value] -> Value)
-> WriterT [SBool] Symbolic [Eval Value]
-> WriterT [SBool] Symbolic Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FinType -> WriterT [SBool] Symbolic (Eval Value))
-> [FinType] -> WriterT [SBool] Symbolic [Eval Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Value -> Eval Value)
-> WriterT [SBool] Symbolic Value
-> WriterT [SBool] Symbolic (Eval Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value -> Eval Value
forall a. a -> Eval a
Eval.ready (WriterT [SBool] Symbolic Value
-> WriterT [SBool] Symbolic (Eval Value))
-> (FinType -> WriterT [SBool] Symbolic Value)
-> FinType
-> WriterT [SBool] Symbolic (Eval Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinType -> WriterT [SBool] Symbolic Value
forallFinType) [FinType]
ts
FTRecord fs :: [(Ident, FinType)]
fs -> [(Ident, Eval Value)] -> Value
forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
VRecord ([(Ident, Eval Value)] -> Value)
-> WriterT [SBool] Symbolic [(Ident, Eval Value)]
-> WriterT [SBool] Symbolic Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Ident, FinType) -> WriterT [SBool] Symbolic (Ident, Eval Value))
-> [(Ident, FinType)]
-> WriterT [SBool] Symbolic [(Ident, Eval Value)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((FinType -> WriterT [SBool] Symbolic (Eval Value))
-> (Ident, FinType) -> WriterT [SBool] Symbolic (Ident, Eval Value)
forall (f :: * -> *) a b t.
Functor f =>
(a -> f b) -> (t, a) -> f (t, b)
traverseSnd ((Value -> Eval Value)
-> WriterT [SBool] Symbolic Value
-> WriterT [SBool] Symbolic (Eval Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value -> Eval Value
forall a. a -> Eval a
Eval.ready (WriterT [SBool] Symbolic Value
-> WriterT [SBool] Symbolic (Eval Value))
-> (FinType -> WriterT [SBool] Symbolic Value)
-> FinType
-> WriterT [SBool] Symbolic (Eval Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinType -> WriterT [SBool] Symbolic Value
forallFinType)) [(Ident, FinType)]
fs
existsFinType :: FinType -> WriterT [SBool] SBV.Symbolic Value
existsFinType :: FinType -> WriterT [SBool] Symbolic Value
existsFinType ty :: FinType
ty =
case FinType
ty of
FTBit -> SBool -> Value
forall b w i. b -> GenValue b w i
VBit (SBool -> Value)
-> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Symbolic SBool
existsSBool_
FTInteger -> SBool -> Value
forall b w i. i -> GenValue b w i
VInteger (SBool -> Value)
-> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Symbolic SBool
existsSInteger_
FTIntMod n :: Integer
n -> do SBool
x <- Symbolic SBool -> WriterT [SBool] Symbolic SBool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Symbolic SBool
existsSInteger_
[SBool] -> WriterT [SBool] Symbolic ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Integer -> SBool -> SBool
inBoundsIntMod Integer
n SBool
x]
Value -> WriterT [SBool] Symbolic Value
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> Value
forall b w i. i -> GenValue b w i
VInteger SBool
x)
FTSeq 0 FTBit -> Value -> WriterT [SBool] Symbolic Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> WriterT [SBool] Symbolic Value)
-> Value -> WriterT [SBool] Symbolic Value
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Value
forall b w i. BitWord b w i => Integer -> Integer -> GenValue b w i
Eval.word 0 0
FTSeq n :: Int
n FTBit -> Integer -> Eval (WordValue SBool SBool SBool) -> Value
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n) (Eval (WordValue SBool SBool SBool) -> Value)
-> (SBool -> Eval (WordValue SBool SBool SBool)) -> SBool -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> (SBool -> WordValue SBool SBool SBool)
-> SBool
-> Eval (WordValue SBool SBool SBool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBool -> WordValue SBool SBool SBool
forall b w i. w -> WordValue b w i
Eval.WordVal (SBool -> Value)
-> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Int -> Symbolic SBool
existsBV_ Int
n)
FTSeq n :: Int
n t :: FinType
t -> do [Value]
vs <- Int
-> WriterT [SBool] Symbolic Value
-> WriterT [SBool] Symbolic [Value]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (FinType -> WriterT [SBool] Symbolic Value
existsFinType FinType
t)
Value -> WriterT [SBool] Symbolic Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> WriterT [SBool] Symbolic Value)
-> Value -> WriterT [SBool] Symbolic Value
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap SBool SBool SBool -> Value
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n) (SeqMap SBool SBool SBool -> Value)
-> SeqMap SBool SBool SBool -> Value
forall a b. (a -> b) -> a -> b
$ [Eval Value] -> SeqMap SBool SBool SBool
forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
Eval.finiteSeqMap ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
Eval.ready [Value]
vs)
FTTuple ts :: [FinType]
ts -> [Eval Value] -> Value
forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
VTuple ([Eval Value] -> Value)
-> WriterT [SBool] Symbolic [Eval Value]
-> WriterT [SBool] Symbolic Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FinType -> WriterT [SBool] Symbolic (Eval Value))
-> [FinType] -> WriterT [SBool] Symbolic [Eval Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Value -> Eval Value)
-> WriterT [SBool] Symbolic Value
-> WriterT [SBool] Symbolic (Eval Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value -> Eval Value
forall a. a -> Eval a
Eval.ready (WriterT [SBool] Symbolic Value
-> WriterT [SBool] Symbolic (Eval Value))
-> (FinType -> WriterT [SBool] Symbolic Value)
-> FinType
-> WriterT [SBool] Symbolic (Eval Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinType -> WriterT [SBool] Symbolic Value
existsFinType) [FinType]
ts
FTRecord fs :: [(Ident, FinType)]
fs -> [(Ident, Eval Value)] -> Value
forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
VRecord ([(Ident, Eval Value)] -> Value)
-> WriterT [SBool] Symbolic [(Ident, Eval Value)]
-> WriterT [SBool] Symbolic Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Ident, FinType) -> WriterT [SBool] Symbolic (Ident, Eval Value))
-> [(Ident, FinType)]
-> WriterT [SBool] Symbolic [(Ident, Eval Value)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((FinType -> WriterT [SBool] Symbolic (Eval Value))
-> (Ident, FinType) -> WriterT [SBool] Symbolic (Ident, Eval Value)
forall (f :: * -> *) a b t.
Functor f =>
(a -> f b) -> (t, a) -> f (t, b)
traverseSnd ((Value -> Eval Value)
-> WriterT [SBool] Symbolic Value
-> WriterT [SBool] Symbolic (Eval Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value -> Eval Value
forall a. a -> Eval a
Eval.ready (WriterT [SBool] Symbolic Value
-> WriterT [SBool] Symbolic (Eval Value))
-> (FinType -> WriterT [SBool] Symbolic Value)
-> FinType
-> WriterT [SBool] Symbolic (Eval Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinType -> WriterT [SBool] Symbolic Value
existsFinType)) [(Ident, FinType)]
fs