refactored sat/prove code for non-console clients

2024-11-29 01:45:36 +03:00 · 2015-07-10 18:19:53 -07:00 · 2015-07-10 18:19:53 -07:00 · 96a2cf2e44
commit 96a2cf2e44
parent ce5bbe9f8a
3 changed files with 171 additions and 126 deletions
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@ -67,6 +67,7 @@ import Cryptol.Utils.PP
 import Cryptol.Utils.Panic(panic)
 import qualified Cryptol.Parser.AST as P
 import qualified Cryptol.Transform.Specialize as S
+import Cryptol.Symbolic (ProverCommand(..), QueryType(..), SatNum(..))
 import qualified Cryptol.Symbolic as Symbolic

 import Control.DeepSeq
@ -356,9 +357,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
@ -369,83 +371,108 @@ 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 iteSolver <- getUser "iteSolver"
  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, iteSolver, 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 useIte <- getUser "iteSolver"
-  EnvBool vrb <- getUser "debug"
-  parseExpr <- replParseExpr str
-  (_,e,s) <- replCheckExpr parseExpr
  decls <- fmap M.deDecls getDynEnv
-  result <- liftModuleCmd $
-    Symbolic.satProveOffline isSat useIte vrb decls mfile (e,s)
-  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
+        , pcUseSolverIte = iteSolver
+        , 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 iteSolver <- getUser "iteSolver"
+  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"
+        , pcUseSolverIte = iteSolver
+        , 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@
--- a/src/Cryptol/REPL/Monad.hs
+++ b/src/Cryptol/REPL/Monad.hs
@ -79,7 +79,7 @@ import qualified Cryptol.TypeCheck 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 Control.Monad.IO.Class
@ -646,12 +646,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" ]

--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@ -1,3 +1,4 @@
+{-# LANGUAGE RecordWildCards #-}
 -- |
 -- Module      :  $Header$
 -- Copyright   :  (c) 2013-2015 Galois, Inc.
@ -16,7 +17,6 @@ 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
@ -67,6 +67,32 @@ 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')
+  , pcUseSolverIte :: Bool
+    -- ^ Whether to force branches (see 'Data.SBV.Dynamic.svSymbolicMerge')
+  , 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.
@ -81,36 +107,38 @@ allSatSMTResults (SBV.AllSatResult (_, rs)) = rs
 thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult]
 thmSMTResults (SBV.ThmResult r) = [r]

-satProve :: Bool
-         -> Maybe Int -- ^ satNum
-         -> (String, Bool, Bool)
-         -> [DeclGroup]
-         -> Maybe FilePath
-         -> (Expr, Schema)
-         -> M.ModuleCmd ProverResult
-satProve isSat mSatNum (proverName, useSolverIte, verbose) edecls mfile (expr, schema) = protectStack useSolverIte $ \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 pcUseSolverIte proverError $ \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
+    case pcProverName of
      "any" -> SBV.sbvAvailableSolvers
-      _ -> return [(lookupProver proverName) { SBV.smtFile = mfile }]
-  let provers' = [ p { SBV.timing = verbose, SBV.verbose = verbose } | p <- provers ]
+      _ -> 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 $
+        when pcVerbose $ liftIO $
          putStrLn $ "Trying proof with " ++
                     intercalate ", " (map show provers)
        (firstProver, res) <- fn provers' e
-        when verbose $ liftIO $
+        when pcVerbose $ liftIO $
          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
+  case predArgTypes pcSchema of
    Left msg -> return (Right (ProverError msg, modEnv), [])
-    Right ts -> do when verbose $ putStrLn "Simulating..."
-                   let env = evalDecls (emptyEnv useSolverIte) extDgs
-                   let v = evalExpr env expr
+    Right ts -> do when pcVerbose $ putStrLn "Simulating..."
+                   let env = evalDecls (emptyEnv pcUseSolverIte) extDgs
+                   let v = evalExpr env pcExpr
                   results' <- runFn $ do
                                 args <- mapM tyFn ts
                                 b <- return $! fromVBit (foldl fromVFun v args)
@ -146,51 +174,41 @@ satProve isSat mSatNum (proverName, useSolverIte, verbose) edecls mfile (expr, s
                                           [ "attempted to evaluate bogus boolean for pretty-printing" ]
                   return (Right (esatexprs, modEnv), [])

-satProveOffline :: Bool
-                -> Bool
-                -> Bool
-                -> [DeclGroup]
-                -> Maybe FilePath
-                -> (Expr, Schema)
-                -> M.ModuleCmd ProverResult
-satProveOffline isSat useIte vrb edecls mfile (expr, schema) =
-  protectStack useIte $ \modEnv -> do
-    let extDgs = allDeclGroups modEnv ++ edecls
+satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String)
+satProveOffline ProverCommand {..} =
+  protectStack pcUseSolverIte (\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 useIte) extDgs
-           let v = evalExpr env expr
-           let satWord | isSat = "satisfiability"
-                       | otherwise = "validity"
-           txt <- SBV.compileToSMTLib True 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 (emptyEnv pcUseSolverIte) extDgs
+           let v = evalExpr env pcExpr
+           smtlib <- SBV.compileToSMTLib True isSat $ do
+             args <- mapM tyFn ts
+             b <- return $! fromVBit (foldl fromVFun v args)
+             return b
+           return (Right (Right smtlib, modEnv), [])
+{-
+-}

 protectStack :: Bool
-             -> M.ModuleCmd ProverResult
-             -> M.ModuleCmd ProverResult
-protectStack usingITE cmd modEnv = X.catchJust isOverflow (cmd modEnv) handler
+             -> (String -> M.ModuleCmd a)
+             -> M.ModuleCmd a
+             -> M.ModuleCmd a
+protectStack usingITE mkErr cmd modEnv =
+  X.catchJust isOverflow (cmd modEnv) handler
  where isOverflow X.StackOverflow = Just ()
        isOverflow _               = Nothing
        msg | usingITE  = msgBase
            | otherwise = msgBase ++ "\n" ++
                          "Using ':set iteSolver=on' might help."
        msgBase = "Symbolic evaluation failed to terminate."
-        handler () = return (Right (ProverError msg, modEnv), [])
+        handler () = mkErr msg modEnv -- (Right (ProverError msg, modEnv), [])

 parseValues :: [FinType] -> [SBV.CW] -> ([Eval.Value], [SBV.CW])
 parseValues [] cws = ([], cws)