From 2d9da2d55bd525e4f275e4b1e774d256f0f6fe64 Mon Sep 17 00:00:00 2001 From: Taimoor Zaeem Date: Sun, 28 Aug 2022 17:13:35 +0500 Subject: [PATCH 01/18] Improve error message for ModuleNameMismatch error. --- src/Cryptol/ModuleSystem/Monad.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index a282a94de..1707c738e 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -192,7 +192,7 @@ instance PP ModuleError where ModuleNameMismatch expected found -> hang (text "[error]" <+> pp (P.srcRange found) <.> char ':') 4 (vcat [ text "File name does not match module name:" - , text "Saw:" <+> pp (P.thing found) + , text " Actual:" <+> pp (P.thing found) , text "Expected:" <+> pp expected ]) From c003895a2b11861b06c6033478293e66f130aa6a Mon Sep 17 00:00:00 2001 From: Taimoor Zaeem Date: Sun, 28 Aug 2022 17:38:41 +0500 Subject: [PATCH 02/18] Add regression test for issue #1253. --- tests/issues/issue1253.icry | 1 + tests/issues/issue1253.icry.stdout | 8 ++++++++ tests/issues/issue1253.icry.stdout.mingw32 | 8 ++++++++ tests/issues/issue1253a.cry | 4 ++++ tests/issues/issue1253b.cry | 2 ++ 5 files changed, 23 insertions(+) create mode 100644 tests/issues/issue1253.icry create mode 100644 tests/issues/issue1253.icry.stdout create mode 100644 tests/issues/issue1253.icry.stdout.mingw32 create mode 100644 tests/issues/issue1253a.cry create mode 100644 tests/issues/issue1253b.cry diff --git a/tests/issues/issue1253.icry b/tests/issues/issue1253.icry new file mode 100644 index 000000000..8a069295d --- /dev/null +++ b/tests/issues/issue1253.icry @@ -0,0 +1 @@ +:l issue1253a.cry diff --git a/tests/issues/issue1253.icry.stdout b/tests/issues/issue1253.icry.stdout new file mode 100644 index 000000000..d7634c35d --- /dev/null +++ b/tests/issues/issue1253.icry.stdout @@ -0,0 +1,8 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Foo + +[error] ./issue1253b.cry:1:8--1:11: + File name does not match module name: + Actual: Foo + Expected: issue1253b diff --git a/tests/issues/issue1253.icry.stdout.mingw32 b/tests/issues/issue1253.icry.stdout.mingw32 new file mode 100644 index 000000000..afe2eabeb --- /dev/null +++ b/tests/issues/issue1253.icry.stdout.mingw32 @@ -0,0 +1,8 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Foo + +[error] .\issue1253b.cry:1:8--1:11: + File name does not match module name: + Actual: Foo + Expected: issue1253b diff --git a/tests/issues/issue1253a.cry b/tests/issues/issue1253a.cry new file mode 100644 index 000000000..bbfa9f016 --- /dev/null +++ b/tests/issues/issue1253a.cry @@ -0,0 +1,4 @@ +module issue1253a where + +import issue1253b + diff --git a/tests/issues/issue1253b.cry b/tests/issues/issue1253b.cry new file mode 100644 index 000000000..05344ea0d --- /dev/null +++ b/tests/issues/issue1253b.cry @@ -0,0 +1,2 @@ +module Foo where + From 8dafb86dc6d63b4b5d55ae047a5ac0d2b450d293 Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 10:44:59 -0700 Subject: [PATCH 03/18] Add :time command --- cryptol.cabal | 6 ++- src/Cryptol/Benchmark.hs | 28 +++++++++++ src/Cryptol/ModuleSystem.hs | 5 ++ src/Cryptol/ModuleSystem/Base.hs | 17 +++++++ src/Cryptol/REPL/Command.hs | 81 +++++++++++++++++++++----------- 5 files changed, 108 insertions(+), 29 deletions(-) create mode 100644 src/Cryptol/Benchmark.hs diff --git a/cryptol.cabal b/cryptol.cabal index c191941ff..fa2a4e040 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -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, diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Benchmark.hs new file mode 100644 index 000000000..b24f7170a --- /dev/null +++ b/src/Cryptol/Benchmark.hs @@ -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 } diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index 10f9062cb..a7450ee8f 100644 --- a/src/Cryptol/ModuleSystem.hs +++ b/src/Cryptol/ModuleSystem.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 7113a488c..83a48d08a 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -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 diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 0f5404faa..e522ba68b 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -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 From c1ede357cb0eadaaec280172972b2f97d9b376ad Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 11:43:21 -0700 Subject: [PATCH 04/18] benchmark: BenchmarkStats deriving Show --- src/Cryptol/Benchmark.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Benchmark.hs index b24f7170a..51988dbce 100644 --- a/src/Cryptol/Benchmark.hs +++ b/src/Cryptol/Benchmark.hs @@ -14,7 +14,7 @@ data BenchmarkStats = BenchmarkStats { benchAvgTime :: !Double , benchAvgCpuTime :: !Double , benchAvgCycles :: !Int64 - } + } deriving Show benchmark :: (a -> IO b) -> a -> IO BenchmarkStats benchmark f x = do From c98882969389255ad809aed172b151ef4cbef583 Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 11:47:04 -0700 Subject: [PATCH 05/18] time command: Improve output formatting --- src/Cryptol/REPL/Command.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index e522ba68b..45879d990 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -1013,8 +1013,8 @@ timeCmd str pos fnm = do Bench.BenchmarkStats {..} <- liftModuleCmd (rethrowEvalError . M.benchmarkExpr expr) rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime - ++ "\tAvg CPU time: " ++ Bench.secs benchAvgCpuTime - ++ "\tAvg cycles: " ++ show benchAvgCycles + ++ " Avg CPU time: " ++ Bench.secs benchAvgCpuTime + ++ " Avg cycles: " ++ show benchAvgCycles readFileCmd :: FilePath -> REPL () readFileCmd fp = do From 7ee80344c3fdc248dc857725b58e354561844dbe Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 15:15:12 -0700 Subject: [PATCH 06/18] time command: Make measurement period configurable --- src/Cryptol/Benchmark.hs | 6 +++--- src/Cryptol/ModuleSystem.hs | 5 +++-- src/Cryptol/ModuleSystem/Base.hs | 6 +++--- src/Cryptol/REPL/Command.hs | 5 +++-- src/Cryptol/REPL/Monad.hs | 17 +++++++++++++++++ 5 files changed, 29 insertions(+), 10 deletions(-) diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Benchmark.hs index 51988dbce..a3a51964f 100644 --- a/src/Cryptol/Benchmark.hs +++ b/src/Cryptol/Benchmark.hs @@ -16,9 +16,9 @@ data BenchmarkStats = BenchmarkStats , benchAvgCycles :: !Int64 } deriving Show -benchmark :: (a -> IO b) -> a -> IO BenchmarkStats -benchmark f x = do - (meas, _) <- runBenchmark (whnfAppIO f x) 10 +benchmark :: Double -> (a -> IO b) -> a -> IO BenchmarkStats +benchmark period f x = do + (meas, _) <- runBenchmark (whnfAppIO f x) period let len = length meas meas' = rescale <$> V.filter ((>= threshold) . measTime) meas sumMeasure sel = U.sum $ measure sel meas' diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index a7450ee8f..17c19576d 100644 --- a/src/Cryptol/ModuleSystem.hs +++ b/src/Cryptol/ModuleSystem.hs @@ -99,8 +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)) +benchmarkExpr :: Double -> T.Expr -> ModuleCmd BenchmarkStats +benchmarkExpr period e env = + runModuleM env (interactive (Base.benchmarkExpr period e)) -- | Typecheck top-level declarations. checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup], Map Name T.TySyn) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 83a48d08a..570361db1 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -612,8 +612,8 @@ evalExpr e = do io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e) -benchmarkExpr :: T.Expr -> ModuleM BenchmarkStats -benchmarkExpr e = do +benchmarkExpr :: Double -> T.Expr -> ModuleM BenchmarkStats +benchmarkExpr period e = do env <- getEvalEnv denv <- getDynEnv evopts <- getEvalOptsAction @@ -626,7 +626,7 @@ benchmarkExpr e = do let eval expr = E.runEval mempty $ E.evalExpr Concrete env' expr >>= E.forceValue - io $ benchmark eval e + io $ benchmark period eval e evalDecls :: [T.DeclGroup] -> ModuleM () evalDecls dgs = do diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 45879d990..b9ecf49b1 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -1005,13 +1005,14 @@ typeOfCmd str pos fnm = do timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL () timeCmd str pos fnm = do + period <- getKnownUser "timeMeasurementPeriod" :: REPL Int 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) + Bench.BenchmarkStats {..} <- liftModuleCmd + (rethrowEvalError . M.benchmarkExpr (fromIntegral period) expr) rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime ++ " Avg CPU time: " ++ Bench.secs benchAvgCpuTime ++ " Avg cycles: " ++ show benchAvgCycles diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index f77cc6d70..062693d1f 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -983,6 +983,15 @@ userOptions = mkOptionMap , " * display try to match the order they were written in the source code" , " * canonical use a predictable, canonical order" ] + + , simpleOpt "timeMeasurementPeriod" ["time-measurement-period"] (EnvNum 10) + checkTimeMeasurementPeriod + $ unlines + [ "The period of time in seconds to spend collecting measurements when" + , " running :time." + , "This is a lower bound and the actual time taken might be higher if the" + , " evaluation takes a long time." + ] ] @@ -1078,6 +1087,14 @@ getUserSatNum = do _ -> panic "REPL.Monad.getUserSatNum" [ "invalid satNum option" ] +checkTimeMeasurementPeriod :: Checker +checkTimeMeasurementPeriod (EnvNum n) + | n >= 1 = noWarns Nothing + | otherwise = noWarns $ + Just "timeMeasurementPeriod must be a positive integer" +checkTimeMeasurementPeriod _ = noWarns $ + Just "unable to parse value for timeMeasurementPeriod" + -- Environment Utilities ------------------------------------------------------- whenDebug :: REPL () -> REPL () From 1c8ff60dc9a209111d4adf5428166c1d929900f5 Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 15:22:57 -0700 Subject: [PATCH 07/18] time command: Fix average calculation --- src/Cryptol/Benchmark.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Benchmark.hs index a3a51964f..ef2b8efcd 100644 --- a/src/Cryptol/Benchmark.hs +++ b/src/Cryptol/Benchmark.hs @@ -19,8 +19,8 @@ data BenchmarkStats = BenchmarkStats benchmark :: Double -> (a -> IO b) -> a -> IO BenchmarkStats benchmark period f x = do (meas, _) <- runBenchmark (whnfAppIO f x) period - let len = length meas - meas' = rescale <$> V.filter ((>= threshold) . measTime) meas + let meas' = rescale <$> V.filter ((>= threshold) . measTime) meas + len = length meas' sumMeasure sel = U.sum $ measure sel meas' pure BenchmarkStats { benchAvgTime = sumMeasure measTime / fromIntegral len From 0d53c059ec177f78b36debafa8ec8c8e9ade31c2 Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 22:04:14 -0700 Subject: [PATCH 08/18] time command: Improve command description --- src/Cryptol/REPL/Command.hs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index b9ecf49b1..72cc463bf 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -255,7 +255,10 @@ nbCommandList = "" , CommandDescr [ ":time" ] ["EXPR"] (ExprArg timeCmd) "Measure the time it takes to evaluate the given expression." - "" + (unlines + [ "The expression will be evaluated many times to get accurate results." + , "The amount of time to spend collecting measurements can be changed" + , " with the timeMeasurementPeriod option." ]) ] commandList :: [CommandDescr] From 25d34678901a37b050aafb1a1ff0687dd46a5ed4 Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 22:07:46 -0700 Subject: [PATCH 09/18] time command: Print measurement period --- src/Cryptol/REPL/Command.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 72cc463bf..1e4497c1e 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -1009,6 +1009,7 @@ typeOfCmd str pos fnm = do timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL () timeCmd str pos fnm = do period <- getKnownUser "timeMeasurementPeriod" :: REPL Int + rPutStrLn $ "Measuring for " ++ show period ++ " seconds" pExpr <- replParseExpr str pos fnm (_, def, sig) <- replCheckExpr pExpr replPrepareCheckedExpr def sig >>= \case From 4af4f6d7bb599b58cc6bb3e9de0b90da7ba73d13 Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 22:39:42 -0700 Subject: [PATCH 10/18] time command: Document command output --- src/Cryptol/REPL/Command.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 1e4497c1e..b75d0f639 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -258,7 +258,9 @@ nbCommandList = (unlines [ "The expression will be evaluated many times to get accurate results." , "The amount of time to spend collecting measurements can be changed" - , " with the timeMeasurementPeriod option." ]) + , " with the timeMeasurementPeriod option." + , "Reports the average wall clock time, CPU time, and cycles." + , "(Cycles are in unspecified units that may be CPU cycles.)"]) ] commandList :: [CommandDescr] From cde5f18dafabfa88405e6c4760fa9d4086f0a37c Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 22:49:52 -0700 Subject: [PATCH 11/18] time command: Add comments --- src/Cryptol/Benchmark.hs | 8 ++++++++ src/Cryptol/ModuleSystem.hs | 1 + 2 files changed, 9 insertions(+) diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Benchmark.hs index ef2b8efcd..c4ef18b4b 100644 --- a/src/Cryptol/Benchmark.hs +++ b/src/Cryptol/Benchmark.hs @@ -1,3 +1,4 @@ +-- | Simple benchmarking of IO functions. module Cryptol.Benchmark ( BenchmarkStats (..) , benchmark @@ -10,12 +11,19 @@ import Data.Int import qualified Data.Vector as V import qualified Data.Vector.Unboxed as U +-- | Statistics returned by 'benchmark'. +-- +-- This is extremely crude compared to the full analysis that criterion can do, +-- but is enough for now. data BenchmarkStats = BenchmarkStats { benchAvgTime :: !Double , benchAvgCpuTime :: !Double , benchAvgCycles :: !Int64 } deriving Show +-- | Benchmark the application of the given function to the given input and the +-- execution of the resulting IO action to WHNF, spending at least the given +-- amount of time in seconds to collect measurements. benchmark :: Double -> (a -> IO b) -> a -> IO BenchmarkStats benchmark period f x = do (meas, _) <- runBenchmark (whnfAppIO f x) period diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index 17c19576d..066319b03 100644 --- a/src/Cryptol/ModuleSystem.hs +++ b/src/Cryptol/ModuleSystem.hs @@ -99,6 +99,7 @@ checkExpr e env = runModuleM env (interactive (Base.checkExpr e)) evalExpr :: T.Expr -> ModuleCmd Concrete.Value evalExpr e env = runModuleM env (interactive (Base.evalExpr e)) +-- | Benchmark an expression. benchmarkExpr :: Double -> T.Expr -> ModuleCmd BenchmarkStats benchmarkExpr period e env = runModuleM env (interactive (Base.benchmarkExpr period e)) From e4b46117112014b65e7ba659b6594fa766577c2f Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 22:56:04 -0700 Subject: [PATCH 12/18] Move Benchmark module to Cryptol.Utils --- cryptol.cabal | 5 ++--- src/Cryptol/ModuleSystem.hs | 2 +- src/Cryptol/ModuleSystem/Base.hs | 2 +- src/Cryptol/REPL/Command.hs | 2 +- src/Cryptol/{ => Utils}/Benchmark.hs | 2 +- 5 files changed, 6 insertions(+), 7 deletions(-) rename src/Cryptol/{ => Utils}/Benchmark.hs (97%) diff --git a/cryptol.cabal b/cryptol.cabal index fa2a4e040..96f2f3c19 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -118,6 +118,7 @@ library Cryptol.Utils.Misc, Cryptol.Utils.Patterns, Cryptol.Utils.Logger, + Cryptol.Utils.Benchmark, Cryptol.Version, Cryptol.ModuleSystem, @@ -218,9 +219,7 @@ library Cryptol.REPL.Command, Cryptol.REPL.Browse, Cryptol.REPL.Monad, - Cryptol.REPL.Trie, - - Cryptol.Benchmark + Cryptol.REPL.Trie Other-modules: Cryptol.Parser.LexerUtils, Cryptol.Parser.ParserUtils, diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index 066319b03..cbb3548ba 100644 --- a/src/Cryptol/ModuleSystem.hs +++ b/src/Cryptol/ModuleSystem.hs @@ -36,7 +36,6 @@ 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 @@ -49,6 +48,7 @@ import Cryptol.Parser.Name (PName) import Cryptol.Parser.NoPat (RemovePatterns) import qualified Cryptol.TypeCheck.AST as T import qualified Cryptol.TypeCheck.Interface as T +import Cryptol.Utils.Benchmark (BenchmarkStats) import qualified Cryptol.Utils.Ident as M -- Public Interface ------------------------------------------------------------ diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 570361db1..d26938131 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -51,7 +51,6 @@ 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(..)) @@ -76,6 +75,7 @@ import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, prim import Cryptol.Utils.PP (pretty) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Logger(logPutStrLn, logPrint) +import Cryptol.Utils.Benchmark import Cryptol.Prelude ( preludeContents, floatContents, arrayContents , suiteBContents, primeECContents, preludeReferenceContents ) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index b75d0f639..ca6a1e070 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -70,7 +70,6 @@ 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 @@ -89,6 +88,7 @@ import qualified Cryptol.TypeCheck.Parseable as T import qualified Cryptol.TypeCheck.Subst as T import Cryptol.TypeCheck.Solve(defaultReplExpr) import Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap) +import qualified Cryptol.Utils.Benchmark as Bench import Cryptol.Utils.PP hiding (()) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.RecordMap diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Utils/Benchmark.hs similarity index 97% rename from src/Cryptol/Benchmark.hs rename to src/Cryptol/Utils/Benchmark.hs index c4ef18b4b..17bc4a31d 100644 --- a/src/Cryptol/Benchmark.hs +++ b/src/Cryptol/Utils/Benchmark.hs @@ -1,5 +1,5 @@ -- | Simple benchmarking of IO functions. -module Cryptol.Benchmark +module Cryptol.Utils.Benchmark ( BenchmarkStats (..) , benchmark , secs From 130ae18573b47f303c1af1ba49623bfec2a31a97 Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 29 Aug 2022 23:05:58 -0700 Subject: [PATCH 13/18] Add :time to CHANGES.md --- CHANGES.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 8207c3258..893da25fb 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -5,6 +5,10 @@ * Fix a bug in the What4 backend that could cause applications of `(@)` with symbolic `Integer` indices to become out of bounds (#1359). +## New features + +* Add a `:time` command to benchmark the evaluation time of expressions. + # 2.13.0 ## Language changes From 09cf06a8e819c2ee49110e18f640203fb9d98a81 Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 30 Aug 2022 14:24:47 -0700 Subject: [PATCH 14/18] time command: bind result to it --- cryptol.cabal | 1 + src/Cryptol/Backend/FloatHelpers.hs | 6 ++++++ src/Cryptol/Eval/Type.hs | 5 +++++ src/Cryptol/REPL/Command.hs | 15 ++++++++++++++- src/Cryptol/TypeCheck/FFI.hs | 5 +++-- 5 files changed, 29 insertions(+), 3 deletions(-) diff --git a/cryptol.cabal b/cryptol.cabal index 96f2f3c19..2ddcdff21 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -119,6 +119,7 @@ library Cryptol.Utils.Patterns, Cryptol.Utils.Logger, Cryptol.Utils.Benchmark, + Cryptol.Utils.Types, Cryptol.Version, Cryptol.ModuleSystem, diff --git a/src/Cryptol/Backend/FloatHelpers.hs b/src/Cryptol/Backend/FloatHelpers.hs index 4aa93d0fd..7c9924cf5 100644 --- a/src/Cryptol/Backend/FloatHelpers.hs +++ b/src/Cryptol/Backend/FloatHelpers.hs @@ -8,6 +8,7 @@ import LibBF import Cryptol.Utils.PP import Cryptol.Utils.Panic(panic) +import Cryptol.Utils.Types import Cryptol.Backend.Monad( EvalError(..) ) @@ -176,3 +177,8 @@ floatFromBits e p bv = BF { bfValue = bfFromBits (fpOpts e p NearEven) bv -- (most significant bit in the significand is set, the rest of it is 0) floatToBits :: Integer -> Integer -> BigFloat -> Integer floatToBits e p bf = bfToBits (fpOpts e p NearEven) bf + + +-- | Create a 64-bit IEEE-754 float. +floatFromDouble :: Double -> BF +floatFromDouble = uncurry BF float64ExpPrec . bfFromDouble diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs index ced6e1c9d..3b7e19aa1 100644 --- a/src/Cryptol/Eval/Type.hs +++ b/src/Cryptol/Eval/Type.hs @@ -18,6 +18,7 @@ import Cryptol.TypeCheck.Solver.InfNat import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Ident (Ident) import Cryptol.Utils.RecordMap +import Cryptol.Utils.Types import Data.Maybe(fromMaybe) import qualified Data.IntMap.Strict as IntMap @@ -86,6 +87,10 @@ tvSeq :: Nat' -> TValue -> TValue tvSeq (Nat n) t = TVSeq n t tvSeq Inf t = TVStream t +-- | The Cryptol @Float64@ type. +tvFloat64 :: TValue +tvFloat64 = uncurry TVFloat float64ExpPrec + -- | Coerce an extended natural into an integer, -- for values known to be finite finNat' :: Nat' -> Integer diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index ca6a1e070..a3f4accb3 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -68,6 +68,7 @@ import qualified Cryptol.ModuleSystem.Renamer as M import qualified Cryptol.Utils.Ident as M import qualified Cryptol.ModuleSystem.Env as M +import Cryptol.Backend.FloatHelpers as FP import qualified Cryptol.Backend.Monad as E import qualified Cryptol.Backend.SeqMap as E import Cryptol.Eval.Concrete( Concrete(..) ) @@ -260,7 +261,11 @@ nbCommandList = , "The amount of time to spend collecting measurements can be changed" , " with the timeMeasurementPeriod option." , "Reports the average wall clock time, CPU time, and cycles." - , "(Cycles are in unspecified units that may be CPU cycles.)"]) + , " (Cycles are in unspecified units that may be CPU cycles.)" + , "Binds the result to" + , " it : { avgTime : Float64" + , " , avgCpuTime : Float64" + , " , avgCycles : Integer }" ]) ] commandList :: [CommandDescr] @@ -1022,6 +1027,14 @@ timeCmd str pos fnm = do rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime ++ " Avg CPU time: " ++ Bench.secs benchAvgCpuTime ++ " Avg cycles: " ++ show benchAvgCycles + let mkStatsRec time cpuTime cycles = recordFromFields + [("avgTime", time), ("avgCpuTime", cpuTime), ("avgCycles", cycles)] + itType = E.TVRec $ mkStatsRec E.tvFloat64 E.tvFloat64 E.TVInteger + itVal = E.VRecord $ mkStatsRec + (pure $ E.VFloat $ FP.floatFromDouble benchAvgTime) + (pure $ E.VFloat $ FP.floatFromDouble benchAvgCpuTime) + (pure $ E.VInteger $ toInteger benchAvgCycles) + bindItVariableVal itType itVal readFileCmd :: FilePath -> REPL () readFileCmd fp = do diff --git a/src/Cryptol/TypeCheck/FFI.hs b/src/Cryptol/TypeCheck/FFI.hs index 3a845cb06..f4bae6e20 100644 --- a/src/Cryptol/TypeCheck/FFI.hs +++ b/src/Cryptol/TypeCheck/FFI.hs @@ -16,6 +16,7 @@ import Cryptol.TypeCheck.FFI.FFIType import Cryptol.TypeCheck.SimpType import Cryptol.TypeCheck.Type import Cryptol.Utils.RecordMap +import Cryptol.Utils.Types -- | Convert a 'Schema' to a 'FFIFunType', along with any 'Prop's that must be -- satisfied for the 'FFIFunType' to be valid. @@ -96,8 +97,8 @@ toFFIBasicType t = | otherwise -> Just $ Left $ FFITypeError t FFIBadWordSize where word = Just . Right . FFIWord n TCon (TC TCFloat) [TCon (TC (TCNum e)) [], TCon (TC (TCNum p)) []] - | e == 8, p == 24 -> float FFIFloat32 - | e == 11, p == 53 -> float FFIFloat64 + | (e, p) == float32ExpPrec -> float FFIFloat32 + | (e, p) == float64ExpPrec -> float FFIFloat64 | otherwise -> Just $ Left $ FFITypeError t FFIBadFloatSize where float = Just . Right . FFIFloat e p _ -> Nothing From f5fc53d2b01a6532c35837406dea4323646ce11c Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 30 Aug 2022 14:25:28 -0700 Subject: [PATCH 15/18] time command: Add Cryptol.Utils.Types --- src/Cryptol/Utils/Types.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 src/Cryptol/Utils/Types.hs diff --git a/src/Cryptol/Utils/Types.hs b/src/Cryptol/Utils/Types.hs new file mode 100644 index 000000000..60cff6eeb --- /dev/null +++ b/src/Cryptol/Utils/Types.hs @@ -0,0 +1,10 @@ +-- | Useful information about various types. +module Cryptol.Utils.Types where + +-- | Exponent and precision of 32-bit IEEE-754 floating point. +float32ExpPrec :: (Integer, Integer) +float32ExpPrec = (8, 24) + +-- | Exponent and precision of 64-bit IEEE-754 floating point. +float64ExpPrec :: (Integer, Integer) +float64ExpPrec = (11, 53) From 0b49544aa946264e189e12c31bcae5432d516db0 Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 30 Aug 2022 14:36:32 -0700 Subject: [PATCH 16/18] time command: add timeQuiet option --- src/Cryptol/REPL/Command.hs | 11 +++++++---- src/Cryptol/REPL/Monad.hs | 3 +++ 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index a3f4accb3..849c7068b 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -1016,7 +1016,9 @@ typeOfCmd str pos fnm = do timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL () timeCmd str pos fnm = do period <- getKnownUser "timeMeasurementPeriod" :: REPL Int - rPutStrLn $ "Measuring for " ++ show period ++ " seconds" + quiet <- getKnownUser "timeQuiet" + unless quiet $ + rPutStrLn $ "Measuring for " ++ show period ++ " seconds" pExpr <- replParseExpr str pos fnm (_, def, sig) <- replCheckExpr pExpr replPrepareCheckedExpr def sig >>= \case @@ -1024,9 +1026,10 @@ timeCmd str pos fnm = do Just (_, expr) -> do Bench.BenchmarkStats {..} <- liftModuleCmd (rethrowEvalError . M.benchmarkExpr (fromIntegral period) expr) - rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime - ++ " Avg CPU time: " ++ Bench.secs benchAvgCpuTime - ++ " Avg cycles: " ++ show benchAvgCycles + unless quiet $ + rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime + ++ " Avg CPU time: " ++ Bench.secs benchAvgCpuTime + ++ " Avg cycles: " ++ show benchAvgCycles let mkStatsRec time cpuTime cycles = recordFromFields [("avgTime", time), ("avgCpuTime", cpuTime), ("avgCycles", cycles)] itType = E.TVRec $ mkStatsRec E.tvFloat64 E.tvFloat64 E.TVInteger diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 062693d1f..ca60dca60 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -992,6 +992,9 @@ userOptions = mkOptionMap , "This is a lower bound and the actual time taken might be higher if the" , " evaluation takes a long time." ] + + , simpleOpt "timeQuiet" ["time-quiet"] (EnvBool False) noCheck + "Suppress output of :time command and only bind result to `it`." ] From d1a9971edd1e1a12c7f19f0a109f95234da12bb3 Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 30 Aug 2022 14:42:47 -0700 Subject: [PATCH 17/18] time command: Add test --- tests/issues/issue1415.icry | 3 +++ tests/issues/issue1415.icry.stdout | 2 ++ 2 files changed, 5 insertions(+) create mode 100644 tests/issues/issue1415.icry create mode 100644 tests/issues/issue1415.icry.stdout diff --git a/tests/issues/issue1415.icry b/tests/issues/issue1415.icry new file mode 100644 index 000000000..85f20a570 --- /dev/null +++ b/tests/issues/issue1415.icry @@ -0,0 +1,3 @@ +:set timeQuiet=on +:time 0x1 + 0x2 +:t it diff --git a/tests/issues/issue1415.icry.stdout b/tests/issues/issue1415.icry.stdout new file mode 100644 index 000000000..deb1890a2 --- /dev/null +++ b/tests/issues/issue1415.icry.stdout @@ -0,0 +1,2 @@ +Loading module Cryptol +it : {avgTime : Float 11 53, avgCpuTime : Float 11 53, avgCycles : Integer} From 7fd1e4dd9a3e3d778d2fe8e5dc54a4e582f94138 Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 30 Aug 2022 16:34:46 -0700 Subject: [PATCH 18/18] time command: Add note on laziness --- src/Cryptol/REPL/Command.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 849c7068b..a988d92ab 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -258,6 +258,10 @@ nbCommandList = "Measure the time it takes to evaluate the given expression." (unlines [ "The expression will be evaluated many times to get accurate results." + , "Note that the first evaluation of a binding may take longer due to" + , " laziness, and this may affect the reported time. If this is not" + , " desired then make sure to evaluate the expression once first before" + , " running :time." , "The amount of time to spend collecting measurements can be changed" , " with the timeMeasurementPeriod option." , "Reports the average wall clock time, CPU time, and cycles."