Abstract Interpretation

patrick cousot

DMI, École Normale Supérieure, Paris ⟨cousot@dmi.ens.fr⟩ ⟨http://www.ens.fr/~cousot⟩

Abstract interpretation [Cousot and Cousot 1977, 1979] is a general theory for approximating the semantics of discrete dynamic systems, e.g. computations of programs. In particular program analysis algorithms can be constructively derived from these abstract semantics.

PRINCIPLES OF ABSTRACT INTERPRETATION

A semantics S of a programming language L associates a semantic value S[[p]] ∈ D in the semantic domain D to each program p of L. The semantic domain D can be transition systems (for small-step operational semantics), pomsets, traces, relations (for big-step operational semantics), higher-order functions (for denotational semantics), and so on. D is usually defined compositionally by induction on the structure of run-time objects (computations, data, etc.). S is defined compositionally by induction on the syntactical structure of programs, using e.g. fixpoint definitions to handle iteration, recursion, and the like.

An empirical approach to abstract interpretation consists in a priori choosing a problem-specific abstract semantics domain D^{♯} and an abstract semantics S^{♯} ∈ L ↦ D^{♯} which is designed intuitively for a specific language L. Then safety, correctness or soundness is established by proving that a soundness relation σ satisfies

∀p ∈ L : σ(S[[p]], S^{♯}[[p]]).

Permission to make digital/hard copy of part or all of this work for personnal or classroom use is granted without fee provided that the copies are not mage or distributed for profit or commercial advantage, the copyright notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or fee.

\begin{matrix}c \\ ◯ \end{matrix} ACM 0360-0300/96/0600-0324 $03.50

If the abstract semantics is computable (D^{♯} is usually assumed to be finite), we can infer that the abstract interpretation is sound in the sense that:

S[[p]] ∈ {S | σ(S, S^{♯}[[p]])},

which may be sufficient to prove program properties e.g. that some “programs cannot go wrong”. However, the choice of D^{♯} and σ offers no guideline for the design of the abstract semantics S^{♯} with respect to the concrete semantics S.

The approach propounded in [Cousot and Cousot 1977, 1979] is constructive in the sense that once the standard semantics S and an approximation α are chosen, one can derive the best choice for the corresponding abstract semantics S^{♯}. More precisely let us call elements of the powerset

D_{Coll} =^{def} ℘(D)

program (concrete) properties. Define S_{Coll} ∈ L ↦ D_{Coll} to be the collecting semantics:

S_{Coll}[[p]] =^{def} {S[[p]]}.

Abstract Interpretation  •  325

(This is a conceptual step, since no other detailed specification of S_{Coll} is needed, but for the design of formal proof methods). S_{Coll}[[p]] is the strongest program property. We have seen that an abstract property P, such as {S | σ(S, S^{♯}[[p]])} above, is weaker in that S_{Coll}[[p]] ⊆ P. We call ⊆ the approximation ordering. Now the abstraction function is a map α ∈ D_{Coll} ↦ D_{Coll}. We call α[D] =^{def} {α(S) | S ∈ D} the abstract domain. We often use an isomorphic representation D^{♯} for α[D] and directly define α ∈ D_{Coll} ↦ D^{♯}. An example would be the approximation of a trace-based semantics by a relational/denotational semantics:

α(P) =^{def} {⟨s_{0}, s_{n}⟩ | s_{0}s_{1} … s_{n} ∈ P }

∪ {⟨s_{0}, ⊥⟩ | s_{0}s_{1} … ∈ P is an infinite trace}.

Another approximation, ignoring distinction between finite and infinite computations, would be the approximation of traces by sets of states:

α(P) =^{def} {s_{i} | ∃s_{0}s_{1} … s_{i} … ∈ P },

which is adequate for safety/invariance properties.

Once such abstract domain D^{♯} and abstraction function α have been chosen, it remains to derive the abstract semantics S^{♯}[[p]], p ∈ L. We proceed compositionally, by induction on the syntactic structure of program p. The price to pay is that in general the ideal α(S_{Coll}[[p]]) has to be approximated by S^{♯}[[p]] ⊇ α(S_{Coll}[[p]]). For example, consider a fixpoint definition (for some syntactic construct p(p_{1}, …, p_{n}) with components p_{1}, …, p_{n}):

S[[p(p_{1}, …, p_{n})]] =^{def} lfp^{⊑} F_{p}

· [S[[p_{1}]], …, S[[p_{n}]]].

For simplicity, we consider the simple case when the computational ordering ⊑ coincide with the approximation ordering ⊆. Assuming, by induction hypothesis, that we know a sound abstract semantics for the program components p_{1}, …, p_{n}:

