Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Trustworthy
Language	Haskell2010

Cryptol.Testing.Random

Description

This module generates random values for Cryptol types.

Synopsis

type Gen g x = Integer -> g -> (SEval x (GenValue x), g)
runOneTest :: RandomGen g => EvalOpts -> Value -> [Gen g Concrete] -> Integer -> g -> IO (TestResult, g)
returnOneTest :: RandomGen g => EvalOpts -> Value -> [Gen g Concrete] -> Integer -> g -> IO ([Value], Value, g)
returnTests :: RandomGen g => g -> EvalOpts -> [Gen g Concrete] -> Value -> Int -> IO [([Value], Value)]
dumpableType :: forall g. RandomGen g => Type -> Maybe [Gen g Concrete]
testableTypeGenerators :: RandomGen g => Type -> Maybe [Gen g Concrete]
randomValue :: (Backend sym, RandomGen g) => sym -> Type -> Maybe (Gen g sym)
randomBit :: (Backend sym, RandomGen g) => sym -> Gen g sym
randomSize :: RandomGen g => Int -> Int -> g -> (Int, g)
randomInteger :: (Backend sym, RandomGen g) => sym -> Gen g sym
randomIntMod :: (Backend sym, RandomGen g) => sym -> Integer -> Gen g sym
randomRational :: (Backend sym, RandomGen g) => sym -> Gen g sym
randomWord :: (Backend sym, RandomGen g) => sym -> Integer -> Gen g sym
randomStream :: (Backend sym, RandomGen g) => Gen g sym -> Gen g sym
randomSequence :: (Backend sym, RandomGen g) => Integer -> Gen g sym -> Gen g sym
randomTuple :: (Backend sym, RandomGen g) => [Gen g sym] -> Gen g sym
randomRecord :: (Backend sym, RandomGen g) => RecordMap Ident (Gen g sym) -> Gen g sym
randomFloat :: (Backend sym, RandomGen g) => sym -> Integer -> Integer -> Gen g sym
randomV :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)
data TestResult
- = Pass
- | FailFalse [Value]
- | FailError EvalError [Value]
isPass :: TestResult -> Bool
evalTest :: EvalOpts -> Value -> [Value] -> IO TestResult
testableType :: Type -> Maybe (Maybe Integer, [Type], [[Value]])
typeSize :: Type -> Maybe Integer
typeValues :: Type -> [Value]
data TestSpec m s = TestSpec {
- testFn :: Integer -> s -> m (TestResult, s)
- testProp :: String
- testTotal :: Integer
- testPossible :: Maybe Integer
- testRptProgress :: Integer -> Integer -> m ()
- testClrProgress :: m ()
- testRptFailure :: TestResult -> m ()
- testRptSuccess :: m ()
}
data TestReport = TestReport {
- reportResult :: TestResult
- reportProp :: String
- reportTestsRun :: Integer
- reportTestsPossible :: Maybe Integer
}
runTests :: Monad m => TestSpec m s -> s -> m TestReport

Documentation

type Gen g x = Integer -> g -> (SEval x (GenValue x), g) Source #

runOneTest Source #

Arguments

:: RandomGen g
=> EvalOpts	how to evaluate things
-> Value	Function under test
-> [Gen g Concrete]	Argument generators
-> Integer	Size
-> g
-> IO (TestResult, g)

Apply a testable value to some randomly-generated arguments. Returns Nothing if the function returned True, or Just counterexample if it returned False.

Please note that this function assumes that the generators match the supplied value, otherwise we'll panic.

returnOneTest Source #

Arguments

:: RandomGen g
=> EvalOpts	How to evaluate things
-> Value	Function to be used to calculate tests
-> [Gen g Concrete]	Argument generators
-> Integer	Size
-> g	Initial random state
-> IO ([Value], Value, g)	Arguments, result, and new random state

returnTests Source #

Arguments

