From generic to specific: off-line optimization for a general constraint solver

ABSTRACT

A general constraint solver simplifies the implementation of program analyses because constraint generation can then be separated from constraint solving. In return, a general solver often needs to sacrifice performance for generality. We describe a strategy that given a set of constraints first performs off-line optimizations (performed before the execution of the solver) which enable a solver to find (potential) equivalences between analysis variables so as to reduce the problem space and thus improve performance. The idea is that different analyses use different subsets of constraints. As a result, a specific property may hold for the subsets and a specific optimization can be conducted on the constraints.

To be concrete, we introduce two off-line algorithms and apply them on the constraints generated by Andersen's pointer analysis, or by a reaching definitions analysis, respectively. The experimental results show that these algorithms dramatically reduce the effort of solving the constraints, by detecting and unifying equivalent analysis variables. Furthermore, because these optimizations are conducted on constraints instead of analysis specifications, we can reuse them for different analyses and even automatically detect the off-line analyses to be used.

REFERENCES

• 1: L. O. Andersen. Program analysis and specialization for the C programming language. PhD thesis, DIKU, University of Copenhagen, May 1994.
• 2: M. Buchholtz, H. R. Nielson, and F. Nielson. Experiments with succinct solvers. Technical Report IMM-TR-2002-4, Technical University of Denmark, 2002.
• 3: 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
• 4: 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
• 5: Ben Hardekopf , Calvin Lin, The ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 6: Nevin Heintze , David McAllester, Linear-time subtransitive control flow analysis, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.261-272, June 16-18, 1997, Las Vegas, Nevada, United States
• 7: 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
• 8: Fritz Henglein, Global tagging optimization by type inference, Proceedings of the 1992 ACM conference on LISP and functional programming, p.205-215, June 22-24, 1992, San Francisco, California, United States
• 9: A. Kanamori and D. Weise. Worklist management strategies. Technical Report MSR-TR-94-12, Microsoft Research, 1994.
• 10: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 11: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 12: Flemming Nielson , Hanne Riis Nielson , Helmut Seidl, A succinct solver for ALFP, Nordic Journal of Computing, v.9 n.4, p.335-372, Winter 2002
• 13: David J. Pearce , Paul H. J. Kelly , Chris Hankin, Online Cycle Detection and Difference Propagation: Applications to Pointer Analysis, Software Quality Control, v.12 n.4, p.311-337, December 2004 [doi>10.1023/B:SQJO.0000039791.93071.a2]
• 14: David J. Pearce , Paul H.J. Kelly , Chris Hankin, Efficient field-sensitive pointer analysis of C, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.1, p.4-es, November 2007 [doi>10.1145/1290520.1290524]
• 15: H. Pilegaard. A feasibility study: The Succinct Solver v2.0, XSB prolog v2.6, and flow-logic based program analysis for carmel. Technical Report SECSAFE-IMM-008-1.0, Technical University of Denmark, 2003.
• 16: Konstantinos Sagonas , Terrance Swift , David S. Warren, XSB as an efficient deductive database engine, Proceedings of the 1994 ACM SIGMOD international conference on Management of data, p.442-453, May 24-27, 1994, Minneapolis, Minnesota, United States
• 17: Marc Shapiro, II , Susan Horwitz, The Effects of the Precision of Pointer Analysis, Proceedings of the 4th International Symposium on Static Analysis, p.16-34, September 08-10, 1997
• 18: 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]
• 19: R. E. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput., 1(2):146--160, 1972.
• 20: Robert Endre Tarjan, Data structures and network algorithms, Society for Industrial and Applied Mathematics, Philadelphia, PA, 1983
• 21: J. Whaley, D. Avots, M. Carbin, and M. S. Lam. Using datalog with binary decision diagrams for program analysis. In K. Yi, editor, APLAS, volume 3780 of Lecture Notes in Computer Science, pages 97--118. Springer, 2005.
• 22: Y. Zhang and F. Nielson. A scalable inclusion constraint solver using unification. In A. King, editor, LOPSTR, volume 4915 of Lecture Notes in Computer Science, pages 121--136. Springer, 2008.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Constraints

General Terms:
Languages, Performance

Keywords:
constraints, datalog, off-line optimization, program analysis, solver technology, unification