Skip to content

Commit 396ccda

Browse files
authored
Merge pull request github#3422 from Cornelius-Riemenschneider/inbounds-ptr
C++: Add InBoundsPointerDeref.qll to experimental
2 parents ea2081c + 3596ff7 commit 396ccda

File tree

6 files changed

+258
-1
lines changed

6 files changed

+258
-1
lines changed
Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
/**
2+
* This library proves that a subset of pointer dereferences in a program are
3+
* safe, i.e. in-bounds.
4+
* It does so by first defining what a pointer dereference is (on the IR
5+
* `Instruction` level), and then using the array length analysis and the range
6+
* analysis together to prove that some of these pointer dereferences are safe.
7+
*
8+
* The analysis is soundy, i.e. it is sound if no undefined behaviour is present
9+
* in the program.
10+
* Furthermore, it crucially depends on the soundiness of the range analysis and
11+
* the array length analysis.
12+
*/
13+
14+
import cpp
15+
private import experimental.semmle.code.cpp.rangeanalysis.ArrayLengthAnalysis
16+
private import semmle.code.cpp.rangeanalysis.RangeAnalysis
17+
18+
/**
19+
* Gets the instruction that computes the address of memory that `i` accesses.
20+
* Only holds if `i` dereferences a pointer, not when the computation of the
21+
* memory address is constant, or if the address of a local variable is loaded/stored to.
22+
*/
23+
private Instruction getMemoryAddressInstruction(Instruction i) {
24+
(
25+
result = i.(FieldAddressInstruction).getObjectAddress() or
26+
result = i.(LoadInstruction).getSourceAddress() or
27+
result = i.(StoreInstruction).getDestinationAddress()
28+
) and
29+
not result instanceof FieldAddressInstruction and
30+
not result instanceof VariableAddressInstruction and
31+
not result instanceof ConstantValueInstruction
32+
}
33+
34+
/**
35+
* All instructions that dereference a pointer.
36+
*/
37+
class PointerDereferenceInstruction extends Instruction {
38+
PointerDereferenceInstruction() { exists(getMemoryAddressInstruction(this)) }
39+
40+
Instruction getAddress() { result = getMemoryAddressInstruction(this) }
41+
}
42+
43+
/**
44+
* Holds if `ptrDeref` can be proven to always access allocated memory.
45+
*/
46+
predicate inBounds(PointerDereferenceInstruction ptrDeref) {
47+
exists(Length length, int lengthDelta, Offset offset, int offsetDelta |
48+
knownArrayLength(ptrDeref.getAddress(), length, lengthDelta, offset, offsetDelta) and
49+
// lower bound - note that we treat a pointer that accesses an array of
50+
// length 0 as on upper-bound violation, but not as a lower-bound violation
51+
(
52+
offset instanceof ZeroOffset and
53+
offsetDelta >= 0
54+
or
55+
offset instanceof OpOffset and
56+
exists(int lowerBoundDelta |
57+
boundedOperand(offset.(OpOffset).getOperand(), any(ZeroBound b), lowerBoundDelta,
58+
/*upper*/ false, _) and
59+
lowerBoundDelta + offsetDelta >= 0
60+
)
61+
) and
62+
// upper bound
63+
(
64+
// both offset and length are only integers
65+
length instanceof ZeroLength and
66+
offset instanceof ZeroOffset and
67+
offsetDelta < lengthDelta
68+
or
69+
exists(int lengthBound |
70+
// array length is variable+integer, and there's a fixed (integer-only)
71+
// lower bound on the variable, so we can guarantee this access is always in-bounds
72+
length instanceof VNLength and
73+
offset instanceof ZeroOffset and
74+
boundedInstruction(length.(VNLength).getInstruction(), any(ZeroBound b), lengthBound,
75+
/* upper*/ false, _) and
76+
offsetDelta < lengthBound + lengthDelta
77+
)
78+
or
79+
exists(int offsetBoundDelta |
80+
length instanceof ZeroLength and
81+
offset instanceof OpOffset and
82+
boundedOperand(offset.(OpOffset).getOperand(), any(ZeroBound b), offsetBoundDelta,
83+
/* upper */ true, _) and
84+
// offset <= offsetBoundDelta, so offset + offsetDelta <= offsetDelta + offsetBoundDelta
85+
// Thus, in-bounds if offsetDelta + offsetBoundDelta < lengthDelta
86+
// as we have length instanceof ZeroLength
87+
offsetDelta + offsetBoundDelta < lengthDelta
88+
)
89+
or
90+
exists(ValueNumberBound b, int offsetBoundDelta |
91+
length instanceof VNLength and
92+
offset instanceof OpOffset and
93+
b.getValueNumber() = length.(VNLength).getValueNumber() and
94+
// It holds that offset <= length + offsetBoundDelta
95+
boundedOperand(offset.(OpOffset).getOperand(), b, offsetBoundDelta, /*upper*/ true, _) and
96+
// it also holds that
97+
offsetDelta < lengthDelta - offsetBoundDelta
98+
// taking both inequalities together we get
99+
// offset <= length + offsetBoundDelta
100+
// => offset + offsetDelta <= length + offsetBoundDelta + offsetDelta < length + offsetBoundDelta + lengthDelta - offsetBoundDelta
101+
// as required
102+
)
103+
)
104+
)
105+
}

