Fixes #1167

This requires newer version simple-smt, which supports calling back into the program when the solver exits
GaloisInc · Jul 21, 2021 · 816523d · 816523d
1 parent ce647eb
commit 816523d
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 7 deletions.
diff --git a/cryptol.cabal b/cryptol.cabal
@@ -65,7 +65,7 @@ library
                        pretty            >= 1.1,
                        process           >= 1.2,
                        sbv               >= 8.6 && < 8.15,
-                       simple-smt        >= 0.7.1,
+                       simple-smt        >= 0.9.7,
                        stm               >= 2.4,
                        strict,
                        text              >= 1.1,
@@ -231,6 +231,7 @@ executable cryptol
                      , directory
                      , filepath
                      , haskeline >= 0.7 && < 0.9
+                     , exceptions
                      , monad-control
                      , text
                      , transformers

diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs
@@ -415,13 +415,18 @@ getPrompt  = mkPrompt `fmap` getRW
 getCallStacks :: REPL Bool
 getCallStacks = eCallStacks <$> getRW
 
+clearTCSolverAction :: REPL (IO ())
+clearTCSolverAction =
+  REPL (\ref -> pure (modifyIORef ref (\rw -> rw { eTCSolver = Nothing })))
+
 getTCSolver :: REPL SMT.Solver
 getTCSolver =
   do rw <- getRW
      case eTCSolver rw of
        Just s -> return s
        Nothing ->
-         do s <- io (SMT.startSolver (eTCConfig rw))
+         do onExit <- clearTCSolverAction
+            s <- io (SMT.startSolver onExit (eTCConfig rw))
             modifyRW_ (\rw' -> rw'{ eTCSolver = Just s })
             return s
 

diff --git a/src/Cryptol/TypeCheck/Solver/SMT.hs b/src/Cryptol/TypeCheck/Solver/SMT.hs
@@ -69,13 +69,14 @@ data Solver = Solver
 
 
 -- | Start a fresh solver instance
-startSolver :: SolverConfig -> IO Solver
-startSolver SolverConfig { .. } =
+startSolver :: IO () -> SolverConfig -> IO Solver
+startSolver onExit SolverConfig { .. } =
    do logger <- if solverVerbose > 0 then SMT.newLogger 0
 
                                      else return quietLogger
       let smtDbg = if solverVerbose > 1 then Just logger else Nothing
-      solver <- SMT.newSolver solverPath solverArgs smtDbg
+      solver <- SMT.newSolverNotify
+                    solverPath solverArgs smtDbg (Just (const onExit))
       _ <- SMT.setOptionMaybe solver ":global-decls" "false"
       -- SMT.setLogic solver "QF_LIA"
       let sol = Solver { .. }
@@ -95,8 +96,8 @@ stopSolver :: Solver -> IO ()
 stopSolver s = void $ SMT.stop (solver s)
 
 -- | Execute a computation with a fresh solver instance.
-withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
-withSolver cfg = bracket (startSolver cfg) stopSolver
+withSolver :: IO () -> SolverConfig -> (Solver -> IO a) -> IO a
+withSolver onExit cfg = bracket (startSolver onExit cfg) stopSolver
 
 -- | Load the definitions used for type checking.
 loadTcPrelude :: Solver -> [FilePath] {- ^ Search in this paths -} -> IO ()