Skip to content

Commit 78d2ac1

Browse files
rdmarsh2rdmarsh2
authored
Merge pull request #3368 from Cornelius-Riemenschneider/local-ala
C++: Add experimental Array Length Tracking library
2 parents 0e0d049 + 2647630 commit 78d2ac1

File tree

6 files changed

+455
-32
lines changed

6 files changed

+455
-32
lines changed

‎cpp/ql/src/experimental/semmle/code/cpp/rangeanalysis/ArrayLengthAnalysis.qll

Lines changed: 282 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,282 @@
1+
/**
2+
* Provides precise tracking of how big the memory pointed to by pointers is.
3+
* For each pointer, we start tracking (starting from the allocation or an array declaration)
4+
* 1) how long is the chunk of memory allocated
5+
* 2) where the current pointer is in this chunk of memory
6+
* As computing this information is obviously not possible for all pointers,
7+
* we do not guarantee the existence of length/offset information for all pointers.
8+
* However, when it exists it is guaranteed to be accurate.
9+
*
10+
* The length and offset are tracked in a similar way to the Rangeanalysis.
11+
* Each length is a `ValueNumber + delta`, and each Offset is an `Operand + delta`.
12+
* We choose to track a `ValueNumber` for length, because the Rangeanalysis offers
13+
* integer bounds on instructions and operands in terms of `ValueNumber`s,
14+
* and `Operand` for offset because integer bounds on `Operand`s are
15+
* tighter than bounds on `Instruction`s.
16+
*/
17+
18+
import cpp
19+
import semmle.code.cpp.ir.IR
20+
private import semmle.code.cpp.ir.ValueNumbering
21+
private import semmle.code.cpp.ir.internal.CppType
22+
private import semmle.code.cpp.models.interfaces.Allocation
23+
private import semmle.code.cpp.rangeanalysis.RangeUtils
24+
25+
private newtype TLength =
26+
TZeroLength() or
27+
TVNLength(ValueNumber vn) {
28+
not vn.getAnInstruction() instanceof ConstantInstruction and
29+
exists(Instruction i |
30+
vn.getAnInstruction() = i and
31+
(
32+
i.getResultIRType() instanceof IRSignedIntegerType or
33+
i.getResultIRType() instanceof IRUnsignedIntegerType
34+
)
35+
|
36+
i instanceof PhiInstruction
37+
or
38+
i instanceof InitializeParameterInstruction
39+
or
40+
i instanceof CallInstruction
41+
or
42+
i.(LoadInstruction).getSourceAddress() instanceof VariableAddressInstruction
43+
or
44+
i.(LoadInstruction).getSourceAddress() instanceof FieldAddressInstruction
45+
or
46+
i.getAUse() instanceof ArgumentOperand
47+
)
48+
}
49+
50+
/**
51+
* Array lengths are represented in a ValueNumber | Zero + delta format.
52+
* This class keeps track of the ValueNumber or Zero.
53+
* The delta is tracked in the predicate `knownArrayLength`.
54+
*/
55+
class Length extends TLength {
56+
string toString() { none() } // overridden in subclasses
57+
}
58+
59+
/**
60+
* This length class corresponds to an array having a constant length
61+
* that is tracked by the delta value.
62+
*/
63+
class ZeroLength extends Length, TZeroLength {
64+
override string toString() { result = "ZeroLength" }
65+
}
66+
67+
/**
68+
* This length class corresponds to an array having variable length, i.e. the
69+
* length is tracked by a value number. One example is an array having length
70+
* `count` for an integer variable `count` in the program.
71+
*/
72+
class VNLength extends Length, TVNLength {
73+
ValueNumber vn;
74+
75+
VNLength() { this = TVNLength(vn) }
76+
77+
/** Gets an instruction with this value number bound. */
78+
Instruction getInstruction() { this = TVNLength(valueNumber(result)) }
79+
80+
ValueNumber getValueNumber() { result = vn }
81+
82+
override string toString() { result = "VNLength(" + vn.getExampleInstruction().toString() + ")" }
83+
}
84+
85+
private newtype TOffset =
86+
TZeroOffset() or
87+
TOpOffset(Operand op) {
88+
op.getAnyDef().getResultIRType() instanceof IRSignedIntegerType or
89+
op.getAnyDef().getResultIRType() instanceof IRUnsignedIntegerType
90+
}
91+
92+
/**
93+
* This class describes the offset of a pointer in a chunk of memory.
94+
* It is either an `Operand` or zero, an additional integer delta is added later.
95+
*/
96+
class Offset extends TOffset {
97+
string toString() { none() } // overridden in subclasses
98+
}
99+
100+
/**
101+
* This class represents a fixed offset, only specified by a delta.
102+
*/
103+
class ZeroOffset extends Offset, TZeroOffset {
104+
override string toString() { result = "ZeroOffset" }
105+
}
106+
107+
/**
108+
* This class represents an offset of an operand.
109+
*/
110+
class OpOffset extends Offset, TOpOffset {
111+
Operand op;
112+
113+
OpOffset() { this = TOpOffset(op) }
114+
115+
Operand getOperand() { result = op }
116+
117+
override string toString() { result = "OpOffset(" + op.getDef().toString() + ")" }
118+
}
119+
120+
private int getBaseSizeForPointerType(PointerType type) { result = type.getBaseType().getSize() }
121+
122+
/**
123+
* Holds if pointer `prev` that points at offset `prevOffset + prevOffsetDelta`
124+
* steps to `array` that points to `offset + offsetDelta` in one step.
125+
* This predicate does not contain any recursive steps.
126+
*/
127+
bindingset[prevOffset, prevOffsetDelta]
128+
predicate simpleArrayLengthStep(
129+
Instruction array, Offset offset, int offsetDelta, Instruction prev, Offset prevOffset,
130+
int prevOffsetDelta
131+
) {
132+
// array assign
133+
array.(CopyInstruction).getSourceValue() = prev and
134+
offset = prevOffset and
135+
offsetDelta = prevOffsetDelta
136+
or
137+
// pointer add with constant
138+
array.(PointerAddInstruction).getLeft() = prev and
139+
offset = prevOffset and
140+
offsetDelta = prevOffsetDelta + getConstantValue(array.(PointerAddInstruction).getRight())
141+
or
142+
// pointer add with variable
143+
array.(PointerAddInstruction).getLeft() = prev and
144+
prevOffset instanceof ZeroOffset and
145+
offset.(OpOffset).getOperand() = array.(PointerAddInstruction).getRightOperand() and
146+
offsetDelta = prevOffsetDelta and
147+
not exists(getConstantValue(array.(PointerAddInstruction).getRight()))
148+
or
149+
// pointer sub with constant
150+
array.(PointerSubInstruction).getLeft() = prev and
151+
offset = prevOffset and
152+
offsetDelta = prevOffsetDelta - getConstantValue(array.(PointerSubInstruction).getRight())
153+
or
154+
// array to pointer decay
155+
array.(ConvertInstruction).getUnary() = prev and
156+
array.getConvertedResultExpression() instanceof ArrayToPointerConversion and
157+
offset = prevOffset and
158+
offsetDelta = prevOffsetDelta
159+
or
160+
// cast of pointer to pointer with the same element size
161+
exists(PointerType fromTyp, PointerType toTyp |
162+
array.(PtrToPtrCastInstruction).getUnary() = prev and
163+
prev.getResultLanguageType().hasType(fromTyp, false) and
164+
array.getResultLanguageType().hasType(toTyp, false) and
165+
offset = prevOffset and
166+
offsetDelta = prevOffsetDelta and
167+
if fromTyp instanceof VoidPointerType
168+
then getBaseSizeForPointerType(toTyp) = 1
169+
else (
170+
if toTyp instanceof VoidPointerType
171+
then getBaseSizeForPointerType(fromTyp) = 1
172+
else getBaseSizeForPointerType(toTyp) = getBaseSizeForPointerType(fromTyp)
173+
)
174+
)
175+
}
176+
177+
/**
178+
* Parses a `sizeExpr` of malloc into a variable part (`lengthExpr`) and an integer offset (`delta`).
179+
*/
180+
private predicate deconstructMallocSizeExpr(Expr sizeExpr, Expr lengthExpr, int delta) {
181+
sizeExpr instanceof AddExpr and
182+
exists(Expr constantExpr |
183+
lengthExpr = sizeExpr.(AddExpr).getAnOperand() and
184+
constantExpr = sizeExpr.(AddExpr).getAnOperand() and
185+
lengthExpr != constantExpr and
186+
delta = constantExpr.getValue().toInt()
187+
)
188+
or
189+
sizeExpr instanceof SubExpr and
190+
exists(Expr constantExpr |
191+
lengthExpr = sizeExpr.(SubExpr).getLeftOperand() and
192+
constantExpr = sizeExpr.(SubExpr).getRightOperand() and
193+
delta = -constantExpr.getValue().toInt()
194+
)
195+
}
196+
197+
/**
198+
* Holds if the instruction `array` is a dynamic memory allocation of `length`+`delta` elements.
199+
*/
200+
private predicate allocation(Instruction array, Length length, int delta) {
201+
exists(AllocationExpr alloc, Type ptrTyp |
202+
array.getUnconvertedResultExpression() = alloc and
203+
array.getResultLanguageType().hasType(ptrTyp, false) and
204+
// ensure that we have the same type of the allocation and the pointer
205+
ptrTyp.stripTopLevelSpecifiers().(PointerType).getBaseType().getUnspecifiedType() =
206+
alloc.getAllocatedElementType().getUnspecifiedType() and
207+
// ensure that the size multiplier of the allocation is the same as the
208+
// size of the type we are allocating
209+
alloc.getSizeMult() = getBaseSizeForPointerType(ptrTyp) and
210+
(
211+
length instanceof ZeroLength and
212+
delta = alloc.getSizeExpr().getValue().toInt()
213+
or
214+
not exists(alloc.getSizeExpr().getValue().toInt()) and
215+
(
216+
exists(Expr lengthExpr |
217+
deconstructMallocSizeExpr(alloc.getSizeExpr(), lengthExpr, delta) and
218+
length.(VNLength).getInstruction().getConvertedResultExpression() = lengthExpr
219+
)
220+
or
221+
not exists(int d | deconstructMallocSizeExpr(alloc.getSizeExpr(), _, d)) and
222+
length.(VNLength).getInstruction().getConvertedResultExpression() = alloc.getSizeExpr() and
223+
delta = 0
224+
)
225+
)
226+
)
227+
}
228+
229+
/**
230+
* Holds if `array` is declared as an array with length `length + lengthDelta`
231+
*/
232+
private predicate arrayDeclaration(Instruction array, Length length, int lengthDelta) {
233+
(
234+
array instanceof VariableAddressInstruction or
235+
array instanceof FieldAddressInstruction
236+
) and
237+
exists(ArrayType type | array.getResultLanguageType().hasType(type, _) |
238+
length instanceof ZeroLength and
239+
lengthDelta = type.getArraySize()
240+
)
241+
}
242+
243+
/**
244+
* Holds if `array` is declared as an array or allocated
245+
* with length `length + lengthDelta`
246+
*/
247+
predicate arrayAllocationOrDeclaration(Instruction array, Length length, int lengthDelta) {
248+
allocation(array, length, lengthDelta)
249+
or
250+
// declaration of variable of array type
251+
arrayDeclaration(array, length, lengthDelta)
252+
}
253+
254+
/**
255+
* Holds if the instruction `array` represents a pointer to a chunk of memory that holds
256+
* `length + lengthDelta` elements, using only local analysis.
257+
* `array` points at `offset + offsetDelta` in the chunk of memory.
258+
* The pointer is in-bounds if `offset + offsetDelta < length + lengthDelta` and
259+
* `offset + offsetDelta >= 0` holds.
260+
* The pointer is out-of-bounds if `offset + offsetDelta >= length + lengthDelta`
261+
* or `offset + offsetDelta < 0` holds.
262+
* All pointers in this predicate are guaranteed to be non-null,
263+
* but are not guaranteed to be live.
264+
*/
265+
predicate knownArrayLength(
266+
Instruction array, Length length, int lengthDelta, Offset offset, int offsetDelta
267+
) {
268+
arrayAllocationOrDeclaration(array, length, lengthDelta) and
269+
offset instanceof ZeroOffset and
270+
offsetDelta = 0
271+
or
272+
// simple step (no phi nodes)
273+
exists(Instruction prev, Offset prevOffset, int prevOffsetDelta |
274+
knownArrayLength(prev, length, lengthDelta, prevOffset, prevOffsetDelta) and
275+
simpleArrayLengthStep(array, offset, offsetDelta, prev, prevOffset, prevOffsetDelta)
276+
)
277+
or
278+
// merge control flow after phi node - but only if all the bounds agree
279+
forex(Instruction input | array.(PhiInstruction).getAnInput() = input |
280+
knownArrayLength(input, length, lengthDelta, offset, offsetDelta)
281+
)
282+
}

