@@ -143,23 +143,23 @@ private predicate hasCapturedRead(Variable v, Cfg::CfgScope scope) {
143
143
}
144
144
145
145
/**
146
- * Holds if `v` is written inside basic block `bb`, which is in the immediate
147
- * outer scope of `scope`.
146
+ * Holds if `v` is written inside basic block `bb` at index `i` , which is in
147
+ * the immediate outer scope of `scope`.
148
148
*/
149
149
pragma [ noinline]
150
- private predicate variableWriteInOuterScope ( Cfg:: BasicBlock bb , LocalVariable v , Cfg:: CfgScope scope ) {
151
- SsaInput:: variableWrite ( bb , _, v , _) and
150
+ private predicate variableWriteInOuterScope (
151
+ Cfg:: BasicBlock bb , int i , LocalVariable v , Cfg:: CfgScope scope
152
+ ) {
153
+ SsaInput:: variableWrite ( bb , i , v , _) and
152
154
scope .getOuterCfgScope ( ) = bb .getScope ( )
153
155
}
154
156
155
157
pragma [ noinline]
156
- private predicate proceedsVariableWriteWithCapturedRead (
157
- Cfg:: BasicBlock bb , LocalVariable v , Cfg:: CfgScope scope
158
+ private predicate hasVariableWriteWithCapturedRead (
159
+ Cfg:: BasicBlock bb , int i , LocalVariable v , Cfg:: CfgScope scope
158
160
) {
159
161
hasCapturedRead ( v , scope ) and
160
- variableWriteInOuterScope ( bb , v , scope )
161
- or
162
- proceedsVariableWriteWithCapturedRead ( bb .getAPredecessor ( ) , v , scope )
162
+ variableWriteInOuterScope ( bb , i , v , scope )
163
163
}
164
164
165
165
/**
@@ -168,7 +168,10 @@ private predicate proceedsVariableWriteWithCapturedRead(
168
168
*/
169
169
private predicate capturedCallRead ( CallCfgNode call , Cfg:: BasicBlock bb , int i , LocalVariable v ) {
170
170
exists ( Cfg:: CfgScope scope |
171
- proceedsVariableWriteWithCapturedRead ( bb , v , scope ) and
171
+ (
172
+ hasVariableWriteWithCapturedRead ( bb , any ( int j | j < i ) , v , scope ) or
173
+ hasVariableWriteWithCapturedRead ( bb .getAPredecessor + ( ) , _, v , scope )
174
+ ) and
172
175
call = bb .getNode ( i )
173
176
|
174
177
// If the read happens inside a block, we restrict to the call that
@@ -199,23 +202,23 @@ private predicate hasCapturedWrite(Variable v, Cfg::CfgScope scope) {
199
202
}
200
203
201
204
/**
202
- * Holds if `v` is read inside basic block `bb`, which is in the immediate
203
- * outer scope of `scope`.
205
+ * Holds if `v` is read inside basic block `bb` at index `i` , which is in the
206
+ * immediate outer scope of `scope`.
204
207
*/
205
208
pragma [ noinline]
206
209
private predicate variableReadActualInOuterScope (
207
- Cfg:: BasicBlock bb , LocalVariable v , Cfg:: CfgScope scope
210
+ Cfg:: BasicBlock bb , int i , LocalVariable v , Cfg:: CfgScope scope
208
211
) {
209
- variableReadActual ( bb , _ , v ) and
212
+ variableReadActual ( bb , i , v ) and
210
213
bb .getScope ( ) = scope .getOuterCfgScope ( )
211
214
}
212
215
213
216
pragma [ noinline]
214
217
private predicate hasVariableReadWithCapturedWrite (
215
- Cfg:: BasicBlock bb , LocalVariable v , Cfg:: CfgScope scope
218
+ Cfg:: BasicBlock bb , int i , LocalVariable v , Cfg:: CfgScope scope
216
219
) {
217
220
hasCapturedWrite ( v , scope ) and
218
- variableReadActualInOuterScope ( bb , v , scope )
221
+ variableReadActualInOuterScope ( bb , i , v , scope )
219
222
}
220
223
221
224
pragma [ noinline]
@@ -324,7 +327,11 @@ private module Cached {
324
327
cached
325
328
predicate capturedCallWrite ( CallCfgNode call , Cfg:: BasicBlock bb , int i , LocalVariable v ) {
326
329
exists ( Cfg:: CfgScope scope |
327
- hasVariableReadWithCapturedWrite ( bb .getASuccessor * ( ) , v , scope ) and
330
+ (
331
+ hasVariableReadWithCapturedWrite ( bb , any ( int j | j > i ) , v , scope )
332
+ or
333
+ hasVariableReadWithCapturedWrite ( bb .getASuccessor + ( ) , _, v , scope )
334
+ ) and
328
335
call = bb .getNode ( i )
329
336
|
330
337
// If the write happens inside a block, we restrict to the call that
0 commit comments