Merge branch 'main' into improve-tainted-arithmetic

This commit is contained in:
Mathias Vorreiter Pedersen
2021-06-23 11:42:45 +02:00
2 changed files with 21 additions and 4 deletions

View File

@@ -39,10 +39,17 @@ private predicate boundedBitwiseAnd(Expr e, Expr andExpr, Expr operand1, Expr op
}
/**
* Holds if `e` is an operand of a binary operation that greatly reduces the range of possible
* output values. For instance, if `e` is the left operand of a remainder expression.
* Holds if `e` is an arithmetic expression that cannot overflow, or if `e` is an operand of an
* operation that may greatly reduces the range of possible values.
*/
predicate bounded(Expr e) {
(
e instanceof UnaryArithmeticOperation or
e instanceof BinaryArithmeticOperation or
e instanceof AssignArithmeticOperation
) and
not convertedExprMightOverflow(e)
or
// For `%` and `&` we require that `e` is bounded by a value that is strictly smaller than the
// maximum possible value of the result type of the operation.
// For example, the function call `rand()` is considered bounded in the following program:

View File

@@ -3,12 +3,12 @@
int rand(void);
void trySlice(int start, int end);
void add_100(int);
#define RAND() rand()
#define RANDN(n) (rand() % n)
#define RAND2() (rand() ^ rand())
#define RAND_MAX 32767
@@ -99,4 +99,14 @@ void randomTester() {
*ptr_r = RAND();
r -= 100; // BAD
}
{
int r = rand();
r = ((2.0 / (RAND_MAX + 1)) * r - 1.0);
add_100(r);
}
}
void add_100(int r) {
r += 100; // GOOD
}