Relations as an abstraction for BDD-based program analysis

ABSTRACT

In this article 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 article 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 interrelated whole program analyses based on BDDs. We have successfully used Jedd to build Paddle, a framework of context-sensitive program analyses, including points-to analysis and call graph construction, as well as several client analyses.

REFERENCES

• 1: David M. Beazley, SWIG: an easy to use tool for integrating scripting languages with C and C++, Proceedings of the 4th conference on USENIX Tcl/Tk Workshop, 1996, p.15-15, July 10-13, 1996, Monterey, California
• 2: Behrmann, G. 2006. The interactive BDD environment. http://iben.sourceforge.net/.
• 3: 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
• 4: 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
• 5: 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
• 6: Beate Bollig , Ingo Wegener, Improving the Variable Ordering of OBDDs Is NP-Complete, IEEE Transactions on Computers, v.45 n.9, p.993-1002, September 1996 [doi>10.1109/12.537122]
• 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: Aske Simon Christensen , Anders Møller , Michael I. Schwartzbach, Extending Java for high-level Web service construction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.6, p.814-875, November 2003 [doi>10.1145/945885.945890]
• 10: W. F. Clocksin , C. S. Mellish, Programming in Prolog, Springer-Verlag New York, Inc., New York, NY, 1987
• 11: 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]
• 12: Manuvir Das, Unification-based pointer analysis with directional assignments, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.35-46, June 18-21, 2000, Vancouver, British Columbia, Canada
• 13: 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
• 14: Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su , Alexander Aiken, Partial online cycle elimination in inclusion constraint graphs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.85-96, June 17-19, 1998, Montreal, Quebec, Canada
• 15: Jeffrey D. Ullman , Hector Garcia-Molina , Jennifer Widom, Database Systems: The Complete Book, Prentice Hall PTR, Upper Saddle River, NJ, 2001
• 16: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 17: Nevin Heintze , Olivier Tardieu, Ultra-fast aliasing analysis using CLA: a million lines of C code in a second, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.254-263, June 2001, Snowbird, Utah, United States
• 18: Hipp, D. R. 2006. SQLite: an embeddable database engine. http://www.sqlite.org/.
• 19: Lhoták, O. 2002. Spark: A flexible points-to analysis framework for Java. M.S. thesis, McGill University.
• 20: Lhoták, O. 2006. Program analysis using binary decision diagrams. Ph.D. thesis, McGill University.
• 21: Lhoták, O. and Hendren, L. 2003. Scaling Java points-to analysis using Spark. In Proceedings of the 12th International Conference on Compiler Construction. G. Hedin, Ed. Lecture Notes in Computer Science, vol. 2622. Springer, 153--169.
• 22: Ondřej Lhoták , Laurie Hendren, Jedd: a BDD-based relational extension of Java, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 23: Donglin Liang , Maikel Pennings , Mary Jean Harrold, Extending and evaluating flow-insenstitive and context-insensitive points-to analyses for Java, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.73-79, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379676]
• 24: Lind-Nielsen, J. 2006. BuDDy, A Binary Decision Diagram Package. http://buddy.sourceforge.net/.
• 25: Meijer, E. and Schulte, W. 2003. Unifying tables, objects, and documents. In Workshop on Declarative Programming in the Context of Object-Oriented Languages. 145--166.
• 26: 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]
• 27: 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]
• 28: Nilsson, M. 2006. GBDD -- A package for representing relations with BDDs. http://www.regularmodelchecking.com/software/docs/stable/gbdd/index.html.
• 29: Nystrom, N., Clarkson, M. R., and Myers, A. C. 2003. Polyglot: An extensible compiler framework for Java. In Proceedings of the 12th International Conference on Compiler Construction. Lecture Notes in Computer Science, vol. 2622. 138--152.
• 30: Poskanzer, J. 2006. thttpd: tiny/turbo/throttling HTTP server. http://www.acme.com/software/thttpd/.
• 31: Qian, F. 2006. SableJBDD, A Java binary decision diagram package. http://www.sable.mcgill.ca/~fqian/SableJBDD/.
• 32: Atanas Rountev , Ana Milanova , Barbara G. Ryder, Points-to analysis for Java using annotated constraints, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.43-55, October 14-18, 2001, Tampa Bay, FL, USA
• 33: Joachim W. Schmidt, Some high level language constructs for data of type relation, ACM Transactions on Database Systems (TODS), v.2 n.3, p.247-261, Sept. 1977 [doi>10.1145/320557.320568]
• 34: 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
• 35: Marc Shapiro , Susan Horwitz, Fast and accurate flow-insensitive points-to analysis, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 15-17, 1997, Paris, France [doi>10.1145/263699.263703]
• 36: Somenzi, F. 2006. CUDD: CU Decision Diagram Package. http://vlsi.colorado.edu/~fabio/CUDD/.
• 37: Seiichiro Tani , Kiyoharu Hamaguchi , Shuzo Yajima, The Complexity of the Optimal Variable Ordering Problems of Shared Binary Decision Diagrams, Proceedings of the 4th International Symposium on Algorithms and Computation, p.389-398, December 15-17, 1993
• 38: Tarjan, R. E. 1972. Depth first search and linear graph algorithms. J. Comput. 1, 2, 146--160.
• 39: Jeffrey D. Ullman, Principles of database and knowledge-base systems, Vol. I, Computer Science Press, Inc., New York, NY, 1988
• 40: Jeffrey D. Ullman, Principles of database and knowledge-base systems, Vol. I, Computer Science Press, Inc., New York, NY, 1988
• 41: Vahidi, A. 2006. JBDD, a Java interface to CUDD and BuDDY. http://javaddlib.sourceforge.net/jbdd/index.html.
• 42: Whaley, J. 2006a. bddbddb. http://bddbddb.sourceforge.net.
• 43: Whaley, J. 2006b. JavaBDD. http://javabdd.sourceforge.net.
• 44: John Whaley , Monica S. Lam, An Efficient Inclusion-Based Points-To Analysis for Strictly-Typed Languages, Proceedings of the 9th International Symposium on Static Analysis, p.180-195, September 17-20, 2002
• 45: 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
• 46: 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
• 47: Jianwen Zhu, Symbolic pointer analysis, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.150-157, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774594]
• 48: 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:
Binary decision diagrams, Boolean formula satisfiability, Java, language design, physical domain assignment, points-to analysis, program analysis, relations