A Formal Framework for the Derivation of Machine-Specific Optimizers

The derivation of machine-specific code optimizers starts from a description of the target machine. A formal instruction-set semantics precisely defmes the concepts characteristic to the machine-code level, such as addressing modes and instructions, side effects, and overlapping of registers or memory cells. The context information relevant for local optimizations is defined by abstract interpretation of instruction semantics. This leads to a notion of instruction equivalence relative to a given context. Based on this notion, optimization rules whose machine-specific applicability criteria can be derived automatically are introduced. The formal nature of this approach serves not only to guarantee the correctness of these criteria, but also to isolate program-dependent from only machine-dependent aspects. This leads to criteria which are most efficient in the sense that they only contain subconditions that must in fact be evaluated at optimization time, while those referring to properties of the instruction set only are folded away in the derivation process.