Using rewriting techniques to produce code generators and proving them correct

AbstractA major problem in deriving a compiler from a formal definition is the production of correct and efficient object code. In this context, we propose a solution to the problem of code-generator generation.Our approach is based on a target machine description where the basic concepts used (storage classes, access modes, access classes and instructions) are hierarchically described by tree patterns. These tree patterns are terms of an abstract data type. The program intermediate representation (input to the code generator) is a term of the same abstract data type.The code generation process is based on access modes and instruction template-driven rewritings. The result is that each program instruction is reduced to a sequence of elementary machine instructions, each of them representing an instance of an instruction template.The axioms of the abstract data type are used to prove that the rewritings preserve the semantics of the intermediate representation