‎cpp/ql/src/semmle/code/cpp/rangeanalysis/RangeAnalysis.qll

Lines changed: 0 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -241,38 +241,6 @@ class CondReason extends Reason, TCondReason {
241241
override string toString() { result = getCond().toString() }
242242
}
243243

244-
/**
245-
* Holds if a cast from `fromtyp` to `totyp` can be ignored for the purpose of
246-
* range analysis.
247-
*/
248-
pragma[inline]
249-
private predicate safeCast(IntegralType fromtyp, IntegralType totyp) {
250-
fromtyp.getSize() < totyp.getSize() and
251-
(
252-
fromtyp.isUnsigned()
253-
or
254-
totyp.isSigned()
255-
)
256-
or
257-
fromtyp.getSize() <= totyp.getSize() and
258-
(
259-
fromtyp.isSigned() and
260-
totyp.isSigned()
261-
or
262-
fromtyp.isUnsigned() and
263-
totyp.isUnsigned()
264-
)
265-
}
266-
267-
private class SafeCastInstruction extends ConvertInstruction {
268-
SafeCastInstruction() {
269-
safeCast(getUnary().getResultType(), getResultType())
270-
or
271-
getResultType() instanceof PointerType and
272-
getUnary().getResultType() instanceof PointerType
273-
}
274-
}
275-
276244
/**
277245
* Holds if `typ` is a small integral type with the given lower and upper bounds.
278246
*/

