Maximal Quantified Precondition Synthesis for Linear Array Loops

Abstract

Precondition inference is an important problem with many applications in verification and testing. Finding preconditions can be tricky as programs often have loops and arrays, which necessitates finding quantified inductive invariants. However, existing techniques have limitations in finding such invariants, especially when preconditions are missing. Further, maximal (or weakest) preconditions are often required to maximize the usefulness of preconditions. So the inferred inductive invariants have to be adequately weak. To address these challenges, we present an approach for maximal quantified precondition inference using an infer-check-weaken framework. Preconditions and inductive invariants are inferred by a novel technique called range abduction, and then checked for maximality and weakened if required. Range abduction attempts to propagate the given quantified postcondition backwards and then strengthen or weaken it as needed to establish inductiveness. Weakening is done in a syntax-guided fashion. Our evaluation performed on a set of public benchmarks demonstrates that the technique significantly outperforms existing techniques in finding maximal preconditions and inductive invariants.

1 Introduction

Many practical problems in software development, verification, and testing rely on good and nontrivial preconditions for programs. Preconditions can be considered as a constraint on a program’s input or used to filter out input values of a program at run-time. While performing verification in a backward fashion, preconditions are used to summarize loops and functions. The maximal (or logically weakest) precondition is desirable in all these applications. Such preconditions can be derived in various methods [3, 13, 14, 25, 45, 46, 53, 54].

However, precondition inference is known to be difficult for programs with unbounded loops, as it requires reasoning about possible behaviors in any any loop iteration. This necessitates the inference of inductive invariants that describe a set of states from which a new iteration can begin and cannot escape. This task becomes particularly challenging in the presence of data structures like arbitrarily-sized arrays. When reasoning about array elements, solvers are expected to support quantifiers, but existing techniques [22, 30, 32, 34, 40] have many limitations.

We present a new technique to automatically infer maximal quantified preconditions for deterministic programs that manipulate arrays and have linear array loops. These loops are non-nested and terminating loops with unique counter variables. The postconditions can have either universal or existential quantification. Since such programs can model many practical programs, several techniques target them, but for assertion checking and not precondition inference [10, 39]. Moreover, we show in this paper that precondition inference is undecidable for this class of programs.

Fig. 1.

An overview of our infer-check-weaken framework.

An overview of our algorithm is shown in Fig. 1. The algorithm operates in an “infer-check-weaken” framework. Our algorithm views the problem as solving a system of constrained Horn clauses (CHCs), which are logical systems to represent the verification conditions of programs, with a missing precondition $\boldsymbol{pre}$. A valid solution for this system is inferred by an abduction-based algorithm, i.e., by systematically answering the questions like “what state at the beginning of the iteration could yield a given state at the end of the iteration?” The solution is then checked for maximality by inferring another precondition ($\boldsymbol{cpre}$) for a system that uses the same CHC encoding of the loop and the complemented (i.e., negated) postcondition. If the solution is not maximal, it is weakened incrementally in a counter-example-guided loop.

The inference algorithm begins with the weakest possible candidate solution and propagates the given quantified postcondition towards the program’s entry point. In the process, it strengthens the candidate solution using our novel technique called range abduction. Range abduction finds a strengthening of quantified formulas by reduction (wherever possible) to abduction over quantifier-free formulas. The obtained formulas are combined with the range formula [22] that essentially represents a boundary between the indices of arrays that are already processed and indices that are yet to be processed. Such a predicate can be obtained using lightweight static analysis over the structure of the CHCs. The inference algorithm uses the Houdini technique [24] to weaken a solution.

Intuitively, range abduction for linear array loops seeks to pose two integer abduction queries over indices that are modified and indices that are not modified. Integer abduction has been used in invariant inference [17, 18], precondition inference [16, 27], and specification synthesis [2, 50]. On the lower level, abduction is often implemented using quantifier elimination, but in our setting the formulas must use quantifiers over array indices that should not be eliminated. Range abduction is designed specifically for this application.

Although efficient, range abduction does not guarantee maximality, and our inference is followed by two additional steps: maximality checking and weakening. The maximality checker tries to determine whether all the states outside the current precondition lead to a violation of the assertion. If they do, the current precondition is maximal. Otherwise, there is at least one state that can be added to the current precondition, and hence an attempt to weaken the precondition is made. The weakening module weakens a precondition and infers an inductive invariant for it using a syntax-guided-synthesis based method.

A prior framework [50] to find specifications (including preconditions) follows a similar approach by iteratively inferring solutions. But it is based on integer abduction and a maximality checking using an SMT solver, and it is applicable only to array-free programs. Furthermore, it does not guarantee maximality in some cases [29]. We experimentally observed that extending the SMT-based maximality checking algorithm of [50] with quantified formulas over arrays makes the tool diverge. This motivated us to design a new maximality checker by using $\boldsymbol{cpre}$ of the complement system and range abduction.

We have implemented our algorithm in a tool called PreQSyn, which takes CHCs as input. On a challenging set of 32 benchmarks, PreQSyn significantly outperforms a prior maximal quantified precondition inference tool P-Gen  [54]. PreQSyn automatically found 31 preconditions and proved 21 of them to be maximal, while in contrast P-Gen found only 2 maximal preconditions and in most cases did not find any preconditions. We also show that a variety of existing array verification tools like VeriAbs  [15], Spacer  [32], and FreqHorn  [22], find it hard to even verify the preconditions we discovered for these benchmarks. Our tool can not only solve them by finding preconditions, but also finds the maximal ones in most of the cases.

The core contributions of this paper are:

• 1. An algorithm, based on a new technique called range abduction, to infer universal and existential quantified preconditions and invariants, effective on linear array loop programs.

• 2. New methods to check maximality and weaken preconditions.

• 3. A tool that implements the algorithms to infer maximal preconditions and can be used as a CHC solver.

• 4. Experimental evaluation demonstrating the effectiveness of the algorithm.

Fig. 2.

C-like example with a universally quantified postcondition and no precondition.

Fig. 3.

CHC encoding of program in Fig. 2.

Fig. 4.

The program used to check maximality; the postcondition is complemented and has no precondition.

In the rest of the paper, we motivate the problem with an example in Sect. 2. The necessary background for abduction and CHCs are provided in Sect. 3. A proof of undecidability of the problem is in Sect. 4. Sect. 5 presents an overview of our inference algorithm and an illustration on the example. The details of range abduction are in Sect. 6, while Sect. 7 has the maximality checking and weakening algorithms. Our experimental evaluation can be found in Sect. 8, related work in Sect. 9, and conclude with limitations and future work in Sect. 10.

2 Motivating Example

We motivate the problem with the program shown in Fig. 2 with three finite-length statically allocated arrays A, B, and C, each of the size N. The arrays are accessed sequentially in the loop: the cells in the first half of C are assigned their corresponding indices, and the remaining elements of C are copied to the corresponding positions in A. The program ends with the postcondition stating the pairwise equality of A and B. Our goal is to find the maximal precondition under which the postcondition holds. Intuitively, such a precondition must be universally quantified because it must express that arrays A, B, and C are properly initialized up to an arbitrary length N.

Further, in order to prove that the postcondition indeed holds after the loop has terminated, we have to show that there exists an inductive invariant that is also universally quantified. To confirm that the precondition is logically the weakest, we need to formally prove that any attempt to extend it by a single point leads to a violation of the postcondition. Thus, the solution we target should have two properties: 1) it should allow us to find an inductive invariant for the loop, and 2) any of its weakening results in a counterexample that violates the assertion.

The only publicly existing tool to find quantified precondition, P-Gen  [54], which is based on predicate abstraction, is unable to solve this program. The last candidate precondition it tries to refine is $N=3 \wedge A[0] = B[0] \wedge A[1] = B[1] \wedge A[2] = B[2]$, which does not constrain the value of array C, thus allowing the program to violate the postcondition, e.g., when $C[2] \ne B[2]$ initially and $A[2] = C[2]$ in the else-branch when $i=2$.

Fig. 3 shows a system of CHCs over relations $\boldsymbol{pre}$ and $\boldsymbol{inv}$, representing the verification conditions of the program in Fig. 2. For brevity, we do not mention the universal quantification over all program variables including arrays, which is implicit. In particular, the first CHC identifies the initial value of the counter but does not give any constraints over A, B, or C (which are essentially deferred to $\boldsymbol{pre}$). The next two CHCs encode the loop body, corresponding to the two possible branches in the body of the loop. The last CHC encodes that no state satisfying the negation of the assertion is reachable.

