Abstract allocation as a unified approach to polyvariance in control-flow analyses

Thomas Gilray, Michael D. Adams, and Matthew Might

Status: Published


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.


Thomas Gilray, Michael D. Adams, and Matthew Might. Abstract allocation as a unified approach to polyvariance in control-flow analyses. Journal of Functional Programming, 28:e18, 2018. doi: 10.1017/S0956796818000138.

BibTeX Entry

  author = {Gilray, Thomas and Adams, Michael D. and Might, Matthew},
  title = {Abstract allocation as a unified approach to polyvariance in control-flow analyses},
  journal = {Journal of Functional Programming},
  pages = {e18},
  year = {2018},
  volume = {28},
  publisher = {Cambridge University Press},
  doi = {10.1017/S0956796818000138},