|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Go to the source code of this file.
Classes | |
| struct | curandStateTest |
| struct | curandStateXORWOW |
| struct | curandStateSobol32 |
| struct | curandStateScrambledSobol32 |
| struct | curandStateSobol64 |
| struct | curandStateScrambledSobol64 |
Macros | |
| #define | MAX_XOR_N (5) |
| #define | SKIPAHEAD_BLOCKSIZE (4) |
| #define | SKIPAHEAD_MASK ((1 << SKIPAHEAD_BLOCKSIZE) - 1) |
| #define | CURAND_2POW32_INV (2.3283064e-10f) |
| #define | CURAND_2POW32_INV_DOUBLE (2.3283064365386963e-10) |
| #define | CURAND_2POW53_INV_DOUBLE (1.1102230246251565e-16) |
| #define | CURAND_2POW32_INV_2PI (2.3283064e-10f * 6.2831855f) |
| #define | CURAND_2POW53_INV_2PI_DOUBLE (1.1102230246251565e-16 * 6.2831853071795860) |
| #define | CURAND_SQRT2 (-1.4142135f) |
| #define | CURAND_SQRT2_DOUBLE (-1.4142135623730951) |
| #define | PRECALC_NUM_MATRICES (8) |
| #define | PRECALC_BLOCK_SIZE (2) |
| #define | PRECALC_BLOCK_MASK ((1 << PRECALC_BLOCK_SIZE) - 1) |
| #define | XORWOW_SEQUENCE_SPACING (67) |
| #define | QUALIFIERS static inline __device__ |
Typedefs | |
| typedef struct curandStateTest | curandStateTest_t |
| typedef struct curandStateXORWOW | curandStateXORWOW_t |
| CURAND XORWOW state. | |
| typedef struct curandStateSobol32 | curandStateSobol32_t |
| CURAND Sobol32 state. | |
| typedef struct curandStateScrambledSobol32 | curandStateScrambledSobol32_t |
| CURAND Scrambled Sobol32 state. | |
| typedef struct curandStateSobol64 | curandStateSobol64_t |
| CURAND Sobol64 state. | |
| typedef struct curandStateScrambledSobol64 | curandStateScrambledSobol64_t |
| CURAND Scrambled Sobol64 state. | |
| typedef struct curandStateXORWOW | curandState_t |
| Default RNG. | |
| typedef struct curandStateXORWOW | curandState |
Functions | |
| void | __curand_matvec (unsigned int *vector, unsigned int *matrix, unsigned int *result, int n) |
| void | __curand_matidentity (unsigned int *matrix, int n) |
| void | __curand_matmat (unsigned int *matrixA, unsigned int *matrixB, int n) |
| void | __curand_veccopy (unsigned int *vector, unsigned int *vectorA, int n) |
| void | __curand_matcopy (unsigned int *matrix, unsigned int *matrixA, int n) |
| void | __curand_matpow (unsigned int *matrix, unsigned int *matrixA, unsigned long long p, int n) |
| float | __curand_uint32AsFloat (unsigned int i) |
| double | __curand_hilouint32AsDouble (unsigned int hi, unsigned int lo) |
| float | __curand_uint32_as_float (unsigned int x) |
| void | curand_init (unsigned long long seed, unsigned long long subsequence, unsigned long long offset, curandStateTest_t *state) |
| unsigned int | curand (curandStateTest_t *state) |
| void | skipahead (unsigned long long n, curandStateTest_t *state) |
| template<typename T, int n> | |
| void | __curand_generate_skipahead_matrix_xor (unsigned int matrix[]) |
| template<typename T, int n> | |
| void | _skipahead_scratch (unsigned long long x, T *state, unsigned int *scratch) |
| template<typename T, int n> | |
| void | _skipahead_sequence_scratch (unsigned long long x, T *state, unsigned int *scratch) |
| void | skipahead (unsigned long long n, curandStateXORWOW_t *state) |
Update XORWOW state to skip n elements. | |
| void | skipahead_sequence (unsigned long long n, curandStateXORWOW_t *state) |
Update XORWOW state to skip ahead n subsequences. | |
| void | _curand_init_scratch (unsigned long long seed, unsigned long long subsequence, unsigned long long offset, curandStateXORWOW_t *state, unsigned int *scratch) |
| void | curand_init (unsigned long long seed, unsigned long long subsequence, unsigned long long offset, curandStateXORWOW_t *state) |
| Initialize XORWOW state. | |
| unsigned int | curand (curandStateXORWOW_t *state) |
| Return 32-bits of pseudorandomness from an XORWOW generator. | |
| template<typename T> | |
| void | skipahead (unsigned int n, T state) |
Update Sobol32 state to skip n elements. | |
| template<typename T> | |
| void | skipahead (unsigned long long n, T state) |
Update Sobol64 state to skip n elements. | |
| template<typename XT> | |
| int | __curand_find_trailing_zero (XT x) |
| Initialize Sobol32 state. | |
| void | curand_init (curandDirectionVectors64_t direction_vectors, unsigned long long offset, curandStateSobol64_t *state) |
| Initialize Sobol64 state. | |
| template<typename PT> | |
| void | _skipahead_stride (int n_log2, PT state) |
| void | curand_init (curandDirectionVectors64_t direction_vectors, unsigned long long scramble_c, unsigned long long offset, curandStateScrambledSobol64_t *state) |
| Initialize Scrambled Sobol64 state. | |
| unsigned int | curand (curandStateSobol32_t *state) |
| Return 32-bits of quasirandomness from a Sobol32 generator. | |
| unsigned int | curand (curandStateScrambledSobol32_t *state) |
| Return 32-bits of quasirandomness from a scrambled Sobol32 generator. | |
| unsigned long long | curand (curandStateSobol64_t *state) |
| Return 64-bits of quasirandomness from a Sobol64 generator. | |
| unsigned long long | curand (curandStateScrambledSobol64_t *state) |
| Return 64-bits of quasirandomness from a scrambled Sobol64 generator. | |
| float | _curand_uniform (unsigned int x) |
| float | _curand_uniform (unsigned long long x) |
| double | _curand_uniform_double (unsigned int x) |
| double | _curand_uniform_double (unsigned long long x) |
| double | _curand_uniform_double_hq (unsigned int x, unsigned int y) |
| double | _curand_uniform_double_64 (unsigned long long x) |
| float | curand_uniform (curandStateTest_t *state) |
| double | curand_uniform_double (curandStateTest_t *state) |
| float | curand_uniform (curandStateXORWOW_t *state) |
| Return a uniformly distributed float from an XORWOW generator. | |
| double | curand_uniform_double (curandStateXORWOW_t *state) |
| Return a uniformly distributed double from an XORWOW generator. | |
| float | curand_uniform (curandStateSobol32_t *state) |
| Return a uniformly distributed float from a Sobol32 generator. | |
| double | curand_uniform_double (curandStateSobol32_t *state) |
| Return a uniformly distributed double from a Sobol32 generator. | |
| float | curand_uniform (curandStateScrambledSobol32_t *state) |
| Return a uniformly distributed float from a scrambled Sobol32 generator. | |
| double | curand_uniform_double (curandStateScrambledSobol32_t *state) |
| Return a uniformly distributed double from a scrambled Sobol32 generator. | |
| float | curand_uniform (curandStateSobol64_t *state) |
| Return a uniformly distributed float from a Sobol64 generator. | |
| double | curand_uniform_double (curandStateSobol64_t *state) |
| Return a uniformly distributed double from a Sobol64 generator. | |
| float | curand_uniform (curandStateScrambledSobol64_t *state) |
| Return a uniformly distributed float from a scrambled Sobol64 generator. | |
| double | curand_uniform_double (curandStateScrambledSobol64_t *state) |
| Return a uniformly distributed double from a scrambled Sobol64 generator. | |
Variables | |
| static unsigned int | precalc_xorwow_matrix [8][2] = {{850664906UL, 4258393217UL}} |
| #define CURAND_2POW32_INV (2.3283064e-10f) |
| #define CURAND_2POW32_INV_2PI (2.3283064e-10f * 6.2831855f) |
| #define CURAND_2POW32_INV_DOUBLE (2.3283064365386963e-10) |
| #define CURAND_2POW53_INV_2PI_DOUBLE (1.1102230246251565e-16 * 6.2831853071795860) |
| #define CURAND_2POW53_INV_DOUBLE (1.1102230246251565e-16) |
| #define CURAND_SQRT2 (-1.4142135f) |
| #define CURAND_SQRT2_DOUBLE (-1.4142135623730951) |
| #define MAX_XOR_N (5) |
| #define PRECALC_BLOCK_MASK ((1 << PRECALC_BLOCK_SIZE) - 1) |
| #define PRECALC_BLOCK_SIZE (2) |
| #define PRECALC_NUM_MATRICES (8) |
| #define QUALIFIERS static inline __device__ |
| #define SKIPAHEAD_BLOCKSIZE (4) |
| #define SKIPAHEAD_MASK ((1 << SKIPAHEAD_BLOCKSIZE) - 1) |
| #define XORWOW_SEQUENCE_SPACING (67) |
| typedef struct curandStateXORWOW curandState |
| typedef struct curandStateXORWOW curandState_t |
Default RNG.
| typedef struct curandStateScrambledSobol32 curandStateScrambledSobol32_t |
CURAND Scrambled Sobol32 state.
| typedef struct curandStateScrambledSobol64 curandStateScrambledSobol64_t |
CURAND Scrambled Sobol64 state.
| typedef struct curandStateSobol32 curandStateSobol32_t |
CURAND Sobol32 state.
| typedef struct curandStateSobol64 curandStateSobol64_t |
CURAND Sobol64 state.
| typedef struct curandStateTest curandStateTest_t |
| typedef struct curandStateXORWOW curandStateXORWOW_t |
CURAND XORWOW state.
| int __curand_find_trailing_zero | ( | XT | x | ) |
Initialize Sobol32 state.
Initialize Sobol32 state in state with the given direction vectors and offset.
The direction vector is a device pointer to an array of 32 unsigned ints. All input values of offset are legal.
| direction_vectors | - Pointer to array of 32 unsigned ints representing the direction vectors for the desired dimension |
| offset | - Absolute offset into sequence |
| state | - Pointer to state to initialize |
Initialize Scrambled Sobol32 state.
Initialize Sobol32 state in state with the given direction vectors and offset.
The direction vector is a device pointer to an array of 32 unsigned ints. All input values of offset are legal.
| direction_vectors | - Pointer to array of 32 unsigned ints representing the direction vectors for the desired dimension |
| scramble_c | Scramble constant |
| offset | - Absolute offset into sequence |
| state | - Pointer to state to initialize |
| void _curand_init_scratch | ( | unsigned long long | seed, |
| unsigned long long | subsequence, | ||
| unsigned long long | offset, | ||
| curandStateXORWOW_t * | state, | ||
| unsigned int * | scratch ) |
| float _curand_uniform | ( | unsigned long long | x | ) |
| double _curand_uniform_double | ( | unsigned int | x | ) |
| double _curand_uniform_double | ( | unsigned long long | x | ) |
| double _curand_uniform_double_64 | ( | unsigned long long | x | ) |
| void _skipahead_stride | ( | int | n_log2, |
| PT | state ) |
| unsigned int curand | ( | curandStateScrambledSobol32_t * | state | ) |
Return 32-bits of quasirandomness from a scrambled Sobol32 generator.
Return 32-bits of quasirandomness from the scrambled Sobol32 generator in state, increment position of generator by one.
| state | - Pointer to state to update |
| unsigned long long curand | ( | curandStateScrambledSobol64_t * | state | ) |
Return 64-bits of quasirandomness from a scrambled Sobol64 generator.
Return 64-bits of quasirandomness from the scrambled Sobol32 generator in state, increment position of generator by one.
| state | - Pointer to state to update |
| unsigned int curand | ( | curandStateSobol32_t * | state | ) |
Return 32-bits of quasirandomness from a Sobol32 generator.
Return 32-bits of quasirandomness from the Sobol32 generator in state, increment position of generator by one.
| state | - Pointer to state to update |
| unsigned long long curand | ( | curandStateSobol64_t * | state | ) |
Return 64-bits of quasirandomness from a Sobol64 generator.
Return 64-bits of quasirandomness from the Sobol64 generator in state, increment position of generator by one.
| state | - Pointer to state to update |
| unsigned int curand | ( | curandStateTest_t * | state | ) |
| unsigned int curand | ( | curandStateXORWOW_t * | state | ) |
Return 32-bits of pseudorandomness from an XORWOW generator.
Return 32-bits of pseudorandomness from the XORWOW generator in state, increment position of generator by one.
| state | - Pointer to state to update |
| void curand_init | ( | curandDirectionVectors64_t | direction_vectors, |
| unsigned long long | offset, | ||
| curandStateSobol64_t * | state ) |
Initialize Sobol64 state.
Initialize Sobol64 state in state with the given direction vectors and offset.
The direction vector is a device pointer to an array of 64 unsigned long longs. All input values of offset are legal.
| direction_vectors | - Pointer to array of 64 unsigned long longs representing the direction vectors for the desired dimension |
| offset | - Absolute offset into sequence |
| state | - Pointer to state to initialize |
| void curand_init | ( | curandDirectionVectors64_t | direction_vectors, |
| unsigned long long | scramble_c, | ||
| unsigned long long | offset, | ||
| curandStateScrambledSobol64_t * | state ) |
Initialize Scrambled Sobol64 state.
Initialize Sobol64 state in state with the given direction vectors and offset.
The direction vector is a device pointer to an array of 64 unsigned long longs. All input values of offset are legal.
| direction_vectors | - Pointer to array of 64 unsigned long longs representing the direction vectors for the desired dimension |
| scramble_c | Scramble constant |
| offset | - Absolute offset into sequence |
| state | - Pointer to state to initialize |
| void curand_init | ( | unsigned long long | seed, |
| unsigned long long | subsequence, | ||
| unsigned long long | offset, | ||
| curandStateTest_t * | state ) |
| void curand_init | ( | unsigned long long | seed, |
| unsigned long long | subsequence, | ||
| unsigned long long | offset, | ||
| curandStateXORWOW_t * | state ) |
Initialize XORWOW state.
Initialize XORWOW state in state with the given seed, subsequence, and offset.
All input values of seed, subsequence, and offset are legal. Large values for subsequence and offset require more computation and so will take more time to complete.
A value of 0 for seed sets the state to the values of the original published version of the xorwow algorithm.
| seed | - Arbitrary bits to use as a seed |
| subsequence | - Subsequence to start at |
| offset | - Absolute offset into sequence |
| state | - Pointer to state to initialize |
| float curand_uniform | ( | curandStateScrambledSobol32_t * | state | ) |
Return a uniformly distributed float from a scrambled Sobol32 generator.
Return a uniformly distributed float between 0.0f and 1.0f from the scrambled Sobol32 generator in state, increment position of generator. Output range excludes 0.0f but includes 1.0f. Denormalized floating point outputs are never returned.
The implementation is guaranteed to use a single call to curand().
| state | - Pointer to state to update |
0.0f and 1.0f | float curand_uniform | ( | curandStateScrambledSobol64_t * | state | ) |
Return a uniformly distributed float from a scrambled Sobol64 generator.
Return a uniformly distributed float between 0.0f and 1.0f from the scrambled Sobol64 generator in state, increment position of generator. Output range excludes 0.0f but includes 1.0f. Denormalized floating point outputs are never returned.
The implementation is guaranteed to use a single call to curand().
| state | - Pointer to state to update |
0.0f and 1.0f | float curand_uniform | ( | curandStateSobol32_t * | state | ) |
Return a uniformly distributed float from a Sobol32 generator.
Return a uniformly distributed float between 0.0f and 1.0f from the Sobol32 generator in state, increment position of generator. Output range excludes 0.0f but includes 1.0f. Denormalized floating point outputs are never returned.
The implementation is guaranteed to use a single call to curand().
| state | - Pointer to state to update |
0.0f and 1.0f | float curand_uniform | ( | curandStateSobol64_t * | state | ) |
Return a uniformly distributed float from a Sobol64 generator.
Return a uniformly distributed float between 0.0f and 1.0f from the Sobol64 generator in state, increment position of generator. Output range excludes 0.0f but includes 1.0f. Denormalized floating point outputs are never returned.
The implementation is guaranteed to use a single call to curand().
| state | - Pointer to state to update |
0.0f and 1.0f | float curand_uniform | ( | curandStateTest_t * | state | ) |
| float curand_uniform | ( | curandStateXORWOW_t * | state | ) |
Return a uniformly distributed float from an XORWOW generator.
Return a uniformly distributed float between 0.0f and 1.0f from the XORWOW generator in state, increment position of generator. Output range excludes 0.0f but includes 1.0f. Denormalized floating point outputs are never returned.
The implementation may use any number of calls to curand() to get enough random bits to create the return value. The current implementation uses one call.
| state | - Pointer to state to update |
0.0f and 1.0f | double curand_uniform_double | ( | curandStateScrambledSobol32_t * | state | ) |
Return a uniformly distributed double from a scrambled Sobol32 generator.
Return a uniformly distributed double between 0.0 and 1.0 from the scrambled Sobol32 generator in state, increment position of generator. Output range excludes 0.0 but includes 1.0. Denormalized floating point outputs are never returned.
The implementation is guaranteed to use a single call to curand() to preserve the quasirandom properties of the sequence.
| state | - Pointer to state to update |
0.0 and 1.0 | double curand_uniform_double | ( | curandStateScrambledSobol64_t * | state | ) |
Return a uniformly distributed double from a scrambled Sobol64 generator.
Return a uniformly distributed double between 0.0 and 1.0 from the scrambled Sobol64 generator in state, increment position of generator. Output range excludes 0.0 but includes 1.0. Denormalized floating point outputs are never returned.
The implementation is guaranteed to use a single call to curand() to preserve the quasirandom properties of the sequence.
| state | - Pointer to state to update |
0.0 and 1.0 | double curand_uniform_double | ( | curandStateSobol32_t * | state | ) |
Return a uniformly distributed double from a Sobol32 generator.
Return a uniformly distributed double between 0.0 and 1.0 from the Sobol32 generator in state, increment position of generator. Output range excludes 0.0 but includes 1.0. Denormalized floating point outputs are never returned.
The implementation is guaranteed to use a single call to curand() to preserve the quasirandom properties of the sequence.
| state | - Pointer to state to update |
0.0 and 1.0 | double curand_uniform_double | ( | curandStateSobol64_t * | state | ) |
Return a uniformly distributed double from a Sobol64 generator.
Return a uniformly distributed double between 0.0 and 1.0 from the Sobol64 generator in state, increment position of generator. Output range excludes 0.0 but includes 1.0. Denormalized floating point outputs are never returned.
The implementation is guaranteed to use a single call to curand() to preserve the quasirandom properties of the sequence.
| state | - Pointer to state to update |
0.0 and 1.0 | double curand_uniform_double | ( | curandStateTest_t * | state | ) |
| double curand_uniform_double | ( | curandStateXORWOW_t * | state | ) |
Return a uniformly distributed double from an XORWOW generator.
Return a uniformly distributed double between 0.0 and 1.0 from the XORWOW generator in state, increment position of generator. Output range excludes 0.0 but includes 1.0. Denormalized floating point outputs are never returned.
The implementation may use any number of calls to curand() to get enough random bits to create the return value. The current implementation uses exactly two calls.
| state | - Pointer to state to update |
0.0 and 1.0 Update Sobol32 state to skip n elements.
Update the Sobol32 state in state to skip ahead n elements.
All values of n are valid.
| n | - Number of elements to skip |
| state | - Pointer to state to update |
| void skipahead | ( | unsigned long long | n, |
| curandStateTest_t * | state ) |
| void skipahead | ( | unsigned long long | n, |
| curandStateXORWOW_t * | state ) |
Update XORWOW state to skip n elements.
Update the XORWOW state in state to skip ahead n elements.
All values of n are valid. Large values require more computation and so will take more time to complete.
| n | - Number of elements to skip |
| state | - Pointer to state to update |
Update Sobol64 state to skip n elements.
Update the Sobol64 state in state to skip ahead n elements.
All values of n are valid.
| n | - Number of elements to skip |
| state | - Pointer to state to update |
| void skipahead_sequence | ( | unsigned long long | n, |
| curandStateXORWOW_t * | state ) |
Update XORWOW state to skip ahead n subsequences.
Update the XORWOW state in state to skip ahead n subsequences. Each subsequence is 

All values of n are valid. Large values require more computation and so will take more time to complete.
| n | - Number of subsequences to skip |
| state | - Pointer to state to update |
|
static |