The missing precondition makes the CHC system in Fig. 3 different from the CHC systems that appear in verification tasks. Hence, existing CHC solvers are not directly applicable here as they can return the strongest solution: $\bot$. For instance, Spacer  [32] (Z3 v4.12.2) returns the solution $\boldsymbol{pre}\mapsto \lambda N,A,B,C .\,\bot$ and $\boldsymbol{inv}\mapsto \lambda i,N,A,B,C .\,\bot$. Such vacuous solutions are not of much use in the applications mentioned earlier.

The CHC system also represents a maximal specification problem, with $\boldsymbol{pre}$ being the specification of an initialization function. However, existing maximal precondition synthesis techniques [2, 29, 50] do not support synthesizing quantified preconditions over arrays.

Our algorithm takes the input CHC system and works in an infer-check-weaken fashion as shown in Fig 1. First, the infer module strengthens and weakens the postcondition from the last CHC via range abduction and Houdini, resp., to find the following precondition (detailed illustration follows in Sect. 5.2):

$$ \lambda N,A,B,C.\,\forall j (0\!\le \! j\! <\! N\! \wedge 2*j\! <\! N\!\!\implies \!\! A[j]\! =\! B[j]) \wedge \! \forall j (0\!\le \! j\! <\! N\! \wedge 2*j\! \ge \!N\!\!\implies \!\! B[j]\! =\! C[j]).$$

We note that this is the maximal precondition for this problem instance, and in general we may not always find the maximal precondition in the first iteration. In any case, we need to check the maximality of the inferred precondition. Our maximality checker does this by trying to find a precondition for the complement of the postcondition (called the “complement program”, see Fig 4). This is achieved by calling the infer module again, albeit with an existentially quantified postcondition. By using the existentially quantified structure of the postcondition, the infer module discovers the following precondition (see Sect. 6.4 for details):

$$ \lambda N,A,B,C.\,\exists j (0\!\le \! j\! <\! N\! \wedge 2*j\! \ge \!N\!\wedge \! B[j]\! \ne \! C[j]). $$

The maximality checker now tries to determine whether all the points that are outside the precondition of the original program are indeed in the precondition of the complement program. For the example program, this is encoded as the following formula:

$$\begin{aligned} \forall A,B,N .\,\big (\lnot (\forall j (0\!\le \! j\! <\! N\! \wedge 2*j\! <\! N\!\!\implies \!\! A[j]\! =\! B[j]) \wedge \forall j (0\!\le \! j\! <\! N\! \wedge 2*j\! \ge \!N\!\!\implies \!\! B[j]\! =\! C[j]))\\ \implies \exists j (0\!\le \! j\! <\! N\! \wedge 2*j\! \ge \!N\!\wedge \! B[j]\! \ne \! C[j])\big ). \end{aligned}$$

If the formula was valid, the current precondition would be maximal since all the states outside would violate the property (as they would be in the precondition of the complement program). In this example, the implication is not valid, because $N=3$, $A=[0,0,0]$, $B=[1,0,0]$, $C=[0,0,0]$ is a counter-example to validity. Our approach then weakens the precondition of the complement program based on the counterexample to the validity check:

$$ \lambda N,A,B,C.\,\exists j (0\!\le \! j\! <\! N\! \wedge 2*j\! \ge \!N\!\!\implies \!\! B[j]\! \ne \! C[j]\!) \vee \! \exists j (0\!\le \! j\! <\! N\! \wedge 2*j\! <\! N\!\wedge \! A[j]\! \ne \! B[j]).$$

The checker now conducts a successful validity check, and the algorithm terminates.

3 Background

This paper builds largely on foundations of Satisfiability Modulo Theories (SMT) problems. SMT aims to determine the existence of an assignment to variables of a first-order logic formula that makes it true. We will be dealing with the logical setting $\mathcal {L}$ of linear integer arithmetic (LIA) with arrays. The signature of the logic includes a finite set of uninterpreted relation symbols $\mathcal {R}$. Each symbol r in $\mathcal {R}$ has an associated arity $a_r$, and an associated type which indicates a type (integer or array) for each argument of the relation.

We write $\varphi (x_1,\ldots ,x_n)$ (where each $x_i$ is a variable with an associated integer/array type) to denote a formula $\varphi$ of this logic, that does not use any of the relation symbols in $\mathcal {R}$, and whose free variables are among $\{x_1, \ldots , x_n\}$. For convenience, we also write $\varphi (\vec {x})$ to denote the same. For a formula $\varphi (\vec {x})$, and an assignment m which maps the variables in $\vec {x}$ to concrete integers/arrays, we write $m \models \varphi$ to denote that $\varphi$ evaluates to $\top$ under m, and say m satisfies $\varphi$, or that m is a model of $\varphi$. A formula $\psi$ is logically weaker than a formula $\varphi$ (denoted $\varphi \implies \psi$), if every model of $\varphi$ also satisfies $\psi$. Hence $\varphi \implies \bot$ denotes that $\varphi$ is unsatisfiable.

An interpretation for a relation symbol $r \in \mathcal {R}$ is defined as a map of the form $\lambda x_1 \ldots \lambda x_n.\varphi (x_1,\ldots ,x_n)$, where $\varphi$ is a well-typed first-order formula that does not contain any symbols from $\mathcal {R}$.

We now present formal definitions of the concepts that will be used in the rest of the paper.

3.1 Abduction

Definition 1

Let $\vec {x}$ and $\vec {y}$ be vectors of variables such that the variables in $\vec {x}$ are also present in $\vec {y}$. Let $\alpha (\vec {y})$ and $\beta (\vec {y})$ be formulas without any relation symbols from $\mathcal {R}$, with free variables in $\vec {y}$. Let r be an uninterpreted relation in $\mathcal {R}$ of arity equal to the length of $\vec {x}$. Consider a formula of the form $r(\vec {x}) \wedge \alpha (\vec {y}) \implies \beta (\vec {y})$. The abduction problem is to find an interpretation $\varphi$ for r, such that:

• 1.  , and

• 2. $\varphi (\vec {x}) \wedge \alpha (\vec {y}) \implies \beta (\vec {y})$.

Intuitively, the problem of abduction is to find a formula $\varphi$ that together with $\alpha$ entails the formula $\beta$ in a non-trivial manner. One can see that for a given abduction problem there may be multiple solutions, but we are interested in a maximal one (i.e. logically weakest), whenever a solution exists. The techniques in [2, 16, 17] compute such a maximal solution for first order theories that admit quantifier elimination. This solution is succinctly presented in the lemma below.

Lemma 1

Let $r(\vec {x}) \wedge \alpha (\vec {y}) \implies \beta (\vec {y})$ be an abduction problem where the underlying first order theory has a method $\textsc {QE} (\vec {q}, \psi )$ whose result is a $\vec {q}$-free formula constructed by (existential) quantifier elimination of variables $\vec {q}$ from the formula $\psi$. Suppose that the given instance has a solution. Then, the following formula $\varphi (\vec {x})$ forms a maximal solution for the abduction problem:

Example 1

Consider an instance of the abduction problem $r(x) \wedge y=0 \implies x > y$. Then $\varphi (x)$ is computed as follows:

$$\begin{aligned} \varphi (x)=\lnot (\textsc {QE} (\{x,y\} \setminus \{x\}, y=0 \wedge x \le y)) = \\\lnot (\textsc {QE} (y, y = 0 \wedge x \le y)) = \lnot (x \le 0) = x > 0. \end{aligned}$$

3.2 Modeling Programs With Constrained Horn Clauses

Constrained Horn clauses (CHCs) [23, 28, 31, 35, 37, 50, 51, 57] are becoming increasingly popular as an intermediate logical representation of programs and their proof obligations. Dealing directly with CHCs as opposed to program statements is convenient and allows for easier creation and handling of various SMT formulas and constructed invariants.

Definition 2

A CHC (in the logic $\mathcal {L}$) is a formula in $\mathcal {L}$ that has the form of one of the following three implications:

$$\begin{aligned} & \forall \vec {x_1} .\,(\varphi _1(\vec {x_1})\implies {r}_1(\vec {x_1})) \end{aligned}$$

(1)

$$\begin{aligned} & \forall \vec {x}_1,\vec {x}_2 .\,({r}_1(\vec {x}_1)\wedge \varphi _2(\vec {x}_1,\vec {x}_2)\implies {r}_{2}(\vec {x}_2)) \end{aligned}$$

(2)

$$\begin{aligned} & \forall \vec {x}_1 .\,({r}_1(\vec {x}_1)\wedge \varphi _3(\vec {x}_1)\implies \bot ) \end{aligned}$$

(3)

where:

• ${r}_1,{r}_2 \in \mathcal {R}$ are uninterpreted relation symbols, where ${r}_1$ and ${r}_2$ may coincide.

