skip to main content
research-article
Open access

Relations as an abstraction for BDD-based program analysis

Published: 01 August 2008 Publication History

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]
Beazley, D. M. 1996. SWIG: An easy to use tool for integrating scripting languages with C and C++. In Proceedings of the 4th USENIX Tcl/Tk Workshop. 129--139.
[2]
Behrmann, G. 2006. The interactive BDD environment. http://iben.sourceforge.net/.
[3]
Berghammer, R., Leoniuk, B., and Milanese, U. 2002. Implementation of relational algebra using binary decision diagrams. In Proceedings of the 6th International Conference on Relational Methods in Computer Science. Lecture Notes in Computer Science, vol. 2561. 241--257.
[4]
Berndl, M., Lhoták, O., Qian, F., Hendren, L., and Umanee, N. 2003. Points-to analysis using BDDs. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 103--114.
[5]
Beyer, D., Noack, A., and Lewerentz, C. 2003. Simple and efficient relational querying of software structures. In Proceedings of the 10th Working Conference on Reverse Engineering (WCRE'03). Victoria, Canada, A. van Deursen, E. Stroulia, and M.-A. D. Storey, Eds. IEEE Computer Society, 216--227.
[6]
Bollig, B. and Wegener, I. 1996. Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45, 9, 993--1002.
[7]
Brabrand, C., Møller, A., and Schwartzbach, M. I. 2002. The <bigwig> project. ACM Trans. Internet Tech. 2, 2, 79--114.
[8]
Bryant, R. E. 1992. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24, 3, 293--318.
[9]
Christensen, A. S., Møller, A., and Schwartzbach, M. I. 2003. Extending Java for high-level Web service construction. ACM Trans. Prog. Lang. Syst. 25, 6, 814--875.
[10]
Clocksin, W. F. and Mellish, C. S. 1987. Programming in Prolog. Springer-Verlag, Berlin, Germany.
[11]
Codd, E. F. 1970. A relational model of data for large shared data banks. Commu. ACM 13, 6, 377--387.
[12]
Das, M. 2000. Unification-based pointer analysis with directional assignments. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 35--46.
[13]
Fahmy, H., Holt, R. C., and Cordy, J. R. 2001. Wins and losses of algebraic transformations of software architectures. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE'01). Coronado Island, San Diego, CA. IEEE Computer Society, 51--62.
[14]
Fähndrich, M., Foster, J. S., Su, Z., and Aiken, A. 1998. Partial online cycle elimination in inclusion constraint graphs. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 85--96.
[15]
Garcia-Molina, H., Ullman, J. D., and Widom, J. 2001. Database Systems: The Complete Book. Prentice Hall, Upper Saddle River, NJ.
[16]
Gosling, J., Joy, B., and Steele, G. L. 1996. The Java Language Specification. The Java Series. Addison-Wesley, Reading, MA.
[17]
Heintze, N. and Tardieu, O. 2001. Ultra-fast aliasing analysis using CLA: A million lines of C code in a second. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 254--263.
[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]
Lhoták, O. and Hendren, L. 2004. Jedd: a BDD-based relational extension of Java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 158--169.
[23]
Liang, D., Pennings, M., and Harrold, M. J. 2001. Extending and evaluating flow-insenstitive and context-insensitive points-to analyses for Java. In Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering. ACM Press, 73--79.
[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]
Minato, S. and Somenzi, F. 1997. Arithmetic boolean expression manipulator using BDDs. Formal Methods Syst. Design 10, 2/3, 221--242.
[27]
Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., and Malik, S. 2001. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Conference on Design Automation. ACM Press, 530--535.
[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]
Rountev, A., Milanova, A., and Ryder, B. G. 2001. Points-to analysis for Java using annotated constraints. In Proceedings of the Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA '01). ACM Press, 43--55.
[33]
Schmidt, J. W. 1977. Some high level language constructs for data of type relation. ACM Trans. Data Syst. 2, 3, 247--261.
[34]
Schwartz, J. T., Dewar, R. B. K., Dubinsky, E., and Schonberg, E. 1986. Programming with Sets—An Introduction to Setl. Springer, Berlin, Germany.
[35]
Shapiro, M. and Horwitz, S. 1997. Fast and accurate flow-insensitive points-to analysis. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 1--14.
[36]
Somenzi, F. 2006. CUDD: CU Decision Diagram Package. http://vlsi.colorado.edu/~fabio/CUDD/.
[37]
Tani, S., Hamaguchi, K., and Yajima, S. 1993. The complexity of the optimal variable ordering problems of shared binary decision diagrams. In Proceedings of the 4th International Symposium on Algorithms and Computation (ISAAC'93). Springer-Verlag, 389--398.
[38]
Tarjan, R. E. 1972. Depth first search and linear graph algorithms. J. Comput. 1, 2, 146--160.
[39]
Ullman, J. D. 1988. Principles of Database and Knowledge-Base Systems, Vol. I. Computer Science Press.
[40]
Ullman, J. D. 1989. Principles of Database and Knowledge-Base Systems, Vol. II. Computer Science Press.
[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]
Whaley, J. and Lam, M. S. 2002. An efficient inclusion-based points-to analysis for strictly-typed languages. In Proceedings of the 9th International Symposium on Static Analysis (SAS'02). Lecture Notes in Computer Science, vol. 2477. 180--195.
[45]
Whaley, J. and Lam, M. S. 2004. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 131--144.
[46]
Zhang, L. and Malik, S. 2003. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Proceedings of Design, Automation and Test in Europe (DATE'03). 880--885.
[47]
Zhu, J. 2002. Symbolic pointer analysis. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design. ACM Press, 150--157.
[48]
Zhu, J. and Calman, S. 2004. Symbolic pointer analysis revisited. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 145--157.

Cited By

View all
  • (2013)Alias analysis for object-oriented programsAliasing in Object-Oriented Programming10.5555/2554511.2554523(196-232)Online publication date: 1-Jan-2013
  • (2013)Alias Analysis for Object-Oriented ProgramsAliasing in Object-Oriented Programming. Types, Analysis and Verification10.1007/978-3-642-36946-9_8(196-232)Online publication date: 2013
  • (2011)Pick your contexts wellProceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1926385.1926390(17-30)Online publication date: 26-Jan-2011
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems
ACM Transactions on Programming Languages and Systems  Volume 30, Issue 4
July 2008
358 pages
ISSN:0164-0925
EISSN:1558-4593
DOI:10.1145/1377492
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 2008
Accepted: 01 March 2007
Received: 01 June 2006
Published in TOPLAS Volume 30, Issue 4

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Binary decision diagrams
  2. Boolean formula satisfiability
  3. Java
  4. language design
  5. physical domain assignment
  6. points-to analysis
  7. program analysis
  8. relations

Qualifiers

  • Research-article
  • Research
  • Refereed

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)72
  • Downloads (Last 6 weeks)9
Reflects downloads up to 02 Mar 2025

Other Metrics

Citations

Cited By

View all
  • (2013)Alias analysis for object-oriented programsAliasing in Object-Oriented Programming10.5555/2554511.2554523(196-232)Online publication date: 1-Jan-2013
  • (2013)Alias Analysis for Object-Oriented ProgramsAliasing in Object-Oriented Programming. Types, Analysis and Verification10.1007/978-3-642-36946-9_8(196-232)Online publication date: 2013
  • (2011)Pick your contexts wellProceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1926385.1926390(17-30)Online publication date: 26-Jan-2011
  • (2011)Pick your contexts wellACM SIGPLAN Notices10.1145/1925844.192639046:1(17-30)Online publication date: 26-Jan-2011

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media