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.
- Ayers, A.E. Abstract analysis and optimization of Scheme. PhD thesis, Massachusetts Institute of Technology (1993). Google ScholarDigital Library
- Biernacka, M., Danvy, O. A concrete framework for environment machines. ACM Trans. Comput. Logic 9, 1 (2007) 1--30. Google ScholarDigital Library
- 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).Google Scholar
- 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. Google ScholarDigital Library
- Danvy, O. An analytical approach to program as data objects. DSc thesis, Department of Computer Science, Aarhus University (October, 2006).Google Scholar
- Danvy, O., Nielsen, L.R. Refocusing in reduction semantics. Research Report BRICS RS-04-26, Department of Computer Science, Aarhus University (November 2004).Google Scholar
- Felleisen, M.R., Findler, B., Flatt, M. Semantics Engineering with PLT Redex. MIT Press (August, 2009). Google ScholarDigital Library
- 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 Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Landin, P.J. The mechanical evaluation of expressions. Comput. J. 6, 4 (1964), 308--320.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Midtgaard, J. Control-flow analysis of functional programs. ACM Computing Surveys, (2012), Forthcoming. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Nielson, F., Nielson, H.R., Hankin, C. Principles of Program Analysis. Springer-Verlag, New York (1999). Google ScholarDigital Library
- Plotkin, G. Call-by-name, call-by-value and the λ-calculus. Theoret. Comput. Sci. 1, 2 (December 1975), 125--159.Google ScholarCross Ref
- Reynolds, J.C. Definitional interpreters for higher-order programming languages. In ACM '72: Proceedings of the ACM Annual Conference (1972), ACM, 717--740. Google ScholarDigital Library
- Shivers, O. Control-flow analysis of higher-order languages. PhD thesis, Carnegie Mellon University (1991). Google ScholarDigital Library
- 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). Google ScholarDigital Library
- Tobin-Hochstadt, S., Horn, D.V. Modular analysis via specifications as values. CoRR, abs/1103.1362, (2011).Google Scholar
- 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. Google ScholarDigital Library
- Wright, A.K., Jagannathan, S. Polymorphic splitting: An effective polyvariant flow analysis. ACM Trans. Program. Lang. Syst. 20, 1 (1998), 166--207. Google ScholarDigital Library
Index Terms
- Abstracting abstract machines: a systematic approach to higher-order program analysis
Recommendations
Abstracting definitional interpreters (functional pearl)
In this functional pearl, we examine the use of definitional interpreters as a basis for abstract interpretation of higher-order programming languages. As it turns out, definitional interpreters, especially those written in monadic style, can provide a ...
Abstracting abstract control
DLS '14The strength of a dynamic language is also its weakness: run-time flexibility comes at the cost of compile-time predictability. Many of the hallmarks of dynamic languages such as closures, continuations, various forms of reflection, and a lack of static ...
Abstracting abstract control
DLS '14: Proceedings of the 10th ACM Symposium on Dynamic languagesThe strength of a dynamic language is also its weakness: run-time flexibility comes at the cost of compile-time predictability. Many of the hallmarks of dynamic languages such as closures, continuations, various forms of reflection, and a lack of static ...
Comments