Polynomial Invariants by Linear Algebra

Abstract

We present in this paper a new technique for generating polynomial invariants, divided in two independent parts: a procedure that reduces polynomial assignments composed loops analysis to linear loops under certain hypotheses and a procedure for generating inductive invariants for linear loops. Both of these techniques have a polynomial complexity for a bounded number of variables and we guarantee the completeness of the technique for a bounded degree which we successfully implemented for C programs verification.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

When dealing with computer programming, anyone should be aware of the underlying behavior of the whole code, especially when it comes to life-critical projects composed of million of lines of code [11]. Manual code review cannot scale to the size of actual embedded programs. Testing allows to detect many vulnerabilities but it is never enough to certify their total absence. Indeed, the cost of generating and executing sufficient test cases to meet the most stringent coverage criteria [4] that are expected for critical software becomes quickly prohibitive as the size of the code under test grows. Alternatively, formal methods techniques based on abstraction allow us to prove the absence of error.

However, since a program can, at least in theory, have an infinite number of different behaviors, the verification problem is undecidable and these techniques either lose precision (emitting false alarms) and/or require manual input. One of the main issue of such approach is the analysis of loops, considered as a major research problem since the 70 s [2]. Program verification based on Floyd-Hoare’s inductive assertion [10] and CEGAR-like techniques [7] for model-checking uses loop invariants in order to reduce the problem to an acyclic graph analysis [3] instead of unrolling or accelerating loops [12]. Thus, a lot or research nowadays is focused on the automatic inference of loop invariants [17, 22].

We present in this paper a new technique for generating polynomial invariants, divided in two independent parts: a linearization procedure that reduces the analysis of solvable loops, defined in [22], to the analysis of linear loops; an inductive invariant generation procedure for linear loops. Those two techniques are totally independent from each other, we aim to present in this article their composition in order to find polynomial invariants for polynomial loops. We also add an extension of this composition allowing to treat loops with complex behaviors that induces the presence of complex numbers in our calculation. The linearization algorithm has been inspired by a compiler optimisation technique called operator strength reduction [8]. Our invariant generation is completely independent from the initial state of the loop studied and outputs parametrized invariants, which is very effective on programs using a loop multiple times and loops for which we have no knowledge of the initial state. In addition to being complete for a certain class of polynomial relations, the invariant generation technique has the advantage to be faster than the already existing one for such loops as it relies on polynomial complexity linear algebra algorithms.

Furthermore, a tool implementing this method has been developped in the Frama-C framework for C programs verification [15] as a new plug-in called Pilat (standing for Polynomial Invariants by Linear Algebra Tool). We then compared our performances with Aligator  [17] and Fastind  [5], two invariant generators working on similar kinds of loops. First experiments over a representative benchmark exposed great improvements in term of computation time.

Outline. The rest of this paper is structured as follows. Section 2 introduces the theoretical concepts used all along the article and the kind of programs we focus on. Section 3 presents the application of our technique on a simple example. Section 4.1 presents the linearization step for simplifying the loop, reducing the problem to the study of affine loops. Section 4.2 presents our contribution for generating all polynomial invariants of affine loops. Section 4.3 extends the method with the treatment of invariants containing non-rational expressions. Finally, Sect. 5 compares Pilat to Aligator and Fastind. Due to space constraints, proofs have been omitted. They are available in a separate report [9].

State of the Art. Several methods have been proposed to generate invariants for kinds of loops that are similar to the ones we address in this paper. In particular, the weakest precondition calculus of polynomial properties in [20] is based on the computation of the affine transformation kernel done by the program. This method is based on the computation of the kernel of the affine transformation described by the program. More than requiring the whole program to be affine, this method relies on the fact that once in the program there exists a non-invertible assignment, otherwise the kernel is empty. This assumption is valuable in practice, as a constant initialization is non- invertible, so the results may appear at the end of a whole-program analysis and highly depend on the initial state of the program. On the other hand, our method can generate parametrized invariants, computable without any knowledge of the initial state of a loop, making it more amenable to modular verification.

From a constant propagation technique in [19] to a complete invariant generation in [22], Gröbner bases have proven to be an effective way to handle polynomial invariant generation. Such approaches have been successfully implemented in the tool Aligator  [17]. This tool generates all polynomial invariants of any degree from a succession of p-solvable polynomial mappings in very few steps. It relies on the iterative computation of Gröbner bases of some polynomial ideals, which is a complicated problem proven to be EXPSPACE-complete [18].

Attempts to get rid of Gröbner bases as in [5] using abstract interpretation with a constant-based instead of a iterative-based technique accelerates the computation of invariants by generating abstract loop invariants. However, this technique is incomplete and misses some invariants. The method we propose here is complete for a particular set of loops defined in [22] in the sense that it finds all polynomial relations P of a given degree verifying $P(X) = 0$ at every step of the loop, and has a polynomial complexity in the degree of the invariants seeked for a given number of variables.

2 Preliminaries

