Report Number: CS-TR-75-498
Institution: Stanford University, Department of Computer Science
Title: Automatically Proving the Correctness of Translations Involving Optimized Code
Author: Samet, Hanan
Date: May 1975
Abstract: A formalism is described for proving that programs written in a higher level language are correctly translated to assembly language. In order to demonstrate the validity of the formalism a system has been designed and implemented for proving that programs written in a subset of LISP 1.6 as the high level language are correctly translated to LAP (an assembly language for the PDP-10) as the low level language. This work involves the identification of critical semantic properties of the language and their interrelationship to the instruction repertoire of the computer executing these programs. A primary use of the system is as a postoptimization step in code generation as well as a compiler debugger. The assembly language programs need not have been generated by a compiler and in fact may be handcoded. The primary restrictions on the assembly language programs relate to calling sequences and well-formedness. The assembly language programs are processed by a program understanding system which simulates their effect and returns as its result a representation of the program in the form of a tree. The proof procedure is independent of the intermediary mechanism which translates the high level language into the low level language. A proof consists of applying valid transformations to show the equivalence of the forms corresponding to the assembly language program and the original higher level language program, for which there also exists a tree-like intermediate form. Some interesting results include the ability to handle programs where recursion is implemented by bypassing the start of the program, the detection and pinpointing of a wide class of errors in the assembly language programs, and a deeper understanding of the question of how to deal automatically with translations between high and extremely low level languages. This disseration was submitted to the Department of Computer Science and the Committee on Graduate Studies of Stanford University in partial fulfillment of the requirements for the degree of Doctor of Philosophy.
http://i.stanford.edu/pub/cstr/reports/cs/tr/75/498/CS-TR-75-498.pdf