@@ -179,15 +179,34 @@ predicate isSinkImpl(
179179 pointerAddInstructionHasBounds ( pai , sink1 , sink2 , delta )
180180}
181181
182+ /**
183+ * Yields any instruction that is control-flow reachable from `instr`.
184+ */
185+ bindingset [ instr, result ]
186+ pragma [ inline_late]
187+ Instruction getASuccessor ( Instruction instr ) {
188+ exists ( IRBlock b , int instrIndex , int resultIndex |
189+ result .getBlock ( ) = b and
190+ instr .getBlock ( ) = b and
191+ b .getInstruction ( instrIndex ) = instr and
192+ b .getInstruction ( resultIndex ) = result
193+ |
194+ resultIndex >= instrIndex
195+ )
196+ or
197+ instr .getBlock ( ) .getASuccessor + ( ) = result .getBlock ( )
198+ }
199+
182200/**
183201 * Holds if `sink` is a sink for `InvalidPointerToDerefConfig` and `i` is a `StoreInstruction` that
184202 * writes to an address that non-strictly upper-bounds `sink`, or `i` is a `LoadInstruction` that
185203 * reads from an address that non-strictly upper-bounds `sink`.
186204 */
187205pragma [ inline]
188206predicate isInvalidPointerDerefSink ( DataFlow:: Node sink , Instruction i , string operation , int delta ) {
189- exists ( AddressOperand addr |
190- bounded1 ( addr .getDef ( ) , sink .asInstruction ( ) , delta ) and
207+ exists ( AddressOperand addr , Instruction s |
208+ s = sink .asInstruction ( ) and
209+ bounded1 ( addr .getDef ( ) , s , delta ) and
191210 delta >= 0 and
192211 i .getAnOperand ( ) = addr
193212 |
@@ -247,7 +266,8 @@ newtype TMergedPathNode =
247266 TPathNodeSink ( Instruction i ) {
248267 exists ( DataFlow:: Node n |
249268 InvalidPointerToDerefFlow:: flowTo ( n ) and
250- isInvalidPointerDerefSink ( n , i , _, _)
269+ isInvalidPointerDerefSink ( n , i , _, _) and
270+ i = getASuccessor ( n .asInstruction ( ) )
251271 )
252272 }
253273
@@ -377,15 +397,19 @@ predicate hasFlowPath(
377397}
378398
379399from
380- MergedPathNode source , MergedPathNode sink , int k2 , int k3 , string kstr ,
381- InvalidPointerToDerefFlow:: PathNode source3 , PointerArithmeticInstruction pai , string operation ,
382- Expr offset , DataFlow:: Node n
400+ MergedPathNode source , MergedPathNode sink , int k , string kstr , PointerArithmeticInstruction pai ,
401+ string operation , Expr offset , DataFlow:: Node n
383402where
384- hasFlowPath ( source , sink , source3 , pai , operation , k3 ) and
385- invalidPointerToDerefSource ( pai , source3 .getNode ( ) , k2 ) and
403+ k =
404+ min ( int k2 , int k3 , InvalidPointerToDerefFlow:: PathNode source3 |
405+ hasFlowPath ( source , sink , source3 , pai , operation , k3 ) and
406+ invalidPointerToDerefSource ( pai , source3 .getNode ( ) , k2 )
407+ |
408+ k2 + k3
409+ ) and
386410 offset = pai .getRight ( ) .getUnconvertedResultExpression ( ) and
387411 n = source .asPathNode1 ( ) .getNode ( ) and
388- if ( k2 + k3 ) = 0 then kstr = "" else kstr = " + " + ( k2 + k3 )
412+ if k = 0 then kstr = "" else kstr = " + " + k
389413select sink , source , sink ,
390414 "This " + operation + " might be out of bounds, as the pointer might be equal to $@ + $@" + kstr +
391415 "." , n , n .toString ( ) , offset , offset .toString ( )
0 commit comments