Merge pull request #1075 from GaloisInc/persist-solver

Persist solver

cryptol-remote-api/cryptol-eval-server/Main.hs

@@ -12,9 +12,10 @@ import System.IO (hPutStrLn, stderr)
 import Options.Applicative
 
 import Cryptol.Eval (EvalOpts(..), defaultPPOpts)
-import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName)
+import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName, meSolverConfig)
 import Cryptol.ModuleSystem.Monad (runModuleM, setFocusedModule)
 import Cryptol.TypeCheck.AST (mName)
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import Cryptol.Utils.Ident (ModName, modNameToText, textToModName, preludeName)
 import Cryptol.Utils.Logger (quietLogger)
 
@@ -41,18 +42,18 @@ main = customMain initMod initMod initMod initMod description buildApp
       do paths <- getSearchPaths
          initSt <- setSearchPath paths <$> initialState
          let menv = view moduleEnv initSt
-         let minp = ModuleInput False (pure evOpts) reader menv
+         let minp s = ModuleInput False (pure evOpts) reader menv s
          let die =
                \err ->
                  do hPutStrLn stderr $ "Failed to load " ++ either ("file " ++) (("module " ++) . show) file ++ ":\n" ++ show err
                     exitFailure
-         menv' <-
-           do (res, _warnings) <- either loadModuleByPath loadModuleByName file minp
+         menv' <- SMT.withSolver (meSolverConfig menv) $ \s ->
+           do (res, _warnings) <- either loadModuleByPath loadModuleByName file (minp s)
               -- NB Warnings suppressed when running server
               case res of
                 Left err -> die err
                 Right (m, menv') ->
-                  do res' <- fst <$> runModuleM minp { minpModuleEnv = menv' } (setFocusedModule (mName (snd m)))
+                  do res' <- fst <$> runModuleM (minp s){ minpModuleEnv = menv' } (setFocusedModule (mName (snd m)))
                      case res' of
                        Left err -> die err
                        Right (_, menv'') -> pure menv''

src/Cryptol/ModuleSystem/Base.hs

@@ -40,6 +40,7 @@ import qualified Cryptol.TypeCheck     as T
 import qualified Cryptol.TypeCheck.AST as T
 import qualified Cryptol.TypeCheck.PP as T
 import qualified Cryptol.TypeCheck.Sanity as TcSanity
+
 import Cryptol.Transform.AddModParams (addModParams)
 import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
                            , preludeReferenceName, interactiveName, modNameChunks
@@ -527,12 +528,12 @@ typecheck act i params env = do
          typeCheckingFailed nameMap errs
 
 -- | Generate input for the typechecker.
-genInferInput :: Range -> PrimMap ->
-                          IfaceParams -> IfaceDecls -> ModuleM T.InferInput
+genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM T.InferInput
 genInferInput r prims params env = do
   seeds <- getNameSeeds
   monoBinds <- getMonoBinds
   cfg <- getSolverConfig
+  solver <- getTCSolver
   supply <- getSupply
   searchPath <- getSearchPath
   callStacks <- getCallStacks
@@ -554,10 +555,10 @@ genInferInput r prims params env = do
     , T.inpParamTypes       = ifParamTypes params
     , T.inpParamConstraints = ifParamConstraints params
     , T.inpParamFuns        = ifParamFuns params
+    , T.inpSolver           = solver
     }
 
 
-
 -- Evaluation ------------------------------------------------------------------
 
 evalExpr :: T.Expr -> ModuleM Concrete.Value

src/Cryptol/ModuleSystem/Monad.hs

@@ -29,6 +29,8 @@ import qualified Cryptol.Parser.NoPat as NoPat
 import qualified Cryptol.Parser.NoInclude as NoInc
 import qualified Cryptol.TypeCheck as T
 import qualified Cryptol.TypeCheck.AST as T
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
+
 import           Cryptol.Parser.Position (Range)
 import           Cryptol.Utils.Ident (interactiveName, noModuleName)
 import           Cryptol.Utils.PP
@@ -304,6 +306,7 @@ data RO m =
      , roEvalOpts   :: m EvalOpts
      , roCallStacks :: Bool
      , roFileReader :: FilePath -> m ByteString
+     , roTCSolver   :: SMT.Solver
      }
 
 emptyRO :: ModuleInput m -> RO m
@@ -312,6 +315,7 @@ emptyRO minp =
      , roEvalOpts   = minpEvalOpts minp
      , roCallStacks = minpCallStacks minp
      , roFileReader = minpByteReader minp
+     , roTCSolver   = minpTCSolver minp
      }
 
 newtype ModuleT m a = ModuleT
@@ -364,6 +368,7 @@ data ModuleInput m =
   , minpEvalOpts   :: m EvalOpts
   , minpByteReader :: FilePath -> m ByteString
   , minpModuleEnv  :: ModuleEnv
+  , minpTCSolver   :: SMT.Solver
   }
 
 runModuleT ::
@@ -406,6 +411,9 @@ readBytes fn = do
 getModuleEnv :: Monad m => ModuleT m ModuleEnv
 getModuleEnv = ModuleT get
 
