Ilya Sergey
Dominique Devriese
Matthew Might
Jan Midtgaard
David Darais
ABSTRACT
Recent developments in the systematic construction of abstract interpreters hinted at the possibility of a broad unification of concepts in static analysis. We deliver that unification by showing context-sensitivity, polyvariance, flow-sensitivity, reachability-pruning, heap-cloning and cardinality-bounding to be independent of any particular semantics. Monads become the unifying agent between these concepts and between semantics. For instance, by plugging the same "context-insensitivity monad" into a monadically-parameterized semantics for Java or for the lambda calculus, it yields the expected context-insensitive analysis.
To achieve this unification, we develop a systematic method for transforming a concrete semantics into a monadically-parameterized abstract machine. Changing the monad changes the behavior of the machine. By changing the monad, we recover a spectrum of machines---from the original concrete semantics to a monovariant, flow- and context-insensitive static analysis with a singly-threaded heap and weak updates.
The monadic parameterization also suggests an abstraction over the ubiquitous monotone fixed-point computation found in static analysis. This abstraction makes it straightforward to instrument an analysis with high-level strategies for improving precision and performance, such as abstract garbage collection and widening.
While the paper itself runs the development for continuation-passing style, our generic implementation replays it for direct-style lambda-calculus and Featherweight Java to support generality.
- M. S. Ager, O. Danvy, and J.Midtgaard. A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theor. Comput. Sci., 342(1):149--172, 2005. Google Scholar
Digital Library
- M. Biernacka and O. Danvy. A syntactic correspondence between context-sensitive calculi and abstract machines. Theor. Comput. Sci., 375(1--3):76--108, 2007. Google ScholarDigital Library
- M. M. T. Chakravarty, G. Keller, S. L. P. Jones, and S. Marlow. Associated types with class. In POPL, 2005. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977. Google ScholarDigital Library
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In POPL, 1979. Google ScholarDigital Library
- O. Danvy. A new one-pass transformation into monadic normal form. In CC, volume 2622 of LNCS, 2003. Google ScholarDigital Library
- O. Danvy. Defunctionalized interpreters for programming languages. In ICFP, 2008. Google ScholarDigital Library
- A. Filinski. Monads in action. In POPL, 2010. Google ScholarDigital Library
- C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In PLDI, 1993. Google ScholarDigital Library
- P. Hudak and J. Young. Collecting interpretations of expressions. ACM Trans. Prog. Lang. Syst., 13(2):269--290, 1991. Google ScholarDigital Library
- M. P. Jones. Type Classes with Functional Dependencies. In ESOP, volume 1782 of LNCS, 2000. Google ScholarDigital Library
- A. Lakhotia, D. R. Boccardo, A. Singh, and A.Manacero, Jr. Contextsensitive analysis of obfuscated x86 executables. In PEPM, 2010. Google ScholarDigital Library
- S. Liang, P. Hudak, and M. Jones. Monad transformers and modular interpreters. In POPL, 1995. Google ScholarDigital Library
- M. Might. Environment analysis of higher-order languages. PhD thesis, Georgia Institute of Technology, 2007. Google ScholarDigital Library
- M. Might. Abstract interpreters for free. In SAS, volume 6337 of LNCS, 2010. Google ScholarDigital Library
- M. Might. Shape analysis in the absence of pointers and structure. In VMCAI, volume 5944 of LNCS, 2010. Google ScholarDigital Library
- M. Might and P. Manolios. A posteriori soundness for nondeterministic abstract interpretations. In VMCAI, volume 5944 of LNCS, 2009. Google ScholarDigital Library
- M.Might and O. Shivers. Improving flow analyses via CFA: abstract garbage collection and counting. In ICFP, 2006. Google ScholarDigital Library
- M. Might, Y. Smaragdakis, and D. Van Horn. Resolving and exploiting the k-CFA paradox: illuminating functional vs. objectoriented program analysis. In PLDI, 2010. Google ScholarDigital Library
- F. Nielson. Two-level semantics and abstract interpretation. Theor. Comput. Sci., 69(2):117--242, 1989. Google ScholarDigital Library
- T. Schrijvers and B. C. Oliveira. Monads, zippers and views: virtualizing the monad stack. In ICFP, 2011. Google ScholarDigital Library
- O. G. Shivers. Control-flow analysis of higher-order languages or taming lambda. PhD thesis, Carnegie Mellon University, 1991. Google ScholarDigital Library
- D. Van Horn and M. Might. Abstracting abstract machines. In ICFP, 2010. Google ScholarDigital Library
- D. Van Horn and M. Might. Abstracting abstract machines: a systematic approach to higher-order program analysis. Commun. ACM, 54(9):101--109, 2011. Google ScholarDigital Library
- P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad-hoc. In POPL, 1989. Google ScholarDigital Library
Index Terms
- Monadic abstract interpreters
Recommendations
Monadic abstract interpreters
PLDI '13Recent developments in the systematic construction of abstract interpreters hinted at the possibility of a broad unification of concepts in static analysis. We deliver that unification by showing context-sensitivity, polyvariance, flow-sensitivity, ...
Introspective pushdown analysis of higher-order programs
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programmingIn the static analysis of functional programs, pushdown flow analysis and abstract garbage collection skirt just inside the boundaries of soundness and decidability. Alone, each method reduces analysis times and boosts precision by orders of magnitude. ...
Introspective pushdown analysis of higher-order programs
ICFP '12In the static analysis of functional programs, pushdown flow analysis and abstract garbage collection skirt just inside the boundaries of soundness and decidability. Alone, each method reduces analysis times and boosts precision by orders of magnitude. ...
Reviews
Jacques Carette
Abstract interpretation is an important conceptual framework that unifies many different concepts in static analysis. However, writing a general, modular, abstract interpreter has not been as straightforward. There are two difficulties: a software engineering challenge, and an encoding issue. The software engineering challenge is to find the right abstractions that capture the kind of polymorphism inherent in abstract interpretation. The encoding issue involves finding a way to phrase the operational semantics of languages using a suitable abstract machine that lends itself well to abstract interpretation. This is exactly what the authors solve in this gem of a paper. Aimed directly at experts, the paper walks readers through the process of taking a lambda calculus and rewriting it (using continuation passing style, an explicit store, and explicit contexts) so that it is better suited for abstract interpretation. Next, using an explicit implementation in Haskell, various aspects (nondeterminism, store, time, and addresses) are systematically abstracted away from the interpreter into a monad. Then, to prove that this beautiful series of abstractions is more than mere theory, the authors show how to concretely implement a variety of analyses using this framework. While this section might seem a little ad hoc, they then show how it all fits together in an elegant conceptual framework. This paper is a real tour de force. Not only is it very well written, it presents an extremely elegant solution to an important, thorny problem. The only unfortunate aspect is that the authors chose an initial algebra encoding of their base language, rather than the much more flexible "finally tagless" encoding. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments