LARA

Abstract Interpretation

Goal: Invariant Inference by Approximation

Approximate strongest postcondition $sp$ with operator $sp\#$ whose fixedpoint e.g. has a finite height.

Let PS denote program states and $C = 2^{PS}$ denote the set of all subsets of PS, so $S \subseteq PS$ and $S \in C$ for a set of states S. We introduce an abstract analysis domain A and functions

\begin{equation*} \begin{array}{l} \gamma : A \to C \ \ \mbox{concretization function} \\ \end{array} \end{equation*}

Instead of working with C, we work with simpler domain A, which is the data structure for analysis.

Examples of A:

  • mapping from variables to information about the values they can have (interval analysis, sign analysis, constant propagation)
  • formula F (usually in canonical form) such that $\gamma(F) = \{ x. F \}$

So, we will impose that our domain is partial order. It is useful to require additional property, namely that we have lattice, which have “union”-like and “intersection”-like operations.

Note that $\gamma$ allows us to define set-like operations on A that correspond to operations on A:

\begin{equation*} a_1 \sqsubseteq a_2 \iff \gamma(a_1) \subseteq \gamma(a_2) \end{equation*}

Instead of $sp : C \to C$, we have its approximation $sp\# : A \to A$. To be sound we need to have

\begin{equation*} \gamma(sp\#(a_1,r)) \supseteq sp(\gamma(a_1),r) \end{equation*}

This is the most important condition for abstract interpretation.

One way to find $sp\#$ it is to have $\alpha$ that goes the other way

\begin{equation*} \begin{array}{l} \alpha : C \to A \ \ \mbox{abstraction function} \end{array} \end{equation*}

such that

\begin{equation*} \begin{array}{l} \gamma(\alpha(S)) \supseteq S \\ \alpha(\gamma(a)) = a \end{array} \end{equation*}

Then we can write a definition of $sp\# : A \to A$ in terms of it:

\begin{equation*} sp\#(a,r) = \alpha(sp(\gamma(a),r)) \end{equation*}

and we call this “the best transformer”.

Abstract computation of program semantics

In our lattice we have

\begin{eqnarray*} \gamma(a_1 \sqcup a_2) &\supseteq& \gamma(a_1) \cup \gamma(a_2) \end{eqnarray*}

because of the way we defined order.

Consider first only a single loop.

Then we rewrite our computation of sp for the loop by replacing $sp$ with $sp\#$ and replacing $\cup$ with $\sqcup$. We obtain fixpoint equation for computing the effect of a transitive closur eof a relation (i.e. a loop):

\begin{equation*} sp\#(a,r^*) = a \sqcup sp\#(sp\#(a,r),r^*) \end{equation*}

We can then iterate this equation until it stabilizes.

From the properties of $\gamma$ it follows that the result is approximation of the set of reachable states.

When does it stabilize? Note that the sequence is increasing and if we ever repeat we have stabilized. If there are no infinite ascending chains, the computation terminates.

References