DECOMPILATION - THE ENUMERATION OF TYPES AND GRAMMARS

While a compiler produces low-level object code from high-level source code, a decompiler produces high-level code from low-level code and h as applications in the testing and validation of safety-critical softw are. The decompilation of an object code provides an independent demon stration of correctness that is hard to better for industrial purposes (an alternative is to prove the compiler correct). But, although comp iler compilers are in common use in the software industry, a decompile r compiler is much more unusual. It turns out that a data type specifi cation for a programming-language grammar can be remolded into a funct ional program that enumerates all of the abstract syntax trees of the grammar. This observation is the springboard for a general method for compiling decompilers from the specifications of(nonoptimizing) compil ers. This paper deals with methods and theory, together with an applic ation of the technique. The correctness of a decompiler generated from a simple Occam-like compiler specification is demonstrated. The basic problem of enumerating the syntax trees of grammars, and then stoppin g, is shown to have no recursive solution, but methods of abstract int erpretation can be used to guarantee the adequacy and completeness of our technique in practical instances, including the decompiler for the language presented here.