@@ -185,16 +185,24 @@ class OperandNode extends Node, TOperandNode {
185185 override string toString ( ) { result = this .getOperand ( ) .toString ( ) }
186186}
187187
188+ /** An abstract class that defines conversion-like instructions. */
188189abstract private class SkippableInstruction extends Instruction {
189190 abstract Instruction getSourceInstruction ( ) ;
190191}
191192
193+ /**
194+ * Gets the instruction that is propaged through a non-empty sequence of conversion-like instructions.
195+ */
192196private Instruction skipSkippableInstructionsRec ( SkippableInstruction skip ) {
193197 result = skip .getSourceInstruction ( ) and not result instanceof SkippableInstruction
194198 or
195199 result = skipSkippableInstructionsRec ( skip .getSourceInstruction ( ) )
196200}
197201
202+ /**
203+ * Gets the instruction that is propagated through a (possibly empty) sequence of conversion-like
204+ * instructions.
205+ */
198206private Instruction skipSkippableInstructions ( Instruction instr ) {
199207 result = instr and not result instanceof SkippableInstruction
200208 or
@@ -228,8 +236,16 @@ FieldNode getFieldNodeForFieldInstruction(Instruction instr) {
228236}
229237
230238/**
231- * INTERNAL: do not use. A `FieldNode` represents the state of an object after modifying one
232- * of its fields.
239+ * INTERNAL: do not use. A `FieldNode` represents the state of a field before any partial definitions
240+ * of the field. For instance, in the snippet:
241+ * ```cpp
242+ * struct A { int b, c; };
243+ * // ...
244+ * A a;
245+ * f(a.b.c);
246+ * ```
247+ * there are two `FieldNode`s: one corresponding to `c`, and one corresponding to `b`. Similarly,
248+ * in `a.b.c = x` there are two `FieldNode`s: one for `c` and one for `b`.
233249 */
234250class FieldNode extends Node , TFieldNode {
235251 FieldAddressInstruction field ;
@@ -272,10 +288,9 @@ class FieldNode extends Node, TFieldNode {
272288}
273289
274290/**
275- * INTERNAL: do not use. A `FieldNode` represents the state of an object after modifying one
276- * of its fields.
291+ * INTERNAL: do not use. A partial definition of a `FieldNode`.
277292 */
278- class PostUpdateFieldNode extends PartialDefinition {
293+ class PartialFieldDefinition extends PartialDefinition {
279294 override FieldNode node ;
280295
281296 override FieldNode getPreUpdateNode ( ) { result = node }
@@ -435,6 +450,18 @@ abstract class PostUpdateNode extends Node {
435450 override Location getLocation ( ) { result = getPreUpdateNode ( ) .getLocation ( ) }
436451}
437452
453+ /**
454+ * A partial definition of a node. A partial definition that target arrays or pointers is attached to
455+ * an `InstructionNode` (specifially, to the `ChiInstruction` that follows the `StoreInstruction`), and
456+ * a partial update that targets a `FieldNode` is attached to the `FieldNode`.
457+ *s
458+ * The pre update node of a partial definition of a `FieldNode` is the `FieldNode` itself. This ensures
459+ * that the dataflow library's reverse read mechanism builds up the correct access path for nested
460+ * fields.
461+ * For instance, in `a.b.c = x` there is a partial definition for `c` (let's call it `post[c]`) and a
462+ * partial definition for `b` (let's call it `post[b]`), and there is a read step from `b` to `c`
463+ * (using `instrToFieldNodeReadStep`), so there is a store step from `post[c]` to `post[b]`.
464+ */
438465private newtype TPartialDefinition =
439466 MkPartialDefinition ( Node node ) {
440467 isPointerStoreNode ( node , _, _) or
@@ -681,7 +708,7 @@ predicate localFlowStep(Node nodeFrom, Node nodeTo) { simpleLocalFlowStep(nodeFr
681708private predicate flowOutOfPostUpdate ( PartialDefinitionNode nodeFrom , Node nodeTo ) {
682709 // flow from the "outermost" field to the `ChiInstruction`, or `StoreInstruction`
683710 // if no `ChiInstruction` exists.
684- exists ( AddressOperand addressOperand , PostUpdateFieldNode pd |
711+ exists ( AddressOperand addressOperand , PartialFieldDefinition pd |
685712 pd = nodeFrom .getPartialDefinition ( ) and
686713 not exists ( pd .getPreUpdateNode ( ) .getObjectNode ( ) ) and
687714 pd .getPreUpdateNode ( ) .getNextNode * ( ) = getFieldNodeForFieldInstruction ( addressOperand .getDef ( ) ) and
@@ -707,31 +734,38 @@ private predicate flowOutOfPostUpdate(PartialDefinitionNode nodeFrom, Node nodeT
707734 )
708735}
709736
710- private predicate flowIntoReadNode ( Node nodeFrom , Node nodeTo ) {
711- // flow from the "innermost" field to the load of that field.
712- exists ( FieldNode fieldNode | nodeTo = fieldNode |
713- not exists ( fieldNode .getObjectNode ( ) ) and
714- (
715- exists ( LoadInstruction load |
716- fieldNode .getNextNode * ( ) = getFieldNodeForFieldInstruction ( load .getSourceAddress ( ) ) and
717- nodeFrom .asInstruction ( ) = load .getSourceValueOperand ( ) .getAnyDef ( )
718- )
719- or
720- // We need this to make stores look like loads for the dataflow library. So when there's a store
721- // of the form x->y = z we need to make the field node corresponding to y look like it's reading
722- // from the memory of x.
723- exists ( StoreInstruction store , ChiInstruction chi |
724- chi .getPartial ( ) = store and
725- fieldNode .getNextNode * ( ) = getFieldNodeForFieldInstruction ( store .getDestinationAddress ( ) ) and
726- nodeFrom .asInstruction ( ) = chi .getTotal ( )
727- )
728- or
729- exists ( ReadSideEffectInstruction read |
730- fieldNode .getNextNode * ( ) = getFieldNodeForFieldInstruction ( read .getArgumentDef ( ) ) and
731- nodeFrom .asOperand ( ) = read .getSideEffectOperand ( )
732- )
737+ /**
738+ * Gets the `FieldNode` corresponding to the outermost field that is used to compute `address`.
739+ */
740+ private FieldNode getOutermostFieldNode ( Instruction address ) {
741+ not exists ( result .getObjectNode ( ) ) and
742+ result .getNextNode * ( ) = getFieldNodeForFieldInstruction ( address )
743+ }
744+
745+ private predicate flowIntoReadNode ( Node nodeFrom , FieldNode nodeTo ) {
746+ // flow from the memory of a load to the "outermost" field of that load.
747+ not nodeFrom .asInstruction ( ) .isResultConflated ( ) and
748+ (
749+ exists ( LoadInstruction load |
750+ nodeTo = getOutermostFieldNode ( load .getSourceAddress ( ) ) and
751+ nodeFrom .asInstruction ( ) = load .getSourceValueOperand ( ) .getAnyDef ( )
752+ )
753+ or
754+ // We need this to make stores look like loads for the dataflow library. So when there's a store
755+ // of the form x->y = z we need to make the field node corresponding to y look like it's reading
756+ // from the memory of x.
757+ exists ( StoreInstruction store , ChiInstruction chi |
758+ chi .getPartial ( ) = store and
759+ nodeTo = getOutermostFieldNode ( store .getDestinationAddress ( ) ) and
760+ nodeFrom .asInstruction ( ) = chi .getTotal ( )
733761 )
734762 )
763+ or
764+ exists ( ReadSideEffectInstruction read |
765+ not read .getSideEffectOperand ( ) .getAnyDef ( ) .isResultConflated ( ) and
766+ nodeTo = getOutermostFieldNode ( read .getArgumentDef ( ) ) and
767+ nodeFrom .asOperand ( ) = read .getSideEffectOperand ( )
768+ )
735769}
736770
737771/**
0 commit comments