Combining Forward and Backward Abstract Interpretation of Horn Clauses

Abstract

Alternation of forward and backward analyses is a standard technique in abstract interpretation of programs, which is in particular useful when we wish to prove unreachability of some undesired program states. The current state-of-the-art technique for combining forward (bottom-up, in logic programming terms) and backward (top-down) abstract interpretation of Horn clauses is query-answer transformation. It transforms a system of Horn clauses, such that standard forward analysis can propagate constraints both forward, and backward from a goal. Query-answer transformation is effective, but has issues that we wish to address. For that, we introduce a new backward collecting semantics, which is suitable for alternating forward and backward abstract interpretation of Horn clauses. We show how the alternation can be used to prove unreachability of the goal and how every subsequent run of an analysis yields a refined model of the system. Experimentally, we observe that combining forward and backward analyses is important for analysing systems that encode questions about reachability in C programs. In particular, the combination that follows our new semantics improves the precision of our own abstract interpreter, including when compared to a forward analysis of a query-answer-transformed system.

This work was partially supported by the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013)/ERC Grant Agreement nr. 306595 “STATOR”.

A Proofs

Proposition 2

For every $k \ge 1$, the set $\gamma _{}(d_k) \cup \bigcup _{i=1}^{k-1} \big (\gamma _{}(d_i) \setminus \gamma _{}(b_i)\big )$ is a model of $\mathbb {H}$.

Proof

