C++: Rewrite the range analysis exclusion to be recursive and more robust.

This commit is contained in:
Geoffrey White
2021-04-06 15:57:58 +01:00
parent 3ecd13531f
commit 48ff8e237c
3 changed files with 22 additions and 19 deletions

View File

@@ -29,16 +29,22 @@ predicate isGuarded(SubExpr sub, Expr left, Expr right) {
)
}
/** Holds if `sub` will never be negative. */
predicate nonNegative(SubExpr sub) {
not exprMightOverflowNegatively(sub.getFullyConverted())
/**
* Holds if `e` is known to be less than or equal to `sub.getLeftOperand()`.
*/
predicate exprIsSubLeftOrLess(SubExpr sub, Expr e) {
e = sub.getLeftOperand()
or
// The subtraction is guarded by a check of the form `left >= right`.
exists(GVN left, GVN right |
// This is basically a poor man's version of a directional unbind operator.
strictcount([left, globalValueNumber(sub.getLeftOperand())]) = 1 and
strictcount([right, globalValueNumber(sub.getRightOperand())]) = 1 and
isGuarded(sub, left.getAnExpr(), right.getAnExpr())
exists(Expr other |
// GVN equality
exprIsSubLeftOrLess(sub, other) and
globalValueNumber(e) = globalValueNumber(other)
)
or
exists(Expr other |
// guard constraining `sub`
exprIsSubLeftOrLess(sub, other) and
isGuarded(sub, other, e) // left >= right
)
}
@@ -49,5 +55,5 @@ where
ro.getLesserOperand().getValue().toInt() = 0 and
ro.getGreaterOperand() = sub and
sub.getFullyConverted().getUnspecifiedType().(IntegralType).isUnsigned() and
not nonNegative(sub)
not exprIsSubLeftOrLess(sub, sub.getRightOperand())
select ro, "Unsigned subtraction can never be negative."

View File

@@ -8,10 +8,8 @@
| test.cpp:62:5:62:13 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:69:5:69:13 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:75:8:75:16 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:83:6:83:14 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:92:6:92:14 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:101:6:101:14 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:110:6:110:14 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:119:6:119:14 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:128:6:128:14 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:137:6:137:14 | ... > ... | Unsigned subtraction can never be negative. |
@@ -20,7 +18,6 @@
| test.cpp:182:6:182:14 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:195:6:195:14 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:208:6:208:14 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:219:7:219:15 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:226:8:226:16 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:241:10:241:18 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:252:10:252:18 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:266:10:266:24 | ... > ... | Unsigned subtraction can never be negative. |

View File

@@ -80,7 +80,7 @@ void test2() {
unsigned int a = getAnInt();
unsigned int b = a;
if (a - b > 0) { // GOOD (as a = b) [FALSE POSITIVE]
if (a - b > 0) { // GOOD (as a = b)
// ...
}
}
@@ -107,7 +107,7 @@ void test5() {
unsigned int b = getAnInt();
unsigned int a = b;
if (a - b > 0) { // GOOD (as a = b) [FALSE POSITIVE]
if (a - b > 0) { // GOOD (as a = b)
// ...
}
}
@@ -216,14 +216,14 @@ void test12() {
unsigned int c;
if ((b <= c) && (c <= a)) {
if (a - b > 0) { // GOOD (as b <= a) [FALSE POSITIVE]
if (a - b > 0) { // GOOD (as b <= a)
// ...
}
}
if (b <= c) {
if (c <= a) {
if (a - b > 0) { // GOOD (as b <= a) [FALSE POSITIVE]
if (a - b > 0) { // GOOD (as b <= a)
// ...
}
}
@@ -238,7 +238,7 @@ int test13() {
return 0;
}
return (a - b > 0); // GOOD (as b = 0)
return (a - b > 0); // GOOD (as b = 0) [FALSE POSITIVE]
}
int test14() {