mirror of
https://github.com/GaloisInc/cryptol.git
synced 2025-01-05 15:07:12 +03:00
spawn fewer solver instances during typechecking
This appears to increase performance of the test and benchmark suites substantially, but there may be more opportunities to cut down on the number of solver instances.
This commit is contained in:
Adam C. Foltzer
parent
5c80fc2e1c
commit
1d2a135e44
2
Makefile
2
Makefile
@ -232,7 +232,7 @@ ${CS_BIN}/cryptol-test-runner: \
|
||||
test: ${CS_BIN}/cryptol-test-runner
|
||||
( cd tests && \
|
||||
echo "Testing on $(UNAME)-$(ARCH)" && \
|
||||
$(realpath $(CS_BIN)/cryptol-test-runner) \
|
||||
time $(realpath $(CS_BIN)/cryptol-test-runner) \
|
||||
$(TESTS) \
|
||||
-c $(call adjust-path,${CURDIR}/${PKG_BIN}/cryptol${EXE_EXT}) \
|
||||
-r output \
|
||||
|
||||
@ -66,6 +66,7 @@ import qualified Cryptol.TypeCheck.AST as T
|
||||
import qualified Cryptol.TypeCheck.Subst as T
|
||||
import qualified Cryptol.TypeCheck.InferTypes as T
|
||||
import Cryptol.TypeCheck.Solve(defaultReplExpr)
|
||||
import qualified Cryptol.TypeCheck.Solver.CrySAT as CrySAT
|
||||
import Cryptol.TypeCheck.PP (dump,ppWithNames)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
@ -889,7 +890,7 @@ replEvalExpr expr =
|
||||
|
||||
me <- getModuleEnv
|
||||
let cfg = M.meSolverConfig me
|
||||
mbDef <- io (defaultReplExpr cfg def sig)
|
||||
mbDef <- io $ CrySAT.withSolver cfg (\s -> defaultReplExpr s def sig)
|
||||
|
||||
(def1,ty) <-
|
||||
case mbDef of
|
||||
|
||||
@ -706,8 +706,8 @@ generalize bs0 gs0 =
|
||||
when (not (null ambig)) $ recordError $ AmbiguousType $ map dName bs
|
||||
|
||||
|
||||
cfg <- getSolverConfig
|
||||
(as0,here1,defSu,ws) <- io $ improveByDefaulting cfg maybeAmbig here0
|
||||
solver <- getSolver
|
||||
(as0,here1,defSu,ws) <- io $ improveByDefaultingWith solver maybeAmbig here0
|
||||
mapM_ recordWarning ws
|
||||
let here = map goal here1
|
||||
|
||||
@ -810,8 +810,8 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
|
||||
when (not (null ambig)) $ recordError
|
||||
$ AmbiguousType [ thing (P.bName b) ]
|
||||
|
||||
cfg <- getSolverConfig
|
||||
(_,_,defSu2,ws) <- io $ improveByDefaulting cfg maybeAmbig later
|
||||
solver <- getSolver
|
||||
(_,_,defSu2,ws) <- io $ improveByDefaultingWith solver maybeAmbig later
|
||||
mapM_ recordWarning ws
|
||||
extendSubst defSu2
|
||||
|
||||
|
||||
@ -20,9 +20,12 @@ import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Subst
|
||||
import Cryptol.TypeCheck.Unify(mgu, Result(..), UnificationError(..))
|
||||
import Cryptol.TypeCheck.InferTypes
|
||||
import qualified Cryptol.TypeCheck.Solver.CrySAT as CrySAT
|
||||
import Cryptol.Utils.PP(pp, (<+>), Doc, text, quotes)
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
|
||||
import qualified Control.Applicative as A
|
||||
import Control.Monad.Fix(MonadFix(..))
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import Data.Map (Map)
|
||||
@ -31,8 +34,6 @@ import Data.List(find, minimumBy, groupBy, sortBy)
|
||||
import Data.Maybe(mapMaybe)
|
||||
import Data.Function(on)
|
||||
import MonadLib hiding (mapM)
|
||||
import qualified Control.Applicative as A
|
||||
import Control.Monad.Fix(MonadFix(..))
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq.Generics
|
||||
@ -86,7 +87,7 @@ data InferOutput a
|
||||
deriving Show
|
||||
|
||||
runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
|
||||
runInferM info (IM m) =
|
||||
runInferM info (IM m) = CrySAT.withSolver (inpSolverConfig info) $ \solver ->
|
||||
do rec ro <- return RO { iRange = inpRange info
|
||||
, iVars = Map.map ExtVar (inpVars info)
|
||||
, iTVars = []
|
||||
@ -94,7 +95,7 @@ runInferM info (IM m) =
|
||||
, iNewtypes = fmap mkExternal (inpNewtypes info)
|
||||
, iSolvedHasLazy = iSolvedHas finalRW -- RECURSION
|
||||
, iMonoBinds = inpMonoBinds info
|
||||
, iSolverConfig = inpSolverConfig info
|
||||
, iSolver = solver
|
||||
, iPrimNames = inpPrimNames info
|
||||
}
|
||||
|
||||
@ -187,7 +188,7 @@ data RO = RO
|
||||
-- in where-blocks will never be generalized. Bindings with type
|
||||
-- signatures, and all bindings at top level are unaffected.
|
||||
|
||||
, iSolverConfig :: SolverConfig
|
||||
, iSolver :: CrySAT.Solver
|
||||
|
||||
, iPrimNames :: !PrimMap
|
||||
}
|
||||
@ -270,10 +271,10 @@ recordWarning w =
|
||||
do r <- curRange
|
||||
IM $ sets_ $ \s -> s { iWarnings = (r,w) : iWarnings s }
|
||||
|
||||
getSolverConfig :: InferM SolverConfig
|
||||
getSolverConfig =
|
||||
getSolver :: InferM CrySAT.Solver
|
||||
getSolver =
|
||||
do RO { .. } <- IM ask
|
||||
return iSolverConfig
|
||||
return iSolver
|
||||
|
||||
-- | Retrieve the mapping between identifiers and declarations in the prelude.
|
||||
getPrimMap :: InferM PrimMap
|
||||
|
||||
@ -13,7 +13,7 @@ module Cryptol.TypeCheck.Solve
|
||||
, proveImplication
|
||||
, wfType
|
||||
, wfTypeFunction
|
||||
, improveByDefaulting
|
||||
, improveByDefaultingWith
|
||||
, defaultReplExpr
|
||||
, simpType
|
||||
, simpTypeMaybe
|
||||
@ -86,8 +86,8 @@ simplifyAllConstraints :: InferM ()
|
||||
simplifyAllConstraints =
|
||||
do mapM_ tryHasGoal =<< getHasGoals
|
||||
gs <- getGoals
|
||||
cfg <- getSolverConfig
|
||||
(mb,su) <- io (Num.withSolver cfg (`simpGoals'` gs))
|
||||
solver <- getSolver
|
||||
(mb,su) <- io (simpGoals' solver gs)
|
||||
extendSubst su
|
||||
case mb of
|
||||
Right gs1 -> addGoals gs1
|
||||
@ -97,15 +97,15 @@ simplifyAllConstraints =
|
||||
proveImplication :: Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
|
||||
proveImplication lnam as ps gs =
|
||||
do evars <- varsWithAsmps
|
||||
cfg <- getSolverConfig
|
||||
(mbErr,su) <- io (proveImplicationIO cfg lnam evars as ps gs)
|
||||
solver <- getSolver
|
||||
(mbErr,su) <- io (proveImplicationIO solver lnam evars as ps gs)
|
||||
case mbErr of
|
||||
Right ws -> mapM_ recordWarning ws
|
||||
Left err -> recordError err
|
||||
return su
|
||||
|
||||
|
||||
proveImplicationIO :: SolverConfig
|
||||
proveImplicationIO :: Num.Solver
|
||||
-> Name -- ^ Checking this function
|
||||
-> Set TVar -- ^ These appear in the env., and we should
|
||||
-- not try to default the
|
||||
@ -114,8 +114,7 @@ proveImplicationIO :: SolverConfig
|
||||
-> [Goal] -- ^ Collected constraints
|
||||
-> IO (Either Error [Warning], Subst)
|
||||
proveImplicationIO _ _ _ _ [] [] = return (Right [], emptySubst)
|
||||
proveImplicationIO cfg lname varsInEnv as ps gs =
|
||||
Num.withSolver cfg $ \s ->
|
||||
proveImplicationIO s lname varsInEnv as ps gs =
|
||||
debugBlock s "proveImplicationIO" $
|
||||
|
||||
do debugBlock s "assumes" (debugLog s ps)
|
||||
@ -419,18 +418,6 @@ importSideConds = go [] []
|
||||
3. a substitution which indicates what got defaulted.
|
||||
-}
|
||||
|
||||
improveByDefaulting ::
|
||||
SolverConfig ->
|
||||
[TVar] -> -- candidates for defaulting
|
||||
[Goal] -> -- constraints
|
||||
IO ( [TVar] -- non-defaulted
|
||||
, [Goal] -- new constraints
|
||||
, Subst -- improvements from defaulting
|
||||
, [Warning] -- warnings about defaulting
|
||||
)
|
||||
improveByDefaulting cfg xs gs =
|
||||
Num.withSolver cfg $ \s -> improveByDefaultingWith s xs gs
|
||||
|
||||
improveByDefaultingWith ::
|
||||
Num.Solver ->
|
||||
[TVar] -> -- candidates for defaulting
|
||||
@ -543,16 +530,15 @@ improveByDefaultingWith s as ps =
|
||||
-- | Try to pick a reasonable instantiation for an expression, with
|
||||
-- the given type. This is useful when we do evaluation at the REPL.
|
||||
-- The resulting types should satisfy the constraints of the schema.
|
||||
defaultReplExpr :: SolverConfig -> Expr -> Schema
|
||||
defaultReplExpr :: Num.Solver -> Expr -> Schema
|
||||
-> IO (Maybe ([(TParam,Type)], Expr))
|
||||
defaultReplExpr cfg e s =
|
||||
defaultReplExpr so e s =
|
||||
if all (\v -> kindOf v == KNum) (sVars s)
|
||||
then do let params = map tpVar (sVars s)
|
||||
mbSubst <- tryGetModel cfg params (sProps s)
|
||||
mbSubst <- tryGetModel so params (sProps s)
|
||||
case mbSubst of
|
||||
Just su ->
|
||||
do (res,su1) <- Num.withSolver cfg $ \so ->
|
||||
simpGoals' so (map (makeGoal su) (sProps s))
|
||||
do (res,su1) <- simpGoals' so (map (makeGoal su) (sProps s))
|
||||
return $
|
||||
case res of
|
||||
Right [] | isEmptySubst su1 ->
|
||||
@ -581,14 +567,13 @@ defaultReplExpr cfg e s =
|
||||
-- | Attempt to default the given constraints by asserting them in the SMT
|
||||
-- solver, and asking it for a model.
|
||||
tryGetModel ::
|
||||
SolverConfig ->
|
||||
Num.Solver ->
|
||||
[TVar] -> -- variables to try defaulting
|
||||
[Prop] -> -- constraints
|
||||
IO (Maybe Subst)
|
||||
tryGetModel cfg xs ps =
|
||||
Num.withSolver cfg $ \ s ->
|
||||
-- We are only interested in finite instantiations
|
||||
Num.getModel s (map (pFin . TVar) xs ++ ps)
|
||||
tryGetModel s xs ps =
|
||||
-- We are only interested in finite instantiations
|
||||
Num.getModel s (map (pFin . TVar) xs ++ ps)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user