@@ -381,60 +381,83 @@ module EssaFlow {
381
381
//--------
382
382
// Local flow
383
383
//--------
384
- signature predicate stepSig ( Node nodeFrom , Node nodeTo ) ;
384
+ /** A module for transforming step relations. */
385
+ module StepRelationTransformations {
386
+ /** A step relation */
387
+ signature predicate stepSig ( Node nodeFrom , Node nodeTo ) ;
385
388
386
- /**
387
- * A module to separate import-time from run-time.
388
- *
389
- * We really have two local flow relations, on for module initialisation time (or _import time_) and one for runtime.
390
- * Consider a read from a global variable `x = foo`. At import time there should be a local flow step from `foo` to `x`,
391
- * while at runtime there should be a jump step from the module variable corresponding to `foo` to `x`.
392
- *
393
- * Similarly for, a write `foo = y`, at import time, there is a local flow step from `y` to `foo` while at runtime there
394
- * is a jump step from `y` to the module variable corresponding to `foo`.
395
- *
396
- * We need a way of distinguishing if we are looking at import time or runtime. We have the following helpful facts:
397
- * - All top-level executable statements are import time (and import time only)
398
- * - All -non-top-level code may be executed at runtime (but could also be executed at import time)
399
- *
400
- * We could write an analysis to determine which functions are called at import time, but until we have that, we will go
401
- * with the heuristic that global variables act according to import time rules at top-level program points and according
402
- * to runtime rules everywhere else. This will forego some import time local flow but otherwise be consistent.
403
- */
404
- module Separate< stepSig / 2 rawStep> {
405
389
/**
406
- * Holds if `node` is found at the top level of a module.
390
+ * A module to separate import-time from run-time.
391
+ *
392
+ * We really have two local flow relations, on for module initialisation time (or _import time_) and one for runtime.
393
+ * Consider a read from a global variable `x = foo`. At import time there should be a local flow step from `foo` to `x`,
394
+ * while at runtime there should be a jump step from the module variable corresponding to `foo` to `x`.
395
+ *
396
+ * Similarly for, a write `foo = y`, at import time, there is a local flow step from `y` to `foo` while at runtime there
397
+ * is a jump step from `y` to the module variable corresponding to `foo`.
398
+ *
399
+ * We need a way of distinguishing if we are looking at import time or runtime. We have the following helpful facts:
400
+ * - All top-level executable statements are import time (and import time only)
401
+ * - All -non-top-level code may be executed at runtime (but could also be executed at import time)
402
+ *
403
+ * We could write an analysis to determine which functions are called at import time, but until we have that, we will go
404
+ * with the heuristic that global variables act according to import time rules at top-level program points and according
405
+ * to runtime rules everywhere else. This will forego some import time local flow but otherwise be consistent.
407
406
*/
408
- pragma [ inline]
409
- predicate isTopLevel ( Node node ) { node .getScope ( ) instanceof Module }
410
-
411
- /** Holds if a step can be taken from `nodeFrom` to `nodeTo` at import time. */
412
- predicate importTimeStep ( Node nodeFrom , Node nodeTo ) {
413
- // As a proxy for whether statements can be executed at import time,
414
- // we check if they appear at the top level.
415
- // This will miss statements inside functions called from the top level.
416
- isTopLevel ( nodeFrom ) and
417
- isTopLevel ( nodeTo ) and
418
- rawStep ( nodeFrom , nodeTo )
419
- }
407
+ module Separate< stepSig / 2 rawStep> {
408
+ /**
409
+ * Holds if `node` is found at the top level of a module.
410
+ */
411
+ pragma [ inline]
412
+ predicate isTopLevel ( Node node ) { node .getScope ( ) instanceof Module }
413
+
414
+ /** Holds if a step can be taken from `nodeFrom` to `nodeTo` at import time. */
415
+ predicate importTimeStep ( Node nodeFrom , Node nodeTo ) {
416
+ // As a proxy for whether statements can be executed at import time,
417
+ // we check if they appear at the top level.
418
+ // This will miss statements inside functions called from the top level.
419
+ isTopLevel ( nodeFrom ) and
420
+ isTopLevel ( nodeTo ) and
421
+ rawStep ( nodeFrom , nodeTo )
422
+ }
423
+
424
+ /** Holds if a step can be taken from `nodeFrom` to `nodeTo` at runtime. */
425
+ predicate runtimeStep ( Node nodeFrom , Node nodeTo ) {
426
+ // Anything not at the top level can be executed at runtime.
427
+ not isTopLevel ( nodeFrom ) and
428
+ not isTopLevel ( nodeTo ) and
429
+ rawStep ( nodeFrom , nodeTo )
430
+ }
420
431
421
- /** Holds if a step can be taken from `nodeFrom` to `nodeTo` at runtime. */
422
- predicate runtimeStep ( Node nodeFrom , Node nodeTo ) {
423
- // Anything not at the top level can be executed at runtime.
424
- not isTopLevel ( nodeFrom ) and
425
- not isTopLevel ( nodeTo ) and
426
- rawStep ( nodeFrom , nodeTo )
432
+ /**
433
+ * Holds if a step can be taken from `nodeFrom` to `nodeTo`.
434
+ */
435
+ predicate step ( Node nodeFrom , Node nodeTo ) {
436
+ importTimeStep ( nodeFrom , nodeTo ) or
437
+ runtimeStep ( nodeFrom , nodeTo )
438
+ }
427
439
}
428
440
429
441
/**
430
- * Holds if a step can be taken from `nodeFrom` to `nodeTo`.
442
+ * A module to add steps from post-update nodes.
443
+ * Whenever there is a step from `x` to `y`,
444
+ * we add a step from `[post] x` to `y`.
431
445
*/
432
- predicate step ( Node nodeFrom , Node nodeTo ) {
433
- importTimeStep ( nodeFrom , nodeTo ) or
434
- runtimeStep ( nodeFrom , nodeTo )
446
+ module IncludePostUpdateFlow< stepSig / 2 rawStep> {
447
+ predicate step ( Node nodeFrom , Node nodeTo ) {
448
+ // If a raw step can be taken out of a node `node`, a step can be taken
449
+ // both out of `node` and any post-update node of `node`.
450
+ exists ( Node node | rawStep ( node , nodeTo ) |
451
+ nodeFrom = node
452
+ or
453
+ nodeFrom .( PostUpdateNode ) .getPreUpdateNode ( ) = node
454
+ )
455
+ }
435
456
}
436
457
}
437
458
459
+ import StepRelationTransformations
460
+
438
461
/**
439
462
* This is the local flow predicate that is used as a building block in global
440
463
* data flow.
@@ -455,12 +478,7 @@ predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo) {
455
478
* or at runtime when callables in the module are called.
456
479
*/
457
480
predicate simpleLocalFlowStepForTypetracking ( Node nodeFrom , Node nodeTo ) {
458
- // If there is local flow out of a node `node`, we want flow
459
- // both out of `node` and any post-update node of `node`.
460
- exists ( Node node |
461
- nodeFrom = update ( node ) and
462
- Separate< EssaFlow:: essaFlowStep / 2 > :: step ( node , nodeTo )
463
- )
481
+ IncludePostUpdateFlow< Separate< EssaFlow:: essaFlowStep / 2 > :: step / 2 > :: step ( nodeFrom , nodeTo )
464
482
}
465
483
466
484
private predicate summaryLocalStep ( Node nodeFrom , Node nodeTo ) {
@@ -469,12 +487,7 @@ private predicate summaryLocalStep(Node nodeFrom, Node nodeTo) {
469
487
}
470
488
471
489
predicate summaryFlowSteps ( Node nodeFrom , Node nodeTo ) {
472
- // If there is local flow out of a node `node`, we want flow
473
- // both out of `node` and any post-update node of `node`.
474
- exists ( Node node |
475
- nodeFrom = update ( node ) and
476
- Separate< summaryLocalStep / 2 > :: step ( node , nodeTo )
477
- )
490
+ IncludePostUpdateFlow< Separate< summaryLocalStep / 2 > :: step / 2 > :: step ( nodeFrom , nodeTo )
478
491
}
479
492
480
493
/** `ModuleVariable`s are accessed via jump steps at runtime. */
@@ -498,15 +511,6 @@ predicate runtimeJumpStep(Node nodeFrom, Node nodeTo) {
498
511
)
499
512
}
500
513
501
- /**
502
- * Holds if `result` is either `node`, or the post-update node for `node`.
503
- */
504
- private Node update ( Node node ) {
505
- result = node
506
- or
507
- result .( PostUpdateNode ) .getPreUpdateNode ( ) = node
508
- }
509
-
510
514
//--------
511
515
// Type pruning
512
516
//--------
0 commit comments