Ilinva: Using Abduction to Generate Loop Invariants

TL;DR

Ilinva introduces an automated, generic, and lazy method for synthesizing loop invariants using abductive reasoning, enhancing program verification across diverse languages and domains.

Contribution

It presents a novel approach combining abductive reasoning with invariant synthesis, integrated into the GPiD system and Why3 platform, for improved program property proofs.

Findings

Effective invariant synthesis demonstrated on various programs

Applicable to multiple programming languages and domains

Practical relevance confirmed through experiments

Abstract

We describe a system to prove properties of programs. The key feature of this approach is a method to automatically synthesize inductive invariants of the loops contained in the program. The method is generic, i.e., it applies to a large set of programming languages and application domains; and lazy, in the sense that it only generates invariants that allow one to derive the required properties. It relies on an existing system called GPiD for abductive reasoning modulo theories, and on the platform for program verification Why3. Experiments show evidence of the practical relevance of our approach.

Equations

$$\mathtt{P}$$

$$\mathtt{I}$$

$$wp(\varphi ,\text{empty})$$

$$sp(\varphi ,\text{empty})$$

$$path(\mathtt{P},\ell ,\ell )$$

Full text

1 Introduction

Hoare logic – together with strongest post-conditions or weakest pre-conditions calculi – allow one to verify properties of programs defined by bounded sequences of instructions [20]. Given a pre-condition $\phi$ satisfied by the inputs of program ${\tt P}$, algorithms exist to compute the strongest formula $\psi$ such that $\phi\ \{{\tt P}\}\ \psi$ holds, meaning that if $\phi$ holds initially then $\psi$ is satisfied after ${\tt P}$ is executed, and any formula $\psi^{\prime}$ that holds after ${\tt P}$ is executed is such that $\psi\models\psi^{\prime}$. To check that the final state satisfies some formula $\psi^{\prime}$, we thus only have to check that $\psi^{\prime}$ is a logical consequence of $\psi$. However, in order to handle programs containing loops, it is necessary to associate each loop occurring within the program with an inductive invariant. An inductive invariant for a given loop ${\tt L}$ is a formula that holds every time the program enters ${\tt L}$ (i.e., it must be a logical consequence of the preconditions of ${\tt L}$), and is preserved by the sequence of instructions in ${\tt L}$. Testing whether a formula is an inductive invariant is a straightforward task, and the difficulty resides in generating candidate invariants. These can be supplied by the programmer, but this is a rather tedious and time-consuming task; for usability and scalability, it is preferable to generate those formulas automatically when possible. In this paper, we describe a system to generate such invariants in a completely automated way, via abductive reasoning modulo theories, based on the methodology developed in [13]. Roughly speaking, the algorithm works as follows. Given a program ${\tt P}$ decorated with a set of assertions that are to be established, all loops are first assigned the same candidate invariant $\top$. These invariants are obviously sound: they hold before the loops and are preserved by the sequence of instructions in the loop; however they are usually not strong enough to prove the assertions decorating the program. They are therefore strengthened by adding hypotheses that are sufficient to ensure that the assertions hold; these hypotheses are generated by a tool that performs abductive inferences, and the strengthened formulas are candidate invariants. Additional strengthening steps are taken to guarantee that these candidates are actual invariants, i.e., that they are preserved by the sequence of instructions in the loop. These steps are iterated until a set of candidate invariants that are indeed inductive is obtained.

