This is my note for presentation in CS590 Computer-Aided Program Reasoning seminar on 09/27/2016. We are reading ξ12 of book The Calculus of Computation: Decision Procedures with Applications to Verification to elaborate the intuition and formalization of abstract interpretation, and how that can be used for invariant generation. This seems a relatively easy reading, the chapter is well written.

Please do not hesitate to correct me if I am wrong anywhere. 😁


Since this is a book chapter, the materials are already well-written, it is easy to find the overall clue throughout underlying texts.

  • What’s the ultimate goal?
    • Generate invariants, i.e. assertions that summarize the conditions that must hold at this program point on all paths.
  • A naive approach.
    • Predicate transformers on concrete states.
    • But may not terminate.
  • An improved approach.
    • Abstract Interpretation, intuitionally.
    • Illustrated using interval analysis and Karr’s analysis examples.
  • A formalized approach.
    • Abstract Interpretation, defined with lattice.

Naive approach

Intuitively, the “invariant” can be generated by ∨ assertions in all paths. This is why they call it inductive assertions of programs in the chapter.

Therefore, the question now becomes “how to generate assertion at this program point in different paths”. The answer is straightforward, just propagate by predicate transformers.

We have introduced in detail the weakest precondition (wp) in previous lectures. The strongest postcondition (sp) was paid less attention to at that moment, but is now heavily used in this chapter.

Strongest Postcondition

As the name suggests, predicate transformer strongest postcondition is generating the strongest result after some command, in the sense that ∀ Q . {P} c {Q}, we have sp(P, c) ⇒ Q.

From my understanding, Symbolic Execution is basically doing strongest postcondition propagation under the hood.

There are some interesting rules for sp, it’s interesting to compare them with its wp duals:

  • for assume:

    • sp(F, assume p) ⇔ p ∧ F
    • wp(F, assume p) ⇔ p ⇒ F

  • for assignment:

    • sp(F[v], v := e[v]) ⇔ ∃ v0 . v = e[v0] ∧ F[v0]
    • wp(F[v], v := e) ⇔ F[e]

For sp, it’s basically differentiating two versions of variable v, with v0 being the old value. The notation here that changes F[v] to F[v0] means replacing the parts of v in the formula with v0 and keep everything else unchanged.

Due to this extra ∃ quantifier in sp, wp is generally preferred when possible.

Forward Propagation Algorithm

As mentioned, the goal in chapter is to do invariant generation.

They call some program points that should assign assertions cutpoints, from one cutpoint to another cutpoint constructs a basic path (which is a segment in my dictionary).

My understanding for the defined cutpoint is just the program points that shall be assigned assertions to. One could have different set of cutpoints for different purposes. The assertion map just assigns assertions to each of these program points / cutpoints. The goal – invariant generation – is to find such assertion map. Note that it is not the assertion that holds throughout entire program, just at that program point.

To propagate assertions to each program point (cutpoint), the algorithm is:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
let ForwardPropagate F_pre L =
    S := {L0};
    μ(L0) := Fpre;
    μ(L) := ⊥ for L ∈ L \ {L0};
    while S ≠ ∅ do
        let Lj = choose S in
        S := S \ {Lj};
        foreach Lk ∈ succ(Lj) do
            let F = sp(μ(Lj), Sj;...;Sk) in
            if F ≠> μ(Lk)
            then
              μ(Lk) := μ(Lk) ∨ F;
              S := S ∪ {Lk};
        done;
    done;
    μ

The algorithm is straightforward, it just propagates using sp predicate transformer, and merge the assertions from different branches/paths if necessary. The whole algorithm terminates when all assertions become stable.

Problem of Naive approach

However, there is no guarantee that the algorithm will terminate, possibly due to undecidability of F ≠> μ(Lk), possibly because always including some exact states via ∨ may never reach to an end. Consider the following counter-example:

1
2
3
4
5
6
L0: { Initially: n ≥ 0 }

i := 0
L1: while (i < n) {
    i++;
}

So:

  • From L0 to L1, the assertion is {i = 0 ∧ n ≥ 0}.

  • But from L1 to L1 after one loop iteration, the new formula is added by {i = 1 ∧ n > 0}.

  • This could go on and on forever, because the terminating condition is never reached – Fk ⇒ F_{k-1}, it always fails the check that the newly generated condition i = k ∧ n ≥ k ⇒ (i = 0 ∧ n ≥ 0) ∨ (i = 1 ∧ n ≥ 1) ∨ ... ∨ (i = k-1 ∧ n ≥ k-1), the collected assertion. (Page 320)

    This is because that we are doing some semantic analysis, and the algorithm can only check the next syntactic possible stop, thus L1 itself should always be considered as a next step for L1.

