Skip to content

Commit

Permalink
fix(rpc): reset TC solver on file/module load (#1258)
Browse files Browse the repository at this point in the history
* fix(rpc): reset TC solver on file/module load

Some difficult to reproduce bugs regarding the RPC server hanging
(#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).
  • Loading branch information
Andrew Kent authored Jul 28, 2021
1 parent 1b52a35 commit 03311ce
Show file tree
Hide file tree
Showing 3 changed files with 34 additions and 12 deletions.
15 changes: 13 additions & 2 deletions cryptol-remote-api/src/CryptolServer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -123,6 +126,7 @@ data ServerState =
ServerState { _loadedModule :: Maybe LoadedModule
, _moduleEnv :: ModuleEnv
, _tcSolver :: SMT.Solver
, solverConfig :: SMT.SolverConfig
}

loadedModule :: Lens' ServerState (Maybe LoadedModule)
Expand All @@ -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
Expand Down
6 changes: 4 additions & 2 deletions cryptol-remote-api/src/CryptolServer/LoadModule.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
25 changes: 17 additions & 8 deletions src/Cryptol/TypeCheck/Solver/SMT.hs
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,12 @@
module Cryptol.TypeCheck.Solver.SMT
( -- * Setup
Solver
, SolverConfig
, withSolver
, startSolver
, stopSolver
, isNumeric
, resetSolver

-- * Debugging
, debugBlock
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit 03311ce

Please sign in to comment.