@@ -11,19 +11,21 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
11
11
or
12
12
exists ( TypeFlowNode mid | isNull ( mid ) and step ( mid , n ) )
13
13
or
14
- forex ( TypeFlowNode mid | I :: joinStep ( mid , n ) | isNull ( mid ) ) and
14
+ forex ( TypeFlowNode mid | joinStep ( mid , n ) | isNull ( mid ) ) and
15
15
not isExcludedFromNullAnalysis ( n )
16
16
}
17
17
18
18
/**
19
19
* Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
20
20
* functionally determined by `n2`, and `n1` might take a non-null value.
21
21
*/
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 )
24
24
}
25
25
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
+ }
27
29
28
30
private predicate sccEdge ( TypeFlowNode n1 , TypeFlowNode n2 ) {
29
31
anyStep ( n1 , n2 ) and anyStep + ( n2 , n1 )
@@ -36,9 +38,9 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
36
38
/** Holds if `n` is part of an SCC of size 2 or more represented by `scc`. */
37
39
private predicate sccRepr ( TypeFlowNode n , TypeFlowScc scc ) { scc = Scc:: getEquivalenceClass ( n ) }
38
40
39
- private predicate sccJoinStep ( TypeFlowNode n , TypeFlowScc scc ) {
41
+ private predicate sccJoinStepNotNull ( TypeFlowNode n , TypeFlowScc scc ) {
40
42
exists ( TypeFlowNode mid |
41
- joinStep ( n , mid ) and
43
+ joinStepNotNull ( n , mid ) and
42
44
sccRepr ( mid , scc ) and
43
45
not sccRepr ( n , scc )
44
46
)
@@ -141,13 +143,13 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
141
143
private module JoinStep implements Edge {
142
144
class Node = TypeFlowNode ;
143
145
144
- predicate edge = joinStep / 2 ;
146
+ predicate edge = joinStepNotNull / 2 ;
145
147
}
146
148
147
149
private module SccJoinStep implements Edge {
148
150
class Node = TypeFlowScc ;
149
151
150
- predicate edge = sccJoinStep / 2 ;
152
+ predicate edge = sccJoinStepNotNull / 2 ;
151
153
}
152
154
153
155
private module RankedJoinStep = RankEdge< JoinStep > ;
@@ -172,13 +174,13 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
172
174
exists ( TypeFlowNode mid | exactType ( mid , t ) and step ( mid , n ) )
173
175
or
174
176
// 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))`
176
178
ForAll< TypeFlowNode , RankedJoinStep , ExactTypePropagation > :: flowJoin ( n , t )
177
179
or
178
180
exists ( TypeFlowScc scc |
179
181
sccRepr ( n , scc ) and
180
182
// Optimized version of
181
- // `forex(TypeFlowNode mid | sccJoinStep (mid, scc) | exactType(mid, t))`
183
+ // `forex(TypeFlowNode mid | sccJoinStepNotNull (mid, scc) | exactType(mid, t))`
182
184
ForAll< TypeFlowScc , RankedSccJoinStep , ExactTypePropagation > :: flowJoin ( scc , t )
183
185
)
184
186
}
@@ -327,7 +329,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
327
329
*/
328
330
private predicate unionTypeFlowBaseCand ( TypeFlowNode n , Type t , boolean exact ) {
329
331
exists ( TypeFlowNode next |
330
- joinStep ( n , next ) and
332
+ joinStepNotNull ( n , next ) and
331
333
bestTypeFlowOrTypeFlowBase ( n , t , exact ) and
332
334
not bestTypeFlowOrTypeFlowBase ( next , t , exact ) and
333
335
not exactType ( next , _)
@@ -354,7 +356,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
354
356
not exactType ( n , _) and
355
357
(
356
358
// 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))`
358
360
ForAll< TypeFlowNode , RankedJoinStep , HasUnionTypePropagation > :: flowJoin ( n , _)
359
361
or
360
362
exists ( TypeFlowScc scc |
0 commit comments