Improved approach - Abstract Interpretation

It’s obvious that there is a much simpler invariant for the above example: 0 ≤ i ≤ n.

Now by the improved approach – abstract interpretation – it can over-approximate the concrete states, operate on abstract states, and guarantee termination via some widening heuristic if necessary.

Intuitively,

1
2
3
Abstract    →sp→     Abstract        ...... →sp→ Abstract
   ↑vD               ↗vD   ↖vD                     ↑vD
Concrete →sp→ Concrete →sp→ Concrete ...... →sp→ Concrete

Below are the necessary preparation steps for abstract interpretation, throughout which the basic idea is to do the same set of operations on abstract states.

  1. What the abstract domain is, apparently. It stipulates the form of formulas that could appear in abstract domains.

  2. The mapping relation from concrete states to abstract states, $v_D$. This is an over-approximation, meaning that $F ⇒ v_D(F)$.

  3. The sp transformer was on concrete states, now there should be some sp for abstract states.

    The new $\bar{sp}$ may need basic logic operators, hence we still need to define abstract conjunction and abstract disjunction. The basic rules are:

    1. The resulting formula should reside in abstract domain as well, obviously.

    2. The resulting formula should still be an over-approximation, i.e. $F_1 ○ F_2 ⇒ F_1 \bar{○} F_2$, where $\bar{○}$ is the corresponding operator in abstract domain.

  4. In particular, abstract disjunction ⊔ is emphasized, because it will be used in the same propagation algorithm operating on abstract states.

  5. Abstract implication also needs to be specified. Because it will be used in the abstract domain version algorithm to decide whether it has reached fixpoint. For concrete states, it may even be undecidable.. But by carefully selecting the abstract domain, the implication validity check can become decidable and fast.

  6. The last is yet another novelty – heuristics to ensure algorithm termination, namely, a widening procedure. Intuitively, this is delicately defined to stretch to the limit of over-approximation.

    Formally, let F1, F2, … be an infinite sequence of Fi ∈ D such that $Fi ⇒ F_{i+1}$. Then another sequence Gi can be defined as: G1 = F1, G{i+1} = Gi ▽D F{i+1}.

    1
    2
    3
    F1 → F2 → F3 → ... → Fi → ...
     =   ▽D   ▽D         ▽D
    G1 → G2 → G3 → ... → Gi → ...

    Then it shall have the property that after some i, Gi ⇔ Gi+1. Sequence Gi converges even if Fi doesn’t converge.

With all these preparation, the abstract version of forward propagation algorithm is:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
let AbstractForwardPropagate Fpre L =
    S := {L0};
    μ(L0) := νD(Fpre);
    μ(L) := ⊥ for L ∈ L \ {L0};
    while S ≠ ∅ do
        let Lj = choose S in
        S := S \ {Lj};
        foreach Lk ∈ succ(Lj ) do
            let F = spD(μ(Lj), Sj;...;Sk) in
            if F ≠> μ(Lk)
            then
                if Widen()
                then
                    μ(Lk) := μ(Lk) ▽D (μ(Lk) ⊔D F);
                else
                    μ(Lk) := μ(Lk) ⊔D F;
                S := S ∪ {Lk};
         done;
    done;
    μ

The main difference other than abstract version of operations is the WIDEN() function call. It determines whether widening should be applied (e.g. after specified max iterations, could be more complicated strategies).

This widening is to replace the original abstract disjunction of including more states.

Compare with G{i+1} = Gi ▽D Fi+1, here μ(Lk) := μ(Lk) ▽D (μ(Lk) ⊔D F); has μ(Lk) as G(i) and μ(Lk) ⊔D F as Fi+1.

Demonstration - Interval Analysis

Next, we use the example of Interval Analysis to demonstrate the just defined abstract interpretation approach.

Interval analysis, as the name suggests, extracts the bound of a variable.

Step 1: Define abstract domain

Abstract domain formula literals are of the shape: $v ≤ c$ and $c ≤ v$ for some constant number $c$.

Some simplification rules are also given:

  • ⊥ ∧ F ≡ ⊥
  • ⊤ ∧ F ≡ F
  • c1 ≤ v ∧ c2 ≤ v ≡ max(c1, c2) ≤ v
  • v ≤ c1 ∧ v ≤ c2 ≡ v ≤ min(c1, c2)
  • c1 > c2 ⇒ c1 ≤ v ∧ v ≤ c2 ≡ ⊥

