23
23
* configuration (see `InvalidPointerToDerefConfig`).
24
24
*
25
25
* The dataflow traversal defines the set of sources as any dataflow node `n` such that there exists a pointer-arithmetic
26
- * instruction `pai` found by `AllocationToInvalidPointer.qll` and a `n.asInstruction() >= pai + deltaDerefSourceAndPai`.
27
- * Here, `deltaDerefSourceAndPai` is the constant difference between the source we track for finding a dereference and the
28
- * pointer-arithmetic instruction.
26
+ * instruction `pai` found by `AllocationToInvalidPointer.qll` and a `n.asInstruction() = pai`.
29
27
*
30
28
* The set of sinks is defined as any dataflow node `n` such that `addr <= n.asInstruction() + deltaDerefSinkAndDerefAddress`
31
29
* for some address operand `addr` and constant difference `deltaDerefSinkAndDerefAddress`. Since an address operand is
37
35
* `deltaDerefSinkAndDerefAddress >= 0`. The load attached to `*p` is the "operation". To ensure that the path makes
38
36
* intuitive sense, we only pick operations that are control-flow reachable from the dereference sink.
39
37
*
40
- * To compute how many elements the dereference is beyond the end position of the allocation, we sum the two deltas
41
- * `deltaDerefSourceAndPai` and `deltaDerefSinkAndDerefAddress`. This is done in the `operationIsOffBy` predicate
42
- * (which is the only predicate exposed by this file).
38
+ * We use the `deltaDerefSinkAndDerefAddress` to compute how many elements the dereference is beyond the end position of
39
+ * the allocation. This is done in the `operationIsOffBy` predicate (which is the only predicate exposed by this file).
43
40
*
44
41
* Handling false positives:
45
42
*
@@ -96,7 +93,7 @@ int invalidPointerToDereferenceFieldFlowBranchLimit() { result = 0 }
96
93
private module InvalidPointerToDerefBarrier {
97
94
private module BarrierConfig implements DataFlow:: ConfigSig {
98
95
additional predicate isSource ( DataFlow:: Node source , PointerArithmeticInstruction pai ) {
99
- invalidPointerToDerefSource ( _, pai , _, _ ) and
96
+ invalidPointerToDerefSource ( _, pai , _) and
100
97
// source <= pai
101
98
bounded2 ( source .asInstruction ( ) , pai , any ( int d | d <= 0 ) )
102
99
}
@@ -169,11 +166,11 @@ private module InvalidPointerToDerefBarrier {
169
166
*/
170
167
private module InvalidPointerToDerefConfig implements DataFlow:: StateConfigSig {
171
168
class FlowState extends PointerArithmeticInstruction {
172
- FlowState ( ) { invalidPointerToDerefSource ( _, this , _, _ ) }
169
+ FlowState ( ) { invalidPointerToDerefSource ( _, this , _) }
173
170
}
174
171
175
172
predicate isSource ( DataFlow:: Node source , FlowState pai ) {
176
- invalidPointerToDerefSource ( _, pai , source , _ )
173
+ invalidPointerToDerefSource ( _, pai , source )
177
174
}
178
175
179
176
pragma [ inline]
@@ -198,24 +195,17 @@ private import DataFlow::GlobalWithState<InvalidPointerToDerefConfig>
198
195
199
196
/**
200
197
* Holds if `allocSource` is dataflow node that represents an allocation that flows to the
201
- * left-hand side of the pointer-arithmetic `pai`, and `derefSource <= pai + derefSourcePaiDelta`.
202
- *
203
- * For example, if `pai` is a pointer-arithmetic operation `p + size` in an expression such
204
- * as `(p + size) + 1` and `derefSource` is the node representing `(p + size) + 1`. In this
205
- * case `derefSourcePaiDelta` is 1.
198
+ * left-hand side of the pointer-arithmetic instruction represented by `derefSource`.
206
199
*/
207
200
private predicate invalidPointerToDerefSource (
208
- DataFlow:: Node allocSource , PointerArithmeticInstruction pai , DataFlow:: Node derefSource ,
209
- int deltaDerefSourceAndPai
201
+ DataFlow:: Node allocSource , PointerArithmeticInstruction pai , DataFlow:: Node derefSource
210
202
) {
211
203
// Note that `deltaDerefSourceAndPai` is not necessarily equal to `rhsSizeDelta`:
212
204
// `rhsSizeDelta` is the constant offset added to the size of the allocation, and
213
205
// `deltaDerefSourceAndPai` is the constant difference between the pointer-arithmetic instruction
214
206
// and the instruction computing the address for which we will search for a dereference.
215
207
AllocToInvalidPointer:: pointerAddInstructionHasBounds ( allocSource , pai , _, _) and
216
- // derefSource <= pai + deltaDerefSourceAndPai
217
- bounded2 ( derefSource .asInstruction ( ) , pai , deltaDerefSourceAndPai ) and
218
- deltaDerefSourceAndPai >= 0
208
+ derefSource .asInstruction ( ) = pai
219
209
}
220
210
221
211
/**
@@ -258,11 +248,9 @@ private Instruction getASuccessor(Instruction instr) {
258
248
instr .getBlock ( ) .getASuccessor + ( ) = result .getBlock ( )
259
249
}
260
250
261
- private predicate paiForDereferenceSink (
262
- PointerArithmeticInstruction pai , DataFlow:: Node derefSink , int deltaDerefSourceAndPai
263
- ) {
251
+ private predicate paiForDereferenceSink ( PointerArithmeticInstruction pai , DataFlow:: Node derefSink ) {
264
252
exists ( DataFlow:: Node derefSource |
265
- invalidPointerToDerefSource ( _, pai , derefSource , deltaDerefSourceAndPai ) and
253
+ invalidPointerToDerefSource ( _, pai , derefSource ) and
266
254
flow ( derefSource , derefSink )
267
255
)
268
256
}
@@ -274,10 +262,10 @@ private predicate paiForDereferenceSink(
274
262
*/
275
263
private predicate derefSinkToOperation (
276
264
DataFlow:: Node derefSink , PointerArithmeticInstruction pai , DataFlow:: Node operation ,
277
- string description , int deltaDerefSourceAndPai , int deltaDerefSinkAndDerefAddress
265
+ string description , int deltaDerefSinkAndDerefAddress
278
266
) {
279
267
exists ( Instruction operationInstr , AddressOperand addr |
280
- paiForDereferenceSink ( pai , pragma [ only_bind_into ] ( derefSink ) , deltaDerefSourceAndPai ) and
268
+ paiForDereferenceSink ( pai , pragma [ only_bind_into ] ( derefSink ) ) and
281
269
isInvalidPointerDerefSink ( derefSink , addr , operationInstr , description ,
282
270
deltaDerefSinkAndDerefAddress ) and
283
271
operationInstr = getASuccessor ( derefSink .asInstruction ( ) ) and
@@ -298,11 +286,7 @@ predicate operationIsOffBy(
298
286
DataFlow:: Node allocation , PointerArithmeticInstruction pai , DataFlow:: Node derefSource ,
299
287
DataFlow:: Node derefSink , string description , DataFlow:: Node operation , int delta
300
288
) {
301
- exists ( int deltaDerefSourceAndPai , int deltaDerefSinkAndDerefAddress |
302
- invalidPointerToDerefSource ( allocation , pai , derefSource , deltaDerefSourceAndPai ) and
303
- flow ( derefSource , derefSink ) and
304
- derefSinkToOperation ( derefSink , pai , operation , description , deltaDerefSourceAndPai ,
305
- deltaDerefSinkAndDerefAddress ) and
306
- delta = deltaDerefSourceAndPai + deltaDerefSinkAndDerefAddress
307
- )
289
+ invalidPointerToDerefSource ( allocation , pai , derefSource ) and
290
+ flow ( derefSource , derefSink ) and
291
+ derefSinkToOperation ( derefSink , pai , operation , description , delta )
308
292
}
0 commit comments