Thomas Ball
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.
- 1.A. Aho, R. Sethi, and J. Ullman. Compilers: Principles, Techniques and Tools. Addison-Wesley, 1986. Google Scholar
Digital Library
- 2.G. Ammons and J. R. Larus. Improving data-flow analysis with path profiles. In PLDI 98: Programming Language Design and Implementation, pages 72-84. ACM, 1998. Google ScholarDigital Library
- 3.T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 01: Programming Language Design and Implementation. ACM, 2001. Google ScholarDigital Library
- 4.T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for Boolean programs. In SPIN 00: SPIN Workshop, LNCS 1885, pages 113-130. Springer-Verlag, 2000. Google ScholarDigital Library
- 5.R. Bodik and S. Anik. Path-sensitive value-flow analysis. In POPL 98: Principles of Programming Languages, pages 237-251. ACM, 1998. Google ScholarDigital Library
- 6.R. Bodik, R. Gupta, and M. L. Soffa. Refining data ow information using infeasible paths. In ESEC/FSE 97: European Software Engineering/Foundations of Software Engineering, LNCS 1301, pages 361-377. Springer-Verlag, 1997. Google ScholarDigital Library
- 7.R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, 1986. Google ScholarDigital Library
- 8.M. Das. Unification-based pointer analysis with directional assignments. In PLDI 00: Programming Language Design and Implementation, pages 35-46. ACM, 2000. Google ScholarDigital Library
- 9.S. G. Govindaraju and D. L. Dill. Approximate symbolic model checking using overlapping projections. In Electronic Notes in Theoretical Computer Science, July 1999.Google ScholarCross Ref
- 10.K. McMillan. Symbolic Model Checking: An Approach to the State-Explosion Problem. Kluwer Academic Publishers, 1993. Google ScholarDigital Library
- 11.T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural data ow analysis via graph reachability. InPOPL 95: Principles of Programming Languages, pages 49-61. ACM, 1995. Google ScholarDigital Library
- 12.M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In POPL 99: Principles of Programming Languages, pages 105-118. ACM, 1999. Google ScholarDigital Library
- 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.Google Scholar
- 14.M. Siff. personal communication. July 12 2000.Google Scholar
- 15.S. W. K. Tjiang and J. L. Hennessy. Sharlit - a tool for building optimizers. In PLDI 92: Programming Language Design and Implementation, pages 82-93. ACM, 1992. Google ScholarDigital Library
- 16.G. A. Venkatesh. A framework for construction and evaluation of high-level specifications for program analysis techniques. In PLDI 89: Programming Language Design and Implementation, pages 1-12. ACM, 1989. Google ScholarDigital Library
Index Terms
- Bebop: a path-sensitive interprocedural dataflow engine
Recommendations
Interprocedural pointer alias analysis
We present practical approximation methods for computing and representing interprocedural aliases for a program written in a language that includes pointers, reference parameters, and recursion. We present the following contributions: (1) a framework ...
Side-effect analysis with fast escape filter
SOAP '12: Proceedings of the ACM SIGPLAN International Workshop on State of the Art in Java Program analysisSide-effect analysis is a fundamental static analysis used to determine the memory locations modified or used by each program entity. For the programs with pointers, the analysis can be very imprecise. To improve the precision of side-effect analysis, ...
Comments