Semantic Foundations of Binding-Time Analysis for Imperative Programs
Manuvir Das, Thomas Reps, and Pascal Van Hentenryck
This paper examines the role of dependence analysis in defining
binding-time analyses (BTAs) for imperative programs and in
establishing that such BTAs are safe. In particular, we are concerned
with characterizing safety conditions under which a program
specializer that uses the results of a BTA is guaranteed to terminate.
Our safety conditions are formalized via semantic characterizations of
the statements in a program along two dimensions: static
versus dynamic, and finite versus infinite.
This permits us to give a semantic definition of "static-infinite
computation", a concept that has not been previously formalized. To
illustrate the concepts, we present three different BTAs for an
imperative language; we show that two of them are safe in the absence
of "static-infinite computations".
In developing these notions, we make use of program representation
graphs, which are a program representation similar to the
dependence graphs used in parallelizing and vectorizing compilers. In
operational terms, our BTAs are related to the operation of
program slicing, which can be implemented using such graphs.
(Click here to access the paper:
PostScript,
PDF.)