Using rewriting techniques to produce code generators and proving them correct (Q2639631)

This paper presents a solution to the problem of code-generator generation. The approach is based on a target machine description in which the basic concepts used (storage classes, access modes, instructions) are described by tree patterns that form the terms of an abstract data type. The source program is presented as an input to the code generator in an intermediate representation (IR) which is a term of the same abstract data type. The code generation consists of a rewriting process which modifies the IR until a pattern matches with an instruction template of the target machine. The axioms of the abstract data type are used to prove that the rewritings preserve the semantics of the intermediate representation. The basic concepts are illustrated by MC 68000 examples throughout the paper.