Teach online what4 backend about smtFile option

This cargo-cults the existing code for making the offline `what4` backend and
uses it in the online `what4` backend, thereby fixing #1475. After this patch,
the test case in #1475 now produces an `.smt2` file, as expected.

CHANGES.md

@@ -30,7 +30,7 @@
 * Add a syntax highlight file for Vim,
   available in `syntax-highlight/cryptol.vim`
 
-* Add `:new-seed` and `:set-seed` commands to the REPL. 
+* Add `:new-seed` and `:set-seed` commands to the REPL.
   These affect random test generation,
   and help write reproducable Cryptol scripts.
 
@@ -44,6 +44,9 @@
 
 * Improve documentation for `fromInteger` (#1465)
 
+* Fix a bug that caused Cryptol to ignore the `smtFile` setting when using the
+  What4 backend with an online SMT solver (#1476).
+
 # 2.13.0
 
 ## Language changes

cryptol-remote-api/src/CryptolServer/Sat.hs

@@ -23,6 +23,7 @@ import qualified Data.List as List
 import Data.Scientific (floatingOrInteger)
 import Data.Text (Text)
 import qualified Data.Text as T
+import System.IO (Handle)
 
 import Cryptol.Eval.Concrete (Value)
 import Cryptol.Eval.Type (TValue, tValTy)
@@ -121,12 +122,8 @@ offlineProveSat proverName cmd hConsing = do
     Right _w4Cfg -> do
       smtlibRef <- liftIO $ newIORef ("" :: Text)
       result <- liftModuleCmd $
-        W4.satProveOffline hConsing False cmd $ \f -> do
-          withRWTempFile "smtOutput.tmp" $ \h -> do
-            f h
-            hSeek h AbsoluteSeek 0
-            contents <- TIO.hGetContents h
-            writeIORef smtlibRef contents
+        W4.satProveOffline hConsing False cmd $ w4WriteSMTLibOutput
+                                              $ writeIORef smtlibRef
       case result of
         Just errMsg -> raise $ proverError $ "encountered an error using " ++ proverName ++ " to generate a query: " ++ errMsg
         Nothing -> do
@@ -151,6 +148,8 @@ onlineProveSat proverName cmd hConsing = do
       Right w4Cfg -> do
         (_firstProver, res) <-
           liftModuleCmd $ W4.satProve w4Cfg hConsing False {- warn uninterp fns -} cmd
+                        $ w4WriteSMTLibOutput
+                        $ \_ -> pure ()
         _stats <- liftIO (readIORef (pcProverStats cmd))
         pure res
   case res of
@@ -172,6 +171,18 @@ onlineProveSat proverName cmd hConsing = do
             Nothing -> error $ "type is not convertable: " ++ (show t)
             Just e -> pure (JSONType mempty (tValTy t), e)
 
+-- | Write SMT-Lib output using a What4-based backend.
+w4WriteSMTLibOutput ::
+  (Text -> IO ()) {- ^ Continuation for processing the contents of an SMT-Lib file -} ->
+  (Handle -> IO ()) {- ^ Continuation for writing file output -} ->
+  IO ()
+w4WriteSMTLibOutput put f =
+  withRWTempFile "smtOutput.tmp" $ \h -> do
+    f h
+    hSeek h AbsoluteSeek 0
+    contents <- TIO.hGetContents h
+    put contents
+
 data ProveSatResult
   = Unsatisfiable
   | Invalid CounterExampleType [(JSONType, Expression)]

src/Cryptol/REPL/Command.hs

@@ -478,14 +478,14 @@ qcExpr qcMode exprDoc texpr schema =
   do (val,ty) <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of
        Just res -> pure res
        -- If instance is not found, doesn't necessarily mean that there is no instance.
-       -- And due to nondeterminism in result from the solver (for finding solution to 
+       -- And due to nondeterminism in result from the solver (for finding solution to
        -- numeric type constraints), `:check` can get to this exception sometimes, but
        -- successfully find an instance and test with it other times.
        Nothing -> raise (InstantiationsNotFound schema)
      testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests"
      tenv <- E.envTypes . M.deEnv <$> getDynEnv
      let tyv = E.evalValType tenv ty
-     -- tv has already had polymorphism instantiated 
+     -- tv has already had polymorphism instantiated
      percentRef <- io $ newIORef Nothing
      testsRef <- io $ newIORef 0
 
@@ -852,7 +852,7 @@ proveSatExpr isSat rng exprDoc texpr schema = do
 printSafetyViolation :: T.Expr -> T.Schema -> [E.GenValue Concrete] -> REPL ()
 printSafetyViolation texpr schema vs =
     catch
-      (do fn <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of 
+      (do fn <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of
             Just (fn, _) -> pure fn
             Nothing -> raise (EvalPolyError schema)
           rEval (E.forceValue =<< foldM (\f v -> E.fromVFun Concrete f (pure v)) fn vs))
@@ -887,12 +887,15 @@ onlineProveSat proverName qtype expr schema mfile = do
         , pcSchema       = schema
         , pcIgnoreSafety = ignoreSafety
         }
+  put <- getPutStr
+
   (firstProver, res) <- getProverConfig >>= \case
        Left sbvCfg -> liftModuleCmd $ SBV.satProve sbvCfg cmd
        Right w4Cfg ->
          do ~(EnvBool hashConsing) <- getUser "hashConsing"
             ~(EnvBool warnUninterp) <- getUser "warnUninterp"
             liftModuleCmd $ W4.satProve w4Cfg hashConsing warnUninterp cmd
+                          $ w4WriteSMTLibOutput qtype mfile put
 
   stas <- io (readIORef timing)
   return (firstProver,res,stas)
@@ -917,50 +920,66 @@ offlineProveSat proverName qtype expr schema mfile = do
         , pcSchema       = schema
         , pcIgnoreSafety = ignoreSafety
         }
-
   put <- getPutStr
-  let putLn x = put (x ++ "\n")
-  let displayMsg =
-        do let filename = fromMaybe "standard output" mfile
-           let satWord = case qtype of
-                           SatQuery _  -> "satisfiability"
-                           ProveQuery  -> "validity"
-                           SafetyQuery -> "safety"
-           putLn $
-               "Writing to SMT-Lib file " ++ filename ++ "..."
-           putLn $
-             "To determine the " ++ satWord ++
-             " of the expression, use an external SMT solver."
 
   getProverConfig >>= \case
     Left sbvCfg ->
       do result <- liftModuleCmd $ SBV.satProveOffline sbvCfg cmd
          case result of
            Left msg -> rPutStrLn msg
            Right smtlib -> do
-             io $ displayMsg
+             io $ displayWriteSMTLibMsg qtype mfile put
              case mfile of
                Just path -> io $ writeFile path smtlib
                Nothing -> rPutStr smtlib
 
     Right _w4Cfg ->
       do ~(EnvBool hashConsing) <- getUser "hashConsing"
          ~(EnvBool warnUninterp) <- getUser "warnUninterp"
-         result <- liftModuleCmd $ W4.satProveOffline hashConsing warnUninterp cmd $ \f ->
-                     do displayMsg
-                        case mfile of
-                          Just path ->
-                            X.bracket (openFile path WriteMode) hClose f
-                          Nothing ->
-                            withRWTempFile "smtOutput.tmp" $ \h ->
-                              do f h
-                                 hSeek h AbsoluteSeek 0
-                                 hGetContents h >>= put
+         result <- liftModuleCmd $ W4.satProveOffline hashConsing warnUninterp cmd
+                                 $ w4WriteSMTLibOutput qtype mfile put
 
          case result of
            Just msg -> rPutStrLn msg
            Nothing -> return ()
 
+-- | Write SMT-Lib output using a What4-based backend.
+w4WriteSMTLibOutput ::
+  QueryType ->
+  Maybe FilePath ->
+  (String -> IO ()) {- ^ Continuation for displaying user messages -} ->
+  (Handle -> IO ()) {- ^ Continuation for writing file output -} ->
+  IO ()
+w4WriteSMTLibOutput qtype mfile put f =
+  do displayWriteSMTLibMsg qtype mfile put
+     case mfile of
+       Just path ->
+         X.bracket (openFile path WriteMode) hClose f
+       Nothing ->
+         withRWTempFile "smtOutput.tmp" $ \h ->
+           do f h
+              hSeek h AbsoluteSeek 0
+              hGetContents h >>= put
+
+-- | Display to the user a message indicating that SMT-Lib output is being
+-- written.
+displayWriteSMTLibMsg ::
+  QueryType ->
+  Maybe FilePath ->
+  (String -> IO ()) {- ^ Continuation for displaying user messages -} ->
+  IO ()
+displayWriteSMTLibMsg qtype mfile put =
+  do let putLn x = put (x ++ "\n")
+     let filename = fromMaybe "standard output" mfile
+     let satWord = case qtype of
+                     SatQuery _  -> "satisfiability"
+                     ProveQuery  -> "validity"
+                     SafetyQuery -> "safety"
+     putLn $
+         "Writing to SMT-Lib file " ++ filename ++ "..."
+     putLn $
+       "To determine the " ++ satWord ++
+       " of the expression, use an external SMT solver."
 
 rIdent :: M.Ident
 rIdent  = M.packIdent "result"
@@ -1602,12 +1621,12 @@ moduleCmdResult (res,ws0) = do
 
       -- ignore certain warnings during typechecking
       filterTypecheck :: M.ModuleWarning -> Maybe M.ModuleWarning
-      filterTypecheck (M.TypeCheckWarnings nameMap xs) = 
-        case filter (allow . snd) xs of 
+      filterTypecheck (M.TypeCheckWarnings nameMap xs) =
+        case filter (allow . snd) xs of
           [] -> Nothing
           ys -> Just (M.TypeCheckWarnings nameMap ys)
           where
-            allow :: T.Warning -> Bool 
+            allow :: T.Warning -> Bool
             allow = \case
               T.DefaultingTo _ _ | not warnDefaulting -> False
               T.NonExhaustivePropGuards _ | not warnNonExhConGrds -> False

src/Cryptol/Symbolic/What4.hs

@@ -371,9 +371,10 @@ satProve ::
   Bool {- ^ hash consing -} ->
   Bool {- ^ warn on uninterpreted functions -} ->
   ProverCommand ->
+  ((Handle -> IO ()) -> IO ()) ->
   M.ModuleCmd (Maybe String, ProverResult)
 
-satProve solverCfg hashConsing warnUninterp ProverCommand {..} =
+satProve solverCfg hashConsing warnUninterp ProverCommand {..} outputContinuation =
   protectStack proverError \modIn ->
   M.runModuleM modIn
   do w4sym   <- liftIO makeSym
@@ -411,7 +412,8 @@ satProve solverCfg hashConsing warnUninterp ProverCommand {..} =
   runProver sym logData primMap q =
     case q of
       Left msg -> pure (Nothing, ProverError msg)
-      Right (ts,args,safety,query) ->
+      Right (ts,args,safety,query) -> do
+        liftIO $ outputContinuation (\hdl -> W4.writeZ3SMT2File (w4 sym) hdl [query])
         case pcQueryType of
           ProveQuery ->
             singleQuery sym solverCfg primMap logData ts args (Just safety) query