α(S_{Coll}[[p_{i}]]) ⊆ S^{♯}[[p_{i}]], i = 1, …, n ,

then we look, by algebraic formula manipulation, for F_{p}^{♯} satisfying for all C_{1}, …, C_{n} ∈ D_{Coll}:

\begin{matrix}α(\{F_{p}[S_{1}, …, S_{n}]|∀i = 1, …, n:S_{i}∈C_{i}\}) \\ ⊆ F_{p}^{♯}[α(C_{1}), …, α(C_{n})] \end{matrix}

in order to conclude (under suitable hypotheses, see Cousot and Cousot [1979]) that

\begin{matrix}α(lfp^{⊑} F_{p}[C_{1}, …, C_{n}]) ⊆ lfp^{^{⊑}^{♯}} F_{p}^{♯} \\ · [α(C_{1}), …, α(C_{n})]. \end{matrix}

This leads to the definition of the abstract semantics:

\begin{matrix}S^{♯}[[p(p_{1}, …, p_{n})]] =^{def} lfp^{^{⊑}^{♯}} F_{p}^{♯} \\ · [S^{♯}[[p_{1}]], …, S^{♯}[[p_{n}]]], \end{matrix}

which is sound, by construction, so that no a posteriori verification is necessary. When equality holds, we have a completeness property which is useful to design hierarchies of semantics. By identifying useful abstract algebras consisting of an abstract domain D^{♯} and abstract operations F^{♯} corresponding to common primitive operations F used in the semantic definition of programming languages, one can design abstraction libraries of general scope. Finally, the abstraction can be parameterized with other abstractions in order to obtain generic semantic definitions and abstract interpreters. Contrary to e.g. type inference, soundness (and relative completeness) can be established once for all (may be parameterized by basic abstractions for generic implementations) and not for each particular instance of the program analysis problem.

326  •  P. Cousot

The abstract interpretation framework sketched above is based on an abstraction function α. The existence of a best (most precise) approximation among all the possible sound ones is ensured by choosing α as the upper-adjoint of a Galois connection. Other equivalent formulations using Moore families, closure operators, ideals, … where introduced in Cousot and Cousot [1979]. The case when the computational ordering ⊑ does not coincide with the approximation ordering ⊆ in their concrete or abstract versions is considered in Cousot and Cousot [1994]. Other alternatives are studied in Cousot and Cousot [1992] (using a soundness relation σ, a concretization γ, an abstraction/concretization pair ⟨α, γ⟩ or widenings, which allows for the degree of approximation to evolve during program analysis, so that the abstract domain D^{♯} is not fixed once and for all but evolves during the analysis) .

Under the influence of Mycroft’s early application of abstract interpretation to strictness analysis of lazy functional languages, the standard semantics S is often chosen to be a denotational semantics (see Jones and Nielson [1995] for a survey taking this point of view) which is mainly adequate for functional languages. The original operational-based abstract interpretation [Cousot 1981] turned out to be much more adequate for imperative, logic [Debray 1994] and more recently concurrent, distributed and object-oriented languages. A general framework unifies both point of views [Cousot and Cousot 1994], by lifting operational semantics to handle infinite behaviors, considering the equivalence between rule-based and fixpoint presentations of semantics specifications and viewing denotational semantics as part of a hierarchy of abstractions of operational semantics.

APPLICATION OF ABSTRACT INTERPRETATION

The most widespread use of abstract semantics S^{♯} is for the specification of program analyzers as used for highlyperformant compilers, program transformation (e.g. program vectorization and parallelization), partial evaluation, test generation for program debugging, abstract debugging (involving abstract values/properties instead of concrete ones), polymorphic type inference, effect systems, model checking, verification of hybrid systems, and the like.

An important aspect of research of abstract interpretation is concerned with the composable design of abstractions α by induction on the mathematical structure of the semantic domain D (which, for typed languages, often coincide with the type structure of the language) for all possible data and control structures encountered in programming languages. Let us consider a small range of samples of data abstractions:

– For attribute-independent abstractions of sets of vectors of numbers, one can consider signs, intervals, parity, simple congruences. For relational abstractions, one can consider linear equalities, linear inequalities, congruences, congruencial trapezoids, and so on.

– For the context-free abstraction of formal languages, one can consider regular expressions, grammars (thus making the link with set-based analysis). Unitary-prefix monomial decompositions of rational subsets of a free monoid (such as {X.tl^{m}.hd.tl^{n}.hd.tl^{p} | m = n = p}) provide an example of context-sensitive abstraction [Deutsch 1995]. These abstractions can be used for pointer analysis based on locationfree/storeless models of computation.

