diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index c4a0702f..84043128 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/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 ------------------------------------------------------------- diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index aab9651a..af1fff9f 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/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,6 +190,9 @@ 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 } @@ -193,6 +200,7 @@ data RW = RW 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 diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs index 309b02b4..9910e6a0 100644 --- a/src/Cryptol/Testing/Random.hs +++ b/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)