@@ -391,13 +391,14 @@ module Flow<InputSig Input> implements OutputSig<Input> {
391
391
msg = "ClosureExpr has no body" and not ce .hasBody ( _)
392
392
}
393
393
394
- query predicate closureAliasMustBeLocal ( ClosureExpr ce , Expr access , string msg ) {
394
+ query predicate closureAliasMustBeInSameScope ( ClosureExpr ce , Expr access , string msg ) {
395
395
exists ( BasicBlock bb1 , BasicBlock bb2 |
396
396
ce .hasAliasedAccess ( access ) and
397
397
ce .hasCfgNode ( bb1 , _) and
398
398
access .hasCfgNode ( bb2 , _) and
399
- bb1 .getEnclosingCallable ( ) != bb2 .getEnclosingCallable ( ) and
400
- msg = "ClosureExpr has non-local alias - these are ignored"
399
+ not bb1 .getEnclosingCallable ( ) = callableGetEnclosingCallable * ( bb2 .getEnclosingCallable ( ) ) and
400
+ msg =
401
+ "ClosureExpr has an alias outside the scope of its enclosing callable - these are ignored"
401
402
)
402
403
}
403
404
@@ -440,7 +441,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
440
441
n = strictcount ( VariableWrite vw | localWriteStep ( vw , msg ) ) or
441
442
n = strictcount ( VariableRead vr | uniqueReadVariable ( vr , msg ) ) or
442
443
n = strictcount ( ClosureExpr ce | closureMustHaveBody ( ce , msg ) ) or
443
- n = strictcount ( ClosureExpr ce , Expr access | closureAliasMustBeLocal ( ce , access , msg ) ) or
444
+ n = strictcount ( ClosureExpr ce , Expr access | closureAliasMustBeInSameScope ( ce , access , msg ) ) or
444
445
n = strictcount ( CapturedVariable v , Callable c | variableAccessAstNesting ( v , c , msg ) ) or
445
446
n = strictcount ( Callable c | uniqueCallableLocation ( c , msg ) )
446
447
}
@@ -518,10 +519,39 @@ module Flow<InputSig Input> implements OutputSig<Input> {
518
519
}
519
520
520
521
/** Gets the enclosing callable of `ce`. */
521
- private Callable closureExprGetCallable ( ClosureExpr ce ) {
522
+ private Callable closureExprGetEnclosingCallable ( ClosureExpr ce ) {
522
523
exists ( BasicBlock bb | ce .hasCfgNode ( bb , _) and result = bb .getEnclosingCallable ( ) )
523
524
}
524
525
526
+ /** Gets the enclosing callable of `inner`. */
527
+ pragma [ nomagic]
528
+ private Callable callableGetEnclosingCallable ( Callable inner ) {
529
+ exists ( ClosureExpr closure |
530
+ closure .hasBody ( inner ) and
531
+ result = closureExprGetEnclosingCallable ( closure )
532
+ )
533
+ }
534
+
535
+ /**
536
+ * Gets a callable that contains `ce`, or a reference to `ce` into which `ce` could be inlined without
537
+ * bringing any variables out of scope.
538
+ *
539
+ * If `ce` was to be inlined into that reference, the resulting callable
540
+ * would become the enclosing callable, and thus capture the same variables as `ce`.
541
+ * In some sense, we model captured aliases as if this inlining has happened.
542
+ */
543
+ private Callable closureExprGetAReferencingCallable ( ClosureExpr ce ) {
544
+ result = closureExprGetEnclosingCallable ( ce )
545
+ or
546
+ exists ( Expr expr , BasicBlock bb |
547
+ ce .hasAliasedAccess ( expr ) and
548
+ expr .hasCfgNode ( bb , _) and
549
+ result = bb .getEnclosingCallable ( ) and
550
+ // The reference to `ce` is allowed to occur in a more deeply nested context
551
+ closureExprGetEnclosingCallable ( ce ) = callableGetEnclosingCallable * ( result )
552
+ )
553
+ }
554
+
525
555
/**
526
556
* Holds if `v` is available in `c` through capture. This can either be due to
527
557
* an explicit variable reference or through the construction of a closure
@@ -534,7 +564,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
534
564
)
535
565
or
536
566
exists ( ClosureExpr ce |
537
- c = closureExprGetCallable ( ce ) and
567
+ c = closureExprGetAReferencingCallable ( ce ) and
538
568
closureCaptures ( ce , v ) and
539
569
c != v .getCallable ( )
540
570
)
@@ -562,15 +592,15 @@ module Flow<InputSig Input> implements OutputSig<Input> {
562
592
563
593
/**
564
594
* Holds if `access` is a reference to `ce` evaluated in the `i`th node of `bb`.
565
- * The reference is restricted to be in the same callable as `ce` as a
595
+ * The reference is restricted to be nested within the same callable as `ce` as a
566
596
* precaution, even though this is expected to hold for all the given aliased
567
597
* accesses.
568
598
*/
569
- private predicate localClosureAccess ( ClosureExpr ce , Expr access , BasicBlock bb , int i ) {
599
+ private predicate localOrNestedClosureAccess ( ClosureExpr ce , Expr access , BasicBlock bb , int i ) {
570
600
ce .hasAliasedAccess ( access ) and
571
601
access .hasCfgNode ( bb , i ) and
572
602
pragma [ only_bind_out ] ( bb .getEnclosingCallable ( ) ) =
573
- pragma [ only_bind_out ] ( closureExprGetCallable ( ce ) )
603
+ pragma [ only_bind_out ] ( closureExprGetAReferencingCallable ( ce ) )
574
604
}
575
605
576
606
/**
@@ -587,7 +617,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
587
617
exists ( ClosureExpr ce | closureCaptures ( ce , v ) |
588
618
ce .hasCfgNode ( bb , i ) and ce = closure
589
619
or
590
- localClosureAccess ( ce , closure , bb , i )
620
+ localOrNestedClosureAccess ( ce , closure , bb , i )
591
621
) and
592
622
if v .getCallable ( ) != bb .getEnclosingCallable ( ) then topScope = false else topScope = true
593
623
}
0 commit comments