@@ -7,25 +7,6 @@ private import cpp
77private import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
88private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
99
10- /**
11- * An operand `e` of a division expression (i.e., `e` is an operand of either a `DivExpr` or
12- * a `AssignDivExpr`) is bounded when `e` is the left-hand side of the division.
13- */
14- pragma [ inline]
15- private predicate boundedDiv ( Expr e , Expr left ) { e = left }
16-
17- /**
18- * An operand `e` of a remainder expression `rem` (i.e., `rem` is either a `RemExpr` or
19- * an `AssignRemExpr`) with left-hand side `left` and right-ahnd side `right` is bounded
20- * when `e` is `left` and `right` is upper bounded by some number that is less than the maximum integer
21- * allowed by the result type of `rem`.
22- */
23- pragma [ inline]
24- private predicate boundedRem ( Expr e , Expr rem , Expr left , Expr right ) {
25- e = left and
26- upperBound ( right .getFullyConverted ( ) ) < exprMaxVal ( rem .getFullyConverted ( ) )
27- }
28-
2910/**
3011 * An operand `e` of a bitwise and expression `andExpr` (i.e., `andExpr` is either an `BitwiseAndExpr`
3112 * or an `AssignAndExpr`) with operands `operand1` and `operand2` is the operand that is not `e` is upper
@@ -50,19 +31,10 @@ predicate bounded(Expr e) {
5031 ) and
5132 not convertedExprMightOverflow ( e )
5233 or
53- // For `%` and `&` we require that `e` is bounded by a value that is strictly smaller than the
54- // maximum possible value of the result type of the operation.
55- // For example, the function call `rand()` is considered bounded in the following program:
56- // ```
57- // int i = rand() % (UINT8_MAX + 1);
58- // ```
59- // but not in:
60- // ```
61- // unsigned char uc = rand() % (UINT8_MAX + 1);
62- // ```
63- exists ( RemExpr rem | boundedRem ( e , rem , rem .getLeftOperand ( ) , rem .getRightOperand ( ) ) )
34+ // Optimitically assume that a remainder expression always yields a much smaller value.
35+ e = any ( RemExpr rem ) .getLeftOperand ( )
6436 or
65- exists ( AssignRemExpr rem | boundedRem ( e , rem , rem .getLValue ( ) , rem . getRValue ( ) ) )
37+ e = any ( AssignRemExpr rem ) .getLValue ( )
6638 or
6739 exists ( BitwiseAndExpr andExpr |
6840 boundedBitwiseAnd ( e , andExpr , andExpr .getAnOperand ( ) , andExpr .getAnOperand ( ) )
@@ -73,11 +45,11 @@ predicate bounded(Expr e) {
7345 )
7446 or
7547 // Optimitically assume that a division always yields a much smaller value.
76- boundedDiv ( e , any ( DivExpr div ) .getLeftOperand ( ) )
48+ e = any ( DivExpr div ) .getLeftOperand ( )
7749 or
78- boundedDiv ( e , any ( AssignDivExpr div ) .getLValue ( ) )
50+ e = any ( AssignDivExpr div ) .getLValue ( )
7951 or
80- boundedDiv ( e , any ( RShiftExpr shift ) .getLeftOperand ( ) )
52+ e = any ( RShiftExpr shift ) .getLeftOperand ( )
8153 or
82- boundedDiv ( e , any ( AssignRShiftExpr div ) .getLValue ( ) )
54+ e = any ( AssignRShiftExpr div ) .getLValue ( )
8355}
0 commit comments