Decompilation: the enumeration of types and grammars

ABSTRACT

While a compiler produces low-level object code from high-level source code, a decompiler produces high-level code from low-level code and has applications in the testing and validation of safety-critical software. The decompilation of an object code provides an independent demonstration of correctness that is hard to better for industrial purposes (an alternative is to prove the compiler correct). But, although compiler compilers are in common use in the software industry, a decompiler compiler is much more unusual.It turns out that a data type specification for a programming-language grammar can be remolded into a functional 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) compilers.This paper deals with methods and theory, together with an application 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 stopping, is shown to have no recursive solution, but methods of abstract interpretation can be used to guarantee the adequacy and completeness of our technique in practical instances, including the decompiler for the language presented here.

REFERENCES

• 1: Harold Abelson , Gerald Jay Sussman , Julie Sussman, Structure and interpretation of computer programs, MIT Press, Cambridge, MA, 1985
• 2: S. Abramsky , C. Hankin, Abstract interpretation of declarative languages, Halsted Press, New York, NY, 1987
• 3: George S. Boolos , Richard C. Jeffrey, Computability and logic: 3rd ed., Cambridge University Press, New York, NY, 1989
• 4: BOWEN, J. P. 1992. From programs to object code using logic and logic programming. In Code Generation--Concepts, Tools, Techniques, R. Giegerich and S. L. Graham, Eds. Workshops in Computing. Springer-Verlag, New York, 173-192.
• 5: BOWEN, J. P. 1993. From programs to object code and back again using logic programming: Compilation and decompilation. J. Softw. Maint. Res. Pract. 5, 4 (Dec.), 205-234.
• 6: J. P. Bowen , P. T. Breuer, Decompilation, The REDO compendium: reverse engineering for software maintenance, John Wiley & Sons, Inc., New York, NY, 1993
• 7: BOWEN, J. P., AND STAVRWOU, V. 1993. Safety-critical systems, formal methods and standards. 1EE/BCS Softw. Eng. J. 8, 4 (July), 189-209.
• 8: BOWEN, J. P., BREWER, P. T., AND LANO, K. C. 1993a. A compendium of' formal techniques for software maintenance. IEE/BCS Soflw. Eng. J. 8, 5 (Sept.), 253-262.
• 9: BOWEN, J. P., BREUER, P. T., ANI) LANO, K. C. 1993b. Formal specifications in software maintenance: From code to Z++ and back again. Inf. Softw. Teeh. 35, 11-12 (Nov.-Dec.), 679-690.
• 10: Jonathan P. Bowen , Jifeng He , Paritosh K. Pandya, An Approach to Verifiable Compiling Specification and Prototyping, Proceedings of the 2nd International Workshop on Programming Language Implementation and Logic Programming, p.45-59, August 20-22, 1990
• 11: BREUER, P. T., AND BOWEN, J. P. 1992. Decompilation is the efficient enumeration of types. In Journdes de Travail WSA'92 Analyse Statique, vol. BIGRE 81-82, M. Billaud et al., Eds. IRISA-Campus de Beaulieu, Rennes Cedex, France, 255-273.
• 12: BREUER, P. T., AND LANO, K. C. 1991. Creating specifications from code: Reverse engineering techniques. J. Softw. Maint. Res. Pract. 3, 3 (Sept.), 145-162.
• 13: CLARK, K. L., MCCABE, F., AND GREGORY, S. 1982. IC-PROLOG language features. In Logic Programming, K. L. Clark and S.-A. Tarnlund, Eds. Academic Press, New York.
• 14: D. L. Clutterbuck , B. A. Carré, The verification of low-level code, Software Engineering Journal, v.3 n.3, p.97-111, May 1988
• 15: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 16: DERANSART, P., AND MA~USZYI~SKI, J. 1987. Relating logic programs and attribute grammars. J. Logic Program. 3, 2, 125-163.
• 17: DERANSART, P., JOURDAN, M., AND LORHO, B. 1988. Attribute Grammars. Lecture Notes in Computer Science, vol. 323. Springer-Verlag, New York.
• 18: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 19: HOARE, C. A. R. 1991. Refinement algebra proves correctness of compiling specifications. In 3rd Refinement Workshop, C. C. Morgan and J. C. P. Woodcock, Eds. Workshops in Computing. Springer-Verlag, New York, 33-48.
• 20: HOARE, C. A. R., HE, J., BOWEN, j. P~, AND PANDYA, P. K. 1990~ An algebraic approach to verifiable compiling specification and prototyping of the ProCoS level 0 programming language. In ESPRIT '90 Conference Proceedings. Kluwer Academic Publishers, Dordrecht, The Netherlands, 804-818.
• 21: HOOD, S. T. 1991. Decompiling with definite clause grammars. Res. Rep. ERL-0571-RR, Defence Science and Technology Organisation, Electronics Research Laboratory, Salisbury, South Australia, Sept.
• 22: CORPORATE INMOS Limited, Transputer instruction set: a compiler writer's guide, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 23: Thomas Johnsson, Attribute grammars as a functional programming paradigm, Proc. of a conference on Functional programming languages and computer architecture, p.154-173, October 1987, Portland, Oregon, United States
• 24: KLEENE, S. C. 1967. Mathematical Logic. John Wiley, New York.
• 25: LANO, K. C., AND BR~;UER, P. T. 1990. From programs to Z specifications. In Z User Workshop, Oxford1989, J. E. Nicholls, Ed. Workshops in Computing. Springer-Verlag, New York, 46-70.
• 26: J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 27: Ulf Nilsson , Jan Maluszynski, Logic, Programming and PROLOG, John Wiley & Sons, Inc., New York, NY, 1990
• 28: PAVEY, D. g., AND WINSBORROW, L. A. 1993. Demonstrating equivalence of source code and PROM contents. Comput. J. 36, 7, 654-667.
• 29: Alfred Spector , David Gifford, The space shuttle primary computer system, Communications of the ACM, v.27 n.9, p.872-900, Sept. 1984 [doi>10.1145/358234.358246]
• 30: TURNER, D. A. 1992. Functional programming and Miranda. IFIP Trans. A Comput. Sci. Tech. 12, 32-41.
• 31: H. J. van Zuylen, The REDO compendium: reverse engineering for software maintenance, John Wiley & Sons, Inc., New York, NY, 1993
• 32: WADLER, P. 1987. List comprehensions. In The Implementation of Functional Programming Languages, S. L. Peyton-Jones, Ed. Prentice-Hall International Series in Computer Science. Prentice-Hall, Hemel Hempstead, U.K.
• 33: WARD, M., CALLISS, F. W., AND MUNRO, M. 1989. The maintainer's assistant. In Proceedings of the Conference on Software Maintenance. IEEE, New York, 307-315.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Translator writing systems and compiler generators

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics; Syntax

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Operations on languages

General Terms:
Languages, Theory

Keywords:
abstract interpretation, attribute grammar, decompilation, functional programming, list comprehension, logic programming, reverse engineering