@@ -163,19 +163,46 @@ TGlobalAddress globalAddress(Instruction instr) {
163
163
result = globalAddress ( instr .( PointerOffsetInstruction ) .getLeft ( ) )
164
164
}
165
165
166
- /** Gets a `StoreInstruction` that may be executed after executing `store`. */
167
- pragma [ inline]
168
- StoreInstruction getAStoreStrictlyAfter ( StoreInstruction store ) {
169
- exists ( IRBlock block , int index1 , int index2 |
170
- block .getInstruction ( index1 ) = store and
171
- block .getInstruction ( index2 ) = result and
172
- index2 > index1
166
+ /**
167
+ * Gets a first `StoreInstruction` that writes to address `globalAddress` reachable
168
+ * from `block`.
169
+ */
170
+ StoreInstruction getFirstStore ( IRBlock block , TGlobalAddress globalAddress ) {
171
+ 1 = getStoreRank ( result , block , globalAddress )
172
+ or
173
+ not exists ( getStoreRank ( _, block , globalAddress ) ) and
174
+ result = getFirstStore ( block .getASuccessor ( ) , globalAddress )
175
+ }
176
+
177
+ /**
178
+ * Gets the rank of `store` in block `block` (i.e., a rank of `1` means that it is the
179
+ * first `store` to write to `globalAddress`, a rank of `2` means it's the second, etc.)
180
+ */
181
+ int getStoreRank ( StoreInstruction store , IRBlock block , TGlobalAddress globalAddress ) {
182
+ blockStoresToAddress ( block , _, store , globalAddress ) and
183
+ store =
184
+ rank [ result ] ( StoreInstruction anotherStore , int i |
185
+ blockStoresToAddress ( _, i , anotherStore , globalAddress )
186
+ |
187
+ anotherStore order by i
188
+ )
189
+ }
190
+
191
+ /**
192
+ * Gets a next subsequent `StoreInstruction` to write to `globalAddress`
193
+ * after `store` has done so.
194
+ */
195
+ StoreInstruction getANextStoreTo ( StoreInstruction store , TGlobalAddress globalAddress ) {
196
+ exists ( IRBlock block , int rnk |
197
+ rnk = getStoreRank ( store , block , globalAddress ) and
198
+ rnk + 1 = getStoreRank ( result , block , globalAddress )
173
199
)
174
200
or
175
- exists ( IRBlock block1 , IRBlock block2 |
176
- store .getBlock ( ) = block1 and
177
- result .getBlock ( ) = block2 and
178
- block1 .getASuccessor + ( ) = block2
201
+ exists ( IRBlock block , int rnk , IRBlock succ |
202
+ rnk = getStoreRank ( store , block , globalAddress ) and
203
+ not rnk + 1 = getStoreRank ( _, block , globalAddress ) and
204
+ succ = block .getASuccessor ( ) and
205
+ result = getFirstStore ( succ , globalAddress )
179
206
)
180
207
}
181
208
@@ -192,7 +219,7 @@ predicate stackAddressEscapes(
192
219
stackPointerFlowsToUse ( store .getSourceValue ( ) , vai )
193
220
) and
194
221
// Ensure there's no subsequent store that overrides the global address.
195
- not globalAddress = globalAddress ( getAStoreStrictlyAfter ( store ) . getDestinationAddress ( ) )
222
+ not exists ( getANextStoreTo ( store , globalAddress ) )
196
223
}
197
224
198
225
predicate blockStoresToAddress (
0 commit comments