Bebop: a path-sensitive interprocedural dataflow engine

ABSTRACT

Flow-sensitive data analyses can lose precision because they assume that all paths in a control-flow graph are executable (feasible). Path-sensitive dataflow analyses can rule out infeasible paths by tracking correlations between dataflow facts. To track such correlations, in general, requires recording a set of sets of facts per statement in a program. Naive representation of such sets can lead to a very high memory consumption and running time.We reformulate an interprocedural dataflow algorithm by Reps, Horwitz and Sagiv (based on context-free graph reachability) into a traditional interprocedural flow-sensitive dataflow algorithm. We then show how to use Binary Decision Diagrams (BDDs), a data structure from the model checking community, to turn this reformulated algorithm into an interprocedural path-sensitive dataflow analysis algorithm that tracks a set of set of facts per program statement. We have implemented this algorithm in a tool called \bebop.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: Glenn Ammons , James R. Larus, Improving data-flow analysis with path profiles, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.72-84, June 17-19, 1998, Montreal, Quebec, Canada
• 3: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 4: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 5: Rastisalv Bodík , Sadun Anik, Path-sensitive value-flow analysis, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.237-251, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268966]
• 6: Rastislav Bodík , Rajiv Gupta , Mary Lou Soffa, Refining data flow information using infeasible paths, Proceedings of the 6th European conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, p.361-377, September 22-25, 1997, Zurich, Switzerland
• 7: 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]
• 8: 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
• 9: S. G. Govindaraju and D. L. Dill. Approximate symbolic model checking using overlapping projections. In Electronic Notes in Theoretical Computer Science, July 1999.
• 10: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 11: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 12: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 13: M. Sharir and A. Pnueli. Two approaches to interprocedural data ow analysis. In Program Flow Analysis: Theory and Applications, pages 189-233. Prentice-Hall, 1981.
• 14: M. Siff. personal communication. July 12 2000.
• 15: Steven W. K. Tjiang , John L. Hennessy, Sharlit—a tool for building optimizers, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.82-93, June 15-19, 1992, San Francisco, California, United States
• 16: G. A. Venkatesh, A framework for construction and evaluation of high-level specifications for program analysis techniques, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.1-12, June 19-23, 1989, Portland, Oregon, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs

General Terms:
Algorithms