@@ -140,13 +140,17 @@ module ControlFlow {
140140 * node corresponding to `newWidth`.
141141 */
142142 predicate writesField ( DataFlow:: Node base , Field f , DataFlow:: Node rhs ) {
143+ this .writesFieldInsn ( base .asInstruction ( ) , f , rhs .asInstruction ( ) )
144+ }
145+
146+ private predicate writesFieldInsn ( IR:: Instruction base , Field f , IR:: Instruction rhs ) {
143147 exists ( IR:: FieldTarget trg | trg = super .getLhs ( ) |
144148 (
145- trg .getBase ( ) = base . asInstruction ( ) or
146- trg .getBase ( ) = MkImplicitDeref ( base .asExpr ( ) )
149+ trg .getBase ( ) = base or
150+ trg .getBase ( ) = MkImplicitDeref ( base .( IR :: EvalInstruction ) . getExpr ( ) )
147151 ) and
148152 trg .getField ( ) = f and
149- super .getRhs ( ) = rhs . asInstruction ( )
153+ super .getRhs ( ) = rhs
150154 )
151155 }
152156
@@ -160,21 +164,34 @@ module ControlFlow {
160164 * is the data-flow node corresponding to `base`.
161165 */
162166 predicate writesElement ( DataFlow:: Node base , DataFlow:: Node index , DataFlow:: Node rhs ) {
167+ this .writesElementInsn ( base .asInstruction ( ) , index .asInstruction ( ) , rhs .asInstruction ( ) )
168+ }
169+
170+ private predicate writesElementInsn (
171+ IR:: Instruction base , IR:: Instruction index , IR:: Instruction rhs
172+ ) {
163173 exists ( IR:: ElementTarget trg | trg = super .getLhs ( ) |
164174 (
165- trg .getBase ( ) = base . asInstruction ( ) or
166- trg .getBase ( ) = MkImplicitDeref ( base .asExpr ( ) )
175+ trg .getBase ( ) = base or
176+ trg .getBase ( ) = MkImplicitDeref ( base .( IR :: EvalInstruction ) . getExpr ( ) )
167177 ) and
168- trg .getIndex ( ) = index . asInstruction ( ) and
169- super .getRhs ( ) = rhs . asInstruction ( )
178+ trg .getIndex ( ) = index and
179+ super .getRhs ( ) = rhs
170180 )
171181 }
172182
173183 /**
174184 * Holds if this node sets any field or element of `base` to `rhs`.
175185 */
176186 predicate writesComponent ( DataFlow:: Node base , DataFlow:: Node rhs ) {
177- this .writesElement ( base , _, rhs ) or this .writesField ( base , _, rhs )
187+ this .writesComponentInstruction ( base .asInstruction ( ) , rhs .asInstruction ( ) )
188+ }
189+
190+ /**
191+ * Holds if this node sets any field or element of `base` to `rhs`.
192+ */
193+ predicate writesComponentInstruction ( IR:: Instruction base , IR:: Instruction rhs ) {
194+ this .writesElementInsn ( base , _, rhs ) or this .writesFieldInsn ( base , _, rhs )
178195 }
179196 }
180197
0 commit comments