Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update to master #1424

Merged
merged 20 commits into from
Aug 31, 2022
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Add :time command
qsctr committed Aug 29, 2022
commit 8dafb86dc6d63b4b5d55ae047a5ac0d2b450d293
6 changes: 5 additions & 1 deletion cryptol.cabal
Original file line number Diff line number Diff line change
@@ -52,6 +52,7 @@ library
bytestring >= 0.10,
array >= 0.4,
containers >= 0.5,
criterion-measurement,
cryptohash-sha1 >= 0.11 && < 0.12,
deepseq >= 1.3,
directory >= 1.2.2.0,
@@ -75,6 +76,7 @@ library
text >= 1.1,
tf-random >= 0.5,
transformers-base >= 0.4,
vector,
mtl >= 2.2.1,
time >= 1.6.0.1,
panic >= 0.3,
@@ -216,7 +218,9 @@ library
Cryptol.REPL.Command,
Cryptol.REPL.Browse,
Cryptol.REPL.Monad,
Cryptol.REPL.Trie
Cryptol.REPL.Trie,

Cryptol.Benchmark

Other-modules: Cryptol.Parser.LexerUtils,
Cryptol.Parser.ParserUtils,
28 changes: 28 additions & 0 deletions src/Cryptol/Benchmark.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
module Cryptol.Benchmark
( BenchmarkStats (..)
, benchmark
, secs
) where

import Criterion.Measurement (runBenchmark, secs, threshold)
import Criterion.Measurement.Types
import Data.Int
import qualified Data.Vector as V
import qualified Data.Vector.Unboxed as U

data BenchmarkStats = BenchmarkStats
{ benchAvgTime :: !Double
, benchAvgCpuTime :: !Double
, benchAvgCycles :: !Int64
}

benchmark :: (a -> IO b) -> a -> IO BenchmarkStats
benchmark f x = do
(meas, _) <- runBenchmark (whnfAppIO f x) 10
let len = length meas
meas' = rescale <$> V.filter ((>= threshold) . measTime) meas
sumMeasure sel = U.sum $ measure sel meas'
pure BenchmarkStats
{ benchAvgTime = sumMeasure measTime / fromIntegral len
, benchAvgCpuTime = sumMeasure measCpuTime / fromIntegral len
, benchAvgCycles = sumMeasure measCycles `div` fromIntegral len }
5 changes: 5 additions & 0 deletions src/Cryptol/ModuleSystem.hs
Original file line number Diff line number Diff line change
@@ -20,6 +20,7 @@ module Cryptol.ModuleSystem (
, loadModuleByName
, checkExpr
, evalExpr
, benchmarkExpr
, checkDecls
, evalDecls
, noPat
@@ -35,6 +36,7 @@ module Cryptol.ModuleSystem (

import Data.Map (Map)

import Cryptol.Benchmark (BenchmarkStats)
import qualified Cryptol.Eval.Concrete as Concrete
import Cryptol.ModuleSystem.Env
import Cryptol.ModuleSystem.Interface
@@ -97,6 +99,9 @@ checkExpr e env = runModuleM env (interactive (Base.checkExpr e))
evalExpr :: T.Expr -> ModuleCmd Concrete.Value
evalExpr e env = runModuleM env (interactive (Base.evalExpr e))

benchmarkExpr :: T.Expr -> ModuleCmd BenchmarkStats
benchmarkExpr e env = runModuleM env (interactive (Base.benchmarkExpr e))

-- | Typecheck top-level declarations.
checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup], Map Name T.TySyn)
checkDecls ds env = runModuleM env
17 changes: 17 additions & 0 deletions src/Cryptol/ModuleSystem/Base.hs
Original file line number Diff line number Diff line change
@@ -51,6 +51,7 @@ import Cryptol.ModuleSystem.Env (lookupModule
, ModContext(..)
, ModulePath(..), modulePathLabel)
import Cryptol.Backend.FFI
import Cryptol.Benchmark
import qualified Cryptol.Eval as E
import qualified Cryptol.Eval.Concrete as Concrete
import Cryptol.Eval.Concrete (Concrete(..))
@@ -611,6 +612,22 @@ evalExpr e = do

io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e)

benchmarkExpr :: T.Expr -> ModuleM BenchmarkStats
benchmarkExpr e = do
env <- getEvalEnv
denv <- getDynEnv
evopts <- getEvalOptsAction
let env' = env <> deEnv denv
let tbl = Concrete.primTable evopts
let ?evalPrim = \i -> Right <$> Map.lookup i tbl
let ?range = emptyRange
callStacks <- getCallStacks
let ?callStacks = callStacks

let eval expr = E.runEval mempty $
E.evalExpr Concrete env' expr >>= E.forceValue
io $ benchmark eval e