Mathematical Background. Given a field $\mathbb {K}$, $\mathbb {K}^n$ is the vector space of dimension n composed by vectors with n coefficients in $\mathbb {K}$. Given a family of vector $\varPhi \subset \mathbb {K}^n$, $Vect(\varPhi )$ is the vector space generated by $\varPhi$. Elements of $\mathbb {K}^n$ are denoted $x = (x_1,...,x_n)^t$ a column vector. $\mathcal {M}_n(\mathbb {K})$ is the set of matrices of size $n*n$ and $\mathbb {K}[X]$ is the set of polynomials using variables with coefficients in $\mathbb {K}$. We note $\overline{\mathbb {K}}$ the algebraic closure of $\mathbb {K}$, $\overline{\mathbb {K}}= \{x | \exists P \in \mathbb {K}[X], P(x) = 0\}$. We will use $\langle .,.\rangle$ the linear algebra standard notation, $\langle x,y\rangle = x\cdot y^t$, with $\cdot$ the standard dot product. The kernel of a matrix $A \in \mathcal {M}_n(\mathbb {K})$, denoted $\ker (A)$, is the vector space defined as $\ker (A) = \left\{ x | x \in \mathbb {K}^n, A.x = 0\right\}$. Every matrix of $\mathcal {M}_n(\mathbb {K})$ admits a finite set of eigenvalues $\lambda \in \overline{\mathbb {K}}$ and their associated eigenspaces $E_\lambda$, defined as $E_\lambda = \ker (A - \lambda Id)$, where Id is the identity matrix and $E_\lambda \ne \{ 0\}$. Let E be a $\mathbb {K}$ vector space, $F \subset E$ a sub vector space of E and x an element of F. A vector y is orthogonal to x if $\langle x,y\rangle = 0$. We denote $F^\perp$ the set of vectors orthogonal to every element of F.

Programming Model. We use a basic programming language whose syntax is given in Fig. 1. $Var$ is a set of variables that can be used by a program, and which is supposed to have a total order. Variables take value in a field $\mathbb {K}$. A program state is then a partial mapping $Var \rightharpoonup \mathbb {K}$. Any given program only uses a finite number n of variables. Thus, program states can be represented as a vector $X = (x_1,...,x_n)^t$. In addition, we will note $X' = (x'_1,...,x'_n)^t$ the program state after an assignment. Finally, we assume that for all programs, there exists $x_{n+1} = x'_{n+1} = \mathbbm {1}$ a constant variable always equal to 1.

• The i OR i instruction refers to a non-deterministic condition.

• Each i will be refered to as one of the bodies of the loop.

Multiple variables assignments occur simultaneously within a single instruction. We say that an instruction is affine when it is an assignment for which the right values are affine. If not, we divide instructions in two categories with respect to the following definition, from [22].

Fig. 1.

Code syntax

Definition 1

Let $g\in \mathbb {Q}[X]^m$ be a polynomial mapping. g is solvable if there exists a partition of X into subvectors of variables $x = w_1\uplus ...\uplus w_k$ such that $\forall j,~1\leqslant j \leqslant k$ we have

$$\begin{aligned} g_{w_j}(x) = M_jw_j^T + P_j(w_1,...,w_{j-1}) \end{aligned}$$

with $(M_i)_{1 \leqslant i \leqslant k}$ a matrix family and $(P_i)_{1 \leqslant i \leqslant k}$ a family of polynomial mapping.

An instruction is solvable if the associated assignment is a solvable polynomial mapping. Otherwise, it is unsolvable. Our technique focuses on loops containing only solvable instructions, thus it is not possible to generate invariants for nested loops. It is however possible to find an invariant for a loop containing no inner loop even if it is itself inside a loop, that’s why we allow the construction.

3 Overview of Our Approach

Steps of the Generation. In order to explain our method we will take the following running example, for which we want to compute all invariants of degree 3:

Our method is based on two distinct parts:

• 1. reduction of the polynomial loop to a linear loop;

• 2. linear invariant generation from the linearized loop.

We want to find a linear mapping f that simulates the behavior of the polynomial mapping $P(x,y) = (x + y^2, y + 1)$. To achieve this, we will express the value of every monomial of degree 2 or more using brand new variables. Here, the problem comes from the $y^2$ monomial. In [20], it is described how to consider the evolution of higher degree monomials as affine applications of lower or equal degree monomials when the variables involved in those monomials evolve affinely. We extend this method to express monomials transformations of the loop by affine transformations, reducing the problem to a simpler loop analysis. For example here, $y' = y+1$ is an affine assignment, so there exists an affine representation of $y_2 = y^2$, which is $y_2' = y_2 + 2.y + 1$. Assuming the initial $y_2$ is correct, we are sure to express the value of $y^2$ with the variable $y_2$. Also, if we want to find invariants of degree 3, we will need to express all monomials of degree 3, i.e. xy and $y_3$ the same way. (monomials containing $x^i$ with $i \geqslant 2$ are irrelevant as their expression require the expression of degree 4 monomials). Applying this method to P gives us the linear mapping $f(x,y,y_2,xy,y_3, \mathbbm {1}) = (x + y_2, y + \mathbbm {1}, y_2 + 2.y + \mathbbm {1},xy + x + y_2 + y_3,y_3 + 3.y_2 + 3.y + \mathbbm {1},\mathbbm {1})$, with $\mathbbm {1}$ the constant variable mentioned in the previous section.