‎cpp/ql/src/semmle/code/cpp/rangeanalysis/RangeUtils.qll

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,3 +80,55 @@ predicate backEdge(PhiInstruction phi, PhiInputOperand op) {
8080
phi.getAnOperand() = op and
8181
phi.getBlock() = op.getPredecessorBlock().getBackEdgeSuccessor(_)
8282
}
83+
84+
/**
85+
* Holds if a cast from `fromtyp` to `totyp` can be ignored for the purpose of
86+
* range analysis.
87+
*/
88+
pragma[inline]
89+
private predicate safeCast(IntegralType fromtyp, IntegralType totyp) {
90+
fromtyp.getSize() < totyp.getSize() and
91+
(
92+
fromtyp.isUnsigned()
93+
or
94+
totyp.isSigned()
95+
)
96+
or
97+
fromtyp.getSize() <= totyp.getSize() and
98+
(
99+
fromtyp.isSigned() and
100+
totyp.isSigned()
101+
or
102+
fromtyp.isUnsigned() and
103+
totyp.isUnsigned()
104+
)
105+
}
106+
107+
/**
108+
* A `ConvertInstruction` which casts from one pointer type to another.
109+
*/
110+
class PtrToPtrCastInstruction extends ConvertInstruction {
111+
PtrToPtrCastInstruction() {
112+
getResultType() instanceof PointerType and
113+
getUnary().getResultType() instanceof PointerType
114+
}
115+
}
116+
117+
/**
118+
* A `ConvertInstruction` which casts from one integer type to another in a way
119+
* that cannot overflow or underflow.
120+
*/
121+
class SafeIntCastInstruction extends ConvertInstruction {
122+
SafeIntCastInstruction() { safeCast(getUnary().getResultType(), getResultType()) }
123+
}
124+
125+
/**
126+
* A `ConvertInstruction` which does not invalidate bounds determined by
127+
* range analysis.
128+
*/
129+
class SafeCastInstruction extends ConvertInstruction {
130+
SafeCastInstruction() {
131+
this instanceof PtrToPtrCastInstruction or
132+
this instanceof SafeIntCastInstruction
133+
}
134+
}

0 commit comments

Comments
 (0)