• $\vec {x_1},\vec {x_2}$ are vectors of variables;

• the vectors $\vec {x}_1$ and $\vec {x}_2$ have no common elements, and

• the formulas $\varphi _i$, called constraints, have no uninterpreted symbols from $\mathcal {R}$.

We introduce some auxiliary notation below for convenience. For a CHC C:

• $body (C)$ (resp. $head (C)$) denotes the left (resp. right) side of the implication in C,

• $rel ( body (C))$ denotes the (singleton or empty) set of relation symbols in $\mathcal {R}$ that appear in $body (C)$,

• When C is of type (2), $rel ( head (C))$ denotes the singleton set $\{{r}_{2}\}$ containing the relation appearing in $head (C)$,

• When C is of type (2), $args ( body (C))$ (a.k.a. source variables) denotes $\vec {x}_1$ and $args ( head (C))$ (a.k.a. destination variables) denotes $\vec {x}_2$.

A CHC of type (1) is called a fact, and of type (3) is called a query. For simplicity, for a query C, we write $rel ( head (C))$ = $rel (\bot )$ = $\bot$. In the literature, the CHCs we are considering are called linear as there is at most one relation symbol in the body of a CHC. A system of CHCs is a finite non-empty set of CHCs.

We assume that our precondition inference problem is represented by a system of CHCs S without any facts¹ and there is a designated relation $\boldsymbol{pre}$ (or $\boldsymbol{cpre}$) that appears in $rel ( body (C))$ for some CHC C in S and doesn’t appear in $rel ( head (C'))$ for any other CHC $C'$ in S. Furthermore, we assume that there is a single query in S with a constraint of the form $\varphi \wedge \rho$, where $\lnot \rho$ is the postcondition in the inference problem.

CHCs allow for flexibility of program encoding. For instance, it is safe to assume that each $\varphi _C$ is in Conjunctive Normal Form (CNF). For if C had the following form:

$$\begin{aligned} {r}_1(\vec {x}_1)\wedge (\varphi _1(\vec {x}_1, \vec {x}_2)\vee \varphi _2(\vec {x}_1, \vec {x}_2)) \implies {r}_{2}(\vec {x}_{2}), \end{aligned}$$

it can be transformed into two CHCs:

$$\begin{aligned} {r}_1(\vec {x}_1)\wedge \varphi _1(\vec {x}_1, \vec {x}_2)\implies {r}_{2}(\vec {x}_{2}) \\ {r}_1(\vec {x}_1)\wedge \varphi _2(\vec {x}_1, \vec {x}_2)\implies {r}_{2}(\vec {x}_{2}). \end{aligned}$$

Definition 3 (CHC Solution and Satisfiability)

A solution to a system of CHCs S is a map $\mathcal {M}$ that provides an interpretation for each relation symbol in $\mathcal {R}$, such that for each CHC C in S, $\big ( body (C) \implies head (C)\big )[\mathcal {M}/\mathcal {R}]$² is valid. In this case we say $\mathcal {M}$ is inductive at C. We say S is satisfiable if there exists a solution to it.

Definition 4 (Maximal Precondition)

Let S be a system of CHCs for a precondition inference problem. We call a solution $\mathcal {M}$ to S (precondition) maximal if there is no solution $\mathcal {M}'$ to S with $\mathcal {M}'(\boldsymbol{pre})$ strictly logically weaker (i.e. w.r.t. the implication partial order) than $\mathcal {M}(\boldsymbol{pre})$. $\mathcal {M}(\boldsymbol{pre})$ is also called the weakest precondition.

We now define certain terms that will be used in weakening of a precondition (Sect. 7).

Definition 5 (Complement System)

Given a system of CHCs S, we define a complement system $\overline{S}$ to be the system obtained from S by replacing $\rho$ by $\lnot \rho$ in the query CHC.

Definition 6 (CHC Extension)

Given a system of CHCs S with $\boldsymbol{pre}$ and an interpretation $\varphi$ for $\boldsymbol{pre}$, we define $S_\varphi$, an extension of S w.r.t $\varphi$, to be the system obtained from S by replacing $\boldsymbol{pre}$ by $\varphi$ in the CHC $C \in S$, where $rel ( body (C)) = \{\boldsymbol{pre}\}$

Lemma 2

Given S with $\boldsymbol{pre}$ and its extension $S_\varphi$, if $\mathcal {M}_\varphi$ is a solution to $S_\varphi$ then $\mathcal {M}= \{\lambda r \in \mathcal {R}.\,\text {if}\; r = \boldsymbol{pre}\; \text {then}\; \varphi \; \text {else}\; \mathcal {M}_\varphi (r)\}$ is a solution to S.

To encode program executions, we borrow the notion of CHC unrolling from [21]. Essentially, a CHC unrolling is a symbolic representation of a set of program executions starting from a state satisfying $\varphi$. If the unrolling is satisfiable then the execution terminates in the postcondition.

Definition 7 (Unrolling of CHCs)

Given an extended CHC system $S_\varphi$ over $\mathcal {R}$, let $C_0,\ldots ,C_k$ be a $k+1$-length sequence of CHCs in $S_\varphi$, with $C_0$ being a fact, $C_k$ being a query, and $rel ( head (C_i)) = rel ( body (C_{i + 1}))$ for each i. Then, a k-length unrolling of $S_\varphi$ is defined as below:

Example 2

Consider the CHC system S from Fig. 3. Let $\varphi$ be:

$$(\forall j .\,0\le j<N \!\!\implies \! A[j] = B[j] = 0 \wedge C[j] = 1) \wedge N=1$$

Then $\pi _{\langle C_1,C_2,C_4 \rangle }$, which is a 3-length unrolling of $S_\varphi$, is the following satisfiable formula:

$$\begin{aligned} \pi _{\langle C_1,C_2,C_4 \rangle } \; =\; & (\forall j .\,0 \le j<N \!\!\implies \! A[j] = B[j] = 0 \wedge C[j] = 1) \wedge N=1 \wedge i = 0 \; \wedge \\ & \!i\! <\! N\! \wedge \!2*i\! <\! N\! \wedge C'\!\! = store(C, i, i) \wedge \! i'\! =\! i\! +\! 1 \; \wedge \\ & \lnot (\!i'\! <\! N\!) \wedge (\forall j.\,0\le j<N \!\!\implies \! A[j] \!=\! B[j]). \end{aligned}$$

Our technique addresses deterministic programs. A non-deterministic program in our context has an initial state that can both satisfy and violate the postcondition. More formally,

Definition 8 (Non-deterministic Modulo Postcondition CHCs)

Let S be a system of CHCs that has $\boldsymbol{pre}$ and extendable by a formula $\varphi$. We call S non-deterministic modulo postcondition if there exists an uniquely satisfiable formula s for which there are at least two satisfiable unrollings $\pi _{\langle C_0,\ldots ,C_{\ell } \rangle }$ and $\overline{\pi }_{\langle C_0,\ldots ,C_{m} \rangle }$ corresponding to extensions $S_s$ and $\overline{S}_s$, respectively. Otherwise, we say S is deterministic³.

We assume that the CHCs are representing terminating programs. Hence, for any initial state of a program encoded in CHCs, there exists an unrolling either satisfying or violating the postcondition.

Definition 9 (Terminating CHCs)

Let S be a system of CHCs with $\boldsymbol{pre}$ and extendable by a formula $\varphi$. We say S is terminating if there does not exist an infinite-length unrolling for $S_\top$ and $\overline{S}_\top$ (i.e. S and $\overline{S}$ are extended by $\varphi =\top$).

3.3 Linear Array Loop Programs

Though our algorithms work at the level of CHCs, we are motivated to target CHCs representing linear array loop programs (or “linear loops” in short) that model real-world programs in existing array program verification works [9, 10, 39]. These are terminating programs with non-nested loops. We now present the syntax of a linear loop.

$$\begin{aligned} program \;\rightarrow \; & \texttt {assume}(pre(V,A)); \; stmts; \; post; \\\nonumber stmts \;\rightarrow \; & assign \;\,\,\big |\,\, forloop \;\,\,\big |\,\,stmts;stmts \\\nonumber assign \;\rightarrow \; & v = f(V,A) \;\,\,\big |\,\,a[i] = f(V,A) \;\,\,\big |\,\,\texttt {if} (\phi (V)) \; \{assign\} \; \texttt {else} \; \{assign\} \\\nonumber & \,\,\big |\,\,assign;assign \\\nonumber forloop \;\rightarrow \; & \texttt {for} \;(i = l(V);\; c(i,V); \; i = h(i)) \;\{ assign \} \\\nonumber post \;\rightarrow \; & \texttt {assert}(\forall x .\,R(x, V) \implies Q(x, V, A)) \;\,\,\big |\,\,\texttt {assert}(\exists x .\,R(x, V) \wedge Q(x, V, A)) \end{aligned}$$

Here V and A are disjoint sets of integer and array variables, respectively, $i \in V$ is a loop counter, $v \ne i \in V$ is an integer variable, f is a term over V and A such that any access to A is done by i, l is an integer term over V, h is an integer term over i which results in a monotonically increasing (or decreasing) assignment, and c is a guard of the form $i < u$ or $i > u$ for some integer term u over V, and $\phi$ is a boolean predicate. The postcondition $\rho$ is given as a condition in assert, where R is a predicate in LIA over quantified and integer variables that represent a range of array elements, and Q is a property over an array with array read-access done only by x. For example, the formula $\forall x .\,0 \le x < N \implies B[x] = 42$ is in this form, where B is an array variable.

The precondition (and inductive invariants) inferred by our algorithm will be of the same quantification as the postcondition. Further, it can be conjunctions in case of universal quantification and disjunctions in case of existential quantification. Specifically, we consider preconditions (and inductive invariants) of the form described in (4). Such a form has been found effective in inferring inductive invariants in the existing works for array programs like [22, 32, 33, 38].

$$\begin{aligned} \bigwedge \big (\forall x .\,R(x, V) \implies Q(x, V, A)\big ) \;\; \text { or } \;\; \bigvee \big (\exists x .\,R(x, V) \wedge Q(x, V, A)\big ) \end{aligned}$$

(4)

A formal description of CHCs that represent linear loop programs is given in Sect. 6.1.

4 Undecidability of Maximal Precondition Inference for Linear Loops

Although linear loops and postconditions have syntactic restrictions, inference of maximal preconditions for such programs in the considered form (i.e.  (4)) is still undecidable. In this section we prove this result.

We reduce the halting problem of two-counter machines [42] to the maximal precondition inference problem. Recall that a two counter machine $M = (C_1, C_2, L)$ has two counters $C_1$ and $C_2$, which are initially set to 0, and a finite set of instructions $L = \{ l_1, \ldots , l_k\}$, where each instruction $l_i$ is of type inc, decjz, and a designated halt instruction $l_h$. Given a two-counter machine $M = (C_1 ,C_2, L)$, deciding whether it halts, i.e. the halt instruction $l_h \in L$ is reached, is undecidable.

Theorem 1

The problem of computing the maximal precondition for linear array loop programs in the form described in  (4) is uncomputable.

Proof Sketch We construct a linear array loop program with a single loop whose body simulates the execution of one transition of a two-counter machine, and an array records the locations the machine can reach after the transition.⁴

The undecidability of the problem notwithstanding, many real-life programs, like industrial battery controllers [9], adhere to linear array loop structures. Consequently, techniques like [10, 39] have been developed to address such programs, but focusing on assertion checking rather than precondition inference. The existing precondition inference technique [54] finds it challenging to infer a precondition for such programs (details in Section 8). Motivated by these challenges, we propose a sound technique that infers maximal preconditions.

5 Inferring Preconditions and Invariants by Abduction

In this section, we give an overview of our approach for abductive inference of preconditions and inductive invariants. We first explain its basic principles, and then demonstrate them on the running example.

5.1 Overview

We assume that the input system of CHCs S represents a precondition inference problem, i.e. it has no facts, a single query, and a designated relation ($\boldsymbol{pre}$ or $\boldsymbol{cpre}$) for the precondition. Since we are interested in the precondition inference for array programs, we assume that the query has a quantified constraint $\rho$.

The high-level algorithm is given in Algorithm 1. It is called InferAbd and is inspired by an earlier work on specification synthesis [50]. InferAbd incrementally attempts to discover an interpretation for each uninterpreted predicate in $\mathcal {R}$ by propagating the assertion backward, strengthening it when needed to establish inductiveness, or weakening if something went wrong during the inference of inductive invariants.

InferAbd (Algorithm 1) constructs a solution $\mathcal {M}$ for a system of CHCs recursively. $\mathcal {M}$ initially maps all the predicates in $\mathcal {R}$ to $\top$. At each call, the algorithm searches for a CHC C (line 3) such that $\mathcal {M}$ is not inductive at C. This inductiveness check is reduced to a satisfiability check, which is performed by an SMT solver (line 4). If $\varphi$ is satisfiable then $\mathcal {M}$ is not inductive at the corresponding C, and thus $\mathcal {M}$ needs strengthening.

Note that in the first call of InferAbd, the initial $\mathcal {M}$ is inductive for all the CHCs except the query, thus the interpretations will be created for the predicates that appear in the body of the query. In the subsequent calls, these interpretations could be either strengthened or propagated through the bodies of the CHCs where they appear in the heads, towards the precondition.

In InferAbd, we write $\psi \leftarrow \textsc {Abduce}(\varphi , \vec {x}, S)$ to denote an invocation of a new abduction algorithm (Algorithm 2) to obtain a formula $\psi$ over variables $\vec {x}$ that makes $\varphi$ valid. InferAbd uses Abduce as existing abduction solvers have limited support for arrays. In order to support arrays and quantifiers, Abduce abstracts quantified formulas over arrays and integers into quantifier-free formulas only over integers. To do this, Abduce considers two abduction queries for a CHC in S: 1) for the array element that is being rewritten (if any), and 2) for all other elements that are not changed. The formal description of Abduce is in Sect 6 along with illustration. However, by doing this “arrays-to-integer” reduction, Abduce could introduce some imprecision, which is fixed by running the Houdini algorithm (details in Sect 6.3).

InferAbd may not terminate because the series of strengthening predicates obtained in each iteration may diverge. But the recursion in InferAbd can be easily augmented by a threshold condition that forces the termination with an unknown result after reaching a predetermined recursion depth.

Theorem 2

Whenever Algorithm 1 terminates, it returns a solution $\mathcal {M}$ to S.

5.2 Approach in Action

We demonstrate the precondition inference approach on the example from Sect. 2 and Fig. 3.

Synthesizing an invariant for ${\boldsymbol{inv}}$ The algorithm begins with obtaining an initial candidate interpretation to $\boldsymbol{inv}$ from the query CHC. The predicate is the query constraint (i.e. the postcondition $\lnot \rho$) with a slight modification:

The modification includes drop** the loop condition and strengthening it by conjuncting a range formula [21] to the antecedent ($j < i$ here). In simple terms, the range formula is a predicate that represents the boundary between indices that are modified and not modified. It can be ($j < i$) or ($j > i$), based on whether the loop counter is increasing or decreasing, respectively (formal definition in  11).

Our algorithm then checks if any of the CHCs in $Worklist$ are not valid. In this case, the second CHC is not valid. The algorithm then follows backward reasoning and attempts to update the current interpretation of $\boldsymbol{inv}$ by abductive strengthening to make it inductive using a series of SMT checks and quantifier elimination queries.

The algorithm does abductive strengthening by posing two queries. The first one is to accommodate the write to the i-th element of the array. This strengthening for the second CHC is posed as an abduction query for $\psi _1$ that is constructed by restricting to only a single cell of the array that is rewritten in the loop:

$$\begin{aligned} \psi _1(A,B,C, j) \wedge A'[j]\! =\! A[j] \wedge B'[j]\! =\! B[j] \wedge \boldsymbol{C'[j] = j} \implies A'[j]\! =\! B'[j]. \end{aligned}$$

Here, all the array terms (like A[j], $A'[j]$, B[j], etc.) are further replaced by fresh integer variables which allows us to use a standard abduction solver and get the following solution:

$$\psi _1 \mapsto \lambda A,B,C,j .\,A[j]\! =\! B[j].$$

Intuitively, $\psi _1$ gives the weakest precondition on A[i], B[i] and C[i] before the i-th loop iteration, such that the desired postcondition holds for $A'[i]$ and $B'[i]$ after the iteration.

The second abduction query accommodates all the other elements in the range $0\!\le \! j\! <\! N\wedge j \ne i$ that are unaffected in the i-th iteration:

$$\begin{aligned} \psi _2(A,B,C, j) \wedge A'[j]\! =\! A[j] \wedge \boldsymbol{C'[j]\! =\! C[j]} \wedge B'[j]\! =\! B[j] \implies A'[j]\! =\! B'[j]. \end{aligned}$$

The delta w.r.t. the first query is shown in bold. This query also has the same solution as $\psi _1$.

$$\psi _2 \mapsto \lambda A,B,C,j .\,A[j]\! =\! B[j].$$

To build the new invariant from $\psi _2$ and $\psi _1$ to the new invariant candidate, we split the array range into two segments based on the range formula, and its negation:

The second conjunct is derived from $\psi _2$ and the range formula ($j < i$), whereas the third conjunct is from $\psi _1$ and negation of the range formula ($j \ge i$). If the CHC has any additional constraints (like $2*i < N$ here) that will be added in the antecedent as well.

While validating this candidate, the algorithm goes over the CHCs again and checks the implications: it now turns out to be not inductive for the third CHC. The algorithm thus repeats the abductive strengthening and poses two queries:

$$\begin{aligned} \psi _3(A,B,C, j) \wedge B'[j]\! =\! B[j] \wedge C'[j]\! =\! C[j] \wedge \boldsymbol{A'[j] \!=\! C[j]} \implies A'[j]\! =\! B'[j],\\\psi _4(A,B,C, j) \wedge B'[j]\! =\! B[j] \wedge C'[j]\! =\! C[j] \wedge \boldsymbol{A'[j] \!=\! A[j]} \implies A'[j]\! =\! B'[j],\\\end{aligned}$$

getting the following next candidate, that is subsequently validated:

$$\begin{aligned} \boldsymbol{inv}\mapsto \lambda A,B,C,i .\,&\forall j (0\!\le \! j\! <\! N\wedge \! j <\! i \implies A[j]\! =\! B[j]) \wedge \\ &\forall j (0\!\le \! j\! <\! N\wedge j < i\! \wedge \! 2*j\! < \! N\! \!\!\implies \!\! A[j]\! =\! B[j]) \ \wedge \\ &\forall j (0\!\le \! j\! <\! N\wedge j \ge i\! \wedge \! 2*j\! < \! N\! \!\!\implies \!\! A[j]\! =\! B[j])\ \wedge \\ &\forall j (0\!\le \! j\! <\! N\wedge j < i\! \wedge \! 2*j\! \ge \! N\! \!\!\implies \!\! A[j]\! =\! B[j])\ \wedge \\ &\forall j (0\!\le \! j\! <\! N\wedge j \ge i\! \wedge \! 2*j\! \ge \! N\! \!\!\implies \!\! B[j]\! =\! C[j]). \end{aligned}$$

Synthesizing ${\boldsymbol{pre}}$ Finally, the precondition is obtained from the solution for $\boldsymbol{inv}$. Because the first CHC initializes the counter i to zero, all the conjuncts with $j<i$ simplify to true and the rest simplifies to:

$$\begin{aligned} \boldsymbol{pre}\mapsto \lambda N,A,B,C.\,\forall j (0\!\le \! j\! <\! N\wedge 2*j < N \!\!&\implies \!\! A[j]\! =\! B[j]) \ \wedge \\\forall j (0\!\le \! j\! <\! N\wedge 2*j \ge N \!\!&\implies \!\! B[j]\! =\! C[j]). \end{aligned}$$

6 Range Abduction

In this section, we present our technique called range abduction for inferring quantified invariants, and subsequently, quantified preconditions. We define the Abduce method for quantified formulas over arrays and linear arithmetic that can be used in the general algorithm of abductive invariant synthesis. Its core features include the capability to selectively apply quantifier elimination, such that it keeps all quantifiers that are explicit in the abducible formula. As its main computational vehicle, the method uses quantifier elimination over linear arithmetic on formulas produced from the actual abducibles by over-approximating (as precisely as possible) the array computation.

6.1 Preliminaries

CHCs We first formally describe the CHC structure that we support corresponding to linear loops. We assume that the inputs are given as CHCs, where bodies are in CNF (otherwise, it can be transformed following Sect. 3.2). For each CHC, we consider two disjoint vectors of source (resp., destination) variables, ${\vec {v}}$ and ${\vec {a}}$ (resp., ${\vec {v}}\,'$ and ${\vec {a}}\,'$), such that only ${\vec {a}}$ (resp., ${\vec {a}}\,'$) consists of array variables.

We allow only a single index to access elements of all arrays $b\in {\vec {a}}$ in each CHC C, and without loss of generality we assume that it is an integer variable $i\in {\vec {v}}$ (usually, a loop counter).⁵ For simplicity, we also introduce a set of temporary integer variables ${\vec {t}}$ that store some elements selected from arrays and can be used in other parts of C (e.g., to compute the next value to be written to an array $b'$ via some function f). Thus, we assume that only three possible types of constraints are used to equate arrays (or their elements), and that they appear in recursive CHCs, that is:

$$\begin{aligned} \begin{aligned} \boldsymbol{inv}_1&({\vec {v}}, {\vec {a}}) \wedge \big [(a'=a\wedge )^{*}\big ] \wedge \big [(t = a[i]\wedge )^{*}\big ] \wedge \\&\big [(b' = store (b, i, f({\vec {v}}, {\vec {t}}))\wedge )^{*}\big ] \wedge \varphi ({\vec {v}}, {\vec {v}}\,', {\vec {t}}) \implies \boldsymbol{inv}_2({\vec {v}}\,', {\vec {a}}\,') \end{aligned} \end{aligned}$$

(5)

where $^{*}$ is Kleene star, $a,b \in {\vec {a}}$, $a', b' \in {\vec {a}}\,'$, $t\in {\vec {t}}$, and $\varphi$ is over only non-array variables. Note that sequences of stores (e.g., nested) could be supported after some sort of a CHC normalization, e.g., by introducing temporary uninterpreted predicates and splitting C. Symbols $\boldsymbol{inv}_1$ and $\boldsymbol{inv}_2$ might refer to the same predicate.

Queries There is only a single query among CHCs, and it has the form of either of the two implications:

$$\begin{aligned} \boldsymbol{inv}({\vec {v}}, {\vec {a}})\! \wedge \! \varphi ({\vec {v}}) \wedge \exists x.\,\! (R( x, {\vec {v}}) \wedge Q( x, {\vec {v}}, {\vec {a}}))&\!\implies \! \bot \end{aligned}$$

(6)

$$\begin{aligned} \boldsymbol{inv}({\vec {v}}, {\vec {a}}) \!\wedge \! \varphi ({\vec {v}}) \wedge \forall x.\,\! (R( x, {\vec {v}}) \!\implies \! Q( x, {\vec {v}}, {\vec {a}})) &\!\implies \! \bot \end{aligned}$$

(7)

In the body of the query, there is a quantifier-free conjunct $\varphi$ and a quantified formula with subformulas R and Q. Formula $\varphi$ could represent the termination condition of the array processing loop/recursion (captured in the other CHCs). The subformulas R and Q could represent, respectively, a range of elements in an array (giving a condition over possible index x of the array), and a property over an array element (indexed using the x variable). We restrict read-accesses of arrays to the quantified variable only.

The formula in the query determines an initial candidate interpretation for the predicate in the query. For instance, in (6) and (7), respectively:

(8)

(9)

Applying Algorithm 1 We assume that an iteration of the algorithm deals with a map** $\mathcal {M}$ and the following CHC, where $\mathcal {M}(\boldsymbol{inv}_1)$ might be currently $\top$, but $\mathcal {M}(\boldsymbol{inv}_2)$ is quantified:

$$\begin{aligned} \boldsymbol{inv}_1({\vec {v}}, {\vec {a}}) \wedge \varphi ({\vec {v}}, {\vec {a}}, {\vec {v}}\,', {\vec {a}}\,')\implies \boldsymbol{inv}_2({\vec {v}}, {\vec {a}}) \end{aligned}$$

(10)

Abductive strengthening is needed when the following implication is not valid on substitutions of interpretations of $\boldsymbol{inv}_1$ and $\boldsymbol{inv}_2$ (line 6 of Algorithm 1), thus necessitating to find $\psi$, such that the following is valid:

$$\begin{aligned} \psi \wedge \varphi \implies \mathcal {M}(\boldsymbol{inv}_2) \end{aligned}$$

(11)

Intuitively, for $\psi$ our algorithm reuses the quantified structure of $\mathcal {M}(\boldsymbol{inv}_2)$. For all quantifier-free conjuncts of $\mathcal {M}(\boldsymbol{inv}_2)$, strengthening is done following the simple abduction, like e.g., in [17]. For quantified formulas, the algorithm is trickier. In the rest of this section, we assume that algorithms are strengthening w.r.t. formulas $\pi _{\exists }$ and $\pi _{\forall }$ having the forms, respectively (9) and (8).

6.2 Core Technique

The basic principle behind our quantified abductive strengthening is in the preservation of the range. That is, if the quantified formula on the right side of (11) has form (9) or (8), then it intuitively means that some property $Q(x, {\vec {v}}, {\vec {a}})$ should hold either for all elements of array(s) (when quantification is universal), or some elements of arrays ${\vec {a}}$ (when quantification is existential), determined by $R(x,{\vec {v}})$. Thus, an interpretation of predicate $\psi$ on the left side of (11) should also constrain all elements of (some) arrays belonging to the same range.

Since by our syntax restrictions we allow elements of arrays $b\in {\vec {a}}$ to be rewritten using only a single index i, each constraint $b' = store (b, i, f({\vec {v}}, {\vec {t}}))$ can be safely replaced in the CHC body as:

$$\begin{aligned} b'[i]=f({\vec {v}}, {\vec {t}}) \qquad \text {and}\qquad \forall j .\,i \ne j\!\implies \! b'[i]=b[i] \end{aligned}$$

In the following, we are going to use the auxiliary map** to reduce abduction over array and integer variables to purely integer abduction.

Definition 10

Let ${\vec {a}}$, ${\vec {t}}$, and ${\vec {t}}'$ be sets of array variables, integer variables, and integer terms, respectively, all of the same cardinality. A bijection $\mathcal{S}\mathcal{S}: {\vec {t}}' \rightarrow {\vec {t}}$ is called select-substitution w.r.t. index i, if for every $a\in {\vec {a}}$, there exists $t\in {\vec {t}}$ such that $\mathcal{S}\mathcal{S}(a[i]) = t$.

The pseudocode of our range abduction is given in Algorithm 2. Below we discuss its details.

Universally-quantified formulas (8) The abduction query $\pi$ of the form  (11) can be decomposed (line 1) into two stronger abduction queries, $\pi _1, \pi _2$:

$$\begin{aligned} \psi _1 \!\wedge \! \big [(b'[i]= f({\vec {v}}, {\vec {t}})\wedge )^{*}\big ]\!\! \! \ldots \!\!\implies \! \! (R( i, {\vec {v}})\!\implies \!\! Q( i, {\vec {v}}, {\vec {a}})) \end{aligned}$$

(12)

$$\begin{aligned} \psi _2 \!\wedge \! \big [(b'[i]=b[i]\wedge )^{*}\big ] \!\ldots \! \implies \! \! (R( i, {\vec {v}})\!\implies \! Q( i, {\vec {v}}, {\vec {a}})) \end{aligned}$$

(13)

Since $\mathcal {M}(\boldsymbol{inv}_2)$ is universally-quantified and due to our syntactic restrictions, only the i-th elements of any source arrays are relevant for the abduction query. Thus, without loss of generality, our algorithm lowers the (possibly) universally-quantified formula in $\mathcal {M}(\boldsymbol{inv}_2)$ to a quantifier-free formula over the i-th array element, and further replaces all the array access terms of the form a[i] to integer terms $a_i$ using a select-substitution $\mathcal{S}\mathcal{S}$, essentially boiling down to two abduction queries over pure integer arithmetic with abducibles $\psi '_1$ and $\psi '_2$ (lines 3, 4).

After the abduction solver returns $\psi '_1$ and $\psi '_2$ for the integer arithmetic queries, the $\mathcal{S}\mathcal{S}^{-1}$ map** is applied to replace integer terms $a_i$ by array terms a[i] to get $\psi _1$ and $\psi _2$ that constitute solutions to queries (12) and (13)(line 5).

It remains finally to re-introduce the universal quantifier for x to $\psi _1[x/i]$ and $\psi _2[x/i]$ to get a solution to our main abduction query (11). There are several ways to do it. One way is to not introduce quantifiers for $\psi _1$ as the query (12) captures the effect of a single store to an i-th element of an array. For $\psi _2$, then, the quantifier’s range will span over all the original range except i. However, this way, seemingly obvious, does not work in practice because the produced invariant is unlikely to be inductive.

Another way is to split the range into two segments with the border at i. It would intuitively correspond to the range formula computation of  [22], i.e., the sub-array that has already been processed in the loop encoded by the CHC, and the sub-array that remains to be processed. The former restricts the range of $\psi _2$ (lines 10,  14) and the latter of $\psi _1$ (lines 9,  13). More formally:

Definition 11

For an inductive CHC C with loop counter i, where i is in the interval [l, u], and a free variable j, the range formula is $j < i$ when $i \ge l$ is inductive at C, and $j > i$ when $i \le u$ is inductive at C.

In Algorithm 2, $\sigma$ is the range formula returned by ComputeRangeFormula. Additionally, GetCondition adds predicates that are present in the constraint of the CHC (like $2*i < N$) after substituting the loop counters in them by the quantified variables.

Existentially-quantified formulas (9) Similar to the universally-quantified case, the abduction query (11) for existential quantification will be decomposed into two abduction queries. Queries (12) and (13) in this case have the form:

$$\begin{aligned} \psi _1 \wedge \big [(b'[i]= f({\vec {v}}, {\vec {t}}) \wedge )^{*}\big ] \!\ldots \! &\implies (R( i, {\vec {v}}) \wedge Q( i, {\vec {v}}, {\vec {a}}))\\ \psi _2\wedge \big [(b'[i]=b[i]\wedge )^{*}\big ]\!\ldots \!&\implies (R( i, {\vec {v}}) \wedge Q( i, {\vec {v}}, {\vec {a}})) \end{aligned}$$

The remainder of the algorithm in this case is the same as in the universally-quantified case with the exception that we disjoin two quantified solutions for the abduction queries before checking if it is inductive.

6.3 Houdini Algorithm

The strengthening performed by Algorithm 2 might result in a too strong candidate invariant for already validated CHCs. To resolve this, Algorithm 1 weakens the candidate invariants by using an existing algorithm called Houdini [24](line 7). Given a set of relations R and a map** $\mathcal {M}$, Houdini recursively weakens $\mathcal {M}$ until it is inductive at each CHC C whose $rel ( head (C)) \in R$. It does this by finding a counterexample to inductiveness and drop** the conjuncts that don’t satisfy the counterexample.

6.4 Illustration of Existentially Quantified Precondition Inference

We end this section by illustrating Algorithm 1 on an existentially quantified postcondition from Fig. 4. The CHCs of this program are given in Fig. 5.

Fig. 5.

CHC encoding of program in Fig. 4.

The algorithm chooses an initial candidate for $\boldsymbol{inv}$ from the query. The loop condition is dropped like universal quantification, but the range formula is not conjuncted for existential postcondition as this often results in a too strong precondition, viz. $\bot$.

Algorithm 1 now checks if either the second or third CHC in the Worklist is not inductive. Since the third CHC is not inductive, Abduce is called. The result of two abduction queries corresponding to i-th element and non i-th element, i.e. $\psi _1$ and $\psi _2$, will be $B[j]\! \ne \! C[j]$ and $A[j]\! \ne \! B[j]$, respectively. Further, quantification and range formulas are added, which will result in the candidate:

Now, the Houdini algorithm finds that the candidate is not inductive at the third CHC. For instance, it finds a counterexample to validity of the form:

$$\begin{aligned} a[j] \ne b[j] \; \text {for}\; j = i \; \text {, otherwise}\; a[j] = b[j] \\b[j] \ne c[j] \; \text {for}\; j = i+2 \; \text {, otherwise} \; b[j] = c[j] \end{aligned}$$

It drops the conjunct $\exists j .\,0\!\le \! j\! <\! N\wedge A[j]\! \ne \! B[j]$ that does not satisfy the counterexample. The rest are found to be inductive at the third and second CHCs.

$$\begin{aligned} \boldsymbol{inv}\mapsto \lambda i,\!N,\!A,\!B,\!C .\,&\exists j .\,0\!\le \! j\! <\! N\wedge j \ge i \wedge 2*j \ge N \wedge B[j]\! \ne \! C[j] \vee \\&\exists j .\,0\!\le \! j\! <\! N\wedge j < i \wedge 2*j \ge N \wedge A[j]\! \ne \! B[j] \end{aligned}$$

Finally, the precondition $\boldsymbol{cpre}$ is computed from the first CHC by substituting $i=0$, resulting in:

$$\begin{aligned} \boldsymbol{cpre}\mapsto \lambda i,\!N,\!A,\!B,\!C .\,\exists j .\,0\!\le \! j\! <\! N\wedge 2*j \ge N \wedge B[j]\! \ne \! C[j] \end{aligned}$$

7 Maximal Preconditions

The interpretation of $\boldsymbol{pre}$ generated by Algorithm 1 is guaranteed to be a precondition by Theorem 2, but it could be non-maximal. That is, it may exclude some initial states from which the postcondition holds. In this section, we propose a technique that checks whether a precondition is maximal (i.e. logically weakest). If not, it incrementally weakens the precondition in a loop until it becomes maximal.

7.1 Overview

Algorithm 3 gives a description of the maximality checker. Given a precondition inference problem via a system of CHCs S, it returns a maximal precondition on termination. It first generates a precondition for S using Algorithm 1. In order to check whether the precondition is maximal, the algorithm infers another precondition for the complement CHC system $\overline{S}$ (line 2). Recall from Definition 5 that this system has the same structure as S except the postcondition in the query is complemented. To avoid confusion, we consider $\boldsymbol{pre}$ of this system is substituted by another uninterpreted relation with the same arity $\boldsymbol{cpre}$. For example, Fig 5 is the complement CHC system of Fig 3.

The maximality check is performed next by checking whether all the states that are outside $\mathcal {M}(\boldsymbol{pre})$ are in $\overline{\mathcal {M}}(\boldsymbol{cpre})$(line 4). Intuitively, if all the states in $\lnot \mathcal {M}(\boldsymbol{pre})$ are in $\overline{\mathcal {M}}(\boldsymbol{cpre})$ then those states violate the postcondition as $\overline{\mathcal {M}}(\boldsymbol{cpre})$ is the precondition of the complement postcondition. The validity check is reduced to a satisfiability check by negation and the model to the satisfiability check is called a counterexample-to-maximality, or CTM.

The algorithm uses the CTM to determine which of $\boldsymbol{pre}$ or $\boldsymbol{cpre}$ has to be weakened by invoking the method UnrollCHC (line 6). Intuitively, UnrollCHC performs a task similar to executing the program represented by CHCs with CTM as the initial state. More precisely, UnrollCHC will find unrollings (Definition 7) of different lengths for the extensions $S_{ctm}$ and $\overline{S}_{ctm}$ and terminates when an unrolling is satisfiable. It then returns whether the unrolling was from $S_{ctm}$, or $\overline{S}_{ctm}$. For a deterministic CHC system (Definition 8), a satisfiable unrolling exists either for $S_{ctm}$, or $\overline{S}_{ctm}$.

In the next step, the algorithm will weaken $\boldsymbol{cpre}$ if the unrolling is from $S_{ctm}$, or $\boldsymbol{pre}$ if the unrolling is from $\overline{S}_{ctm}$. The weakening is performed by Weaken, which will be called with an appropriate CHC system and the current interpretation for the precondition(lines 10, 8). Weaken will generalize the precondition and find inductive invariants. This loop of checking for CTM and weakening one of the precondition continues till the maximal precondition is found.

Theorem 3

The precondition returned by Algorithm 3, when it terminates, is maximal when S is deterministic and terminating.

Example 3

In Sect 5.2 and Sect 6.4, Algorithm 1 found the following interpretations for $\boldsymbol{pre}$ and $\boldsymbol{cpre}$:

$$\begin{aligned} \boldsymbol{pre}\mapsto \lambda N,A,B,C.\,\forall j .\,0\!\le \! j\! <\! N\wedge 2*j < N \!\!&\implies \!\! A[j]\! =\! B[j] \wedge \\\forall j .\,0\!\le \! j\! <\! N\wedge 2*j \ge N \!\!&\implies \!\! B[j]\! =\! C[j]. \end{aligned}$$

$$\begin{aligned} \boldsymbol{cpre}\mapsto \lambda i,\!N,\!A,\!B,\!C .\,\exists j .\,0\!\le \! j\! <\! N\wedge 2*j \ge N \wedge B[j]\! \ne \! C[j]. \end{aligned}$$

The reader may notice that $\boldsymbol{cpre}$ is not maximal, hence it is not possible to check whether $\boldsymbol{pre}$ is maximal. We now illustrate how Algorithm 3 determines this.

After finding the interpretations, Algorithm 3 checks the following formula:

$$\begin{aligned} \lnot (\forall j .\,0\!\le \! j\! <\! N\! \wedge 2*j\! <\! N\!\!\implies \!\! A[j]\! =\! B[j]\! &\wedge \! \forall j .\,0\!\le \! j\! <\! N\! \wedge 2*j\! \ge \!N\!\!\implies \!\! B[j]\! =\! C[j]\!)\\ &\implies \\ \exists j .\,0\!\le \! j\! <\! N\! \wedge 2*j\! \ge \!N&\!\!\implies \!\! B[j]\! \ne \! C[j]\!\\ \end{aligned}$$

Since this formula is satisfiable, the algorithm deduces that at least one among $\mathcal {M}(\boldsymbol{pre})$ and $\mathcal {M}_c(\boldsymbol{cpre})$ is not maximal. Suppose it gets the following satisfiability model, or CTM:

$$N=1 \wedge A[0] = 0 \wedge B[0] = 1 \wedge C[0] = 0.$$

$\textsc {UnrollCHC}$ finds that the CHCs violate the property when the CTM is the initial state. Hence, $\boldsymbol{cpre}$, the precondition of negation of the property, can be weakened by at least one point, viz. CTM.

7.2 Weakening of Precondition

Once the precondition that has to be weakened is determined, a trivial weakening is to add the CTM to the current interpretation. However, this may cause non-termination as there can be infinitely many CTMs. In this section, we propose a heuristic in Algorithm 4 that can accelerate the weakening process.

Algorithm 4 works in two stages. First, it finds a formula $\varphi$ that is generally weaker than the trivial solution $\mathcal {M}(\boldsymbol{pre}) \vee ctm$ (lines 3- 5). To do this, it enumerates (line 3) a formula $\sigma$ from an input grammar G (a sample grammar is given in [49]) and then checks if it is weaker. Then, it finds inductive invariants $\mathcal {M}'$ (line 7) for the extended system $S_\varphi$ (recall Definition 6) using a slightly modified version of range abduction (algorithmic description is in [49]). By Lemma 2, $\varphi$ and $\mathcal {M}'$ together forms a solution to the input system S.

Theorem 4

Algorithm 4 returns a solution $\mathcal {M}'$ to S, and $\mathcal {M}(\boldsymbol{pre}) \vee ctm \implies \mathcal {M}'(\boldsymbol{pre})$

Example 4

We continue illustration of Example 3. Algorithm 4 is called with a complement CHC system (Fig 5) and $\mathcal {M}(\boldsymbol{cpre})\mapsto \lambda i,\!N,\!A,\!B,\!C .\,\exists j .\,0\!\le \! j\! <\! N\wedge 2*j \ge N \wedge B[j]\! \ne \! C[j]$ and $ctm = N=1 \wedge A[0] = 0 \wedge B[0] = 1 \wedge C[j] = 0$. Suppose that the algorithm samples $\sigma$ as $\exists j .\,0\!\le \! j\! <\! N\wedge 2*j < N \wedge A[j]\! \ne \! B[j]$ based on the constraints from query and second CHC. Since the check at line 4 passes, $\varphi$ will be assigned:

$$\exists j .\,0\!\le \! j\! <\! N\wedge 2*j \ge N \wedge B[j]\! \ne \! C[j] \vee \exists j .\,0\!\le \! j\! <\! N\wedge 2*j < N \wedge A[j]\! \ne \! B[j].$$

InvInfer uses the postcondition to compute $\mathcal {M}[{r}_{i+1}]$ and $\sigma$ to compute $\mathcal {M}[{r}_{i-1}]$. It then adds $j < i$ to the former, $j \ge i$ to the latter, and disjuncts them (due to existential quantification) to get:

$$\begin{aligned} \boldsymbol{inv}\mapsto \lambda i,\!N,\!A,\!B,\!C .\,&\exists j .\,0 \le j < i \wedge A[j]\! \ne \! B[j] \vee \\&\exists j .\,i \le j < N \wedge 2*j \ge N \wedge B[j]\! \ne \! C[j] \vee \\&\exists j .\,i \le j < N \wedge 2*j < N \wedge A[j]\! \ne \! B[j] \end{aligned}$$

Since this is inductive at all CHCs, the algorithm returns with $\varphi$ and $\boldsymbol{inv}$. Algorithm 3 will perform its check and finds that $\boldsymbol{pre}$ is maximal.

8 Evaluation

Tool We implemented our algorithms in a tool called PreQSyn on top of the FreqHorn framework [22]. Our tool takes as input a precondition-inference problem encoded as a set of CHCs. It uses Z3 [44] to solve SMT queries. Quantifier elimination is performed using the solver from [20] that uses model-based projection [5]. On a successful execution, our tool infers maximal preconditions and inductive invariants for the loops.

Evaluation Goals We evaluate PreQSyn on the following research questions:

• RQ1 Can PreQSyn infer universal and existential preconditions? How many of them can it prove maximal?

• RQ2 Can PreQSyn compete with existing maximal quantified precondition inference tools?

• RQ3 How challenging for state-of-the-art is to infer invariants with preconditions?

• RQ4 How do various modules of PreQSyn influence its performance?

Benchmarks and Configuration We use 32 precondition inference problems with 29 universal and 3 existential quantified postconditions. Since none of the benchmarks from [54] had quantified postconditions, we derived a majority (26/32) of benchmarks from the existing verification benchmarks of [22] that have been collected from various sources like SV-COMP. In particular, we considered 48 benchmarks from the public repository of [22] that have multiple loops, i.e., the first loop has an array initialization, and the other loops involve various types of array processing like copying, modifying, filtering, and searching among the elements. We then excluded the first (initialization) loop from each benchmark, thus targeting the necessity of synthesizing a quantified precondition that would intuitively describe how the arrays need to be initialized in order to meet the postcondition. We further excluded benchmarks that gave repetitive problems (8/48) and did not meet our syntactic restrictions (viz. had non-quantified postconditions (6/48), had nested loops (5/48), or had non-linear expressions (3/48)). We added 6 new benchmarks to test different features of our tool.

We performed the experiments on an Ubuntu 20.04 machine with a 2.5 GHz processor and 16 GB memory. A timeout of 100s was given to all the tools.

RQ1 PreQSyn inferred a precondition for 31/32 benchmarks. The failed benchmark timed out in the inductiveness check. Out of 31 preconditions, 22 were proved to be maximal automatically. All the successful benchmarks were completed within 5 seconds. Overall, PreQSyn solved CHC tasks numbering 31 with universally quantified and 30 existentially quantified postconditions corresponding to $\boldsymbol{pre}$ and $\boldsymbol{cpre}$.

On manual inspection of 9 benchmarks for which PreQSyn found a precondition but was unable to prove maximality, 5 were found to be non-deterministic. However, the inferred preconditions for them were sufficiently weak. The rest 4 failed in different stages of weakening $\boldsymbol{cpre}$. Among these benchmarks, we found that 3/4 preconditions (i.e. $\boldsymbol{pre}$) were actually maximal.⁶

RQ2 We ran P-Gen (with Z3 v2.0 as its SMT solver) on semantically equivalent C programs manually constructed from the CHCs. P-Gen found only 2/32 preconditions as maximal. Both of them were existentially quantified. It timed out on 5/32 benchmarks. On the remaining 25/32 benchmarks it exited without finding a precondition. Overall, PreQSyn inferred significantly more preconditions than P-Gen due to the generalization capability of range abduction.

RQ3 We tried to replace our invariant inference technique by an existing one, thus evaluating the need to discover our invariants. Existing state-of-the-art CHC solving tools can handle arrays, to some extent, namely: Spacer  [32](Z3 v4.8.10), a PDR-based invariant inference tool, and FreqHorn  [22] (v.0.6), a SyGuS based invariant inference tool. So we pose the simpler problem of inferring invariants with preconditions to them. Furthermore, we also pose this as an assertion checking problem to VeriAbs  [15] (v1.4.2), a portfolio solver that targets linear loops and the gold winner of SV-COMP 2022 ReachSafety Category [4] and the winner of array category since several years.

To create invariant inference and verification problems, we consider 42 precondition inference problems corresponding to $\boldsymbol{pre}$ and $\boldsymbol{cpre}$ for which PreQSyn was able to find the maximal preconditions. The 42 precondition inference problems were converted manually to verification problems by using the maximal preconditions. For Spacer, the CHCs were annotated by the maximal interpretations of $\boldsymbol{pre}$ and $\boldsymbol{cpre}$, for VeriAbs, semantically equivalent C programs with maximal preconditions as loops, and for FreqHorn original CHCs were provided as input.

Out of 42 problems, 21 each of universally and existentially quantified postconditions, VeriAbs solved 37, FreqHorn solved 20, and Spacer solved 11.

RQ4 We disabled Houdini algorithm from line 7 of Algorithm 1 and PreQSyn found preconditions for 27 benchmarks compared to 31 with the range abduction algorithm. Out of 27, only 6 were proved maximal. We conclude that weakening by Houdini is useful, especially when postconditions are existentially quantified. We extended the SMT-based maximality checking algorithm from [50], but it was unsuccessful in proving the 21 problems that our maximality checker proved.

9 Related Work

The problem of precondition inference appears in multiple applications and has been the subject of numerous works. Broadly, these works can be classified as static [13, 14, 45, 54], dynamic [3, 25, 41, 53], and a mix of both [46]. Our technique falls in the first category. The two works closest to ours are [14] and [54] which compute maximal quantified preconditions for array programs, using abstract interpretation and CEGAR-based predicate abstraction, respectively. Unlike the technique in [14], our work does not require predefined abstract domains. The technique in  [54] computes over-approximations of safe and unsafe states (i.e. over-approximations of $\boldsymbol{pre}$ and $\boldsymbol{cpre}$) and then refines them till they become disjoint. The over-approximations are computed using predicate abstraction and the predicates required for the refinement of the abstraction are derived from a set of heuristic rules. Our technique differs from theirs in several ways: we rely on abduction-based techniques to infer necessary predicates, while they rely on minimal unsat cores; we infer quantified inductive invariants that witness the correctness of the inferred preconditions, while their technique does not; finally, we target quantified postconditions while they consider only quantifier-free postconditions.

The problem of inferring universally quantified inductive invariants has received considerable attention. The inference is made using methods such as abstract interpretation [30], predicate abstraction using Skolem constants [40] and interpolation [34], an extension of IC3 for arrays [32], and syntax-guided synthesis [22]. These techniques, apart from being restricted to universal quantification, also expect a precondition. Our technique overcomes these limitations by inferring preconditions including existentially quantified ones.

Many techniques verify programs with arrays by transforming them to a sound abstraction without explicitly generating inductive invariants. The abstraction can be obtained by considering all the array elements as a single cell [7], or multiple fixed cells and then converting to array-free nonlinear CHCs [43], overapproximating unknown loop bounds to a smaller known bound [39], accelerating entire transition relations [8], using CHC transformations [6, 35] and induction based techniques [9,10,11]. The portfolio solver VeriAbs  [1] used in our experiment predominantly used the shrinking  [39] technique to verify, which does not generate invariants. The tool also has induction-based techniques  [9,10,11] that implicitly generate invariants, but are not given to the user. RAPID  [26] translates the semantics of the input program into formulas in trace logic. Then the formulas are verified using a theorem prover. Though sound lemmas are used to translate loops, it currently does not support the extraction of invariants from the lemmas. Apart from the inability to generate explicit invariants, all of these techniques need preconditions to verify the programs.

Our technique works on CHCs, which has gained much attention in recent years for different verification and inference tasks  [19, 21, 22, 32, 36, 50, 51, 57]. Most of these techniques do not handle arrays, and when they do, do not generate maximal preconditions.

The core part of our algorithm uses abductive inference. Abduction has been used for programs without arrays to infer invariants [17, 18], preconditions [16, 27], and specifications [2, 50]. The technique in  [56] finds specification over uninterpreted functions by overcoming the limitation of integer abduction engines through a data-driven approach. In contrast, our technique extends the abduction itself for quantified formulas over arrays.

Recent works in specification synthesis uses artifacts like input-output examples, comments in the code, partial code snippets, and user-supplied constraints and languages to infer specifications [12, 47, 55]. In comparison, our work uses the entire program and postcondition expressed as a logical formula to find maximal preconditions.

10 Limitations and Future Work

The restriction on array access statements simplifies the conversion between array and integer terms in range abduction. However, this can be relaxed to support terms like a[b[i]], $a[i+1]$ among others, by enhancing the select-substitution (recall Def 10).

The restriction on form of postconditions, inductive invariants and preconditions is required for effective range abduction and SMT checks. Our approach can easily support alternating quantifiers, if the structure of the postcondition is close to the inductive invariant.

For non-deterministic programs, Algorithm 4 will not terminate when a CTM has two satisfiable unrollings: $\pi$ and $\overline{\pi }$ (refer Definition 8). Hence, the maximality check will be inconclusive. Nevertheless, Algorithm 1 can still generate preconditions (with inductive invariants) for such programs, often maximal ones as observed in our experiments. We extend our approach to non-deterministic CHCs in  [48].

In the case of non-terminating programs, an initial state with non-terminating execution can be added to either $\boldsymbol{pre}$ or $\boldsymbol{cpre}$, as it will have inductive invariants for both. If added to the latter, the maximality check could wrongly conclude that $\boldsymbol{pre}$ is maximal when it’s not. Therefore, relaxing this restriction affects the soundness of the maximality check. An interesting future direction for maximality checking would be to extend the work presented in [29] to incorporate array handling.

11 Data Availability and Artifact

The artifact accompanying the paper is publicly available at  [52].