Module StepRelationTransformations::PhaseDependentFlow

A module to separate import-time from run-time.

We really have two local flow relations, one for module initialisation time (or import time) and one for runtime. Consider a read from a global variable x = foo. At import time there should be a local flow step from foo to x, while at runtime there should be a jump step from the module variable corresponding to foo to x.

Similarly, for a write foo = y, at import time, there is a local flow step from y to foo while at runtime there is a jump step from y to the module variable corresponding to foo.

We need a way of distinguishing if we are looking at import time or runtime. We have the following helpful facts:

• All top-level executable statements are import time (and import time only)
• All non-top-level code may be executed at runtime (but could also be executed at import time)

We could write an analysis to determine which functions are called at import time, but until we have that, we will go with the heuristic that global variables act according to import time rules at top-level program points and according to runtime rules everywhere else. This will forego some import time local flow but otherwise be consistent.