@@ -570,7 +570,14 @@ module Flow<InputSig Input> implements OutputSig<Input> {
570
570
pragma [ only_bind_out ] ( closureExprGetCallable ( ce ) )
571
571
}
572
572
573
- /** Holds if we need an additional read of `v` TODO */
573
+ /**
574
+ * Holds if we need an additional read of `v` in the `i`th node of `bb` in
575
+ * order to synchronize the value stored on `closure`.
576
+ * `topScope` is true if the read is in the defining callable of `v`.
577
+ *
578
+ * Side-effects of potentially calling `closure` at this point will be
579
+ * observed in a similarly synthesized post-update node for this read of `v`.
580
+ */
574
581
private predicate synthRead (
575
582
CapturedVariable v , BasicBlock bb , int i , boolean topScope , Expr closure
576
583
) {
@@ -582,6 +589,10 @@ module Flow<InputSig Input> implements OutputSig<Input> {
582
589
if v .getCallable ( ) != bb .getEnclosingCallable ( ) then topScope = false else topScope = true
583
590
}
584
591
592
+ /**
593
+ * Holds if there is an access of a captured variable inside a closure in the
594
+ * `i`th node of `bb`, such that we need to synthesize a `this.` qualifier.
595
+ */
585
596
private predicate synthThisQualifier ( BasicBlock bb , int i ) {
586
597
synthRead ( _, bb , i , false , _) or
587
598
captureRead ( _, bb , i , false , _) or
@@ -592,6 +603,11 @@ module Flow<InputSig Input> implements OutputSig<Input> {
592
603
TVariable ( CapturedVariable v ) or
593
604
TThis ( Callable c ) { captureAccess ( _, c ) }
594
605
606
+ /**
607
+ * A storage location for a captured variable in a specific callable. This is
608
+ * either the variable itself (in its defining scope) or an instance variable
609
+ * `this` (in a capturing scope).
610
+ */
595
611
private class CaptureContainer extends TCaptureContainer {
596
612
string toString ( ) {
597
613
exists ( CapturedVariable v | this = TVariable ( v ) and result = v .toString ( ) )
@@ -600,6 +616,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
600
616
}
601
617
}
602
618
619
+ /** Holds if `cc` needs a definition at the entry of its callable scope. */
603
620
private predicate entryDef ( CaptureContainer cc , BasicBlock bb , int i ) {
604
621
exists ( Callable c |
605
622
entryBlock ( bb ) and
@@ -681,6 +698,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
681
698
TMallocNode ( ClosureExpr ce ) { hasConstructorCapture ( ce , _) }
682
699
683
700
class ClosureNode extends TClosureNode {
701
+ /** Gets a textual representation of this node. */
684
702
string toString ( ) {
685
703
exists ( CapturedVariable v | this = TSynthRead ( v , _, _, _) and result = v .toString ( ) )
686
704
or
@@ -705,6 +723,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
705
723
result = "malloc" and this = TMallocNode ( _)
706
724
}
707
725
726
+ /** Gets the location of this node. */
708
727
Location getLocation ( ) {
709
728
exists ( CapturedVariable v , BasicBlock bb , int i , Expr closure |
710
729
this = TSynthRead ( v , bb , i , _) and
@@ -893,6 +912,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
893
912
|
894
913
post = true
895
914
or
915
+ // for a constructor call the regulare ExprNode is the post-update for the MallocNode
896
916
post = false and hasConstructorCapture ( closure , v )
897
917
)
898
918
or
0 commit comments