Now comes the second part of the algorithm, the invariant generation. Informally, an invariant for a loop is a formula that

• 1. is valid at the beginning of the loop;

• 2. stays valid after every loop step.

We are interested in finding semi-invariants complying only with the second criterion such that they can be expressed as a linear equation over X, containing the assignment’s original variables and the new ones generated by the linearization procedure. In this setting, a formula satisfying the second criterion is then a vector of coefficients $\varphi$ such that

$$\begin{aligned} \langle \varphi ,X\rangle = 0 \Rightarrow \langle \varphi ,f(X)\rangle = 0 \end{aligned}$$

(1)

By linear algebra, the following is always true

$$\begin{aligned} \langle \varphi ,f(X)\rangle = \langle f^*(\varphi ),X\rangle \end{aligned}$$

(2)

where $f^*$ is the dual of f. If $\varphi$ happens to be an eigenvector of $f^*$ (i.e. there exists $\lambda$ such that $f^*(\varphi ) = \lambda \varphi )$, the Eq. (1) becomes

$$\begin{aligned} \langle \varphi ,X\rangle = 0\Rightarrow & {} \langle f^*(\varphi ),X\rangle = 0\mathrm {~by~(2)}\\ \langle \varphi ,X\rangle = 0\Rightarrow & {} \langle \lambda .\varphi ,X\rangle = 0\\ \langle \varphi ,X\rangle = 0\Rightarrow & {} \lambda .\langle \varphi ,X\rangle = 0 \end{aligned}$$

which is always true. We just need to transpose the matrix representing f to compute $f^*$ . It returns $f^*(x,y,y_2,y_3,\mathbbm {1}) = (x,y + y_2 + y_3, x + y_2 + 3.y_3,y_3,y + y_2 + y_3 + \mathbbm {1},y + y_2 + y_3 + \mathbbm {1})$. $f^*$ only admits the eigenvalue 1. The eigenspace of $f^*$ associated to 1 is generated by two independants vectors, $e_1 = (-6,1,-3,2,0)^t$ and $e_2 = (0,0,0,0,1)^t$. Eventually, we get the formula $F_{k1,k2} = (k_1.(-6.x + y -3.y_2 + 2.y_3) + k_2.\mathbbm {1} = 0)$ as invariant, with $k_1,k_2 \in \mathbb {Q}$. By writing $k = -\frac{k_2}{k_1}$ and replacing $\mathbbm {1}$ with 1, we can rewrite it with only one parameter, $F_k = (-6.x + y -3.y_2 + 2y_3 = k)$. In this case, information on the initial state of the loop allows to fix the value of the parameter k. For example if the loop starts with $(x = 0, y = 0)$, then $-6.x + y -3.y^2 + 2.y^3 = 0$, and $F_0$ is an invariant. The next section will show how the work done on our example can be generalized on any (solvable) loop. In particular, Sect. 4.1 will deal with the linearization of polynomial assignments. Then we will see in Sect. 4.2 that the eigenspace of the application actually represents all the possible invariants of f and that we can always reduce them to find a formula with only one parameter.

Extension of the Basic Method. The application’s eigenvector may not always be rational. For example, applying the previous technique on a mapping such as $f(x,y) = (y, 2.x)$ will give us invariants with coefficients involving $\sqrt{2}$. Dealing with irrational and/or complex values raises some issues in our current implementation setting. Therefore, we propose in Sect. 4.3 a solution to stick with rational numbers. Eventually, we treat the case when a condition occur in loops in Sect. 4.4.

4 Automated Generation of Loop Invariants

4.1 Strength Reduction of Polynomial Loops

Lowerization. Let P be a program containing a single loop with a single solvable assignment $X {:}= g(X)$. In order to reduce the invariant generation problem for solvable polynomial loops to the one for affine loops, we need to find a linear mapping f that perfectly matches g. As shown in Fig. 2, the first loop L1 is polynomial but there exists a similar affine loop, namely L2, computing the same vector of values plus and thanks to an extra variable xy.

Fig. 2.

Polynomial and affine loop having the same behavior

Definition 2

