From 03311cec9e4f8dda1aaf5fe35256d99e06438a3d Mon Sep 17 00:00:00 2001
From: Andrew Kent <andrew@galois.com>
Date: Wed, 28 Jul 2021 14:07:23 -0700
Subject: [PATCH] fix(rpc): reset TC solver on file/module load (#1258)

* fix(rpc): reset TC solver on file/module load

Some difficult to reproduce bugs regarding the RPC server hanging
(https://github.com/GaloisInc/cryptol/issues/1250) seemed to be
related to the type checker solver (Z3) hanging after periods of
extended use. I.e., a module would load/error quickly normally,
but if preceded by enough prior solver/server activity, Z3
would consistently hang. To avoid this, we can simply reset the
solver and reload the type checker prelude when the server is asked
to load a file or module. This solves the Z3 hang issues in observed
cases and requires no additional forking (which we're trying to
minimize when possible).
---
 cryptol-remote-api/src/CryptolServer.hs       | 15 +++++++++--
 .../src/CryptolServer/LoadModule.hs           |  6 +++--
 src/Cryptol/TypeCheck/Solver/SMT.hs           | 25 +++++++++++++------
 3 files changed, 34 insertions(+), 12 deletions(-)

diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs
index 582e3b2e6..ab7406ea1 100644
--- a/cryptol-remote-api/src/CryptolServer.hs
+++ b/cryptol-remote-api/src/CryptolServer.hs
@@ -85,6 +85,9 @@ modifyModuleEnv f =
 getTCSolver :: CryptolCommand SMT.Solver
 getTCSolver = CryptolCommand $ const $ view tcSolver <$> Argo.getState
 
+getTCSolverConfig :: CryptolCommand SMT.SolverConfig
+getTCSolverConfig = CryptolCommand $ const $ solverConfig <$> Argo.getState
+
 liftModuleCmd :: ModuleCmd a -> CryptolCommand a
 liftModuleCmd cmd =
     do Options callStacks evOpts <- getOptions
@@ -123,6 +126,7 @@ data ServerState =
   ServerState { _loadedModule :: Maybe LoadedModule
               , _moduleEnv :: ModuleEnv
               , _tcSolver :: SMT.Solver
+              , solverConfig :: SMT.SolverConfig
               }
 
 loadedModule :: Lens' ServerState (Maybe LoadedModule)
@@ -141,14 +145,21 @@ initialState =
      -- NOTE: the "pure ()" is a callback which is invoked if/when the solver
      -- stops for some reason.  This is just a placeholder for now, and could
      -- be replaced by something more useful.
-     s <- SMT.startSolver (pure ()) (defaultSolverConfig (meSearchPath modEnv))
-     pure (ServerState Nothing modEnv s)
+     let sCfg = defaultSolverConfig (meSearchPath modEnv)
+     s <- SMT.startSolver (pure ()) sCfg
+     pure (ServerState Nothing modEnv s sCfg)
 
 extendSearchPath :: [FilePath] -> ServerState -> ServerState
 extendSearchPath paths =
   over moduleEnv $ \me -> me { meSearchPath = nubOrd $ paths ++ meSearchPath me }
 
 
+resetTCSolver :: CryptolCommand ()
+resetTCSolver = do
+  s <- getTCSolver
+  sCfg <- getTCSolverConfig
+  liftIO $ SMT.resetSolver s sCfg
+
 instance FreshM CryptolCommand where
   liftSupply f = do
     serverState <- CryptolCommand $ const Argo.getState
diff --git a/cryptol-remote-api/src/CryptolServer/LoadModule.hs b/cryptol-remote-api/src/CryptolServer/LoadModule.hs
index 4f29aa001..63294f6d1 100644
--- a/cryptol-remote-api/src/CryptolServer/LoadModule.hs
+++ b/cryptol-remote-api/src/CryptolServer/LoadModule.hs
@@ -25,7 +25,8 @@ loadFileDescr :: Doc.Block
 loadFileDescr = Doc.Paragraph [Doc.Text "Load the specified module (by file path)."]
 
 loadFile :: LoadFileParams -> CryptolCommand ()
-loadFile (LoadFileParams fn) =
+loadFile (LoadFileParams fn) = do
+  resetTCSolver
   void $ liftModuleCmd (loadModuleByPath fn)
 
 newtype LoadFileParams
@@ -49,7 +50,8 @@ loadModuleDescr :: Doc.Block
 loadModuleDescr = Doc.Paragraph [Doc.Text "Load the specified module (by name)."]
 
 loadModule :: LoadModuleParams -> CryptolCommand ()
-loadModule (LoadModuleParams mn) =
+loadModule (LoadModuleParams mn) = do
+  resetTCSolver
   void $ liftModuleCmd (loadModuleByName mn)
 
 newtype JSONModuleName
diff --git a/src/Cryptol/TypeCheck/Solver/SMT.hs b/src/Cryptol/TypeCheck/Solver/SMT.hs
index ba81cab0e..4e738dd01 100644
--- a/src/Cryptol/TypeCheck/Solver/SMT.hs
+++ b/src/Cryptol/TypeCheck/Solver/SMT.hs
@@ -15,10 +15,12 @@
 module Cryptol.TypeCheck.Solver.SMT
   ( -- * Setup
     Solver
+  , SolverConfig
   , withSolver
   , startSolver
   , stopSolver
   , isNumeric
+  , resetSolver
 
     -- * Debugging
   , debugBlock
@@ -67,20 +69,22 @@ data Solver = Solver
     -- ^ For debugging
   }
 
+setupSolver :: Solver -> SolverConfig -> IO ()
+setupSolver s cfg = do
+  _ <- SMT.setOptionMaybe (solver s) ":global-decls" "false"
+  loadTcPrelude s (solverPreludePath cfg)
 
 -- | Start a fresh solver instance
 startSolver :: IO () -> SolverConfig -> IO Solver
-startSolver onExit SolverConfig { .. } =
-   do logger <- if solverVerbose > 0 then SMT.newLogger 0
+startSolver onExit sCfg =
+   do logger <- if (solverVerbose sCfg) > 0 then SMT.newLogger 0
 
                                      else return quietLogger
-      let smtDbg = if solverVerbose > 1 then Just logger else Nothing
+      let smtDbg = if (solverVerbose sCfg) > 1 then Just logger else Nothing
       solver <- SMT.newSolverNotify
-                    solverPath solverArgs smtDbg (Just (const onExit))
-      _ <- SMT.setOptionMaybe solver ":global-decls" "false"
-      -- SMT.setLogic solver "QF_LIA"
-      let sol = Solver { .. }
-      loadTcPrelude sol solverPreludePath
+                    (solverPath sCfg) (solverArgs sCfg) smtDbg (Just (const onExit))
+      let sol = Solver solver logger
+      setupSolver sol sCfg
       return sol
 
   where
@@ -95,6 +99,11 @@ startSolver onExit SolverConfig { .. } =
 stopSolver :: Solver -> IO ()
 stopSolver s = void $ SMT.stop (solver s)
 
+resetSolver :: Solver -> SolverConfig -> IO ()
+resetSolver s sCfg = do
+  _ <- SMT.simpleCommand (solver s) ["reset"]
+  setupSolver s sCfg
+
 -- | Execute a computation with a fresh solver instance.
 withSolver :: IO () -> SolverConfig -> (Solver -> IO a) -> IO a
 withSolver onExit cfg = bracket (startSolver onExit cfg) stopSolver