Reference. Abstracting abstract machines
Cite
Cited by (4)
Demand Control-Flow Analysis germane-2019-demand
Relatively Complete Pushdown Analysis of Escape Continuations germane-2019-relatively
Abstract allocation as a unified approach to polyvariance in control-flow analyses gilray-2018-abstract
In higher order settings, control-flow analysis aims to model the propagation of both data and control by finitely approximating program behaviors across all possible executions. The polyvariance of an analysis describes the number of distinct abstract representations, or variants, for each syntactic entity (e.g., functions, variables, or intermediate expressions). Monovariance, one of the most basic forms of polyvariance, maintains only a single abstract representation for each variable or expression. Other polyvariant strategies allow a greater number of distinct abstractions and increase analysis complexity with the aim of increasing analysis precision. For example, k -call sensitivity distinguishes flows by the most recent k call sites, k -object sensitivity by a history of allocation points, and argument sensitivity by a tuple of dynamic argument types. From this perspective, even a concrete operational semantics may be thought of as an unboundedly polyvariant analysis. In this paper, we develop a unified methodology that fully captures this design space. It is easily tunable and guarantees soundness regardless of how tuned. We accomplish this by extending the method of abstracting abstract machines, a systematic approach to abstract interpretation of operational abstract-machine semantics. Our approach permits arbitrary instrumentation of the underlying analysis and arbitrary tuning of an abstract-allocation function. We show that the design space of abstract allocators both unifies and generalizes existing notions of polyvariance. Simple changes to the behavior of this function recapitulate classic styles of analysis and yield novel combinations and variants.
Pushdown control-flow analysis for free gilray-2016-pushdown
Cites 31 works (1 here)
With notes (1)
Improving flow analyses via ΓCFA: abstract garbage collection and counting might-2006-improving
External (30)
- Control-flow analysis of functional programs (2012)
- Semantics Engineering with PLT Redex (2009)
- Control-flow analysis of function calls and returns by abstract interpretation (2009)
- A Calculational Approach to Control-Flow Analysis by Abstract Interpretation (2008)
- Types and trace effects of higher order programs (2008)
- Flow analysis of lazy higher-order functional programs (2007)
- A call-by-name lambda-calculus machine (2007)
- An Analytical Approach to Program as Data Objects (2006)
- A systematic approach to static access control (2005)
- A functional correspondence between call-by-need evaluators and lazy abstract machines (2004)
- A tail-recursive machine with stack inspection (2004)
- Modeling an Algebraic Stepper (2001)
- Static enforcement of security with types (2000)
- The calculational design of a generic abstract interpreter (1999)
- Optimizing lazy functional programs using flow inference (1995)
- Space-efficient closure representations (1994)
- The essence of compiling with continuations (1993)
- Abstract analysis and optimization of scheme (1993)
- Control-Flow Analysis of Higher-Order Languages (1991)
- Analysis and efficient implementation of functional programs (PhD thesis) (1991)
- The interprocedural analysis and automatic parallelization of Scheme programs (1989)
- A calculus for assignments in higher-order languages (1987)
- The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages (1987)
- Control operators, the SECD-machine, and the lambda-calculus (1986)
- Un interpréteur du lambda-calcul (1985)
- A flexible approach to interprocedural data flow analysis and programs with recursive data structures (1982)
- Flow analysis of lambda expressions (1981)
- Systematic design of program analysis frameworks (1979)
- Abstract interpretation (1977)
- The Mechanical Evaluation of Expressions (1964)