Abstract
In this paper, we present a new method for supporting abstraction refinement in path-sensitive dataflow analysis. We show how an adjustable merge criterion can be used as an interface to control the degree of abstraction. In particular, we partition the merge criterion with two sets of predicates — one related to the dataflow facts being propagated and the other related to path feasibility. These tracked predicates are then used to guide merge operations and path feasibility analysis, so that expensive computations are performed only at the right places. Refinement amounts to lazily growing the path predicate set to recover lost precision. We have implemented our refinement technique in ESP, a software validation tool for C/C++ programs. We apply ESP to validate a future version of Windows against critical security properties. Our experience suggests that applying iterative refinement to path-sensitive dataflow analysis is both effective in cutting down spurious errors and scalable enough for solving real world problems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ball, T., Rajamani, S.: The SLAM project: Debugging system software via static analysis. In: Proceedings of the ACM Symposium on Principles of Programming Languages (POPL) (2002)
Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Proceedings of the 8th International SPIN Workshop on Model Checking of Software, pp. 103–122. Springer, New York (2001)
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (2002)
Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: Proceedings of the ACM Symposium on Principles of Programming Languages (POPL) (2004)
Flanagan, C.: Automatic Software Model Checking Using CLP. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 189–203. Springer, Heidelberg (2003)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the ACM Symposium on Principles of Programming Languages (POPL) (1977)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural data flow analysis via graph reachability. In: Proceedings of the ACM Symposium on Principles of Programming Languages (POPL) (1995)
Bodik, R., Gupta, R., Soffa, M.L.: Refining data flow information using infeasible paths. In: Jazayeri, M. (ed.) ESEC 1997. LNCS, vol. 1301. Springer, Heidelberg (1997)
Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI) (2002)
Dor, N., Adams, S., Das, M., Yang, Z.: Software validation via scalable path-sensitive value flow analysis. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA) (2004)
Hampapuram, H., Yang, Y., Das, M.: Symbolic path simulatin in path-sensitive datflow analysis. In: Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE) (2005)
Strom, R., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering 12(1), 157–171 (1986)
Das, M.: Unification-based pointer analysis with directional assignments. In: ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI) (2000)
Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 268. Springer, Heidelberg (2001)
Holley, L.H., Rosen, B.K.: Qualified data flow problems. In: Proceedings of the ACM Symposium on Principles of Programming Languages (POPL) (1980)
Heintze, N., Tardieu, O.: Demand-driven pointer analysis. In: ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation (PLDI) (2001)
Guyer, S.Z., Lin, C.: Client-driven pointer analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694. Springer, Heidelberg (2003)
Plevyak, J., Chien, A.A.: Precise concrete type inference for object-oriented languages. In: Proceedings of the Ninth Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) (1994)
Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)
Handjieva, M., Tzolovski, S.: Refining static analyses by trace-based partitioning using control flow. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 200–214. Springer, Heidelberg (1998)
Fischer, J., Jhala, R., Majumdar, R.: Joining dataflow with predicates. In: Gilbert, H., Handschuh, H. (eds.) FSE 2005. LNCS, vol. 3557. Springer, Heidelberg (2005)
M. Leino, K.R., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 119–134. Springer, Heidelberg (2005)
Adams, S., Ball, T., Das, M., Lerner, S., Rajamani, S.K., Seigle, M., Weimer, W.: Speeding up dataflow analysis using flow-insensitive pointer analysis. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, p. 230. Springer, Heidelberg (2002)
Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: Localizing errors in counterexample traces. SIGPLAN Not. 38(1), 97–105 (2003)
Groce, A., Visser, W.: What went wrong: Explaining counterexamples. In: SPIN Workshop on Model Checking of Software, pp. 121–135 (May 2003)
Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Software - Practice and Experience 30(7), 775–802 (2000)
Musuvathi, M.S., Park, D., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: Proceedings of the Fifth Symposium on Operating Systems Design and Implementation (OSDI) (2002)
Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Proceedings of the ACM Symposium on Principles of programming Languages (POPL) (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dhurjati, D., Das, M., Yang, Y. (2006). Path-Sensitive Dataflow Analysis with Iterative Refinement. In: Yi, K. (eds) Static Analysis. SAS 2006. Lecture Notes in Computer Science, vol 4134. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11823230_27
Download citation
DOI: https://doi.org/10.1007/11823230_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37756-6
Online ISBN: 978-3-540-37758-0
eBook Packages: Computer ScienceComputer Science (R0)