From 09afc2f0a4749a73ab6c11948e7ac497ebcd03c3 Mon Sep 17 00:00:00 2001 From: James LaMar Date: Mon, 14 Nov 2022 15:54:52 -0800 Subject: [PATCH 1/2] Add handling for seedable RNG in cryptol REPL --- src/Cryptol/REPL/Command.hs | 56 ++++++++++++++++++++++++++++++----- src/Cryptol/REPL/Monad.hs | 21 +++++++++++++ src/Cryptol/Testing/Random.hs | 15 +++++----- 3 files changed, 78 insertions(+), 14 deletions(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index c4a0702f3..a1c203a38 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 aab9651a3..af1fff9f4 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 309b02b42..54be15a43 100644 --- a/src/Cryptol/Testing/Random.hs +++ b/src/Cryptol/Testing/Random.hs @@ -103,16 +103,17 @@ returnTests :: RandomGen g -> [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 + -> 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. -} @@ -446,15 +447,15 @@ randomTests :: (MonadIO m, RandomGen g) => Value {- ^ function under test -} -> [Gen g Concrete] {- ^ input value generators -} -> g {- ^ Inital random generator -} -> - m (TestResult, Integer) + 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) From 3b9cea31a7f5b74d1d3e6b558924eefbb1acea3e Mon Sep 17 00:00:00 2001 From: James LaMar Date: Tue, 15 Nov 2022 11:53:50 -0800 Subject: [PATCH 2/2] Preserve previous Random API --- src/Cryptol/REPL/Command.hs | 4 ++-- src/Cryptol/Testing/Random.hs | 25 ++++++++++++++++++++++--- 2 files changed, 24 insertions(+), 5 deletions(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index a1c203a38..840431281 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -419,7 +419,7 @@ dumpTestsCmd outFile str pos fnm = case TestR.dumpableType tyv of Nothing -> raise (TypeNotTestable ty) Just gens -> return gens - tests <- withRandomGen (\g -> 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 @@ -513,7 +513,7 @@ qcExpr qcMode exprDoc texpr schema = prt testingMsg (res,num) <- withRandomGen - (randomTests (\n -> ppProgress percentRef testsRef n testNum) + (randomTests' (\n -> ppProgress percentRef testsRef n testNum) testNum val gens) `Ex.catch` (\ex -> do rPutStrLn "\nTest interrupted..." num <- io $ readIORef testsRef diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs index 54be15a43..9910e6a0e 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,16 +98,24 @@ returnOneTest fun argGens sz g0 = go _ (_ : _) = panic "Cryptol.Testing.Random" ["Too many arguments to function while generating tests"] go v [] = return v +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 + -- 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 +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 +returnTests' g gens fun num = go gens g 0 where go args g0 n | n >= num = return ([], g0) @@ -442,13 +452,22 @@ exhaustiveTests ppProgress val = go 0 failure -> return (failure, testNum) 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) +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 +randomTests' ppProgress maxTests val gens = go 0 where go !testNum g | testNum >= maxTests = return ((Pass, testNum), g)