@@ -122,6 +122,47 @@ private module Cached {
122122 FlowSummaryImpl:: Private:: Steps:: summaryJumpStep ( n1 , n2 )
123123 }
124124
125+ bindingset [ store]
126+ pragma [ inline_late]
127+ private predicate nodeHasInstructionLate ( Node node , StoreInstruction store , int indirectionIndex ) {
128+ nodeHasInstruction ( node , store , indirectionIndex )
129+ }
130+
131+ pragma [ nomagic]
132+ private predicate storeStepSource (
133+ Operand fieldAddress , int contentIndirectionIndex , Node node , boolean certain
134+ ) {
135+ exists ( int indirectionIndex , int numberOfLoads , StoreInstruction store |
136+ nodeHasInstructionLate ( node , store , indirectionIndex ) and
137+ numberOfLoadsFromOperand ( fieldAddress , store .getDestinationAddressOperand ( ) , numberOfLoads ,
138+ certain ) and
139+ contentIndirectionIndex = 1 + indirectionIndex + numberOfLoads
140+ )
141+ }
142+
143+ pragma [ nomagic]
144+ private predicate hasFieldAddressAndField ( Field f , PostFieldUpdateNode pfu , Operand fieldAddress ) {
145+ pfu .getIndirectionIndex ( ) = 1 and
146+ pfu .getUpdatedField ( ) = f and
147+ pfu .getFieldAddress ( ) = fieldAddress
148+ }
149+
150+ pragma [ nomagic]
151+ private predicate hasFieldAndIndirectionIndex ( Field f , int indirectionIndex , FieldContent fc ) {
152+ fc .getAField ( ) = f and
153+ fc .getIndirectionIndex ( ) = indirectionIndex
154+ }
155+
156+ pragma [ nomagic]
157+ private predicate storeStepTarget (
158+ Operand address , int indirectionIndex , PostFieldUpdateNode pfu , FieldContent fc
159+ ) {
160+ exists ( Field f |
161+ hasFieldAddressAndField ( f , pfu , address ) and
162+ hasFieldAndIndirectionIndex ( f , indirectionIndex , fc )
163+ )
164+ }
165+
125166 /**
126167 * Holds if data can flow from `node1` to `node2` via an assignment to `f`.
127168 * Thus, `node2` references an object with a field `f` that contains the
@@ -132,19 +173,9 @@ private module Cached {
132173 */
133174 cached
134175 predicate storeStepImpl ( Node node1 , Content c , Node node2 , boolean certain ) {
135- exists (
136- PostFieldUpdateNode postFieldUpdate , int indirectionIndex1 , int numberOfLoads ,
137- StoreInstruction store , FieldContent fc
138- |
139- postFieldUpdate = node2 and
140- fc = c and
141- nodeHasInstruction ( node1 , pragma [ only_bind_into ] ( store ) ,
142- pragma [ only_bind_into ] ( indirectionIndex1 ) ) and
143- postFieldUpdate .getIndirectionIndex ( ) = 1 and
144- numberOfLoadsFromOperand ( postFieldUpdate .getFieldAddress ( ) ,
145- store .getDestinationAddressOperand ( ) , numberOfLoads , certain ) and
146- fc .getAField ( ) = postFieldUpdate .getUpdatedField ( ) and
147- getIndirectionIndexLate ( fc ) = 1 + indirectionIndex1 + numberOfLoads
176+ exists ( Operand fieldAddress , int indirectionIndex |
177+ storeStepSource ( fieldAddress , indirectionIndex , node1 , certain ) and
178+ storeStepTarget ( fieldAddress , indirectionIndex , node2 , c )
148179 )
149180 or
150181 // models-as-data summarized flow
0 commit comments