Merge pull request #6581 from geoffw0/uncontrolledarith2

CPP: Improvements for cpp/uncontrolled-arithmetic
This commit is contained in:
Mathias Vorreiter Pedersen
2021-09-07 09:48:59 +01:00
committed by GitHub
4 changed files with 164 additions and 31 deletions

View File

@@ -41,7 +41,8 @@ private predicate stmtDominates(Stmt dominator, Stmt dominated) {
}
/**
* Holds if the value of `use` is guarded to be less than something.
* Holds if the value of `use` is guarded to be less than something, and `e`
* is in code controlled by that guard (where the guard condition held).
*/
pragma[nomagic]
predicate guardedLesser(Operation e, Expr use) {
@@ -67,7 +68,8 @@ predicate guardedLesser(Operation e, Expr use) {
}
/**
* Holds if the value of `use` is guarded to be greater than something.
* Holds if the value of `use` is guarded to be greater than something, and `e`
* is in code controlled by that guard (where the guard condition held).
*/
pragma[nomagic]
predicate guardedGreater(Operation e, Expr use) {
@@ -120,6 +122,10 @@ predicate missingGuardAgainstOverflow(Operation e, VariableAccess use) {
// overflow possible if large or small
e instanceof MulExpr and
not (guardedLesser(e, varUse(v)) and guardedGreater(e, varUse(v)))
or
// overflow possible if large or small
e instanceof AssignMulExpr and
not (guardedLesser(e, varUse(v)) and guardedGreater(e, varUse(v)))
)
}
@@ -147,5 +153,9 @@ predicate missingGuardAgainstUnderflow(Operation e, VariableAccess use) {
// underflow possible if large or small
e instanceof MulExpr and
not (guardedLesser(e, varUse(v)) and guardedGreater(e, varUse(v)))
or
// underflow possible if large or small
e instanceof AssignMulExpr and
not (guardedLesser(e, varUse(v)) and guardedGreater(e, varUse(v)))
)
}

View File

