Symbolic pointer analysis revisited

ABSTRACT

Pointer analysis is a critical problem in optimizing compiler, parallelizing compiler, software engineering and most recently, hardware synthesis. While recent efforts have suggested symbolic method, which uses Bryant's Binary Decision Diagram as an alternative to capture the point-to relation, no speed advantage has been demonstrated for context-insensitive analysis, and results for context-sensitive analysis are only preliminary.In this paper, we refine the concept of symbolic transfer function proposed earlier and establish a common framework for both context-insensitive and context-sensitive pointer analysis. With this framework, our transfer function of a procedure can abstract away the impact of its callers and callees, and represent its point-to information completely, compactly and canonically. In addition, we propose a symbolic representation of the invocation graph, which can otherwise be exponentially large. In contrast to the classical frameworks where context-sensitive point-to information of a procedure has to be obtained by the application of its transfer function exponentially many times, our method can obtain point-to information of all contexts in a single application. Our experimental evaluation on a wide range of C benchmarks indicates that our context-sensitive pointer analysis can be made almost as fast as its context-insensitive counterpart.

REFERENCES

• 1: SPEC CPU2000 benchmarks. http://www.specbench.org/cpu2000/.
• 2: S. B. Akers. Binary decision diagrams. IEEE Transactions on Computer, C-27(6):509--516, June 1978.
• 3: O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, Computer Science Department, University of Copenhagen, 1994.
• 4: T. Ball and T. Millstein. Polymorphic predicate abstraction. Technical Report MSR-TR-2001-10, Microsoft Research, June 24, 2003.
• 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: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 7: J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In International Conference on Very Large Scale Integration, Edinburgh, Scotland, 1991.
• 8: J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, (13), 1994.
• 9: J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, Washington, DC, 1990.
• 10: Ramkrishna Chatterjee , Barbara G. Ryder , William A. Landi, Relevant context inference, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.133-146, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292554]
• 11: Ben-Chung Cheng , Wen-Mei W. Hwu, Modular interprocedural pointer analysis using access paths: design, implementation, and evaluation, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.57-69, June 18-21, 2000, Vancouver, British Columbia, Canada
• 12: O. Coudert, C. Berthet, and J. C. Madre. A unified framework for the formal verification of sequential circuits. In Proceedings of the International Conference on Computer-Aided Design, pages 126--129, November 1990.
• 13: O. Coudert and J. C. Madre. Symbolic computation of the valid states of a sequential machine: Algorithms and discussion. In ACM Workshop on Formal Methods in VLSI Design, 1991.
• 14: Maryam Emami , Rakesh Ghiya , Laurie J. Hendren, Context-sensitive interprocedural points-to analysis in the presence of function pointers, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.242-256, June 20-24, 1994, Orlando, Florida, United States
• 15: Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su , Alexander Aiken, Partial online cycle elimination in inclusion constraint graphs, ACM SIGPLAN Notices, v.33 n.5, p.85-96, May 1998
• 16: Manuel Fähndrich , Jakob Rehof , Manuvir Das, Scalable context-sensitive flow analysis using instantiation constraints, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.253-263, June 18-21, 2000, Vancouver, British Columbia, Canada
• 17: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, Polymorphic versus Monomorphic Flow-Insensitive Points-to Analysis for C, Proceedings of the 7th International Symposium on Static Analysis, p.175-198, June 29-July 01, 2000
• 18: Daniel D. Gajski, Principles of digital design, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 19: 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
• 20: Michael Hind, Pointer analysis: haven't we solved this problem yet?, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.54-61, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379665]
• 21: Michael Hind , Michael Burke , Paul Carini , Jong-Deok Choi, Interprocedural pointer alias analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.4, p.848-894, July 1999 [doi>10.1145/325478.325519]
• 22: Michael Hind , Anthony Pioli, Assessing the Effects of Flow-Sensitivity on Pointer Alias Analyses, Proceedings of the 5th International Symposium on Static Analysis, p.57-81, September 14-16, 1998
• 23: Michael Hind , Anthony Pioli, Which pointer analysis should I use?, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.113-123, August 21-24, 2000, Portland, Oregon, United States
• 24: William Landi , Barbara G. Ryder, A safe approximate algorithm for interprocedural aliasing, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.235-248, June 15-19, 1992, San Francisco, California, United States
• 25: Chunho Lee , Miodrag Potkonjak , William H. Mangione-Smith, MediaBench: a tool for evaluating and synthesizing multimedia and communicatons systems, Proceedings of the 30th annual ACM/IEEE international symposium on Microarchitecture, p.330-335, December 01-03, 1997, Research Triangle Park, North Carolina, United States
• 26: 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
• 27: Donglin Liang , Mary Jean Harrold, Efficient Computation of Parameterized Pointer Information for Interprocedural Analyses, Proceedings of the 8th International Symposium on Static Analysis, p.279-298, July 16-18, 2001
• 28: Ana Milanova , Atanas Rountev , Barbara G. Ryder, Parameterized object sensitivity for points-to and side-effect analyses for Java, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 29: In-Ho Moon , James H. Kukula , Kavita Ravi , Fabio Somenzi, To split or to conjoin: the question in image computation, Proceedings of the 37th conference on Design automation, p.23-28, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337305]
• 30: Atanas Rountev , Satish Chandra, Off-line variable substitution for scaling points-to analysis, ACM SIGPLAN Notices, v.35 n.5, p.47-56, May 2000
• 31: Erik Ruf, Context-insensitive alias analysis reconsidered, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.13-22, June 18-21, 1995, La Jolla, California, United States
• 32: B. Ryder. Prolangs analysis framework. http://www.prolangs.rutgers.edu.
• 33: 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]
• 34: M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, pages 189--234. Prentice Hall, 1981.
• 35: F. Somenzi. CUDD: Binary decision diagram package release. http://vlsi.Colorado.EDU/fabio/CUDD/cuddIntro.html, 1998.
• 36: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 37: R. Tarjan. Depth first search and linear graph algorithms. SIAM Journal of Computing, 1(2):146--160, 1972.
• 38: 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
• 39: Robert P. Wilson , Monica S. Lam, Efficient context-sensitive pointer analysis for C programs, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.1-12, June 18-21, 1995, La Jolla, California, United States
• 40: Sean Zhang , Barbara G. Ryder , William Landi, Program decomposition for pointer aliasing: a step toward practical analyses, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.81-92, October 16-18, 1996, San Francisco, California, United States
• 41: 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]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers; Optimization

General Terms:
Experimentation, Languages

Keywords:
binary decision diagrams, call graph construction, pointer analysis