Skip to content

Commit 1bbadb5

Browse files
Merge pull request github#6568 from andersfugmann/andersfugmann/improve_upper_bound
C++: Improve predicate upperBound in SimpleRangeAnalysis
2 parents 3e17fdc + 270dbd2 commit 1bbadb5

File tree

11 files changed

+127
-41
lines changed

11 files changed

+127
-41
lines changed
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
lgtm,codescanning
2+
* The `SimpleRangeAnalysis` library includes information from the
3+
immediate guard for determining the upper bound of a stack
4+
variable for improved accuracy.

cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeSSA.qll

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -95,10 +95,19 @@ class RangeSsaDefinition extends ControlFlowNodeBase {
9595

9696
/**
9797
* If this definition is a phi node corresponding to a guard,
98-
* then return the variable and the guard.
98+
* then return the variable access and the guard.
9999
*/
100-
predicate isGuardPhi(VariableAccess v, Expr guard, boolean branch) {
101-
guard_defn(v, guard, this, branch)
100+
predicate isGuardPhi(VariableAccess va, Expr guard, boolean branch) {
101+
guard_defn(va, guard, this, branch)
102+
}
103+
104+
/**
105+
* If this definition is a phi node corresponding to a guard,
106+
* then return the variable guarded, the variable access and the guard.
107+
*/
108+
predicate isGuardPhi(StackVariable v, VariableAccess va, Expr guard, boolean branch) {
109+
guard_defn(va, guard, this, branch) and
110+
va.getTarget() = v
102111
}
103112

104113
/** Gets the primary location of this definition. */

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

Lines changed: 26 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1530,6 +1530,29 @@ private predicate isUnsupportedGuardPhi(Variable v, RangeSsaDefinition phi, Vari
15301530
)
15311531
}
15321532

1533+
/**
1534+
* Gets the upper bound of the expression, if the expression is guarded.
1535+
* An upper bound can only be found, if a guard phi node can be found, and the
1536+
* expression has only one immediate predecessor.
1537+
*/
1538+
private float getGuardedUpperBound(VariableAccess guardedAccess) {
1539+
exists(
1540+
RangeSsaDefinition def, StackVariable v, VariableAccess guardVa, Expr guard, boolean branch
1541+
|
1542+
def.isGuardPhi(v, guardVa, guard, branch) and
1543+
// If the basic block for the variable access being examined has
1544+
// more than one predecessor, the guard phi node could originate
1545+
// from one of the predecessors. This is because the guard phi
1546+
// node is attached to the block at the end of the edge and not on
1547+
// the actual edge. It is therefore not possible to determine which
1548+
// edge the guard phi node belongs to. The predicate below ensures
1549+
// that there is one predecessor, albeit somewhat conservative.
1550+
exists(unique(BasicBlock b | b = def.(BasicBlock).getAPredecessor())) and
1551+
guardedAccess = def.getAUse(v) and
1552+
result = max(float ub | upperBoundFromGuard(guard, guardVa, ub, branch))
1553+
)
1554+
}
1555+
15331556
cached
15341557
private module SimpleRangeAnalysisCached {
15351558
/**
@@ -1565,9 +1588,9 @@ private module SimpleRangeAnalysisCached {
15651588
*/
15661589
cached
15671590
float upperBound(Expr expr) {
1568-
// Combine the upper bounds returned by getTruncatedUpperBounds into a
1569-
// single maximum value.
1570-
result = max(float ub | ub = getTruncatedUpperBounds(expr) | ub)
1591+
// Combine the upper bounds returned by getTruncatedUpperBounds and
1592+
// getGuardedUpperBound into a single maximum value
1593+
result = min([max(getTruncatedUpperBounds(expr)), getGuardedUpperBound(expr)])
15711594
}
15721595

15731596
/**

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

Lines changed: 20 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -594,6 +594,11 @@
594594
| test.c:659:9:659:9 | u | 0 |
595595
| test.c:664:12:664:12 | s | -2147483648 |
596596
| test.c:665:7:665:8 | s2 | -4 |
597+
| test.c:670:7:670:7 | x | -2147483648 |
598+
| test.c:671:9:671:9 | y | -2147483648 |
599+
| test.c:675:7:675:7 | y | -2147483648 |
600+
| test.c:684:7:684:7 | x | -2147483648 |
601+
| test.c:689:7:689:7 | x | -2147483648 |
597602
| test.cpp:10:7:10:7 | b | -2147483648 |
598603
| test.cpp:11:5:11:5 | x | -2147483648 |
599604
| test.cpp:13:10:13:10 | x | -2147483648 |
@@ -647,16 +652,18 @@
647652
| test.cpp:97:10:97:10 | i | -2147483648 |
648653
| test.cpp:97:22:97:22 | i | -2147483648 |
649654
| test.cpp:98:5:98:5 | i | -2147483648 |
650-
| test.cpp:105:7:105:7 | n | -32768 |
651-
| test.cpp:108:7:108:7 | n | 0 |
652-
| test.cpp:109:5:109:5 | n | 1 |
653-
| test.cpp:111:5:111:5 | n | 0 |
654-
| test.cpp:114:8:114:8 | n | 0 |
655-
| test.cpp:115:5:115:5 | n | 0 |
656-
| test.cpp:117:5:117:5 | n | 1 |
657-
| test.cpp:120:3:120:3 | n | 0 |
658-
| test.cpp:120:8:120:8 | n | 1 |
659-
| test.cpp:120:12:120:12 | n | 0 |
660-
| test.cpp:121:4:121:4 | n | 0 |
661-
| test.cpp:121:8:121:8 | n | 0 |
662-
| test.cpp:121:12:121:12 | n | 1 |
655+
| test.cpp:98:9:98:9 | i | -2147483648 |
656+
| test.cpp:99:5:99:5 | i | -2147483648 |
657+
| test.cpp:106:7:106:7 | n | -32768 |
658+
| test.cpp:109:7:109:7 | n | 0 |
659+
| test.cpp:110:5:110:5 | n | 1 |
660+
| test.cpp:112:5:112:5 | n | 0 |
661+
| test.cpp:115:8:115:8 | n | 0 |
662+
| test.cpp:116:5:116:5 | n | 0 |
663+
| test.cpp:118:5:118:5 | n | 1 |
664+
| test.cpp:121:3:121:3 | n | 0 |
665+
| test.cpp:121:8:121:8 | n | 1 |
666+
| test.cpp:121:12:121:12 | n | 0 |
667+
| test.cpp:122:4:122:4 | n | 0 |
668+
| test.cpp:122:8:122:8 | n | 0 |
669+
| test.cpp:122:12:122:12 | n | 1 |

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,5 +15,5 @@
1515
| test.c:394:20:394:36 | ... ? ... : ... | 0.0 | 0.0 | 100.0 |
1616
| test.c:606:5:606:14 | ... ? ... : ... | 0.0 | 1.0 | 0.0 |
1717
| test.c:607:5:607:14 | ... ? ... : ... | 0.0 | 0.0 | 1.0 |
18-
| test.cpp:120:3:120:12 | ... ? ... : ... | 0.0 | 1.0 | 0.0 |
19-
| test.cpp:121:3:121:12 | ... ? ... : ... | 0.0 | 0.0 | 1.0 |
18+
| test.cpp:121:3:121:12 | ... ? ... : ... | 0.0 | 1.0 | 0.0 |
19+
| test.cpp:122:3:122:12 | ... ? ... : ... | 0.0 | 0.0 | 1.0 |

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,5 +15,5 @@
1515
| test.c:394:20:394:36 | ... ? ... : ... | 100.0 | 99.0 | 100.0 |
1616
| test.c:606:5:606:14 | ... ? ... : ... | 32767.0 | 32767.0 | 0.0 |
1717
| test.c:607:5:607:14 | ... ? ... : ... | 32767.0 | 0.0 | 32767.0 |
18-
| test.cpp:120:3:120:12 | ... ? ... : ... | 32767.0 | 32767.0 | 0.0 |
19-
| test.cpp:121:3:121:12 | ... ? ... : ... | 32767.0 | 0.0 | 32767.0 |
18+
| test.cpp:121:3:121:12 | ... ? ... : ... | 32767.0 | 32767.0 | 0.0 |
19+
| test.cpp:122:3:122:12 | ... ? ... : ... | 32767.0 | 0.0 | 32767.0 |

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

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -664,3 +664,28 @@ void test_mod(int s) {
664664
int s2 = s % 5;
665665
out(s2); // -4 .. 4
666666
}
667+
668+
void exit(int);
669+
void guard_with_exit(int x, int y) {
670+
if (x) {
671+
if (y != 0) {
672+
exit(0);
673+
}
674+
}
675+
out(y); // ..
676+
677+
// This test ensures that we correctly identify
678+
// that the upper bound for y is max_int when calling `out(y)`.
679+
// The RangeSsa will place guardPhy on `out(y)`, and consequently there is no
680+
// frontier phi node at out(y).
681+
}
682+
683+
void test(int x) {
684+
if (x >= 10) {
685+
return;
686+
}
687+
// The basic below has two predecessors.
688+
label:
689+
out(x);
690+
goto label;
691+
}

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,7 @@ int ref_to_number(int &i, const int &ci, int &aliased) {
9595
return alias;
9696

9797
for (; i <= 12345; i++) { // test that widening works for references
98+
i = i;
9899
i;
99100
}
100101

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

Lines changed: 24 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -584,16 +584,21 @@
584584
| test.c:639:9:639:10 | ss | 2 |
585585
| test.c:645:8:645:8 | s | 2147483647 |
586586
| test.c:645:15:645:15 | s | 127 |
587-
| test.c:645:23:645:23 | s | 15 |
588-
| test.c:646:18:646:18 | s | 15 |
589-
| test.c:646:22:646:22 | s | 15 |
587+
| test.c:645:23:645:23 | s | 9 |
588+
| test.c:646:18:646:18 | s | 9 |
589+
| test.c:646:22:646:22 | s | 9 |
590590
| test.c:647:9:647:14 | result | 127 |
591591
| test.c:653:7:653:7 | i | 0 |
592592
| test.c:654:9:654:9 | i | 2147483647 |
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 |
596596
| test.c:665:7:665:8 | s2 | 4 |
597+
| test.c:670:7:670:7 | x | 2147483647 |
598+
| test.c:671:9:671:9 | y | 2147483647 |
599+
| test.c:675:7:675:7 | y | 2147483647 |
600+
| test.c:684:7:684:7 | x | 2147483647 |
601+
| test.c:689:7:689:7 | x | 15 |
597602
| test.cpp:10:7:10:7 | b | 2147483647 |
598603
| test.cpp:11:5:11:5 | x | 2147483647 |
599604
| test.cpp:13:10:13:10 | x | 2147483647 |
@@ -646,17 +651,19 @@
646651
| test.cpp:95:12:95:16 | alias | 2147483647 |
647652
| test.cpp:97:10:97:10 | i | 65535 |
648653
| test.cpp:97:22:97:22 | i | 32767 |
649-
| test.cpp:98:5:98:5 | i | 32767 |
650-
| test.cpp:105:7:105:7 | n | 32767 |
651-
| test.cpp:108:7:108:7 | n | 32767 |
652-
| test.cpp:109:5:109:5 | n | 32767 |
653-
| test.cpp:111:5:111:5 | n | 0 |
654-
| test.cpp:114:8:114:8 | n | 32767 |
655-
| test.cpp:115:5:115:5 | n | 0 |
656-
| test.cpp:117:5:117:5 | n | 32767 |
657-
| test.cpp:120:3:120:3 | n | 32767 |
658-
| test.cpp:120:8:120:8 | n | 32767 |
659-
| test.cpp:120:12:120:12 | n | 0 |
660-
| test.cpp:121:4:121:4 | n | 32767 |
661-
| test.cpp:121:8:121:8 | n | 0 |
662-
| test.cpp:121:12:121:12 | n | 32767 |
654+
| test.cpp:98:5:98:5 | i | 2147483647 |
655+
| test.cpp:98:9:98:9 | i | 12345 |
656+
| test.cpp:99:5:99:5 | i | 32767 |
657+
| test.cpp:106:7:106:7 | n | 32767 |
658+
| test.cpp:109:7:109:7 | n | 32767 |
659+
| test.cpp:110:5:110:5 | n | 32767 |
660+
| test.cpp:112:5:112:5 | n | 0 |
661+
| test.cpp:115:8:115:8 | n | 32767 |
662+
| test.cpp:116:5:116:5 | n | 0 |
663+
| test.cpp:118:5:118:5 | n | 32767 |
664+
| test.cpp:121:3:121:3 | n | 32767 |
665+
| test.cpp:121:8:121:8 | n | 32767 |
666+
| test.cpp:121:12:121:12 | n | 0 |
667+
| test.cpp:122:4:122:4 | n | 32767 |
668+
| test.cpp:122:8:122:8 | n | 0 |
669+
| test.cpp:122:12:122:12 | n | 32767 |

cpp/ql/test/query-tests/Critical/OverflowStatic/test.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,3 +46,13 @@ void f2(char *src)
4646
ptr = &(buffer[1]);
4747
memcpy(ptr, src, 100); // BAD [NOT DETECTED]
4848
}
49+
50+
void f3() {
51+
int i;
52+
char buffer[5];
53+
for (i=0; i<10; i++) {
54+
if (i < 5) {
55+
buffer[i] = 0; // GOOD
56+
}
57+
}
58+
}

0 commit comments

Comments
 (0)