@@ -312,11 +312,13 @@ Instruction getASuccessor(Instruction instr) {
312312 */
313313pragma [ inline]
314314predicate isInvalidPointerDerefSink ( DataFlow:: Node sink , Instruction i , string operation , int delta ) {
315- exists ( AddressOperand addr , Instruction s |
315+ exists ( AddressOperand addr , Instruction s , IRBlock b |
316316 s = sink .asInstruction ( ) and
317- bounded1 ( addr .getDef ( ) , s , delta ) and
317+ boundedImpl ( addr .getDef ( ) , s , delta ) and
318318 delta >= 0 and
319- i .getAnOperand ( ) = addr
319+ i .getAnOperand ( ) = addr and
320+ b = i .getBlock ( ) and
321+ not b = InvalidPointerToDerefBarrier:: getABarrierBlock ( delta )
320322 |
321323 i instanceof StoreInstruction and
322324 operation = "write"
@@ -326,6 +328,60 @@ predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string o
326328 )
327329}
328330
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+
329385/**
330386 * A configuration to track flow from a pointer-arithmetic operation found
331387 * by `AllocToInvalidPointerConfig` to a dereference of the pointer.
@@ -338,6 +394,8 @@ module InvalidPointerToDerefConfig implements DataFlow::ConfigSig {
338394
339395 predicate isBarrier ( DataFlow:: Node node ) {
340396 node = any ( DataFlow:: SsaPhiNode phi | not phi .isPhiRead ( ) ) .getAnInput ( true )
397+ or
398+ node = InvalidPointerToDerefBarrier:: getABarrierNode ( )
341399 }
342400}
343401
@@ -382,7 +440,7 @@ newtype TMergedPathNode =
382440 // pointer, but we want to raise an alert at the dereference.
383441 TPathNodeSink ( Instruction i ) {
384442 exists ( DataFlow:: Node n |
385- InvalidPointerToDerefFlow:: flowTo ( n ) and
443+ InvalidPointerToDerefFlow:: flowTo ( pragma [ only_bind_into ] ( n ) ) and
386444 isInvalidPointerDerefSink ( n , i , _, _) and
387445 i = getASuccessor ( n .asInstruction ( ) )
388446 )
0 commit comments