C++: Relax the restrictions on when '%' is a barrier and accept test changes.

This commit is contained in:
Mathias Vorreiter Pedersen
2021-06-25 15:15:26 +02:00
parent a6f1f8d3b6
commit 4fc60aedc6
3 changed files with 8 additions and 31 deletions

View File

@@ -15,16 +15,11 @@ pragma[inline]
private predicate boundedDiv(Expr e, Expr left) { e = left }
/**
* An operand `e` of a remainder expression `rem` (i.e., `rem` is either a `RemExpr` or
* an `AssignRemExpr`) with left-hand side `left` and right-ahnd side `right` is bounded
* when `e` is `left` and `right` is upper bounded by some number that is less than the maximum integer
* allowed by the result type of `rem`.
* An operand `e` of a remainder expression (i.e., `e` is an operand of either a `RemExpr` or
* a `AssignRemExpr`) is bounded when `e` is the left-hand side of the remainder.
*/
pragma[inline]
private predicate boundedRem(Expr e, Expr rem, Expr left, Expr right) {
e = left and
upperBound(right.getFullyConverted()) < exprMaxVal(rem.getFullyConverted())
}
private predicate boundedRem(Expr e, Expr left) { e = left }
/**
* An operand `e` of a bitwise and expression `andExpr` (i.e., `andExpr` is either an `BitwiseAndExpr`
@@ -50,19 +45,9 @@ predicate bounded(Expr e) {
) 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:
// ```
// int i = rand() % (UINT8_MAX + 1);
// ```
// but not in:
// ```
// unsigned char uc = rand() % (UINT8_MAX + 1);
// ```
exists(RemExpr rem | boundedRem(e, rem, rem.getLeftOperand(), rem.getRightOperand()))
boundedRem(e, any(RemExpr rem).getLeftOperand())
or
exists(AssignRemExpr rem | boundedRem(e, rem, rem.getLValue(), rem.getRValue()))
boundedRem(e, any(AssignRemExpr rem).getLValue())
or
exists(BitwiseAndExpr andExpr |
boundedBitwiseAnd(e, andExpr, andExpr.getAnOperand(), andExpr.getAnOperand())