Merge pull request #1365 from geoffw0/uninit

CPP: Fix for the 'LoopConditionAlwaysTrueUponEntry' logic
This commit is contained in:
Jonas Jensen
2019-06-19 11:01:57 +02:00
committed by GitHub
8 changed files with 272 additions and 14 deletions

View File

@@ -131,20 +131,28 @@ private predicate bbLoopEntryConditionAlwaysTrueAt(BasicBlock bb, int i, Control
}
/**
* Basic block `pred` ends with a condition belonging to a loop, and that
* condition is provably true upon entry. Basic block `succ` is a successor
* of `pred`, and `skipsLoop` indicates whether `succ` is the false-successor
* of `pred`.
* Basic block `pred` contains all or part of the condition belonging to a loop,
* and there is an edge from `pred` to `succ` that concludes the condition.
* If the edge corrseponds with the loop condition being found to be `true`, then
* `skipsLoop` is `false`. Otherwise the edge corresponds with the loop condition
* being found to be `false` and `skipsLoop` is `true`. Non-concluding edges
* within a complex loop condition are not matched by this predicate.
*/
private predicate bbLoopConditionAlwaysTrueUponEntrySuccessor(BasicBlock pred, BasicBlock succ, boolean skipsLoop) {
succ = pred.getASuccessor() and
exists(ControlFlowNode last |
last = pred.getEnd() and
loopConditionAlwaysTrueUponEntry(_, last) and
if succ = pred.getAFalseSuccessor() then
skipsLoop = true
else
skipsLoop = false
exists(Expr cond |
loopConditionAlwaysTrueUponEntry(_, cond) and
cond.getAChild*() = pred.getEnd() and
succ = pred.getASuccessor() and
not cond.getAChild*() = succ.getStart() and
(
(
succ = pred.getAFalseSuccessor() and
skipsLoop = true
) or (
succ = pred.getATrueSuccessor() and
skipsLoop = false
)
)
)
}
@@ -176,7 +184,7 @@ predicate bbSuccessorEntryReachesLoopInvariant(BasicBlock pred, BasicBlock succ,
// The edge from `pred` to `succ` is _not_ from a loop condition provably
// true upon entry, so the values of `predSkipsFirstLoopAlwaysTrueUponEntry`
// and `succSkipsFirstLoopAlwaysTrueUponEntry` must be the same.
not bbLoopConditionAlwaysTrueUponEntrySuccessor(pred, _, _) and
not bbLoopConditionAlwaysTrueUponEntrySuccessor(pred, succ, _) and
succSkipsFirstLoopAlwaysTrueUponEntry = predSkipsFirstLoopAlwaysTrueUponEntry and
// Moreover, if `pred` contains the entry point of a loop where the
// condition is provably true upon entry, then `succ` is not allowed

View File

@@ -45,6 +45,10 @@ class Stmt extends StmtParent, @stmt {
/**
* Gets the statement following this statement in the same block, if any.
*
* Note that this is not widely useful, because this doesn't have a result for
* the last statement of a block. Consider using the `ControlFlowNode` class
* to trace the flow of control instead.
*/
Stmt getFollowingStmt() {
exists(Block b, int i | this = b.getStmt(i) and

View File

@@ -0,0 +1,24 @@
| test.cpp:35:2:37:2 | for(...;...;...) ... | test.cpp:35:18:35:23 | ... < ... | 1 | i | { ... } | i | ExprStmt |
| test.cpp:43:2:45:2 | for(...;...;...) ... | test.cpp:43:18:43:26 | ... < ... | | i | { ... } | i | ExprStmt |
| test.cpp:74:2:77:2 | while (...) ... | test.cpp:74:9:74:17 | ... > ... | 1 | count | { ... } | count | ExprStmt |
| test.cpp:84:2:88:2 | while (...) ... | test.cpp:84:9:84:17 | ... > ... | | count | { ... } | count | if (...) ... |
| test.cpp:171:3:173:3 | while (...) ... | test.cpp:171:10:171:43 | ... != ... | 0 | | { ... } | 0 | return ... |
| test.cpp:251:2:255:2 | while (...) ... | test.cpp:251:9:251:12 | loop | 1 | loop | { ... } | loop | return ... |
| test.cpp:263:2:267:2 | while (...) ... | test.cpp:263:9:263:20 | ... && ... | 1 | 1 | { ... } | ... && ... | return ... |
| test.cpp:275:2:279:2 | while (...) ... | test.cpp:275:9:275:13 | ! ... | 1 | stop | { ... } | stop | return ... |
| test.cpp:287:2:291:2 | while (...) ... | test.cpp:287:9:287:20 | ... && ... | 1 | loop | { ... } | loop | return ... |
| test.cpp:299:2:303:2 | while (...) ... | test.cpp:299:9:299:20 | ... && ... | 1 | loop | { ... } | ... && ..., loop | return ... |
| test.cpp:311:2:315:2 | while (...) ... | test.cpp:311:9:311:21 | ... \|\| ... | 1 | ... \|\| ... | { ... } | 0 | return ... |
| test.cpp:323:2:328:2 | while (...) ... | test.cpp:323:9:323:17 | ... ? ... : ... | | b, c | { ... } | c | return ... |
| test.cpp:336:2:341:2 | while (...) ... | test.cpp:336:9:336:21 | ... \|\| ... | 1 | b, c | { ... } | c | return ... |
| test.cpp:348:2:351:17 | do (...) ... | test.cpp:351:11:351:15 | 0 | | { ... } | { ... } | { ... } | return ... |
| test.cpp:361:2:364:2 | while (...) ... | test.cpp:361:9:361:21 | ... \|\| ... | 1 | ... \|\| ... | { ... } | 0 | while (...) ... |
| test.cpp:365:2:368:2 | while (...) ... | test.cpp:365:9:365:13 | ! ... | 1 | stop | { ... } | stop | while (...) ... |
| test.cpp:369:2:373:2 | while (...) ... | test.cpp:369:9:369:21 | ... \|\| ... | 1 | b, c | { ... } | c | do (...) ... |
| test.cpp:374:2:376:17 | do (...) ... | test.cpp:376:11:376:15 | 0 | | do (...) ... | { ... } | { ... } | return ... |
| test.cpp:384:2:386:2 | while (...) ... | test.cpp:384:9:384:12 | 1 | 1 | 1 | { ... } | | return ... |
| test.cpp:394:2:396:2 | while (...) ... | test.cpp:394:9:394:21 | ... , ... | | { ... } | { ... } | | |
| test.cpp:404:3:408:3 | while (...) ... | test.cpp:404:10:404:13 | loop | 1 | loop | { ... } | | |
| test.cpp:416:2:418:2 | for(...;...;...) ... | test.cpp:416:18:416:23 | ... < ... | 1 | i | { ... } | i | return ... |
| test.cpp:424:2:425:2 | for(...;...;...) ... | test.cpp:424:18:424:23 | ... < ... | 1 | i | { ... } | i | return ... |
| test.cpp:433:2:434:2 | for(...;...;...) ... | test.cpp:433:18:433:22 | 0 | 0 | | { ... } | 0 | return ... |

View File

@@ -0,0 +1,13 @@
import cpp
import LoopConditionsConst
from Loop l, Expr condition
where
l.getCondition() = condition
select
l, condition,
concat(int val | loopEntryConst(condition, val) | val.toString(), ", "),
concat(BasicBlock bb | bb.getASuccessor() = l.getStmt() | bb.toString(), ", "),
concat(l.getStmt().toString(), ", "),
concat(BasicBlock bb | bb.getASuccessor() = l.getFollowingStmt() | bb.toString(), ", "),
concat(l.getFollowingStmt().toString(), ", ")

View File

@@ -0,0 +1,10 @@
import cpp
import semmle.code.cpp.controlflow.internal.ConstantExprs
predicate loopEntryConst(Expr condition, int val)
{
exists(LoopEntryConditionEvaluator x, ControlFlowNode loop |
x.isLoopEntry(condition, loop) and
val = x.getValue(condition)
)
}

View File

@@ -8,3 +8,9 @@
| test.cpp:132:9:132:9 | j | The variable $@ may not be initialized here. | test.cpp:126:6:126:6 | j | j |
| test.cpp:219:3:219:3 | x | The variable $@ may not be initialized here. | test.cpp:218:7:218:7 | x | x |
| test.cpp:243:13:243:13 | i | The variable $@ may not be initialized here. | test.cpp:241:6:241:6 | i | i |
| test.cpp:329:9:329:11 | val | The variable $@ may not be initialized here. | test.cpp:321:6:321:8 | val | val |
| test.cpp:336:10:336:10 | a | The variable $@ may not be initialized here. | test.cpp:333:7:333:7 | a | a |
| test.cpp:369:10:369:10 | a | The variable $@ may not be initialized here. | test.cpp:358:7:358:7 | a | a |
| test.cpp:378:9:378:11 | val | The variable $@ may not be initialized here. | test.cpp:359:6:359:8 | val | val |
| test.cpp:417:10:417:10 | j | The variable $@ may not be initialized here. | test.cpp:414:9:414:9 | j | j |
| test.cpp:436:9:436:9 | j | The variable $@ may not be initialized here. | test.cpp:431:9:431:9 | j | j |

View File

@@ -242,4 +242,196 @@ void test21()
v3 = v1 >> i; // BAD: i is not initialized
v3 = v2 >> 1; // BAD: v2 is not initialized [NOT DETECTED]
}
}
int test22() {
bool loop = true;
int val;
while (loop)
{
val = 1;
loop = false;
}
return val; // GOOD
}
int test23() {
bool loop = true, stop = false;
int val;
while (loop && true)
{
val = 1;
loop = false;
}
return val; // GOOD
}
int test24() {
bool stop = false;
int val;
while (!stop)
{
val = 1;
stop = true;
}
return val; // GOOD
}
int test25() {
bool loop = true, stop = false;
int val;
while (true && loop)
{
val = 1;
loop = false;
}
return val; // GOOD
}
int test26() {
bool loop = true, stop = false;
int val;
while (loop && loop)
{
val = 1;
loop = false;
}
return val; // GOOD
}
int test27() {
bool loop = true, stop = false;
int val;
while (loop || false)
{
val = 1;
loop = false;
}
return val; // GOOD
}
int test28() {
bool a = true, b = true, c = true;
int val;
while (a ? b : c)
{
val = 1;
a = false;
c = false;
}
return val; // GOOD [FALSE POSITIVE]
}
int test29() {
bool a, b = true, c = true;
int val;
while ((a && b) || c) // BAD (a is uninitialized)
{
val = 1;
b = false;
c = false;
}
return val; // GOOD
}
int test30() {
int val;
do
{
val = 1;
} while (false);
return val; // GOOD
}
int test31() {
bool loop = true;
bool stop = false;
bool a, b = true, c = true;
int val;
while (loop || false)
{
loop = false;
}
while (!stop)
{
stop = true;
}
while ((a && b) || c) // BAD (a is uninitialized)
{
b = false;
c = false;
}
do
{
} while (false);
return val; // BAD
}
int test32() {
int val;
while (true)
{
}
return val; // GOOD (never reached)
}
int test33() {
int val;
while (val = 1, true) {
return val; // GOOD
}
}
int test34() {
bool loop = true;
int val;
{
while (loop)
{
val = 1;
loop = false;
}
}
return val; // GOOD
}
int test35() {
int i, j;
for (int i = 0; i < 10; i++, j = 1) {
return j; // BAD
}
}
int test36() {
int i, j;
for (int i = 0; i < 10; i++, j = 1) {
}
return j; // GOOD
}
int test38() {
int i, j;
for (int i = 0; false; i++, j = 1) {
}
return j; // BAD
}