cpp/ql/src/semmle/code/cpp/rangeanalysis/Bound.qll

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,12 +68,15 @@ class ValueNumberBound extends Bound, TBoundValueNumber {
6868

6969
ValueNumberBound() { this = TBoundValueNumber(vn) }
7070

71-
/** Gets the SSA variable that equals this bound. */
71+
/** Gets an `Instruction` that equals this bound. */
7272
override Instruction getInstruction(int delta) {
7373
this = TBoundValueNumber(valueNumber(result)) and delta = 0
7474
}
7575

7676
override string toString() { result = vn.getExampleInstruction().toString() }
7777

7878
override Location getLocation() { result = vn.getLocation() }
79+
80+
/** Gets the value number that equals this bound. */
81+
ValueNumber getValueNumber() { result = vn }
7982
}

cpp/ql/test/experimental/library-tests/rangeanalysis/arraylengthanalysis/test.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,3 +88,8 @@ void test2(unsigned int count, bool b) {
8888
a = (int*) malloc(sizeof(int) * (1024 - count));
8989
sink(a); // none, as the size expression is too complicated
9090
}
91+
92+
void test3(unsigned int object) {
93+
unsigned int* ptr = &object;
94+
sink(ptr); // TODO, none, but should be (Zero, 1, Zero, 0)
95+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
| test.cpp:14:18:14:18 | FieldAddress: a |
2+
| test.cpp:15:18:15:18 | FieldAddress: b |
3+
| test.cpp:26:5:26:12 | Store: ... = ... |
4+
| test.cpp:27:13:27:16 | Load: access to array |
5+
| test.cpp:33:5:33:12 | Store: ... = ... |
6+
| test.cpp:48:5:48:16 | Store: ... = ... |
7+
| test.cpp:61:7:61:14 | Store: ... = ... |
8+
| test.cpp:70:7:70:14 | Store: ... = ... |
9+
| test.cpp:81:11:81:14 | Load: access to array |
10+
| test.cpp:85:5:85:12 | Store: ... = ... |
11+
| test.cpp:87:3:87:11 | Store: ... = ... |
12+
| test.cpp:91:3:91:18 | Store: ... = ... |
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
import cpp
2+
import experimental.semmle.code.cpp.rangeanalysis.InBoundsPointerDeref
3+
4+
from PointerDereferenceInstruction ptrAccess
5+
where inBounds(ptrAccess)
6+
select ptrAccess
Lines changed: 126 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,126 @@
1+
void *malloc(unsigned long);
2+
3+
typedef struct A {
4+
int a;
5+
int b;
6+
char * c;
7+
} A;
8+
9+
void test1(unsigned int count) {
10+
if (count < 1) {
11+
return;
12+
}
13+
A* ptr = (A*) malloc(sizeof(A) * count);
14+
ptr[count - 1].a = 1000; // in-bounds
15+
ptr[count - 1].b = 1001; // in-bounds
16+
ptr[1].c = 0; // unknown
17+
ptr[count - 2].a = 1002; // dependant on call-site
18+
ptr[count].b = 1003; // out-of-bounds
19+
ptr[-1].c = 0; // out-of-bounds
20+
}
21+
22+
void test2(unsigned int count) {
23+
int* a = (int*) malloc(sizeof(int) * count);
24+
25+
for(unsigned int i = 0; i < count; ++i) {
26+
a[i] = 0; // in-bounds
27+
int l = a[i]; // in-bounds
28+
}
29+
30+
a = (int*) malloc(sizeof(int) * count);
31+
a = a + 2;
32+
for(unsigned int i = 0; i < count - 2; ++i) {
33+
a[i] = 0; // in-bounds
34+
}
35+
36+
for(unsigned int i = 0; i < count; ++i) {
37+
*a = 1; // in-bounds but not detected, array length tracking is not advanced enough for this
38+
a++;
39+
}
40+
41+
void* v = malloc(count);
42+
for(unsigned int i = 0; i < count; ++i) {
43+
((char *)v)[i] = 0; // in-bounds, but due to void-allocation not detected
44+
}
45+
46+
int stack[100];
47+
for(unsigned int i = 0; i < 100; ++i) {
48+
stack[i] = 0; // in-bounds
49+
}
50+
51+
for(unsigned int i = 0; i < count; ++i) {
52+
a = (int*) malloc(sizeof(int) * count);
53+
for (int j = 0; j < count; ++j) {
54+
a[j] = 0; // in-bounds, but not detected due to RangeAnalysis shortcomings
55+
}
56+
}
57+
58+
for(unsigned int i = 0; i < 10; ++i) {
59+
a = (int*) malloc(sizeof(int) * i);
60+
for (unsigned int j = 0; j < i; ++j) {
61+
a[j] = 0; // in-bounds
62+
}
63+
}
64+
65+
}
66+
void test3(int count) {
67+
for(int i = 0; i < count; ++i) {
68+
int * a = (int*) malloc(sizeof(int) * i);
69+
for (int j = 0; j < i; ++j) {
70+
a[j] = 0; // in-bounds
71+
}
72+
}
73+
}
74+
75+
76+
void test4(unsigned long count) {
77+
if (count < 1) {
78+
return;
79+
}
80+
int* a = (int*) malloc(sizeof(int) * count);
81+
int b = a[0] + 3; // in-bounds
82+
a = a + 2;
83+
unsigned int i = 0;
84+
for(; i < count - 2; ++i) {
85+
a[i] = 0; // in-bounds
86+
}
87+
a[-2] = 0; // in-bounds
88+
a[-3] = 0; // out-of-bounds
89+
a[i] = 0; // out-of-bounds
90+
a[count - 2] = 0; // out-of-bounds
91+
a[count - 3] = 0; // in-bounds
92+
}
93+
94+
void test5(unsigned int count) {
95+
int* a = (int*) malloc(sizeof(int) * count);
96+
a[0] = 0; // unknown, call-site dependant
97+
}
98+
99+
100+
void test6(unsigned int count, bool b) {
101+
if(count < 4) {
102+
return;
103+
}
104+
int* a = (int*) malloc(sizeof(int) * count);
105+
if (b) {
106+
a += 2;
107+
} else {
108+
a += 3;
109+
} // we lose all information about a after the phi-node here
110+
a[-2] = 0; // unknown
111+
a[-3] = 0; // unknown
112+
a[-4] = 0; // unknown
113+
a[0] = 0; // unknown
114+
}
115+
116+
void test7(unsigned int object) {
117+
unsigned int* ptr = &object;
118+
*ptr = 0; // in-bounds, but needs ArrayLengthAnalysis improvements.
119+
}
120+
121+
void test8() {
122+
void (*foo)(unsigned int);
123+
foo = &test7;
124+
foo(4); // in-bounds, but needs ArrayLengthAnalysis improvements.
125+
}
126+

0 commit comments

Comments
 (0)