+getTCSolver :: Monad m => ModuleT m SMT.Solver
+getTCSolver = ModuleT (roTCSolver <$> ask)
+
 setModuleEnv :: Monad m => ModuleEnv -> ModuleT m ()
 setModuleEnv = ModuleT . set
 

src/Cryptol/REPL/Command.hs

@@ -1648,13 +1648,16 @@ liftModuleCmd cmd =
   do evo <- getEvalOptsAction
      env <- getModuleEnv
      callStacks <- getCallStacks
-     let minp = M.ModuleInput
+     let cfg = M.meSolverConfig env
+     let minp s =
+             M.ModuleInput
                 { minpCallStacks = callStacks
                 , minpEvalOpts   = evo
                 , minpByteReader = BS.readFile
                 , minpModuleEnv  = env
+                , minpTCSolver   = s
                 }
-     moduleCmdResult =<< io (cmd minp)
+     moduleCmdResult =<< io (SMT.withSolver cfg (cmd . minp))
 
 moduleCmdResult :: M.ModuleRes a -> REPL a
 moduleCmdResult (res,ws0) = do

src/Cryptol/TypeCheck.hs

@@ -52,6 +52,8 @@ import           Cryptol.Utils.Ident (exprModName,packIdent)
 import           Cryptol.Utils.PP
 import           Cryptol.Utils.Panic(panic)
 
+
+
 tcModule :: P.Module Name -> InferInput -> IO (InferOutput Module)
 tcModule m inp = runInferM inp (inferModule m)
 

src/Cryptol/TypeCheck/InferTypes.hs

@@ -47,6 +47,7 @@ data SolverConfig = SolverConfig
     -- ^ Look for the solver prelude in these locations.
   } deriving (Show, Generic, NFData)
 
+
 -- | The types of variables in the environment.
 data VarType = ExtVar Schema
                -- ^ Known type

src/Cryptol/TypeCheck/Monad.hs

@@ -85,8 +85,9 @@ data InferInput = InferInput
     -- identifier (e.g., @number@).
 
   , inpSupply :: !Supply              -- ^ The supply for fresh name generation
-  } deriving Show
 
+  , inpSolver :: SMT.Solver           -- ^ Solver connection for typechecking
+  }
 
 -- | This is used for generating various names.
 data NameSeeds = NameSeeds
@@ -116,7 +117,7 @@ bumpCounter = do RO { .. } <- IM ask
                  io $ modifyIORef' iSolveCounter (+1)
 
 runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
-runInferM info (IM m) = SMT.withSolver (inpSolverConfig info) $ \solver ->
+runInferM info (IM m) =
   do counter <- newIORef 0
      rec ro <- return RO { iRange     = inpRange info
                          , iVars          = Map.map ExtVar (inpVars info)
@@ -131,7 +132,7 @@ runInferM info (IM m) = SMT.withSolver (inpSolverConfig info) $ \solver ->
                          , iSolvedHasLazy = iSolvedHas finalRW     -- RECURSION
                          , iMonoBinds     = inpMonoBinds info
                          , iCallStacks    = inpCallStacks info
-                         , iSolver        = solver
+                         , iSolver        = inpSolver info
                          , iPrimNames     = inpPrimNames info
                          , iSolveCounter  = counter
                          }

src/Cryptol/TypeCheck/Solver/SMT.hs

@@ -16,6 +16,8 @@ module Cryptol.TypeCheck.Solver.SMT
   ( -- * Setup
     Solver
   , withSolver
+  , startSolver
+  , stopSolver
   , isNumeric
 
     -- * Debugging
@@ -65,20 +67,19 @@ data Solver = Solver
     -- ^ For debugging
   }
 
--- | Execute a computation with a fresh solver instance.
-withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
-withSolver SolverConfig{ .. } =
-     bracket
-       (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
-           _ <- SMT.setOptionMaybe solver ":global-decls" "false"
-           -- SMT.setLogic solver "QF_LIA"
-           let sol = Solver { .. }
-           loadTcPrelude sol solverPreludePath
-           return sol)
-       (\s -> void $ SMT.stop (solver s))
+-- | Start a fresh solver instance
+startSolver :: SolverConfig -> IO Solver
+startSolver 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
+      _ <- SMT.setOptionMaybe solver ":global-decls" "false"
+      -- SMT.setLogic solver "QF_LIA"
+      let sol = Solver { .. }
+      loadTcPrelude sol solverPreludePath
+      return sol
 
   where
   quietLogger = SMT.Logger { SMT.logMessage = \_ -> return ()
@@ -88,6 +89,13 @@ withSolver SolverConfig{ .. } =
                            , SMT.logUntab   = return ()
                            }
 
+-- | Shut down a solver instance
+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
 
 -- | Load the definitions used for type checking.
 loadTcPrelude :: Solver -> [FilePath] {- ^ Search in this paths -} -> IO ()
@@ -388,8 +396,3 @@ instance Mk (Type,Type,Type) where
   mk tvs f (x,y,z) = SMT.fun f [ toSMT tvs x, toSMT tvs y, toSMT tvs z ]
 
 --------------------------------------------------------------------------------
-
-
-
-
-