@@ -8,8 +8,10 @@ edges
| test.c:81:23:81:26 | call to rand | test.c:83:9:83:9 | r |
| test.c:99:14:99:19 | call to rand | test.c:100:5:100:5 | r |
| test.c:125:13:125:16 | call to rand | test.c:127:9:127:9 | r |
| test.c:148:22:148:25 | call to rand | test.c:150:9:150:9 | r |
| test.c:148:22:148:27 | (unsigned int)... | test.c:150:9:150:9 | r |
| test.c:131:13:131:16 | call to rand | test.c:133:5:133:5 | r |
| test.c:137:13:137:16 | call to rand | test.c:139:10:139:10 | r |
| test.c:155:22:155:25 | call to rand | test.c:157:9:157:9 | r |
| test.c:155:22:155:27 | (unsigned int)... | test.c:157:9:157:9 | r |
| test.cpp:8:9:8:12 | Store | test.cpp:24:11:24:18 | call to get_rand |
| test.cpp:8:9:8:12 | call to rand | test.cpp:8:9:8:12 | Store |
| test.cpp:13:2:13:15 | Chi [[]] | test.cpp:30:13:30:14 | get_rand2 output argument [[]] |
@@ -21,11 +23,23 @@ edges
| test.cpp:30:13:30:14 | get_rand2 output argument [[]] | test.cpp:30:13:30:14 | Chi |
| test.cpp:36:13:36:13 | Chi | test.cpp:37:7:37:7 | r |
| test.cpp:36:13:36:13 | get_rand3 output argument [[]] | test.cpp:36:13:36:13 | Chi |
| test.cpp:78:10:78:13 | call to rand | test.cpp:82:10:82:10 | x |
| test.cpp:90:10:90:13 | call to rand | test.cpp:94:10:94:10 | x |
| test.cpp:129:10:129:13 | call to rand | test.cpp:132:10:132:10 | b |
| test.cpp:147:11:147:14 | call to rand | test.cpp:149:11:149:16 | (int)... |
| test.cpp:147:11:147:14 | call to rand | test.cpp:149:16:149:16 | y |
| test.cpp:62:19:62:22 | call to rand | test.cpp:65:9:65:9 | x |
| test.cpp:62:19:62:24 | (unsigned int)... | test.cpp:65:9:65:9 | x |
| test.cpp:86:10:86:13 | call to rand | test.cpp:90:10:90:10 | x |
| test.cpp:98:10:98:13 | call to rand | test.cpp:102:10:102:10 | x |
| test.cpp:137:10:137:13 | call to rand | test.cpp:146:9:146:9 | y |
| test.cpp:151:10:151:13 | call to rand | test.cpp:154:10:154:10 | b |
| test.cpp:169:11:169:14 | call to rand | test.cpp:171:11:171:16 | (int)... |
| test.cpp:169:11:169:14 | call to rand | test.cpp:171:16:171:16 | y |
| test.cpp:189:10:189:13 | call to rand | test.cpp:196:7:196:7 | x |
| test.cpp:189:10:189:13 | call to rand | test.cpp:198:7:198:7 | x |
| test.cpp:189:10:189:13 | call to rand | test.cpp:199:7:199:7 | x |
| test.cpp:190:10:190:13 | call to rand | test.cpp:204:7:204:7 | y |
| test.cpp:190:10:190:13 | call to rand | test.cpp:205:7:205:7 | y |
| test.cpp:190:10:190:13 | call to rand | test.cpp:208:7:208:7 | y |
| test.cpp:215:11:215:14 | call to rand | test.cpp:219:8:219:8 | x |
| test.cpp:223:20:223:23 | call to rand | test.cpp:227:8:227:8 | x |
| test.cpp:223:20:223:25 | (unsigned int)... | test.cpp:227:8:227:8 | x |
nodes
| test.c:18:13:18:16 | call to rand | semmle.label | call to rand |
| test.c:21:17:21:17 | r | semmle.label | r |
@@ -43,9 +57,13 @@ nodes
| test.c:100:5:100:5 | r | semmle.label | r |
| test.c:125:13:125:16 | call to rand | semmle.label | call to rand |
| test.c:127:9:127:9 | r | semmle.label | r |
| test.c:148:22:148:25 | call to rand | semmle.label | call to rand |
| test.c:148:22:148:27 | (unsigned int)... | semmle.label | (unsigned int)... |
| test.c:150:9:150:9 | r | semmle.label | r |
| test.c:131:13:131:16 | call to rand | semmle.label | call to rand |
| test.c:133:5:133:5 | r | semmle.label | r |
| test.c:137:13:137:16 | call to rand | semmle.label | call to rand |
| test.c:139:10:139:10 | r | semmle.label | r |
| test.c:155:22:155:25 | call to rand | semmle.label | call to rand |
| test.c:155:22:155:27 | (unsigned int)... | semmle.label | (unsigned int)... |
| test.c:157:9:157:9 | r | semmle.label | r |
| test.cpp:8:9:8:12 | Store | semmle.label | Store |
| test.cpp:8:9:8:12 | call to rand | semmle.label | call to rand |
| test.cpp:13:2:13:15 | Chi [[]] | semmle.label | Chi [[]] |
@@ -60,15 +78,33 @@ nodes
| test.cpp:36:13:36:13 | Chi | semmle.label | Chi |
| test.cpp:36:13:36:13 | get_rand3 output argument [[]] | semmle.label | get_rand3 output argument [[]] |
| test.cpp:37:7:37:7 | r | semmle.label | r |
| test.cpp:78:10:78:13 | call to rand | semmle.label | call to rand |
| test.cpp:82:10:82:10 | x | semmle.label | x |
| test.cpp:90:10:90:13 | call to rand | semmle.label | call to rand |
| test.cpp:94:10:94:10 | x | semmle.label | x |
| test.cpp:129:10:129:13 | call to rand | semmle.label | call to rand |
| test.cpp:132:10:132:10 | b | semmle.label | b |
| test.cpp:147:11:147:14 | call to rand | semmle.label | call to rand |
| test.cpp:149:11:149:16 | (int)... | semmle.label | (int)... |
| test.cpp:149:16:149:16 | y | semmle.label | y |
| test.cpp:62:19:62:22 | call to rand | semmle.label | call to rand |
| test.cpp:62:19:62:24 | (unsigned int)... | semmle.label | (unsigned int)... |
| test.cpp:65:9:65:9 | x | semmle.label | x |
| test.cpp:86:10:86:13 | call to rand | semmle.label | call to rand |
| test.cpp:90:10:90:10 | x | semmle.label | x |
| test.cpp:98:10:98:13 | call to rand | semmle.label | call to rand |
| test.cpp:102:10:102:10 | x | semmle.label | x |
| test.cpp:137:10:137:13 | call to rand | semmle.label | call to rand |
| test.cpp:146:9:146:9 | y | semmle.label | y |
| test.cpp:151:10:151:13 | call to rand | semmle.label | call to rand |
| test.cpp:154:10:154:10 | b | semmle.label | b |
| test.cpp:169:11:169:14 | call to rand | semmle.label | call to rand |
| test.cpp:171:11:171:16 | (int)... | semmle.label | (int)... |
| test.cpp:171:16:171:16 | y | semmle.label | y |
| test.cpp:189:10:189:13 | call to rand | semmle.label | call to rand |
| test.cpp:190:10:190:13 | call to rand | semmle.label | call to rand |
| test.cpp:196:7:196:7 | x | semmle.label | x |
| test.cpp:198:7:198:7 | x | semmle.label | x |
| test.cpp:199:7:199:7 | x | semmle.label | x |
| test.cpp:204:7:204:7 | y | semmle.label | y |
| test.cpp:205:7:205:7 | y | semmle.label | y |
| test.cpp:208:7:208:7 | y | semmle.label | y |
| test.cpp:215:11:215:14 | call to rand | semmle.label | call to rand |
| test.cpp:219:8:219:8 | x | semmle.label | x |
| test.cpp:223:20:223:23 | call to rand | semmle.label | call to rand |
| test.cpp:223:20:223:25 | (unsigned int)... | semmle.label | (unsigned int)... |
| test.cpp:227:8:227:8 | x | semmle.label | x |
#select
| test.c:21:17:21:17 | r | test.c:18:13:18:16 | call to rand | test.c:21:17:21:17 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:18:13:18:16 | call to rand | Uncontrolled value |
| test.c:35:5:35:5 | r | test.c:34:13:34:18 | call to rand | test.c:35:5:35:5 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:34:13:34:18 | call to rand | Uncontrolled value |
@@ -79,13 +115,27 @@ nodes
| test.c:83:9:83:9 | r | test.c:81:23:81:26 | call to rand | test.c:83:9:83:9 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:81:23:81:26 | call to rand | Uncontrolled value |
| test.c:100:5:100:5 | r | test.c:99:14:99:19 | call to rand | test.c:100:5:100:5 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:99:14:99:19 | call to rand | Uncontrolled value |
| test.c:127:9:127:9 | r | test.c:125:13:125:16 | call to rand | test.c:127:9:127:9 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:125:13:125:16 | call to rand | Uncontrolled value |
| test.c:150:9:150:9 | r | test.c:148:22:148:25 | call to rand | test.c:150:9:150:9 | r | $@ flows to here and is used in arithmetic, potentially causing an underflow. | test.c:148:22:148:25 | call to rand | Uncontrolled value |
| test.c:150:9:150:9 | r | test.c:148:22:148:27 | (unsigned int)... | test.c:150:9:150:9 | r | $@ flows to here and is used in arithmetic, potentially causing an underflow. | test.c:148:22:148:25 | call to rand | Uncontrolled value |
| test.c:133:5:133:5 | r | test.c:131:13:131:16 | call to rand | test.c:133:5:133:5 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:131:13:131:16 | call to rand | Uncontrolled value |
| test.c:139:10:139:10 | r | test.c:137:13:137:16 | call to rand | test.c:139:10:139:10 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:137:13:137:16 | call to rand | Uncontrolled value |
| test.c:157:9:157:9 | r | test.c:155:22:155:25 | call to rand | test.c:157:9:157:9 | r | $@ flows to here and is used in arithmetic, potentially causing an underflow. | test.c:155:22:155:25 | call to rand | Uncontrolled value |
| test.c:157:9:157:9 | r | test.c:155:22:155:27 | (unsigned int)... | test.c:157:9:157:9 | r | $@ flows to here and is used in arithmetic, potentially causing an underflow. | test.c:155:22:155:25 | call to rand | Uncontrolled value |
| test.cpp:25:7:25:7 | r | test.cpp:8:9:8:12 | call to rand | test.cpp:25:7:25:7 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:8:9:8:12 | call to rand | Uncontrolled value |
| test.cpp:31:7:31:7 | r | test.cpp:13:10:13:13 | call to rand | test.cpp:31:7:31:7 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:13:10:13:13 | call to rand | Uncontrolled value |
| test.cpp:37:7:37:7 | r | test.cpp:18:9:18:12 | call to rand | test.cpp:37:7:37:7 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:18:9:18:12 | call to rand | Uncontrolled value |
| test.cpp:82:10:82:10 | x | test.cpp:78:10:78:13 | call to rand | test.cpp:82:10:82:10 | x | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:78:10:78:13 | call to rand | Uncontrolled value |
| test.cpp:94:10:94:10 | x | test.cpp:90:10:90:13 | call to rand | test.cpp:94:10:94:10 | x | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:90:10:90:13 | call to rand | Uncontrolled value |
| test.cpp:132:10:132:10 | b | test.cpp:129:10:129:13 | call to rand | test.cpp:132:10:132:10 | b | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:129:10:129:13 | call to rand | Uncontrolled value |
| test.cpp:149:11:149:16 | (int)... | test.cpp:147:11:147:14 | call to rand | test.cpp:149:11:149:16 | (int)... | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:147:11:147:14 | call to rand | Uncontrolled value |
| test.cpp:149:16:149:16 | y | test.cpp:147:11:147:14 | call to rand | test.cpp:149:16:149:16 | y | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:147:11:147:14 | call to rand | Uncontrolled value |
| test.cpp:65:9:65:9 | x | test.cpp:62:19:62:22 | call to rand | test.cpp:65:9:65:9 | x | $@ flows to here and is used in arithmetic, potentially causing an underflow. | test.cpp:62:19:62:22 | call to rand | Uncontrolled value |
| test.cpp:65:9:65:9 | x | test.cpp:62:19:62:24 | (unsigned int)... | test.cpp:65:9:65:9 | x | $@ flows to here and is used in arithmetic, potentially causing an underflow. | test.cpp:62:19:62:22 | call to rand | Uncontrolled value |
| test.cpp:90:10:90:10 | x | test.cpp:86:10:86:13 | call to rand | test.cpp:90:10:90:10 | x | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:86:10:86:13 | call to rand | Uncontrolled value |
| test.cpp:102:10:102:10 | x | test.cpp:98:10:98:13 | call to rand | test.cpp:102:10:102:10 | x | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:98:10:98:13 | call to rand | Uncontrolled value |
| test.cpp:146:9:146:9 | y | test.cpp:137:10:137:13 | call to rand | test.cpp:146:9:146:9 | y | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:137:10:137:13 | call to rand | Uncontrolled value |
| test.cpp:154:10:154:10 | b | test.cpp:151:10:151:13 | call to rand | test.cpp:154:10:154:10 | b | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:151:10:151:13 | call to rand | Uncontrolled value |
| test.cpp:171:11:171:16 | (int)... | test.cpp:169:11:169:14 | call to rand | test.cpp:171:11:171:16 | (int)... | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:169:11:169:14 | call to rand | Uncontrolled value |
| test.cpp:171:16:171:16 | y | test.cpp:169:11:169:14 | call to rand | test.cpp:171:16:171:16 | y | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:169:11:169:14 | call to rand | Uncontrolled value |
| test.cpp:196:7:196:7 | x | test.cpp:189:10:189:13 | call to rand | test.cpp:196:7:196:7 | x | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:189:10:189:13 | call to rand | Uncontrolled value |
| test.cpp:198:7:198:7 | x | test.cpp:189:10:189:13 | call to rand | test.cpp:198:7:198:7 | x | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:189:10:189:13 | call to rand | Uncontrolled value |
| test.cpp:199:7:199:7 | x | test.cpp:189:10:189:13 | call to rand | test.cpp:199:7:199:7 | x | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:189:10:189:13 | call to rand | Uncontrolled value |
| test.cpp:204:7:204:7 | y | test.cpp:190:10:190:13 | call to rand | test.cpp:204:7:204:7 | y | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:190:10:190:13 | call to rand | Uncontrolled value |
| test.cpp:205:7:205:7 | y | test.cpp:190:10:190:13 | call to rand | test.cpp:205:7:205:7 | y | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:190:10:190:13 | call to rand | Uncontrolled value |
| test.cpp:208:7:208:7 | y | test.cpp:190:10:190:13 | call to rand | test.cpp:208:7:208:7 | y | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:190:10:190:13 | call to rand | Uncontrolled value |
| test.cpp:219:8:219:8 | x | test.cpp:215:11:215:14 | call to rand | test.cpp:219:8:219:8 | x | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:215:11:215:14 | call to rand | Uncontrolled value |
| test.cpp:227:8:227:8 | x | test.cpp:223:20:223:23 | call to rand | test.cpp:227:8:227:8 | x | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:223:20:223:23 | call to rand | Uncontrolled value |
| test.cpp:227:8:227:8 | x | test.cpp:223:20:223:25 | (unsigned int)... | test.cpp:227:8:227:8 | x | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:223:20:223:23 | call to rand | Uncontrolled value |

