Making abstract interpretations complete

By: R. Giacobazzi, F. Ranzato, and F. Scozzari

Roberto Giacobazzi
Dip. Scientifico e Tecnologico
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2, 37134 Verona (Italy)
giaco@sci.univr.it

Abstract:

Completeness is a desirable, although uncommon, feature of abstract interpretations, formalizing the intuition that, relatively to the properties encoded by the underlying abstract domains, there is no loss of information accumulated in abstract computations. Thus, complete abstract interpretations can be rightly understood as optimal. We deal with both pointwise completeness involving generic semantic operations and (least) fixpoint-based completeness. Both completeness and fixpoint completeness are shown to be properties that only depend on the underlying abstract domains. Our primary goal is then to solve the problem of making abstract interpretations complete by minimally extending or restricting the underlying abstract domains. Under the weak and reasonable hypothesis of dealing with continuous semantic operations, we provide constructive characterizations for the least complete extensions and the greatest complete restrictions of abstract domains. As far as fixpoint completeness is concerned, for merely monotone semantic operators, greatest fixpoint complete restrictions of abstract domains are constructively characterized, while it is shown that the existence of least fixpoint complete extensions cannot be, in general, guaranteed, even under strong hypotheses. These methodologies, which in finite settings give rise to effective algorithms, provide advanced formal tools for manipulating and comparing abstract interpretations, useful both in static program analysis and in semantics design. In the field of abstract interpretation-based program analysis, a number of examples illustrating these techniques are given.

Available from the JACM-upcoming page: paper2101.ps