Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-21T13:41:01.076Z Has data issue: false hasContentIssue false
  • English
  • Français

Systematic abstraction of abstract machines

Part of: JFP Research Articles

Published online by Cambridge University Press:  15 August 2012

DAVID VAN HORN  and
MATTHEW MIGHT
DAVID VAN HORN
Affiliation:
College of Computer and Information Science, Northeastern University, Boston, MA 02115, USA (e-mail: dvanhorn@ccs.neu.edu)
MATTHEW MIGHT
Affiliation:
School of Computing, University of Utah, Salt Lake City, UT 84112, USA (e-mail: might@cs.utah.edu
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines for higher-order and imperative programming languages. To demonstrate the technique and support our claim, we transform the CEK machine of Felleisen and Friedman (Proc. of the 14th ACM SIGACT-SIGPLAN Symp. Prin. Program. Langs, 1987, pp. 314–325), a lazy variant of Krivine's machine (Higher-Order Symb. Comput. Vol 20, 2007, pp. 199–207), and the stack-inspecting CM machine of Clements and Felleisen (ACM Trans. Program. Lang. Syst. Vol 26, 2004, pp. 1029–1052) 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 of store-allocated continuations, leads to machines that abstract into static analyses simply by bounding their stores. These machines are parameterized by allocation functions that tune performance and precision and substantially expand the space of analyses that this framework can represent. We demonstrate that the technique scales up uniformly to allow static analysis of realistic language features, including tail calls, conditionals, mutation, exceptions, first-class continuations, and even garbage collection. In order to close the gap between formalism and implementation, we provide translations of the mathematics as running Haskell code for the initial development of our method.

Type
Articles
Information
Journal of Functional Programming , Volume 22 , Special Issue 4-5: ICFP 2010 , September 2012 , pp. 705 - 746
Copyright
Copyright © Cambridge University Press 2012

References

Ager, M. S., Danvy, O. & Midtgaard, J. (2004, June) A functional correspondence between call-by-need evaluators and lazy abstract machines. Inf. Process. Lett. 90 (5), 223–232.CrossRefGoogle Scholar
Ashley, J. M. & Dybvig, R. K. (1998) A practical and flexible flow analysis for higher-order languages. ACM Trans. Program. Lang. Syst. 20 (4), 845–868.CrossRefGoogle Scholar
Ayers, A. E. (1993) Abstract Analysis and Optimization of Scheme. PhD. thesis, Cambridge, MA, USA.Google Scholar
Biernacka, M. & Danvy, O. (2007) A concrete framework for environment machines. ACM Trans. Comput. Logic 9 (1), 1–30.CrossRefGoogle Scholar
Bouajjani, A., Esparza, J. & Maler, O. (1997) Reachability analysis of pushdown automata: Application to model-checking. In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR '97) Warsaw, Poland, pp. 135–150.CrossRefGoogle Scholar
Clements, J. & Felleisen, M. (2004, November) A tail-recursive machine with stack inspection. ACM Trans. Program. Lang. Syst. 26 (6), 1029–1052.CrossRefGoogle Scholar
Clements, J., Flatt, M. & Felleisen, M. (2001) Modeling an algebraic stepper. In Proceedings of the 10th European Symposium on Programming Languages and Systems (ESOP '01), pp. 320–334.CrossRefGoogle Scholar
Cousot, P. (1999) The calculational design of a generic abstract interpreter. In Calculational System Design, Broy, M. & Steinbrüggen, R. (eds), NATO ASI Series F. IOS Press, Amsterdam, pp. 421–506.Google Scholar
Cousot, P. & Cousot, R. (1977) 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, Atlanta, GA, USA pp. 238–252.Google Scholar
Cousot, P. & Cousot, R. (1979) Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '79), San Antonio, TX, USA, pp. 269–282.Google Scholar
Danvy, O. (2006, October) An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, Aarhus University, Aarhus, Denmark.Google Scholar
Danvy, O. & Nielsen, L. R. (2004, November) Refocusing in reduction semantics. Research Report BRICS RS-04-26, Department of Computer Science, Aarhus University, Denmark. (A preliminary version appeared in the informal Proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science, vol. 59.4.)CrossRefGoogle Scholar
Earl, C., Might, M. & Van Horn, D. (2010) Pushdown control-flow analysis of higher-order programs. In Workshop on Scheme and Functional Programming, Montreal, Canada, pp. 24–35.Google Scholar
Faxén, K. (1995) Optimizing lazy functional programs using flow inference. In Static Analysis, Lecture Notes in Computer Science, vol. 983, Springer, pp. 136–153.CrossRefGoogle Scholar
Felleisen, M. (1987) The Calculi of Lambda-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD. thesis, Indiana University, Indianapolis, IN, USA.Google Scholar
Felleisen, M., Findler, R. B. & Flatt, M. (2009, August) Semantics Engineering with PLT Redex. Cambridge, MA: MIT Press.Google Scholar
Felleisen, M. & Friedman, D. P. (1986, August) Control operators, the SECD-machine, and the Lambda-Calculus. In Proceedings of the IFIP TC 2/WG2.2 Working Conference on Formal Description of Programming Concepts Part III, Ebberup, Denmark, pp. 193–219.Google Scholar
Felleisen, M. & Friedman, D. P. (1987) A calculus for assignments in higher-order languages. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages POPL '87, Munich, Germany, pp. 314–325.Google Scholar
Flanagan, C., Sabry, A., Duba, B. F. & Felleisen, M. (1993, June) The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation (PLDI '93), Albuquerque, NM, USA, pp. 237–247.CrossRefGoogle Scholar
Harrison, W. L. (1989, October) The interprocedural analysis and automatic parallelization of scheme programs. LISP Symb. Comput. 2 (3), 179–396.Google Scholar
Jones, N. D. (1981) Flow analysis of lambda expressions (preliminary version). In Proceedings of the 8th Colloquium on Automata, Languages and Programming, Acre (Akko), Israel, pp. 114–128.CrossRefGoogle Scholar
Jones, N. & Andersen, N. (2007, May) Flow analysis of lazy higher-order functional programs. Theor. Comput. Sci. 375 (1–3), 120–136.CrossRefGoogle Scholar
Jones, N. D. & Muchnick, S. S. (1982) A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '82), Albuquerque, NM, USA, pp. 66–74.Google Scholar
Kodumal, J. & Aiken, A. (2004, June) The set constraint/CFL reachability connection in practice. In Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation (PLDI '04), Washington, DC, USA, pp. 207–218.CrossRefGoogle Scholar
Krivine, J.-L. (1985) Un interpréteur du lambda-calcul. Technical report, Notes de cours de. DEA, Universite de Paris 7.Google Scholar
Krivine, J.-L. (2007, September) A call-by-name lambda-calculus machine. Higher-Order Symb. Comput. 20 (3), 199–207.CrossRefGoogle Scholar
Landin, P. J. (1964) The mechanical evaluation of expressions. Comput. J. 6 (4), 308–320.CrossRefGoogle Scholar
Meunier, P., Findler, R. B. & Felleisen, M. (2006, January) Modular set-based analysis from contracts. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '06), Charleston, SC, USA, pp. 218–231.CrossRefGoogle Scholar
Midtgaard, J. (2012, June) Control-flow analysis of functional programs. ACM Comput. Surv. 44 (3), 10:1–10:33.CrossRefGoogle Scholar
Midtgaard, J. & Jensen, T. (2008) A calculational approach to Control-Flow analysis by abstract interpretation. In SAS, Alpuente, M. and Vidal, G. (eds), LNCS vol. 5079. Heidelberg, Germany: Springer, pp. 347–362.Google Scholar
Midtgaard, J. & Jensen, T. P. (2009) Control-flow analysis of function calls and returns by abstract interpretation. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09), Edinburgh, Scotland, pp. 287–298.CrossRefGoogle Scholar
Might, M. & Shivers, O. (2006) Improving flow analyses via Gamma-CFA: Abstract garbage collection and counting. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming (ICFP '06), Portland, OR, USA, pp. 13–25.Google Scholar
Morrisett, G., Felleisen, M. & Harper, R. (1995) Abstract models of memory management. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture (FPCA '95), La Jolla, CA, USA, pp. 66–77.CrossRefGoogle Scholar
Nielson, F., Nielson, H. R. & Hankin, C. (1999) Principles of Program Analysis. New York: Springer.CrossRefGoogle Scholar
Pottier, F., Skalka, C. & Smith, S. (2005, March) A systematic approach to static access control. ACM Trans. Program. Lang. Syst. 27 (2), 344–382.CrossRefGoogle Scholar
Reps, T. (1998, December) Program analysis via graph reachability. Inf. Softw. Technol. 40 (11–12), 701–726.CrossRefGoogle Scholar
Reynolds, J. C. (1972) Definitional interpreters for higher-order programming languages. In Proceedings of the ACM Annual Conference (ACM 1972), New York, USA, pp. 717–740.Google Scholar
Sestoft, P. (1991, October) Analysis and Efficient Implementation of Functional Programs. PhD. thesis, University of Copenhagen, Denmark.Google Scholar
Shao, Z. & Appel, A. W. (1994) Space-efficient closure representations. In Proceedings of the 1994 ACM Conference on LISP and Functional Programming (LFP '94), New York, USA, pp. 150–161.CrossRefGoogle Scholar
Sharir, M. & Pnueli, A. (1981) Approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, Jones, Neil D. and Muchnick, Steven S. (eds), Ch. 7. Upper Saddle River, NJ: Prentice-Hall, pp. 189–234.Google Scholar
Shivers, O. G. (1991) Control-Flow Analysis of Higher-Order Languages. PhD. thesis, Carnegie Mellon University, Pittsburgh, PA, USA.Google Scholar
Skalka, C. & Smith, S. (2000, September) Static enforcement of security with types. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, pp. 34–45.CrossRefGoogle Scholar
Skalka, C., Smith, S. & Van Horn, D. (2008) Types and trace effects of higher order programs. J. Funct. Program. 18 (02), 179–249.CrossRefGoogle Scholar
Van Horn, D. & Might, M. (2010) Abstracting abstract machines. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP '10), Baltimore, MD, USA, pp. 51–62.CrossRefGoogle Scholar
Van Horn, D. & Might, M. (2011, September) Abstracting abstract machines: A systematic approach to higher-order program analysis. Commun. ACM 54 (9), 101–109.CrossRefGoogle Scholar
Vardoulakis, D. & Shivers, O. (2011, May) CFA2: A context-free approach to control-flow analysis. Logical Methods Comput. Sci. 7 (2), 1–39.Google Scholar
Wright, A. K. & Jagannathan, S. (1998) Polymorphic splitting: An effective polyvariant flow analysis. ACM Trans. Program. Lang. Syst. 20 (1), 166–207.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.