C++: Add linear expression logic.

This commit is contained in:
Geoffrey White
2021-04-06 18:30:18 +01:00
parent 48ff8e237c
commit 60e4faba4c
3 changed files with 19 additions and 4 deletions

View File

@@ -14,6 +14,7 @@ import cpp
import semmle.code.cpp.commons.Exclusions
import semmle.code.cpp.valuenumbering.GlobalValueNumbering
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
import semmle.code.cpp.controlflow.Guards
/**
@@ -46,6 +47,22 @@ predicate exprIsSubLeftOrLess(SubExpr sub, Expr e) {
exprIsSubLeftOrLess(sub, other) and
isGuarded(sub, other, e) // left >= right
)
or
exists(Expr other, float p, float q |
// linear access of `other`
exprIsSubLeftOrLess(sub, other) and
linearAccess(e, other, p, q) and // e = p * other + q
p <= 1 and
q <= 0
)
or
exists(Expr other, float p, float q |
// linear access of `e`
exprIsSubLeftOrLess(sub, other) and
linearAccess(other, e, p, q) and // other = p * e + q
p >= 1 and
q >= 0
)
}
from RelationalOperation ro, SubExpr sub

View File

@@ -8,9 +8,7 @@
| 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:92:6:92:14 | ... > ... | Unsigned subtraction can never be negative. |
| test.cpp:101:6:101: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. |
| test.cpp:146:7:146:15 | ... > ... | Unsigned subtraction can never be negative. |

View File

@@ -89,7 +89,7 @@ void test3() {
unsigned int a = getAnInt();
unsigned int b = a - 1;
if (a - b > 0) { // GOOD (as a >= b) [FALSE POSITIVE]
if (a - b > 0) { // GOOD (as a >= b)
// ...
}
}
@@ -116,7 +116,7 @@ void test6() {
unsigned int b = getAnInt();
unsigned int a = b + 1;
if (a - b > 0) { // GOOD (as a >= b) [FALSE POSITIVE]
if (a - b > 0) { // GOOD (as a >= b)
// ...
}
}