@@ -287,10 +287,12 @@ private module RankEdge<edgeSig/2 edge> implements RankedEdge {
287
287
}
288
288
289
289
private signature module TypePropagation {
290
- predicate candType ( TypeFlowNode n , RefType t ) ;
290
+ class Typ ;
291
+
292
+ predicate candType ( TypeFlowNode n , Typ t ) ;
291
293
292
294
bindingset [ t]
293
- predicate supportsType ( TypeFlowNode n , RefType t ) ;
295
+ predicate supportsType ( TypeFlowNode n , Typ t ) ;
294
296
}
295
297
296
298
/** Implements recursion through `forall` by way of edge ranking. */
@@ -300,7 +302,7 @@ private module ForAll<RankedEdge Edge, TypePropagation T> {
300
302
* thus is a candidate bound for `n`.
301
303
*/
302
304
pragma [ nomagic]
303
- private predicate candJoinType ( TypeFlowNode n , RefType t ) {
305
+ private predicate candJoinType ( TypeFlowNode n , T :: Typ t ) {
304
306
exists ( TypeFlowNode mid |
305
307
T:: candType ( mid , t ) and
306
308
Edge:: edgeRank ( _, mid , n )
@@ -311,7 +313,7 @@ private module ForAll<RankedEdge Edge, TypePropagation T> {
311
313
* Holds if `t` is a candidate bound for `n` that is also valid for data coming
312
314
* through the edges into `n` ranked from `1` to `r`.
313
315
*/
314
- private predicate flowJoin ( int r , TypeFlowNode n , RefType t ) {
316
+ private predicate flowJoin ( int r , TypeFlowNode n , T :: Typ t ) {
315
317
(
316
318
r = 1 and candJoinType ( n , t )
317
319
or
@@ -325,7 +327,7 @@ private module ForAll<RankedEdge Edge, TypePropagation T> {
325
327
* coming through all the incoming edges, and therefore is a valid bound for
326
328
* `n`.
327
329
*/
328
- predicate flowJoin ( TypeFlowNode n , RefType t ) { flowJoin ( Edge:: lastRank ( n ) , n , t ) }
330
+ predicate flowJoin ( TypeFlowNode n , T :: Typ t ) { flowJoin ( Edge:: lastRank ( n ) , n , t ) }
329
331
}
330
332
331
333
module RankedJoinStep = RankEdge< joinStep / 2 > ;
@@ -342,6 +344,8 @@ private predicate exactTypeBase(TypeFlowNode n, RefType t) {
342
344
}
343
345
344
346
private module ExactTypePropagation implements TypePropagation {
347
+ class Typ = RefType ;
348
+
345
349
predicate candType = exactType / 2 ;
346
350
347
351
predicate supportsType = exactType / 2 ;
@@ -387,10 +391,10 @@ private predicate upcastCand(TypeFlowNode n, RefType t1, RefType t1e, RefType t2
387
391
private predicate unconstrained ( BoundedType t ) {
388
392
t .( Wildcard ) .isUnconstrained ( )
389
393
or
390
- t .( BoundedType ) . getUpperBoundType ( ) instanceof TypeObject and
394
+ t .getUpperBoundType ( ) instanceof TypeObject and
391
395
not t .( Wildcard ) .hasLowerBound ( )
392
396
or
393
- unconstrained ( t .( BoundedType ) . getUpperBoundType ( ) )
397
+ unconstrained ( t .getUpperBoundType ( ) )
394
398
or
395
399
unconstrained ( t .( Wildcard ) .getLowerBoundType ( ) )
396
400
}
@@ -537,6 +541,8 @@ private predicate typeFlowBase(TypeFlowNode n, RefType t) {
537
541
}
538
542
539
543
private module TypeFlowPropagation implements TypePropagation {
544
+ class Typ = RefType ;
545
+
540
546
predicate candType = typeFlow / 2 ;
541
547
542
548
bindingset [ t]
@@ -644,6 +650,17 @@ private predicate unionTypeFlowBaseCand(TypeFlowNode n, RefType t, boolean exact
644
650
)
645
651
}
646
652
653
+ private module HasUnionTypePropagation implements TypePropagation {
654
+ class Typ = Unit ;
655
+
656
+ predicate candType ( TypeFlowNode mid , Unit unit ) {
657
+ exists ( unit ) and
658
+ ( unionTypeFlowBaseCand ( mid , _, _) or hasUnionTypeFlow ( mid ) )
659
+ }
660
+
661
+ predicate supportsType = candType / 2 ;
662
+ }
663
+
647
664
/**
648
665
* Holds if all incoming type flow can be traced back to a
649
666
* `unionTypeFlowBaseCand`, such that we can compute a union type bound for `n`.
@@ -652,15 +669,15 @@ private predicate unionTypeFlowBaseCand(TypeFlowNode n, RefType t, boolean exact
652
669
private predicate hasUnionTypeFlow ( TypeFlowNode n ) {
653
670
not exactType ( n , _) and
654
671
(
655
- forex ( TypeFlowNode mid | joinStep ( mid , n ) |
656
- unionTypeFlowBaseCand ( mid , _, _) or hasUnionTypeFlow ( mid )
657
- )
672
+ // Optimized version of
673
+ // `forex(TypeFlowNode mid | joinStep(mid, n) | unionTypeFlowBaseCand(mid, _, _) or hasUnionTypeFlow(mid))`
674
+ ForAll < RankedJoinStep , HasUnionTypePropagation > :: flowJoin ( n , _ )
658
675
or
659
676
exists ( TypeFlowNode scc |
660
677
sccRepr ( n , scc ) and
661
- forex ( TypeFlowNode mid | sccJoinStep ( mid , scc ) |
662
- unionTypeFlowBaseCand ( mid , _, _) or hasUnionTypeFlow ( mid )
663
- )
678
+ // Optimized version of
679
+ // `forex(TypeFlowNode mid | sccJoinStep(mid, scc) | unionTypeFlowBaseCand(mid, _, _) or hasUnionTypeFlow(mid))`
680
+ ForAll < RankedSccJoinStep , HasUnionTypePropagation > :: flowJoin ( scc , _ )
664
681
)
665
682
or
666
683
exists ( TypeFlowNode mid | step ( mid , n ) and hasUnionTypeFlow ( mid ) )
0 commit comments