All these should be intuitive.

Some computation rules are given:

  • [l1, u1] + [l2, u2] = [l1+l2, u1+u2]

  • c = [c, c]

  • introduce ∞ and -∞

  • [∞, -∞] is empty interval

  • [l1, u1] ⊓ [l2, u2] =

    • [∞, -∞] if max(l1, l2) > min(u1, u2)
    • [max(l1, l2), min(u1, u2)] otherwise

The following several rules are over-approximation:

  • [l1, u1] ⊔ [l2, u2] = [min(l1, l2), max(u1, u2)].

    • Note that this is a so called interval hull. It may include many unrelated segments in between.

  • [l1, u1] ≤ [l2, u2] if l1 ≤ u2.

    • i.e. as long as there exists any elements in two intervals that v1 ≤ v2.

  • [l1, u1] = [l2, u2] if [l1, u1] ⊓ [l2, u2] ≠ [∞, -∞].

    • i.e. as long as there exists any elements in two intervals that v1 = v2.

Step 2: Define mapping relation $v_{Di}$

Now given some concrete state formula, $v_{DI}$ over-approximates it into a abstract domain formula.

For clause literals it only filters out those clauses such as:

  • $av = b$
  • $av ≤ b$
  • $b ≤ av$

and extract condition of variable $v$ in the basic abstract state formula as just defined.

However, this very weak filtering will lose much valuable information such as those more complicated inequality formulas, e.g. $j + 2n ≤ 4$.

That’s why a non-trivial $v_{Di}(H, G’)$ is defined, which basically uses the context information in $G’$ to simplify $H$. This can re-pick up the lost information of $j + 2n ≤ 4$, otherwise it just trivially distributes vD to each conjunctive clauses.

More formally, this is written as

$v_{Di}(F, G ∧ v_{Di}(F))$

For example,

1
2
3
F: i = 0 ∧ n ≥ 0 ∧ j+2n ≤ 4
H: j+2n ≤ 4
G: j ≥ 5

With the extra context $G: j ≥ 5$,

1
2
3
4
5
6
7
= vDi (H, G ∧ vDi(F))
= vDi (j+2n≤4, 5≤j ∧ 0≤i ∧ i≤0 ∧ 0≤n)
= ⊥

because
j+2n = [5,∞] + 2[0,∞] = [5, ∞] !≤ [4,4]
So j+2n≤4 = ⊥

Without this context information, the interval won’t be [-∞, ∞].

Note that $F ⇒ v_{Di}(F)$, so if without $G$,

$v_{Di}(F, v_{Di}(F))$

should be the same as $v_{Di}(F)$. It’s the added context information $G$ that makes everything more accurate.

This schema due to weak $v_{Di}$ is also used in subsequent abstract domain transformers $\bar{sp}$.

Step 3: Define abstract domain transformer $\bar{sp}$

⊓ in abstract domain for interval analysis is just ∧.

assume

The similar idea of “using more information” in last step can also be used here.

$$\bar{sp}_{D_i}(F, assume \ p) ⇔ v_{D_i}(p, F) ∧ F$$

This $v_{Di}(p, F)$ is also intentionally making it more accurate here with the existing context information $F$.

Otherwise $v_{Di}(p)$ may directly discard those non-basic constraints.

assignment

Let [l, u] be the interval evaluation of $e$ under the context of $F$, and $G$ is all the rest literals of $F$ not involving $v$, then

$\bar{sp}_{D_i}(F, v := e) ⇔ l ≤ v ∧ v ≤ u ∧ G$

This is straightforward.

When $e$ is too complicated, e.g. not a linear expression, set the interval of $v$ to ⊤.

Step 4: Define interval disjunction $⊔_{D_i}$

In interval analysis abstract domain, for

$$F: x ∈ [l_1, u_1] \\ G: x ∈ [l_2, u_2] \\ F ⊔_{Di} G = [l_1, u_1] ⊔ [l_2, u_2]$$

i.e. the interval hull. Over-approximation, again.

Step 5: Define interval implication

In interval analysis abstract domain, for $F: x_i ∈ [l_i, u_i]$, $G: x_i ∈ [m_i, v_i]$, then $F ⇒ G$ iff $∀ x_i, [l_i, u_i] ⊆ [m_i, v_i]$. i.e. subset.

