Update benchmarks to find Prelude and CryptolTC.z3

Since they don’t run in the normal REPL environment, they need to know
about where to find the Prelude and CryptolTC.z3 more directly.

bench/Main.hs

@@ -12,6 +12,8 @@ module Main where
 
 import qualified Data.Text.Lazy     as T
 import qualified Data.Text.Lazy.IO  as T
+import           System.FilePath ((</>))
+import qualified System.Directory   as Dir
 
 import qualified Cryptol.Eval as E
 import qualified Cryptol.Eval.Monad as E
@@ -39,7 +41,9 @@ import qualified Data.SBV.Dynamic as SBV
 import Criterion.Main
 
 main :: IO ()
-main = defaultMain [
+main = do
+  cd <- Dir.getCurrentDirectory
+  defaultMain [
     bgroup "parser" [
         parser "Prelude" "lib/Cryptol.cry"
       , parser "Extras"  "lib/Cryptol/Extras.cry"
@@ -49,26 +53,26 @@ main = defaultMain [
       , parser "AES" "bench/data/AES.cry"
       , parser "SHA512" "bench/data/SHA512.cry"
       ]
-  , bgroup "typechecker" [
-        tc "Prelude" "lib/Cryptol.cry"
-      , tc "Extras"  "lib/Cryptol/Extras.cry"
-      , tc "PreludeWithExtras" "bench/data/PreludeWithExtras.cry"
-      , tc "BigSequence" "bench/data/BigSequence.cry"
-      , tc "BigSequenceHex" "bench/data/BigSequenceHex.cry"
-      , tc "AES" "bench/data/AES.cry"
-      , tc "SHA512" "bench/data/SHA512.cry"
+   , bgroup "typechecker" [
+        tc cd "Prelude" "lib/Cryptol.cry"
+      , tc cd "Extras"  "lib/Cryptol/Extras.cry"
+      , tc cd "PreludeWithExtras" "bench/data/PreludeWithExtras.cry"
+      , tc cd "BigSequence" "bench/data/BigSequence.cry"
+      , tc cd "BigSequenceHex" "bench/data/BigSequenceHex.cry"
+      , tc cd "AES" "bench/data/AES.cry"
+      , tc cd "SHA512" "bench/data/SHA512.cry"
       ]
-  , bgroup "conc_eval" [
-        ceval "AES" "bench/data/AES.cry" "bench_correct"
-      , ceval "ZUC" "bench/data/ZUC.cry" "ZUC_TestVectors"
-      , ceval "SHA512" "bench/data/SHA512.cry" "testVector1 ()"
+   , bgroup "conc_eval" [
+        ceval cd "AES" "bench/data/AES.cry" "bench_correct"
+      , ceval cd "ZUC" "bench/data/ZUC.cry" "ZUC_TestVectors"
+      , ceval cd "SHA512" "bench/data/SHA512.cry" "testVector1 ()"
       ]
-  , bgroup "sym_eval" [
-        seval "AES" "bench/data/AES.cry" "bench_correct"
-      , seval "ZUC" "bench/data/ZUC.cry" "ZUC_TestVectors"
-      , seval "SHA512" "bench/data/SHA512.cry" "testVector1 ()"
+   , bgroup "sym_eval" [
+        seval cd "AES" "bench/data/AES.cry" "bench_correct"
+      , seval cd "ZUC" "bench/data/ZUC.cry" "ZUC_TestVectors"
+      , seval cd "SHA512" "bench/data/SHA512.cry" "testVector1 ()"
       ]
-  ]
+   ]
 
 -- | Make a benchmark for parsing a Cryptol module
 parser :: String -> FilePath -> Benchmark
@@ -85,8 +89,9 @@ parser name path =
 
 -- | Make a benchmark for typechecking a Cryptol module. Does parsing
 -- in the setup phase in order to isolate typechecking
-tc :: String -> FilePath -> Benchmark
-tc name path =
+tc :: String -> String -> FilePath -> Benchmark
+tc cd name path =
+  let withLib = M.withPrependedSearchPath [cd </> "lib"] in
   let setup = do
         bytes <- T.readFile path
         let cfg = P.defaultConfig
@@ -95,7 +100,7 @@ tc name path =
                 }
             Right pm = P.parseModule cfg bytes
         menv <- M.initialModuleEnv
-        (Right ((prims, scm, tcEnv), menv'), _) <- M.runModuleM menv $ do
+        (Right ((prims, scm, tcEnv), menv'), _) <- M.runModuleM menv $ withLib $ do
           -- code from `loadModule` and `checkModule` in
           -- `Cryptol.ModuleSystem.Base`
           let pm' = M.addPrelude pm
@@ -109,18 +114,19 @@ tc name path =
           return (prims, scm, tcEnv)
         return (prims, scm, tcEnv, menv')
   in env setup $ \ ~(prims, scm, tcEnv, menv) ->
-    bench name $ nfIO $ M.runModuleM menv $ do
+    bench name $ nfIO $ M.runModuleM menv $ 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 tcEnv
 
-ceval :: String -> FilePath -> T.Text -> Benchmark
-ceval name path expr =
+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
-        (Right (texpr, menv'), _) <- M.runModuleM menv $ do
+        (Right (texpr, menv'), _) <- M.runModuleM menv $ withLib $ do
           m <- M.loadModuleByPath path
           M.setFocusedModule (T.mName m)
           let Right pexpr = P.parseExpr expr
@@ -129,16 +135,17 @@ ceval name path expr =
         return (texpr, menv')
   in env setup $ \ ~(texpr, menv) ->
     bench name $ nfIO $ E.runEval $ do
-      env <- E.evalDecls (S.allDeclGroups menv) mempty
-      (e :: E.Value) <- E.evalExpr env texpr
+      env' <- E.evalDecls (S.allDeclGroups menv) mempty
+      (e :: E.Value) <- E.evalExpr env' texpr
       E.forceValue e
 
 
-seval :: String -> FilePath -> T.Text -> Benchmark
-seval name path expr =
+seval :: String -> String -> FilePath -> T.Text -> Benchmark
+seval cd name path expr =
+  let withLib = M.withPrependedSearchPath [cd </> "lib"] in
   let setup = do
         menv <- M.initialModuleEnv
-        (Right (texpr, menv'), _) <- M.runModuleM menv $ do
+        (Right (texpr, menv'), _) <- M.runModuleM menv $ withLib $ do
           m <- M.loadModuleByPath path
           M.setFocusedModule (T.mName m)
           let Right pexpr = P.parseExpr expr
@@ -147,7 +154,7 @@ seval name path expr =
         return (texpr, menv')
   in env setup $ \ ~(texpr, menv) ->
     bench name $ nfIO $ E.runEval $ do
-      env <- E.evalDecls (S.allDeclGroups menv) mempty
-      (e :: S.Value) <- E.evalExpr env texpr
+      env' <- E.evalDecls (S.allDeclGroups menv) mempty
+      (e :: S.Value) <- E.evalExpr env' texpr
       E.io $ SBV.compileToSMTLib SBV.SMTLib2 False $
          return (S.fromVBit e)

bench/data/SHA512.cry

@@ -2,11 +2,14 @@
 
 module SHA512 where
 
+/*
 sha512 : {b, a} (a*1024 == 128 + b + 1 + 1024 - (b+129) % 1024,
                  a*1024 % 1024 == 0,
                  a * 1024 - b >= 129,
                  2^^128 - 1 >= b,
                  fin (a + 1)) => [b] -> [512]
+
+                 */
 sha512 M = result
   where
     M' = (pad M)

cryptol.cabal

@@ -261,5 +261,7 @@ benchmark cryptol-bench
                      , criterion
                      , cryptol
                      , deepseq
+                     , directory
+                     , filepath
                      , sbv
                      , text

src/Cryptol/ModuleSystem/Monad.hs

@@ -28,7 +28,7 @@ import qualified Cryptol.Parser.NoInclude as NoInc
 import qualified Cryptol.TypeCheck as T
 import qualified Cryptol.TypeCheck.AST as T
 import           Cryptol.Parser.Position (Range)
-import           Cryptol.Utils.Ident (interactiveName)
+import           Cryptol.Utils.Ident (interactiveName, packModName)
 import           Cryptol.Utils.PP
 
 import Control.Monad.IO.Class
@@ -346,8 +346,7 @@ getImportSource  = ModuleT $ do
   ro <- ask
   case roLoading ro of
     is : _ -> return is
-    _      -> panic "ModuleSystem: getImportSource" ["Import stack is empty"]
-
+    _      -> return (FromModule (packModName ["<none>"])) -- panic "ModuleSystem: getImportSource" ["Import stack is empty"]
 
 getIface :: P.ModName -> ModuleM Iface
 getIface mn = ModuleT $ do