Let g be a polynomial mapping of degree d using m variables. g is linearizable if there exists a linear mapping f such that $X' = g(X) \Rightarrow (X',P(X')) = f(X,P(X))$, where $P : \mathbb {Q}^m \rightarrow \mathbb {Q}^n$ is a polynomial of degree d.

By considering polynomials as entries of the application, we are able to consider the evolution of the polynomial value instead of recomputing it for every loop step. This is the case in the previous example, where the computation of xy as $x * y$ is made once at the beginning of the loop. Afterwards, its evolution depends linearly of itself, x and y. Similarly, if we want to consider $y^n$ for some $n\ge 2$, we would just need to express the evolution of $y^n$ by a linear combination of itself and lower degree monomials, which could themselves be expressed as linear combinations of lower degree monomials, until we reach an affine application. We call this process the polynomial mappings lowerization or linearization.

Remark. This example and our running example have the good property to be linearizable. However, this property is not true for all polynomials loops. Consider for example the mapping $f(x) = x^2$. Trying to express $x^2$ as a linear variable will force us to consider the monomials $x^4$, $x^8$ and so on. Thus, we need to restrain our study to mappings that do not polynomially transform a variable itself. This class of polynomials corresponds to solvable polynomial mappings, defined in Definition 1.

Property 1

For every solvable polynomial mapping g, g is linearizable.

For example, let $g(x,y) = (x + y^2,y+1)$. g is linearized by $f(x,y,y_2) = (x+y_2,y+1,y_2 + 2y + 1)$. Indeed with $(x',y') = g(x,y)$, we have $(x',y',y'^2 ) = f(x,y,y^2)$

Linearization Algorithm. The algorithm is divided in two parts: the solvability verification of the mapping and, if successful, the linearization process. The solvability verification consists in finding an appropriate partitioning of the variables that respects the solvable constraint. It is nothing more than checking that a variable v cannot be in a polynomial (i.e. non linear) assignment of another variable that itself depend on v. This check can be reduced to verifying the acyclicity of a graph, which can be computed e.g. by Tarjan’s [23] or Johnson’s [13] algorithms.

The linearization process then consists in considering all monomials as new variables, then finding their linear evolution by replacing each of their variables by the transformation made by the initial application. This may create new monomials, for which we similarly create new variables until all necessary monomials have been mapped to a variable. Since we tested the solvability of the loop, the variable creation process will eventually stop. Indeed, if this was not the case, this would mean that a variable x transitively depends on $x^d$ with $d > 1$.

Elevation. We saw how to transform a polynomial application into a linear mapping by adding extra variables representing the successive products and powers of every variable. This information can be useful in order to generate invariants but in fact, most of the time, this is not enough. In our running example of Sect. 2, $g(x,y) = (x + y^2, y + 1)$, the degree of the mapping is 2 but there exists no invariant of degree 2 for this loop. In order to deal with higher-degree invariants, we need not just to linearize g, we also have to add more variables to our study. As we can represent monomials of variables of a solvable mapping as linear applications, we can extend the method to generate higher degree monomials such as $y^3$ for example : we elevate g to a higher degree. The process of elevation is described in [20] as a way to express polynomial relations on a linear program.

Property 2

Every solvable polynomial mapping g using n variables is linearizable by a linear mapping f using at most ${n+d \atopwithdelims ()d}$ new variables, where d is the degree of P, the polynomial linearizing g as in Definition 2.

Note. The complexity of the transformation is polynomial for d or n fixed. The lowerization algorithm can be used as shown above by adding variables computing the high degree monomials we want to linearize. Moreover, $n+d \atopwithdelims ()d$ is an upper bound and in practice, we usually need much less variables. For instance, in our running example, we don’t need to consider $x.y^2$. Indeed, if we tried to linearize this monomial, we would end up with $x.y^2 = x.y^2 + x.y + x + y^4 + 2y^3 + y^2$, a polynomial of degree 4. Detecting that a monomial m is relevant or not can be done by computing the degree of its transformation. For example, the assignment of x is a degree 2 polynomial, so $x^2$ associated transformation will be of degree 4. Here, there is actually only two interesting monomials of degree 3, which are xy and $y^3$. Though those variables will be useless for the linearized mapping, they are still easily computable: $y_3' = y_3 + 3.y_2 + 3.y + 1$ and $xy = xy + x + y_2 + y_3$. This limits the necessary variables to only 6 ($x,y,y_2,y_3,xy,\mathbbm {1}$) instead of ${5\atopwithdelims ()2}=10$. This upper bound in only reached for affine transformations when searching for polynomial invariants, as all possible monomials need to be treated.

4.2 Invariant Generation

The transformation described previously doesn’t linearize a whole program, but only a loop. Polynomial assignments must be performed before the loop starts to initialize the new monomials. The method we present only focuses on the loop behavior itself, allowing any kind of operation outside of the loop.

Eigenspace. Loop invariants are logical formulas satisfied at every step of a loop. We can characterize them with two criteria: they have to hold at the beginning of the loop (initialization criterion) and if they hold at one step, then they hold at the next step (heredity criterion). Our technique is based on the discovery of linear combinations of variables that are equal to 0 and satisfying the heredity criterion. For example, the loop of Sect. 3 admits the formula $-6.x + y -3.y_2 + 2y_3 = k$ as a good invariant candidate. Indeed, if we set k in accordance with the values of the variables at the beginning of the loop, then this formula will be true for any step of the loop. We call such formulas semi-invariants.

Definition 3

Let $\varphi : \mathbb {K}^n \mapsto \mathbb {K}$ and $f :\mathbb {K}^n \mapsto \mathbb {K}^n$ two linear mappings. $\varphi$ is a semi-invariant for f iff $\forall X$, $\varphi (X) = 0 \Rightarrow \varphi (f(X)) = 0$.

Definition 4

Let $\varphi : \mathbb {K}^n \mapsto \mathbb {K}$, $f :\mathbb {K}^n \mapsto \mathbb {K}^n$ and $X \in \mathbb {K}^n$. $\varphi$ is an invariant for f with initial state X iff $\varphi (X) = 0$ and $\varphi$ is a semi-invariant for f.

The key point of our technique relies on the fact that if there exists $\lambda , f^*(\varphi ) = \lambda \varphi$, then we know that $\varphi$ is a semi-invariant. Indeed, we can rewrite Definition 3 by $\langle \varphi ,x\rangle = 0 \Rightarrow \langle \varphi ,f(x)\rangle = 0$. By linear algebra, we have $\langle \varphi ,f(x)\rangle = \langle f^*(\varphi ),x\rangle$, with $f^*$ the dual of f. If $\exists \lambda , f^*(\varphi ) = \lambda \varphi$, then we can deduce that $\langle \varphi ,x\rangle = 0 \Rightarrow \lambda \langle \varphi ,x\rangle = 0$. This formula is always true, thus we know that $\varphi$ is a semi-invariant. Such $\varphi$ are commonly called eigenvectors of $f^*$. We will not adress the problem of computing the eigenvectors of an application as this problem have been widely studied (in [21] for example).

Recall our running example $g(x,y) = (x + y^2,y+1)$, linearized by the application $f(x,y,y_2,xy,y_3,\mathbbm {1}) = (x + y_2,y+\mathbbm {1},y_2 + 2y + \mathbbm {1}, xy + x + y_2 + y_3,y_3 + 3y_2 + 3y + \mathbbm {1},\mathbbm {1})$. $f^*$ admits $e_1 = (-6,1,-3,0,2,0)^t$ and $e_2 = (0,0,0,0,0,1)^t$ as eigenvectors associated to the eigenvalue $\lambda = 1$. It means that if $\langle k_1.e_1 + k_2e_2,x\rangle = 0$, then

$$\begin{aligned} \langle k_1.e_1 + k_2e_2,f(X)\rangle= & {} \langle f^*(k_1.e_1 + k_2e_2),X\rangle \\ ~= & {} \langle \lambda (k_1.e_1 + k_2e_2),X\rangle \\ ~= & {} 0 \end{aligned}$$

In other words, $\langle k_1.e_1 + k_2e_2,X\rangle = 0$ is a semi-invariant. Then, by expanding it, we can find that $-6.x + y -3.y_2 + 2y_3 = k$, with $k = -\frac{k_2}{k_1}$ is a semi-invariant. In terms of the original variables, we have thus $-6.x + y -3.y^2+ 2y^3 = k$.

Being an eigenvector of $f^*$ does not just guarantee a formula to be a semi-invariant of a loop transformed by f. This is also a necessary condition.

Theorem 1

$\varphi : \mathbb {K}^n \mapsto \mathbb {K}$ is a semi-invariant if and only if $\exists \lambda \in \mathbb {K}, \exists \varphi \in E_\lambda ,$ where $E_\lambda = ker (f^* - \lambda Id)$.

It is now clear that the set of invariants is exactly the union of all eigenspaces of $f^*$, i.e. a vector space union (which is not a vector space itself). An element $\varphi$ of $E_\lambda$ of basis $\{e_1,...e_n\}$ is a linear combination of $e_1,...,e_n$:

$$\begin{aligned} \varphi = \sum \limits _{{k = 1}}^{n} k_ie_i \end{aligned}$$

The parameters $k_i$ can be chosen with respect to the initial state of the loop.

Expression of Eigenvectors as Invariants. More than a syntactic sugar, the variable $\mathbbm {1}$ brings interesting properties over the kind of invariants we generate for an application f. The vector $e_\mathbbm {1}$ such that $\langle e_\mathbbm {1},X\rangle = \mathbbm {1}$ is always an eigenvector associated to the eigenvalue 1. Indeed, by definition $f(\mathbbm {1})=\mathbbm {1}$, hence $f^*(e_\mathbbm {1})=e_\mathbbm {1}$. For example, let’s take the mapping $f(x,y,xy,\mathbbm {1}) = (2x, \frac{1}{2}y + 1,xy + 2x,\mathbbm {1})$. This mapping admits 3 eigenvalues : $2,~\frac{1}{2}$ and 1. There exists two eigenvectors for the eigenvalue 1 : $(-2,0,1,0)$ and $(0,0,0,1) = e_\mathbbm {1}$. We have then the semi-invariant $k_1.(-2x + xy) + k_2 = 0$, or $-2x + xy = \frac{-k_2}{k_1}$. This implies that the two parameters $k_1$ and $k_2$ can be reduced to only one paramter $k = \frac{-k_2}{k_1}$, which simplifies a lot the equation by providing a way to compute the parameter at the initial state if we know it. For our example, $\frac{-k_2}{k_1}$ would be $-2x_ init + x_ init .y_ init$, where $x_ init$ and $y_ init$ are the initial values of x and y. More generally, each eigenvector associated to 1 gives us an invariant $\varphi$ that can be rewritten as $\varphi (X) = k$, where k is inferred from the initial value of the loop variables.

We can generalize this observation to eigenvectors associated to any eigenvalue. To illustrate this category, let us take as example $f(x,y,z) = (2x,2y,2z)$. Eigenvectors associated to 2 are $e_1=(1,0,0)$, $e_2=(0,1,0)$ and $e_3=(0,0,1)$, thus $k_1x + k_2y + k_3z= 0$ is a semi invariant, for any $k_1$, $k_2$ and $k_3$ satisfying the formula for the initial condition of the loop. However, if we try to set e.g. $k_1=k_2 = 1$, using $x + y + kz = 0$ as semi invariant, we won’t be able to find a proper invariant when $y_ init$ or $x_ init \ne 0$ and $z_ init = 0$. Thus, in order to keep the genericity of our formulas, we cannot afford to simplify the invariant as easily as we can do for invariants associated to the eigenvalue 1. Namely for every $e_i$, we have to test whether $\langle e_i,X_ init \rangle =0$. For each $e_i$ for which this is the case, $\langle e_i,X\rangle = 0$ is itself an invariant if $\langle e_i,X_ init \rangle = 0$. However, if there exists an i such that $\langle e_i,X_ init \rangle \ne 0$, then we can simplify the problem. For example, we assume that $z_ init \ne 0$. Then $k_1x_ init + k_2y_ init + k_3z_ init = 0 \Leftrightarrow \frac{k_1x_ init + k_2y_ init }{z_ init } =- k_3$. We know then that $k_1x + k_2y = \frac{k_1x_ init + k_2y_ init }{z_ init }z$ is a semi-invariant. By writing $g(k_1,k_2) = \frac{k_1x_ init + k_2y_ init }{z_ init }$, we have

$\left\{ { \begin{array}{lll} x &{}=&{} g(1,0)z\\ y &{}=&{} g(0,1)z \end{array} } \right.$

As g is a linear application, these two invariants implies that $\forall k_1,k_2, k_1x + k_2y = g(k_1,k_2)z$ is a semi-invariant.

Property 3

Let $\mathcal {F}$ a semi-invariant expressed as $\mathcal {F} = \sum \limits _{i=0}^nk_ie_i$.

If $\langle e_0,X_{init}\rangle \ne 0$, then we have that

$$\begin{aligned} \bigwedge \limits _{i = 1}^n (\langle e_i,X\rangle = -\frac{\langle e_i,X_{init}\rangle }{\langle e_0,X_{init}\rangle }\langle e_0,X\rangle )\mathrm {~is~an~invariant} \Leftrightarrow \langle \mathcal {F},X_{init}\rangle = 0 \end{aligned}$$

We are now able to use pairs of eigenvectors to express invariants by knowing the initial condition.

Algorithm. As we are restricting our study to solvable loops, that we know can be replaced without loss of generality by linear loops, we assume the input of this algorithm is a family of linear mappings. We can easily compose them via their matrix representation. We end up with a new matrix A. Computing the dual of A is computing the matrix $A^T$. Then, eigenvectors of $A^T$ can be computed by many algorithms in the linear algebra literature [21]. As the eigenvalue problem is known to be polynomial, our invariant generation algorithm is also polynomial.

4.3 Extension of the Method

  Let $A \in \mathcal {M}_n(\mathbb {Q})$. In the general case, A admits irrational and complex eigenvalues and eigenvectors, which end up generating irrational or complex invariants. We cannot accept such representation for a further analysis of the input program because of the future use of these invariants, by SMT solvers for example which hardly deal with non-rational numbers. For example, let us take the function $f(x,y) = (y,2x)$. This mapping admits two eigenvalues: $\lambda _x = \sqrt{2}$ and $\lambda _y = -\sqrt{2}$. In this example, the previous method would output the invariants $k.(x + \sqrt{2} y) = 0$ and $k'.(x-\sqrt{2} y) = 0$. With x and y integers or rationals, this would be possible iff $k = k' = 0$. However, by considering the variable xy the invariant generation procedure outputs the invariant $k.(xy) = 0$, which is possible if x or y equals 0. This raises the issue of finding a product of variables that will give us a rational invariant. We aim to treat the problem at its source: the algebraic character of the matrix eigenvalues. A value x is algebraic in $\mathbb {Q}$ if there exists a polynomial P in $\mathbb {Q}[X]$ such that $P(x) = 0$. Assuming we have a geometric relation between the complex eigenvalues $\lambda _i$ (i.e. a product q of eigenvalues that is rational), we will build a monomial m as a product of variables $x_i$ associated to $\lambda _i$ such that the presence of this monomial induces the presence of a rational eigenvalue, namely q. Moreover, a rational eigenvalue of a matrix is always associated to a rational eigenvector. Indeed, the kernel of a rational matrix is always a $\mathbb {Q}$-vector space. If $\lambda \in \mathbb {Q}$ is an eigenvalue of A, then $A - \lambda .Id$ is a rational matrix and its kernel is not empty.

Definition 5

Let $A \in \mathcal {M}_n(\mathbb {Q})$ . We denote $\varPsi _d(A)$ the elevation matrix such that $\forall X = (x_1,...,x_n)\in \mathbb {Q}^n, \varPsi _d(A).p(X) = p(A.X)$, with $p \in (\mathbb {Q}[X]^k)$ a polynomial associating X to all possible monomials of degree d or lower.

For example, if we have $A = \left( \begin{array}{ll} a &{} b\\ c &{} d \end{array}\right)$ as a transformation for $X = (x,y)$, we have as transformation for the variables $(x^2,xy,y^2,x,y)$ the matrix

$$\varPsi _2(A) = \left( \begin{array}{lllll} a^2 &{} 2ab&{} b^2 &{} 0 &{} 0\\ ac &{} ad + bc&{} bd &{} 0 &{} 0\\ c^2 &{} 2cd &{} d^2 &{} 0 &{} 0\\ 0 &{} 0 &{} 0 &{} a &{} b\\ 0 &{} 0 &{} 0 &{} c &{} d \end{array}\right) $$

Property 4

Let $A\in \mathcal {M}_d(\mathbb {Q}),\varLambda (M)$ the eigenvalue set of a matrix M and d an integer. Then for any product p of d or less elements of $\varLambda (A), p \in \varLambda (\varPsi _d(A))$.

We can generalize this property for more variables. After working with two variables, we get a new matrix with new variables that we can combine similarly, and so on. Thanks to this property, if we have a multiplicative relation between eigenvalues we are able to create home-made variables in the elevated application whose presence implies the presence of rational eigenvalues.

Though we could brute-force the search of rational products of irrational eigenvalues in order to find all possibilities of variable products that have rational eigenvalues, we could search for algebraic relations, i.e. multiplicative relations between algebraic values. This subject is treated in [14] and we will not focus on it. However, we can guarantee that there exists at least one monomial having a rational eigenvalue. Indeed, it is known that the product of all eigenvalues of a rational matrix is equal to its determinant. As the determinant of a rational matrix is always rational, we know that the product of all variables infers the presence of the determinant of the matrix as eigenvalue of the elevated matrix. Coming back to the previous example, we have the algebraic relation $\lambda _x.\lambda _y = -2$. If we consider the evolution of xy, we have $(xy') = 2xy$. Note that the eigenvalue associated to xy is 2 and not $-2$. Indeed, we know that $A = P^{-1}JP$, with

$P = \left( \begin{array}{ll} 1 &{} -1\\ \sqrt{2} &{} -\sqrt{2} \end{array}\right)$

and J an upper-triangular matrix, which means the eigenvalues of A are on the diagonal of J. xy in the base of J would be $(x + \sqrt{2}y)(x - \sqrt{2}y) = x^2 - 2y^2$, and we have well $\lambda _x^2 - 2\lambda _y^2 = -2$.

Finally, by knowing that $\lambda _x^2 = 2$, $\lambda _y^2 = 2$ and $\lambda _x\lambda _y = -2$, we will consider the variables $x^2$, $y^2$ and xy in our analysis of f. We can deduce new semi-invariants from these variables: $k_1(xy) + k_2(2x^2 + y^2) = 0$ with the eigenvectors associated to 2 and $k.(y^2 - 2x^2) = 0$ with the eigenvector associated to $-2$.

4.4 Multiple Loops

In this short section, we present our method to treat non-deterministic loops, i.e. loops with non-deterministic conditions. At the beginning of each iteration, the loop can choose randomly between all its bodies. This representation is equivalent to the definition in Sect. 2.

Definition 6

Let $F = \{A_i\}_{1 \leqslant i \leqslant n}$ a family of matrices and Inv(F) the set of invariants of a loop whose different bodies can be encoded by elements of F. $Inv (F) = \{\varphi | \forall X, \varphi .X = 0 \Rightarrow \bigwedge \limits _{i=1}^n \varphi .A_i.X = 0 \}$

Property 5

Let $F = \{A_i\}_{1 \leqslant i \leqslant n}$ a family of matrices.

$$\begin{aligned} Inv(F) = \bigcap \limits _{i=1}^nInv(A_i) \end{aligned}$$

As the set of invariants of a single-body loop are a vector spaces union, its intersection with another set of invariants is also a vector space union. Although we do not consider the condition used by the program to choose the correct body, we still can discover useful invariants. Let us consider the following example, taken from [22], that computes the product of x and y in variable z:

We have to deal with two applications: $f_1(x,y,z) = (2x, (y-1)/2, x + z)$ and $f_2(x,y,z) = (2x, y/2, z)$. The elevation to the degree 2 of $f_1$ and $f_2$ returns applications having both 10 eigenvectors. For simplicity, we focus on invariants associated to the eigenvalue 1.

First, we notice that $e_4 = e'_4$. Then, we can see that $\langle e_1 + e_2,X\rangle = xy + z = \langle e'_1 + e'_2,X\rangle$. Thus, $e_1 + e_2 = e'_1 + e'_2$. Eventually, we find that $e_1 + e_2 + k.e_4 \in (Vect(\{e_i\}_{i\in [1,4]}) \cap Vect(\{e'_i\}_{i\in [1,4]}))$. That’s why $(\langle e_1 + e_2 + k.e_4,X\rangle = 0)$ is a semi-invariant for both $f_1$ and $f_2$, hence for the whole loop. Replacing $\langle k.e_4,X\rangle$ by $k = -k'$ and $\langle e_1 + e_2,X\rangle$ by $xy + z$ gives us $xy + z = k'$.

Algorithm. The intersection of two vector spaces corresponds to the vectors that both vector spaces have in common. It means that such elements can be expressed by elements of the base of each vector space. Let $B_1$ and $B_2$ the bases of the two vector spaces. If $e \in \mathrm {Vect}\{B_1\}$ and $e \in \mathrm {Vect}\{B_2\}$, then $e \in \ker \{(B_1B_2)\}$. To compute the intersection of a vector space union, we just have to compute the kernels of each combination of vector space in the union.

5 Implementation and Experimentation

In order to test our method, we implemented an invariant generator as a plugin of Frama-C [15], a framework for the verification of C programs written in OCaml. Tests have been made on a Dell Precision M4800 with 16 GB RAM and 8 cores. Time does not include parsing time of the code, but only the invariant computation from the Frama-C representation of the program to the formulas. Moreover, our tool doesn’t implement the extension of our method and may output irrational invariants or fail on complex eigenvalues. Benchmark is available at [6]. The second column of the Table 1 represents the number of variables used in the program. The third column represents the invariant degree used for Pilat and Fastind. The last three columns are the computation time of the tools in ms. O.O.T. represents an aborted ten minutes computation and – indicates that no invariant is found.

Table 1. Performance results with our implementation Pilat

All the tested functions are examples for which the presence of a polynomial invariant is compulsory for their verification. The choice of high degree for some functions is motivated by our will to show the efficiency of our tool to find high degree invariants as choosing a higher degree induces computing a bigger set of relations. In the other cases, degree is choosen for its usefulness.

Fig. 3.

Euclidean division C loop and generation of its associated invariants.

For example in Fig. 3 we were interested in finding the invariant $x + qy = k$ for eucli_div. That’s why we set the degree to 2. Let X be the vector of variables $(x,y,q,xq,xy,qy,y_2,x_2,q_2,\mathbbm {1})$. The matrix A representing the loop in Fig. 3 has only one eigenvalue: 1. There exist 4 eigenvectors $\{e_i\}_{i\in [1;4]}$ associated to 1 in A, so $\langle \sum \limits _{i = 1}^4k_ie_i,X\rangle = 0$ is a semi-invariant. One of these eigenvectors, let’s say $e_1$, correspond to the constant variable, i.e. $e_1.X = \mathbbm {1} = 1$, thus we have $\langle \sum \limits _{i = 2}^4k_ie_i,X\rangle = -k_1$ as invariant. In our case, $\langle e_2,X\rangle = y$, $\langle e_3,X\rangle = x + yq$ and $\langle e_4,X\rangle = y_2$. We can remove $(y = k)$ and $(y_2 = k)$ that are evident because y does not change inside the loop. The remaining invariant is $x + yq = k$.

6 Conclusion and Future Work

We presented a simple and effective method to generate non-trivial invariants. One of its great advantages is to only rely on linear algebra theory, and generate modular invariants. Still our method has some issues that we are currently investigating. First, it is incomplete for integers: invariants we generate are only correct for rationals. Perhaps surprisingly, this issue does not come from the invariant generation, but from the linearization procedure which badly takes into account the division. For example in C, the operation $x' = \frac{x}{2}$ with x uneven returns $\frac{x - 1}{2}$. This behavior is not taken into account by the elevation, which can freely multiply this x by a variable y with $y' = 2y$. This returns the assignment $xy' = xy$ which is false if x is odd. Next, we do not treat interleaving loops as we cannot yet compose invariants with our generation technique. The tool has been successfully implemented as an independent tool of Frama-C.

Our next step is to use those invariants with the Frama-C tools Value (a static value analyser) and WP (a weakest precondition calculus API) to apply a CEGAR-loop on counter-examples generated by CaFE, a temporal logic model checker based on [1]. Also, we want the next version of the tool to handle irrational eigenvalues as decribed in Sect. 4.3.