Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl)

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.

References

1. 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.
2. 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.
3. 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.
4. 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).
5. 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.
6. 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.
7. 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.
8. 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.
9. Olivier Danvy. 1994. Back to Direct Style. Sci. Comput. Program. 22, 3 (1994), 183–195.
10. Olivier Danvy. 2003. A New One-Pass Transformation into Monadic Normal Form. In CC (Lecture Notes in Computer Science), Vol. 2622. Springer, 77–89.
11. 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.
12. Olivier Danvy. 2006a. An Analytical Approach to Programs as Data Objects. DSc thesis. Department of Computer Science, Aarhus University, Aarhus, Denmark.
13. 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.
14. 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.
15. 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.
16. 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.
17. Olivier Danvy and Andrzej Filinski. 1992. Representing control: A study of the CPS transformation. Mathematical structures in computer science 2, 4 (1992), 361–391.
18. Olivier Danvy and Julia L. Lawall. 1992. Back to Direct Style II: First-Class Continuations. In LISP and Functional Programming. 299–310.
19. 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.
20. 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).
21. Olivier Danvy and Kevin Millikin. 2009. Refunctionalization at work. Science of Computer Programming 74, 8 (2009), 534 – 549.
22. 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.
23. Olivier Danvy and Lasse R. Nielsen. 2004. Refocusing in reduction semantics. BRICS Report Series 11, 26 (2004).
24. David Darais. 2017. Mechanizing Abstract Interpretation. PhD Dissertation. Department of Computer Science, University of Maryland.
25. 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.
26. 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.4268
27. 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.
28. 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.
29. 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.
30. 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.
31. 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.
32. Georgios Fourtounis, Nikolaos S Papaspyrou, and Panagiotis Theofilopoulos. 2014. Modular polymorphic defunctionalization. Computer Science and Information Systems 11, 4 (2014), 1417–1434.
33. Daniel P. Friedman and Anurag Medhekar. 2003. Tutorial: Using an Abstracted Interpreter to Understand Abstract Interpretation, Course notes for CSCI B621, Indiana University.
34. 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.
35. 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.
36. 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.
37. 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.
38. Peter J. Landin. 1966. The next 700 programming languages. Commun. ACM 9, 3 (1966), 157–166.
39. John McCarthy. 1960. Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I. Commun. ACM 3, 4 (April 1960), 184–195.
40. 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.
41. Eugenio Moggi. 1991. Notions of computation and monads. Information and Computation 93, 1 (1991), 55 – 92.
42. 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.
43. François Pottier and Nadji Gauthier. 2006. Polymorphic typed defunctionalization and concretization. Higher-Order and Symbolic Computation 19, 1 (01 Mar 2006), 125–162.
44. 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 }.
45. John C. Reynolds. 1998. Definitional Interpreters Revisited. Higher-Order and Symbolic Computation 11, 4 (1998), 355–361.
46. 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.
47. 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.
48. 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.
49. 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.
50. 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.
51. 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.
52. David Van Horn and Matthew Might. 2012. Systematic abstraction of abstract machines. Journal of Functional Programming 22, 4-5 (2012), 705–746.
53. 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.
54. 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.
55. 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.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Compilers

      • Interpreters

    • General programming languages

      • Language types

        • Functional languages

• Theory of computation

  • Models of computation

    • Abstract machines