Marc Berndl
Laurie Hendren
ABSTRACT
This paper reports on a new approach to solving a subset-based points-to analysis for Java using Binary Decision Diagrams (BDDs). In the model checking community, BDDs have been shown very effective for representing large sets and solving very large verification problems. Our work shows that BDDs can also be very effective for developing a points-to analysis that is simple to implement and that scales well, in both space and time, to large programs.The paper first introduces BDDs and operations on BDDs using some simple points-to examples. Then, a complete subset-based points-to algorithm is presented, expressed completely using BDDs and BDD operations. This algorithm is then refined by finding appropriate variable orderings and by making the algorithm propagate sets incrementally, in order to arrive at a very efficient algorithm. Experimental results are given to justify the choice of variable ordering, to demonstrate the improvement due to incrementalization, and to compare the performance of the BDD-based solver to an efficient hand-coded graph-based solver. Finally, based on the results of the BDD-based solver, a variety of BDD-based queries are presented, including the points-to query.
- Lars Ole Andersen. Program Analysis and Specialization for the C Programming Language, May 1994. Ph.D thesis, DIKU, University of Copenhagen.]]Google Scholar
- Ashes suite collection http://www.sable.mcgill.ca/software/.]]Google Scholar
- Thomas Ball and Sriram K. Rajamani. Bebop: A Path-sensitive Interprocedural Dataflow Engine. In Proceedings of PASTE'01, pages 97--103, Jun 2001.]] Google ScholarDigital Library
- David Basin, Stefan Friedrich, Marek Gawkowski, and Joachim Posegga. Bytecode Model Checking: An Experimental Analysis. In Dragan Bosnacki and Stefan Leue, editors, Model Checking Software, 9th International SPIN Workshop, volume 2318 of LNCS, pages 42--59. Springer-Verlag, Apr 2002.]] Google ScholarDigital Library
- Randal E. Bryant. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams. ACM Computing Surveys, 24(3):293--318, 1992.]] Google ScholarDigital Library
- Manuvir Das. Unification-based pointer analysis with directional assignments. In Proceedings of PLDI'00, pages 35--46, Jun 2000.]] Google ScholarDigital Library
- Jeffrey Dean, David Grove, and Craig Chambers. Optimization of object-oriented programs using static class hierarchy analysis. In Walter G. Olthoff, editor, ECOOP'95---Object-Oriented Programming, 9th European Conference, volume 952 of Lecture Notes in Computer Science, pages 77--101, \AAarhus, Denmark, Aug 1995. Springer.]] Google ScholarDigital Library
- Matthew B. Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina S. Pasareanu, Robby, Hongjun Zheng, and W Visser. Tool-Supported Program Abstraction for Finite-State Verification. In Proceedings of ICSE, pages 177--187, 2001.]] Google ScholarDigital Library
- Maryam Emami, Rakesh Ghiya, and Laurie J. Hendren. Context-sensitive interprocedural points-to analysis in the presence of function pointers. In Proceedings of PLDI'94, pages 242--256, 1994.]] Google ScholarDigital Library
- Manuel Fähndrich, Jeffery S. Foster, Zhendong Su, and Alexander Aiken. Partial online cycle elimination in inclusion constraint graphs. In Proceedings of PLDI'98, pages 85--96, Montreal, Canada, Jun 1998.]] Google ScholarDigital Library
- Nevin Heintze. Analysis of large code bases: The compile-link-analyze model, 1999. http://cm.bell-labs.com/cm/cs/who/nch/cla.ps.]]Google Scholar
- Nevin Heintze and Olivier Tardieu. Ultra-fast aliasing analysis using CLA: A million lines of C code in a second. In Proceedings of PLDI'01, pages 254--263, June 2001.]] Google ScholarDigital Library
- Pascal Van Hentenryck, Agostino Cortesi, and Baudouin Le Charlier. Evaluation of the domain Prop. Journal of Logic Programming, 23(3):237--278, 1995.]]Google ScholarCross Ref
- Michael Hind. Pointer Analysis: Haven't We Solved This Problem Yet? In Proceedings of PASTE'01, pages 54--61, Jun 2001.]] Google ScholarDigital Library
- jEdit: Open source programmer's text editor. http://www.jedit.org/.]]Google Scholar
- J.R. Burch, E.M. Clarke, D.E. Long, K.L. MacMillan, and D.L. Dill. Symbolic Model Checking for Sequential Circuit Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401--424, 1994.]]Google ScholarDigital Library
- Ondrej Lhoták. Spark: A flexible points-to analysis framework for Java. Master's thesis, McGill University, December 2002.]]Google Scholar
- Ondrej Lhoták and Laurie Hendren. Scaling Java points-to analysis using Spark. In G. Hedin, editor, Compiler Construction, 12th International Conference, volume 2622 of LNCS, pages 153--169, Warsaw, Poland, April 2003. Springer.]]Google ScholarDigital Library
- Donglin Liang, Maikel Pennings, and Mary Jean Harrold. Extending and evaluating flow-insensitive and context-insensitive points-to analyses for Java. In Proceedings of PASTE'01, pages 73--79, 2001.]] Google ScholarDigital Library
- Jørn Lind-Nielsen. BuDDy, A Binary Decision Diagram Package. Department of Information Technology, Technical University of Denmark, http://www.itu.dk/research/buddy/.]]Google Scholar
- R. Manevich, G. Ramalingam, J. Field, D. Goyal, and M. Sagiv. Compactly Representing First-Order Structures for Static Analysis. In Manuel V. Hermenegildo and German Puebla, editors, Proceedings of SAS'02, volume 2477 of LNCS, Madrid, Spain, September 2002. Springer.]] Google ScholarDigital Library
- Vincenzo Martena and Pierluigi San Pietro. Alias Analysis by Means of a Model Checker. In R. Wilhelm, editor, Compiler Construction, 10th International Conference, volume 2027 of LNCS, pages 3--19, Genova, Italy, April 2001. Springer.]] Google ScholarDigital Library
- Cristoph Meinel and Thorsten Theobald. Algorithms and Data Structures in VLSI Design. Springer, 1998.]] Google ScholarDigital Library
- Atanas Rountev and Satish Chandra. Off-line Variable Substitution for Scaling Points-to Analysis. In Proceedings of PLDI'00, pages 47--56, Jun 2000.]] Google ScholarDigital Library
- Atanas Rountev, Ana Milanova, and Barbara Ryder. Points-to analysis for Java using annotated constraints. In Proceedings of OOPSLA'01, pages 43--55, 2001.]] Google ScholarDigital Library
- David A. Schmidt. Data Flow Analysis is Model Checking of Abstract Interpretations. In Proceedings of POPL'98, pages 38--48, Jan 1998.]] Google ScholarDigital Library
- David A. Schmidt and Bernhard Steffen. Program analysis as model checking of abstract interpretations. In Proceedings of SAS'98, pages 351--380, 1998.]]Google Scholar
- Marc Shapiro and Susan Horwitz. Fast and accurate flow-insensitive points-to analysis. In Proceedings of POPL'97, pages 1--14, Paris, France, Jan 1997.]] Google ScholarDigital Library
- John W. Sias, Wen mei W. Hwu, and David I. August. Accurate and Efficient Predicate Analysis with Binary Decision Diagrams. In Proceedings of the 33rd annual IEEE/ACM International Symposium on Microarchitecture, pages 112--123, Dec 2000.]] Google ScholarDigital Library
- SPEC jbb200 benchmark http://www.spec.org/osg/jbb2000/.]]Google Scholar
- SPEC jvm98 benchmarks http://www.spec.org/osg/jvm98/.]]Google Scholar
- Bjarne Steensgaard. Points-to analysis in almost linear time. In Proceedings of POPL'96, pages 32--41, Jan 1996.]] Google ScholarDigital Library
- Vijay Sundaresan, Laurie Hendren, Chrislain Razafimahefa, Raja Vallée-Rai, Patrick Lam, Etienne Gagnon, and Charles Godin. Practical virtual method call resolution for Java. In Proceedings of the 2000 OOPSLA, pages 264--280, 2000.]] Google ScholarDigital Library
- John Whaley and Monica Lam. An efficient inclusion-based points-to analysis for strictly-typed languages. In Proceedings of SAS'02, volume 2477 of LNCS, 2002.]] Google ScholarDigital Library
- Aiguo Xie and Peter A. Beerel. Implicit enumeration of strongly connected components. In International Conference on Computer-Aided Design, pages 37--40, Nov 1999.]] Google ScholarDigital Library
Index Terms
- Points-to analysis using BDDs
Recommendations
Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation
We present Paddle, a framework of BDD-based context-sensitive points-to and call graph analyses for Java, as well as client analyses that use their results. Paddle supports several variations of context-sensitive analyses, including call site strings ...
Points-to analysis using BDDs
This paper reports on a new approach to solving a subset-based points-to analysis for Java using Binary Decision Diagrams (BDDs). In the model checking community, BDDs have been shown very effective for representing large sets and solving very large ...
Using XBDDs and ZBDDs in points-to analysis
Binary decision diagrams (BDDs) have recently become widely accepted as a space-efficient method of representing relations in points-to or reference analyses. When BDDs are used to represent relations, each element of a domain is assigned a bit pattern ...
Comments