David Darais
Nicholas Labich
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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 nice basis for a wide variety of collecting semantics, abstract interpretations, symbolic executions, and their intermixings.
But the real insight of this story is a replaying of an insight from Reynold's landmark paper, Definitional Interpreters for Higher-Order Programming Languages, in which he observes definitional interpreters enable the defined-language to inherit properties of the defining-language. We show the same holds true for definitional abstract interpreters. Remarkably, we observe that abstract definitional interpreters can inherit the so-called “pushdown control flow” property, wherein function calls and returns are precisely matched in the abstract semantics, simply by virtue of the function call mechanism of the defining-language.
The first approaches to achieve this property for higher-order languages appeared within the last ten years, and have since been the subject of many papers. These approaches start from a state-machine semantics and uniformly involve significant technical engineering to recover the precision of pushdown control flow. In contrast, starting from a definitional interpreter, the pushdown control flow property is inherent in the meta-language and requires no further technical mechanism to achieve.
Supplemental Material
Available for Download
zip
icfp17-main114-s.zip (845 MB)
This reusable artifact is an open-format virtual machine containing the Abstracting Definitional Interpreters framework, implementations, tests, and paper. See the included README for full instructions. To build the library, run the unit tests, and compile/execute the paper as a literate racket program, just boot the virtual machine and run the following commands: $ cd ~/monadic-eval $ make $ make test $ make pdf
- Mads S. Ager, Olivier Danvy, and Jan Midtgaard. A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theoretical Computer Science, 2005. Google Scholar
Digital Library
- Roland N Bol and Lars Degerstedt. Tabulated Resolution for Well Founded Semantics. In Proc. ILPS, 1993.Google Scholar
- Weidong Chen and David S Warren. Tabled evaluation with delaying for general logic programs. Journal of the ACM (JACM) 43(1), pp. 20–74, 1996. Google ScholarDigital Library
- David Darais, Matthew Might, and David Van Horn. Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis. In Proc. Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2015.Google Scholar
- Steven Dawson, C. R. Ramakrishnan, and David S. Warren. Practical Program Analysis Using General Purpose Logic Programming Systems—a Case Study. In Proc. Proceedings of the ACM SIGPLAN 1996 Conference on Programming Language Design and Implementation, 1996.Google ScholarDigital Library
- Christopher Earl. Introspective Pushdown Analysis and Nebo. PhD dissertation, University of Utah, 2014.Google Scholar
- Christopher Earl, Matthew Might, and David Van Horn. Pushdown control-flow analysis of higher-order programs. In Proc. Workshop on Scheme and Functional Programming, 2010.Google Scholar
- Christopher Earl, Ilya Sergey, Matthew Might, and David Van Horn. Introspective pushdown analysis of higher-order programs. In Proc. Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, 2012. Google ScholarDigital Library
- Sebastian Fischer, Oleg Kiselyov, and Chung-chieh Shan. Purely functional lazy nondeterministic programming. Journal of Functional Programming 21(4-5), pp. 413–465, 2011. Google ScholarDigital Library
- Matthew Flatt and Matthias Felleisen. Units: Cool Modules for HOT Languages. In Proc. Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation, 1998. Google ScholarDigital Library
- Matthew Flatt and PLT. Reference: Racket. PLT Inc., 2010.Google Scholar
- Daniel P. Friedman and Anurag Medhekar. Tutorial: Using an Abstracted Interpreter to Understand Abstract Interpretation, Course notes for CSCI B621, Indiana University. 2003.Google Scholar
- Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, and David Van Horn. Pushdown Controlflow Analysis for Free. In Proc. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016.Google Scholar
- Robert Glück. Simulation of Two-Way Pushdown Automata Revisited. In Proc. Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, Manhattan, Kansas, USA, 19-20th September 2013, 2013. Google ScholarCross Ref
- Ralf Hinze. Deriving Backtracking Monad Transformers. In Proc. Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, 2000. Google ScholarDigital Library
- Suresh Jagannathan, Peter Thiemann, Stephen Weeks, and Andrew Wright. Single and loving it: must-alias analysis for higher-order languages. In Proc. POPL ’98: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1998. Google ScholarDigital Library
- Suresh Jagannathan and Stephen Weeks. A unified treatment of flow analysis in higher-order languages. In Proc. POPL ’95: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995. Google ScholarDigital Library
- Gerda Janssens and Konstantinos F Sagonas. On the Use of Tabling for Abstract Interpretation: An Experiment with Abstract Equation Systems. In Proc. TAPD, 1998.Google Scholar
- Mauro Javier Jaskelioff. Lifting of operations in modular monadic semantics. PhD dissertation, University of Nottingham, 2009.Google Scholar
- J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, and David Van Horn. Pushdown flow analysis with abstract garbage collection. Journal of Functional Programming, 2014.Google ScholarCross Ref
- J. Ian Johnson and David Van Horn. Abstracting Abstract Control. In Proc. Proceedings of the 10th ACM Symposium on Dynamic Languages, 2014.Google Scholar
- Neil D. Jones and Flemming Nielson. Abstract Interpretation: A Semantics-based Tool for Program Analysis. In Proc. Handbook of Logic in Computer Science (Vol. 4), 1995.Google Scholar
- James C. King. Symbolic Execution and Program Testing. Commun. ACM, 1976.Google ScholarDigital Library
- Oleg Kiselyov. Typed tagless final interpreters. In Proc. Generic and Indexed Programming, 2012. Google ScholarDigital Library
- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry. Backtracking, Interleaving, and Terminating Monad Transformers: (Functional Pearl). In Proc. Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, 2005. Google ScholarDigital Library
- Sheng Liang, Paul Hudak, and Mark Jones. Monad Transformers and Modular Interpreters. In Proc. Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995. Google ScholarDigital Library
- Jan Midtgaard. Control-flow Analysis of Functional Programs. ACM Comput. Surv., 2012. Google ScholarDigital Library
- Jan Midtgaard and Thomas Jensen. A Calculational Approach to Control-FlowAnalysis by Abstract Interpretation. In Proc. Static Analysis Symposium, 2008. Google ScholarDigital Library
- Jan Midtgaard and Thomas P. Jensen. Control-flow Analysis of Function Calls and Returns by Abstract Interpretation. In Proc. ICFP ’09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, 2009. Google ScholarDigital Library
- Matthew Might. Environment analysis of higher-order languages. PhD dissertation, Georgia Institute of Technology, 2007a.Google Scholar
- Matthew Might. Logic-flow Analysis of Higher-order Programs. In Proc. Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007b. Google ScholarDigital Library
- Matthew Might and Olin Shivers. Environment analysis via ∆-CFA. In Proc. POPL ’06: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006a.Google ScholarDigital Library
- Matthew Might and Olin Shivers. Improving Flow Analyses via ΓCFA: Abstract Garbage Collection and Counting. In Proc. ICFP’06, 2006b. Google ScholarDigital Library
- Matthew Might and David Van Horn. A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-OrderPrograms. In Proc. Static Analysis, 2011.Google Scholar
- Eugenio Moggi. An Abstract View of Programming Languages. Edinburgh University, 1989.Google Scholar
- Greg Morrisett, Matthias Felleisen, and Robert Harper. Abstract Models of Memory Management. In Proc. Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, 1995. Google ScholarDigital Library
- Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn. Soft Contract Verification. In Proc. Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, 2014. Google ScholarDigital Library
- Phúc C. Nguyễn and David Van Horn. Relatively Complete Counterexamples for Higher-order Programs. In Proc. Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015. Google ScholarDigital Library
- Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Principles of Program Analysis. 1999.Google Scholar
- Atze van der Ploeg and Oleg Kiselyov. Reflection without remorse: revealing a hidden sequence to speed up monadic reflection. In Proc. Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, 2014.Google Scholar
- John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proc. ACM ’72: Proceedings of the ACM Annual Conference, 1972. Google ScholarDigital Library
- Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, and Frank Piessens. Monadic Abstract Interpreters. In Proc. Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013. Google ScholarDigital Library
- Olin Shivers. Control-flow analysis of higher-order languages. PhD dissertation, Carnegie Mellon University, 1991.Google Scholar
- Guy L. Steele Jr. Building Interpreters by Composing Monads. In Proc. Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1994. Google ScholarDigital Library
- Terrance Swift and David S Warren. XSB: Extending Prolog with tabled logic programming. Theory and Practice of Logic Programming 12(1-2), pp. 157–187, 2012. Google ScholarDigital Library
- Hisao Tamaki and Taisuke Sato. OLD resolution with tabulation. In Proc. International Conference on Logic Programming, 1986. Google ScholarCross Ref
- Sam Tobin-Hochstadt, Vincent St-Amour, Ryan Culpepper, Matthew Flatt, and Matthias Felleisen. Languages As Libraries. In Proc. Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011. Google ScholarDigital Library
- Sam Tobin-Hochstadt and David Van Horn. Higher-order symbolic execution via contracts. In Proc. Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, 2012. Google ScholarDigital Library
- David Van Horn and Matthew Might. Abstracting Abstract Machines. In Proc. Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, 2010. Google ScholarDigital Library
- David Van Horn and Matthew Might. Systematic abstraction of abstract machines. Journal of Functional Programming, 2012. Google ScholarDigital Library
- Alexander Vandenbroucke, Tom Schrijvers, and Frank Piessens. Fixing non-determinism. In Proc. IFL 2015: Symposium on the implementation and application of functional programming languages Proceedings, 2016.Google Scholar
- Dimitrios Vardoulakis. CFA2: Pushdown Flow Analysis for Higher-Order Languages. PhD dissertation, Northeastern University, 2012.Google Scholar
- Dimitrios Vardoulakis and Olin Shivers. CFA2: a Context-FreeApproach to Control-FlowAnalysis. Logical Methods in Computer Science, 2011. Google ScholarCross Ref
- Andrew K. Wright and Suresh Jagannathan. Polymorphic splitting: an effective polyvariant flow analysis. ACM Trans. Program. Lang. Syst., 1998.Google Scholar
Index Terms
- Abstracting definitional interpreters (functional pearl)
Recommendations
Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl)
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 ...
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 ...
Definitional interpreters for higher-order programming languages
ACM '72: Proceedings of the ACM annual conference - Volume 2Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters which are themselves written in a programming language based on the lambda calculus (i.e., an applicative language ...
Comments