Document Open Access Logo

Higher-Order Demand-Driven Program Analysis

Authors Zachary Palmer, Scott F. Smith

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2016.19.pdf
  • Filesize: 0.63 MB
  • 25 pages

Document Identifiers

Author Details

Zachary Palmer
Scott F. Smith

Cite AsGet BibTex

Zachary Palmer and Scott F. Smith. Higher-Order Demand-Driven Program Analysis. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 19:1-19:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.ECOOP.2016.19

Abstract

We explore a novel approach to higher-order program analysis that brings ideas of on-demand lookup from first-order CFL-reachability program analyses to higher-order programs. The analysis needs to produce only a control-flow graph; it can derive all other information including values of variables directly from the graph. Several challenges had to be overcome, including how to build the control-flow graph on-the-fly and how to deal with non-local variables in functions. The resulting analysis is flow- and context-sensitive with a provable polynomial-time bound. The analysis is formalized and proved correct and terminating, and an initial implementation is described.
Keywords
  • functional programming
  • program analysis
  • polynomial-time
  • demand-driven
  • flow-sensitive
  • context-sensitive

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR'97, 1997. Google Scholar
  2. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977. Google Scholar
  3. Christopher Earl, Matthew Might, and David Van Horn. Pushdown control-flow analysis of higher-order programs. In Workshop on Scheme and Functional Programming, 2010. Google Scholar
  4. M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 1992. Google Scholar
  5. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In PLDI, 1993. Google Scholar
  6. Susan Horwitz, Thomas Reps, and Mooly Sagiv. Demand interprocedural dataflow analysis. In Foundations of Software Engineering, 1995. Google Scholar
  7. Suresh Jagannathan and Stephen Weeks. A unified treatment of flow analysis in higher-order languages. In POPL '95, 1995. Google Scholar
  8. J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, and David Van Horn. Pushdown flow analysis with abstract garbage collection. JFP, 2014. Google Scholar
  9. John Kodumal and Alex Aiken. The set constraint/CFL reachability connection in practice. In PLDI, 2004. Google Scholar
  10. John Lamping. An algorithm for optimal lambda calculus reduction. In POPL, 1990. Google Scholar
  11. Yi Lu, Lei Shang, Xinwei Xie, and Jingling Xue. An incremental points-to analysis with CFL-reachability. In Compiler Construction, 2013. Google Scholar
  12. Jan Midtgaard. Control-flow analysis of functional programs. ACM Comput. Surv., 2012. Google Scholar
  13. Matthew Might. Abstract interpreters for free. In Proceedings of the 17th International Conference on Static Analysis, 2010. Google Scholar
  14. Matthew Might and Olin Shivers. Improving flow analyses via ΓCFA: Abstract garbage collection and counting. In ICFP, Portland, Oregon, 2006. Google Scholar
  15. Matthew Might, Yannis Smaragdakis, and David Van Horn. Resolving and exploiting the k-CFA paradox: Illuminating functional vs. object-oriented program analysis. In PLDI, 2010. Google Scholar
  16. Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1999. Google Scholar
  17. Zachary Palmer and Leandro Facchinetti. Odefa proof-of-concept implementation. https://github.com/JHU-PL-Lab/odefa-proof-of-concept, 2015. Accessed: 2015-10-11.
  18. Jakob Rehof and Manuel Fähndrich. Type-base flow analysis: from polymorphic subtyping to CFL-reachability. In POPL, New York, NY, USA, 2001. Google Scholar
  19. Thomas Reps. Demand interprocedural program analysis using logic databases. In Application of Logic Databases, 1994. Google Scholar
  20. Thomas Reps. Shape analysis as a generalized path problem. In PEPM, 1995. Google Scholar
  21. Thomas Reps, Susan Horwitz, and Mooly Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, 1995. Google Scholar
  22. Olin Shivers. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie-Mellon University, 1991. TR CMU-CS-91-145. Google Scholar
  23. Yannis Smaragdakis and Martin Bravenboer. Using Datalog for fast and easy program analysis. In Datalog Reloaded: First International Workshop, 2011. Google Scholar
  24. David Van Horn and Harry G. Mairson. Deciding kCFA is complete for EXPTIME. In ICFP, 2008. Google Scholar
  25. David Van Horn and Matthew Might. Abstracting abstract machines. In ICFP, 2010. Google Scholar
  26. Dimitrios Vardoulakis and Olin Shivers. CFA2: A context-free approach to control-flow analysis. In European Symposium on Programming, 2010. Google Scholar
  27. Dimitrios Vardoulakis and Olin Shivers. Pushdown flow analysis of first-class control. In ICFP, 2011. Google Scholar
  28. Christopher P. Wadsworth. Semantics and Pragmatics of the Lambda-calculus. PhD thesis, University of Oxford, 1971. Google Scholar
  29. Xin Zhang, Mayur Naik, and Hongseok Yang. Finding optimum abstractions in parametric dataflow analysis. In PLDI, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact