mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-10-05 18:08:04 +03:00
Try to fix benchmarks
This commit is contained in:
Bretton
parent
d04aa87e72
commit
40d60e4049
109
bench/Main.hs
109
bench/Main.hs
@ -11,13 +11,19 @@
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
module Main where
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Concurrent.MVar
|
||||
import Control.DeepSeq ( force )
|
||||
import Control.Monad.IO.Class( liftIO )
|
||||
import qualified Data.ByteString as BS
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.Text.IO as T
|
||||
import System.FilePath ((</>))
|
||||
import qualified System.Directory as Dir
|
||||
|
||||
import Cryptol.Backend.SBV (SBV (..))
|
||||
|
||||
import qualified Cryptol.Eval as E
|
||||
import qualified Cryptol.Eval.Value as E
|
||||
import qualified Cryptol.Eval.Concrete as C
|
||||
@ -25,22 +31,28 @@ import qualified Cryptol.Eval.Concrete as C
|
||||
import qualified Cryptol.ModuleSystem.Base as M
|
||||
import qualified Cryptol.ModuleSystem.Env as M
|
||||
import qualified Cryptol.ModuleSystem.Monad as M
|
||||
import qualified Cryptol.ModuleSystem.Name as M
|
||||
import qualified Cryptol.ModuleSystem.NamingEnv as M
|
||||
import Cryptol.ModuleSystem.Interface (noIfaceParams)
|
||||
import qualified Cryptol.ModuleSystem.Interface as M
|
||||
import qualified Cryptol.ModuleSystem.Renamer as R
|
||||
|
||||
import qualified Cryptol.Parser as P
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import qualified Cryptol.Parser.NoInclude as P
|
||||
|
||||
import qualified Cryptol.Eval.SBV as S
|
||||
import qualified Cryptol.Symbolic.SBV as S
|
||||
|
||||
import qualified Cryptol.TypeCheck as T
|
||||
import qualified Cryptol.TypeCheck.AST as T
|
||||
import qualified Cryptol.TypeCheck as T
|
||||
import qualified Cryptol.TypeCheck.AST as T
|
||||
import Cryptol.TypeCheck.Interface (genIface)
|
||||
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
|
||||
|
||||
import qualified Cryptol.Utils.Ident as I
|
||||
import Cryptol.Utils.Logger(quietLogger)
|
||||
|
||||
import qualified Data.SBV.Dynamic as SBV
|
||||
import qualified Data.SBV as SBV
|
||||
import qualified Data.SBV.Dynamic as SBV (svTrue)
|
||||
|
||||
import Criterion.Main
|
||||
|
||||
@ -107,48 +119,68 @@ tc cd name path =
|
||||
}
|
||||
Right pm = P.parseModule cfg bytes
|
||||
menv <- M.initialModuleEnv
|
||||
(eres, _) <- M.runModuleM (evOpts,menv) $ withLib $ do
|
||||
solver <- SMT.startSolver (pure ()) $
|
||||
T.defaultSolverConfig $ M.meSearchPath menv
|
||||
let minp = M.ModuleInput
|
||||
{ M.minpCallStacks = True
|
||||
, M.minpEvalOpts = pure evOpts
|
||||
, M.minpByteReader = BS.readFile
|
||||
, M.minpModuleEnv = menv
|
||||
, M.minpTCSolver = solver
|
||||
}
|
||||
(eres, _) <- M.runModuleM minp $ withLib $ do
|
||||
-- code from `loadModule` and `checkModule` in
|
||||
-- `Cryptol.ModuleSystem.Base`
|
||||
let pm' = M.addPrelude pm
|
||||
M.loadDeps pm'
|
||||
enim <- M.io (P.removeIncludesModule path pm')
|
||||
enim <- M.io (P.removeIncludesModule BS.readFile path pm')
|
||||
nim <- either (error "Failed to remove includes") return enim
|
||||
npm <- M.noPat nim
|
||||
(tcEnv,declsEnv,scm) <- M.renameModule npm
|
||||
rm <- M.renameModule npm
|
||||
prims <- if P.thing (P.mName pm) == I.preludeName
|
||||
then return (M.toPrimMap declsEnv)
|
||||
then return (M.toPrimMap $ R.rmDefines rm)
|
||||
else M.getPrimMap
|
||||
return (prims, scm, tcEnv)
|
||||
return (prims, R.rmModule rm, R.rmImported rm)
|
||||
case eres of
|
||||
Right ((prims, scm, tcEnv), menv') ->
|
||||
return (prims, scm, tcEnv, menv')
|
||||
return (prims, scm, tcEnv, minp, menv')
|
||||
Left _ -> error $ "Failed to load " ++ name
|
||||
in env setup $ \ ~(prims, scm, tcEnv, menv) ->
|
||||
bench name $ whnfIO $ M.runModuleM (evOpts,menv) $ withLib $ do
|
||||
in env setup $ \ ~(prims, scm, tcEnv, minp, menv) ->
|
||||
bench name $ whnfIO $ M.runModuleM minp $ withLib $ do
|
||||
let act = M.TCAction { M.tcAction = T.tcModule
|
||||
, M.tcLinter = M.moduleLinter (P.thing (P.mName scm))
|
||||
, M.tcPrims = prims
|
||||
}
|
||||
M.typecheck act scm noIfaceParams tcEnv
|
||||
M.typecheck act scm M.noIfaceParams tcEnv
|
||||
|
||||
ceval :: String -> String -> FilePath -> T.Text -> Benchmark
|
||||
ceval cd name path expr =
|
||||
let withLib = M.withPrependedSearchPath [cd </> "lib"] in
|
||||
let setup = do
|
||||
menv <- M.initialModuleEnv
|
||||
(eres, _) <- M.runModuleM (evOpts,menv) $ withLib $ do
|
||||
solver <- SMT.startSolver (pure ()) $
|
||||
T.defaultSolverConfig $ M.meSearchPath menv
|
||||
let minp = M.ModuleInput
|
||||
{ M.minpCallStacks = True
|
||||
, M.minpEvalOpts = pure evOpts
|
||||
, M.minpByteReader = BS.readFile
|
||||
, M.minpModuleEnv = menv
|
||||
, M.minpTCSolver = solver
|
||||
}
|
||||
(eres, _) <- M.runModuleM minp $ withLib $ do
|
||||
m <- M.loadModuleByPath path
|
||||
M.setFocusedModule (T.mName m)
|
||||
let Right pexpr = P.parseExpr expr
|
||||
(_, texpr, _) <- M.checkExpr pexpr
|
||||
return texpr
|
||||
case eres of
|
||||
Right (texpr, menv') -> return (texpr, menv')
|
||||
Right (texpr, menv') -> do
|
||||
let tbl = C.primTable (pure evOpts)
|
||||
return (texpr, \i -> Right <$> Map.lookup i tbl, menv')
|
||||
Left _ -> error $ "Failed to load " ++ name
|
||||
in env setup $ \ ~(texpr, menv) ->
|
||||
bench name $ nfIO $ E.runEval evOpts $ do
|
||||
let ?evalPrim = C.evalPrim
|
||||
in env setup $ \ ~(texpr, evalPrim, menv) ->
|
||||
bench name $ nfIO $ E.runEval mempty $ do
|
||||
let ?evalPrim = evalPrim
|
||||
env' <- E.evalDecls C.Concrete (M.allDeclGroups menv) mempty
|
||||
(e :: C.Value) <- E.evalExpr C.Concrete env' texpr
|
||||
E.forceValue e
|
||||
@ -159,19 +191,44 @@ seval cd name path expr =
|
||||
let withLib = M.withPrependedSearchPath [cd </> "lib"] in
|
||||
let setup = do
|
||||
menv <- M.initialModuleEnv
|
||||
(eres, _) <- M.runModuleM (evOpts,menv) $ withLib $ do
|
||||
solver <- SMT.startSolver (pure ()) $
|
||||
T.defaultSolverConfig $ M.meSearchPath menv
|
||||
let minp = M.ModuleInput
|
||||
{ M.minpCallStacks = True
|
||||
, M.minpEvalOpts = pure evOpts
|
||||
, M.minpByteReader = BS.readFile
|
||||
, M.minpModuleEnv = menv
|
||||
, M.minpTCSolver = solver
|
||||
}
|
||||
(eres, _) <- M.runModuleM minp $ withLib $ do
|
||||
m <- M.loadModuleByPath path
|
||||
M.setFocusedModule (T.mName m)
|
||||
let Right pexpr = P.parseExpr expr
|
||||
(_, texpr, _) <- M.checkExpr pexpr
|
||||
return texpr
|
||||
ds <- do
|
||||
(_mp, mo) <-
|
||||
M.loadModuleFrom True (M.FromModule I.preludeReferenceName)
|
||||
let decls = T.mDecls mo
|
||||
let nms = fst <$> Map.toList (M.ifDecls (M.ifPublic (genIface m)))
|
||||
let ds = Map.fromList
|
||||
[ (I.prelPrim (I.identText (M.nameIdent nm))
|
||||
, T.EWhere (T.EVar nm) decls)
|
||||
| nm <- nms ]
|
||||
pure ds
|
||||
return (texpr, ds)
|
||||
case eres of
|
||||
Right (texpr, menv') -> return (texpr, menv')
|
||||
Right ((texpr, ds), menv') -> return (texpr, menv', ds)
|
||||
Left _ -> error $ "Failed to load " ++ name
|
||||
in env setup $ \ ~(texpr, menv) ->
|
||||
bench name $ whnfIO $ fmap force E.runEval evOpts $ S.sbvEval $ do
|
||||
let ?evalPrim = S.evalPrim
|
||||
env' <- E.evalDecls S.SBV (M.allDeclGroups menv) mempty
|
||||
(e :: S.Value) <- E.evalExpr S.SBV env' texpr
|
||||
in env setup $ \ ~(texpr, menv, ds) ->
|
||||
bench name $ whnfIO $ fmap force $ S.runProver (Left S.defaultProver) S.doSBVEval $ do
|
||||
sbvState <- SBV.symbolicEnv
|
||||
stateMVar <- liftIO (newMVar sbvState)
|
||||
defRelsVar <- liftIO (newMVar SBV.svTrue)
|
||||
let sym = SBV stateMVar defRelsVar
|
||||
let tbl = S.primTable sym (pure evOpts)
|
||||
let ?evalPrim = \i -> (Right <$> Map.lookup i tbl) <|>
|
||||
(Left <$> Map.lookup i ds)
|
||||
env' <- E.evalDecls sym (M.allDeclGroups menv) mempty
|
||||
(e :: S.Value) <- E.evalExpr sym env' texpr
|
||||
liftIO $ SBV.generateSMTBenchmark False $
|
||||
return (E.fromVBit e)
|
||||
|
||||
@ -305,6 +305,8 @@ benchmark cryptol-bench
|
||||
ld-options: -static -pthread
|
||||
ghc-options: -optl-fuse-ld=bfd
|
||||
build-depends: base
|
||||
, bytestring
|
||||
, containers
|
||||
, criterion
|
||||
, cryptol
|
||||
, deepseq
|
||||
|
||||
@ -18,7 +18,8 @@
|
||||
{-# LANGUAGE TypeSynonymInstances #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
module Cryptol.Eval.SBV
|
||||
( primTable
|
||||
( Value
|
||||
, primTable
|
||||
) where
|
||||
|
||||
import qualified Control.Exception as X
|
||||
|
||||
@ -20,7 +20,9 @@
|
||||
module Cryptol.Symbolic.SBV
|
||||
( SBVProverConfig
|
||||
, defaultProver
|
||||
, doSBVEval
|
||||
, proverNames
|
||||
, runProver
|
||||
, setupProver
|
||||
, satProve
|
||||
, satProveOffline
|
||||
|
||||
Loading…
Reference in New Issue
Block a user