Merge pull request #1420 from GaloisInc/time-command

Add `:time` command

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

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,
@@ -116,6 +118,8 @@ library
                        Cryptol.Utils.Misc,
                        Cryptol.Utils.Patterns,
                        Cryptol.Utils.Logger,
+                       Cryptol.Utils.Benchmark,
+                       Cryptol.Utils.Types,
                        Cryptol.Version,
 
                        Cryptol.ModuleSystem,

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

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

src/Cryptol/ModuleSystem.hs

@@ -20,6 +20,7 @@ module Cryptol.ModuleSystem (
   , loadModuleByName
   , checkExpr
   , evalExpr
+  , benchmarkExpr
   , checkDecls
   , evalDecls
   , noPat
@@ -47,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 ------------------------------------------------------------
@@ -97,6 +99,11 @@ 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))
+
 -- | Typecheck top-level declarations.
 checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup], Map Name T.TySyn)
 checkDecls ds env = runModuleM env

src/Cryptol/ModuleSystem/Base.hs

@@ -75,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 )
@@ -611,6 +612,22 @@ evalExpr e = do
 
   io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e)
 
+benchmarkExpr :: Double -> T.Expr -> ModuleM BenchmarkStats
+benchmarkExpr period 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 period eval e
+
 evalDecls :: [T.DeclGroup] -> ModuleM ()
 evalDecls dgs = do
   env <- getEvalEnv

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(..) )
@@ -88,6 +89,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
@@ -252,6 +254,22 @@ 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."
+    (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."
+      , "  (Cycles are in unspecified units that may be CPU cycles.)"
+      , "Binds the result to"
+      , "  it : { avgTime : Float64"
+      , "       , avgCpuTime : Float64"
+      , "       , avgCycles : Integer }" ])
   ]
 
 commandList :: [CommandDescr]
@@ -999,6 +1017,32 @@ 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
+  period <- getKnownUser "timeMeasurementPeriod" :: REPL Int
+  quiet <- getKnownUser "timeQuiet"
+  unless quiet $
+    rPutStrLn $ "Measuring for " ++ show period ++ " seconds"
+  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 (fromIntegral period) expr)
+      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
+          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
   bytes <- replReadFile fp (\err -> rPutStrLn (show err) >> return Nothing)
@@ -1569,39 +1613,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

src/Cryptol/REPL/Monad.hs

@@ -983,6 +983,18 @@ 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."
+    ]
+
+  , simpleOpt "timeQuiet" ["time-quiet"] (EnvBool False) noCheck
+    "Suppress output of :time command and only bind result to `it`."
   ]
 
 
@@ -1078,6 +1090,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 ()

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

src/Cryptol/Utils/Benchmark.hs

@@ -0,0 +1,36 @@
+-- | Simple benchmarking of IO functions.
+module Cryptol.Utils.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
+
+-- | 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
+  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
+    , benchAvgCpuTime = sumMeasure measCpuTime / fromIntegral len
+    , benchAvgCycles = sumMeasure measCycles `div` fromIntegral len }

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)

tests/issues/issue1415.icry

@@ -0,0 +1,3 @@
+:set timeQuiet=on
+:time 0x1 + 0x2
+:t it

tests/issues/issue1415.icry.stdout

@@ -0,0 +1,2 @@
+Loading module Cryptol
+it : {avgTime : Float 11 53, avgCpuTime : Float 11 53, avgCycles : Integer}