Semantic Foundations of Binding-Time Analysis for Imperative Programs

This paper examines the role of dependence analysis in defining bindingtime 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. 1