View File

@@ -126,10 +126,17 @@ void moreTests() {
r = r * 100; // BAD
}
{
int r = rand();
r *= 100; // BAD [NOT DETECTED]
r *= 100; // BAD
}
{
int r = rand();
int v = 100;
v *= r; // BAD
}
{

View File

@@ -42,8 +42,8 @@ int rand(int min, int max);
unsigned rand(int max);
void test_with_bounded_randomness() {
int r = rand(0, 10);
r++; // GOOD
int r = rand(0, 10);
r++; // GOOD
unsigned unsigned_r = rand(10);
unsigned_r++; // GOOD
@@ -57,6 +57,14 @@ int test_remainder_subtract()
return x - y; // GOOD (as y <= x)
}
unsigned int test_remainder_subtract_unsigned()
{
unsigned int x = rand();
unsigned int y = x % 100; // y <= x
return x - y; // GOOD (as y <= x) [FALSE POSITIVE]
}
typedef unsigned long size_t;
int snprintf(char *s, size_t n, const char *format, ...);
@@ -124,6 +132,20 @@ int test_conditional_assignment_2()
return y * 10; // GOOD (as y <= 100)
}
int test_conditional_assignment_3()
{
int x = rand();
int y = 100;
int c = 10;
if (x < y)
{
y = x;
}
return y * c; // GOOD (as y <= 100) [FALSE POSITIVE]
}
int test_underflow()
{
int x = rand();
@@ -161,3 +183,47 @@ void test_float()
int z = (int)y * 5; // GOOD
}
}
void test_if_const_bounded()
{
int x = rand();
int y = rand();
int c = 10;
if (x < 1000)
{
x = x * 2; // GOOD
x = x * c; // GOOD [FALSE POSITIVE]
} else {
x = x * 2; // BAD
x = x * c; // BAD
}
if (y > 1000)
{
y = y * 2; // BAD
y = y * c; // BAD
} else {
y = y * 2; // GOOD
y = y * c; // GOOD [FALSE POSITIVE]
}
}
void test_mod_limit()
{
{
int x = rand();
int y = 100;
int z;
z = (x + y) % 1000; // BAD
}
{
unsigned int x = rand();
unsigned int y = 100;
unsigned int z;
z = (x + y) % 1000; // DUBIOUS (this could overflow but the result is controlled) [REPORTED]
}
}