@@ -241,6 +241,7 @@ pragma[nomagic]
241
241
predicate pointerAddInstructionHasBounds (
242
242
PointerAddInstruction pai , DataFlow:: Node sink1 , DataFlow:: Node sink2 , int delta
243
243
) {
244
+ InterestingPointerAddInstruction:: isInteresting ( pragma [ only_bind_into ] ( pai ) ) and
244
245
exists ( Instruction right , Instruction instr2 |
245
246
pai .getRight ( ) = right and
246
247
pai .getLeft ( ) = sink1 .asInstruction ( ) and
@@ -251,6 +252,29 @@ predicate pointerAddInstructionHasBounds(
251
252
)
252
253
}
253
254
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
+
254
278
/**
255
279
* Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
256
280
* left operand of the pointer-arithmetic operation.
0 commit comments