@@ -381,60 +381,83 @@ module EssaFlow {
381381//--------
382382// Local flow
383383//--------
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 ) ;
385388
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> {
405389 /**
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.
407406 */
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+ }
420431
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+ }
427439 }
428440
429441 /**
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`.
431445 */
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+ }
435456 }
436457}
437458
459+ import StepRelationTransformations
460+
438461/**
439462 * This is the local flow predicate that is used as a building block in global
440463 * data flow.
@@ -455,12 +478,7 @@ predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo) {
455478 * or at runtime when callables in the module are called.
456479 */
457480predicate 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 )
464482}
465483
466484private predicate summaryLocalStep ( Node nodeFrom , Node nodeTo ) {
@@ -469,12 +487,7 @@ private predicate summaryLocalStep(Node nodeFrom, Node nodeTo) {
469487}
470488
471489predicate 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 )
478491}
479492
480493/** `ModuleVariable`s are accessed via jump steps at runtime. */
@@ -498,15 +511,6 @@ predicate runtimeJumpStep(Node nodeFrom, Node nodeTo) {
498511 )
499512}
500513
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-
510514//--------
511515// Type pruning
512516//--------
0 commit comments