David Van Horn
ABSTRACT
We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines. To demonstrate the technique and support our claim, we transform the CEK machine of Felleisen and Friedman, a lazy variant of Krivine's machine, and the stack-inspecting CM machine of Clements and Felleisen into abstract interpretations of themselves. The resulting analyses bound temporal ordering of program events; predict return-flow and stack-inspection behavior; and approximate the flow and evaluation of by-need parameters. For all of these machines, we find that a series of well-known concrete machine refactorings, plus a technique we call store-allocated continuations, leads to machines that abstract into static analyses simply by bounding their stores. We demonstrate that the technique scales up uniformly to allow static analysis of realistic language features, including tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection.
Supplemental Material
- }}Mads S. Ager, Olivier Danvy, and Jan Midtgaard. A functional correspondence between call-by-need evaluators and lazy abstract machines. Information Processing Letters, 90(5):223--232, June 2004. Google Scholar
Digital Library
- }}Andrew E. Ayers. Abstract analysis and optimization of Scheme. PhD thesis, Massachusetts Institute of Technology, 1993. Google ScholarDigital Library
- }}John Clements and Matthias Felleisen. A tail-recursive machine with stack inspection. ACM Trans. Program. Lang. Syst., 26(6):1029--1052, November 2004. Google ScholarDigital Library
- }}John Clements, Matthew Flatt, and Matthias Felleisen. Modeling an algebraic stepper. In ESOP '01: Proceedings of the 10th European Symposium on Programming Languages and Systems, pages 320--334, 2001. Google ScholarDigital Library
- }}Patrick Cousot. The calculational design of a generic abstract interpreter. In M. Broy and R. Steinbrüggen, editors, Calculational System Design. 1999.Google Scholar
- }}Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 238--252, 1977. Google ScholarDigital Library
- }}Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In POPL '79: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 269--282, 1979. Google ScholarDigital Library
- }}Olivier Danvy. An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, Aarhus University, October 2006.Google Scholar
- }}Karl Faxén. Optimizing lazy functional programs using flow inference. In Static Analysis, pages 136--153. 1995. Google ScholarDigital Library
- }}Matthias Felleisen. The Calculi of Lambda-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Indiana University, 1987. Google ScholarDigital Library
- }}Matthias Felleisen, Robert B. Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. August 2009. Google ScholarDigital Library
- }}Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD-machine, and the lambda-calculus. In 3rd Working Conference on the Formal Description of Programming Concepts, August 1986.Google Scholar
- }}Mattias Felleisen and D. P. Friedman. A calculus for assignments in higher-order languages. In POPL '87: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 314+, 1987. Google ScholarDigital Library
- }}Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In PLDI '93: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, pages 237--247, June 1993. Google ScholarDigital Library
- }}Williams L. Harrison. The interprocedural analysis and automatic parallelization of scheme programs. LISP and Symbolic Computation, 2(3):179--396, October 1989.Google ScholarCross Ref
- }}N. Jones and N. Andersen. Flow analysis of lazy higher-order functional programs. Theoretical Computer Science, 375(1-3):120--136, May 2007. Google ScholarDigital Library
- }}Neil D. Jones. Flow analysis of lambda expressions (preliminary version). In Proceedings of the 8th Colloquium on Automata, Languages and Programming, pages 114--128, 1981. Google ScholarDigital Library
- }}Neil D. Jones and Steven S. Muchnick. 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, pages 66--74, 1982. Google ScholarDigital Library
- }}Jean-Louis Krivine. Un interpréteur du lambda-calcul. 1985.Google Scholar
- }}Jean-Louis Krivine. A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, 20(3):199--207, September 2007. Google ScholarDigital Library
- }}Peter J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308--320, 1964.Google ScholarCross Ref
- }}Jan Midtgaard. Control-flow analysis of functional programs. Technical Report BRICS RS-07-18, DAIMI, Department of Computer Science, University of Aarhus, December 2007. To appear in revised form in ACM Computing Surveys.Google ScholarCross Ref
- }}Jan Midtgaard and Thomas Jensen. A calculational approach to control-flow analysis by abstract interpretation. In María Alpuente and Germán Vidal, editors, SAS, volume 5079 of Lecture Notes in Computer Science, pages 347--362, 2008. Google ScholarDigital Library
- }}Jan Midtgaard and Thomas P. Jensen. 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, pages 287--298, 2009. Google ScholarDigital Library
- }}Matthew Might and Olin Shivers. Improving flow analyses via?CFA: Abstract garbage collection and counting. In ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, pages 13--25, 2006. Google ScholarDigital Library
- }}François Pottier, Christian Skalka, and Scott Smith. A systematic approach to static access control. ACM Trans. Program. Lang. Syst., 27(2):344--382, March 2005. Google ScholarDigital Library
- }}Peter Sestoft. Analysis and efficient implementation of functional programs. PhD thesis, University of Copenhagen, October 1991.Google Scholar
- }}Zhong Shao and Andrew W. Appel. Space-efficient closure representations.In LFP '94: Proceedings of the 1994 ACM Conference on LISP and Functional Programming, pages 150--161, 1994. Google ScholarDigital Library
- }}Olin G. Shivers. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University, 1991. Google ScholarDigital Library
- }}Christian Skalka and Scott Smith. Static enforcement of security with types. In ICFP '00: Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming, pages 34--45, September 2000. Google ScholarDigital Library
- }}Christian Skalka, Scott Smith, and David Van Horn. Types and trace effects of higher order programs. Journal of Functional Programming, 18(02):179--249, 2008. Google ScholarDigital Library
Index Terms
- Abstracting abstract machines
Recommendations
Abstracting abstract machines
ICFP '10We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines. To demonstrate the technique and support our claim, we transform the CEK machine ...
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