Translation and optimization for a core calculus with exceptions

ABSTRACT

A requirement of any source language is to be rich in features and concise to use by the programmers. As a drawback, it is often too complex to analyse, causing research studies to omit some of the fancy features. For instance, exception handling is an important aspect of programming languages that is instrumental for building robust software with good error handling capability. However, exceptions are often omitted during the initial formulation on program analysis and optimization. Moreover, when considering the traditional approach of converting programs from high level languages to machine code, the target code is meant for the machine, being too cryptic (or low level) for program analysis. Our goal is to design an intermediate, minimal but expressive, core calculus which can be easily analysed and manipulated, and to show that this calculus can handle major language features by translating a significant imperative source language into it. The translation to the core calculus enables us to easily analyse and optimize the code, while not sacrificing the flexibility and rich characteristic of the source language.

REFERENCES

• 1: D. Ancona , G. Lagorio , E. Zucca, A core calculus for Java exceptions, Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.16-30, October 14-18, 2001, Tampa Bay, FL, USA
• 2: Mike Barnett , K. Rustan M. Leino, Weakest-precondition of unstructured programs, Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, September 05-06, 2005, Lisbon, Portugal
• 3: Matthias Blume , Umut A. Acar , Wonseok Chae, Exception Handlers as Extensible Cases, Proceedings of the 6th Asian Symposium on Programming Languages and Systems, p.273-289, December 09-11, 2008, Bangalore, India [doi>10.1007/978-3-540-89330-1_20]
• 4: Egon Börger , Wolfram Schulte, A Practical Method for Specification and Analysis of Exception Handling-A Java/JVM Case Study, IEEE Transactions on Software Engineering, v.26 n.9, p.872-887, September 2000 [doi>10.1109/32.877847]
• 5: Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, and George C. Necula. JVer: A Java verifier. In CAV, pages 144--147, 2005.
• 6: Jong-Deok Choi , David Grove , Michael Hind , Vivek Sarkar, Efficient and precise modeling of exceptions for the analysis of Java programs, ACM SIGSOFT Software Engineering Notes, v.24 n.5, p.21-31, Sept. 1999
• 7: Michał Cierniak , Guei-Yuan Lueh , James M. Stichnoth, Practicing JUDO: Java under dynamic optimizations, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.13-26, June 18-21, 2000, Vancouver, British Columbia, Canada
• 8: Sophia Drossopoulou and Susan Eisenbach. Java is type safe -- probably. In ECOOP, pages 389--418, 1997.
• 9: Sophia Drossopoulou and Tanya Valkevych. Java exceptions throw no surprises. Technical report, March 2000.
• 10: Manuel Fahndrich , Jeffrey Foster , Jason Cu , Alexander Aiken, Tracking down Exceptions in Standard ML Programs, University of California at Berkeley, Berkeley, CA, 1998
• 11: Manuel Fähndrich , Alexander Aiken, Program Analysis Using Mixed Term and Set Constraints, Proceedings of the 4th International Symposium on Static Analysis, p.114-126, September 08-10, 1997
• 12: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 13: Kevin Glynn , Peter J. Stuckey , Martin Sulzmann , Harald Søndergaard, Exception analysis for non-strict languages, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.98-109, October 04-06, 2002, Pittsburgh, PA, USA
• 14: Paul Hudak , Simon Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph Fasel , María M. Guzmán , Kevin Hammond , John Hughes , Thomas Johnsson , Dick Kieburtz , Rishiyur Nikhil , Will Partain , John Peterson, Report on the programming language Haskell: a non-strict, purely functional language version 1.2, ACM SIGPLAN Notices, v.27 n.5, p.1-164, May 1992 [doi>10.1145/130697.130699]
• 15: Marieke Huisman , Bart Jacobs, Java Program Verification via a Hoare Logic with Abrupt Termination, Proceedings of the Third Internationsl Conference on Fundamental Approaches to Software Engineering: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.284-303, March 25-April 02, 2000
• 16: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 17: Jang-Wu Jo , Byeong-Mo Chang , Kwangkeun Yi , Kwang-Moo Choe, An uncaught exception analysis for Java, Journal of Systems and Software, v.72 n.1, p.59-69, June 2004 [doi>10.1016/S0164-1212(03)00057-8]
• 18: Simon Peyton Jones , Alastair Reid , Fergus Henderson , Tony Hoare , Simon Marlow, A semantics for imprecise exceptions, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.25-36, May 01-04, 1999, Atlanta, Georgia, United States
• 19: Gerwin Klein , Tobias Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.619-695, July 2006 [doi>10.1145/1146809.1146811]
• 20: K. Rustan M. Leino , Wolfram Schulte, Exception Safety for C#, Proceedings of the Software Engineering and Formal Methods, Second International Conference, p.218-227, September 28-30, 2004 [doi>10.1109/SEFM.2004.14]
• 21: H.H. Nguyen, C. David, S.C. Qin, and W.N. Chin. Automated verification of shape and size properties via separation logic. In VMCAI, Nice, France, January 2007.
• 22: Tobias Nipkow , David von Oheimb, Java_light is type-safe—definitely, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-170, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268960]
• 23: Takeshi Ogasawara , Hideaki Komatsu , Toshio Nakatani, A study of exception handling and its dynamic optimization in Java, Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.83-95, October 14-18, 2001, Tampa Bay, FL, USA
• 24: François Pessaux , Xavier Leroy, Type-based analysis of uncaught exceptions, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.276-290, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292565]
• 25: Norman Ramsey , Simon Peyton Jones, A single intermediate language that supports multiple implementations of exceptions, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.285-298, June 18-21, 2000, Vancouver, British Columbia, Canada
• 26: S. B. Sanjabi , C.-H. L. Ong, Fully abstract semantics of additive aspects by translation, Proceedings of the 6th international conference on Aspect-oriented software development, March 12-16, 2007, Vancouver, British Columbia, Canada [doi>10.1145/1218563.1218579]
• 27: Olin Shivers , David Fisher, Multi-return function call, Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, September 19-21, 2004, Snow Bird, UT, USA
• 28: Saurabh Sinha , Mary Jean Harrold, Analysis and Testing of Programs with Exception Handling Constructs, IEEE Transactions on Software Engineering, v.26 n.9, p.849-871, September 2000 [doi>10.1109/32.877846]
• 29: Eelco Visser. Program transformation with Stratego/XT. Rules, strategies, tools, and systems in Stratego/XT 0.9. Technical Report UU-CS-2004-011, Department of Information and Computing Sciences, Utrecht University, 2004.
• 30: Westley Weimer , George C. Necula, Exceptional situations and program reliability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.2, p.1-51, March 2008 [doi>10.1145/1330017.1330019]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Code generation

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
      D.3.4 Processors
          Subjects: Optimization

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs

General Terms:
Design, Languages, Theory

Keywords:
exceptions, optimization, translation