Abstract interpretation

Abstract interpretation of computer programs

Given a programming or specification language, abstract interpretation consists of giving several semantics linked by relations of abstraction. A semantics is a mathematical characterization of a possible behavior of the program. The most precise semantics, describing very closely the actual execution of the program, are called the concrete semantics. For instance, the concrete semantics of an imperative programming language may associate to each program the set of execution traces it may produce – an execution trace being a sequence of possible consecutive states of the execution of the program; a state typically consists of the value of the program counter and the memory locations (globals, stack and heap). More abstract semantics are then derived; for instance, one may consider only the set of reachable states in the executions (which amounts to considering the last states in finite traces).

The goal of static analysis is to derive a computable semantic interpretation at some point. For instance, one may choose to represent the state of a program manipulating integer variables by forgetting the actual values of the variables and only keeping their signs (+, − or 0). For some elementary operations, such as multiplication, such an abstraction does not lose any precision: to get the sign of a product, it is sufficient to know the sign of the operands. For some other operations, the abstraction may lose precision: for instance, it is impossible to know the sign of a sum whose operands are respectively positive and negative.

Sometimes a loss of precision is necessary to make the semantics decidable (see Rice's theorem and the halting problem). In general, there is a compromise to be made between the precision of the analysis and its decidability (computability), or tractability (computational cost).

In practice the abstractions that are defined are tailored to both the program properties one desires to analyze, and to the set of target programs. The first large scale automated analysis of computer programs with abstract interpretation was motivated by the accident that resulted in the destruction of the first flight of the Ariane 5 rocket in 1996.

Formalization

Let ${\displaystyle L}$ be an ordered set, called concrete set, and let ${\displaystyle L^{\prime }}$ be another ordered set, called abstract set. These two sets are related to each other by defining total functions that map elements from one to the other.

A function ${\displaystyle \alpha }$ is called an abstraction function if it maps an element ${\displaystyle x}$ in the concrete set ${\displaystyle L}$ to an element ${\displaystyle \alpha (x)}$ in the abstract set ${\displaystyle L^{\prime }}$. That is, element ${\displaystyle \alpha (x)}$ in ${\displaystyle L^{\prime }}$ is the abstraction of ${\displaystyle x}$ in ${\displaystyle L}$.

A function ${\displaystyle \gamma }$ is called a concretization function if it maps an element ${\displaystyle x^{\prime }}$ in the abstract set ${\displaystyle L^{\prime }}$ to an element ${\displaystyle \gamma (x^{\prime })}$ in the concrete set ${\displaystyle L}$. That is, element ${\displaystyle \gamma (x^{\prime })}$ in ${\displaystyle L}$ is a concretization of ${\displaystyle x^{\prime }}$ in ${\displaystyle L^{\prime }}$.

Let ${\displaystyle L_1}$, ${\displaystyle L_2}$, ${\displaystyle L_1^{\prime }}$, and ${\displaystyle L_2^{\prime }}$ be ordered sets. The concrete semantics ${\displaystyle f}$ is a monotonic function from ${\displaystyle L_1}$ to ${\displaystyle L_2}$. A function ${\displaystyle f^{\prime }}$ from ${\displaystyle L_1^{\prime }}$ to ${\displaystyle L_2^{\prime }}$ is said to be a valid abstraction of ${\displaystyle f}$ if, for all ${\displaystyle x^{\prime }}$ in ${\displaystyle L_1^{\prime }}$, we have ${\displaystyle (f\circ \gamma )(x^{\prime })\le (\gamma \circ f^{\prime })(x^{\prime })}$.

Program semantics are generally described using fixed points in the presence of loops or recursive procedures. Suppose that ${\displaystyle L}$ is a complete lattice and let ${\displaystyle f}$ be a monotonic function from ${\displaystyle L}$ into ${\displaystyle L}$. Then, any ${\displaystyle x^{\prime }}$ such that ${\displaystyle f(x^{\prime })\le x^{\prime }}$ is an overapproximation of the least fixed-point of ${\displaystyle f}$, which exists, according to the Knaster–Tarski theorem.

The difficulty is now to obtain such an ${\displaystyle x^{\prime }}$. If ${\displaystyle L^{\prime }}$ is of finite height, or at least verifies the ascending chain condition (all ascending sequences are ultimately stationary), then such an ${\displaystyle x^{\prime }}$ may be obtained as the stationary limit of the ascending sequence ${\displaystyle x_n^{\prime }}$ defined by induction as follows: ${\displaystyle x_0^{\prime }=\mathrm{\perp }}$ (the least element of ${\displaystyle L^{\prime }}$) and ${\displaystyle x_{n+1}^{\prime }=f^{\prime }(x_n^{\prime })}$.

In other cases, it is still possible to obtain such an ${\displaystyle x^{\prime }}$ through a (pair-)widening operator, defined as a binary operator ${\displaystyle \mathrm{\nabla }:L\times L\to L}$ which satisfies the following conditions:

1. For all ${\displaystyle x}$ and ${\displaystyle y}$, we have ${\displaystyle x\le x\mathrm{\nabla }y}$ and ${\displaystyle y\le x\mathrm{\nabla }y}$, and
2. For any ascending sequence ${\displaystyle (y_n^{\prime }{)}_{n\ge 0}}$, the sequence defined by ${\displaystyle x_0^{\prime }:=\mathrm{\perp }}$ and ${\displaystyle x_{n+1}^{\prime }:=x_n^{\prime }\mathrm{\nabla }{y}_n^{\prime }}$ is ultimately stationary. We can then take ${\displaystyle y_n^{\prime }=f^{\prime }(x_n^{\prime })}$.

In some cases, it is possible to define abstractions using Galois connections ${\displaystyle (\alpha ,\gamma )}$ where ${\displaystyle \alpha }$ is from ${\displaystyle L}$ to ${\displaystyle L^{\prime }}$ and ${\displaystyle \gamma }$ is from ${\displaystyle L^{\prime }}$ to ${\displaystyle L}$. This supposes the existence of best abstractions, which is not necessarily the case. For instance, if we abstract sets of couples ${\displaystyle (x,y)}$ of real numbers by enclosing convex polyhedra, there is no optimal abstraction to the disc defined by ${\displaystyle x^2+y^2\le 1}$.

Examples of abstract domains

Numerical abstract domains

One can assign to each variable ${\displaystyle x}$ available at a given program point an interval ${\displaystyle [L_x,H_x]}$. A state assigning the value ${\displaystyle v(x)}$ to variable ${\displaystyle x}$ will be a concretization of these intervals if, for all ${\displaystyle x}$, we have ${\displaystyle v(x)\in [L_x,H_x]}$. From the intervals ${\displaystyle [L_x,H_x]}$ and ${\displaystyle [L_y,H_y]}$ for variables ${\displaystyle x}$ and ${\displaystyle y}$, respectively, one can easily obtain intervals for ${\displaystyle x+y}$ (namely, ${\displaystyle [L_x+L_y,H_x+H_y]}$) and for ${\displaystyle x-y}$ (namely, ${\displaystyle [L_x-H_y,H_x-L_y]}$); note that these are exact abstractions, since the set of possible outcomes for, say, ${\displaystyle x+y}$, is precisely the interval ${\displaystyle [L_x+L_y,H_x+H_y]}$. More complex formulas can be derived for multiplication, division, etc., yielding so-called interval arithmetics.

Let us now consider the following very simple program:

y = x; z = x - y;

With reasonable arithmetic types, the result for z should be zero. But if we do interval arithmetic starting from x in [0, 1], one gets z in [−1, +1]. While each of the operations taken individually was exactly abstracted, their composition isn't.

The problem is evident: we did not keep track of the equality relationship between x and y; actually, this domain of intervals does not take into account any relationships between variables, and is thus a non-relational domain. Non-relational domains tend to be fast and simple to implement, but imprecise.

Some examples of relational numerical abstract domains are:

• congruence relations on integers
• convex polyhedra (cf. left picture) – with some high computational costs
• difference-bound matrices
• "octagons"
• linear equalities

and combinations thereof (such as the reduced product, cf. right picture).

When one chooses an abstract domain, one typically has to strike a balance between keeping fine-grained relationships, and high computational costs.

Machine word abstract domains

While high-level languages such as Python or Haskell use unbounded integers by default, lower-level programming languages such as C or assembly language typically operate on finitely-sized machine words, which are more suitably modeled using the integers modulo $2^n$ (where n is the bit width of a machine word). There are several abstract domains suitable for various analyses of such variables.

The bitfield domain treats each bit in a machine word separately, i.e., a word of width n is treated as an array of n abstract values. The abstract values are taken from the set $\{0,1,\mathrm{\perp }\}$, and the abstraction and concretization functions are given by: ${\displaystyle \gamma (0)=\{0\}}$, ${\displaystyle \gamma (1)=\{1\}}$, ${\displaystyle \gamma (\mathrm{\perp })=\{0,1\}}$, ${\displaystyle \alpha (\{0\})=0}$, ${\displaystyle \alpha (\{1\})=1}$, ${\displaystyle \alpha (\{0,1\})=\mathrm{\perp }}$, ${\displaystyle \alpha (\{\})=\mathrm{\perp }}$. Bitwise operations on these abstract values are identical with the corresponding logical operations in some three-valued logics:

Further domains include the signed interval domain and the unsigned interval domain. All three of these domains support forwards and backwards abstract operators for common operations such as addition, shifts, xor, and multiplication. These domains can be combined using the reduced product.