Add handling for seedable RNG in cryptol REPL

src/Cryptol/REPL/Command.hs

@@ -109,6 +109,8 @@ import qualified Control.Exception as X
 import Control.Monad hiding (mapM, mapM)
 import qualified Control.Monad.Catch as Ex
 import Control.Monad.IO.Class(liftIO)
+import Text.Read (readMaybe)
+import Control.Applicative ((<|>))
 import Data.ByteString (ByteString)
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Char8 as BS8
@@ -130,7 +132,8 @@ import qualified Data.Set as Set
 import System.IO
          (Handle,hFlush,stdout,openTempFile,hClose,openFile
          ,IOMode(..),hGetContents,hSeek,SeekMode(..))
-import System.Random.TF(newTFGen)
+import qualified System.Random.TF as TF
+import qualified System.Random.TF.Instances as TFI
 import Numeric (showFFloat)
 import qualified Data.Text as T
 import Data.IORef(newIORef,readIORef,writeIORef)
@@ -142,6 +145,8 @@ import Prelude.Compat
 
 import qualified Data.SBV.Internals as SBV (showTDiff)
 
+
+
 -- Commands --------------------------------------------------------------------
 
 -- | Commands.
@@ -272,6 +277,17 @@ nbCommandList  =
       , "  it : { avgTime : Float64"
       , "       , avgCpuTime : Float64"
       , "       , avgCycles : Integer }" ])
+
+  , CommandDescr [ ":set-seed" ] ["SEED"] (OptionArg seedCmd)
+      "Seed the random number generator for operations using randomness"
+      (unlines
+        [ "A seed takes the form of either a single integer or a 4-tuple"
+        , "of unsigned 64-bit integers.  Examples of commands using randomness"
+        , "are dumpTests and check."
+        ])
+  , CommandDescr [ ":new-seed"] [] (NoArg newSeedCmd)
+      "Randomly generate and set a new seed for the random number generator"
+      ""
   ]
 
 commandList :: [CommandDescr]
@@ -317,6 +333,8 @@ commandList  =
       [ "Converts all foreign declarations in the given Cryptol file into C"
       , "function declarations, and writes them to a file with the same name"
       , "but with a .h extension." ])
+
+
   ]
 
 genHelp :: [CommandDescr] -> [String]
@@ -395,14 +413,13 @@ dumpTestsCmd outFile str pos fnm =
      (val, ty) <- replEvalExpr expr
      ppopts <- getPPValOpts
      testNum <- getKnownUser "tests" :: REPL Int
-     g <- io newTFGen
      tenv <- E.envTypes . M.deEnv <$> getDynEnv
      let tyv = E.evalValType tenv ty
      gens <-
        case TestR.dumpableType tyv of
          Nothing -> raise (TypeNotTestable ty)
          Just gens -> return gens
