@@ -357,37 +357,48 @@ private class ArrayToPointerConvertInstruction extends ConvertInstruction {
357357
358358private predicate arrayReadStep ( Node node1 , ArrayContent a , Node node2 ) {
359359 a = TArrayContent ( ) and
360- (
361- // In cases such as:
362- // ```cpp
363- // void f(int* pa) {
364- // *pa = source();
365- // }
366- // ...
367- // int x;
368- // f(&x);
369- // use(x);
370- // ```
371- // the load on `x` in `use(x)` will exactly overlap with its definition (in this case the definition
372- // is a `BufferMayWriteSideEffect`).
373- exists ( LoadInstruction load |
374- node1 .asInstruction ( ) = load .getSourceValue ( ) and
375- load = node2 .asInstruction ( )
376- )
377- or
378- // Explicit dereferences such as `*p` or `p[i]` where `p` is a pointer or array.
379- exists ( LoadInstruction load |
380- node1 .asInstruction ( ) = load .getSourceValueOperand ( ) .getAnyDef ( ) and
381- load = node2 .asInstruction ( ) and
382- (
383- load .getSourceAddress ( ) instanceof LoadInstruction or
384- load .getSourceAddress ( ) instanceof ArrayToPointerConvertInstruction or
385- load .getSourceAddress ( ) instanceof PointerAddInstruction
386- )
360+ // Explicit dereferences such as `*p` or `p[i]` where `p` is a pointer or array.
361+ exists ( LoadInstruction load |
362+ load .getSourceValueOperand ( ) .isDefinitionInexact ( ) and
363+ node1 .asInstruction ( ) = load .getSourceValueOperand ( ) .getAnyDef ( ) and
364+ load = node2 .asInstruction ( ) and
365+ (
366+ load .getSourceAddress ( ) instanceof LoadInstruction or
367+ load .getSourceAddress ( ) instanceof ArrayToPointerConvertInstruction or
368+ load .getSourceAddress ( ) instanceof PointerAddInstruction
387369 )
388370 )
389371}
390372
373+ /**
374+ * In cases such as:
375+ * ```cpp
376+ * void f(int* pa) {
377+ * *pa = source();
378+ * }
379+ * ...
380+ * int x;
381+ * f(&x);
382+ * use(x);
383+ * ```
384+ * the load on `x` in `use(x)` will exactly overlap with its definition (in this case the definition
385+ * is a `BufferMayWriteSideEffect`). This predicate pops the `ArrayContent` (pushed by the store in `f`)
386+ * from the access path.
387+ */
388+ private predicate exactReadStep ( Node node1 , ArrayContent a , Node node2 ) {
389+ a = TArrayContent ( ) and
390+ exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi |
391+ not chi .isResultConflated ( ) and
392+ chi .getPartial ( ) = write and
393+ node1 .asInstruction ( ) = write and
394+ node2 .asInstruction ( ) = chi and
395+ // To distinquish this case from the `arrayReadStep` case we require that the entire variable was
396+ // overwritten by the `BufferMayWriteSideEffectInstruction` (i.e., there is a load that reads the
397+ // entire variable).
398+ exists ( LoadInstruction load | load .getSourceValue ( ) = chi )
399+ )
400+ }
401+
391402/**
392403 * Holds if data can flow from `node1` to `node2` via a read of `f`.
393404 * Thus, `node1` references an object with a field `f` whose value ends up in
@@ -396,6 +407,7 @@ private predicate arrayReadStep(Node node1, ArrayContent a, Node node2) {
396407predicate readStep ( Node node1 , Content f , Node node2 ) {
397408 fieldReadStep ( node1 , f , node2 ) or
398409 arrayReadStep ( node1 , f , node2 ) or
410+ exactReadStep ( node1 , f , node2 ) or
399411 suppressArrayRead ( node1 , f , node2 )
400412}
401413
0 commit comments