@@ -118,6 +118,8 @@ module ControlFlow {
118118 /** Gets the left-hand side of this write. */
119119 IR:: WriteTarget getLhs ( ) { result = super .getLhs ( ) }
120120
121+ private predicate isInitialization ( ) { super .isInitialization ( ) }
122+
121123 /** Gets the right-hand side of this write. */
122124 DataFlow:: Node getRhs ( ) { super .getRhs ( ) = result .asInstruction ( ) }
123125
@@ -134,13 +136,20 @@ module ControlFlow {
134136 * Holds if this node sets the value of field `f` on `base` (or its implicit dereference) to
135137 * `rhs`.
136138 *
137- * For example, for the assignment `x.width = newWidth`, `base` is either the data-flow node
138- * corresponding to `x` or (if `x` is a pointer) the data-flow node corresponding to the
139- * implicit dereference `*x`, `f` is the field referenced by `width`, and `rhs` is the data-flow
140- * node corresponding to `newWidth`.
139+ * For example, for the assignment `x.width = newWidth`, `base` is the post-update node of
140+ * either the data-flow node corresponding to `x` or (if `x` is a pointer) the data-flow node
141+ * corresponding to the implicit dereference `*x`, `f` is the field referenced by `width`, and
142+ * `rhs` is the data-flow node corresponding to `newWidth`. If this `WriteNode` is a struct
143+ * initialization then there is no need for a post-update node and `base` is the struct literal
144+ * being initialized.
141145 */
142146 predicate writesField ( DataFlow:: Node base , Field f , DataFlow:: Node rhs ) {
143- this .writesFieldInsn ( base .asInstruction ( ) , f , rhs .asInstruction ( ) )
147+ exists ( DataFlow:: Node b | this .writesFieldInsn ( b .asInstruction ( ) , f , rhs .asInstruction ( ) ) |
148+ this .isInitialization ( ) and base = b
149+ or
150+ not this .isInitialization ( ) and
151+ b = base .( DataFlow:: PostUpdateNode ) .getPreUpdateNode ( )
152+ )
144153 }
145154
146155 private predicate writesFieldInsn ( IR:: Instruction base , Field f , IR:: Instruction rhs ) {
@@ -158,13 +167,22 @@ module ControlFlow {
158167 * Holds if this node sets the value of element `index` on `base` (or its implicit dereference)
159168 * to `rhs`.
160169 *
161- * For example, for the assignment `xs[i] = v`, `base` is either the data-flow node
162- * corresponding to `xs` or (if `xs` is a pointer) the data-flow node corresponding to the
163- * implicit dereference `*xs`, `index` is the data-flow node corresponding to `i`, and `rhs`
164- * is the data-flow node corresponding to `base`.
170+ * For example, for the assignment `xs[i] = v`, `base` is the post-update node of the data-flow
171+ * node corresponding to `xs` or (if `xs` is a pointer) the implicit dereference `*xs`, `index`
172+ * is the data-flow node corresponding to `i`, and `rhs` is the data-flow node corresponding to
173+ * `base`. If this `WriteNode` corresponds to the initialization of an array/slice/map then
174+ * there is no need for a post-update node and `base` is the array/slice/map literal being
175+ * initialized.
165176 */
166177 predicate writesElement ( DataFlow:: Node base , DataFlow:: Node index , DataFlow:: Node rhs ) {
167- this .writesElementInsn ( base .asInstruction ( ) , index .asInstruction ( ) , rhs .asInstruction ( ) )
178+ exists ( DataFlow:: Node b |
179+ this .writesElementInsn ( b .asInstruction ( ) , index .asInstruction ( ) , rhs .asInstruction ( ) )
180+ |
181+ this .isInitialization ( ) and base = b
182+ or
183+ not this .isInitialization ( ) and
184+ b = base .( DataFlow:: PostUpdateNode ) .getPreUpdateNode ( )
185+ )
168186 }
169187
170188 private predicate writesElementInsn (
@@ -184,7 +202,7 @@ module ControlFlow {
184202 * Holds if this node sets any field or element of `base` to `rhs`.
185203 */
186204 predicate writesComponent ( DataFlow:: Node base , DataFlow:: Node rhs ) {
187- this .writesComponentInstruction ( base . asInstruction ( ) , rhs . asInstruction ( ) )
205+ this .writesElement ( base , _ , rhs ) or this . writesField ( base , _ , rhs )
188206 }
189207
190208 /**
0 commit comments