Verification of Code Generators Using Term Rewriting Systems

Code generators for modern compilers are difficult to construct. To build a code generator that produces correct target code, we require detailed knowledge of the intermediate representation (IR) generated by the compiler’s front-end and intimate knowledge of the instruction set available on the target machine. We then put this knowledge to use by mapping the individual IR instructions to a sequence of target instructions that are identical in meaning. That is, the semantics of the original program and thus the original IR instructions that make up the program are preserved by this mapping. Unfortunately, it is often the case that errors are introduced by an incorrect mapping that results in the generation of incorrect code. Usually these incorrect code sequences can only be detected by compiling complete programs and testing their execution on some finite number of test cases. Because these test cases are finite, they are not sufficient to guarantee that our code generator will produce correct code in all cases. To guarantee correctness we require a general mechanism that will allow us to reason about the meaning of an IR instruction and the meaning of the target instruction sequence to determine if they are semantically identical. This reasoning procedure should not only allo