@@ -81,8 +81,8 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
81
81
* ```
82
82
*
83
83
* We do this by splitting the task up into two configurations:
84
- * 1. `AllocToInvalidPointerConf ` find flow from `malloc(size)` to `begin + size`, and
85
- * 2. `InvalidPointerToDerefConf ` finds flow from `begin + size` to an `end` (on line 3).
84
+ * 1. `AllocToInvalidPointerConfig ` find flow from `malloc(size)` to `begin + size`, and
85
+ * 2. `InvalidPointerToDerefConfig ` finds flow from `begin + size` to an `end` (on line 3).
86
86
*
87
87
* Finally, the range-analysis library will find a load from (or store to) an address that
88
88
* is non-strictly upper-bounded by `end` (which in this case is `*p`).
@@ -180,13 +180,13 @@ predicate isSinkImpl(
180
180
}
181
181
182
182
/**
183
- * Holds if `sink` is a sink for `InvalidPointerToDerefConf ` and `i` is a `StoreInstruction` that
183
+ * Holds if `sink` is a sink for `InvalidPointerToDerefConfig ` and `i` is a `StoreInstruction` that
184
184
* writes to an address that non-strictly upper-bounds `sink`, or `i` is a `LoadInstruction` that
185
185
* reads from an address that non-strictly upper-bounds `sink`.
186
186
*/
187
187
pragma [ inline]
188
- predicate isInvalidPointerDerefSink ( DataFlow:: Node sink , Instruction i , string operation ) {
189
- exists ( AddressOperand addr , int delta |
188
+ predicate isInvalidPointerDerefSink ( DataFlow:: Node sink , Instruction i , string operation , int delta ) {
189
+ exists ( AddressOperand addr |
190
190
bounded1 ( addr .getDef ( ) , sink .asInstruction ( ) , delta ) and
191
191
delta >= 0 and
192
192
i .getAnOperand ( ) = addr
@@ -201,13 +201,13 @@ predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string o
201
201
202
202
/**
203
203
* A configuration to track flow from a pointer-arithmetic operation found
204
- * by `AllocToInvalidPointerConf ` to a dereference of the pointer.
204
+ * by `AllocToInvalidPointerConfig ` to a dereference of the pointer.
205
205
*/
206
206
module InvalidPointerToDerefConfig implements DataFlow:: ConfigSig {
207
207
predicate isSource ( DataFlow:: Node source ) { invalidPointerToDerefSource ( _, source , _) }
208
208
209
209
pragma [ inline]
210
- predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _) }
210
+ predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _, _ ) }
211
211
212
212
predicate isBarrier ( DataFlow:: Node node ) {
213
213
node = any ( DataFlow:: SsaPhiNode phi | not phi .isPhiRead ( ) ) .getAnInput ( true )
@@ -237,17 +237,17 @@ predicate invalidPointerToDerefSource(
237
237
}
238
238
239
239
newtype TMergedPathNode =
240
- // The path nodes computed by the first projection of `AllocToInvalidPointerConf `
240
+ // The path nodes computed by the first projection of `AllocToInvalidPointerConfig `
241
241
TPathNode1 ( AllocToInvalidPointerFlow:: PathNode1 p ) or
242
- // The path nodes computed by `InvalidPointerToDerefConf `
242
+ // The path nodes computed by `InvalidPointerToDerefConfig `
243
243
TPathNode3 ( InvalidPointerToDerefFlow:: PathNode p ) or
244
- // The read/write that uses the invalid pointer identified by `InvalidPointerToDerefConf `.
245
- // This one is needed because the sink identified by `InvalidPointerToDerefConf ` is the
244
+ // The read/write that uses the invalid pointer identified by `InvalidPointerToDerefConfig `.
245
+ // This one is needed because the sink identified by `InvalidPointerToDerefConfig ` is the
246
246
// pointer, but we want to raise an alert at the dereference.
247
247
TPathNodeSink ( Instruction i ) {
248
248
exists ( DataFlow:: Node n |
249
249
InvalidPointerToDerefFlow:: flowTo ( n ) and
250
- isInvalidPointerDerefSink ( n , i , _)
250
+ isInvalidPointerDerefSink ( n , i , _, _ )
251
251
)
252
252
}
253
253
@@ -321,7 +321,15 @@ query predicate edges(MergedPathNode node1, MergedPathNode node2) {
321
321
or
322
322
node1 .asPathNode3 ( ) .getASuccessor ( ) = node2 .asPathNode3 ( )
323
323
or
324
- joinOn2 ( node1 .asPathNode3 ( ) , node2 .asSinkNode ( ) , _)
324
+ joinOn2 ( node1 .asPathNode3 ( ) , node2 .asSinkNode ( ) , _, _)
325
+ }
326
+
327
+ query predicate nodes ( MergedPathNode n , string key , string val ) {
328
+ AllocToInvalidPointerFlow:: PathGraph1:: nodes ( n .asPathNode1 ( ) , key , val )
329
+ or
330
+ InvalidPointerToDerefFlow:: PathGraph:: nodes ( n .asPathNode3 ( ) , key , val )
331
+ or
332
+ key = "semmle.label" and val = n .asSinkNode ( ) .toString ( )
325
333
}
326
334
327
335
query predicate subpaths (
@@ -335,8 +343,8 @@ query predicate subpaths(
335
343
}
336
344
337
345
/**
338
- * Holds if `p1` is a sink of `AllocToInvalidPointerConf ` and `p2` is a source
339
- * of `InvalidPointerToDerefConf `, and they are connected through `pai`.
346
+ * Holds if `p1` is a sink of `AllocToInvalidPointerConfig ` and `p2` is a source
347
+ * of `InvalidPointerToDerefConfig `, and they are connected through `pai`.
340
348
*/
341
349
predicate joinOn1 (
342
350
PointerArithmeticInstruction pai , AllocToInvalidPointerFlow:: PathNode1 p1 ,
@@ -347,37 +355,37 @@ predicate joinOn1(
347
355
}
348
356
349
357
/**
350
- * Holds if `p1` is a sink of `InvalidPointerToDerefConf ` and `i` is the instruction
358
+ * Holds if `p1` is a sink of `InvalidPointerToDerefConfig ` and `i` is the instruction
351
359
* that dereferences `p1`. The string `operation` describes whether the `i` is
352
360
* a `StoreInstruction` or `LoadInstruction`.
353
361
*/
354
362
pragma [ inline]
355
- predicate joinOn2 ( InvalidPointerToDerefFlow:: PathNode p1 , Instruction i , string operation ) {
356
- isInvalidPointerDerefSink ( p1 .getNode ( ) , i , operation )
363
+ predicate joinOn2 ( InvalidPointerToDerefFlow:: PathNode p1 , Instruction i , string operation , int delta ) {
364
+ isInvalidPointerDerefSink ( p1 .getNode ( ) , i , operation , delta )
357
365
}
358
366
359
367
predicate hasFlowPath (
360
368
MergedPathNode source1 , MergedPathNode sink , InvalidPointerToDerefFlow:: PathNode source3 ,
361
- PointerArithmeticInstruction pai , string operation
369
+ PointerArithmeticInstruction pai , string operation , int delta
362
370
) {
363
371
exists ( InvalidPointerToDerefFlow:: PathNode sink3 , AllocToInvalidPointerFlow:: PathNode1 sink1 |
364
372
AllocToInvalidPointerFlow:: flowPath ( source1 .asPathNode1 ( ) , _, sink1 , _) and
365
373
joinOn1 ( pai , sink1 , source3 ) and
366
374
InvalidPointerToDerefFlow:: flowPath ( source3 , sink3 ) and
367
- joinOn2 ( sink3 , sink .asSinkNode ( ) , operation )
375
+ joinOn2 ( sink3 , sink .asSinkNode ( ) , operation , delta )
368
376
)
369
377
}
370
378
371
379
from
372
- MergedPathNode source , MergedPathNode sink , int k , string kstr ,
380
+ MergedPathNode source , MergedPathNode sink , int k2 , int k3 , string kstr ,
373
381
InvalidPointerToDerefFlow:: PathNode source3 , PointerArithmeticInstruction pai , string operation ,
374
382
Expr offset , DataFlow:: Node n
375
383
where
376
- hasFlowPath ( source , sink , source3 , pai , operation ) and
377
- invalidPointerToDerefSource ( pai , source3 .getNode ( ) , k ) and
384
+ hasFlowPath ( source , sink , source3 , pai , operation , k3 ) and
385
+ invalidPointerToDerefSource ( pai , source3 .getNode ( ) , k2 ) and
378
386
offset = pai .getRight ( ) .getUnconvertedResultExpression ( ) and
379
387
n = source .asPathNode1 ( ) .getNode ( ) and
380
- if k = 0 then kstr = "" else kstr = " + " + k
388
+ if ( k2 + k3 ) = 0 then kstr = "" else kstr = " + " + ( k2 + k3 )
381
389
select sink , source , sink ,
382
390
"This " + operation + " might be out of bounds, as the pointer might be equal to $@ + $@" + kstr +
383
391
"." , n , n .toString ( ) , offset , offset .toString ( )
0 commit comments