Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
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
- 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 {}
- runTests :: Monad m => TestSpec m s -> s -> m TestReport
Documentation
:: 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.
:: 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.
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.
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.
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
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 EvalError
s.
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 #
TestSpec | |
|
data TestReport Source #
TestReport | |
|