mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-30 23:45:23 +03:00
backport prover command interface
Conflicts: src/Cryptol/REPL/Command.hs src/Cryptol/Symbolic.hs
This commit is contained in:
Adam C. Foltzer
parent
917cc27145
commit
579ccc96a0
@ -40,7 +40,8 @@ flag self-contained
|
||||
library
|
||||
Default-language:
|
||||
Haskell98
|
||||
Build-depends: base >= 4.6 && < 5,
|
||||
Build-depends: base >= 4.7 && < 5,
|
||||
base-compat >= 0.6,
|
||||
array >= 0.4,
|
||||
async >= 2.0,
|
||||
containers >= 0.5,
|
||||
@ -56,7 +57,7 @@ library
|
||||
process >= 1.2,
|
||||
QuickCheck >= 2.7,
|
||||
random >= 1.0.1,
|
||||
sbv (>= 4.3 && < 5.0) || (>= 5.1 && < 5.2),
|
||||
sbv >= 5.3 && < 5.4,
|
||||
smtLib >= 1.0.7,
|
||||
syb >= 0.4,
|
||||
text >= 1.1,
|
||||
|
||||
@ -54,6 +54,7 @@ import Cryptol.Utils.Panic(panic)
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.Prims.Doc(helpDoc)
|
||||
import qualified Cryptol.Transform.Specialize as S
|
||||
import Cryptol.Symbolic (ProverCommand(..), QueryType(..), SatNum(..))
|
||||
import qualified Cryptol.Symbolic as Symbolic
|
||||
|
||||
import Control.DeepSeq
|
||||
@ -336,9 +337,10 @@ satCmd, proveCmd :: String -> REPL ()
|
||||
satCmd = cmdProveSat True
|
||||
proveCmd = cmdProveSat False
|
||||
|
||||
-- | Run a SAT solver on the given expression. Binds the @it@ variable
|
||||
-- to a record whose form depends on the expression given. See ticket
|
||||
-- #66 for a discussion of this design.
|
||||
-- | Console-specific version of 'proveSat'. Prints output to the
|
||||
-- console, and binds the @it@ variable to a record whose form depends
|
||||
-- on the expression given. See ticket #66 for a discussion of this
|
||||
-- design.
|
||||
cmdProveSat :: Bool -> String -> REPL ()
|
||||
cmdProveSat isSat "" =
|
||||
do xs <- getPropertyNames
|
||||
@ -349,81 +351,104 @@ cmdProveSat isSat "" =
|
||||
then rPutStr $ ":sat " ++ x ++ "\n\t"
|
||||
else rPutStr $ ":prove " ++ x ++ "\n\t"
|
||||
cmdProveSat isSat x
|
||||
cmdProveSat isSat str = do
|
||||
cmdProveSat isSat expr = do
|
||||
let cexStr | isSat = "satisfying assignment"
|
||||
| otherwise = "counterexample"
|
||||
EnvString proverName <- getUser "prover"
|
||||
EnvString fileName <- getUser "smtfile"
|
||||
let mfile = if fileName == "-" then Nothing else Just fileName
|
||||
case proverName of
|
||||
"offline" -> offlineProveSat isSat str mfile
|
||||
_ -> onlineProveSat isSat str proverName mfile
|
||||
"offline" -> do
|
||||
result <- offlineProveSat isSat expr mfile
|
||||
case result of
|
||||
Left msg -> rPutStrLn msg
|
||||
Right smtlib -> do
|
||||
let filename = fromMaybe "standard output" mfile
|
||||
let satWord | isSat = "satisfiability"
|
||||
| otherwise = "validity"
|
||||
rPutStrLn $
|
||||
"Writing to SMT-Lib file " ++ filename ++ "..."
|
||||
rPutStrLn $
|
||||
"To determine the " ++ satWord ++
|
||||
" of the expression, use an external SMT solver."
|
||||
case mfile of
|
||||
Just path -> io $ writeFile path smtlib
|
||||
Nothing -> rPutStr smtlib
|
||||
_ -> do
|
||||
result <- onlineProveSat isSat expr proverName mfile
|
||||
ppOpts <- getPPValOpts
|
||||
case result of
|
||||
Symbolic.EmptyResult ->
|
||||
panic "REPL.Command" [ "got EmptyResult for online prover query" ]
|
||||
Symbolic.ProverError msg -> rPutStrLn msg
|
||||
Symbolic.ThmResult ts -> do
|
||||
rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.")
|
||||
let (t, e) = mkSolverResult cexStr (not isSat) (Left ts)
|
||||
bindItVariable t e
|
||||
Symbolic.AllSatResult tevss -> do
|
||||
let tess = map (map $ \(t,e,_) -> (t,e)) tevss
|
||||
vss = map (map $ \(_,_,v) -> v) tevss
|
||||
ppvs vs = do
|
||||
parseExpr <- replParseExpr expr
|
||||
let docs = map (pp . E.WithBase ppOpts) vs
|
||||
-- function application has precedence 3
|
||||
doc = ppPrec 3 parseExpr
|
||||
rPrint $ hsep (doc : docs) <+>
|
||||
text (if isSat then "= True" else "= False")
|
||||
resultRecs = map (mkSolverResult cexStr isSat . Right) tess
|
||||
collectTes tes = (t, es)
|
||||
where
|
||||
(ts, es) = unzip tes
|
||||
t = case nub ts of
|
||||
[t'] -> t'
|
||||
_ -> panic "REPL.Command.onlineProveSat"
|
||||
[ "satisfying assignments with different types" ]
|
||||
(ty, exprs) =
|
||||
case resultRecs of
|
||||
[] -> panic "REPL.Command.onlineProveSat"
|
||||
[ "no satisfying assignments after mkSovlerResult" ]
|
||||
[(t, e)] -> (t, [e])
|
||||
_ -> collectTes resultRecs
|
||||
forM_ vss ppvs
|
||||
case (ty, exprs) of
|
||||
(t, [e]) -> bindItVariable t e
|
||||
(t, es ) -> bindItVariables t es
|
||||
|
||||
onlineProveSat :: Bool
|
||||
-> String -> String -> Maybe FilePath -> REPL ()
|
||||
-> String -> String -> Maybe FilePath -> REPL Symbolic.ProverResult
|
||||
onlineProveSat isSat str proverName mfile = do
|
||||
EnvBool verbose <- getUser "debug"
|
||||
mSatNum <- getUserSatNum
|
||||
let cexStr | isSat = "satisfying assignment"
|
||||
| otherwise = "counterexample"
|
||||
satNum <- getUserSatNum
|
||||
parseExpr <- replParseExpr str
|
||||
(expr, schema) <- replCheckExpr parseExpr
|
||||
denv <- getDynEnv
|
||||
result <- liftModuleCmd $
|
||||
Symbolic.satProve
|
||||
isSat
|
||||
mSatNum
|
||||
(proverName, verbose)
|
||||
(M.deDecls denv)
|
||||
mfile
|
||||
(expr, schema)
|
||||
ppOpts <- getPPValOpts
|
||||
case result of
|
||||
Symbolic.EmptyResult ->
|
||||
panic "REPL.Command" [ "got EmptyResult for online prover query" ]
|
||||
Symbolic.ProverError msg -> rPutStrLn msg
|
||||
Symbolic.ThmResult ts -> do
|
||||
rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.")
|
||||
let (t, e) = mkSolverResult cexStr (not isSat) (Left ts)
|
||||
bindItVariable t e
|
||||
Symbolic.AllSatResult tevss -> do
|
||||
let tess = map (map $ \(t,e,_) -> (t,e)) tevss
|
||||
vss = map (map $ \(_,_,v) -> v) tevss
|
||||
ppvs vs = do
|
||||
let docs = map (pp . E.WithBase ppOpts) vs
|
||||
-- function application has precedence 3
|
||||
doc = ppPrec 3 parseExpr
|
||||
rPrint $ hsep (doc : docs) <+>
|
||||
text (if isSat then "= True" else "= False")
|
||||
resultRecs = map (mkSolverResult cexStr isSat . Right) tess
|
||||
collectTes tes = (t, es)
|
||||
where
|
||||
(ts, es) = unzip tes
|
||||
t = case nub ts of
|
||||
[t'] -> t'
|
||||
_ -> panic "REPL.Command.onlineProveSat"
|
||||
[ "satisfying assignments with different types" ]
|
||||
(ty, exprs) =
|
||||
case resultRecs of
|
||||
[] -> panic "REPL.Command.onlineProveSat"
|
||||
[ "no satisfying assignments after mkSovlerResult" ]
|
||||
[(t, e)] -> (t, [e])
|
||||
_ -> collectTes resultRecs
|
||||
forM_ vss ppvs
|
||||
case (ty, exprs) of
|
||||
(t, [e]) -> bindItVariable t e
|
||||
(t, es ) -> bindItVariables t es
|
||||
|
||||
offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL ()
|
||||
offlineProveSat isSat str mfile = do
|
||||
EnvBool vrb <- getUser "debug"
|
||||
parseExpr <- replParseExpr str
|
||||
exsch <- replCheckExpr parseExpr
|
||||
decls <- fmap M.deDecls getDynEnv
|
||||
result <- liftModuleCmd $
|
||||
Symbolic.satProveOffline isSat vrb decls mfile exsch
|
||||
case result of
|
||||
Symbolic.ProverError msg -> rPutStrLn msg
|
||||
Symbolic.EmptyResult -> return ()
|
||||
_ -> panic "REPL.Command" [ "unexpected prover result for offline prover" ]
|
||||
let cmd = Symbolic.ProverCommand {
|
||||
pcQueryType = if isSat then SatQuery satNum else ProveQuery
|
||||
, pcProverName = proverName
|
||||
, pcVerbose = verbose
|
||||
, pcExtraDecls = decls
|
||||
, pcSmtFile = mfile
|
||||
, pcExpr = expr
|
||||
, pcSchema = schema
|
||||
}
|
||||
liftModuleCmd $ Symbolic.satProve cmd
|
||||
|
||||
offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
|
||||
offlineProveSat isSat str mfile = do
|
||||
EnvBool verbose <- getUser "debug"
|
||||
parseExpr <- replParseExpr str
|
||||
(expr, schema) <- replCheckExpr parseExpr
|
||||
decls <- fmap M.deDecls getDynEnv
|
||||
let cmd = Symbolic.ProverCommand {
|
||||
pcQueryType = if isSat then SatQuery (SomeSat 0) else ProveQuery
|
||||
, pcProverName = "offline"
|
||||
, pcVerbose = verbose
|
||||
, pcExtraDecls = decls
|
||||
, pcSmtFile = mfile
|
||||
, pcExpr = expr
|
||||
, pcSchema = schema
|
||||
}
|
||||
liftModuleCmd $ Symbolic.satProveOffline cmd
|
||||
|
||||
-- | Make a type/expression pair that is suitable for binding to @it@
|
||||
-- after running @:sat@ or @:prove@
|
||||
|
||||
@ -80,7 +80,7 @@ import qualified Cryptol.TypeCheck.AST as T
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.Symbolic (proverNames, lookupProver)
|
||||
import Cryptol.Symbolic (proverNames, lookupProver, SatNum(..))
|
||||
|
||||
import Control.Monad (ap,unless,when)
|
||||
import Data.IORef
|
||||
@ -582,12 +582,12 @@ checkSatNum val = case val of
|
||||
_ -> return $ Just "must be an integer > 0 or \"all\""
|
||||
_ -> return $ Just "unable to parse a value for satNum"
|
||||
|
||||
getUserSatNum :: REPL (Maybe Int)
|
||||
getUserSatNum :: REPL SatNum
|
||||
getUserSatNum = do
|
||||
EnvString s <- getUser "satNum"
|
||||
case s of
|
||||
"all" -> return Nothing
|
||||
_ | Just n <- readMaybe s -> return (Just n)
|
||||
"all" -> return AllSat
|
||||
_ | Just n <- readMaybe s -> return (SomeSat n)
|
||||
_ -> panic "REPL.Monad.getUserSatNum"
|
||||
[ "invalid satNum option" ]
|
||||
|
||||
|
||||
@ -6,23 +6,24 @@
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TupleSections #-}
|
||||
|
||||
module Cryptol.Symbolic where
|
||||
|
||||
import Control.Monad (replicateM, when, zipWithM)
|
||||
import Control.Monad.IO.Class
|
||||
import Data.List (transpose, intercalate)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Control.Exception as X
|
||||
|
||||
import qualified Data.SBV.Dynamic as SBV
|
||||
|
||||
import qualified Cryptol.ModuleSystem as M
|
||||
import qualified Cryptol.ModuleSystem.Env as M
|
||||
import qualified Cryptol.ModuleSystem.Monad as M
|
||||
|
||||
import Cryptol.Symbolic.Prims
|
||||
import Cryptol.Symbolic.Value
|
||||
@ -75,6 +76,30 @@ lookupProver s =
|
||||
|
||||
type SatResult = [(Type, Expr, Eval.Value)]
|
||||
|
||||
data SatNum = AllSat | SomeSat Int
|
||||
deriving (Show)
|
||||
|
||||
data QueryType = SatQuery SatNum | ProveQuery
|
||||
deriving (Show)
|
||||
|
||||
data ProverCommand = ProverCommand {
|
||||
pcQueryType :: QueryType
|
||||
-- ^ The type of query to run
|
||||
, pcProverName :: String
|
||||
-- ^ Which prover to use (one of the strings in 'proverConfigs')
|
||||
, pcVerbose :: Bool
|
||||
-- ^ Verbosity flag passed to SBV
|
||||
, pcExtraDecls :: [DeclGroup]
|
||||
-- ^ Extra declarations to bring into scope for symbolic
|
||||
-- simulation
|
||||
, pcSmtFile :: Maybe FilePath
|
||||
-- ^ Optionally output the SMTLIB query to a file
|
||||
, pcExpr :: Expr
|
||||
-- ^ The typechecked expression to evaluate
|
||||
, pcSchema :: Schema
|
||||
-- ^ The 'Schema' of @pcExpr@
|
||||
}
|
||||
|
||||
-- | A prover result is either an error message, an empty result (eg
|
||||
-- for the offline prover), a counterexample or a lazy list of
|
||||
-- satisfying assignments.
|
||||
@ -83,42 +108,65 @@ data ProverResult = AllSatResult [SatResult] -- LAZY
|
||||
| EmptyResult
|
||||
| ProverError String
|
||||
|
||||
satSMTResults :: SBV.SatResult -> [SBV.SMTResult]
|
||||
satSMTResults (SBV.SatResult r) = [r]
|
||||
|
||||
allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult]
|
||||
allSatSMTResults (SBV.AllSatResult (_, rs)) = rs
|
||||
|
||||
thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult]
|
||||
thmSMTResults (SBV.ThmResult r) = [r]
|
||||
|
||||
satProve :: Bool
|
||||
-> Maybe Int -- ^ satNum
|
||||
-> (String, Bool)
|
||||
-> [DeclGroup]
|
||||
-> Maybe FilePath
|
||||
-> (Expr, Schema)
|
||||
-> M.ModuleCmd ProverResult
|
||||
satProve isSat mSatNum (proverName, verbose) edecls mfile (expr, schema) = protectStack $ \modEnv -> do
|
||||
let extDgs = allDeclGroups modEnv ++ edecls
|
||||
proverError :: String -> M.ModuleCmd ProverResult
|
||||
proverError msg modEnv = return (Right (ProverError msg, modEnv), [])
|
||||
|
||||
satProve :: ProverCommand -> M.ModuleCmd ProverResult
|
||||
satProve ProverCommand {..} = protectStack proverError $ \modEnv ->
|
||||
M.runModuleM modEnv $ do
|
||||
let (isSat, mSatNum) = case pcQueryType of
|
||||
ProveQuery -> (False, Nothing)
|
||||
SatQuery sn -> case sn of
|
||||
SomeSat n -> (True, Just n)
|
||||
AllSat -> (True, Nothing)
|
||||
let extDgs = allDeclGroups modEnv ++ pcExtraDecls
|
||||
provers <-
|
||||
case proverName of
|
||||
"any" -> SBV.sbvAvailableSolvers
|
||||
_ -> return [(lookupProver proverName) { SBV.smtFile = mfile }]
|
||||
let provers' = [ p { SBV.timing = verbose, SBV.verbose = verbose } | p <- provers ]
|
||||
case pcProverName of
|
||||
"any" -> M.io SBV.sbvAvailableSolvers
|
||||
_ -> return [(lookupProver pcProverName) { SBV.smtFile = pcSmtFile }]
|
||||
let provers' = [ p { SBV.timing = pcVerbose, SBV.verbose = pcVerbose } | p <- provers ]
|
||||
let tyFn = if isSat then existsFinType else forallFinType
|
||||
let runProver fn tag e = do
|
||||
when verbose $ liftIO $
|
||||
case provers of
|
||||
[prover] -> do
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Trying proof with " ++ show prover
|
||||
res <- M.io (fn prover e)
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Got result from " ++ show prover
|
||||
return (tag res)
|
||||
_ ->
|
||||
return [ SBV.ProofError
|
||||
prover
|
||||
[":sat with option prover=any requires option satNum=1"]
|
||||
| prover <- provers ]
|
||||
runProvers fn tag e = do
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Trying proof with " ++
|
||||
intercalate ", " (map show provers)
|
||||
(firstProver, res) <- fn provers' e
|
||||
when verbose $ liftIO $
|
||||
(firstProver, res) <- M.io $ fn provers' e
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Got result from " ++ show firstProver
|
||||
return (tag res)
|
||||
let runFn | isSat = runProver SBV.allSatWithAny allSatSMTResults
|
||||
| otherwise = runProver SBV.proveWithAny thmSMTResults
|
||||
case predArgTypes schema of
|
||||
Left msg -> return (Right (ProverError msg, modEnv), [])
|
||||
Right ts -> do when verbose $ putStrLn "Simulating..."
|
||||
let env = evalDecls emptyEnv extDgs
|
||||
let v = evalExpr env expr
|
||||
let runFn = case pcQueryType of
|
||||
ProveQuery -> runProvers SBV.proveWithAny thmSMTResults
|
||||
SatQuery sn -> case sn of
|
||||
SomeSat 1 -> runProvers SBV.satWithAny satSMTResults
|
||||
_ -> runProver SBV.allSatWith allSatSMTResults
|
||||
case predArgTypes pcSchema of
|
||||
Left msg -> return (ProverError msg)
|
||||
Right ts -> do when pcVerbose $ M.io $ putStrLn "Simulating..."
|
||||
let env = evalDecls mempty extDgs
|
||||
let v = evalExpr env pcExpr
|
||||
results' <- runFn $ do
|
||||
args <- mapM tyFn ts
|
||||
b <- return $! fromVBit (foldl fromVFun v args)
|
||||
@ -152,48 +200,37 @@ satProve isSat mSatNum (proverName, verbose) edecls mfile (expr, schema) = prote
|
||||
| otherwise = show . SBV.ThmResult . head
|
||||
boom = panic "Cryptol.Symbolic.sat"
|
||||
[ "attempted to evaluate bogus boolean for pretty-printing" ]
|
||||
return (Right (esatexprs, modEnv), [])
|
||||
return esatexprs
|
||||
|
||||
satProveOffline :: Bool
|
||||
-> Bool
|
||||
-> [DeclGroup]
|
||||
-> Maybe FilePath
|
||||
-> (Expr, Schema)
|
||||
-> M.ModuleCmd ProverResult
|
||||
satProveOffline isSat vrb edecls mfile (expr, schema) =
|
||||
protectStack $ \modEnv -> do
|
||||
let extDgs = allDeclGroups modEnv ++ edecls
|
||||
satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String)
|
||||
satProveOffline ProverCommand {..} =
|
||||
protectStack (\msg modEnv -> return (Right (Left msg, modEnv), [])) $ \modEnv -> do
|
||||
let isSat = case pcQueryType of
|
||||
ProveQuery -> False
|
||||
SatQuery _ -> True
|
||||
let extDgs = allDeclGroups modEnv ++ pcExtraDecls
|
||||
let tyFn = if isSat then existsFinType else forallFinType
|
||||
let filename = fromMaybe "standard output" mfile
|
||||
case predArgTypes schema of
|
||||
Left msg -> return (Right (ProverError msg, modEnv), [])
|
||||
case predArgTypes pcSchema of
|
||||
Left msg -> return (Right (Left msg, modEnv), [])
|
||||
Right ts ->
|
||||
do when vrb $ putStrLn "Simulating..."
|
||||
let env = evalDecls emptyEnv extDgs
|
||||
let v = evalExpr env expr
|
||||
let satWord | isSat = "satisfiability"
|
||||
| otherwise = "validity"
|
||||
txt <- SBV.compileToSMTLib smtMode isSat $ do
|
||||
args <- mapM tyFn ts
|
||||
b <- return $! fromVBit (foldl fromVFun v args)
|
||||
liftIO $ putStrLn $
|
||||
"Writing to SMT-Lib file " ++ filename ++ "..."
|
||||
return b
|
||||
liftIO $ putStrLn $
|
||||
"To determine the " ++ satWord ++
|
||||
" of the expression, use an external SMT solver."
|
||||
case mfile of
|
||||
Just path -> writeFile path txt
|
||||
Nothing -> putStr txt
|
||||
return (Right (EmptyResult, modEnv), [])
|
||||
do when pcVerbose $ putStrLn "Simulating..."
|
||||
let env = evalDecls mempty extDgs
|
||||
let v = evalExpr env pcExpr
|
||||
smtlib <- SBV.compileToSMTLib SBV.SMTLib2 isSat $ do
|
||||
args <- mapM tyFn ts
|
||||
b <- return $! fromVBit (foldl fromVFun v args)
|
||||
return b
|
||||
return (Right (Right smtlib, modEnv), [])
|
||||
|
||||
protectStack :: M.ModuleCmd ProverResult
|
||||
-> M.ModuleCmd ProverResult
|
||||
protectStack cmd modEnv = X.catchJust isOverflow (cmd modEnv) handler
|
||||
protectStack :: (String -> M.ModuleCmd a)
|
||||
-> M.ModuleCmd a
|
||||
-> M.ModuleCmd a
|
||||
protectStack mkErr cmd modEnv =
|
||||
X.catchJust isOverflow (cmd modEnv) handler
|
||||
where isOverflow X.StackOverflow = Just ()
|
||||
isOverflow _ = Nothing
|
||||
msg = "Symbolic evaluation failed to terminate."
|
||||
handler () = return (Right (ProverError msg, modEnv), [])
|
||||
handler () = mkErr msg modEnv
|
||||
|
||||
parseValues :: [FinType] -> [SBV.CW] -> ([Eval.Value], [SBV.CW])
|
||||
parseValues [] cws = ([], cws)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user