@@ -143,23 +143,23 @@ private predicate hasCapturedRead(Variable v, Cfg::CfgScope scope) {
143143}
144144
145145/**
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`.
148148 */
149149pragma [ 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
152154 scope .getOuterCfgScope ( ) = bb .getScope ( )
153155}
154156
155157pragma [ 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
158160) {
159161 hasCapturedRead ( v , scope ) and
160- variableWriteInOuterScope ( bb , v , scope )
161- or
162- proceedsVariableWriteWithCapturedRead ( bb .getAPredecessor ( ) , v , scope )
162+ variableWriteInOuterScope ( bb , i , v , scope )
163163}
164164
165165/**
@@ -168,7 +168,10 @@ private predicate proceedsVariableWriteWithCapturedRead(
168168 */
169169private predicate capturedCallRead ( CallCfgNode call , Cfg:: BasicBlock bb , int i , LocalVariable v ) {
170170 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
172175 call = bb .getNode ( i )
173176 |
174177 // 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) {
199202}
200203
201204/**
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`.
204207 */
205208pragma [ noinline]
206209private predicate variableReadActualInOuterScope (
207- Cfg:: BasicBlock bb , LocalVariable v , Cfg:: CfgScope scope
210+ Cfg:: BasicBlock bb , int i , LocalVariable v , Cfg:: CfgScope scope
208211) {
209- variableReadActual ( bb , _ , v ) and
212+ variableReadActual ( bb , i , v ) and
210213 bb .getScope ( ) = scope .getOuterCfgScope ( )
211214}
212215
213216pragma [ noinline]
214217private predicate hasVariableReadWithCapturedWrite (
215- Cfg:: BasicBlock bb , LocalVariable v , Cfg:: CfgScope scope
218+ Cfg:: BasicBlock bb , int i , LocalVariable v , Cfg:: CfgScope scope
216219) {
217220 hasCapturedWrite ( v , scope ) and
218- variableReadActualInOuterScope ( bb , v , scope )
221+ variableReadActualInOuterScope ( bb , i , v , scope )
219222}
220223
221224pragma [ noinline]
@@ -324,7 +327,11 @@ private module Cached {
324327 cached
325328 predicate capturedCallWrite ( CallCfgNode call , Cfg:: BasicBlock bb , int i , LocalVariable v ) {
326329 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
328335 call = bb .getNode ( i )
329336 |
330337 // If the write happens inside a block, we restrict to the call that
0 commit comments