Towards scalable flow and context sensitive pointer analysis

ABSTRACT

Pointer analysis, a classic problem in software program analysis, has emerged as an important problem to solve in design automation, at a time when complex designs, specified in the form of C code, need to be synthesized or verified. However, precise pointer analysis algorithms that are both context and flow sensitive (FSCS), have not been shown to scale. In this paper, we report a new solution for FSCS analysis, which can evaluate the program states of all program points under billions of different calling paths. Our solution extends the recently proposed symbolic pointer analysis (SPA) technology, which exploits the efficiency of Binary Decision Diagrams (BDDs). With our new strategy of problem solving, called superposed symbolic computation, and its application on our generic pointer analysis framework, we are able to report the first result on all SPEC2000 benchmarks that completes context sensitive, flow insensitive analysis in seconds, and context sensitive, flow sensitive analysis in minutes.

REFERENCES

• 1: 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
• 2: 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]
• 3: 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.
• 4: Venkatesan T. Chakaravarthy, New results on the computability and complexity of points--to analysis, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.115-125, January 15-17, 2003, New Orleans, Louisiana, USA
• 5: 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
• 6: 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.
• 7: Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , F. Kenneth Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.451-490, Oct. 1991 [doi>10.1145/115372.115320]
• 8: S. A. Edwards. The challenges of hardware synthesis from C-like languages. In Proceedings of the International Workshop of Logic and Synthesis (IWLS), June 2004.
• 9: 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
• 10: 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
• 11: 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
• 12: D. Gajski, J. Zhu, D. Doemer, A. Gerstlauer, and S. Zhao. SpecC: Specification Language and Methodology. Kluwer Academic Publishers, Boston, March 2000.
• 13: 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
• 14: 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]
• 15: 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
• 16: 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
• 17: Stan Liao , Steve Tjiang , Rajesh Gupta, An efficient implementation of reactivity for modeling hardware in the scenic design environment, Proceedings of the 34th annual conference on Design automation, p.70-75, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266037]
• 18: Giovanni De Micheli, Hardware synthesis from C/C++ models, Proceedings of the conference on Design, automation and test in Europe, p.80-es, January 1999, Munich, Germany [doi>10.1145/307418.307527]
• 19: Preeti Ranjan Panda , Luc Semeria , Giovanni de Micheli, Cache-efficient memory layout of aggregate data structures, Proceedings of the 14th international symposium on Systems synthesis, September 30-October 03, 2001, Montréal, P.Q., Canada [doi>10.1145/500001.500026]
• 20: An introduction to quantum computing for non-physicists, ACM Computing Surveys (CSUR), v.32 n.3, p.300-335, Sept. 2000 [doi>10.1145/367701.367709]
• 21: L. Semeria and G. D. Micheli. Resolution, optimization, and encoding of pointer variables for the behavioral synthesis from C. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, February 2001.
• 22: L. Semeria, K. Sata, and G. D. Micheli. Synthesis of hardware models in C with pointers and complex data structures. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, February 2001.
• 23: F. Somenzi. CUDD: Binary decision diagram package release. http://vlsi.Colorado.EDU/~fabio/CUDD/cuddIntro.html, 1998.
• 24: SystemC Web Site. http://www.systemc.org.
• 25: 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
• 26: 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
• 27: J. Zhu, Static memory allocation by pointer analysis and coloring, Proceedings of the conference on Design, automation and test in Europe, p.785-790, March 2001, Munich, Germany
• 28: 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]
• 29: 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
• 30: J. Zhu, R. Doemer, and D. Gajski. Syntax and semantics of SpecC+ language. In Proceedings of the Ninth Workshop on Synthesis and System Integration of Mixed Technologies, Japan, December 1997.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

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

General Terms:
Algorithms, Experimentation, Languages

Keywords:
binary decision diagrams, high-level synthesis, pointer analysis