Abstract
Abstracting abstract machines is a systematic methodology for constructing sound static analyses for higher-order languages, by deriving small-step abstract abstract machines (AAMs) that perform abstract interpretation from abstract machines that perform concrete evaluation. Darais et al. apply the same underlying idea to monadic definitional interpreters, and obtain monadic abstract definitional interpreters (ADIs) that perform abstract interpretation in big-step style using monads. Yet, the relation between small-step abstract abstract machines and big-step abstract definitional interpreters is not well studied.
In this paper, we explain their functional correspondence and demonstrate how to systematically transform small-step abstract abstract machines into big-step abstract definitional interpreters. Building on known semantic interderivation techniques from the concrete evaluation setting, the transformations include linearization, lightweight fusion, disentanglement, refunctionalization, and the left inverse of the CPS transform. Linearization expresses nondeterministic choice through first-order data types, after which refunctionalization transforms the first-order data types that represent continuations into higher-order functions. The refunctionalized AAM is an abstract interpreter written in continuation-passing style (CPS) with two layers of continuations, which can be converted back to direct style with delimited control operators. Based on the known correspondence between delimited control and monads, we demonstrate that the explicit use of monads in abstract definitional interpreters is optional.
All transformations properly handle the collecting semantics and nondeterminism of abstract interpretation. Remarkably, we reveal how precise call/return matching in control-flow analysis can be obtained by refunctionalizing a small-step abstract abstract machine with proper caching.
Supplemental Material
- Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. 2003. A Functional Correspondence Between Evaluators and Abstract Machines. In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming (PPDP ’03). ACM, New York, NY, USA, 8–19. Google ScholarDigital Library
- Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. 2004. A functional correspondence between call-by-need evaluators and lazy abstract machines. Inform. Process. Lett. 90, 5 (2004), 223 – 232. Google ScholarDigital Library
- Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. 2005. A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theoretical Computer Science 342, 1 (2005), 149–172. Google ScholarDigital Library
- Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. 2005. An Operational Foundation for Delimited Continuations in the CPS Hierarchy. Logical Methods in Computer Science Volume 1, Issue 2 (Nov. 2005).Google Scholar
- Malgorzata Biernacka and Olivier Danvy. 2009. Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part II: Reduction Semantics and Abstract Machines. In Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Jens Palsberg (Ed.), Vol. 5700. Springer, 186–206. Google ScholarDigital Library
- Henry Cejtin, Suresh Jagannathan, and Stephen Weeks. 2000. Flow-Directed Closure Conversion for Typed Languages. In Programming Languages and Systems, 9th European Symposium on Programming, ESOP 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings (Lecture Notes in Computer Science), Gert Smolka (Ed.), Vol. 1782. Springer, 56–71. Google ScholarDigital Library
- Charles Consel. 1993. A Tour of Schism: A Partial Evaluation System for Higher-order Applicative Languages. In Proceedings of the 1993 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM ’93). ACM, New York, NY, USA, 145–154. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. ACM, 238–252. Google ScholarDigital Library
- Olivier Danvy. 1994. Back to Direct Style. Sci. Comput. Program. 22, 3 (1994), 183–195. Google ScholarDigital Library
- Olivier Danvy. 2003. A New One-Pass Transformation into Monadic Normal Form. In CC (Lecture Notes in Computer Science), Vol. 2622. Springer, 77–89. Google ScholarDigital Library
- Olivier Danvy. 2004. A Rational Deconstruction of Landin’s SECD Machine. In Implementation and Application of Functional Languages, 16th International Workshop, IFL 2004, Lübeck, Germany, September 8-10, 2004, Revised Selected Papers (Lecture Notes in Computer Science), Clemens Grelck, Frank Huch, Greg Michaelson, and Philip W. Trinder (Eds.), Vol. 3474. Springer, 52–71. Google ScholarDigital Library
- Olivier Danvy. 2006a. An Analytical Approach to Programs as Data Objects. DSc thesis. Department of Computer Science, Aarhus University, Aarhus, Denmark.Google Scholar
- Olivier Danvy. 2006b. Refunctionalization at Work. In Mathematics of Program Construction, 8th International Conference, MPC 2006, Kuressaare, Estonia, July 3-5, 2006, Proceedings (Lecture Notes in Computer Science), Tarmo Uustalu (Ed.), Vol. 4014. Springer, 4. Google ScholarDigital Library
- Olivier Danvy. 2008. Defunctionalized Interpreters for Programming Languages. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08). ACM, New York, NY, USA, 131–142. Google ScholarDigital Library
- Olivier Danvy. 2009. Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part I: Denotational Semantics, Natural Semantics, and Abstract Machines. In Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Jens Palsberg (Ed.), Vol. 5700. Springer, 162–185. Google ScholarDigital Library
- Olivier Danvy and Andrzej Filinski. 1990. Abstracting Control. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming (LFP ’90). ACM, New York, NY, USA, 151–160. Google ScholarDigital Library
- Olivier Danvy and Andrzej Filinski. 1992. Representing control: A study of the CPS transformation. Mathematical structures in computer science 2, 4 (1992), 361–391.Google Scholar
- Olivier Danvy and Julia L. Lawall. 1992. Back to Direct Style II: First-Class Continuations. In LISP and Functional Programming. 299–310. Google ScholarDigital Library
- Olivier Danvy and Kevin Millikin. 2008a. On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion. Inform. Process. Lett. 106, 3 (2008), 100 – 109. Google ScholarDigital Library
- Olivier Danvy and Kevin Millikin. 2008b. A Rational Deconstruction of Landin’s SECD Machine with the J Operator. Logical Methods in Computer Science 4, 4 (2008).Google Scholar
- Olivier Danvy and Kevin Millikin. 2009. Refunctionalization at work. Science of Computer Programming 74, 8 (2009), 534 – 549. Google ScholarDigital Library
- Olivier Danvy and Lasse R. Nielsen. 2001. Defunctionalization at Work. In Proceedings of the 3rd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP ’01). ACM, New York, NY, USA, 162–174. Google ScholarDigital Library
- Olivier Danvy and Lasse R. Nielsen. 2004. Refocusing in reduction semantics. BRICS Report Series 11, 26 (2004).Google Scholar
- David Darais. 2017. Mechanizing Abstract Interpretation. PhD Dissertation. Department of Computer Science, University of Maryland.Google Scholar
- David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn. 2017. Abstracting Definitional Interpreters (Functional Pearl). Proc. ACM Program. Lang. 1, ICFP, Article 12 (Aug. 2017), 25 pages. Google ScholarDigital Library
- Christopher Earl, Matthew Might, and David Van Horn. 2010. Pushdown Control-Flow Analysis of Higher-Order Programs. CoRR abs/1007.4268 (2010). arXiv: 1007.4268 http://arxiv.org/abs/1007.4268Google Scholar
- Christopher Earl, Ilya Sergey, Matthew Might, and David Van Horn. 2012. Introspective Pushdown Analysis of Higher-order Programs. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP ’12). ACM, New York, NY, USA, 177–188. Google ScholarDigital Library
- Richard A. Eisenberg and Jan Stolarek. 2014. Promoting Functions to Type Families in Haskell. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell (Haskell ’14). ACM, New York, NY, USA, 95–106. Google ScholarDigital Library
- Matthias Felleisen and Daniel P. Friedman. 1987. A calculus for assignments in higher-order languages. In Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. ACM, 314. Google ScholarDigital Library
- Andrzej Filinski. 1994. Representing Monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’94). ACM, New York, NY, USA, 446–457. Google ScholarDigital Library
- Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The Essence of Compiling with Continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation (PLDI ’93). ACM, New York, NY, USA, 237–247. Google ScholarDigital Library
- Georgios Fourtounis, Nikolaos S Papaspyrou, and Panagiotis Theofilopoulos. 2014. Modular polymorphic defunctionalization. Computer Science and Information Systems 11, 4 (2014), 1417–1434.Google ScholarCross Ref
- Daniel P. Friedman and Anurag Medhekar. 2003. Tutorial: Using an Abstracted Interpreter to Understand Abstract Interpretation, Course notes for CSCI B621, Indiana University.Google Scholar
- Thomas Gilray, Michael D. Adams, and Matthew Might. 2016a. Allocation Characterizes Polyvariance: A Unified Methodology for Polyvariant Control-flow Analysis. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016). ACM, New York, NY, USA, 407–420. Google ScholarDigital Library
- Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, and David Van Horn. 2016b. Pushdown Control-flow Analysis for Free. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). ACM, New York, NY, USA, 691–704. Google ScholarDigital Library
- James Ian Johnson and David Van Horn. 2014. Abstracting Abstract Control. In Proceedings of the 10th ACM Symposium on Dynamic Languages (DLS ’14). ACM, New York, NY, USA, 11–22. Google ScholarDigital Library
- Neil D. Jones. 1981. Flow Analysis of Lambda Expressions (Preliminary Version). In Automata, Languages and Programming, 8th Colloquium, Acre (Akko), Israel, July 13-17, 1981, Proceedings (Lecture Notes in Computer Science), Shimon Even and Oded Kariv (Eds.), Vol. 115. Springer, 114–128. Google ScholarDigital Library
- Peter J. Landin. 1966. The next 700 programming languages. Commun. ACM 9, 3 (1966), 157–166. Google ScholarDigital Library
- John McCarthy. 1960. Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I. Commun. ACM 3, 4 (April 1960), 184–195. Google ScholarDigital Library
- Matthew Might, Yannis Smaragdakis, and David Van Horn. 2010. Resolving and Exploiting the k-CFA Paradox: Illuminating Functional vs. Object-oriented Program Analysis. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’10). ACM, New York, NY, USA, 305–315. Google ScholarDigital Library
- Eugenio Moggi. 1991. Notions of computation and monads. Information and Computation 93, 1 (1991), 55 – 92. Google ScholarDigital Library
- Atsushi Ohori and Isao Sasano. 2007. Lightweight Fusion by Fixed Point Promotion. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’07). ACM, New York, NY, USA, 143–154. Google ScholarDigital Library
- François Pottier and Nadji Gauthier. 2006. Polymorphic typed defunctionalization and concretization. Higher-Order and Symbolic Computation 19, 1 (01 Mar 2006), 125–162. Google ScholarDigital Library
- John C. Reynolds. 1972. Definitional Interpreters for Higher-Order Programming Languages. In Proceedings of 25th ACM National Conference. ACM, Boston, Massachusetts, 717–740. Reprinted in Higher-Order and Symbolic Computation 11(4):363-397, 1998, with a foreword { Reynolds 1998 }. Google ScholarDigital Library
- John C. Reynolds. 1998. Definitional Interpreters Revisited. Higher-Order and Symbolic Computation 11, 4 (1998), 355–361. Google ScholarDigital Library
- Tiark Rompf, Ingo Maier, and Martin Odersky. 2009. Implementing First-class Polymorphic Delimited Continuations by a Type-directed Selective CPS-transform. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP ’09). ACM, New York, NY, USA, 317–328. Google ScholarDigital Library
- Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, and Frank Piessens. 2013. Monadic Abstract Interpreters. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’13). ACM, New York, NY, USA, 399–410. Google ScholarDigital Library
- Olin Shivers. 1988. Control Flow Analysis in Scheme. In Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation (PLDI ’88). ACM, New York, NY, USA, 164–174. Google ScholarDigital Library
- Olin Shivers. 1991. The Semantics of Scheme Control-flow Analysis. In Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM ’91). ACM, New York, NY, USA, 190–198. Google ScholarDigital Library
- Sam Tobin-Hochstadt and David Van Horn. 2012. Higher-order Symbolic Execution via Contracts. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA ’12). ACM, New York, NY, USA, 537–554. Google ScholarDigital Library
- David Van Horn and Matthew Might. 2010. Abstracting Abstract Machines. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP ’10). ACM, New York, NY, USA, 51–62. Google ScholarDigital Library
- David Van Horn and Matthew Might. 2012. Systematic abstraction of abstract machines. Journal of Functional Programming 22, 4-5 (2012), 705–746. Google ScholarDigital Library
- Dimitrios Vardoulakis and Olin Shivers. 2010. CFA2: A Context-free Approach to Control-flow Analysis. In Proceedings of the 19th European Conference on Programming Languages and Systems (ESOP’10). Springer-Verlag, Berlin, Heidelberg, 570–589. Google ScholarDigital Library
- Philip Wadler. 1985. How to replace failure by a list of successes a method for exception handling, backtracking, and pattern matching in lazy functional languages. In Functional Programming Languages and Computer Architecture, Jean-Pierre Jouannaud (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 113–128. Google ScholarDigital Library
- Philip Wadler. 1992. The Essence of Functional Programming. In Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’92). ACM, New York, NY, USA, 1–14. Google ScholarDigital Library
Index Terms
- Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl)
Recommendations
Staged abstract interpreters: fast and modular whole-program analysis via meta-programming
It is well known that a staged interpreter is a compiler: specializing an interpreter to a given program produces an equivalent executable that runs faster. This connection is known as the first Futamura projection. It is even more widely known that an ...
Monadic abstract interpreters
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and ImplementationRecent 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, ...
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, ...
Comments