@@ -211,10 +211,17 @@ private predicate fieldStoreStepNoChi(Node node1, FieldContent f, PostUpdateNode
211211 )
212212}
213213
214+ private FieldAddressInstruction getFieldInstruction ( Instruction instr ) {
215+ result = instr or
216+ result = instr .( CopyValueInstruction ) .getUnary ( )
217+ }
218+
214219pragma [ noinline]
215- private predicate getWrittenField ( StoreInstruction store , Field f , Class c ) {
220+ private predicate getWrittenField ( Instruction instr , Field f , Class c ) {
216221 exists ( FieldAddressInstruction fa |
217- fa = store .getDestinationAddress ( ) and
222+ fa =
223+ getFieldInstruction ( [ instr .( StoreInstruction ) .getDestinationAddress ( ) ,
224+ instr .( WriteSideEffectInstruction ) .getDestinationAddress ( ) ] ) and
218225 f = fa .getField ( ) and
219226 c = f .getDeclaringType ( )
220227 )
@@ -265,7 +272,23 @@ private predicate arrayStoreStepChi(Node node1, ArrayContent a, PostUpdateNode n
265272predicate storeStep ( Node node1 , Content f , PostUpdateNode node2 ) {
266273 fieldStoreStepNoChi ( node1 , f , node2 ) or
267274 fieldStoreStepChi ( node1 , f , node2 ) or
268- arrayStoreStepChi ( node1 , f , node2 )
275+ arrayStoreStepChi ( node1 , f , node2 ) or
276+ fieldStoreStepAfterArraySuppression ( node1 , f , node2 )
277+ }
278+
279+ // This predicate pushes the correct `FieldContent` onto the access path when the
280+ // `suppressArrayRead` predicate has popped off an `ArrayContent`.
281+ private predicate fieldStoreStepAfterArraySuppression (
282+ Node node1 , FieldContent f , PostUpdateNode node2
283+ ) {
284+ exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi , Class c |
285+ not chi .isResultConflated ( ) and
286+ node1 .asInstruction ( ) = chi and
287+ node2 .asInstruction ( ) = chi and
288+ chi .getPartial ( ) = write and
289+ getWrittenField ( write , f .getAField ( ) , c ) and
290+ f .hasOffset ( c , _, _)
291+ )
269292}
270293
271294bindingset [ result , i]
@@ -302,11 +325,88 @@ private predicate fieldReadStep(Node node1, FieldContent f, Node node2) {
302325 )
303326}
304327
328+ /**
329+ * When a store step happens in a function that looks like an array write such as:
330+ * ```cpp
331+ * void f(int* pa) {
332+ * pa = source();
333+ * }
334+ * ```
335+ * it can be a write to an array, but it can also happen that `f` is called as `f(&a.x)`. If that is
336+ * the case, the `ArrayContent` that was written by the call to `f` should be popped off the access
337+ * path, and a `FieldContent` containing `x` should be pushed instead.
338+ * So this case pops `ArrayContent` off the access path, and the `fieldStoreStepAfterArraySuppression`
339+ * predicate in `storeStep` ensures that we push the right `FieldContent` onto the access path.
340+ */
341+ predicate suppressArrayRead ( Node node1 , ArrayContent a , Node node2 ) {
342+ a = TArrayContent ( ) and
343+ exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi |
344+ node1 .asInstruction ( ) = write and
345+ node2 .asInstruction ( ) = chi and
346+ chi .getPartial ( ) = write and
347+ getWrittenField ( write , _, _)
348+ )
349+ }
350+
351+ private class ArrayToPointerConvertInstruction extends ConvertInstruction {
352+ ArrayToPointerConvertInstruction ( ) {
353+ this .getUnary ( ) .getResultType ( ) instanceof ArrayType and
354+ this .getResultType ( ) instanceof PointerType
355+ }
356+ }
357+
358+ private Instruction skipOneCopyValueInstruction ( Instruction instr ) {
359+ not instr instanceof CopyValueInstruction and result = instr
360+ or
361+ result = instr .( CopyValueInstruction ) .getUnary ( )
362+ }
363+
364+ private Instruction skipCopyValueInstructions ( Instruction instr ) {
365+ result = skipOneCopyValueInstruction * ( instr ) and not result instanceof CopyValueInstruction
366+ }
367+
305368private predicate arrayReadStep ( Node node1 , ArrayContent a , Node node2 ) {
306369 a = TArrayContent ( ) and
307- exists ( LoadInstruction load |
370+ // Explicit dereferences such as `*p` or `p[i]` where `p` is a pointer or array.
371+ exists ( LoadInstruction load , Instruction address |
372+ load .getSourceValueOperand ( ) .isDefinitionInexact ( ) and
308373 node1 .asInstruction ( ) = load .getSourceValueOperand ( ) .getAnyDef ( ) and
309- load = node2 .asInstruction ( )
374+ load = node2 .asInstruction ( ) and
375+ address = skipCopyValueInstructions ( load .getSourceAddress ( ) ) and
376+ (
377+ address instanceof LoadInstruction or
378+ address instanceof ArrayToPointerConvertInstruction or
379+ address instanceof PointerOffsetInstruction
380+ )
381+ )
382+ }
383+
384+ /**
385+ * In cases such as:
386+ * ```cpp
387+ * void f(int* pa) {
388+ * *pa = source();
389+ * }
390+ * ...
391+ * int x;
392+ * f(&x);
393+ * use(x);
394+ * ```
395+ * the load on `x` in `use(x)` will exactly overlap with its definition (in this case the definition
396+ * is a `BufferMayWriteSideEffect`). This predicate pops the `ArrayContent` (pushed by the store in `f`)
397+ * from the access path.
398+ */
399+ private predicate exactReadStep ( Node node1 , ArrayContent a , Node node2 ) {
400+ a = TArrayContent ( ) and
401+ exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi |
402+ not chi .isResultConflated ( ) and
403+ chi .getPartial ( ) = write and
404+ node1 .asInstruction ( ) = write and
405+ node2 .asInstruction ( ) = chi and
406+ // To distinquish this case from the `arrayReadStep` case we require that the entire variable was
407+ // overwritten by the `BufferMayWriteSideEffectInstruction` (i.e., there is a load that reads the
408+ // entire variable).
409+ exists ( LoadInstruction load | load .getSourceValue ( ) = chi )
310410 )
311411}
312412
@@ -317,7 +417,9 @@ private predicate arrayReadStep(Node node1, ArrayContent a, Node node2) {
317417 */
318418predicate readStep ( Node node1 , Content f , Node node2 ) {
319419 fieldReadStep ( node1 , f , node2 ) or
320- arrayReadStep ( node1 , f , node2 )
420+ arrayReadStep ( node1 , f , node2 ) or
421+ exactReadStep ( node1 , f , node2 ) or
422+ suppressArrayRead ( node1 , f , node2 )
321423}
322424
323425/**
0 commit comments