@@ -11,19 +11,21 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
1111 or
1212 exists ( TypeFlowNode mid | isNull ( mid ) and step ( mid , n ) )
1313 or
14- forex ( TypeFlowNode mid | I :: joinStep ( mid , n ) | isNull ( mid ) ) and
14+ forex ( TypeFlowNode mid | joinStep ( mid , n ) | isNull ( mid ) ) and
1515 not isExcludedFromNullAnalysis ( n )
1616 }
1717
1818 /**
1919 * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
2020 * functionally determined by `n2`, and `n1` might take a non-null value.
2121 */
22- private predicate joinStep ( TypeFlowNode n1 , TypeFlowNode n2 ) {
23- I :: joinStep ( n1 , n2 ) and not isNull ( n1 )
22+ private predicate joinStepNotNull ( TypeFlowNode n1 , TypeFlowNode n2 ) {
23+ joinStep ( n1 , n2 ) and not isNull ( n1 )
2424 }
2525
26- private predicate anyStep ( TypeFlowNode n1 , TypeFlowNode n2 ) { joinStep ( n1 , n2 ) or step ( n1 , n2 ) }
26+ private predicate anyStep ( TypeFlowNode n1 , TypeFlowNode n2 ) {
27+ joinStepNotNull ( n1 , n2 ) or step ( n1 , n2 )
28+ }
2729
2830 private predicate sccEdge ( TypeFlowNode n1 , TypeFlowNode n2 ) {
2931 anyStep ( n1 , n2 ) and anyStep + ( n2 , n1 )
@@ -36,9 +38,9 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
3638 /** Holds if `n` is part of an SCC of size 2 or more represented by `scc`. */
3739 private predicate sccRepr ( TypeFlowNode n , TypeFlowScc scc ) { scc = Scc:: getEquivalenceClass ( n ) }
3840
39- private predicate sccJoinStep ( TypeFlowNode n , TypeFlowScc scc ) {
41+ private predicate sccJoinStepNotNull ( TypeFlowNode n , TypeFlowScc scc ) {
4042 exists ( TypeFlowNode mid |
41- joinStep ( n , mid ) and
43+ joinStepNotNull ( n , mid ) and
4244 sccRepr ( mid , scc ) and
4345 not sccRepr ( n , scc )
4446 )
@@ -141,13 +143,13 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
141143 private module JoinStep implements Edge {
142144 class Node = TypeFlowNode ;
143145
144- predicate edge = joinStep / 2 ;
146+ predicate edge = joinStepNotNull / 2 ;
145147 }
146148
147149 private module SccJoinStep implements Edge {
148150 class Node = TypeFlowScc ;
149151
150- predicate edge = sccJoinStep / 2 ;
152+ predicate edge = sccJoinStepNotNull / 2 ;
151153 }
152154
153155 private module RankedJoinStep = RankEdge< JoinStep > ;
@@ -172,13 +174,13 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
172174 exists ( TypeFlowNode mid | exactType ( mid , t ) and step ( mid , n ) )
173175 or
174176 // The following is an optimized version of
175- // `forex(TypeFlowNode mid | joinStep (mid, n) | exactType(mid, t))`
177+ // `forex(TypeFlowNode mid | joinStepNotNull (mid, n) | exactType(mid, t))`
176178 ForAll< TypeFlowNode , RankedJoinStep , ExactTypePropagation > :: flowJoin ( n , t )
177179 or
178180 exists ( TypeFlowScc scc |
179181 sccRepr ( n , scc ) and
180182 // Optimized version of
181- // `forex(TypeFlowNode mid | sccJoinStep (mid, scc) | exactType(mid, t))`
183+ // `forex(TypeFlowNode mid | sccJoinStepNotNull (mid, scc) | exactType(mid, t))`
182184 ForAll< TypeFlowScc , RankedSccJoinStep , ExactTypePropagation > :: flowJoin ( scc , t )
183185 )
184186 }
@@ -327,7 +329,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
327329 */
328330 private predicate unionTypeFlowBaseCand ( TypeFlowNode n , Type t , boolean exact ) {
329331 exists ( TypeFlowNode next |
330- joinStep ( n , next ) and
332+ joinStepNotNull ( n , next ) and
331333 bestTypeFlowOrTypeFlowBase ( n , t , exact ) and
332334 not bestTypeFlowOrTypeFlowBase ( next , t , exact ) and
333335 not exactType ( next , _)
@@ -354,7 +356,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
354356 not exactType ( n , _) and
355357 (
356358 // Optimized version of
357- // `forex(TypeFlowNode mid | joinStep (mid, n) | unionTypeFlowBaseCand(mid, _, _) or hasUnionTypeFlow(mid))`
359+ // `forex(TypeFlowNode mid | joinStepNotNull (mid, n) | unionTypeFlowBaseCand(mid, _, _) or hasUnionTypeFlow(mid))`
358360 ForAll< TypeFlowNode , RankedJoinStep , HasUnionTypePropagation > :: flowJoin ( n , _)
359361 or
360362 exists ( TypeFlowScc scc |
0 commit comments