Abstract
Path-sensitive data flow analysis pairs classical data flow analysis with an analysis of feasibility of paths to improve precision. In this paper we propose a framework for path-sensitive backward data flow analysis that is enhanced with an abstraction of the predicate domain. The abstraction is based on a three-valued logic. It follows the strategy that path predicates are simplified if possible (without calling an external predicate solver) and every predicate that could not be reduced to a simple predicate is abstracted to the unknown value, for which the feasibility is undecided. The implementation of the framework scales well and delivers promising results.
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.
Similar content being viewed by others
References
Bodík, R., Gupta, R., Soffa, M.L.: Refining data flow information using infeasible paths. In: Proc. of ESEC/FSE, pp. 361–377. ACM (1997)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL, pp. 238–252. ACM (1977)
Cifuentes, C., Scholz, B.: Parfait – designing a scalable bug checker. In: Proc. of the Static Analysis Workshop, pp. 4–11. ACM (2008)
Dhurjati, D., Das, M., Yang, Y.: Path-sensitive dataflow analysis with iterative refinement. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 425–442. Springer, Heidelberg (2006)
Dijkstra, E.W.: A Discipline of Programming. Prentice Hall (1976)
Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Proc. of PLDI, pp. 57–68. ACM (2002)
Fisher, J., Jhala, R., Majumdar, R.: Joining dataflow with predicates. In: Proc. of ESEC/FSE, pp. 227–236. ACM (2005)
Ginsberg, M.: Multivalued logics: A uniform approach to inference in artificial intelligence. Computational Intelligence 4, 265–316 (1988)
Hayes, I.J., Fidge, C.J., Lermer, K.: Semantic characterisation of dead control-flow paths. IEE Proceedings—Software 148(6), 175–186 (2001)
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. of POPL, pp. 58–70. ACM (2002)
Holley, L.H., Rosen, B.K.: Qualified data flow problems. In: Proc. of POPL, pp. 68–82. ACM (1980)
Hampapuram, H., Yang, Y., Das, M.: Symbolic path simulation in path-sensitive dataflow analysis. In: Proc. of PASTE, pp. 52–58. ACM (2005)
Kildall, G.A.: A unified approach to global program optimization. In: Proc. of POPL, pp. 194–206. ACM (1973)
Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: Proc. of the International Symposium on Code Generation and Optimization (CGO 2004), pp. 75–86 (2004)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis. Springer (1999)
Rival, X., Mauborgne, L.: The trace partitioning abstract domain. In: ACM TOPLAS (August 29, 2007)
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: ACM TOPLAS, vol. 24(3), pp. 217–298 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Winter, K., Zhang, C., Hayes, I.J., Keynes, N., Cifuentes, C., Li, L. (2013). Path-Sensitive Data Flow Analysis Simplified. In: Groves, L., Sun, J. (eds) Formal Methods and Software Engineering. ICFEM 2013. Lecture Notes in Computer Science, vol 8144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41202-8_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-41202-8_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41201-1
Online ISBN: 978-3-642-41202-8
eBook Packages: Computer ScienceComputer Science (R0)