From 8205401bb13f31447c1feb891a39608d2f7c217b Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 9 Dec 2024 10:17:13 -0500 Subject: [PATCH] Add a tcSmtFile REPL option `tcSmtFile` is to `tcSolver` as `smtFile` is to `prover`. The `tcSmtFile` option allows users to record typechecker-related SMT solver interactions to a file. This requires using a more recent `simple-smt` version to bring in the changes from https://github.com/yav/simple-smt/pull/25 and https://github.com/yav/simple-smt/pull/27, which are needed to plumb the relevant information down to the `simple-smt` API. Fixes #1782. --- CHANGES.md | 3 ++ cabal.project | 7 +++++ src/Cryptol/REPL/Monad.hs | 11 ++++++++ src/Cryptol/TypeCheck/InferTypes.hs | 6 +++- src/Cryptol/TypeCheck/Solver/SMT.hs | 43 +++++++++++++++++++++++------ 5 files changed, 61 insertions(+), 9 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 11ffd01cd..e9e074c96 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -24,6 +24,9 @@ * The REPL properly supports tab completion for the `:t` and `:check` commands. ([#1780](https://github.com/GaloisInc/cryptol/issues/1780)) +* Add a REPL option `tcSmtFile` that allows writing typechecker-related SMT + solver interactions to a file. + # 3.2.0 -- 2024-08-20 ## Language changes diff --git a/cabal.project b/cabal.project index d8665fc91..80da5b8a8 100644 --- a/cabal.project +++ b/cabal.project @@ -3,3 +3,10 @@ packages: cryptol-remote-api tests deps/argo/argo + +-- TODO RGS: Remove this once the changes from +-- https://github.com/yav/simple-smt/pull/27 are released to Hackage +source-repository-package + type: git + location: https://github.com/RyanGlScott/simple-smt + tag: 519d76a51c3c992120c69532f76311d7ac16718c diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 47900b1ac..e76350492 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -972,6 +972,17 @@ userOptions = mkOptionMap setModuleEnv me { M.meMonoBinds = b } _ -> return () + , OptionDescr "tcSmtFile" ["tc-smt-file"] (EnvString "-") noCheck + (unlines + [ "The file to record SMT solver interactions in the type checker (for debugging or offline proving)." + , "Use \"-\" for stdout." ]) $ + \case EnvString fileName -> do let mfile = if fileName == "-" then Nothing else Just fileName + modifyRW_ (\rw -> rw { eTCConfig = (eTCConfig rw) + { T.solverSmtFile = mfile + }}) + resetTCSolver + _ -> return () + , OptionDescr "tcSolver" ["tc-solver"] (EnvProg "z3" [ "-smt2", "-in" ]) noCheck -- TODO: check for the program in the path "The solver that will be used by the type checker." $ diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs index 0b8199f16..171d4f431 100644 --- a/src/Cryptol/TypeCheck/InferTypes.hs +++ b/src/Cryptol/TypeCheck/InferTypes.hs @@ -45,6 +45,9 @@ data SolverConfig = SolverConfig , solverVerbose :: Int -- ^ How verbose to be when type-checking , solverPreludePath :: [FilePath] -- ^ Look for the solver prelude in these locations. + , solverSmtFile :: Maybe FilePath + -- ^ The optional file to record SMT solver interactions in the type + -- checker. If 'Nothing', this will print to @stdout@ instead. } deriving (Show, Generic, NFData) @@ -58,6 +61,7 @@ defaultSolverConfig searchPath = , solverArgs = [ "-smt2", "-in" ] , solverVerbose = 0 , solverPreludePath = searchPath + , solverSmtFile = Nothing } -- | The types of variables in the environment. @@ -389,7 +393,7 @@ instance PP (WithNames DelayedCt) where ppPrec _ (WithNames d names) = sig $$ hang "we need to show that" - 2 (vcat ( vars ++ asmps ++ + 2 (vcat ( vars ++ asmps ++ [ hang "the following constraints hold:" 2 (vcat $ bullets diff --git a/src/Cryptol/TypeCheck/Solver/SMT.hs b/src/Cryptol/TypeCheck/Solver/SMT.hs index 7cba94637..d8f67ae9b 100644 --- a/src/Cryptol/TypeCheck/Solver/SMT.hs +++ b/src/Cryptol/TypeCheck/Solver/SMT.hs @@ -41,12 +41,13 @@ import qualified SimpleSMT as SMT import Data.Map ( Map ) import qualified Data.Map as Map import qualified Data.Set as Set -import Data.Maybe(catMaybes) +import Data.Maybe(catMaybes,isJust) import Data.List(partition) import Control.Exception import Control.Monad(msum,zipWithM,void) import Data.Char(isSpace) import Text.Read(readMaybe) +import System.IO(IOMode(..), hClose, openFile) import qualified System.IO.Strict as StrictIO import System.FilePath(()) import System.Directory(doesFileExist) @@ -80,12 +81,38 @@ setupSolver s cfg = do -- | Start a fresh solver instance startSolver :: IO () -> SolverConfig -> IO Solver startSolver onExit sCfg = - do logger <- if (solverVerbose sCfg) > 0 then SMT.newLogger 0 - - else return quietLogger - let smtDbg = if (solverVerbose sCfg) > 1 then Just logger else Nothing - solver <- SMT.newSolverNotify - (solverPath sCfg) (solverArgs sCfg) smtDbg (Just (const onExit)) + do let smtFileEnabled = isJust (solverSmtFile sCfg) + (logger, mbLoggerCloseHdl) <- + -- There are two scenarios under which we want to explicitly log SMT + -- solver interactions: + -- + -- 1. The user wants to debug-print interactions with the `tcDebug` + -- option + -- 2. The user wants to write interactions to the `tcSmtFile` option + -- + -- We enable logging if either one is true. + if (solverVerbose sCfg) > 0 || smtFileEnabled + then case solverSmtFile sCfg of + Nothing -> + do logger <- SMT.newLogger 0 + pure (logger, Nothing) + Just file -> + do loggerHdl <- openFile file WriteMode + logger <- SMT.newLoggerWithHandle loggerHdl 0 + pure (logger, Just (hClose loggerHdl)) + else pure (quietLogger, Nothing) + let smtDbg = if (solverVerbose sCfg) > 1 || smtFileEnabled + then Just logger + else Nothing + solver <- SMT.newSolverWithConfig + (SMT.defaultConfig (solverPath sCfg) (solverArgs sCfg)) + { SMT.solverOnExit = + Just $ \_exitCode -> + do onExit + sequence_ mbLoggerCloseHdl + , SMT.solverLogger = + maybe SMT.noSolverLogger SMT.smtSolverLogger smtDbg + } let sol = Solver solver logger setupSolver sol sCfg return sol @@ -150,7 +177,7 @@ loadString s str = go (dropComments str) debugBlock :: Solver -> String -> IO a -> IO a debugBlock s@Solver { .. } name m = - do debugLog s name + do debugLog s (";;; " ++ name) SMT.logTab logger a <- m SMT.logUntab logger