Jedd: a BDD-based relational extension of Java

ABSTRACT

In this paper we present Jedd, a language extension to Java that supports a convenient way of programming with Binary Decision Diagrams (BDDs). The Jedd language abstracts BDDs as database-style relations and operations on relations, and provides static type rules to ensure that relational operations are used correctly.The paper provides a description of the Jedd language and reports on the design and implementation of the Jedd translator and associated runtime system. Of particular interest is the approach to assigning attributes from the high-level relations to physical domains in the underlying BDDs, which is done by expressing the constraints as a SAT problem and using a modern SAT solver to compute the solution. Further, a runtime system is defined that handles memory management issues and supports a browsable profiling tool for tuning the key BDD operations.The motivation for designing Jedd was to support the development of whole program analyses based on BDDs, and we have used Jedd to express five key interrelated whole program analyses in our Soot compiler framework. We provide some examples of this application and discuss our experiences using Jedd.

REFERENCES

• 1: Thomas Ball , Sriram K. Rajamani, Bebop: a path-sensitive interprocedural dataflow engine, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.97-103, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379690]
• 2: D. M. Beazley. SWIG: An easy to use tool for integrating scripting languages with C and C++. In Proceedings of the 4th USENIX Tcl/Tk Workshop, pages 129--139, July 1996.
• 3: Gerd Behrmann. The interactive BDD environment. http://iben.sourceforge.net/.
• 4: Rudolf Berghammer , Barbara Leoniuk , Ulf Milanese, Implementation of Relational Algebra Using Binary Decision Diagrams, Revised Papers from the 6th International Conference and 1st Workshop of COST Action 274 TARSKI on Relational Methods in Computer Science, p.241-257, October 16-21, 2001
• 5: Marc Berndl , Ondrej Lhoták , Feng Qian , Laurie Hendren , Navindra Umanee, Points-to analysis using BDDs, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 6: Dirk Beyer , Andreas Noack , Claus Lewerentz, Simple and Efficient Relational Querying of Software Structures, Proceedings of the 10th Working Conference on Reverse Engineering, p.216, November 13-17, 2003
• 7: Claus Brabrand , Anders Møller , Michael I. Schwartzbach, The <bigwig> project, ACM Transactions on Internet Technology (TOIT), v.2 n.2, p.79-114, May 2002 [doi>10.1145/514183.514184]
• 8: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 9: W. F. Clocksin , Christopher S. Mellish, Programming in Prolog (3rd ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 10: E. F. Codd, A relational model of data for large shared data banks, Communications of the ACM, v.13 n.6, p.377-387, June 1970 [doi>10.1145/362384.362685]
• 11: H. M. Fahmy , R. C. Holt , James R. Cordy, Wins and Losses of Algebraic Transformations of Software Architectures, Proceedings of the 16th IEEE international conference on Automated software engineering, p.51, November 26-29, 2001
• 12: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 13: Ondřej Lhoták and Laurie Hendren. Jedd: A BDD-based relational extension of Java. Technical Report 2003-7, McGill University, Sable Research Group, 2003.
• 14: Jorn Lind-Nielsen. BuDDy, A Binary Decision Diagram Package. Department of Information Technology, Technical University of Denmark, http://www.itu.dk/research/buddy/.
• 15: Roman Manevich , G. Ramalingam , John Field , Deepak Goyal , Mooly Sagiv, Compactly Representing First-Order Structures for Static Analysis, Proceedings of the 9th International Symposium on Static Analysis, p.196-212, September 17-20, 2002
• 16: Erik Meijer and Wolfram Schulte. Unifying tables, objects, and documents. In Workshop on Declarative Programming in the Context of Object-Oriented Languages, pages 145--166, August 2003.
• 17: Shin-Ichi Minato , F. Somenzi, Arithmetic Boolean Expression Manipulator Using BDDs, Formal Methods in System Design, v.10 n.2-3, p.221-242, April -May 1997 [doi>10.1023/A:1008643722423]
• 18: Shin-ichi Minato, Zero-suppressed BDDs for set manipulation in combinatorial problems, Proceedings of the 30th international conference on Design automation, p.272-277, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164890]
• 19: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 20: Marcus Nilsson. GBDD - A package for representing relations with BDDs. http://user.it.uu.se/-~marcusn/projects/rmc/docs/gbdd/index.html.
• 21: N. Nystrom, M. R. Clarkson, and A. C. Myers. Polyglot: An extensible compiler framework for Java. In 12th International Conference on Compiler Construction, volume 2622 of LNCS, pages 138--152, 2003.
• 22: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 23: J. T. Schwartz , R. B. Dewar , E. Schonberg , E. Dubinsky, Programming with sets; an introduction to SETL, Springer-Verlag New York, Inc., New York, NY, 1986
• 24: Ganesh Sittampalam , Oege de Moor , Ken Friis Larsen, Incremental execution of transformation specifications, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-38, January 14-16, 2004, Venice, Italy
• 25: Fabio Somenzi. CUDD: CU Decision Diagram Package. Department of Electrical and Computer Engineering, University of Colorado at Boulder, http://vlsi.colorado.edu/~fabio/CUDD/.
• 26: Arash Vahidi. Arash's Java interface to BDDs. http://www.chl.chalmers.se/~vahidi/bdd/bdd.html.
• 27: Raja Vallée-Rai , Etienne Gagnon , Laurie J. Hendren , Patrick Lam , Patrice Pominville , Vijay Sundaresan, Optimizing Java Bytecode Using the Soot Framework: Is It Feasible?, Proceedings of the 9th International Conference on Compiler Construction, p.18-34, March 25-April 02, 2000
• 28: John Whaley. JavaBDD - Java binary decision diagram library. http://javabdd.sourceforge.net/.
• 29: John Whaley , Monica S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 30: Lintao Zhang , Sharad Malik, Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications, Proceedings of the conference on Design, Automation and Test in Europe, p.10880, March 03-07, 2003
• 31: Xiangyu Zhang , Rajiv Gupta , Youtao Zhang, Efficient Forward Computation of Dynamic Slices Using Reduced Ordered Binary Decision Diagrams, Proceedings of the 26th International Conference on Software Engineering, p.502-511, May 23-28, 2004
• 32: Jianwen Zhu , Silvian Calman, Symbolic pointer analysis revisited, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors

  E. Data
  E.2 DATA STORAGE REPRESENTATIONS

General Terms:
Design, Experimentation, Languages

Keywords:
Java, binary decision diagrams, boolean formula satisfiability, language design, program analysis, relations