Abstracting abstract machines: a systematic approach to higher-order program analysis

Abstract

Predictive models are fundamental to engineering reliable software systems. However, designing conservative, computable approximations for the behavior of programs (static analyses) remains a difficult and error-prone process for modern high-level programming languages. What analysis designers need is a principled method for navigating the gap between semantics and analytic models: analysis designers need a method that tames the interaction of complex languages features such as higher-order functions, recursion, exceptions, continuations, objects and dynamic allocation.

We contribute a systematic approach to program analysis that yields novel and transparently sound static analyses. Our approach relies on existing derivational techniques to transform high-level language semantics into low-level deterministic state-transition systems (with potentially infinite state spaces). We then perform a series of simple machine refactorings to obtain a sound, computable approximation, which takes the form of a non-deterministic state-transition systems with finite state spaces. The approach scales up uniformly to enable program analysis of realistic language features, including higher-order functions, tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection.

References

1. Ayers, A.E. Abstract analysis and optimization of Scheme. PhD thesis, Massachusetts Institute of Technology (1993).
2. Biernacka, M., Danvy, O. A concrete framework for environment machines. ACM Trans. Comput. Logic 9, 1 (2007) 1--30.
3. Cousot, P. The calculational design of a generic abstract interpreter. In M. Broy and R. Steinbrüggen. eds. Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999).
4. Cousot, P., Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (New York, 1977), ACM, 238--252.
5. Danvy, O. An analytical approach to program as data objects. DSc thesis, Department of Computer Science, Aarhus University (October, 2006).
6. Danvy, O., Nielsen, L.R. Refocusing in reduction semantics. Research Report BRICS RS-04-26, Department of Computer Science, Aarhus University (November 2004).
7. Felleisen, M.R., Findler, B., Flatt, M. Semantics Engineering with PLT Redex. MIT Press (August, 2009).
8. Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M. The essence of compiling with continuations. In PLDI'93: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation (New York, June 1993), ACM, 37--247
9. Jones, N.D. Flow analysis of lambda expressions (preliminary version). In Proceedings of the 8th Colloquium on Automata, Languages and Programming (Springer-Verlag, 1981), 14--128.
10. Jones, N.D., Muchnick, S.S. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '82 (New York, 1982), ACM, 66--74.
11. Landin, P.J. The mechanical evaluation of expressions. Comput. J. 6, 4 (1964), 308--320.
12. Meunier, P.R., Findler, B., Felleisen, M. Modular set-based analysis from contracts. In POPL '06: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, January, 2006), ACM, 218--231.
13. Midtgaard, J. Control-flow analysis of functional programs. ACM Computing Surveys, (2012), Forthcoming.
14. Midtgaard, J., Jensen, T. A calculational approach to control-flow analysis by abstract interpretation. In M. Alpuente and G. Vidal. eds. SAS, volume 5079 of LNCS, Springer (2008), 347--362.
15. Midtgaard, J., Jensen, T.P. Control-flow analysis of function calls and returns by abstract interpretation. In ICFP'09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (New York, 2009), ACM, 287--298.
16. Might, M., Shivers, O. Improving flow analyses via ΓCFA: Abstract garbage collection and counting. In Proceedings of the 11th ACM International Conference on Functional Programming (ICFP 2006), (New York, September, 2006), 13--25.
17. Might, M., Smaragdakis, Y., Van Horn, D. Resolving and exploiting the k-CFA paradox: Illuminating functional vs. object-oriented program analysis. In PLDI'10: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (New York, 2010), ACM, 305--315.
18. Nielson, F., Nielson, H.R., Hankin, C. Principles of Program Analysis. Springer-Verlag, New York (1999).
19. Plotkin, G. Call-by-name, call-by-value and the λ-calculus. Theoret. Comput. Sci. 1, 2 (December 1975), 125--159.
20. Reynolds, J.C. Definitional interpreters for higher-order programming languages. In ACM '72: Proceedings of the ACM Annual Conference (1972), ACM, 717--740.
21. Shivers, O. Control-flow analysis of higher-order languages. PhD thesis, Carnegie Mellon University (1991).
22. Sperber, M. Dybvig, R.K., Flatt, M., van Straaten, A., Findler, R. Matthews, J. Revised {6} Report on the Algorithmic Language Scheme. Cambridge University Press (2010).
23. Tobin-Hochstadt, S., Horn, D.V. Modular analysis via specifications as values. CoRR, abs/1103.1362, (2011).
24. Van Horn, D., Mairson, H.G. Deciding kCFA is complete for EXPTIME. In ICFP '08: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (New York, 2008), ACM, 275--282.
25. Wright, A.K., Jagannathan, S. Polymorphic splitting: An effective polyvariant flow analysis. ACM Trans. Program. Lang. Syst. 20, 1 (1998), 166--207.

Index Terms

• Theory of computation

  • Logic

  • Models of computation

    • Computability

  • Semantics and reasoning

    • Program semantics