We rely on two existing systems to accomplish this task. The first one is Why3 (see, e.g., http://why3.lri.fr/ or [16]), a well-known and widely-used platform for deductive program verification that is used to compute verification conditions and verify assertions. The second system, GPiD, is designed to generate implicants111An implicant of a formula $\psi$ is a formula $\phi$ such that $\phi\models\psi$. It is the dual notion of that of implicates of quantifier-free formulas modulo theories [14]. This system is used as an abductive reasoning procedure, thanks to the following property: if $\phi\not\models\psi$, finding a hypothesis $\phi^{\prime}$ such that $\phi\wedge\phi^{\prime}\models\psi$ is equivalent to finding $\phi^{\prime}$ such that $\phi^{\prime}\models\phi\Rightarrow\psi$. GPiD is generic, since it only relies on the existence of a decision procedure for the considered theory (counter-examples are exploited when available to speed-up the generation of the implicants when available). Both systems are connected in the Ilinva framework.

Related Work.

A large number of different techniques have been proposed to generate loop invariants automatically, especially on numeric domains [9, 10], but also in more expressive logics, for programs containing arrays or expressible using combination of theories [26, 8, 23, 18, 22, 24]. We only briefly review the main ideas of the most popular and successful approaches. Methods based on abstract interpretations (see, e.g., [11, 25]) work by executing the program in a symbolic way, on some abstract domain, and try to compute over-estimations of the possible states of the memory after an unbounded number of iterations of the loop. Counter-examples generated from runs can be exploited to refine the considered abstraction [17, 19]. The idea is that upon detection of a run for which the assertion is violated, if the run does not correspond to a concrete execution path, then the considered abstraction may be refined to dismiss it.

Candidate invariants can also be inferred by generating formulas of some user-provided patterns and testing them against some particular executions of the program [15]. Those formulas that are violated in any of the runs can be rejected, and the soundness of the remaining candidates can be checked afterwards. Invariants can be computed by using iterative backward algorithms [27], starting from the post-condition and computing weakest pre-conditions until a fixpoint is reached (if any). Other approaches [21] have explored the use of quantifier elimination to refine properties obtained using a representation of all execution paths.

The work that is closest to our approach is [13], which presents an algorithm to compute invariants as boolean combinations of linear constraints over integers. The algorithm is similar to ours, and also uses abduction to strengthen candidate invariant so that verification conditions are satisfied. The algorithms differ by the way the verification conditions and abductive hypotheses are proceeded: in our approach the conditions always propagate forward from an invariant to another along execution paths, and we eagerly ensure that all the loop invariants are inductive. Another difference is that we use a completely different technique to perform abductive reasoning: in [13] is based on model construction and quantifier elimination for Presburger arithmetic, whereas our approach uses a generic algorithm, assuming only the existence of a decision procedure for the underlying theory. This permits to generate invariants expressed in theories that are out of the scope of [13].

Contribution.

The main contribution is the implementation of a general framework for the generation of loop invariants, connecting the platform Why3 and GPiD. The evaluation demonstrates that the system permits to generate loop invariants for a wide range of theories, though it suffers from a large search space which may induce a large computation time.

2 Verification Conditions

In what follows, we consider formulas in a base logic expressing properties of the memory and assume that such formulas are closed under the usual boolean connectives. These formulas are interpreted modulo some theory ${\cal T}$, where $\models_{{\cal T}}$ denotes logical entailment w.r.t. ${\cal T}$. The memory is modified by programs, which are sequences of instructions; they are inductively defined as follows:

[TABLE]

where ${\tt P}^{\prime}$, ${\tt P}_{1}$ and ${\tt P}_{2}$ are programs, ${\tt C}$ is a condition on the state of the memory, $\phi$ is a formula and ${\tt I}$ is an instruction. Assumptions correspond to formulas that are taken as hypotheses, they are mostly useful to specify pre-conditions. Assertions correspond to formulas that are to be proved. Base instructions are left unspecified, they depend on the target language and application domain; they may include, for instance, assignments and pointer redirection. The formula $\phi$ in the while loop is a candidate loop invariant, it is meant to hold every time condition ${\tt C}$ is tested. In our setting each candidate loop invariant will be set to $\top$ before invoking Ilinva (except when another formula is provided by, e.g., the user), and the program will iteratively update these formulas. We assume that conditions contain no instructions, i.e., that the evaluation of these conditions does not affect the memory. We write ${\tt P}\sim{\tt P}^{\prime}$ if programs ${\tt P}$ and ${\tt P}^{\prime}$ are identical up to the loop candidate invariants.

An example of a program is provided in Figure 1. It uses assignments on integers and usual constructors and functions on lists as base instructions. It contains one loop with candidate invariant $\top$ (Line 1) and one assertion (Line 1).

It contains one loop for which we will generate an invariant.

A location is a finite sequence of natural numbers. The empty location is denoted by $\varepsilon$ and the concatenation of two locations $\ell$ and $\ell^{\prime}$ is denoted by $\ell.\ell^{\prime}$. If $\ell$ is a location and $S$ is a set of locations then $\ell.S$ denotes the set $\{\ell.\ell^{\prime}\mid\ell^{\prime}\in S\}$. The set of locations in a program ${\tt P}$ or in an instruction ${\tt I}$ is inductively defined as follows:

• •

If ${\tt P}$ is an empty sequence then $\mathrm{loc}({\tt P})=\{0\}$.

• •

If ${\tt P}={\tt I}\ ;\ {\tt P}^{\prime}$ then $\mathrm{loc}({\tt P})=\{0\}\cup 0.\mathrm{loc}({\tt I})\cup\{(i+1).p\mid i\in{\mathbb{N}},i.p\in\mathrm{loc}({\tt P}^{\prime})\}$.

• •

If ${\tt I}$ is a base instruction or an assumption/assertion, then $\mathrm{loc}({\tt I})=\emptyset$.

• •

If ${\tt I}=\texttt{if }{\tt C}\texttt{ then }{\tt P}_{1}\texttt{ else }{\tt P}_{2}$ then $\mathrm{loc}({\tt I})=1.\mathrm{loc}({\tt P}_{1})\cup 2.\mathrm{loc}({\tt P}_{2})$.

• •

If ${\tt I}=\texttt{while }{\tt C}\texttt{ do }{\tt P}_{1}\{\phi\}\texttt{ end}$ then $\mathrm{loc}({\tt I})=1.\mathrm{loc}({\tt P}_{1})$.

For instance, a program ${\tt I}_{1}\ ;\ {\tt I}_{2}$ where ${\tt I}_{1},{\tt I}_{2}$ denote base instructions has three locations: [math] (beginning of the program), $1$ (between ${\tt I}_{1}$ and ${\tt I}_{2}$) and $2$ (end of the program). Note that there are no locations within an atomic instruction. The program in Figure 1 has eight locations, namely [math], $1$, $2$, $2.1.0$, $2.1.1$, $2.1.2$, $3$, $4$. We denote by ${\tt P}|_{\ell}$ the instruction occurring just after location $\ell$ in ${\tt P}$ (if any):

• •

If ${\tt P}={\tt I}\ ;\ {\tt P}^{\prime}$ then ${\tt P}|_{0}={\tt I}$, ${\tt P}|_{0.\ell}={\tt I}|_{\ell}$ and ${\tt P}|_{(i+1).\ell}={\tt P}^{\prime}|_{i.\ell}$.

• •

If ${\tt I}=\texttt{if }{\tt C}\texttt{ then }{\tt P}_{1}\texttt{ else }{\tt P}_{2}$ then ${\tt I}|_{1.\ell}={\tt P}_{1}|_{\ell}$ and ${\tt I}|_{2.\ell}={\tt P}_{2}|_{\ell}$.

• •

If ${\tt I}=\texttt{while }{\tt C}\texttt{ do }{\tt P}_{1}\{\phi\}\texttt{ end}$ then ${\tt I}|_{1.\ell}={\tt P}_{1}|_{\ell}$.

Note that $\ell\mapsto{\tt P}|_{\ell}$ is a partial function, since locations denoting the end of a sequence do not correspond to an instruction. We denote by $\mathrm{lloc}({\tt P})$ the set of locations $\ell$ in ${\tt P}$ such that ${\tt P}|_{\ell}$ is a loop and by $\mathrm{loops}({\tt P})=\{{\tt P}|_{\ell}\mid\ell\in\mathrm{lloc}({\tt P})\}$ the set of loops occurring in ${\tt P}$. For instance, if ${\tt P}$ denotes the program in Figure 1, then ${\tt P}|_{1}$ is $\mathbf{let\ }\texttt{L}\leftarrow\mathbf{list}(1,\mathbf{nil})$, and $\mathrm{lloc}({\tt P})=\{2\}$.

We denote by $<$ the usual order on locations: $\ell<\ell^{\prime}$ iff either there exist numbers $i,j$ and locations $\ell_{1},\ell_{2},\ell_{3}$ such that $\ell=\ell_{1}.i.\ell_{2}$, $\ell=\ell_{1}.j.\ell_{3}$ and $i<j$, or there exists a location $\ell^{\prime\prime}$ such that $\ell^{\prime}=\ell.\ell^{\prime\prime}$.

We assume the existence of a procedure $\mathrm{VCgen}$ that, given a program ${\tt P}$, generates a set of verification conditions for ${\tt P}$. These verification conditions are formulas of the form $\phi\Rightarrow\psi$, each of which is meant to be valid. Given a program ${\tt P}$, the set of conditions $\mathrm{VCgen}({\tt P})$ can be decomposed as follows:

Assertion conditions, which ensure that the assertion formulas hold at the corresponding location in the program. These conditions also include additional properties to prevent memory access errors, e.g., to verify that the index of an array is within the defined valid range of indexes. The set of assertion conditions for program ${\tt P}$ is denoted by $\mathrm{VCgen}_{\mathrm{a}}({\tt P})$. 2. 2.

Propagation conditions, ensuring that loop invariants do propagate. Given a loop ${\tt L}$ occurring at position $\ell$ in program ${\tt P}$, we denote by $\mathrm{VCgen}_{\mathrm{ind}}({\tt P},\ell)$ the set of assertions ensuring that the loop invariant for ${\tt L}$ propagates. 3. 3.

Loop pre-conditions, ensuring that the loop invariants hold when the corresponding loop is entered. Given a loop ${\tt L}$ occurring at position $\ell$ in program ${\tt P}$, we denote by $\mathrm{VCgen}_{\mathrm{init}}({\tt P},\ell)$ the set of assertions ensuring that the loop invariant holds before loop ${\tt L}$ is entered.

Thus, $\mathrm{VCgen}({\tt P})=\mathrm{VCgen}_{\mathrm{a}}({\tt P})\cup\left(\bigcup_{\ell\in\mathrm{lloc}({\tt P})}(\mathrm{VCgen}_{\mathrm{ind}}({\tt P},\ell)\cup\mathrm{VCgen}_{\mathrm{init}}({\tt P},\ell))\right).$ Such verification conditions are generally defined using standard weakest pre-condition or strongest post-condition calculi (see, e.g., [12]), where loop invariant are used as under-approximations. Formal definitions are recalled in Figures 2 and 3 (the definition for the basic instructions depends on the application language and is thus omitted). For the sake of readability, we assume, by a slight abuse of notation, that the condition ${\tt C}$ is also a formula in the base logic.

This permits to define the goal of the paper in a more formal way: our aim is to define an algorithm that, given a program ${\tt P}$, constructs a program ${\tt P}^{\prime}\sim{\tt P}$ (i.e., constructs loop invariants for each loop in ${\tt P}$) such that $\mathrm{VCgen}({\tt P}^{\prime})$ only contains valid formulas. Note that all the loops and invariants must be handled globally since verification conditions depend on one another.

3 Abduction

As mentioned above, abductive reasoning will be performed by generating implicants. Because it would not be efficient to blindly generate all implicants of a formula, this generation is controlled by fixing the literals that can occur in an implicant. We thus consider a set ${\cal A}$ of literals in the considered logic, called the abducible literals.

Definition 1

Let $\phi$ be a formula. An ${\cal A}$-implicant of $\phi$ (modulo ${\cal T}$) is a conjunction (or set) of literals $l_{1}\wedge\dots\wedge l_{n}$ such that $l_{i}\in{\cal A}$, for all $i\in\llbracket 1\mathrel{{.}\,{.}}\nobreak n\rrbracket$ and $l_{1}\wedge\dots\wedge l_{n}\models_{{\cal T}}\phi$.

We use the procedure GPiD described in [14] to generate ${\cal A}$-implicants. A simplified version of this procedure is presented in Algorithm 1. A call to the procedure GPiD($\phi,M,A,{\cal P}$) is meant to generate ${\cal A}$-implicants of $\phi$ that: (i) are of the form $M\cup A^{\prime}$, for some $A^{\prime}\subseteq A$; (ii) are as general as possible; and (iii) satisfy property ${\cal P}$. When $M$ itself is not an ${\cal A}$-implicant of $\phi$, a subset of relevant literals from $A$ is computed (Line 1), and for each literal in this subset, a recursive call is made to the procedure after augmenting $M$ with this literal and discarding all those that become irrelevant (Lines 1 and 1). In particular, the algorithm is parameterized by an ordering $<$ on abducible literals which is used to ensure that sets of hypotheses are explored in a non-redundant way. The algorithm relies on the existence of a decision procedure for testing satisfiability in ${\cal T}$ (Line 1). In practice, this procedure does not need terminating or complete222However, Theorem 3.1 only holds if the proof procedure is terminating and complete., e.g., it may be called with a timeout (any “unknown” result is handled as “satisfiable”). At Line 1, a model of the formula $\{\neg\phi\}\cup M$ is used to prune the search space, by dismissing some abducible literals. In practice, no such model may be available, either because no model building algorithm exists for the considered theory or because of termination issues. In this case, no such pruning is performed. Property ${\cal P}$ denotes an abstract property of sets of literals. It is used to control the form of generated ${\cal A}$-implicants, it is for example possible to force the algorithm to only generate ${\cal A}$-implicants with a fixed maximal size. For Theorem 3.1 to hold, it is simply required that ${\cal P}$ be closed under subsets, i.e., that for all sets of abducible literals $B$ and $C$, $B\subseteq C\wedge{\cal P}(C)\Rightarrow{\cal P}(B)$.

Compared to [14], details that are irrelevant for the purpose of the present paper are skipped and the procedure has been adapted to generate ${\cal A}$-implicants instead of implicates (implicants and implicates are dual notions).

Theorem 3.1 ([14])

The call $\textsc{GPiD}(\phi,\emptyset,{\cal A},{\cal P})$ terminates and returns a set of ${\cal A}$-implicants of $\phi$ satisfying ${\cal P}$. Further, if ${\cal P}$ is closed under subsets, then for every ${\cal A}$-implicant $I$ of $\phi$ satisfying ${\cal P}$, there exists $I^{\prime}\in\textsc{GPiD}(\phi,\emptyset,{\cal A},{\cal P})$ such that $I\models_{{\cal T}}I^{\prime}$.

This procedure also comes with generic algorithms for pruning redundant ${\cal A}$-implicants i.e., for removing all ${\cal A}$-implicants $I$ such that there exist another ${\cal A}$-implicant $I^{\prime}$ such that $I\models_{{\cal T}}I^{\prime}$, see [14, Section $4$].

4 Generating Loop Invariants

In this section, we present an algorithm for the generation of loop invariants. As explained in Section 2, we distinguish between $3$ kinds of verification conditions, which will be handled in different ways: assertion and propagation conditions; and loop pre-conditions. As can be seen from the rules in Figure 2, loop invariants can occur as antecedents in verification conditions, this is typically the case when a loop occurs just before an assertion in some execution path. In such a situation, we say that the considered condition depends on loop ${\tt L}$. When a condition depends on a loop, a strengthening of the loop invariant of loop ${\tt L}$ yields a strengthening of the hypotheses of the verification condition, i.e., makes the condition less general (easier to prove).

This principle is used in Algorithm 2, which we briefly describe before going into details. Starting with a program ${\tt P}$ in which it is assumed that every loop invariant is inductive, the algorithm attempts to recursively generate invariants that make all assertion conditions in ${\tt P}$ valid. It begins by selecting a non-valid formula $\phi$ from $\mathrm{VCgen}_{\mathrm{a}}({\tt P})$ and a location $\ell\in\mathrm{lloc}({\tt P})$ such that $\phi$ depends on $\ell$, then generates a set of hypotheses that would make $\phi$ valid (Line 2). For each such hypothesis $\xi$, a loop location $\ell^{\prime}$ such that $\ell^{\prime}\leq\ell$ is selected, and a formula $\xi^{\prime}$ that is a weakest precondition at $\ell^{\prime}$ causing $\xi$ to hold at location $\ell$ is computed (Line 2). This formula is added to the invariant of the loop at location $\ell^{\prime}$ (Line 2), so that if this invariant was $\psi$, the new candidate invariant is $\xi^{\prime}\wedge\psi$. If $\xi^{\prime}$ does not hold before entering the loop then $\xi$ is discarded (Line 2); otherwise, the program attempts to update the other loop invariants to ensure that $\xi^{\prime}$ propagates (Line 2). When this succeeds, a recursive call is made with the updated invariants (Line 2) to handle the other non-valid assertion conditions.

Procedure $\textsc{Abduce}(\phi)$ (invoked Line 2 of Algorithm 2) is described in Algorithm 3. It generates formulas $\xi$ that logically entail $\phi$; it is used to generate the candidate hypotheses for strengthening. It first extracts a set of abducible literals ${\cal A}$ by collecting variables and symbols from the program and/or from the theory ${\cal T}$ and combining them to create literals up to a certain depth (procedure GetAbducibles at Line 3). To avoid any redundancy, this task is actually done in two steps: a set of abducible literals for the entire program is initially constructed (this is done once at the beginning of the search), and depending on the considered program location, a subset of these literals is selected. The abducible literals that are logically entailed by $\phi$ modulo ${\cal T}$ are filtered out (Line 3), and procedure GPiD is called to generate ${\cal A}$-implicants of $\phi$. Finally, ${\cal A}$-implicants are combined to form disjunctive formulas. Note that another way of generating disjunction of literals would be to add these disjunction in the initial set of abducible literals, but this solution would greatly increase the search space.

Each of the hypotheses $\xi$ generated by $\textsc{Abduce}(\phi)$ is used to strengthen the invariant of a loop occurring at position $\ell^{\prime}\leq\ell$ (Line 2 in Algorithm 2). The strengthening formula is computed using the Weakest Precondition Calculus on $\xi$, on a program obtained from ${\tt P}$ by ignoring all loops between $\ell^{\prime}$ and $\ell$, since they have corresponding invariants. To this purpose we define a function $\mathit{bp}(\phi,{\tt P},\ell,\ell^{\prime})$ which, for positions $\ell^{\prime}\leq\ell$, back-propagates abductive hypotheses from a location $\ell$ to $\ell^{\prime}$ (see Figure 4). This is done by extracting the part of the code $\mathit{path}({\tt P},\ell^{\prime},\ell)$ between the locations $\ell^{\prime}$ and $\ell$ while ignoring loops, and computing the weakest precondition corresponding to this part of the code and the formula $\phi$.

The addition of hypothesis $\xi^{\prime}$ to the invariant of the loop at position $\ell^{\prime}$ ensures that the considered assertion $\phi$ holds, but it is necessary to ensure that this strengthened invariant is still inductive. This is done as follows. Line 2 of Algorithm 2 filters away all candidates for which the precondition before entering the loop is no longer valid, and Algorithm 4 ensures that the candidate still propagates. This algorithm behaves similarly to Algorithm 2 (testing the verification conditions in $\mathrm{VCgen}_{\mathrm{ind}}({\tt P},\ell)$ instead of those in $\mathrm{VCgen}_{\mathrm{a}}({\tt P})$), except that it strengthens the invariants that correspond either to the considered loop, or to other loops occurring within it (in the case of nested loops). Note that in this case, properties must be propagated forward, from location $\ell$ to the actual location of the strengthened invariant, using a Strongest Postcondition Calculus (Function $\mathit{fp}(\phi,{\tt P},\ell,\ell^{\prime})$ in Figure 4). This technique avoids considering hypotheses that do not propagate.

When applied on the program in Figure 1, Ilinva first sets the initial invariant of the loop to $\top$ and considers the assertion $\phi:\mathbf{head}(\texttt{L})=\mathbf{length}(\texttt{L})$. As the entailment $\top\models\phi$ does not hold, it will call GPiD to get an implicant of $\top\Rightarrow\phi$. Assume that GPiD returns the (trivial) solution $\phi$. As $\phi$ indeed holds when the loop is entered333This can be checked by computing the weakest precondition of $\phi$ w.r.t. Lines $1,2$. The obtained formula is $\mathbf{head}(\mathbf{list}(1,\mathbf{nil}))=\mathbf{length}(\mathbf{list}(1,\mathbf{nil}))$ which is equivalent to $\top$ (w.r.t. the usual definitions of $\mathbf{list}$ and $\mathbf{head}$)., Ilinva will add $\phi$ to the invariant of the loop and call Ind. Since $\phi$ does not propagate Ind will further strengthen the invariant, yielding, e.g., the correct solution: $\phi\wedge\texttt{i}=\mathbf{head}(\texttt{L})$.

The efficiency of Algorithm 2 crucially depends on the order in which candidate hypotheses are processed at Line 2 for the strengthening operation. The heuristic used in our current implementation is to try the simplest hypotheses with the highest priority. Abducible atoms are therefore ordered as follows: first boolean variables, then equations between variables of the same sort, then applications of predicate symbols to variables (of the appropriate sorts) and finally deep literals involving function symbols (up to a certain depth). In every case, negative literals are also considered, with the same priority as the corresponding atom. Similarly, unit ${\cal A}$-implicants are tested before non-unit ones, and single ${\cal A}$-implicants before disjunctions of ${\cal A}$-implicants. In the iteration on line 2 of Algorithm 2, the loops that are closest to the considered assertions are considered first. Due to the number of loops involved, numerous parameters are used to control the application of the procedures, by fixing limits on the number of abducible literals that may be considered and on the maximal size of ${\cal A}$-implicants. When a call to Ilinva fails, these parameters are increased, using an iterative deepening search strategy. The parameter controlling the maximal number of ${\cal A}$-implicants in the disjunctions (currently either $1$ or $2$) is fixed outside of the loop as it has a strong impact on the computation cost.

The following theorem states the main properties of the algorithm.

Theorem 4.1

Let ${\tt P}$ be a program such that $\mathrm{VCgen}_{\mathrm{ind}}({\tt P},\ell)$ and $\mathrm{VCgen}_{\mathrm{init}}({\tt P},\ell)$ are valid for all $\ell\in\mathrm{lloc}({\tt P})$. If Ilinva (${\tt P}$) terminates and returns a program ${\tt P}^{\prime}$ other than $\mathbf{fail}$, then ${\tt P}\sim{\tt P}^{\prime}$ and $\mathrm{VCgen}({\tt P}^{\prime})$ is valid modulo ${\cal T}$. Furthermore, if the considered set of abducible literals is finite (i.e., if there exists a finite set ${\cal A}$ such that $\textsc{GetAbducibles}(\phi)\subseteq{\cal A}$ for all formulas $\phi$), then Ilinva (${\tt P}$) terminates.

Proof

{conference}

The proof is provided in the extended version444TODO: Import the extended version on arxiv and add the link to the extended version here.

{report} The proof is by induction on the recursive calls. It is clear that ${\tt P}\sim{\tt P}^{\prime}$ because the algorithm only modifies loop invariants. By construction (Line 2 of Algorithm 2), $\mathrm{VCgen}_{\mathrm{a}}({\tt P})$ must be valid when ${\tt P}$ is returned. By hypothesis $\mathrm{VCgen}_{\mathrm{ind}}({\tt P},\ell)$ and $\mathrm{VCgen}_{\mathrm{init}}({\tt P},\ell)$ are valid, and by definition $\mathrm{VCgen}({\tt P})=\mathrm{VCgen}_{\mathrm{a}}({\tt P})\cup\bigcup_{\ell\in\mathrm{lloc}({\tt P})}(\mathrm{VCgen}_{\mathrm{init}}({\tt P},\ell)\cup\mathrm{VCgen}_{\mathrm{ind}}({\tt P},\ell))$, thus $\mathrm{VCgen}({\tt P})$ is valid in this case. Furthermore, it is easy to check, by inspection of Algorithm 4, that all the recursive calls to Ilinva occur on programs such that $\mathrm{VCgen}_{\mathrm{ind}}({\tt P},\ell)$ is valid. Furthermore, all the formulas $\mathrm{VCgen}_{\mathrm{init}}({\tt P},\ell^{\prime})$ are also valid, due to the tests at Line 2 in Algorithm 2 and Line 4 in Algorithm 4 (indeed, it is clear that the strengthening of the invariant at location $\ell^{\prime}$ preserves the validity of $\mathrm{VCgen}_{\mathrm{init}}({\tt P},\ell)$ for $\ell\not=\ell^{\prime}$). Thus the precondition above holds for these recursive calls and the result follows by the induction hypothesis.

Termination is immediate since there are only finitely many possible candidate invariants built on ${\cal A}$, thus the (strict) strengthening relation (formally defined as: $\phi>\psi\iff\psi\models\phi\wedge\phi\not\models\psi$) forms a well-founded order. At each recursive call, one of the invariants is strictly strengthened and the other ones are left unchanged hence the multiset of invariants is strictly decreasing, according to the multiset extension of the strengthening relation.

5 Implementation

5.1 Overview

The Ilinva algorithm described in Section 4 has been implemented by connecting Why3 with GPiD. {report} A workflow graph of this implementation is shown on Figure 5. The input file (a WhyML program) and a configuration is forwarded to the tool via the command line. The tool then loads this input file within a wrapper where it identifies the candidate loop invariants that may be strengthened by the system. This wrapper will also modify the candidate loop invariants within the program when strengthened, and can export the corresponding file at any time.

The main system then forwards the configuration to the invariant generation algorithm. During the execution of the Ilinva algorithm, the WhyML wrapper is tasked to query Why3 to check whether the latter is able to prove all the assertions of the updated program, and if not to recover the verification conditions that are not satisfied. Selected conditions are transferred to the main generator which will create appropriate abduction tasks for them, ask GPiD for implicants, select the meaningful ones and strengthen associated candidate loop invariants accordingly. When a proof for the verification conditions of the program is found, the file wrapper returns the program updated with the corresponding loop invariants. We also expressed that GPiD candidates can be pruned when they contradict loops initial conditions. Note that both GPiD and Why3 call external SMT solvers to check the satisfiability of formulas.

{conference} A workflow graph of this implementation is detailed in the extended paper. Note that both systems themselves call external SMT solvers to check the satisfiability of formulas.

In particular, the GPiD toolbox is easy to plug to any SMTlib2-compliant SMT solver. The framework is actually generic, in the sense that it could be plugged with other systems, both to generate and verify proof obligations and to strengthen loop invariants. It is also independent of the constructions used for defining the language: other constructions (e.g., for loops) can be considered, provided they are handled by the program verification framework.

{report}

Given an input program written in WhyML, Why3 generates a verification condition the validity of which will ensure that all the asserted properties are verified (including additional conditions related to, e.g., memory safety) This initial verification condition is split by Why3 into several subtasks. These conditions are enriched with all appropriate information (e.g., theories, axioms,…) and sent to external SMT solvers to check satisfiability. The conditions we are interested in are those linked to the proofs of the program assertions, as well as those ensuring that the candidate loop invariants are inductive. In our implementation, Why3 is taken as a black box, and we merely recover the files that are passed from Why3 to the SMT solvers, together with additional configuration data for the solvers we can extract from Why3. If the proof obligation fails, then we relate the file to the corresponding assertion in the WhyML program and extract the set of abducible literals as explained in Section 4, restricting ourselves to symbols corresponding to WhyML variables, functions and predicates. We then tune the SMTlib2 file to adapt it for computations by GPiD and invoke GPiD with the same SMT-solver as the one used by Why3 to check satisfiability, as the problem is expected to be optimized/configured for it. We also configure GPiD to skip the exploration of subtrees that will produce candidate invariants that do not satisfy the loop preconditions. GPiD returns a stream of solutions to the abductive reasoning problem. We then backward-translate the formulas into the WhyML formalism and use them to strengthen loop invariants. For efficiency, the systems run in parallel: the generation of abductive hypotheses (by GPiD, via the procedure Abduce) and their processing in WhyML (via Ilinva) is organized as a pipe-line, where new abduction solutions are computed during the processing of the first ones.

To bridge Ilinva and Why3, we had to devise an interface, which is able to analyze WhyML programs and to identify loop locations and the corresponding invariants. It invokes Why3 to generate and prove the associated verification tasks, and it recovers the failed ones. The library also includes tools to extract and modify loop invariants, to extract variables and reference variables in WhyML files, as well as types, predicates and functions, and wrappers to call the Why3 executable and external tools, and to extract the files sent by WhyML to SMT-solvers.

5.2 Distribution

The Abdulot framework is available on GitHub [7]. It contains an revamped interface to the GPiD libraries and algorithm, a generic library of the Ilinva algorithm automatically plugged with GPiD, the code interface for Why3 and the related executables. GPiD interfaces and related executables are generated for CVC4, Z3 and AltErgo 555Those are the three solvers the Why3 documentation recommends to work with as an initial setup. (see also http://why3.lri.fr/@External Provers.) via their SMTlib2 interface. Note that the SMT solvers are not provided by our framework, they must be installed separately (all versions with an SMTlib2-compatible interface are supported). Additional interfaces and executables can be produced using C++ libraries for MiniSAT, CVC4 and Z3 if their supported version is available666The AltErgo interface provided by the tool uses an SMTlib2 interface that is under heavy development and that, in practice, does not work well with the examples we send it..

The framework also provides libraries and toolbox executables to work with abducible files, C++ libraries to handle WhyML files, helpers for the generation of abducible literals out of SMTlib2 files, and an extensive lisp parser. It also includes a documentation, which explains in particular how to extend it to other solvers and program verification framework. All the tools can be compiled using any C++ 11 compliant compiler. The whole list of dependencies is available in the documentation, as well as a dependency graph for the different parts of the framework.

6 Experiments

We use benchmarks collected from several sources [13, 4, 5, 6, 1, 2, 3] (see also [7] for a more detailed view of the benchmark sources), with additional examples corresponding to standard algorithms for division and exponentiation (involving lists, arrays, and non linear arithmetic). Some of these benchmarks have been translated777The translation was done by hand. from C or Java into WhyML. In all cases, the initial invariant associated with each loop is $\top$. We used Z3 for the benchmarks containing real arithmetic, AltErgo for lists and arrays and CVC4 in all the other cases. All examples are embedded with the source of the Ilinva tool.

6.1 Results

We ran Ilinva on each example, first without disjunctive invariants (i.e., taking $n=1$ in Procedure Abduce) then with disjunctions of size $2$. The results are reported in Figure 6. For each example, we report whether our tool was able generate invariants allowing Why3 to check the soundness of all program assertions before the timeout, in which case we also report the time Ilinva took to do so (columns T(C) when generating conjunctions only and T(D) when generating implicants containing disjunctions). We also report the number of candidate invariants that have been tried (columns C(D) and C(D)) and the number of abducible literals that were sent to the GPiD algorithm (column Abd). Note that the number of candidate invariants does not correspond to the number of SMT calls that are made by the system: those made by GPiD to generate these candidates are not taken into account. The timeout is set to $20$ min. For some of the examples that we deemed interesting, we allowed the algorithm to run longer. We report those cases by putting the results between parentheses. Light gray cells indicate that the program terminates before the timeout without returning any solution, and dark gray cells indicate that the timeout was reached. Empty cells mean that the tool could not generate any candidate invariant. The last column of both tables report the time Why3 takes to prove all the assertions of an example when correct invariants are provided.

The tests were performed on a computer powered by a dual-core Intel i5 processor running at 1.3GHz with 4 GB of RAM, under macOS 10.14.3. We used Why3 version 1.2.0 and the SMT solvers AltErgo (version 2.2.0), CVC4 (prerelease of version 1.7) and Z3 (version 4.7.1).

An essential point concerns the handling of local solver timeouts. Indeed, most calls to the SMT solver in the abductive reasoning procedure will involve satisfiable formulas, and the solvers usually take a lot of time to terminate on such formulas (or in the worst case will not terminate at all if the theory is not decidable, e.g., for problems involving first-order axioms). We thus need to set a timeout after which a call will be considered as satisfiable (see Section 3). Obviously, we neither want this timeout to be too high as it can significantly increase computation time, nor too low, since it could make us miss solutions. We decided to set this timeout to $1$ second, independently of the solver used, after measuring the computation time of the Why3 verification conditions already satisfied (for which the solver returns unsat) across all benchmarks. We worked under the assumption that the computation time required to prove the other verification conditions when possible would be roughly similar.

6.2 Discussion

As can be observed, Ilinva is able to generate solutions for a wide range of theories, although the execution time is usually high. The number of invariant candidates is relatively high, which has a major impact on the efficiency and scalability of the approach.

When applied to examples involving arithmetic invariants, the program is rather slow, compared to the approach based on minimization and quantifier elimination [13]. This is not surprising, since it is very unlikely that a purely generic approach based on a model-based tree exploration algorithm involving many calls to an SMT solver can possibly compete with a more specific procedure exploiting particular properties of the considered theory. We also wish to emphasize that the fact that our framework is based on an external program verification system (which itself calls external solvers) involves a significant overcost compared to a more integrated approach: for instance, for the Oxy examples (taken from [13]), the time used by Why3 to check the verification conditions once the correct invariants have been generated is often greater than the total time reported in [13] for computing the invariants and checking all properties. Of course, our choice also has clear advantages in terms of genericity, generality and evolvability.

When applied to theories that are harder for SMT solvers, the algorithm can still generate satisfying invariants. However, due to the high number of candidates it tries, combined with the heavy time cost of a verification (which can be several seconds), it may take some time to do so.

The number of abducible literals has a strong impact on the efficiency of the process, leading to timeouts when the considered program contains many variables or function/predicate symbols. It can be observed that the abduction depth is rather low in all examples ($1$ or $2$).

Our prototype has some technical limitations that have a significant impact on the time cost of the execution. For instance, we use SMTlib2 files for communication between GPiD and CVC4 or Z3, instead of using the available APIs. We went back to this solution, which is clearly not optimal for performance, because we experienced many problems coping with the numerous changes in the specifications when updating the solvers to always use the latest versions. The fact that Why3 is taken as a black box also yields some time consumption, first in the (backward and forward) translations (e.g., to associate program variables to their logical counterparts), but also in the verification tasks, which have to be rechecked from the beginning each time an invariant is updated. Our aim in the present paper was not to devise an efficient system, but rather to assess the feasability and usefulness of this approach. Still, the cost of the numerous calls to the SMT solvers and the size of the search tree of the abduction procedure remain the bottleneck of the approach, especially for hard theories (e.g., non-linear arithmetics) for which most calls with satisfiable formulas yield to a local timeout (see Section 6.1).

7 Conclusion and Future Work

By combining our generic system GPiD for abductive reasoning modulo theories with the Why3 platform to generate verification conditions, we obtained a tool to check properties of WhyML programs, which is able to compute loop invariants in a purely automated way.

The main drawback of our approach is that the set of possible abducible literals is large, yielding a huge search space, especially if disjunctions of ${\cal A}$-implicants are considered. Therefore, we believe that our system in its current state is mainly useful when used in an interactive way. For instance, the user could provide the properties of interest for some of the loops and let the system automatically compute suitable invariants by combining these properties, or the program could rely on the user to choose between different solutions to the abduction problem before applying the strengthening. Beside, it is also useful for dealing with theories for which no specific abductive reasoning procedure exists, especially for reasoning in the presence of user-defined symbols or axioms.

In the future, we will focus on the definition of suitable heuristics for automatically selecting abducible literals and ordering them, to reduce the search space and avoid backtracking. The number of occurrences of symbols should be taken into account, as well as properties propagating from previous invariant strengthening. A promising approach is to use dynamic program analysis tools to select relevant abducibles. It would also be interesting to adapt the GPiD algorithm to explore the search space width-first, to ensure that simplest solutions are always generated first. Another option is to give Ilinva a more precise control on the GPiD algorithm, e.g., to explore some branches more deeply, based on information related to the verification conditions. GPiD could also be tuned to generate disjunctions of solutions in a more efficient way.

From a more technical point of view, a tighter integration with the Why3 platform would certainly be beneficial, as explained in Section 6.2. The framework could be extended to handle procedures and functions (with pre- and -post conditions).

A current limitation of our tool is that it cannot handle problems in which Why3 relies on a combination of different solvers to check the desired properties. In this case, Ilinva cannot generate the invariants, as the same SMT solver is used for each abduction problem (trying all solvers in parallel on every problem would be possible in theory but this would greatly increase the search space). This problem could be overcome by using heuristic approaches to select the most suited solver for a given problem.

From a theoretical point of view, it would be interesting to investigate the completeness of our approach. It is clear that no general completeness result possibly holds, due to usual theoretical limitations, however, if we assume that a program ${\tt P}^{\prime}\sim{\tt P}$ such that $\mathrm{VCgen}({\tt P}^{\prime})$ is valid exists, does the call $\textsc{Ilinva}({\tt P})$ always succeed? This of course would require that the invariants in ${\tt P}^{\prime}$ can be constructed from abducibles occurring in the set returned by the procedure GetAbducibles.