Reference. Abstract allocation as a unified approach to polyvariance in control-flow analyses
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.
Cite
Cites 54 works (3 here)
With notes (3)
Abstracting abstract machines vanhorn-2010-abstracting
Resolving and exploiting the -CFA paradox: illuminating functional vs. object-oriented program analysis might-2010-resolving
Improving flow analyses via ΓCFA: abstract garbage collection and counting might-2006-improving
External (51)
- Racket Programming Language (2015)
- A Survey of Polyvariance in Abstract Interpretations (2014)
- Concrete and abstract interpretation: Better together (2014)
- A unified approach to polyvariance in abstract interpretations (2013)
- Hash-flow taint analysis of higher-order programs (2012)
- Abstract Interpreters for Free (2010)
- Subcubic Control Flow Analysis Algorithms (2009)
- A Posteriori Soundness for Non-Deterministic Abstract Interpretations (2009)
- Compiling with Continuations (2007)
- Program Analysis Using Binary Decision Diagrams (2006)
- Context-Sensitive Points-to Analysis: Is it Worth It? (2006)
- Faithful Translations Between Polyvariant Flows and Polymorphic Types (2000)
- Type-Directed Flow Analysis for Typed Intermediate Languages (1997)
- A modular, polyvariant and type-based closure analysis (1997)
- The Cartesian Product Algorithm (1995)
- Making Type Inference Practical (1992)
- Control-Flow Analysis of Higher-Order Languages (1991)
- Natural Semantics (1987)
- A Structural Approach to Operational Semantics (1981)
- Program Flow Analysis: Theory and S pplications (1981)
- Static determination of dynamic properties of programs (1976)
- 10.1145/512950.512973
- 10.1145/1044834.1044835
- 10.1145/2678015.2682536
- 10.1145/1391984.1391987
- 10.1145/2500365.2500604
- 10.2140/pjm.1955.5.285
- 10.1145/2678015.2682542
- 10.1145/3062341.3062380
- 10.1145/271510.271523
- 10.1145/2398856.2364576
- 10.1145/1133981.1134018
- 10.1145/1411204.1411243
- 10.1145/155090.155113
- 10.1007/bf01808954
- 10.1145/582153.582161
- 10.1145/1557898.1557905
- 10.1145/1640089.1640108
- 10.1145/263699.263744
- 10.1145/567752.567778
- 10.1145/2951913.2951936
- 10.1145/2914770.2837631
- 10.1145/199448.199536
- 10.1145/2491956.2462191
- 10.1145/1291151.1291179
- 10.1145/1108792.1108797
- 10.1145/1863543.1863554
- 10.1145/2187671.2187672
- 10.1017/s095679680100394x
- 10.1145/1926385.1926390
- 10.1007/978-3-642-11957-6_30