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

Thomas Gilray, Michael D. Adams, Matthew Brendon Might

Research output: Contribution to journalArticle

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.

LanguageEnglish (US)
JournalJournal of Functional Programming
DOIs
StateAccepted/In press - Jan 1 2018

Fingerprint

Flow control
Semantics
Syntactics
Tuning

ASJC Scopus subject areas

  • Software

Cite this

Abstract allocation as a unified approach to polyvariance in control-flow analyses. / Gilray, Thomas; Adams, Michael D.; Might, Matthew Brendon.

In: Journal of Functional Programming, 01.01.2018.

Research output: Contribution to journalArticle

@article{4dfa129c77c64f07994a510f9a776444,
title = "Abstract allocation as a unified approach to polyvariance in control-flow analyses",
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.",
author = "Thomas Gilray and Adams, {Michael D.} and Might, {Matthew Brendon}",
year = "2018",
month = "1",
day = "1",
doi = "10.1017/S0956796818000138",
language = "English (US)",
journal = "Journal of Functional Programming",
issn = "0956-7968",
publisher = "Cambridge University Press",

}

TY - JOUR

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

AU - Gilray, Thomas

AU - Adams, Michael D.

AU - Might, Matthew Brendon

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85052663929&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85052663929&partnerID=8YFLogxK

U2 - 10.1017/S0956796818000138

DO - 10.1017/S0956796818000138

M3 - Article

JO - Journal of Functional Programming

T2 - Journal of Functional Programming

JF - Journal of Functional Programming

SN - 0956-7968

ER -