@@ -312,11 +312,13 @@ Instruction getASuccessor(Instruction instr) {
312
312
*/
313
313
pragma [ inline]
314
314
predicate isInvalidPointerDerefSink ( DataFlow:: Node sink , Instruction i , string operation , int delta ) {
315
- exists ( AddressOperand addr , Instruction s |
315
+ exists ( AddressOperand addr , Instruction s , IRBlock b |
316
316
s = sink .asInstruction ( ) and
317
- bounded1 ( addr .getDef ( ) , s , delta ) and
317
+ boundedImpl ( addr .getDef ( ) , s , delta ) and
318
318
delta >= 0 and
319
- i .getAnOperand ( ) = addr
319
+ i .getAnOperand ( ) = addr and
320
+ b = i .getBlock ( ) and
321
+ not b = InvalidPointerToDerefBarrier:: getABarrierBlock ( delta )
320
322
|
321
323
i instanceof StoreInstruction and
322
324
operation = "write"
@@ -326,6 +328,60 @@ predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string o
326
328
)
327
329
}
328
330
331
+ module InvalidPointerToDerefBarrier {
332
+ private module BarrierConfig implements DataFlow:: ConfigSig {
333
+ predicate isSource ( DataFlow:: Node source ) {
334
+ // The sources is the same as in the sources for `InvalidPointerToDerefConfig`.
335
+ invalidPointerToDerefSource ( _, source , _)
336
+ }
337
+
338
+ additional predicate isSink (
339
+ DataFlow:: Node left , DataFlow:: Node right , IRGuardCondition g , int state , boolean testIsTrue
340
+ ) {
341
+ // The sink is any "large" side of a relational comparison.
342
+ g .comparesLt ( left .asOperand ( ) , right .asOperand ( ) , state , true , testIsTrue )
343
+ }
344
+
345
+ predicate isSink ( DataFlow:: Node sink ) { isSink ( _, sink , _, _, _) }
346
+ }
347
+
348
+ private import DataFlow:: Global< BarrierConfig >
349
+
350
+ private int getInvalidPointerToDerefSourceDelta ( DataFlow:: Node node ) {
351
+ exists ( DataFlow:: Node source |
352
+ flow ( source , node ) and
353
+ invalidPointerToDerefSource ( _, source , result )
354
+ )
355
+ }
356
+
357
+ private predicate operandGuardChecks (
358
+ IRGuardCondition g , Operand left , Operand right , int state , boolean edge
359
+ ) {
360
+ exists ( DataFlow:: Node nLeft , DataFlow:: Node nRight , int state0 |
361
+ nRight .asOperand ( ) = right and
362
+ nLeft .asOperand ( ) = left and
363
+ BarrierConfig:: isSink ( nLeft , nRight , g , state0 , edge ) and
364
+ state = getInvalidPointerToDerefSourceDelta ( nRight ) and
365
+ state0 <= state
366
+ )
367
+ }
368
+
369
+ Instruction getABarrierInstruction ( int state ) {
370
+ exists ( IRGuardCondition g , ValueNumber value , Operand use , boolean edge |
371
+ use = value .getAUse ( ) and
372
+ operandGuardChecks ( pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( use ) , _, state ,
373
+ pragma [ only_bind_into ] ( edge ) ) and
374
+ result = value .getAnInstruction ( ) and
375
+ g .controls ( result .getBlock ( ) , edge )
376
+ )
377
+ }
378
+
379
+ DataFlow:: Node getABarrierNode ( ) { result .asOperand ( ) = getABarrierInstruction ( _) .getAUse ( ) }
380
+
381
+ pragma [ nomagic]
382
+ IRBlock getABarrierBlock ( int state ) { result .getAnInstruction ( ) = getABarrierInstruction ( state ) }
383
+ }
384
+
329
385
/**
330
386
* A configuration to track flow from a pointer-arithmetic operation found
331
387
* by `AllocToInvalidPointerConfig` to a dereference of the pointer.
@@ -338,6 +394,8 @@ module InvalidPointerToDerefConfig implements DataFlow::ConfigSig {
338
394
339
395
predicate isBarrier ( DataFlow:: Node node ) {
340
396
node = any ( DataFlow:: SsaPhiNode phi | not phi .isPhiRead ( ) ) .getAnInput ( true )
397
+ or
398
+ node = InvalidPointerToDerefBarrier:: getABarrierNode ( )
341
399
}
342
400
}
343
401
@@ -382,7 +440,7 @@ newtype TMergedPathNode =
382
440
// pointer, but we want to raise an alert at the dereference.
383
441
TPathNodeSink ( Instruction i ) {
384
442
exists ( DataFlow:: Node n |
385
- InvalidPointerToDerefFlow:: flowTo ( n ) and
443
+ InvalidPointerToDerefFlow:: flowTo ( pragma [ only_bind_into ] ( n ) ) and
386
444
isInvalidPointerDerefSink ( n , i , _, _) and
387
445
i = getASuccessor ( n .asInstruction ( ) )
388
446
)
0 commit comments