Semantic Foundations of Binding-Time Analysis for Imperative Programs
- Manuvir Das ,
- Thomas Reps ,
- Pascal Van Hentenryck
PEPM '95 Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation |
Published by Association for Computing Machinery, Inc.
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. The 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, the BTAs are related to the operation of program slicing, which can be implemented using such graphs.
Copyright © 1995 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org. The definitive version of this paper can be found at ACM's Digital Library -http://www.acm.org/dl/.