Loop Summarization with Rational Vector Addition Systems

This section illustrates the high-level structure of our invariant generation scheme. The goal is to compute a transition formula that summarizes the behavior of a given program. A transition formula is a formula over a set of program variables \(\textsf {Var}\) along with primed copies \(\textsf {Var}'\), representing the state of the program before and after executing a computation (respectively). For any given program P, a transition formula \(\mathbf {TF}[\![P ]\!]\) can be computed by recursion on syntax:¹

where \((-)^\star \) is a function that computes an over-approximation of the transitive closure of a transition formula. The contribution of this paper is a method for computing this \((-)^\star \) operation, which is based on first over-approximating the input transition formula by a \(\mathbb {Q}\)-VASR, and then computing the (exact) reachability relation of the \(\mathbb {Q}\)-VASR.

We illustrate the analysis on an integer model of a persistent queue data structure, pictured in Fig. 1. The example consists of two operations (enqueue and dequeue), as well as a test harness (harness) that non-deterministically executes enqueue and dequeue operations. The queue achieves O(1) amortized memory operations (mem_ops) in enqueue and queue by implementing the queue as two lists, front and back (whose lengths are modeled as front_len and back_len, respectively): the sequence of elements in the queue is the front list followed by the reverse of the back list. We will show that the queue functions use O(1) amortized memory operations by finding a summary for harness that implies a linear bound on mem_ops (the number of memory operations in the computation) in terms of nb_ops (the total number of enqueue/dequeue operations executed in some sequence of operations).

We analyze the queue compositionally, in “bottom-up” fashion (i.e., starting from deeply-nested code and working our way back up to a summary for harness). There are two loops of interest, one in dequeue and one in harness. Since the dequeue loop is nested inside the harness loop, dequeue is analyzed first. We start by computing a transition formula that represents one execution of the body of the dequeue loop:Observe that each variable in the loop is incremented by a constant value. As a result, the loop update can be captured faithfully by a vector addition system. In particular, we see that this loop body formula is simulated by the \(\mathbb {Q}\)-VASR \(V_{\texttt {deq}}\) (below), where the correspondence between the state-space of \(\textit{Body}_{\texttt {deq}}\) and \(V_{\texttt {deq}}\) is given by the identity transformation (i.e., each dimension of \(V_{\texttt {deq}}\) simply represents one of the variables of \(\textit{Body}_{\texttt {deq}}\)). A formula representing the reachability relation of a vector addition system can be computed in polytime. For the case of \(V_{\texttt {deq}}\), a formula representing k steps of the \(\mathbb {Q}\)-VASR is simplyTo capture information about the pre-condition of the loop, we can project the primed variables to obtain \(\texttt {back\_len} > 0\); similarly, for the post-condition, we can project the unprimed variables to obtain \(\texttt {back\_len}' \ge 0\). Finally, combining (\(\dagger \)) (translated back into the vocabulary of the program) and the pre/post-condition, we form the following approximation of the dequeue loop’s behavior:Using this summary for the dequeue loop, we proceed to compute a transition formula for the body of the harness loop (omitted for brevity). Just as with the dequeue loop, we analyze the harness loop by synthesizing a \(\mathbb {Q}\)-VASR that simulates it, \(V_{\texttt {har}}\) (below), where the correspondence between the state space of the harness loop and \(V_{\texttt {har}}\) is given by the transformation \(S_{\texttt {har}}\):

\(\begin{array}{l} \begin{bmatrix}v\\ w\\ x\\ y\\ z\end{bmatrix} = \underbrace{\begin{bmatrix} 0 &{} 0 &{} 0 &{} 1 &{} 0\\ 0 &{} 1 &{} 0 &{} 0 &{} 0\\ 0 &{} 3 &{} 1 &{} 0 &{} 0\\ 1 &{} 1 &{} 0 &{} 0 &{} 0\\ 0 &{} 0 &{} 0 &{} 0 &{} 1\\ \end{bmatrix}}_{S_{\texttt {har}}} \begin{bmatrix}{} \texttt {front\_len}\\ \texttt {back\_len}\\ \texttt {mem\_ops}\\ \texttt {size}\\ \texttt {nb\_ops}\end{bmatrix}; i{.}e{.}{,} \left( \begin{array}{ll} &{}\texttt {size} = v\\ \wedge &{}\texttt {back\_len} = w\\ \wedge &{}\texttt {mem\_ops}+3\texttt {back\_len} = x\\ \wedge &{}\texttt {back\_len} + \texttt {front\_len} = y\\ \wedge &{}\texttt {nb\_ops} = z\\ \end{array}\right) . \\ V_{\texttt {har}} = \left\{ \underbrace{\begin{bmatrix}v\\ w\\ x\\ y\\ z\end{bmatrix} \rightarrow \begin{bmatrix}v+1\\ w+1\\ x+4\\ y+1\\ z+1\end{bmatrix}}_{\texttt {enqueue}}, \underbrace{\begin{bmatrix}v\\ w\\ x\\ y\\ z\end{bmatrix} \rightarrow \begin{bmatrix}v-1\\ w\\ x+2\\ y-1\\ z+1\end{bmatrix}}_{\texttt {dequeue} \text { fast}}, \underbrace{\begin{bmatrix}v\\ w\\ x\\ y\\ z\end{bmatrix} \rightarrow \begin{bmatrix}v-1\\ 0\\ x+2\\ y-1\\ z+1\end{bmatrix}}_{\texttt {dequeue} \text { slow}} \right\} \end{array}\)

Unlike the dequeue loop, we do not get an exact characterization of the dynamics of each changed variable. In particular, in the slow dequeue path through the loop, the value of front_len, back_len, and mem_ops change by a variable amount. Since back_len is set to 0, its behavior can be captured by a reset. The dynamics of front_len and mem_ops cannot be captured by a \(\mathbb {Q}\)-VASR, but (using our dequeue summary) we can observe that the sum of front_len + back_len is decremented by 1, and the sum of mem_ops + 3back_len is incremented by 2.

We compute the following formula that captures the reachability relation of \(V_{\texttt {har}}\) (taking \(k_1\) steps of enqueue, \(k_2\) steps of dequeue fast, and \(k_3\) steps of dequeue slow) under the inverse image of the state correspondence \(S_{\texttt {har}}\):From the above formula (along with pre/post-condition formulas), we obtain a summary for the harness loop (omitted for brevity). Using this summary we can prove (supposing that we start in a state where all variables are zero) that mem_ops is at most 4 times nb_ops (i.e., enqueue and dequeue use O(1) amortized memory operations).

This section shows how to compute a \(\mathbb {Q}\)-VASR abstraction for a consistent conjunctive formula. When the input formula is in \(\exists \text {LRA}\), the computed \(\mathbb {Q}\)-VASR abstraction will be a best \(\mathbb {Q}\)-VASR abstraction of the input formula. The intuition is that, since \(\exists \text {LRA}{}\) is a convex theory, a best \(\mathbb {Q}\)-VASR abstraction consists of a single transition. For \(\exists \text {LIRA}{}\) formulas, our procedure produces a \(\mathbb {Q}\)-VASR abstract that is not guaranteed to be best, precisely because \(\exists \text {LIRA}{}\) is not convex.

Let C be consistent, conjunctive transition formula. Observe that the set \({\textit{Res}_C \triangleq \{ \langle \mathbf {s}, a \rangle : C \,\models \, \mathbf {s} \cdot \mathbf {x'} = a\}}\), which represents linear combinations of variables that are reset across C, forms a vector space. Similarly, the set \(\textit{Inc}_C = \{ \langle \mathbf {s}, a \rangle : C \,\models \,\mathbf {s} \cdot \mathbf {x'} = \mathbf {s} \cdot \mathbf {x} + a\}\), which represents linear combinations of variables that are incremented across C, forms a vector space. We compute bases for both \(\textit{Res}_C\) and \(\textit{Inc}_C\), say \(\{ \langle \mathbf {s}_1, a_1 \rangle , ..., \langle \mathbf {s}_m,a_m \rangle \}\) and \(\{ \langle \mathbf {s}_{m+1}, a_{m+1} \rangle , ..., \langle \mathbf {s}_d,a_d \rangle \}\), respectively. We define \(\hat{\alpha }(C)\) to be the \(\mathbb {Q}\)-VASR abstraction \(\hat{\alpha }(C) \triangleq (S, \{(\mathbf {r}, \mathbf {a})\})\), where

This section shows how to compute least upper bounds w.r.t. the \(\preceq \) order.

By definition of the \(\preceq \) order, if \((S,V{})\) is an upper bound of \((S^1,V{}^1)\) and \((S^2,V{}^2)\), then there must exist matrices \(T^1\) and \(T^2\) such that \(T^1S^1 = S = T^2S^2\), \(V^1 \Vdash _{T^1} V\), and \(V^2 \Vdash _{T^2} V\). As we shall see, if (S, V) is a least upper bound, then it is completely determined by the matrices \(T^1\) and \(T^2\). Thus, we shift our attention to computing simulation matrices \(T^1\) and \(T^2\) that induce a least upper bound.

In view of the desired equation \(T^1S^1 = S = T^2S^2\), let us consider the constraint \(T^1S^1 = T^2S^2\) on two unknown matrices \(T^1\) and \(T^2\). Clearly, we have \(T^1S^1 = T^2S^2\) iff each \((T^1_i,T^2_i)\) belongs to the set \(\mathcal {T} \triangleq \{ (\mathbf {t}^1, \mathbf {t}^2) : \mathbf {t}^1S^1 = \mathbf {t}^2S^2 \}\). Observe that \(\mathcal {T}\) is a vector space, so there is a best solution to the constraint \(T^1S^1 = T^2S^2\): choose \(T^1\) and \(T^2\) so that the set of all row pairs \((T^1_i,T^2_i)\) forms a basis for \(\mathcal {T}\). In the following, we use \(\textit{pushout}(S^1,S^2)\) to denote a function that computes such a best \((T^1, T^2)\).

While \(\textit{pushout}\) gives a best solution to the equation \(T^1S^1 = T^2S^2\), it is not sufficient for the purpose of computing least upper bounds for \(\mathbb {Q}\)-VASR abstractions, because \(T^1\) and \(T^2\) may not respect the structure of the \(\mathbb {Q}\)-VASR \(V^1\) and \(V^2\) (i.e., there may be no \(\mathbb {Q}\)-VASR V such that \(V^1 \Vdash _{T^1} V\) and \(V^2 \Vdash _{T^2} V\)). Thus, we must further constrain our problem by requiring that \(T^1\) and \(T^2\) are coherent with respect to \(V^1\) and \(V^2\) (respectively).

For any d-dimensional \(\mathbb {Q}\)-VASR \(V{}\) and coherence class \(C = \{c_1,...,c_k\}\) of \(V{}\), define \(\varPi _{C}\) to be the \(k \times d\) dimensional matrix whose rows are \(\mathbf {e}_{c_1}, ..., \mathbf {e}_{c_k}\). Intuitively, \(\varPi _{C}\) is a projection onto the set of dimensions in C.

Coherence is a necessary and sufficient condition for linear simulations between \(\mathbb {Q}\)-VASR in a sense described in Lemmas 1 and 2.

Let \(V{}\) be a d-dimensional \(\mathbb {Q}\)-VASR and let \(T \in \mathbb {Q}^{e \times d}\) be a matrix that is coherent with respect to \(V{}\) and has no zero rows. Then there is a (unique) e-dimensional \(\mathbb {Q}\)-VASR \(\textit{image}(V{},T)\) such that its transition relation \(\rightarrow _{\textit{image}(V{},T)}\) is equal to \(\{(T\mathbf {u},T\mathbf {v}) : \mathbf {u} \rightarrow _{V} \mathbf {v}\}\) (the image of \(V{}\)’s transition relation under T). This \(\mathbb {Q}\)-VASR can be defined by:where \(T \boxtimes \mathbf {r}\) is the reset vector \(\mathbf {r}\) translated along T (i.e., \((T \boxtimes \mathbf {r})_i = r_j\) where j is an arbitrary choice among dimensions for which \(T_{ij}\) is non-zero—at least one such j exists because the row \(T_i\) is non-zero by assumption, and the choice of j is arbitrary because all such j belong to the same coherence class by the assumption that T is coherent with respect to \(V{}\)).

Finally, prior to describing our least upper bound algorithm, we must define a technical condition that is both assumed and preserved by the procedure:

Intuitively, a \(\mathbb {Q}\)-VASR abstraction that is not normal contains information that is either inconsistent or redundant.

We now present a strategy for computing least upper bounds of \(\mathbb {Q}\)-VASR abstractions. Fix (normal) \(\mathbb {Q}\)-VASR abstractions \((S^1,V{}^1)\) and \((S^2,V^2{})\). Lemmas 1 and 2 together show that a pair of matrices \(\widetilde{T}^1\) and \(\widetilde{T}^2\) induce an upper bound (not necessarily least) on \((S^1,V{}^1)\) and \((S^2,V^2{})\) exactly when the following conditions hold: (1) \(\widetilde{T}^1S^1 = \widetilde{T}^2S^2\), (2) \(\widetilde{T}^1\) is coherent w.r.t. \(V^1\), (3) \(\widetilde{T}^2\) is coherent w.r.t. \(V^2\), and (4) neither \(\widetilde{T}^1\) nor \(\widetilde{T}^2\) contain zero rows. The upper bound induced by \(\widetilde{T}^1\) and \(\widetilde{T}^2\) is given byWe now consider how to compute a best such \(\widetilde{T}^1\) and \(\widetilde{T}^2\). Observe that conditions (1), (2), and (3) hold exactly when for each row i, \((\widetilde{T}^1_i, \widetilde{T}^2_i)\) belongs to the setSince a row vector \(\mathbf {t}^i\) is coherent w.r.t. \(V^i\) iff its non-zero positions belong to the same coherence class of \(V^i\) (equivalently, \(\mathbf {t}^i = \mathbf {u}\varPi _{C^i}\) for some coherence class \(C^i\) and vector \(\mathbf {u}\)), we have \(\mathcal {T} = \bigcup _{C^1,C^2} \mathcal {T}(C^1,C^2)\), where the union is over all coherence classes \(C^1\) of \(V^1\) and \(C^2\) of \(V^2\), andObserve that each \(\mathcal {T}(C^1,C^2)\) is a vector space, so we can compute a pair of matrices \(T^1\) and \(T^2\) such that the rows \((T^1_i, T^2_i)\) collectively form a basis for each \(\mathcal {T}(C^1,C^2)\). Since \((S^1,V{}^1)\) and \((S^2,V^2{})\) are normal (by assumption), neither \(T^1\) nor \(T^2\) may contain zero rows (condition (4) is satisfied). Finally, we have that \(\textit{ub}(T^1,T^2)\) is the least upper bound of \((S^1,V{}^1)\) and \((S^2,V^2{})\). Algorithm 2 is a straightforward realization of this strategy.

In the following, we give a method for over-approximating the transitive closure of a transition formula \(F(\mathbf {x},\mathbf {x}')\) using a \(\mathbb {Q}\)-VASRS. We start by defining predicate \(\mathbb {Q}\)-VASRS, a variation of \(\mathbb {Q}\)-VASRS with control states that correspond to disjoint state predicates (where the states intuitively belong to the transition formula F rather than the \(\mathbb {Q}\)-VASRS itself). We extend linear simulations and best abstractions to predicate \(\mathbb {Q}\)-VASRS, and give an algorithm for synthesizing best predicate \(\mathbb {Q}\)-VASRS abstractions (for a given set of predicates). Finally, we give an end-to-end algorithm for over-approximating the transitive closure of a transition formula.

We extend linear simulations to predicate \(\mathbb {Q}\)-VASRS as follows:

We define a \(\mathbb {Q}\)-VASRS abstraction over \(\mathbf {x} = x_1,...,x_n\) to be a pair \((S,\mathcal {V}{})\) consisting of a rational matrix \(S \in \mathbb {Q}^{d \times n}\) and a predicate \(\mathbb {Q}\)-VASRS of dimension d over \(\mathbf {x}\). We extend the simulation preorder \(\preceq \) to \(\mathbb {Q}\)-VASRS abstractions in the natural way. Extending the definition of “best” abstractions requires more care, since we can always find a “better” \(\mathbb {Q}\)-VASRS abstraction (strictly smaller in \(\preceq \) order) by using a finer set of predicates. However, if we consider only predicate \(\mathbb {Q}\)-VASRS that share the same set of control states, then best abstractions do exist and can be computed using Algorithm 3.

Algorithm 3 works as follows: first, for each pair of formulas \(p, q \in P\), compute a best \(\mathbb {Q}\)-VASR abstraction of the formula \(p(\mathbf {x}) \wedge F(\mathbf {x},\mathbf {x}') \wedge q(\mathbf {x}')\) and call it \((S_{p,q},V{}_{p,q})\). \((S_{p,q},V{}_{p,q})\) over-approximates the transitions of F that begin in a program state satisfying p and end in a program state satisfying q. Second, we compute the least upper bound of all \(\mathbb {Q}\)-VASR abstractions \((S_{p,q},V{}_{p,q})\) to get a \(\mathbb {Q}\)-VASR abstraction (S, V) for F. As a side-effect of the least upper bound computation, we obtain a linear simulation \(T_{p,q}\) from \((S_{p,q},V_{p,q})\) to (S, V) for each p, q. A best \(\mathbb {Q}\)-VASRS abstraction of \(F(\mathbf {x},\mathbf {x}')\) with control states P has S as its simulation matrix and has the image of \(V_{p,q}\) under \(T_{p,q}\) as the edges from p to q.

We now describe iter-VASRS (Algorithm 4), which uses \(\mathbb {Q}\)-VASRS to over-approximate the transitive closure of transition formulas. Towards our goal of predictable program analysis, we desire the analysis to be monotone in the sense that if F and G are transition formulas such that F entails G, then iter-VASRS(F) entails iter-VASRS(G). A sufficient condition to guarantee monotonicity of the overall analysis is to require that the set of control states that we compute for F is at least as fine as the set of control states we compute for G. We can achieve this by making the set of control states P of input transition formula \(F(\mathbf {x},\mathbf {x}')\) equal to the set of connected regions of the topological closure of \(\exists \mathbf {x}'{.}F\) (lines 1–4). Note that this set of predicates may fail the contract of abstract-VASRS: there may exist a transition \(\mathbf {u} \rightarrow _F \mathbf {v}\) such that \(\mathbf {v} \,\not \models \, \bigvee P\) (this occurs when there is a state of F with no outgoing transitions). As a result, \((S,\mathcal {V}) =\) abstract-VASRS(F, P) does not necessarily approximate F; however, it does over-approximate \(F \wedge \bigvee P(\mathbf {x}')\). An over-approximation of the transitive closure of F can easily be obtained from \(\textit{reach}(\mathcal {V})(S\mathbf {x},S\mathbf {x}')\) (the over-approximation of the transitive closure of \(F \wedge \bigvee P(\mathbf {x}')\) obtained from the \(\mathbb {Q}\)-VASRS abstraction (\(S,\mathcal {V}\))) by sequentially composing with the disjunction of F and the identity relation (line 6).

Precision Improvement. The abstract-VASRS algorithm uses predicates to infer the control structure of a \(\mathbb {Q}\)-VASRS, but after computing the \(\mathbb {Q}\)-VASRS abstraction, iter-VASRS makes no further use of the predicates (i.e., the predicates are irrelevant in the computation of \(\textit{reach}(\mathcal {V})\)). Predicates can be used to improve iter-VASRS as follows: the reachability relation of a \(\mathbb {Q}\)-VASRS is expressed by a formula that uses auxiliary variables to represent the state at which the computation begins and ends [8]. These variables can be used to encode that the pre-state of the transitive closure must satisfy the predicate corresponding to the begin state and the post-state must satisfy the predicate corresponding to the end state. As an example, consider the Fig. 2 and suppose that we wish to prove the invariant \(x \le 2i\) under the pre-condition \(i = 0 \wedge x = 0\). While this invariant holds, we cannot prove it because there is counter example if the computation begins at \(i\%2 == 1\). By applying the above improvement, we can prove that the computation must begin at \(i\%2 == 0\), and the invariant is verified.