For convenience, let us replace the direct consequence relation $\mathbb {T}_{\mathbb {H}}$ with two objects: the set of initial atoms $\mathbb {I}_{\mathbb {H}}= \{ a' \mid (\varnothing , a') \in \mathbb {T}_{\mathbb {H}}\}$ and the set of consecutions $\mathbb {T}_{\mathbb {H}}^{\rightarrow }= \{ (A, a') \in \mathbb {T}_{\mathbb {H}}\mid A \ne \varnothing \}$. Then, for every $R,X \subseteq \mathbb {A}$, ${\text {post}}^{}(\mathbb {T}_{\mathbb {H}},X) = \mathbb {I}_{\mathbb {H}}\cup {\text {post}}^{}(\mathbb {T}_{\mathbb {H}}^{\rightarrow },X)$ and ${\text {pre}}^{}\!|_{R}(\mathbb {T}_{\mathbb {H}},X) = {\text {pre}}^{}\!|_{R}(\mathbb {T}_{\mathbb {H}}^{\rightarrow },X)$.

Now let us consider the first three elements of the descending sequence, $d_1$, $b_1$, and $d_2$. For $d_1$ it holds that $\mathbb {I}_{\mathbb {H}}\cup {\text {post}}^{}(\mathbb {T}_{\mathbb {H}}^{\rightarrow },\gamma _{}(d_1)) \subseteq \gamma _{}(d_1)$. That is, $\gamma _{}(d_1)$ is a model of $\mathbb {H}$ and the lemma statement holds for $k=1$.

For $b_1$, it holds that $(\gamma _{}(g) \cap \gamma _{}(d_1)) \cup {\text {pre}}^{}\!|_{\gamma _{}(d_1)}(\mathbb {T}_{\mathbb {H}}^{\rightarrow },\gamma _{}(b_1)) \subseteq \gamma _{}(b_1)$. This means that for every conseqution $(A, a') \in \mathbb {T}_{\mathbb {H}}^{\rightarrow }$, if $A \subseteq \gamma _{}(d_1)$ and $A \cap (\gamma _{}(d_1) \setminus \gamma _{}(b_1)) \ne \varnothing$, then $a' \in (\gamma _{}(d_1) \setminus \gamma _{}(b_1))$.

Finally, for $d_2$ it holds that $(\mathbb {I}_{\mathbb {H}}\cup {\text {post}}^{}(\mathbb {T}_{\mathbb {H}}^{\rightarrow },\gamma _{}(d_2))) \cap \gamma _{}(b_1) \subseteq d_2$. First, this means that $\mathbb {I}_{\mathbb {H}}\subseteq (\gamma _{}(d_1) \setminus \gamma _{}(b_1)) \cup \gamma _{}(d_2)$. Indeed, by definition of $d_1$, $\mathbb {I}_{\mathbb {H}}\subseteq \gamma _{}(d_1)$ and by definition of $d_2$, $\mathbb {I}_{\mathbb {H}}\cap \gamma _{}(b_1) \subseteq \gamma _{}(d_2)$. Second, this means that ${\text {post}}^{}(\mathbb {T}_{\mathbb {H}}^{\rightarrow },(\gamma _{}(d_1) \setminus \gamma _{}(b_1)) \cup \gamma _{}(d_2)) \subseteq (\gamma _{}(d_1) \setminus \gamma _{}(b_1)) \cup \gamma _{}(d_2)$. Indeed, let is pick an arbitrary $(A, a') \in \mathbb {T}_{\mathbb {H}}^{\rightarrow }$, s.t. $A \subseteq (\gamma _{}(d_1) \setminus \gamma _{}(b_1)) \cup \gamma _{}(d_2)$. There are two possible cases. If $A \subseteq \gamma _{}(d_2)$ then by definition of $d_2$, either $a' \in \gamma _{}(d_2)$, or $a' \in (\gamma _{}(d_1) \setminus \gamma _{}(b_1))$. If $A \not \subseteq \gamma _{}(d_2)$ then $A \cap (\gamma _{}(d_1) \setminus \gamma _{}(b_1)) \ne \varnothing$, and $a' \in \gamma _{}(d_1) \setminus \gamma _{}(b_1)$. This proves the statement of the lemma for $k = 2$ and also provides the base case for the following inductive proof.

Now let $k > 2$, $L_k = \bigcup _{i=1}^{k-1} \big (\gamma _{}(d_i) \setminus \gamma _{}(b_i)\big )$, and $M_k = \gamma _{}(d_k) \cup L_k$. Let the induction hypothesis be that: $\mathbb {I}_{\mathbb {H}}\subseteq M_k$, ${\text {post}}^{}(\mathbb {T}_{\mathbb {H}}^{\rightarrow },M_k) \subseteq M_k$ (i.e., $M_k$ is a model of $\mathbb {H}$), and for every $(A, a') \in \mathbb {T}_{\mathbb {H}}^{\rightarrow }$, if $A \subseteq M_k$ and $A \cap L_k \ne \varnothing$, then $a' \in L_k$.

Then, let us consider the two subsequent elements: $b_k$ and $d_{k+1}$ and the two sets: $L_{k+1} = M_k \setminus \gamma _{}(b_k)$ and $M_{k+1} = L_{k+1} \cup \gamma _{}(d_{k+1})$.

For $b_k$ it holds that $(\gamma _{}(g) \cap \gamma _{}(d_k)) \cup {\text {pre}}^{}\!|_{\gamma _{}(d_k)}(\mathbb {T}_{\mathbb {H}}^{\rightarrow },\gamma _{}(b_k)) \subseteq \gamma _{}(b_k)$. That is, for every $(A, a') \in \mathbb {T}_{\mathbb {H}}^{\rightarrow }$, if $A \subseteq \gamma _{}(d_k)$ and $A \cap (\gamma _{}(d_k) \setminus \gamma _{}(b_k)) \ne \varnothing$, then $a' \in (\gamma _{}(d_k) \setminus \gamma _{}(b_k))$.

For $d_{k+1}$ it holds that $(\mathbb {I}_{\mathbb {H}}\cup {\text {post}}^{}(\mathbb {T}_{\mathbb {H}}^{\rightarrow },\gamma _{}(d_{k+1}))) \cap \gamma _{}(b_k) \subseteq \gamma _{}(d_{k+1})$.

First, observe that $\mathbb {I}_{\mathbb {H}}\subseteq M_{k+1}$. Indeed, we know that $\mathbb {I}_{\mathbb {H}}\subseteq M_k$ and that $M_{k+1} = (M_k \setminus \gamma _{}(b_k)) \cup \gamma _{}(d_{k+1})$. By definition of $d_{k+1}$, $\mathbb {I}_{\mathbb {H}}\cap \gamma _{}(b_k) \subseteq \gamma _{}(d_{k+1})$. Thus, $\mathbb {I}_{\mathbb {H}}\subseteq M_{k+1}$.

Second, let us pick an arbitrary $(A, a') \in \mathbb {T}_{\mathbb {H}}^{\rightarrow }$, s.t. $A \subseteq M_{k+1}$. Since $M_k$ is a model of H, we know that $a' \in M_k$. But then, there are three possible cases. (i) If $A \subseteq \gamma _{}(d_{k+1})$, then either $a' \in \gamma _{}(d_{k+1})$, or $a' \notin \gamma _{}(b_k)$. That is, $a' \in (M_k \setminus \gamma _{}(b_k)) \cup \gamma _{}(d_{k+1}) = M_{k+1}$. (ii) If $A \subseteq \gamma _{}(d_k)$ and $A \not \subseteq \gamma _{}(d_{k+1})$, then $A \cap (\gamma _{}(d_k) \setminus \gamma _{}(b_k)) \ne \varnothing$, and $a' \in \gamma _{}(d_k) \setminus \gamma _{}(b_k) \subseteq M_{k+1}$. (iii) Finally, if $A \not \subseteq \gamma _{}(d_k)$, then $A \cap L_k \ne \varnothing$, and from the hypothesis $a' \in L_k$. There are no other possible cases. This means that ${\text {post}}^{}(\mathbb {T}_{\mathbb {H}}^{\rightarrow },M_{k+1}) \subseteq M_{k+1}$ and thus $M_{k+1}$ is a model of $\mathbb {H}$. Also, from (ii) and (iii) it follows that for $(A, a') \in \mathbb {T}_{\mathbb {H}}^{\rightarrow }$, if $A \subseteq M_{k+1}$ and $A \cap L_{k+1} \ne \varnothing$, then $a' \in L_{k+1}$.