Purity Analysis: An Abstract Interpretation Formulation

Autor:	Ganesan Ramalingam, Ravichandhran Madhavan, Kapil Vaswani
Rok vydání:	2011
Předmět:	Correctness Theoretical computer science Computer science Abstract interpretation Algorithm Graph
Zdroj:	Static Analysis ISBN: 9783642237010 SAS
Popis:	Salcianu and Rinard present a compositional purity analysis that computes a summary for every procedure describing its side-effects. In this paper, we formalize a generalization of this analysis as an abstract interpretation, present several optimizations and an empirical evaluation showing the value of these optimizations. The Salcianu-Rinard analysis makes use of abstract heap graphs, similar to various heap analyses and computes a shape graph at every program point of an analyzed procedure. The key to our formalization is to view the shape graphs of the analysis as an abstract state transformer rather than as a set of abstract states: the concretization of a shape graph is a function that maps a concrete state to a set of concrete states. The abstract interpretation formulation leads to a better understanding of the algorithm. More importantly, it makes it easier to change and extend the basic algorithm, while guaranteeing correctness, as illustrated by our optimizations.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::e6a98bd411d1d00bafcb4afaa4ee2856 https://doi.org/10.1007/978-3-642-23702-7_6 Zobrazit plný text záznamu