@@ -151,6 +151,11 @@ signature module OutputSig<InputSig I> {
151151 /**
152152 * A data flow node that we need to reference in the step relations for
153153 * 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.
154159 */
155160 class ClosureNode ;
156161
@@ -229,61 +234,73 @@ module Flow<InputSig Input> implements OutputSig<Input> {
229234 private import Input
230235
231236 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+ }
237246 }
238247
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+ }
243256 }
244257
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+ }
251268 }
252269
253270 query predicate uniqueToString ( string msg , int n ) {
254271 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
256273 elem = "BasicBlock"
257274 or
258275 n = strictcount ( CapturedVariable v | not exists ( v .toString ( ) ) ) and elem = "CapturedVariable"
259276 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"
261278 or
262- n = strictcount ( Callable c | relevantCallable ( c ) and not exists ( c .toString ( ) ) ) and
279+ n = strictcount ( RelevantCallable c | not exists ( c .toString ( ) ) ) and
263280 elem = "Callable"
264281 |
265282 msg = n + " " + elem + "(s) are missing toString"
266283 )
267284 or
268285 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
270287 elem = "BasicBlock"
271288 or
272289 n = strictcount ( CapturedVariable v | 2 <= strictcount ( v .toString ( ) ) ) and
273290 elem = "CapturedVariable"
274291 or
275- n = strictcount ( Expr e | relevantExpr ( e ) and 2 <= strictcount ( e .toString ( ) ) ) and
292+ n = strictcount ( RelevantExpr e | 2 <= strictcount ( e .toString ( ) ) ) and
276293 elem = "Expr"
277294 or
278- n = strictcount ( Callable c | relevantCallable ( c ) and 2 <= strictcount ( c .toString ( ) ) ) and
295+ n = strictcount ( RelevantCallable c | 2 <= strictcount ( c .toString ( ) ) ) and
279296 elem = "Callable"
280297 |
281298 msg = n + " " + elem + "(s) have multiple toStrings"
282299 )
283300 }
284301
285302 query predicate uniqueEnclosingCallable ( BasicBlock bb , string msg ) {
286- relevantBasicBlock ( bb ) and
303+ bb instanceof RelevantBasicBlock and
287304 (
288305 msg = "BasicBlock has no enclosing callable" and not exists ( bb .getEnclosingCallable ( ) )
289306 or
@@ -293,19 +310,19 @@ module Flow<InputSig Input> implements OutputSig<Input> {
293310 }
294311
295312 query predicate uniqueDominator ( BasicBlock bb , string msg ) {
296- relevantBasicBlock ( bb ) and
313+ bb instanceof RelevantBasicBlock and
297314 msg = "BasicBlock has multiple immediate dominators" and
298315 2 <= strictcount ( getImmediateBasicBlockDominator ( bb ) )
299316 }
300317
301318 query predicate localDominator ( BasicBlock bb , string msg ) {
302- relevantBasicBlock ( bb ) and
319+ bb instanceof RelevantBasicBlock and
303320 msg = "BasicBlock has non-local dominator" and
304321 bb .getEnclosingCallable ( ) != getImmediateBasicBlockDominator ( bb ) .getEnclosingCallable ( )
305322 }
306323
307324 query predicate localSuccessor ( BasicBlock bb , string msg ) {
308- relevantBasicBlock ( bb ) and
325+ bb instanceof RelevantBasicBlock and
309326 msg = "BasicBlock has non-local successor" and
310327 bb .getEnclosingCallable ( ) != getABasicBlockSuccessor ( bb ) .getEnclosingCallable ( )
311328 }
@@ -322,7 +339,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
322339 }
323340
324341 query predicate uniqueLocation ( Expr e , string msg ) {
325- relevantExpr ( e ) and
342+ e instanceof RelevantExpr and
326343 (
327344 msg = "Expr has no location" and not exists ( e .getLocation ( ) )
328345 or
@@ -331,7 +348,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
331348 }
332349
333350 query predicate uniqueCfgNode ( Expr e , string msg ) {
334- relevantExpr ( e ) and
351+ e instanceof RelevantExpr and
335352 (
336353 msg = "Expr has no cfg node" and not e .hasCfgNode ( _, _)
337354 or
@@ -413,7 +430,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
413430 }
414431
415432 query predicate uniqueCallableLocation ( Callable c , string msg ) {
416- relevantCallable ( c ) and
433+ c instanceof RelevantCallable and
417434 (
418435 msg = "Callable has no location" and not exists ( c .getLocation ( ) )
419436 or
@@ -622,13 +639,12 @@ module Flow<InputSig Input> implements OutputSig<Input> {
622639 entryBlock ( bb ) and
623640 pragma [ only_bind_out ] ( bb .getEnclosingCallable ( ) ) = c and
624641 i =
625- - 1 +
626- min ( int j |
642+ min ( int j |
627643 j = 1 or
628644 captureRead ( _, bb , j , _, _) or
629645 captureWrite ( _, bb , j , _, _) or
630646 synthRead ( _, bb , j , _, _)
631- )
647+ ) - 1
632648 |
633649 cc = TThis ( c )
634650 or
@@ -637,9 +653,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
637653 }
638654
639655 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 ;
643657
644658 BasicBlock getImmediateBasicBlockDominator ( BasicBlock bb ) {
645659 result = Input:: getImmediateBasicBlockDominator ( bb )
@@ -666,7 +680,7 @@ module Flow<InputSig Input> implements OutputSig<Input> {
666680
667681 predicate variableRead ( BasicBlock bb , int i , SourceVariable cc , boolean certain ) {
668682 (
669- synthThisQualifier ( bb , i ) and cc = TThis ( bb .( Input :: BasicBlock ) . getEnclosingCallable ( ) )
683+ synthThisQualifier ( bb , i ) and cc = TThis ( bb .getEnclosingCallable ( ) )
670684 or
671685 exists ( CapturedVariable v | cc = TVariable ( v ) |
672686 captureRead ( v , bb , i , true , _) or synthRead ( v , bb , i , true , _)
0 commit comments