:: RandomGen g
=> g	The random generator state
-> EvalOpts	How to evaluate things
-> [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

Return a collection of random tests.

dumpableType :: forall g. RandomGen g => Type -> Maybe [Gen g Concrete] Source #

Given a (function) type, compute generators for the function's arguments. This is like testableTypeGenerators, but allows the result to be any finite type instead of just Bit.

testableTypeGenerators :: RandomGen g => Type -> Maybe [Gen g Concrete] Source #

Given a (function) type, compute generators for the function's arguments. Currently we do not support polymorphic functions. In principle, we could apply these to random types, and test the results.

randomValue :: (Backend sym, RandomGen g) => sym -> Type -> Maybe (Gen g sym) Source #

A generator for values of the given type. This fails if we are given a type that lacks a suitable random value generator.

randomBit :: (Backend sym, RandomGen g) => sym -> Gen g sym Source #

Generate a random bit value.

randomSize :: RandomGen g => Int -> Int -> g -> (Int, g) Source #

randomInteger :: (Backend sym, RandomGen g) => sym -> Gen g sym Source #

Generate a random integer value. The size parameter is assumed to vary between 1 and 100, and we use it to generate smaller numbers first.

randomIntMod :: (Backend sym, RandomGen g) => sym -> Integer -> Gen g sym Source #

randomRational :: (Backend sym, RandomGen g) => sym -> Gen g sym Source #

randomWord :: (Backend sym, RandomGen g) => sym -> Integer -> Gen g sym Source #

Generate a random word of the given length (i.e., a value of type [w]) The size parameter is assumed to vary between 1 and 100, and we use it to generate smaller numbers first.

randomStream :: (Backend sym, RandomGen g) => Gen g sym -> Gen g sym Source #

Generate a random infinite stream value.

randomSequence :: (Backend sym, RandomGen g) => Integer -> Gen g sym -> Gen g sym Source #

Generate a random sequence. This should be used for sequences other than bits. For sequences of bits use "randomWord".

randomTuple :: (Backend sym, RandomGen g) => [Gen g sym] -> Gen g sym Source #

Generate a random tuple value.

randomRecord :: (Backend sym, RandomGen g) => RecordMap Ident (Gen g sym) -> Gen g sym Source #

Generate a random record value.

randomFloat Source #

Arguments

:: (Backend sym, RandomGen g)
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> Gen g sym

randomV :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym) Source #

Produce a random value with the given seed. If we do not support making values of the given type, return zero of that type. TODO: do better than returning zero

data TestResult Source #

A test result is either a pass, a failure due to evaluating to False, or a failure due to an exception raised during evaluation

Constructors

Pass
FailFalse [Value]
FailError EvalError [Value]

isPass :: TestResult -> Bool Source #

evalTest :: EvalOpts -> Value -> [Value] -> IO TestResult Source #

Apply a testable value to some arguments. Note that this function assumes that the values come from a call to testableType (i.e., things are type-correct). We run in the IO monad in order to catch any EvalErrors.

testableType :: Type -> Maybe (Maybe Integer, [Type], [[Value]]) Source #

Given a (function) type, compute all possible inputs for it. We also return the types of the arguments and the total number of test (i.e., the length of the outer list.

typeSize :: Type -> Maybe Integer Source #

Given a fully-evaluated type, try to compute the number of values in it. Returns Nothing for infinite types, user-defined types, polymorphic types, and, currently, function spaces. Of course, we can easily compute the sizes of function spaces, but we can't easily enumerate their inhabitants.

typeValues :: Type -> [Value] Source #

Returns all the values in a type. Returns an empty list of values, for types where typeSize returned Nothing.

data TestSpec m s Source #

Constructors

TestSpec
Fields testFn :: Integer -> s -> m (TestResult, s) testProp :: String The property as entered by the user testTotal :: Integer testPossible :: Maybe Integer Nothing indicates infinity testRptProgress :: Integer -> Integer -> m () testClrProgress :: m () testRptFailure :: TestResult -> m () testRptSuccess :: m ()

data TestReport Source #

Constructors

TestReport
Fields reportResult :: TestResult reportProp :: String The property as entered by the user reportTestsRun :: Integer reportTestsPossible :: Maybe Integer

runTests :: Monad m => TestSpec m s -> s -> m TestReport Source #