Recent PhD Theses - 3
| Author
| Ashok Sreenivas
|
| Title
| A Framework for Imperative Program Transformations
|
| Thesis Supervisor
| K.V. Nori, S. Biswas, A. Sanyal.
|
| Date of Defence
| 25 November, 1998
|
| Institute granting Degree
| Indian Institute of Technology, Bombay
|
| Current Address
| Email: ashoks@pune.tcs.co.in
|
|
| Tata Research, Design and Development Centre (TRDDC)
|
|
| 54B, Hadapsar Industrial Estate, Hadapsar, Pune 411 013
|
Abstract
Programs are transformed by a variety of programming tools such as
editors, compilers, optimisers, re-engineering tools,
reverse-engineering tools etc. In this work we study an important
sub-class of program transformations, namely, semantically
invariant program transformations of imperative language
programs. As program transformations are usually motivated by certain
well-defined goals, they are performed under some conditions defined
by program analyses. Of the various techniques of program
analyses such as data flow analyses, abstract interpretation and type
inference, we concentrate on data flow analyses performed over
programs represented as control flow graphs.
Most applications of program transformations perform a cascade
of transformations, in which each transform is based on some analyses.
Therefore, it is imperative that the data flow information associated
with the program is updated at each step of the cascade, so that
the program remains consistent with its data flow information.
In this work, we develop a framework using which
-
program transformations can be specified and reasoned about
formally and
-
it is guaranteed that programs are
transformed such that their data flow information is kept consistent
during transformation.
First, we develop an elegant model of data flow information based on a
symbolic representation, and show that this model enables us to
present a simple solution to the problem of incremental data flow
analysis. Based on this symbolic representation of data flow
information, we develop an efficient implementation mechanism for both
exhaustive and incremental analyses, using which we maintain the
consistency of a program under transformation. This forms the first
part of the work.
In the second part, we concentrate on program transformations, and
identify a set of control flow graph transform primitives, based on
which programs can be transformed. In order to be able to formally
reason about the run-time behaviour of the program under
transformation, we study the effects of each of these primitives on
the execution semantics of a control flow graph and develop a set of
rules for semantic invariance of a program under transformation.
Finally, based on the transform primitives, we develop a language to
enable specification of program transformations, and exemplify our
transformation framework by specifying a few transforms using this
language and proving them correct.
Previous Thesis
Next Thesis