Efficient Symbolic Analysis of Programs.
Abstract
This paper is concerned with constructing, for each expression in a given program text, a symbolic expression whose value is equal to the value of the text expression for all executions of the program. A cover is a mapping from text expressions to such symbolic expressions. Covers can be used for constant propagation, code motion, and a variety of other program optimizations. Covers can also be used as an aid in symbolic program execution and for finding loop invariants for program verification. We describe a direct (non-iterative) algorithm for computing a cover. The cover computed by an algorithm is characterized as the minimum of a certain fixed point equation, and is in general a better cover than might be computed by iteration methods (which can compute fixed point covers which are not minimal). Our algorithm is efficient and applicable to all flow graphs. A variant of an algorithm is implemented by (KK) in an optimizing compiler for Pascal. R1 extends our algorithm to symbolic analysis of programs with records, such as LISP and PASCAL programs. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1982
- Accession Number
- ADA122660
Entities
People
- Harry R. Lewis
- John Reif
Organizations
- Harvard University