@@ -7,7 +7,7 @@ signature module UniversalFlowInput<LocationSig Location> {
77 * A node for which certain data flow properties may be proved. For example,
88 * expressions and method declarations.
99 */
10- class TypeFlowNode {
10+ class FlowNode {
1111 /** Gets a textual representation of this node. */
1212 string toString ( ) ;
1313
@@ -20,16 +20,16 @@ signature module UniversalFlowInput<LocationSig Location> {
2020 *
2121 * For a given `n2`, this predicate must include all possible `n1` that can flow to `n2`.
2222 */
23- predicate step ( TypeFlowNode n1 , TypeFlowNode n2 ) ;
23+ predicate step ( FlowNode n1 , FlowNode n2 ) ;
2424
2525 /** Holds if `n` represents a `null` value. */
26- predicate isNullValue ( TypeFlowNode n ) ;
26+ predicate isNullValue ( FlowNode n ) ;
2727
2828 /**
2929 * Holds if `n` should be excluded from the set of null values even if
3030 * the null analysis determines that `n` is always null.
3131 */
32- default predicate isExcludedFromNullAnalysis ( TypeFlowNode n ) { none ( ) }
32+ default predicate isExcludedFromNullAnalysis ( FlowNode n ) { none ( ) }
3333}
3434
3535module UfMake< LocationSig Location, UniversalFlowInput< Location > I> {
@@ -39,49 +39,49 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
3939 * Holds if data can flow from `n1` to `n2` in one step, and `n1` is
4040 * functionally determined by `n2`.
4141 */
42- private predicate uniqStep ( TypeFlowNode n1 , TypeFlowNode n2 ) { n1 = unique( TypeFlowNode n | step ( n , n2 ) ) }
42+ private predicate uniqStep ( FlowNode n1 , FlowNode n2 ) { n1 = unique( FlowNode n | step ( n , n2 ) ) }
4343
4444 /**
4545 * Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
4646 * functionally determined by `n2`.
4747 */
48- private predicate joinStep ( TypeFlowNode n1 , TypeFlowNode n2 ) { step ( n1 , n2 ) and not uniqStep ( n1 , n2 ) }
48+ private predicate joinStep ( FlowNode n1 , FlowNode n2 ) { step ( n1 , n2 ) and not uniqStep ( n1 , n2 ) }
4949
5050 /** Holds if `null` is the only value that flows to `n`. */
51- private predicate isNull ( TypeFlowNode n ) {
51+ private predicate isNull ( FlowNode n ) {
5252 isNullValue ( n )
5353 or
54- exists ( TypeFlowNode mid | isNull ( mid ) and uniqStep ( mid , n ) )
54+ exists ( FlowNode mid | isNull ( mid ) and uniqStep ( mid , n ) )
5555 or
56- forex ( TypeFlowNode mid | joinStep ( mid , n ) | isNull ( mid ) ) and
56+ forex ( FlowNode mid | joinStep ( mid , n ) | isNull ( mid ) ) and
5757 not isExcludedFromNullAnalysis ( n )
5858 }
5959
6060 /**
6161 * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
6262 * functionally determined by `n2`, and `n1` might take a non-null value.
6363 */
64- predicate joinStepNotNull ( TypeFlowNode n1 , TypeFlowNode n2 ) {
64+ predicate joinStepNotNull ( FlowNode n1 , FlowNode n2 ) {
6565 joinStep ( n1 , n2 ) and not isNull ( n1 )
6666 }
6767
68- predicate anyStep ( TypeFlowNode n1 , TypeFlowNode n2 ) {
68+ predicate anyStep ( FlowNode n1 , FlowNode n2 ) {
6969 joinStepNotNull ( n1 , n2 ) or uniqStep ( n1 , n2 )
7070 }
7171
72- private predicate sccEdge ( TypeFlowNode n1 , TypeFlowNode n2 ) {
72+ private predicate sccEdge ( FlowNode n1 , FlowNode n2 ) {
7373 anyStep ( n1 , n2 ) and anyStep + ( n2 , n1 )
7474 }
7575
76- private module Scc = QlBuiltins:: EquivalenceRelation< TypeFlowNode , sccEdge / 2 > ;
76+ private module Scc = QlBuiltins:: EquivalenceRelation< FlowNode , sccEdge / 2 > ;
7777
7878 private class TypeFlowScc = Scc:: EquivalenceClass ;
7979
8080 /** Holds if `n` is part of an SCC of size 2 or more represented by `scc`. */
81- private predicate sccRepr ( TypeFlowNode n , TypeFlowScc scc ) { scc = Scc:: getEquivalenceClass ( n ) }
81+ private predicate sccRepr ( FlowNode n , TypeFlowScc scc ) { scc = Scc:: getEquivalenceClass ( n ) }
8282
83- private predicate sccJoinStepNotNull ( TypeFlowNode n , TypeFlowScc scc ) {
84- exists ( TypeFlowNode mid |
83+ private predicate sccJoinStepNotNull ( FlowNode n , TypeFlowScc scc ) {
84+ exists ( FlowNode mid |
8585 joinStepNotNull ( n , mid ) and
8686 sccRepr ( mid , scc ) and
8787 not sccRepr ( n , scc )
@@ -93,11 +93,11 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
9393 private signature module Edge {
9494 class Node ;
9595
96- predicate edge ( TypeFlowNode n1 , Node n2 ) ;
96+ predicate edge ( FlowNode n1 , Node n2 ) ;
9797 }
9898
9999 private signature module RankedEdge< NodeSig Node> {
100- predicate edgeRank ( int r , TypeFlowNode n1 , Node n2 ) ;
100+ predicate edgeRank ( int r , FlowNode n1 , Node n2 ) ;
101101
102102 int lastRank ( Node n ) ;
103103 }
@@ -109,9 +109,9 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
109109 * Holds if `r` is a ranking of the incoming edges `(n1,n2)` to `n2`. The used
110110 * ordering is not necessarily total, so the ranking may have gaps.
111111 */
112- private predicate edgeRank1 ( int r , TypeFlowNode n1 , Node n2 ) {
112+ private predicate edgeRank1 ( int r , FlowNode n1 , Node n2 ) {
113113 n1 =
114- rank [ r ] ( TypeFlowNode n , int startline , int startcolumn |
114+ rank [ r ] ( FlowNode n , int startline , int startcolumn |
115115 edge ( n , n2 ) and
116116 n .getLocation ( ) .hasLocationInfo ( _, startline , startcolumn , _, _)
117117 |
@@ -128,7 +128,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
128128 }
129129
130130 /** Holds if `r` is a ranking of the incoming edges `(n1,n2)` to `n2`. */
131- predicate edgeRank ( int r , TypeFlowNode n1 , Node n2 ) {
131+ predicate edgeRank ( int r , FlowNode n1 , Node n2 ) {
132132 exists ( int r1 |
133133 edgeRank1 ( r1 , n1 , n2 ) and
134134 edgeRank2 ( r , r1 , n2 )
@@ -141,10 +141,10 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
141141 private signature module TypePropagation {
142142 class Typ ;
143143
144- predicate candType ( TypeFlowNode n , Typ t ) ;
144+ predicate candType ( FlowNode n , Typ t ) ;
145145
146146 bindingset [ t]
147- predicate supportsType ( TypeFlowNode n , Typ t ) ;
147+ predicate supportsType ( FlowNode n , Typ t ) ;
148148 }
149149
150150 /** Implements recursion through `forall` by way of edge ranking. */
@@ -155,7 +155,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
155155 */
156156 pragma [ nomagic]
157157 private predicate candJoinType ( Node n , T:: Typ t ) {
158- exists ( TypeFlowNode mid |
158+ exists ( FlowNode mid |
159159 T:: candType ( mid , t ) and
160160 E:: edgeRank ( _, mid , n )
161161 )
@@ -171,7 +171,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
171171 or
172172 flowJoin ( r - 1 , n , t ) and E:: edgeRank ( r , _, n )
173173 ) and
174- forall ( TypeFlowNode mid | E:: edgeRank ( r , mid , n ) | T:: supportsType ( mid , t ) )
174+ forall ( FlowNode mid | E:: edgeRank ( r , mid , n ) | T:: supportsType ( mid , t ) )
175175 }
176176
177177 /**
@@ -183,7 +183,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
183183 }
184184
185185 private module JoinStep implements Edge {
186- class Node = TypeFlowNode ;
186+ class Node = FlowNode ;
187187
188188 predicate edge = joinStepNotNull / 2 ;
189189 }
@@ -199,35 +199,35 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
199199 private module RankedSccJoinStep = RankEdge< SccJoinStep > ;
200200
201201 signature module NullaryPropertySig {
202- predicate hasPropertyBase ( TypeFlowNode n ) ;
202+ predicate hasPropertyBase ( FlowNode n ) ;
203203
204- default predicate barrier ( TypeFlowNode n ) { none ( ) }
204+ default predicate barrier ( FlowNode n ) { none ( ) }
205205 }
206206
207207 module FlowNullary< NullaryPropertySig P> {
208208 private module Propagation implements TypePropagation {
209209 class Typ = Unit ;
210210
211- predicate candType ( TypeFlowNode n , Unit u ) { hasProperty ( n ) and exists ( u ) }
211+ predicate candType ( FlowNode n , Unit u ) { hasProperty ( n ) and exists ( u ) }
212212
213213 predicate supportsType = candType / 2 ;
214214 }
215215
216- predicate hasProperty ( TypeFlowNode n ) {
216+ predicate hasProperty ( FlowNode n ) {
217217 P:: hasPropertyBase ( n )
218218 or
219219 not P:: barrier ( n ) and
220220 (
221- exists ( TypeFlowNode mid | hasProperty ( mid ) and uniqStep ( mid , n ) )
221+ exists ( FlowNode mid | hasProperty ( mid ) and uniqStep ( mid , n ) )
222222 or
223223 // The following is an optimized version of
224- // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
225- ForAll< TypeFlowNode , RankedJoinStep , Propagation > :: flowJoin ( n , _)
224+ // `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
225+ ForAll< FlowNode , RankedJoinStep , Propagation > :: flowJoin ( n , _)
226226 or
227227 exists ( TypeFlowScc scc |
228228 sccRepr ( n , scc ) and
229229 // Optimized version of
230- // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid))`
230+ // `forex(FlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid))`
231231 ForAll< TypeFlowScc , RankedSccJoinStep , Propagation > :: flowJoin ( scc , _)
232232 )
233233 )
@@ -240,9 +240,9 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
240240 bindingset [ t1, t2]
241241 default predicate propImplies ( Prop t1 , Prop t2 ) { t1 = t2 }
242242
243- predicate hasPropertyBase ( TypeFlowNode n , Prop t ) ;
243+ predicate hasPropertyBase ( FlowNode n , Prop t ) ;
244244
245- default predicate barrier ( TypeFlowNode n ) { none ( ) }
245+ default predicate barrier ( FlowNode n ) { none ( ) }
246246 }
247247
248248 module Flow< PropertySig P> {
@@ -252,7 +252,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
252252 predicate candType = hasProperty / 2 ;
253253
254254 bindingset [ t]
255- predicate supportsType ( TypeFlowNode n , Typ t ) {
255+ predicate supportsType ( FlowNode n , Typ t ) {
256256 exists ( Typ t0 | hasProperty ( n , t0 ) and P:: propImplies ( t0 , t ) )
257257 }
258258 }
@@ -261,21 +261,21 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
261261 * Holds if the runtime type of `n` is exactly `t` and if this bound is a
262262 * non-trivial lower bound, that is, `t` has a subtype.
263263 */
264- predicate hasProperty ( TypeFlowNode n , P:: Prop t ) {
264+ predicate hasProperty ( FlowNode n , P:: Prop t ) {
265265 P:: hasPropertyBase ( n , t )
266266 or
267267 not P:: barrier ( n ) and
268268 (
269- exists ( TypeFlowNode mid | hasProperty ( mid , t ) and uniqStep ( mid , n ) )
269+ exists ( FlowNode mid | hasProperty ( mid , t ) and uniqStep ( mid , n ) )
270270 or
271271 // The following is an optimized version of
272- // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`
273- ForAll< TypeFlowNode , RankedJoinStep , Propagation > :: flowJoin ( n , t )
272+ // `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`
273+ ForAll< FlowNode , RankedJoinStep , Propagation > :: flowJoin ( n , t )
274274 or
275275 exists ( TypeFlowScc scc |
276276 sccRepr ( n , scc ) and
277277 // Optimized version of
278- // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid, t))`
278+ // `forex(FlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid, t))`
279279 ForAll< TypeFlowScc , RankedSccJoinStep , Propagation > :: flowJoin ( scc , t )
280280 )
281281 )
0 commit comments