@@ -151,6 +151,11 @@ signature module OutputSig<InputSig I> {
151
151
/**
152
152
* A data flow node that we need to reference in the step relations for
153
153
* captured variables.
154
+ *
155
+ * Note that only the `SynthesizedCaptureNode` subclass is expected to be
156
+ * added as additional nodes in `DataFlow::Node`. The other subclasses are
157
+ * expected to already be present and are included here in order to reference
158
+ * them in the step relations.
154
159
*/
155
160
class ClosureNode ;
156
161
@@ -229,61 +234,73 @@ module Flow<InputSig Input> implements OutputSig<Input> {
229
234
private import Input
230
235
231
236
additional module ConsistencyChecks {
232
- private predicate relevantExpr ( Expr e ) {
233
- e instanceof VariableRead or
234
- any ( VariableWrite vw ) .getSource ( ) = e or
235
- e instanceof ClosureExpr or
236
- any ( ClosureExpr ce ) .hasAliasedAccess ( e )
237
+ final private class FinalExpr = Expr ;
238
+
239
+ private class RelevantExpr extends FinalExpr {
240
+ RelevantExpr ( ) {
241
+ this instanceof VariableRead or
242
+ any ( VariableWrite vw ) .getSource ( ) = this or
243
+ this instanceof ClosureExpr or
244
+ any ( ClosureExpr ce ) .hasAliasedAccess ( this )
245
+ }
237
246
}
238
247
239
- private predicate relevantBasicBlock ( BasicBlock bb ) {
240
- exists ( Expr e | relevantExpr ( e ) and e .hasCfgNode ( bb , _) )
241
- or
242
- exists ( VariableWrite vw | vw .hasCfgNode ( bb , _) )
248
+ final private class FinalBasicBlock = BasicBlock ;
249
+
250
+ private class RelevantBasicBlock extends FinalBasicBlock {
251
+ RelevantBasicBlock ( ) {
252
+ exists ( RelevantExpr e | e .hasCfgNode ( this , _) )
253
+ or
254
+ exists ( VariableWrite vw | vw .hasCfgNode ( this , _) )
255
+ }
243
256
}
244
257
245
- private predicate relevantCallable ( Callable c ) {
246
- exists ( BasicBlock bb | relevantBasicBlock ( bb ) and bb .getEnclosingCallable ( ) = c )
247
- or
248
- exists ( CapturedVariable v | v .getCallable ( ) = c )
249
- or
250
- exists ( ClosureExpr ce | ce .hasBody ( c ) )
258
+ final private class FinalCallable = Callable ;
259
+
260
+ private class RelevantCallable extends FinalCallable {
261
+ RelevantCallable ( ) {
262
+ exists ( RelevantBasicBlock bb | bb .getEnclosingCallable ( ) = this )
263
+ or
264
+ exists ( CapturedVariable v | v .getCallable ( ) = this )
265
+ or
266
+ exists ( ClosureExpr ce | ce .hasBody ( this ) )
267
+ }
251
268
}
252
269
253
270
query predicate uniqueToString ( string msg , int n ) {
254
271
exists ( string elem |
255
- n = strictcount ( BasicBlock bb | relevantBasicBlock ( bb ) and not exists ( bb .toString ( ) ) ) and
272
+ n = strictcount ( RelevantBasicBlock bb | not exists ( bb .toString ( ) ) ) and
256
273
elem = "BasicBlock"
257
274
or
258
275
n = strictcount ( CapturedVariable v | not exists ( v .toString ( ) ) ) and elem = "CapturedVariable"
259
276
or
260
- n = strictcount ( Expr e | relevantExpr ( e ) and not exists ( e .toString ( ) ) ) and elem = "Expr"
277
+ n = strictcount ( RelevantExpr e | not exists ( e .toString ( ) ) ) and elem = "Expr"
261
278
or
262
- n = strictcount ( Callable c | relevantCallable ( c ) and not exists ( c .toString ( ) ) ) and
279
+ n = strictcount ( RelevantCallable c | not exists ( c .toString ( ) ) ) and
263
280
elem = "Callable"
264
281
|
265
282
msg = n + " " + elem + "(s) are missing toString"
266
283
)
267
284
or
268
285
exists ( string elem |
269
- n = strictcount ( BasicBlock bb | relevantBasicBlock ( bb ) and 2 <= strictcount ( bb .toString ( ) ) ) and
286
+ n = strictcount ( RelevantBasicBlock bb | 2 <= strictcount ( bb .toString ( ) ) ) and
270
287
elem = "BasicBlock"
271
288
or
272
289
n = strictcount ( CapturedVariable v | 2 <= strictcount ( v .toString ( ) ) ) and
273
290
elem = "CapturedVariable"
274
291
or
275
- n = strictcount ( Expr e | relevantExpr ( e ) and 2 <= strictcount ( e .toString ( ) ) ) and
292
+ n = strictcount ( RelevantExpr e | 2 <= strictcount ( e .toString ( ) ) ) and
276
293
elem = "Expr"
277
294
or
278
- n = strictcount ( Callable c | relevantCallable ( c ) and 2 <= strictcount ( c .toString ( ) ) ) and
295
+ n = strictcount ( RelevantCallable c | 2 <= strictcount ( c .toString ( ) ) ) and
279
296
elem = "Callable"
280
297
|
281
298
msg = n + " " + elem + "(s) have multiple toStrings"
282
299
)
283
300
}
284
301
285
302
query predicate uniqueEnclosingCallable ( BasicBlock bb , string msg ) {
286
- relevantBasicBlock ( bb ) and
303
+ bb instanceof RelevantBasicBlock and
287
304
(
288
305
msg = "BasicBlock has no enclosing callable" and not exists ( bb .getEnclosingCallable ( ) )
289
306
or
@@ -293,19 +310,19 @@ module Flow<InputSig Input> implements OutputSig<Input> {
293
310
}
294
311
295
312
query predicate uniqueDominator ( BasicBlock bb , string msg ) {
296
- relevantBasicBlock ( bb ) and
313
+ bb instanceof RelevantBasicBlock and
297
314
msg = "BasicBlock has multiple immediate dominators" and
298
315
2 <= strictcount ( getImmediateBasicBlockDominator ( bb ) )
299
316
}
300
317
301
318
query predicate localDominator ( BasicBlock bb , string msg ) {
302
- relevantBasicBlock ( bb ) and
319
+ bb instanceof RelevantBasicBlock and
303
320
msg = "BasicBlock has non-local dominator" and
304
321
bb .getEnclosingCallable ( ) != getImmediateBasicBlockDominator ( bb ) .getEnclosingCallable ( )
305
322
}
306
323
307
324
query predicate localSuccessor ( BasicBlock bb , string msg ) {
308
- relevantBasicBlock ( bb ) and
325
+ bb instanceof RelevantBasicBlock and
309
326
msg = "BasicBlock has non-local successor" and
310
327
bb .getEnclosingCallable ( ) != getABasicBlockSuccessor ( bb ) .getEnclosingCallable ( )
311
328
}
@@ -322,7 +339,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
322
339
}
323
340
324
341
query predicate uniqueLocation ( Expr e , string msg ) {
325
- relevantExpr ( e ) and
342
+ e instanceof RelevantExpr and
326
343
(
327
344
msg = "Expr has no location" and not exists ( e .getLocation ( ) )
328
345
or
@@ -331,7 +348,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
331
348
}
332
349
333
350
query predicate uniqueCfgNode ( Expr e , string msg ) {
334
- relevantExpr ( e ) and
351
+ e instanceof RelevantExpr and
335
352
(
336
353
msg = "Expr has no cfg node" and not e .hasCfgNode ( _, _)
337
354
or
@@ -413,7 +430,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
413
430
}
414
431
415
432
query predicate uniqueCallableLocation ( Callable c , string msg ) {
416
- relevantCallable ( c ) and
433
+ c instanceof RelevantCallable and
417
434
(
418
435
msg = "Callable has no location" and not exists ( c .getLocation ( ) )
419
436
or
@@ -622,13 +639,12 @@ module Flow<InputSig Input> implements OutputSig<Input> {
622
639
entryBlock ( bb ) and
623
640
pragma [ only_bind_out ] ( bb .getEnclosingCallable ( ) ) = c and
624
641
i =
625
- - 1 +
626
- min ( int j |
642
+ min ( int j |
627
643
j = 1 or
628
644
captureRead ( _, bb , j , _, _) or
629
645
captureWrite ( _, bb , j , _, _) or
630
646
synthRead ( _, bb , j , _, _)
631
- )
647
+ ) - 1
632
648
|
633
649
cc = TThis ( c )
634
650
or
@@ -637,9 +653,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
637
653
}
638
654
639
655
private module CaptureSsaInput implements Ssa:: InputSig {
640
- class BasicBlock instanceof Input:: BasicBlock {
641
- string toString ( ) { result = super .toString ( ) }
642
- }
656
+ final class BasicBlock = Input:: BasicBlock ;
643
657
644
658
BasicBlock getImmediateBasicBlockDominator ( BasicBlock bb ) {
645
659
result = Input:: getImmediateBasicBlockDominator ( bb )
@@ -666,7 +680,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
666
680
667
681
predicate variableRead ( BasicBlock bb , int i , SourceVariable cc , boolean certain ) {
668
682
(
669
- synthThisQualifier ( bb , i ) and cc = TThis ( bb .( Input :: BasicBlock ) . getEnclosingCallable ( ) )
683
+ synthThisQualifier ( bb , i ) and cc = TThis ( bb .getEnclosingCallable ( ) )
670
684
or
671
685
exists ( CapturedVariable v | cc = TVariable ( v ) |
672
686
captureRead ( v , bb , i , true , _) or synthRead ( v , bb , i , true , _)
0 commit comments