– For the abstraction of sets of graphs, as used e.g. in store-based pointer analysis, one can refer to Deutsch [1995]. To remain succint on control structures, let us consider the example of program loops which involve solving an equation X = F_{ℓ}^{♯}(X) originating from the fixpoint definition lfp^{^{⊑}^{♯}} F_{ℓ}^{♯} of the abstract semantics S^{♯}[[ℓ]] of a program ℓ. This is one of the typical algorithmic problems involved in abstract interpretation. One classical solution, when F_{ℓ}^{♯} is a monotonic operator on a poset ⟨D^{♯}, ⊑^{♯}⟩ with infimum ⊥, is iteration: X^{0} =^{def} ⊥, X^{n+1} =^{def} F_{ℓ}^{♯}(X^{n}) until convergence. Widenings [Cousot and Cousot 1977] can be used to accelerate convergence (in large or infinite domains) and cope with the lack of least upper bounds during fixpoint iteration. Widenings can be understood as local dynamic change of abstract semantic domain during the analysis [Cousot and Cousot 1992].

The complexity issues in abstract interpretation have only been touched upon. A common error is that abstract interpretation is thought to be inherently exponential (as opposed to polynomial dataflow analysis). This can be exactly the contrary! It can be polynomial or polynomial on the average but exponential in pathological cases which are rare enough to be cut off by widening (e.g. polymorphic type inference à la Hindley-Milner). In general, exponential costs can be avoided by using widenings introducing further approximation as analysis time elapses. The common idea that program analyzers should be as fast as compilers does not necessarily take the cost/benefit trade-off into account. Is it better to spend 8 (night) hours of CPU time or 8 (day) hours of man-power for finding a crucial programming error?

CONCLUSION AND RESEARCH PERSPECTIVES

Although the designer of program analyzers may prefer empirical approaches, abstract interpretation is often an indispensable guideline to avoid conceptual errors since it provides a methodology to design a formal specification. It provides a synthetic understanding of the abundant literature on semantics, type systems, logics of computations, program verification, program analysis, partial evaluation, and the like, all involving more or less refined or abstract semantics of computations.

A number of problems remains to be considered or more thoroughly studied, e.g.: Semantics

– general frameworks formalizing the notion of semantic approximation; – models of computations (e.g. true concurrency) to be used in concrete semantics;

– design of hierarchies of parameterized semantics for programming languages (such as concurrent and object-oriented languages); Domains

– abstract domains for non-numerical objects,

– design of abstraction functions specifying different program analysis methods in order to compare their relative power,

– decomposition/combination of existing program analyses; Algorithms

– equation resolution and convergence acceleration methods,

– compositional design of widenings; Abstract interpreters

– design and implementation of generalpurpose libraries of abstract domains and their associated operations;

– design of language-specific generic abstract interpreters; and

– formal or experimental study of the complexity/benefit tradeoff of program analyses.

REFERENCES

Cousot, P. 1981. Semantic foundations of program analysis. In Program Flow Analysis: Theory and Applications. S.S. Muchnick and N. Jones Eds., Prentice-Hall, Englewood Cliffs, NJ, Ch. 10, 303–342. Cousot, P. and Cousot, R. 1994. Higherorder abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), invited paper. In Proceedings of 1994 ICCL, Toulouse, France (May 16–19), IEEE, Los Alamitos, CA, 95–112.

Cousot, P. and Cousot, R. 1992. Abstract interpretation frameworks. J. of Logic and Comput. 2, 4 (Aug.), 511–547. Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In Proceedings of the 6th POPL (San Antonio, TX), ACM Press, New York, 269–282.

328  •  P. Cousot

Cousot, P. and Cousot, R. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th POPL (Los Angeles, CA), ACM Press, New York, 238–252.

Debray, S. K. 1994. Formal bases for dataflow analysis of logic programs. In Advances in Logic Programming Theory, International Schools for Computer Scientists, G. Levi, Ed., Clarendon Press, New York, Sect. 3, 115–182.

Deutsch, A. 1995. Semantic models and abstract interpretation techniques for inductive data structures and pointers. Invited paper. In Proceedings of PEPM ’95 (La Jolla, CA, June 21-23), ACM Press, New York, 226–229.

Jones, N. and Nielson, F. 1995. Abstract interpretation: a semantic-based tool for program analysis. In Semantic modelling, S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, Eds., number 4 in Handbook of Logic in Computer Science. Clarendon Press, New York.