-     tests <- io $ TestR.returnTests g gens val testNum
+     tests <- withRandomGen (\g -> io $ TestR.returnTests' g gens val testNum)
      out <- forM tests $
             \(args, x) ->
               do argOut <- mapM (rEval . E.ppValue Concrete ppopts) args
@@ -494,11 +511,11 @@ qcExpr qcMode exprDoc texpr schema =
        Just (sz,tys,_,gens) | qcMode == QCRandom -> do
             rPutStrLn "Using random testing."
             prt testingMsg
-            g <- io newTFGen
             (res,num) <-
-                  Ex.catch (randomTests (\n -> ppProgress percentRef testsRef n testNum)
-                                        testNum val gens g)
-                         (\ex -> do rPutStrLn "\nTest interrupted..."
+              withRandomGen
+                (randomTests' (\n -> ppProgress percentRef testsRef n testNum)
+                                      testNum val gens)
+              `Ex.catch` (\ex -> do rPutStrLn "\nTest interrupted..."
                                     num <- io $ readIORef testsRef
                                     let report = TestReport exprDoc Pass num sz
                                     ppReport tys False report
@@ -1783,6 +1800,31 @@ replEdit file = do
 
 type CommandMap = Trie CommandDescr
 
+newSeedCmd :: REPL ()
+newSeedCmd =
+  do  seed <- createAndSetSeed
+      rPutStrLn "Seed initialized to:"
+      rPutStrLn (show seed)
+  where
+    createAndSetSeed =
+      withRandomGen $ \g0 ->
+        let (s1, g1) = TFI.random g0
+            (s2, g2) = TFI.random g1
+            (s3, g3) = TFI.random g2
+            (s4, _)  = TFI.random g3
+            seed = (s1, s2, s3, s4)
+        in  pure (seed, TF.seedTFGen seed)
+
+seedCmd :: String -> REPL ()
+seedCmd s =
+  case mbGen of
+    Nothing -> rPutStrLn "Could not parse seed argument - expecting an integer or 4-tuple of integers."
+    Just gen -> setRandomGen gen
+
+  where
+    mbGen =
+          (TF.mkTFGen <$> readMaybe s)
+      <|> (TF.seedTFGen <$> readMaybe s)
 
 -- Command Parsing -------------------------------------------------------------
 

src/Cryptol/REPL/Monad.hs

@@ -57,6 +57,9 @@ module Cryptol.REPL.Monad (
   , validEvalContext
   , updateREPLTitle
   , setUpdateREPLTitle
+  , withRandomGen
+  , setRandomGen
+  , getRandomGen
 
     -- ** Config Options
   , EnvVal(..)
@@ -131,6 +134,7 @@ import qualified Data.Set as Set
 import Text.Read (readMaybe)
 
 import Data.SBV (SBVException)
+import qualified System.Random.TF as TF
 
 import Prelude ()
 import Prelude.Compat
@@ -186,13 +190,17 @@ data RW = RW
     -- Used as a kind of id for the current solver, which helps avoid
     -- a race condition where the callback of a dead solver runs after
     -- a new one has been started.
+
+  , eRandomGen :: TF.TFGen
+    -- ^ Random number generator for things like QC and dumpTests
   }
 
 
 -- | Initial, empty environment.
 defaultRW :: Bool -> Bool -> Logger -> IO RW
 defaultRW isBatch callStacks l = do
   env <- M.initialModuleEnv
+  rng <- TF.newTFGen
   let searchPath = M.meSearchPath env
   let solverConfig = T.defaultSolverConfig searchPath
   return RW
@@ -209,6 +217,7 @@ defaultRW isBatch callStacks l = do
     , eTCConfig    = solverConfig
     , eTCSolver    = Nothing
     , eTCSolverRestarts = 0
+    , eRandomGen = rng
     }
 
 -- | Build up the prompt for the REPL.
@@ -652,6 +661,18 @@ setDynEnv denv = do
   me <- getModuleEnv
   setModuleEnv (me { M.meDynEnv = denv })
 
+getRandomGen :: REPL TF.TFGen
+getRandomGen = eRandomGen <$> getRW
+
+setRandomGen :: TF.TFGen -> REPL ()
+setRandomGen rng = modifyRW_ (\s -> s { eRandomGen = rng })
+
+withRandomGen :: (TF.TFGen -> REPL (a, TF.TFGen)) -> REPL a
+withRandomGen repl =
+  do  g <- getRandomGen
+      (result, g') <- repl g
+      setRandomGen g'
+      pure result
 
 -- | Given an existing qualified name, prefix it with a
 -- relatively-unique string. We make it unique by prefixing with a

src/Cryptol/Testing/Random.hs

@@ -23,8 +23,10 @@ module Cryptol.Testing.Random
 , TestResult(..)
 , isPass
 , returnTests
+, returnTests'
 , exhaustiveTests
 , randomTests
+, randomTests'
 ) where
 
 import qualified Control.Exception as X
@@ -96,23 +98,32 @@ returnOneTest fun argGens sz g0 =
      go _ (_ : _) = panic "Cryptol.Testing.Random" ["Too many arguments to function while generating tests"]
      go v [] = return v
 
-
--- | Return a collection of random tests.
 returnTests :: RandomGen g
          => g -- ^ The random generator state
          -> [Gen g Concrete] -- ^ Generators for the function arguments
          -> Value -- ^ The function itself
          -> Int -- ^ How many tests?
          -> IO [([Value], Value)] -- ^ A list of pairs of random arguments and computed outputs
-returnTests g gens fun num = go gens g 0
+                                       --   as well as the new state of the RNG
+returnTests g gens fun num = fst <$> returnTests' g gens fun num
+
+-- | Return a collection of random tests.
+returnTests' :: RandomGen g
+         => g -- ^ The random generator state
+         -> [Gen g Concrete] -- ^ Generators for the function arguments
+         -> Value -- ^ The function itself
+         -> Int -- ^ How many tests?
+         -> IO ([([Value], Value)], g) -- ^ A list of pairs of random arguments and computed outputs
+                                       --   as well as the new state of the RNG
+returnTests' g gens fun num = go gens g 0
   where
     go args g0 n
-      | n >= num = return []
+      | n >= num = return ([], g0)
       | otherwise =
         do let sz = toInteger (div (100 * (1 + n)) num)
            (inputs, output, g1) <- returnOneTest fun args sz g0
-           more <- go args g1 (n + 1)
-           return ((inputs, output) : more)
+           (more, g2) <- go args g1 (n + 1)
+           return ((inputs, output) : more, g2)
 
 {- | Given a (function) type, compute generators for the function's
 arguments. -}
@@ -447,14 +458,23 @@ randomTests :: (MonadIO m, RandomGen g) =>
   [Gen g Concrete] {- ^ input value generators -} ->
   g {- ^ Inital random generator -} ->
   m (TestResult, Integer)
-randomTests ppProgress maxTests val gens = go 0
+randomTests ppProgress maxTests val gens g = fst <$> randomTests' ppProgress maxTests val gens g
+
+randomTests' :: (MonadIO m, RandomGen g) =>
+  (Integer -> m ()) {- ^ progress callback -} ->
+  Integer {- ^ Maximum number of tests to run -} ->
+  Value {- ^ function under test -} ->
+  [Gen g Concrete] {- ^ input value generators -} ->
+  g {- ^ Inital random generator -} ->
+  m ((TestResult, Integer), g)
+randomTests' ppProgress maxTests val gens = go 0
   where
   go !testNum g
-    | testNum >= maxTests = return (Pass, testNum)
+    | testNum >= maxTests = return ((Pass, testNum), g)
     | otherwise =
       do ppProgress testNum
          let sz' = div (100 * (1 + testNum)) maxTests
          (res, g') <- liftIO (runOneTest val gens sz' g)
          case res of
            Pass -> go (testNum+1) g'
-           failure -> return (failure, testNum)
+           failure -> return ((failure, testNum), g)