@@ -391,6 +391,17 @@ 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 closureAliasMustBeInSameScope ( ClosureExpr ce , Expr access , string msg ) {
395
+ exists ( BasicBlock bb1 , BasicBlock bb2 |
396
+ ce .hasAliasedAccess ( access ) and
397
+ ce .hasCfgNode ( bb1 , _) and
398
+ access .hasCfgNode ( bb2 , _) and
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"
402
+ )
403
+ }
404
+
394
405
private predicate astClosureParent ( Callable closure , Callable parent ) {
395
406
exists ( ClosureExpr ce , BasicBlock bb |
396
407
ce .hasBody ( closure ) and ce .hasCfgNode ( bb , _) and parent = bb .getEnclosingCallable ( )
@@ -430,6 +441,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
430
441
n = strictcount ( VariableWrite vw | localWriteStep ( vw , msg ) ) or
431
442
n = strictcount ( VariableRead vr | uniqueReadVariable ( vr , msg ) ) or
432
443
n = strictcount ( ClosureExpr ce | closureMustHaveBody ( ce , msg ) ) or
444
+ n = strictcount ( ClosureExpr ce , Expr access | closureAliasMustBeInSameScope ( ce , access , msg ) ) or
433
445
n = strictcount ( CapturedVariable v , Callable c | variableAccessAstNesting ( v , c , msg ) ) or
434
446
n = strictcount ( Callable c | uniqueCallableLocation ( c , msg ) )
435
447
}
@@ -521,14 +533,16 @@ module Flow<InputSig Input> implements OutputSig<Input> {
521
533
}
522
534
523
535
/**
524
- * Gets a callable that contains a reference to `ce` into which `ce` could be inlined without
536
+ * Gets a callable that contains `ce`, or a reference to `ce` into which `ce` could be inlined without
525
537
* bringing any variables out of scope.
526
538
*
527
539
* If `ce` was to be inlined into that reference, the resulting callable
528
540
* would become the enclosing callable, and thus capture the same variables as `ce`.
529
541
* In some sense, we model captured aliases as if this inlining has happened.
530
542
*/
531
543
private Callable closureExprGetAReferencingCallable ( ClosureExpr ce ) {
544
+ result = closureExprGetEnclosingCallable ( ce )
545
+ or
532
546
exists ( Expr expr , BasicBlock bb |
533
547
ce .hasAliasedAccess ( expr ) and
534
548
expr .hasCfgNode ( bb , _) and
@@ -538,11 +552,6 @@ module Flow<InputSig Input> implements OutputSig<Input> {
538
552
)
539
553
}
540
554
541
- /** Gets a callable containing `ce` or one of its aliases. */
542
- private Callable closureExprGetCallable ( ClosureExpr ce ) {
543
- result = [ closureExprGetEnclosingCallable ( ce ) , closureExprGetAReferencingCallable ( ce ) ]
544
- }
545
-
546
555
/**
547
556
* Holds if `v` is available in `c` through capture. This can either be due to
548
557
* an explicit variable reference or through the construction of a closure
@@ -555,7 +564,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
555
564
)
556
565
or
557
566
exists ( ClosureExpr ce |
558
- c = closureExprGetCallable ( ce ) and
567
+ c = closureExprGetAReferencingCallable ( ce ) and
559
568
closureCaptures ( ce , v ) and
560
569
c != v .getCallable ( )
561
570
)
@@ -587,11 +596,11 @@ module Flow<InputSig Input> implements OutputSig<Input> {
587
596
* precaution, even though this is expected to hold for all the given aliased
588
597
* accesses.
589
598
*/
590
- private predicate localClosureAccess ( ClosureExpr ce , Expr access , BasicBlock bb , int i ) {
599
+ private predicate localOrNestedClosureAccess ( ClosureExpr ce , Expr access , BasicBlock bb , int i ) {
591
600
ce .hasAliasedAccess ( access ) and
592
601
access .hasCfgNode ( bb , i ) and
593
602
pragma [ only_bind_out ] ( bb .getEnclosingCallable ( ) ) =
594
- pragma [ only_bind_out ] ( closureExprGetCallable ( ce ) )
603
+ pragma [ only_bind_out ] ( closureExprGetAReferencingCallable ( ce ) )
595
604
}
596
605
597
606
/**
@@ -608,7 +617,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
608
617
exists ( ClosureExpr ce | closureCaptures ( ce , v ) |
609
618
ce .hasCfgNode ( bb , i ) and ce = closure
610
619
or
611
- localClosureAccess ( ce , closure , bb , i )
620
+ localOrNestedClosureAccess ( ce , closure , bb , i )
612
621
) and
613
622
if v .getCallable ( ) != bb .getEnclosingCallable ( ) then topScope = false else topScope = true
614
623
}
0 commit comments