@@ -60,7 +60,7 @@ signature module UniversalFlowInput<LocationSig Location> {
60
60
default predicate isExcludedFromNullAnalysis ( FlowNode n ) { none ( ) }
61
61
}
62
62
63
- module UfMake < LocationSig Location, UniversalFlowInput< Location > I> {
63
+ module Make < LocationSig Location, UniversalFlowInput< Location > I> {
64
64
private import I
65
65
66
66
/**
@@ -170,48 +170,48 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
170
170
int lastRank ( Node n ) { result = max ( int r | edgeRank ( r , _, n ) ) }
171
171
}
172
172
173
- private signature module TypePropagation {
174
- class Typ ;
173
+ private signature module PropPropagation {
174
+ class Prop ;
175
175
176
- predicate candType ( FlowNode n , Typ t ) ;
176
+ predicate candProp ( FlowNode n , Prop t ) ;
177
177
178
178
bindingset [ t]
179
- predicate supportsType ( FlowNode n , Typ t ) ;
179
+ predicate supportsProp ( FlowNode n , Prop t ) ;
180
180
}
181
181
182
182
/** Implements recursion through `forall` by way of edge ranking. */
183
- private module ForAll< NodeSig Node, RankedEdge< Node > E, TypePropagation T> {
183
+ private module ForAll< NodeSig Node, RankedEdge< Node > E, PropPropagation T> {
184
184
/**
185
- * Holds if `t` is a bound that holds on one of the incoming edges to `n` and
186
- * thus is a candidate bound for `n`.
185
+ * Holds if `t` is a property that holds on one of the incoming edges to `n` and
186
+ * thus is a candidate property for `n`.
187
187
*/
188
188
pragma [ nomagic]
189
- private predicate candJoinType ( Node n , T:: Typ t ) {
189
+ private predicate candJoinProp ( Node n , T:: Prop t ) {
190
190
exists ( FlowNode mid |
191
- T:: candType ( mid , t ) and
191
+ T:: candProp ( mid , t ) and
192
192
E:: edgeRank ( _, mid , n )
193
193
)
194
194
}
195
195
196
196
/**
197
- * Holds if `t` is a candidate bound for `n` that is also valid for data coming
197
+ * Holds if `t` is a candidate property for `n` that is also valid for data coming
198
198
* through the edges into `n` ranked from `1` to `r`.
199
199
*/
200
- private predicate flowJoin ( int r , Node n , T:: Typ t ) {
200
+ private predicate flowJoin ( int r , Node n , T:: Prop t ) {
201
201
(
202
- r = 1 and candJoinType ( n , t )
202
+ r = 1 and candJoinProp ( n , t )
203
203
or
204
204
flowJoin ( r - 1 , n , t ) and E:: edgeRank ( r , _, n )
205
205
) and
206
- forall ( FlowNode mid | E:: edgeRank ( r , mid , n ) | T:: supportsType ( mid , t ) )
206
+ forall ( FlowNode mid | E:: edgeRank ( r , mid , n ) | T:: supportsProp ( mid , t ) )
207
207
}
208
208
209
209
/**
210
- * Holds if `t` is a candidate bound for `n` that is also valid for data
211
- * coming through all the incoming edges, and therefore is a valid bound for
210
+ * Holds if `t` is a candidate property for `n` that is also valid for data
211
+ * coming through all the incoming edges, and therefore is a valid property for
212
212
* `n`.
213
213
*/
214
- predicate flowJoin ( Node n , T:: Typ t ) { flowJoin ( E:: lastRank ( n ) , n , t ) }
214
+ predicate flowJoin ( Node n , T:: Prop t ) { flowJoin ( E:: lastRank ( n ) , n , t ) }
215
215
}
216
216
217
217
private module JoinStep implements Edge {
@@ -237,12 +237,12 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
237
237
}
238
238
239
239
module FlowNullary< NullaryPropertySig P> {
240
- private module Propagation implements TypePropagation {
241
- class Typ = Unit ;
240
+ private module Propagation implements PropPropagation {
241
+ class Prop = Unit ;
242
242
243
- predicate candType ( FlowNode n , Unit u ) { hasProperty ( n ) and exists ( u ) }
243
+ predicate candProp ( FlowNode n , Unit u ) { hasProperty ( n ) and exists ( u ) }
244
244
245
- predicate supportsType = candType / 2 ;
245
+ predicate supportsProp = candProp / 2 ;
246
246
}
247
247
248
248
predicate hasProperty ( FlowNode n ) {
@@ -278,14 +278,14 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
278
278
}
279
279
280
280
module Flow< PropertySig P> {
281
- private module Propagation implements TypePropagation {
282
- class Typ = P:: Prop ;
281
+ private module Propagation implements PropPropagation {
282
+ class Prop = P:: Prop ;
283
283
284
- predicate candType = hasProperty / 2 ;
284
+ predicate candProp = hasProperty / 2 ;
285
285
286
286
bindingset [ t]
287
- predicate supportsType ( FlowNode n , Typ t ) {
288
- exists ( Typ t0 | hasProperty ( n , t0 ) and P:: propImplies ( t0 , t ) )
287
+ predicate supportsProp ( FlowNode n , Prop t ) {
288
+ exists ( Prop t0 | hasProperty ( n , t0 ) and P:: propImplies ( t0 , t ) )
289
289
}
290
290
}
291
291
0 commit comments