Skip to content

Commit 39d9395

Browse files
committed
C++: Fix off-by-one in range analysis for 'RemExpr'.
1 parent 81aa115 commit 39d9395

File tree

4 files changed

+9
-9
lines changed

4 files changed

+9
-9
lines changed

cpp/ql/src/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -863,16 +863,16 @@ private float getLowerBoundsImpl(Expr expr) {
863863
result = 0
864864
or
865865
// If either input could be negative then the output could be
866-
// negative. If so, the lower bound of `x%y` is `-abs(y)`, which is
867-
// equal to `min(-y,y)`.
866+
// negative. If so, the lower bound of `x%y` is `-abs(y) + 1`, which is
867+
// equal to `min(-y + 1,y - 1)`.
868868
exists(float childLB |
869869
childLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and
870870
not childLB >= 0
871871
|
872-
result = getFullyConvertedLowerBounds(remExpr.getRightOperand())
872+
result = getFullyConvertedLowerBounds(remExpr.getRightOperand()) - 1
873873
or
874874
exists(float rhsUB | rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand()) |
875-
result = -rhsUB
875+
result = -rhsUB + 1
876876
)
877877
)
878878
)
@@ -1058,7 +1058,7 @@ private float getUpperBoundsImpl(Expr expr) {
10581058
expr = remExpr and
10591059
rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand())
10601060
|
1061-
result = rhsUB
1061+
result = rhsUB - 1
10621062
or
10631063
// If the right hand side could be negative then we need to take its
10641064
// absolute value. Since `abs(x) = max(-x,x)` this is equivalent to
@@ -1067,7 +1067,7 @@ private float getUpperBoundsImpl(Expr expr) {
10671067
rhsLB = getFullyConvertedLowerBounds(remExpr.getRightOperand()) and
10681068
not rhsLB >= 0
10691069
|
1070-
result = -rhsLB
1070+
result = -rhsLB + 1
10711071
)
10721072
)
10731073
or

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -593,7 +593,7 @@
593593
| test.c:658:7:658:7 | u | 0 |
594594
| test.c:659:9:659:9 | u | 0 |
595595
| test.c:664:12:664:12 | s | -2147483648 |
596-
| test.c:665:7:665:8 | s2 | -5 |
596+
| test.c:665:7:665:8 | s2 | -4 |
597597
| test.cpp:10:7:10:7 | b | -2147483648 |
598598
| test.cpp:11:5:11:5 | x | -2147483648 |
599599
| test.cpp:13:10:13:10 | x | -2147483648 |

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -662,5 +662,5 @@ void guard_bound_out_of_range(void) {
662662

663663
void test_mod(int s) {
664664
int s2 = s % 5;
665-
out(s2); // -4 .. 4 [BUG: is -5 .. 5]
665+
out(s2); // -4 .. 4
666666
}

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -593,7 +593,7 @@
593593
| test.c:658:7:658:7 | u | 0 |
594594
| test.c:659:9:659:9 | u | 4294967295 |
595595
| test.c:664:12:664:12 | s | 2147483647 |
596-
| test.c:665:7:665:8 | s2 | 5 |
596+
| test.c:665:7:665:8 | s2 | 4 |
597597
| test.cpp:10:7:10:7 | b | 2147483647 |
598598
| test.cpp:11:5:11:5 | x | 2147483647 |
599599
| test.cpp:13:10:13:10 | x | 2147483647 |

0 commit comments

Comments
 (0)