Step 6: Define widening

With all the steps above, it has simplified a lot, but still cannot guarantee termination.

See the example below:

1
2
3
4
5
6
@L0: i = 0 ∧ n ≥ 0
while
	@L1: ?
	(i < n) {
	i := i + 1
}

In this tiny program there are two so called “basic paths” (I’d prefer call them segments).

1
2
3
4
5
6
7
8
9
(1) before while loop
	@L0: i = 0 ∧ n ≥ 0
	@L1: ?

(2) while loop iteration
	@L1: ?
	assume i < n;
	i := i + 1
	@L1: ?

And our goal is to generate the invariant @L1.

According to the algorithm, it will keep “run” the iteration and add newly generated assertion to invariant, all on abstract domain.

At the end of kth iteration, the newly generated formula $0 ≤ i ∧ i ≤ k ∧ 0 ≤ n$ never ⇒ the existing invariant formula $0 ≤ i ∧ i ≤ k-1 ∧ 0 ≤ n$.

To solve this, it needs to over-approximate even more, using the widening operator $▽_{D_i}$.

For each variable v, suppose that $F$ asserts $v ∈ [l_1, u_1]$ and $G$ asserts $v ∈ [l_2, u_2]$.

Then $F ▽_{Di} G$ asserts that $v ∈ [l, u]$, where

  • l = −∞ if $l_2 < l_1$, and otherwise $l = l_1$;
  • u = ∞ if $u_2 > u_1$, and otherwise $u = u_1$.

According to usage, $F$ is the accumulated invariant, so the idea is that if the new invariant $G$ is still beyond the bound of $F$, $F$ chooses ∞/-∞ as the new bound. Apparently, in this way $F$ will definitely reach some fixpoint, thus guarantee termination.

Demonstration - Karr’s Analysis

Omitted due to time of preparation..

Formalized approach - Abstract Interpretation with Lattices

All above is using some notation that is easy to understand, while in literatures, Abstract Interpretation is defined using more mathematical notations – operations on lattices.

We should have seen lattices in Discrete Mathematics.

A lattice $(S, ⊔, ⊓)$ is a set equipped with join ⊔ and meet ⊓ operators that are commutative / associative, idempotent.

Knaster-Tarski Theorem.

The fixpoints of a monotone function on a complete lattice comprise a complete lattice.

It guarantees the existence of the least fixpoint and the greatest fixpoint of monotone function f.

My comprehension is that, if it terminates (has fixpoint) in abstract domain, it is also valid for the concrete domain. But by adding concrete state one by one it may never reach this fixpoint.

For abstract interpretation, consider the possible program states to be a lattice, then

  • join is ∪
  • meet is ∩
  • partial order is ⊆
  • the greatest element is all-states
  • the least element is empty-state

This is represented by $C_p = (2^S, ∪, ∩)$. This is the concrete domain.

On this lattice, define $F_p(S’)$ as $S’ ∪ P(S’)$. Here $P(S’)$ means the next reachable states from set S’.

Compare $F_p$ to the predicate transformer together with the inclusion phase in our algorithm.

Then ForwardPropagate algorithm is like starting from those states satisfying the initial assertion, and aim to include all the reachable states into the set.

But again, as we have shown, this may not terminate.

So define abstract domain $A_p = (A, ⊔, ⊓)$ corresponding to the concrete domain $C_p$.

Two functions for mapping to/from abstract/concrete domains are needed: (recall $v_{D_i}$)

  • $α: 2^S → A$, from concrete domain to abstract domain. abstraction function
  • $γ: A → 2^S$, from abstract domain to concrete domain. concretization function

Apparently, these functions should preserve partial order!

$F_p$ is operating on concrete domain $C_p$, so there should be a dual $\bar{F_p}$ on abstract domain $A_p$. It is valid if

$∀ a ∈ A . F_p(γ(a)) ⊆ γ(\bar{F_p}(a))$

Intuitively,

1
2
3
a    → Fp-bar(a)
↓γ()             ↘
γ(a) → Fp(γ(a)) ⊆ γ(Fp-bar(a))

which basically means $\bar{Fp}$ is a corresponding over-approximation of Fp in the abstract domain.

So, as you can see, all are operating on these two abstract/concrete domains.

□


PS: To display LaTeX symbols on this blog, I integrated MathJax engine, but it seems my blog engine Hexo will treat _ as italic at a higher priority than subscript.. which lead to a lot of problems in re-formatting.. 😒