@@ -241,6 +241,7 @@ pragma[nomagic]
241241predicate pointerAddInstructionHasBounds (
242242 PointerAddInstruction pai , DataFlow:: Node sink1 , DataFlow:: Node sink2 , int delta
243243) {
244+ InterestingPointerAddInstruction:: isInteresting ( pragma [ only_bind_into ] ( pai ) ) and
244245 exists ( Instruction right , Instruction instr2 |
245246 pai .getRight ( ) = right and
246247 pai .getLeft ( ) = sink1 .asInstruction ( ) and
@@ -251,6 +252,29 @@ predicate pointerAddInstructionHasBounds(
251252 )
252253}
253254
255+ module InterestingPointerAddInstruction {
256+ private module PointerAddInstructionConfig implements DataFlow:: ConfigSig {
257+ predicate isSource ( DataFlow:: Node source ) {
258+ // The sources is the same as in the sources for the second
259+ // projection in the `AllocToInvalidPointerConfig` module.
260+ hasSize ( source .asConvertedExpr ( ) , _, _)
261+ }
262+
263+ predicate isSink ( DataFlow:: Node sink ) {
264+ sink .asInstruction ( ) = any ( PointerAddInstruction pai ) .getLeft ( )
265+ }
266+ }
267+
268+ private import DataFlow:: Global< PointerAddInstructionConfig >
269+
270+ predicate isInteresting ( PointerAddInstruction pai ) {
271+ exists ( DataFlow:: Node n |
272+ n .asInstruction ( ) = pai .getLeft ( ) and
273+ flowTo ( n )
274+ )
275+ }
276+ }
277+
254278/**
255279 * Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
256280 * left operand of the pointer-arithmetic operation.
0 commit comments