Dionna Glaze
ABSTRACT
The strength of a dynamic language is also its weakness: run-time flexibility comes at the cost of compile-time predictability. Many of the hallmarks of dynamic languages such as closures, continuations, various forms of reflection, and a lack of static types make many programmers rejoice, while compiler writers, tool developers, and verification engineers lament. The dynamism of these features simply confounds statically reasoning about programs that use them. Consequently, static analyses for dynamic languages are few, far between, and seldom sound.
The "abstracting abstract machines" (AAM) approach to constructing static analyses has recently been proposed as a method to ameliorate the difficulty of designing analyses for such language features. The approach, so called because it derives a function for the sound and computable approximation of program behavior starting from the abstract machine semantics of a language, provides a viable approach to dynamic language analysis since all that is required is a machine description of the interpreter.
The AAM recipe as originally described produces finite state abstractions: the behavior of a program is approximated as a finite state machine. Such a model is inherently imprecise when it comes to reasoning about the control stack of the interpreter: a finite state machine cannot faithfully represent a stack. Recent advances have shown that higher-order programs can be approximated with pushdown systems. However, such models, founded in automata theory, either breakdown or require significant engineering in the face of dynamic language features that inspect or modify the control stack.
In this paper, we tackle the problem of bringing pushdown flow analysis to the domain of dynamic language features. We revise the abstracting abstract machines technique to target the stronger computational model of pushdown systems. In place of automata theory, we use only abstract machines and memoization. As case studies, we show the technique applies to a language with closures, garbage collection, stack-inspection, and first-class composable continuations.
Supplemental Material
Available for Download
Install Racket v5.3 or newer, and run any file to see some test programs' abstract traces.
- Massimo Bartoletti, Pierpaolo Degano, and Gian L. Ferrari. Stack inspection and secure program transformations. International Journal of Information Security, 2(3-4), 2004. Google Scholar
Digital Library
- Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. On the static and dynamic extents of delimited continuations. Science of Computer Programming, 60(3), 2006. Google ScholarDigital Library
- Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR '97: Concurrency Theory, 1997. Google ScholarDigital Library
- Byeong-Mo Chang. Static check analysis for Java stack inspection. SIGPLAN Notices, 41(3), 2006. Google ScholarDigital Library
- John Clements and Matthias Felleisen. A tail-recursive machine with stack inspection. ACM Trans. Program. Lang. Syst., 26(6), 2004. Google ScholarDigital Library
- Stephen A. Cook. Linear time simulation of deterministic two-way pushdown automata. In IFIP Congress (1), 1971.Google Scholar
- P. Cousot. Abstract interpretation and application to static analysis (invited tutorial). Part I: Basic concepts of abstract interpretation; Part II: Applications of abstract interpretation. In Proc. First IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, 2007.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 POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977. Google ScholarDigital Library
- Patrick Cousot, Radhia Cousot, Jerome Feret, Laurent Mauborgne, Antoine Mine, David Monniaux, and Xavier Rival. Varieties of static analyzers: A comparison with Astree, invited paper. In Proc. First IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, 2007. Google ScholarDigital Library
- Olivier Danvy. An Analytical Approach to Program as Data Objects . DSc thesis, Department of Computer Science, Aarhus University, 2006.Google Scholar
- Olivier Danvy and Andrzej Filinski. Abstracting control. In LFP '90: Proceedings of the 1990 ACM conference on LISP and functional programming, 1990. Google ScholarDigital Library
- Christopher Earl, Matthew Might, and David Van Horn. Pushdown control-flow analysis of higher-order programs. In 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 Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, 2012. Google ScholarDigital Library
- Matthias Felleisen, Robert B. Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. 2009. Google ScholarDigital Library
- Andrzej Filinski. Representing monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1994. Google ScholarDigital Library
- Robert B. Findler and Matthias Felleisen. Contracts for higher-order functions. In ICFP '02: Proceedings of the seventh ACM SIGPLAN International Conference on Functional Programming, 2002. Google ScholarDigital Library
- Robert Gluck. Simulation of two-way pushdown automata revisited. In Semantics, Abstract Interpretation, and Reasoning about Pro- grams: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, 2013.Google ScholarCross Ref
- Dionna Glaze, Nicholas Labich, Matthew Might, and David Van Horn. Optimizing abstract abstract machines. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, 2013. Google ScholarDigital Library
- J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, and David Van Horn. Pushdown flow analysis with abstract garbage collection. Journal of Functional Programming, 24(2-3), 2014.Google ScholarCross Ref
- Neil D. Jones. A note on linear time simulation of deterministic two-way pushdown automata. Inf. Process. Lett., 6(4):110--112, August 1977.Google ScholarCross Ref
- Vineeth Kashyap, Kyle Dewey, Ethan A. Kuefner, John Wagner, Kevin Gibbons, John Sarracino, Ben Wiedermann, and Ben Hard- ekopf. JSAI: Designing a sound, configurable, and efficient static analyzer for JavaScript. CoRR, abs/1403.3996, 2014.Google Scholar
- Oleg Kiselyov. An argument against call/cc, 2012. http://okmij.org/ftp/continuations/against-callcc.html.Google Scholar
- Oleg Kiselyov and Chung chieh Shan. Delimited continuations in operating systems. In Modeling and Using Context, 2007. Google ScholarDigital Library
- George Kuan, David MacQueen, and Robert B. Findler. A rewriting semantics for type inference. In Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, volume 4421, 2007. Google ScholarDigital Library
- Jay McCarthy. Concerning PLT webserver commit 72ec6342ea. private communication.Google Scholar
- Matthew Might and Olin Shivers. Improving flow analyses via CFA: Abstract garbage collection and counting. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, 2006. Google ScholarDigital Library
- Matthew Might, Benjamin Chambers, and Olin Shivers. Model checking via CFA. In Proceedings of the 8th International Conference on Verification, Model Checking and Abstract Interpretation, 2007. Google ScholarDigital Library
- Steven S. Muchnick and Neil D. Jones. Program Flow Analysis: Theory and Applications. Prentice Hall, 1981. Google ScholarDigital Library
- Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, and Kwangkeun Yi. Design and implementation of sparse global analyses for C-like languages. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012. Google ScholarDigital Library
- Christian Queinnec. Continuations and web servers. Higher-Order and Symbolic Computation, 17(4), 2004. Google ScholarDigital Library
- John H. Reif and Harry R. Lewis. Symbolic evaluation and the global value graph. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977. Google ScholarDigital Library
- Thomas Reps, Susan Horwitz, and Mooly Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995. Google ScholarDigital Library
- S. Salvati and I. Walukiewicz. Krivine machines and higher-order schemes. In Proceedings of the 38th International Conference on Automata, Languages and Programming, 2011. Google ScholarDigital Library
- Stefan Schwoon and Javier Esparza. A note on On-the-Fly verification algorithms. In Tools and Algorithms for the Construction and Analysis of Systems. 2005. Google ScholarDigital Library
- Olin Shivers and Aaron J. Turon. Modular rollback through control logging: A pair of twin functional pearls. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, 2011. Google ScholarDigital Library
- Olin G. Shivers. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University, 1991. Google ScholarDigital Library
- David Van Horn and Matthew Might. Abstracting abstract machines. In 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, 22(Special Issue 4-5), 2012. Google ScholarDigital Library
- Dimitrios Vardoulakis. CFA2: Pushdown Flow Analysis for Higher-Order Languages. PhD thesis, Northeastern University, 2012. Google ScholarDigital Library
- Dimitrios Vardoulakis and Olin Shivers. CFA2: a Context-Free approach to Control-Flow analysis. Logical Methods in Computer Science, 7(2), 2011.Google Scholar
- Dimitrios Vardoulakis and Olin Shivers. Pushdown flow analysis of first-class control. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, 2011. Google ScholarDigital Library
- Mark N. Wegman and F. Kenneth Zadeck. Constant propagation with conditional branches. ACM Trans. Program. Lang. Syst., 13(2), 1991. Google ScholarDigital Library
- Kwangkeun Yi, Hosik Choi, Jaehwang Kim, and Yongdai Kim. An empirical study on classification methods for alarms from a bug-finding static C analyzer. Inf. Process. Lett., 102(2-3), 2007. Google ScholarDigital Library
Index Terms
- Abstracting abstract control
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 perform ...
Pushdown control-flow analysis for free
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesTraditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Abstracting abstract control
DLS '14The strength of a dynamic language is also its weakness: run-time flexibility comes at the cost of compile-time predictability. Many of the hallmarks of dynamic languages such as closures, continuations, various forms of reflection, and a lack of static ...
Comments