@@ -7,25 +7,6 @@ private import cpp
7
7
private import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
8
8
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
9
9
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
-
29
10
/**
30
11
* An operand `e` of a bitwise and expression `andExpr` (i.e., `andExpr` is either an `BitwiseAndExpr`
31
12
* 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) {
50
31
) and
51
32
not convertedExprMightOverflow ( e )
52
33
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 ( )
64
36
or
65
- exists ( AssignRemExpr rem | boundedRem ( e , rem , rem .getLValue ( ) , rem . getRValue ( ) ) )
37
+ e = any ( AssignRemExpr rem ) .getLValue ( )
66
38
or
67
39
exists ( BitwiseAndExpr andExpr |
68
40
boundedBitwiseAnd ( e , andExpr , andExpr .getAnOperand ( ) , andExpr .getAnOperand ( ) )
@@ -73,11 +45,11 @@ predicate bounded(Expr e) {
73
45
)
74
46
or
75
47
// Optimitically assume that a division always yields a much smaller value.
76
- boundedDiv ( e , any ( DivExpr div ) .getLeftOperand ( ) )
48
+ e = any ( DivExpr div ) .getLeftOperand ( )
77
49
or
78
- boundedDiv ( e , any ( AssignDivExpr div ) .getLValue ( ) )
50
+ e = any ( AssignDivExpr div ) .getLValue ( )
79
51
or
80
- boundedDiv ( e , any ( RShiftExpr shift ) .getLeftOperand ( ) )
52
+ e = any ( RShiftExpr shift ) .getLeftOperand ( )
81
53
or
82
- boundedDiv ( e , any ( AssignRShiftExpr div ) .getLValue ( ) )
54
+ e = any ( AssignRShiftExpr div ) .getLValue ( )
83
55
}
0 commit comments