switch to wrapping ranges
This commit is contained in:
parent
0f773895d1
commit
827e4cbe82
@ -232,23 +232,8 @@ DEEPSTATE_INLINE static void DeepState_Check(int expr) {
|
||||
}
|
||||
}
|
||||
|
||||
/* Return a symbolic value in a the range `[low_inc, high_inc]`.
|
||||
*
|
||||
* Current implementation saturates values. An alternative implementation
|
||||
* worth exploring, and perhaps supporting in addition to saturation, is
|
||||
* something like:
|
||||
*
|
||||
* x = symbolic_value;
|
||||
* size = (high - low) + 1
|
||||
* if (symbolic mode) {
|
||||
* assume 0 <= x and x < size
|
||||
* return low + x
|
||||
* } else {
|
||||
* return low + (x % size)
|
||||
* }
|
||||
*
|
||||
* This type of version lets a reducer drive toward zero.
|
||||
*/
|
||||
/* Return a symbolic value in a the range `[low_inc, high_inc]`. */
|
||||
/* Saturating version here is an alternative, but worse for fuzzing:
|
||||
#define DEEPSTATE_MAKE_SYMBOLIC_RANGE(Tname, tname) \
|
||||
DEEPSTATE_INLINE static tname DeepState_ ## Tname ## InRange( \
|
||||
tname low, tname high) { \
|
||||
@ -268,6 +253,22 @@ DEEPSTATE_INLINE static void DeepState_Check(int expr) {
|
||||
return x; \
|
||||
} \
|
||||
}
|
||||
*/
|
||||
#define DEEPSTATE_MAKE_SYMBOLIC_RANGE(Tname, tname) \
|
||||
DEEPSTATE_INLINE static tname DeepState_ ## Tname ## InRange( \
|
||||
tname low, tname high) { \
|
||||
if (low > high) { \
|
||||
return DeepState_ ## Tname ## InRange(high, low); \
|
||||
} \
|
||||
const tname x = DeepState_ ## Tname(); \
|
||||
const tname size = (high - low) + 1; \
|
||||
if (DeepState_UsingSymExec) { \
|
||||
(void) DeepState_Assume(0 <= x && x < size); \
|
||||
return low + x; \
|
||||
} else { \
|
||||
return low + (x % size); \
|
||||
} \
|
||||
}
|
||||
|
||||
DEEPSTATE_MAKE_SYMBOLIC_RANGE(Size, size_t)
|
||||
DEEPSTATE_MAKE_SYMBOLIC_RANGE(Int64, int64_t)
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user