evalDecls :: [T.DeclGroup] -> ModuleM ()
evalDecls dgs = do
env <- getEvalEnv
81 changes: 53 additions & 28 deletions src/Cryptol/REPL/Command.hs
Original file line number Diff line number Diff line change
@@ -70,6 +70,7 @@ import qualified Cryptol.ModuleSystem.Env as M

import qualified Cryptol.Backend.Monad as E
import qualified Cryptol.Backend.SeqMap as E
import qualified Cryptol.Benchmark as Bench
import Cryptol.Eval.Concrete( Concrete(..) )
import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Env as E
@@ -252,6 +253,9 @@ nbCommandList =
, CommandDescr [ ":extract-coq" ] [] (NoArg allTerms)
"Print out the post-typechecked AST of all currently defined terms,\nin a Coq-parseable format."
""
, CommandDescr [ ":time" ] ["EXPR"] (ExprArg timeCmd)
"Measure the time it takes to evaluate the given expression."
""
]

commandList :: [CommandDescr]
@@ -999,6 +1003,19 @@ typeOfCmd str pos fnm = do
rPrint $ runDoc fDisp $ group $ hang
(ppPrec 2 expr <+> text ":") 2 (pp sig)

timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL ()
timeCmd str pos fnm = do
pExpr <- replParseExpr str pos fnm
(_, def, sig) <- replCheckExpr pExpr
replPrepareCheckedExpr def sig >>= \case
Nothing -> raise (EvalPolyError sig)
Just (_, expr) -> do
Bench.BenchmarkStats {..} <-
liftModuleCmd (rethrowEvalError . M.benchmarkExpr expr)
rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime
++ "\tAvg CPU time: " ++ Bench.secs benchAvgCpuTime
++ "\tAvg cycles: " ++ show benchAvgCycles

readFileCmd :: FilePath -> REPL ()
readFileCmd fp = do
bytes <- replReadFile fp (\err -> rPutStrLn (show err) >> return Nothing)
@@ -1569,39 +1586,47 @@ replSpecExpr e = liftModuleCmd $ S.specialize e
replEvalExpr :: P.Expr P.PName -> REPL (Concrete.Value, T.Type)
replEvalExpr expr =
do (_,def,sig) <- replCheckExpr expr
replEvalCheckedExpr def sig >>= \mb_res -> case mb_res of
replEvalCheckedExpr def sig >>= \case
Just res -> pure res
Nothing -> raise (EvalPolyError sig)

replEvalCheckedExpr :: T.Expr -> T.Schema -> REPL (Maybe (Concrete.Value, T.Type))
replEvalCheckedExpr def sig =
do validEvalContext def
validEvalContext sig

s <- getTCSolver
mbDef <- io (defaultReplExpr s def sig)

case mbDef of
Nothing -> pure Nothing
Just (tys, def1) ->
do warnDefaults tys
let su = T.listParamSubst tys
let ty = T.apSubst su (T.sType sig)
whenDebug (rPutStrLn (dump def1))

tenv <- E.envTypes . M.deEnv <$> getDynEnv
let tyv = E.evalValType tenv ty

-- add "it" to the namespace via a new declaration
itVar <- bindItVariable tyv def1

let itExpr = case getLoc def of
Nothing -> T.EVar itVar
Just rng -> T.ELocated rng (T.EVar itVar)

-- evaluate the it variable
val <- liftModuleCmd (rethrowEvalError . M.evalExpr itExpr)
return $ Just (val,ty)
replPrepareCheckedExpr def sig >>=
traverse \(tys, def1) -> do
let su = T.listParamSubst tys
let ty = T.apSubst su (T.sType sig)
whenDebug (rPutStrLn (dump def1))

tenv <- E.envTypes . M.deEnv <$> getDynEnv
let tyv = E.evalValType tenv ty

-- add "it" to the namespace via a new declaration
itVar <- bindItVariable tyv def1

let itExpr = case getLoc def of
Nothing -> T.EVar itVar
Just rng -> T.ELocated rng (T.EVar itVar)

-- evaluate the it variable
val <- liftModuleCmd (rethrowEvalError . M.evalExpr itExpr)
return (val,ty)

-- | Check that we are in a valid evaluation context and apply defaulting.
replPrepareCheckedExpr :: T.Expr -> T.Schema ->
REPL (Maybe ([(T.TParam, T.Type)], T.Expr))
replPrepareCheckedExpr def sig = do
validEvalContext def
validEvalContext sig

s <- getTCSolver
mbDef <- io (defaultReplExpr s def sig)

case mbDef of
Nothing -> pure Nothing
Just (tys, def1) -> do
warnDefaults tys
pure $ Just (tys, def1)
where
warnDefaults ts =
case ts of