Lower Runtime Bounds for Integer Programs

Abstract

We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs. To this end, we construct symbolic representations of program executions using a framework for iterative, under-approximating program simplification. The core of this simplification is a method for (under-approximating) program acceleration based on recurrence solving and a variation of ranking functions. Afterwards, we deduce asymptotic lower bounds from the resulting simplified programs. We implemented our technique in our tool LoAT and show that it infers non-trivial lower bounds for a large number of examples.

Supported by the DFG grant GI 274/6-1 and the Air Force Research Laboratory (AFRL).

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

Recent advances in program analysis yield efficient methods to find upper bounds on the complexity of sequential integer programs. Here, one usually considers “worst-case complexity”, i.e., for any variable valuation, one analyzes the length of the longest execution starting from that valuation. But in many cases, in addition to upper bounds, it is also important to find lower bounds for this notion of complexity. Together with an analysis for upper bounds, this can be used to infer tight complexity bounds. Lower bounds also have important applications in security analysis, e.g., to detect possible denial-of-service or side-channel attacks, as programs whose runtime depends on a secret parameter “leak” information about that parameter. In general, concrete lower bounds that hold for arbitrary variable valuations can hardly be expressed concisely. In contrast, asymptotic bounds are easily understood by humans and witness possible attacks in a convenient way.

We first introduce our program model in Sect. 2. In Sect. 3, we show how to use a variation of classical ranking functions which we call metering functions to under-estimate the number of iterations of a simple loop (i.e., a single transition t looping on a location $\ell$). Then, we present a framework for repeated program simplifications in Sect. 4. It simplifies full programs (with branching and sequences of possibly nested loops) to programs with only simple loops. Moreover, it eliminates simple loops by (under-)approximating their effect using a combination of metering functions and recurrence solving. In this way, programs are transformed to simplified programs without loops. In Sect. 5, we then show how to extract asymptotic lower bounds and variables that influence the runtime from simplified programs. Finally, we conclude with an experimental evaluation of our implementation LoAT in Sect. 6. For all proofs, we refer to [16].

Related Work. While there are many techniques to infer upper bounds on the worst-case complexity of integer programs (e.g., [1–4, 8, 9, 14, 19, 26]), there is little work on lower bounds. In [3], it is briefly mentioned that their technique could also be adapted to infer lower instead of upper bounds for abstract cost rules, i.e., integer procedures with (possibly multiple) outputs. However, this only considers best-case lower bounds instead of worst-case lower bounds as in our technique. Upper and lower bounds for cost relations are inferred in [1]. Cost relations extend recurrence equations such that, e.g., non-determinism can be modeled. However, this technique also considers best-case lower bounds only.

A method for best-case lower bounds for logic programs is presented in [11]. Moreover, we recently introduced a technique to infer worst-case lower bounds for term rewrite systems (TRSs) [15]. However, TRSs differ fundamentally from the programs considered here, since they do not allow integers and have no notion of a “program start”. Thus, the technique of [15], based on synthesizing families of reductions by automatic induction proofs, is very different to the present paper.

To simplify programs, we use a variant of loop acceleration to summarize the effect of applying a loop repeatedly. Acceleration is mostly used in over-approximating settings (e.g., [13, 17, 21, 24]), where handling non-determinism is challenging, as loop summaries have to cover all possible non-deterministic choices. However, our technique is under-approximating, i.e., we can instantiate non-deterministic values arbitrarily. In contrast to the under-approximating acceleration technique in [22], instead of quantifier elimination we use an adaptationof ranking functions to under-estimate the number of loop iterations symbolically.

2 Preliminaries

We consider sequential non-recursive imperative integer programs, allowing non-linear arithmetic and non-determinism, whereas heap usage and concurrency are not supported. While most existing abstractions that transform heap programs to integer programs are “over-approximations”, we would need an under-approximating abstraction to ensure that the inference of worst-case lower bounds is sound. As in most related work, we treat numbers as mathematical integers $\mathbb {Z}$. However, the transformation from [12] can be used to handle machine integers correctly by inserting explicit normalization steps at possible overflows.

$\mathcal {A}(\mathcal {V})$ is the set of arithmetic terms¹ over the variables $\mathcal {V}$ and $\mathcal {F}(\mathcal {V})$ is the set of conjunctions² of (in)equations over $\mathcal {A}(\mathcal {V})$. So for $x,y \in \mathcal {V}$, $\mathcal {A}(\mathcal {V})$ contains terms like $x \cdot y + 2^y$ and $\mathcal {F}(\mathcal {V})$ contains formulas such as $x \cdot y \le 2^y \wedge y > 0$.

We fix a finite set of program variables $\mathcal {PV}$ and represent integer programs as directed graphs. Nodes are program locations $\mathcal {L}$ and edges are program transitions $\mathcal {T}$ where $\mathcal {L}$ contains a canonical start location $\ell _0$. W.l.o.g., no transition leads back to $\ell _0$ and all transitions $\mathcal {T}$ are reachable from $\ell _0$. To model non-deterministic program data, we introduce pairwise disjoint finite sets of temporary variables $\mathcal {TV}_\ell$ with $\mathcal {PV}\cap \mathcal {TV}_\ell = \varnothing$ and define $\mathcal {V}_\ell = \mathcal {PV}\cup \mathcal {TV}_\ell$ for all locations $\ell \in \mathcal {L}$.

Definition 1

(Programs). Configurations $(\ell , \varvec{v})$ consist of a location $\ell \in \mathcal {L}$ and a valuation $\varvec{v}: \mathcal {V}_\ell \rightarrow \mathbb {Z}$. $\mathcal {V}\! al _\ell = \mathcal {V}_\ell \rightarrow \mathbb {Z}$ is the set of all valuations for $\ell \in \mathcal {L}$ and valuations are lifted to terms $\mathcal {A}(\mathcal {V}_\ell )$ and formulas $\mathcal {F}(\mathcal {V}_\ell )$ as usual. A transition $t = (\ell ,\gamma ,\eta ,c,\ell ')$ can evaluate a configuration $(\ell , \varvec{v})$ if the guard $\gamma \in \mathcal {F}(\mathcal {V}_\ell )$ issatisfied (i.e., $\varvec{v}(\gamma )$ holds) to a new configuration $(\ell ', \varvec{v}')$. The update $\eta : \mathcal {PV}\rightarrow \mathcal {A}(\mathcal {V}_\ell )$ maps any $x \in \mathcal {PV}$ to a term $\eta (x)$ where $\varvec{v}(\eta (x)) \in \mathbb {Z}$ for all $\varvec{v}\in \mathcal {V}\! al _{\ell }$. Itdetermines $\varvec{v}'$ by setting $\varvec{v}'(x) = \varvec{v}(\eta (x))$ for $x \in \mathcal {PV}$, while $\varvec{v}'(x)$ for $x \in \mathcal {TV}_{\ell '}$ is arbitrary. Such an evaluation step has cost $k = \varvec{v}(c)$ for $c\in \mathcal {A}(\mathcal {V}_\ell )$ and is written $(\ell , \varvec{v}) \rightarrow _{t, k} (\ell ', \varvec{v}')$. We use $\mathsf {src}(t) = \ell$, $\mathsf {guard}(t) = \gamma$, $\mathsf {cost}(t) = c$, and $\mathsf {dest}(t) = \ell '$. We sometimes drop the indices t, k and write $(\ell , \varvec{v}) \rightarrow _{k}^* (\ell ', \varvec{v}')$ if $(\ell , \varvec{v}) \rightarrow _{k_1} \dots \rightarrow _{k_{m}} (\ell ', \varvec{v}')$ and $\sum _{1\le i \le m}k_i = k$. A program is a set of transitions $\mathcal {T}$.

Fig. 1.

Example integer program

Figure 1 shows an example, where the pseudo-code on the left corresponds to the program on the right. Here, $\texttt {random}(x,y)$ returns a random integer $m$ with $x< m < y$ and we fix $-\omega< m < \omega$ for all numbers $m$. The loop at location $\ell _1$ sets y to a value that is quadratic in x. Thus, the loop at $\ell _2$ is executed quadratically often where in each iteration, the inner loop at $\ell _3$ may also be repeated quadratically often. Thus, the length of the program’s worst-case execution is a polynomial of degree 4 in x. Our technique can infer such lower bounds automatically.

In the graph of Fig. 1, we write the costs of a transition in $[\;]$ next to its name and represent the updates by imperative commands. We use $x$ to refer to the value of the variable $x$ before the update and $x'$ to refer to $x$’s value after the update. Here, $\mathcal {PV}= \{x,y,z,u\}$, $\mathcal {TV}_{\ell _3} = \{ tv \}$, and $\mathcal {TV}_\ell = \varnothing$ for all locations $\ell \ne \ell _3$. We have $(\ell _3, \varvec{v}) \rightarrow _{t_4} (\ell _3, \varvec{v}')$ for all valuations $\varvec{v}$ where $\varvec{v}(u) > 0$, $\varvec{v}( tv ) > 0$, $\varvec{v}'(u) = \varvec{v}(u) - \varvec{v}( tv )$, and $\varvec{v}'(v) = \varvec{v}(v)$ for all $v \in \{x,y,z\}$.

Our goal is to find a lower bound on the worst-case runtime of a program $\mathcal {T}$. To this end, we define its derivation height [18] by a function $\mathsf {dh}_\mathcal {T}$ that operates on valuations $\varvec{v}$ of the program variables (i.e., $\varvec{v}$ is not defined for temporary variables). The function $\mathsf {dh}_\mathcal {T}$ maps $\varvec{v}$ to the maximum of the costs of all evaluation sequences starting in configurations $(\ell _0, \varvec{v}_{\ell _0})$ where $\varvec{v}_{\ell _0}$ is an extension of $\varvec{v}$ to $\mathcal {V}_{\ell _0}$. So in our example we have $\mathsf {dh}_\mathcal {T}(\varvec{v}) = 2$ for all valuations $\varvec{v}$ where $\varvec{v}(x) = 0$, since then we can only apply the transitions $t_0$ and $t_2$ once. For all valuations $\varvec{v}$ with $\varvec{v}(x) > 1$, our method will detect that the worst-case runtime of our program is at least $\frac{1}{8}\varvec{v}(x)^4 + \frac{1}{4}\varvec{v}(x)^3 + \frac{7}{8}\varvec{v}(x)^2 + \frac{7}{4}\varvec{v}(x)$. From this concrete lower bound, our approach will infer that the asymptotic runtime of the program is in $\varOmega (x^4)$. In particular, the runtime of the program depends on $x$. Hence, if $x$ is “secret”, then the program is vulnerable to side-channel attacks.

Definition 2

(Derivation Height). Let $\mathcal {V}\! al = \mathcal {PV}\rightarrow \mathbb {Z}$. The derivation height $\mathsf {dh}_\mathcal {T}: \mathcal {V}\! al \rightarrow \mathbb {R}_{\ge 0} \cup \{\omega \}$ of a program $\mathcal {T}$ is defined as $\mathsf {dh}_\mathcal {T}(\varvec{v}) = \sup \{ k \in \mathbb {R} \mid \exists \varvec{v}_{\ell _0} \in \mathcal {V}\! al _{\ell _0},\ell \in \mathcal {L}, \varvec{v}_\ell \in \mathcal {V}\! al _\ell \, . \;\; \varvec{v}_{\ell _0}|_\mathcal {PV}= \varvec{v}\; \wedge \; (\ell _0, \varvec{v}_{\ell _0}) \rightarrow ^*_k (\ell , \varvec{v}_\ell ) \}$.

Since $\rightarrow ^*_k$ also permits evaluations with 0 steps, we always have $\mathsf {dh}_\mathcal {T}(\varvec{v}) \ge 0$. Obviously, $\mathsf {dh}_\mathcal {T}$ is not computable in general, and thus our goal is to compute a lower bound that is as precise as possible (i.e., a lower bound which is, e.g., unbounded,³ exponential, or a polynomial of a degree as high as possible).

3 Estimating the Number of Iterations of Simple Loops

We now show how to under-estimate the number of possible iterations of a simpleloop $t = (\ell ,\gamma ,\eta ,c,\ell )$. More precisely, we infer a term $b\in \mathcal {A}(\mathcal {V}_\ell )$ such that for all $\varvec{v}\in \mathcal {V}\! al _\ell$ with $\varvec{v}\models \gamma$, there is a $\varvec{v}' \in \mathcal {V}\! al _\ell$ with $(\ell ,\varvec{v}) \rightarrow ^{\lceil \varvec{v}(b)\rceil }_t (\ell ,\varvec{v}')$. Here, $\lceil k \rceil = \min \{m \in \mathbb {N}\mid m \ge k\}$ for all $k \in \mathbb {R}$. Moreover, $(\ell ,\varvec{v}) \rightarrow ^{m}_t (\ell ,\varvec{v}')$ means that $(\ell , \varvec{v}) = (\ell , \varvec{v}_0) \rightarrow _{t,k_1} (\ell , \varvec{v}_1) \rightarrow _{t,k_2} \dots \rightarrow _{t,k_{m}} (\ell , \varvec{v}_m) = (\ell , \varvec{v}')$ for some costs $k_1, \ldots , k_m$. We say that $(\ell ,\varvec{v}) \rightarrow ^{m}_t (\ell ,\varvec{v}')$ preserves $\mathcal {TV}_{\ell }$ iff $\varvec{v}( tv ) = \varvec{v}_i( tv ) = \varvec{v}'( tv )$ for all $tv \in \mathcal {TV}_\ell$ and all $0 \le i \le m$. Accordingly, we lift the update $\eta$ to arbitrary arithmetic terms by leaving temporary variables unchanged (i.e., if $\mathcal {PV}= \{ x_1, \ldots , x_n \}$ and $b\in \mathcal {A}(\mathcal {V}_\ell )$, then $\eta (b) = b[x_1/\eta (x_1), \ldots , x_n/\eta (x_n)]$, where [x / a] denotes the substitution that replaces all occurrences of the variable x by a).

To find such estimations, we use an adaptation of ranking functions [2, 6, 25] which we call metering functions. We say that a term $b\in \mathcal {A}(\mathcal {V}_\ell )$ is a ranking function ⁴ for $t =(\ell ,\gamma ,\eta ,c,\ell )$ iff the following conditions hold.

$$\begin{aligned} \gamma&\implies b> 0 \end{aligned}$$

(1)

$$\begin{aligned} \gamma&\implies \eta (b) \le b-1 \end{aligned}$$

(2)

So e.g., $x$ is a ranking function for $t_1$ in Fig. 1. If $\mathcal {TV}_\ell = \varnothing$, then for any valuation $\varvec{v}\in \mathcal {V}\! al$, $\varvec{v}(b)$ over-estimates the number of repetitions of the loop t: (2) ensures that $\varvec{v}(b)$ decreases at least by 1 in each loop iteration, and (1) requires that $\varvec{v}(b)$ is positive whenever the loop can be executed. In contrast, metering functions are under-estimations for the maximal number of repetitions of a simple loop.

Definition 3

(Metering Function). Let $t = (\ell ,\gamma ,\eta ,c,\ell )$ be a transition. We call $b\in \mathcal {A}(\mathcal {V}_\ell )$ a metering function for $t$ iff the following conditions hold:

$$\begin{aligned} \lnot \gamma&\implies b\le 0 \end{aligned}$$

(3)

$$\begin{aligned} \gamma&\implies \eta (b) \ge b- 1 \end{aligned}$$

(4)

Here, (4) ensures that $\varvec{v}(b)$ decreases at most by 1 in each loop iteration, and (3) requires that $\varvec{v}(b)$ is non-positive if the loop cannot be executed. Thus, the loop can be executed at least $\varvec{v}(b)$ times (i.e., $\varvec{v}(b)$ is an under-estimation).

For the transition $t_1$ in the example of Fig. 1, $x$ is also a valid metering function. Condition (3) requires $\lnot x > 0 \implies x \le 0$ and (4) requires $x > 0 \implies x-1 \ge x-1$. While $x$ is a metering and a ranking function, $\frac{x}{2}$ is a metering, but not a ranking function for $t_1$. Similarly, $x^2$ is a ranking, but not a metering function for $t_1$. Theorem 4 states that a simple loop t with a metering function $b$ can be executed at least $\lceil \varvec{v}(b) \rceil$ times when starting with the valuation $\varvec{v}$.

Theorem 4

(Metering Functions are Under-Estimations). Let $b$ be a metering function for $t = (\ell ,\gamma ,\eta ,c,\ell )$. Then $b$ under-estimates t, i.e., for all $\varvec{v}\in \mathcal {V}\! al _\ell$ with $\varvec{v}\models \gamma$ there is an evaluation $(\ell ,\varvec{v}) \rightarrow ^{\lceil \varvec{v}(b) \rceil }_t (\ell ,\varvec{v}')$ that preserves $\mathcal {TV}_{\ell }$.

Our implementation builds upon a well-known transformation based on Farkas’ Lemma [6, 25] to find linear metering functions. The basic idea is to search for coefficients of a linear template polynomial $b$ such that (3) and (4) hold for all possible instantiations of the variables $\mathcal {V}_\ell$. In addition to (3) and (4), we also require (1) to avoid trivial solutions like $b= 0$. Here, the coefficients of b are existentially quantified, while the variables from $\mathcal {V}_\ell$ are universally quantified. As in [6, 25], eliminating the universal quantifiers using Farkas’ Lemma allows us to use standard SMT solvers to search for $b$’s coefficients efficiently.

When searching for a metering function for $t = (\ell ,\gamma ,\eta ,c,\ell )$, one can omit constraints from $\gamma$ that are irrelevant for $t$’s termination. So if $\gamma$ is $\varphi \wedge \psi$, $\, \psi \in \mathcal {F}(\mathcal {PV})$, and $\gamma \!\implies \!\eta (\psi )$, then it suffices to find a metering function $b$ for $t' = (\ell ,\varphi , \eta ,c,\ell )$. The reason is that if $\varvec{v}\models \gamma$ and $(\ell ,\varvec{v}) \rightarrow _{t'} (\ell ,\varvec{v}')$, then $\varvec{v}' \models \psi$ (since $\varvec{v}\models \gamma$ entails $\varvec{v}\models \eta (\psi )$). Hence, if $\varvec{v}\models \gamma$ then $(\ell ,\varvec{v}) \rightarrow ^{\lceil \varvec{v}(b)\rceil }_{t'} (\ell ,\varvec{v}')$ implies $(\ell ,\varvec{v}) \rightarrow ^{\lceil \varvec{v}(b)\rceil }_{t} (\ell ,\varvec{v}')$, i.e., $b$ under-estimates t. So if $t = (\ell , \, x< y \, \wedge \, 0 < y, \, x'=x+1, c, \ell )$, we can consider $t'\!=\!(\ell , \, x < y ,\, x'\!=\!x\!+\!1, c, \ell )$ instead. While $t$ only has complex metering functions like $\min (y-x,y)$, $t'$ has the metering function $y - x$.

Example 5

(Unbounded Loops). Loops $t = (\ell ,\gamma ,\eta ,c,\ell )$ where the whole guard can be omitted (since $\gamma \implies \eta (\gamma )$) do not terminate. Here, we also allow $\omega$ as under-estimation. So for $\mathcal {T}= \{(\ell _0, true ,\mathsf {id},1,\ell ),\,t\}$ with $t = (\ell , \, 0 < x, \, x'=x+1, \, y, \, \ell )\}$, we can omit $0 <x$ since $0< x\!\implies \!0 < x+1$. Hence, $\omega$ under-estimates the resulting loop $(\ell , \, true , \, x'=x+1, \, y, \, \ell )$ and thus, $\omega$ also under-estimates t.

4 Simplifying Programs to Compute Lower Bounds

We now define processors mapping programs to simpler programs. Processors are applied repeatedly to transform the program until extraction of a (concrete) lower bound is straightforward. For this, processors should be sound, i.e., any lowerbound for the derivation height of $\mathsf {proc}(\mathcal {T})$ should also be a lower bound for $\mathcal {T}$.

Definition 6

(Sound Processor). A mapping $\mathsf {proc}$ from programs to programs is sound iff $\mathsf {dh}_\mathcal {T}(\varvec{v}) \ge \mathsf {dh}_{\mathsf {proc}(\mathcal {T})}(\varvec{v})$ holds for all programs $\mathcal {T}$ and all $\varvec{v}\in \mathcal {V}\! al$.

In Sect. 4.1, we show how to accelerate a simple loop $t$ to a transition which is equivalent to applying $t$ multiple times (according to a metering function for $t$). The resulting program can be simplified by chaining subsequent transitions which may result in new simple loops, cf. Sect. 4.2. We describe a simplification strategy which alternates these steps repeatedly. In this way, we eventually obtain a simplified program without loops which directly gives rise to a concrete lower bound.

4.1 Accelerating Simple Loops

Consider a simple loop $t = (\ell ,\gamma ,\eta ,c,\ell )$. For $m \in \mathbb {N}$, let $\eta ^m$ denote m applications of $\eta$. To accelerate t, we compute its iterated update and costs, i.e., a closed form $\eta _{\mathrm {it}}$ of $\eta ^ tv$ and an under-approximation $c_{\mathrm {it}}\in \mathcal {A}(\mathcal {V}_\ell )$ of $\sum _{0\le i < tv }\eta ^i(c)$ for a fresh temporary variable $tv$. If $b$ under-estimates t, then we add the transition $(\ell ,\, \gamma \, \wedge \, 0< tv < b+ 1, \, \eta _{\mathrm {it}},\, c_{\mathrm {it}}, \, \ell )$ to the program. It summarizes $tv$ iterations of t, where $tv$ is bounded by $\lceil b\rceil$. Here, $\eta _{\mathrm {it}}$ and $c_{\mathrm {it}}$ may also contain exponentiation (i.e., we can also infer exponential bounds).

For $\mathcal {PV}= \{x_1,\ldots ,x_n\}$, the iterated update is computed by solving the recurrence equations $x^{(1)} = \eta (x)$ and $x^{( tv +1)} = \eta (x)[x_1/x_1^{( tv )}, \ldots , x_n/x_n^{( tv )}]$ for all $x \in \mathcal {PV}$ and $tv \ge 1$. So for the transition $t_1$ from Fig. 1 we get the recurrence equations $x^{(1)}=x-1$, $x^{( tv _1+1)}=x^{( tv _1)}-1$, $y^{(1)}=y + x$, and $y^{( tv _1+1)}=y^{( tv _1)} + x^{( tv _1)}$. Usually, they can easily be solved using state-of-the-art recurrence solvers [4]. In our example, we obtain the closed forms $\eta _{\mathrm {it}}(x) = x^{( tv _1)} = x - tv _1$ and $\eta _{\mathrm {it}}(y) = y^{( tv _1)} = y + tv _1 \cdot x - \frac{1}{2} tv _1^2 + \frac{1}{2} tv _1$. While $\eta _{\mathrm {it}}(y)$ contains rational coefficients, our approach ensures that $\eta _{\mathrm {it}}$ always maps integers to integers. Thus, we again obtain an integer program. We proceed similarly for the iterated cost of a transition, where we may under-approximate the solution of the recurrence equations $c^{(1)} = c$ and $c^{( tv +1)} = c^{( tv )} + c[x_1/x_1^{( tv )}, \ldots , x_n/x_n^{( tv )}]$. For $t_1$ in Fig. 1, we get $c^{(1)} = 1$ and $c^{( tv _1+1)} = c^{( tv _1)} + 1$ which leads to the closed form $c_{\mathrm {it}}= c^{( tv _1)} = tv _1$.

Theorem 7

(Loop Acceleration). Let $t=(\ell ,\gamma ,\eta ,c,\ell )\in \mathcal {T}$ and let $tv$ be a fresh temporary variable. Moreover, let $\eta _{\mathrm {it}}(x) = \eta ^{ tv }(x)$ for all $x \in \mathcal {PV}$ and let $c_{\mathrm {it}}\!\le \!\sum _{0\le i < tv }\eta ^i(c)$. If $b$ under-estimates $t$, then the processor mapping $\mathcal {T}\!$ to $\mathcal {T}\cup \{ (\ell , \,\gamma \, \wedge \, 0< tv < b+ 1, \, \eta _{\mathrm {it}}, \, c_{\mathrm {it}}, \, \ell ) \}$ is sound.

We say that the resulting new simple loop is accelerated and we refer to all simple loops which were not introduced by Theorem 7 as non-accelerated.

Example 8

(Non-Integer Metering Functions). Theorem 7 also allows metering functions that do not map to the integers. Let $\mathcal {T}= \{(\ell _0, true ,\mathsf {id},1,\ell ),\,t\}$ with $t = (\ell , \, 0<x,\, x'=x-2, \, 1,\, \ell )$. Accelerating $t$ with the metering function $\frac{x}{2}$ yields $(\ell , \, 0< tv <\frac{x}{2}+1, \, x'=x-2 \, tv , \, tv , \, \ell )$. Note that $0< tv <\frac{x}{2}+1$ implies $0 < x$ as $tv$ and x range over $\mathbb {Z}$. Hence, $0 < x$ can be omitted in the resulting guard.

Example 9

(Unbounded Loops Continued). In Example 5, $\omega$ under-estimates $t = (\ell , \, 0 < x, x'=x+1, \, y, \, \ell )$. The accelerated transition is $\overline{t}=(\ell , \, 0 < x \, \wedge \, \gamma ', \, x'=x+ tv , \, tv \cdot y, \ell )$, where $\gamma '$ corresponds to $0< tv < \omega + 1 = \omega$, i.e., $tv$ has no upper bound.

If we cannot find a metering function or fail to obtain the closed form $\eta _{\mathrm {it}}$ or $c_{\mathrm {it}}$ for a simple loop $t$, then we can simplify $t$ by eliminating temporary variables. To do so, we fix their values by adding suitable constraints to $\mathsf {guard}(t)$. As we are interested in witnesses for maximal computations, we use a heuristic that adds constraints $tv = a$ for temporary variables $tv$, where $a\in \mathcal {A}(\mathcal {V}_{\ell })$ is a suitable upper or lower bound on $tv$’s values, i.e., $\mathsf {guard}(t)$ implies $tv \le a$ or $tv \ge a$. This is repeated until we find constraints which allow us to apply loop acceleration. Note that adding additional constraints to $\mathsf {guard}(t)$ is always sound in our setting.

Theorem 10

(Strengthening). Let $t = (\ell ,\gamma ,\eta ,c,\ell ') \in \mathcal {T}$ and $\varphi \in \mathcal {F}(\mathcal {V}_\ell )$. Then the processor mapping $\mathcal {T}$ to $\mathcal {T}\setminus \{t\} \cup \{(\ell , \, \gamma \wedge \varphi , \, \eta , \, c, \, \ell ')\}$ is sound.

In $t_4$ from Fig. 1, $\gamma$ contains $tv > 0$. So $\gamma$ implies the bound $tv \ge 1$ since $tv$ must be instantiated by integers. Hence, we add the constraint $tv = 1$. Now the update $u' = u - tv$ of the transition $t_4$ becomes $u' = u - 1$, and thus, u is a metering function. So after fixing $tv = 1$, $t_4$ can be accelerated similarly to $t_1$.

To simplify the program, we delete a simple loop $t$ after trying to accelerate it. So we just keep the accelerated loop (or none, if acceleration of t still fails after eliminating all temporary variables by strengthening t’s guard). For our example, we obtain the program in Fig. 2 with the accelerated transitions $t_{\overline{1}}$, $t_{\overline{4}}$.

Theorem 11

(Deletion). For $t\!\in \!\mathcal {T}\!\!$, the processor mapping $\mathcal {T}\!$ to $\mathcal {T}\setminus \!\{t\}$ is sound.

Fig. 2.

Accelerating $t_1$ and $t_4$

Fig. 3.

Eliminating $t_{\overline{1}}$ and $t_{\overline{4}}$

4.2 Chaining Transitions

After trying to accelerate all simple loops of a program, we can chain subsequent transitions $t_1, t_2$ by adding a new transition $t_{1.2}$ that simulates their combination. Afterwards, the transitions $t_1$ and $t_2$ can (but need not) be deleted with Theorem 11.

Theorem 12

(Chaining). Let $t_1 = (\ell _1, \gamma _1, \eta _1, c_1, \ell _2)$ and $t_2 = (\ell _2, \gamma _2, \eta _2, c_2, \ell _3)$ with $t_1,t_2 \in \mathcal {T}$. Let $\mathrm {ren}$ be an injective function renaming the variables in $\mathcal {TV}_{\ell _2}$ to fresh ones and let⁵ $t_{1.2} = (\ell _1, \, \gamma _1 \wedge \mathrm {ren}(\eta _1(\gamma _2)), \, \mathrm {ren}\circ \eta _1 \circ \eta _2, \, c_1 + \mathrm {ren}(\eta _1(c_2)), \ell _3)$. Then the processor mapping $\mathcal {T}$ to $\mathcal {T}\cup \{ t_{1.2} \}$ is sound. In the new program $\mathcal {T}\cup \{ t_{1.2} \}$, the temporary variables of $\ell _1$ are defined to be $\mathcal {TV}_{\ell _1} \cup \mathrm {ren}(\mathcal {TV}_{\ell _2})$.

One goal of chaining is loop elimination of all accelerated simple loops. To this end, we chain all subsequent transitions $t', t$ where t is a simple loop and $t'$ is no simple loop. Afterwards, we delete t. Moreover, once $t'$ has been chained with all subsequent simple loops, then we also remove $t'$, since its effect is now covered by the newly introduced (chained) transitions. So in our example from Fig. 2, we chain $t_0$ with $\overline{t}_1$ and $t_3$ with $\overline{t}_4$. The resulting program is depicted in Fig. 3, where we always simplify arithmetic terms and formulas to ease readability.

Chaining also allows location elimination by chaining all pairs of incoming and outgoing transitions for a location $\ell$ and removing them afterwards. It is advantageous to eliminate locations with just a single incoming transition first. This heuristic takes into account which locations were the entry points of loops. So for the example in Fig. 3, it would avoid chaining $t_5$ and $t_{3.\overline{4}}$ in order to eliminate $\ell _2$. In this way, we avoid constructing chained transitions that correspond to a run from the “middle” of a loop to the “middle” of the next loop iteration.

So instead of eliminating $\ell _2$, we chain $t_{0.\overline{1}}$ and $t_{2}$ as well as $t_{3.\overline{4}}$ and $t_{5}$ to eliminate the locations $\ell _1$ and $\ell _3$, leading to the program in Fig. 4. Here, the temporary variables $tv _1$ and $tv _4$ vanish since, before applying arithmetic simplifications, the guards of $t_{0.\overline{1}.2}$ resp. $t_{3.\overline{4}.5}$ imply $tv _1\! =\! x$ resp. $tv _4\! =\! z-1$.

Fig. 4.

Eliminating $\ell _1$ and $\ell _3$

Fig. 5.

Accelerating $t_{3.\overline{4}.5}$

Fig. 6.

Eliminating $t_{\overline{3.\overline{4}.5}}$

Our overall approach for program simplification is shown in Algorithm 1. Of course, this algorithm is a heuristic and other strategies for the application of the processors would also be possible. The set $S$ in Steps 3–5 is needed to handle locations $\ell$ with multiple simple loops. The reason is that each transition $t'$ with $\mathsf {dest}(t') = \ell$ should be chained with each of $\ell$’s simple loops before removing $t'$.

Algorithm 1 terminates: In the loop 2.1–2.2, each iteration decreases the number of temporary variables in $t$. The loop 2 terminates since each iteration reduces the number of non-accelerated simple loops. In loop 4, the number of simple loops is decreasing and for loop 6, the number of reachable locations decreases. The overall loop terminates as it reduces the number of reachable locations. The reason is that the program does not have simple loops anymore when the algorithm reaches Step 6. Thus, at this point there is either a location $\ell$ which can be eliminated or the program does not have a path of length $2$.

According to Algorithm 1, in our example we go back to Step 1 and 2 and apply Loop Acceleration to transition $t_{3.\overline{4}.5}$. This transition has the metering function $z - 1$ and its iterated update sets $u$ to $0$ and $z$ to $z - tv$ for a fresh temporary variable $tv$. To compute $t_{3.\overline{4}.5}$’s iterated costs, we have to find an under-approximation for the solution of the recurrence equations $c^{(1)} = z + 1$ and $c^{( tv +1)} = c^{( tv )} + z^{( tv )} + 1$. After computing the closed form $z - tv$ of $z^{( tv )}$, the second equation simplifies to $c^{( tv +1)} = c^{( tv )} + z - tv + 1$, which results in the closed form $c_{\mathrm {it}}= c^{( tv )} = tv \cdot z-\frac{1}{2} tv ^2 + \frac{3}{2} tv$. In this way, we obtain the program in Fig. 5. A final chaining step and deletion of the only simple loop yields the program in Fig. 6.

5 Asymptotic Lower Bounds for Simplified Programs

After Algorithm 1, all program paths have length $1$. We call such programs simplified and let $\mathcal {T}$ be a simplified program throughout this section. Now for any $\varvec{v}\!\in \!\mathcal {V}\! al _{\ell _0}$,

$$\begin{aligned} \max \{\varvec{v}(\mathsf {cost}(t)) \mid t \in \mathcal {T}, \varvec{v} \ \models \ \mathsf {guard}(t)\}, \end{aligned}$$

(5)

is a lower bound on $\mathcal {T}$’s derivation height $\mathsf {dh}_\mathcal {T}(\varvec{v}|_\mathcal {PV})$, i.e., (5) is the maximal cost of those transitions whose guard is satisfied by $\varvec{v}$. So for the program in Fig. 6, we obtain the bound $\frac{x^2 \cdot tv + x \cdot tv - tv ^2 + 3 tv + 2x + 4}{2}$ for all valuations with $\varvec{v}\models 0< tv < \frac{1}{2}x^2 + \frac{1}{2}x$. However, such bounds do not provide an intuitive understanding of the program’s complexity and are also not suitable to detect possible attacks. Hence, we now show how to derive asymptotic lower bounds for simplified programs. These asymptotic bounds can easily be understood (i.e., a high lower bound can help programmers to improve their program to make it more efficient) and they identify potential attacks. After introducing our notion of asymptotic bounds in Sect. 5.1, we present a technique to derive them automatically in Sect. 5.2.

5.1 Asymptotic Bounds and Limit Problems

While $\mathsf {dh}_\mathcal {T}$ is defined on valuations, asymptotic bounds are usually defined for functions on $\mathbb {N}$. To bridge this gap, we use the common definition of complexity as a function of the size of the input. So the runtime complexity $\mathsf {rc}_\mathcal {T}(n)$ is the maximal cost of any evaluation that starts with a configuration where the sum of the absolute values of all program variables is at most n.

Definition 13

(Runtime Complexity). Let $|\varvec{v}| = \sum _{x \in \mathcal {PV}}|\varvec{v}(x)|$ for all valuations $\varvec{v}$. The runtime complexity $\mathsf {rc}_\mathcal {T}: \mathbb {N}\rightarrow \mathbb {R}_{\ge 0} \cup \{ \omega \}$ is defined as $\mathsf {rc}_\mathcal {T}(n) = \sup \{\mathsf {dh}_\mathcal {T}(\varvec{v}) \mid \varvec{v}\in \mathcal {V}\! al , |\varvec{v}| \le n\}$.

Our goal is to derive an asymptotic lower bound for $\mathsf {rc}_\mathcal {T}$ from a simplified program $\mathcal {T}$. So for the program $\mathcal {T}$ in Fig. 6, we would like to derive $\mathsf {rc}_\mathcal {T}(n) \in \varOmega (n^4)$. As usual, $f(n) \in \varOmega (g(n))$ means that there is an $m > 0$ and an $n_0 \in \mathbb {N}$ such that $f(n) \ge m \cdot g(n)$ holds for all $n \ge n_0$. However, in general, the costs of a transition do not directly give rise to the desired asymptotic lower bound. For instance, in Fig. 6, the costs of the only transition are cubic, but the complexity of the program is a polynomial of degree $4$ (since $tv$ may be quadratic in $x$).

To infer an asymptotic lower bound from a transition $t \in \mathcal {T}$, we try to find an infinite family of valuations $\varvec{v}_n \in \mathcal {V}\! al _{\ell _0}$ (parameterized by $n\in \mathbb {N}$) where there is an $n_0 \in \mathbb {N}$ such that $\varvec{v}_n \ \models \ \mathsf {guard}(t)$ holds for all $n \ge n_0$. This implies $\mathsf {rc}_\mathcal {T}(|\varvec{v}_n|) \in \varOmega (\varvec{v}_n(\mathsf {cost}(t)))$, since for all $n \ge n_0$ we have:

$$ \begin{array}{rcl@{\qquad }l} \mathsf {rc}_\mathcal {T}(|\varvec{v}_n|) &{}\ge &{} \mathsf {dh}_\mathcal {T}(\varvec{v}_n|_{\mathcal {PV}}) &{} \text {as}~ |\, \varvec{v}_n|_{\mathcal {PV}} \, | = |\varvec{v}_n|\\ &{}\ge &{} \varvec{v}_n(\mathsf {cost}(t)) &{} \text {by}~(5) \end{array} $$

We first normalize all constraints in $\mathsf {guard}(t)$ such that they have the form $a > 0$. Now our goal is to find infinitely many models $\varvec{v}_n$ for a formula of the form $\bigwedge _{1 \le i \le k} (a_i > 0)$. Obviously, such a formula is satisfied if all terms $a_i$ are positive constants or increase infinitely towards $\omega$. Thus, we introduce a technique which tries to find out whether fixing the valuations of some variables and increasing or decreasing the valuations of others results in positive resp. increasing valuations of $a_1,\ldots ,a_k$. Our technique operates on so-called limit problems $\{a_1^{\bullet _1},\ldots ,a_k^{\bullet _k}\}$ where $a_i \in \mathcal {A}(\mathcal {V}_{\ell _0})$ and $\bullet _i \in \{+, -, +_!, -_!\}$. Here, $a^+$ (resp. $a^-$) means that a grows towards $\omega$ (resp. $-\omega$) and $a^{+_!}$ (resp. $a^{-_!}$) means that a has to be a positive (resp. negative) constant. So we represent $\mathsf {guard}(t)$ by an initial limit problem $\{ a_1^{\bullet _1},\ldots ,a_k^{\bullet _k} \}$ where $\bullet _i \in \{ +, +_! \}$ for all $1 \le i \le k$. We say that a family of valuations $\varvec{v}_n$ is a solution to a limit problem S iff $\varvec{v}_n$ “satisfies” S for large $n$.

To define this notion formally, for any function $f: \mathbb {N}\rightarrow \mathbb {R}$ we say that $\lim _{n\mapsto \omega } f(n) = \omega$ (resp. $\lim _{n\mapsto \omega } f(n) = -\omega$) iff for every $m \in \mathbb {Z}$ there is an $n_0 \in \mathbb {N}$ such that $f(n) \ge m$ (resp. $f(n) \le m$) holds for all $n \ge n_0$. Similarly, $\lim _{n\mapsto \omega } f(n) = m$ iff there is an $n_0$ such that $f(n) = m$ holds for all $n \ge n_0$.

Definition 14

(Solutions of Limit Problems). For any function $f: \mathbb {N}\rightarrow \mathbb {R}$ and any $\bullet \in \{+, -, +_!, -_!\}$, we say that f satisfies $\bullet$ iff

$$ \begin{array}{l@{\;}l@{\qquad \;\;}l@{\;}l} \lim _{n \mapsto \omega } f(n) = \omega , &{} \text {if } \bullet = + &{} \exists m \in \mathbb {Z}. \; \lim _{n \mapsto \omega } f(n) = m > 0,&{} \text {if } \bullet = +_!\\ \lim _{n \mapsto \omega } f(n) = -\omega , &{} \text {if } \bullet = - &{} \exists m \in \mathbb {Z}. \; \lim _{n \mapsto \omega } f(n) = m < 0, &{} \text {if } \bullet = -_! \end{array}$$

A family $\varvec{v}_n$ of valuations is a solution of a limit problem $S$ iff for every $a^\bullet \in S$, the function $\lambda n.\; \varvec{v}_n(a)$ satisfies $\bullet$. Here, “$\lambda n.\; \varvec{v}_n(a)$” is the function from $\mathbb {N}\rightarrow \mathbb {R}$ that maps any $n \in \mathbb {N}$ to $\varvec{v}_n(a)$.

Example 15

(Bound for Fig. 6 ). In Fig. 6 where $\mathsf {guard}(t)$ is $0< tv < \frac{1}{2}x^2 + \frac{1}{2}x$, the family $\varvec{v}_n$ with $\varvec{v}_n( tv ) = \frac{1}{2}n^2 + \frac{1}{2} n - 1, \varvec{v}_n(x) = n$, and $\varvec{v}_n(y) = \varvec{v}_n(z) = \varvec{v}_n(u) = 0$ is a solution of the initial limit problem $\{ tv ^+, (\frac{1}{2}x^2+\frac{1}{2}x- tv )^{+_!}) \}$. The reason is that the function $\lambda n.\; \varvec{v}_n( tv )$ that maps any $n \in \mathbb {N}$ to $\varvec{v}_n( tv ) = \frac{1}{2}n^2 + \frac{1}{2} n - 1$ satisfies $+$, i.e., $\lim _{n \mapsto \omega } (\frac{1}{2}n^2 + \frac{1}{2} n - 1) = \omega$. Similarly, the function $\lambda n.\; \varvec{v}_n(\frac{1}{2}x^2+\frac{1}{2}x- tv ) = \lambda n.\; 1$ satisfies $+_!$. Section 5.2 will show how to infer such solutions of limit problems automatically. Thus, there is an $n_0$ such that $\varvec{v}_n \ \models \ \mathsf {guard}(t)$ holds for all $n \ge n_0$. Hence, we get the asymptotic lower bound $\mathsf {rc}_\mathcal {T}(|\varvec{v}_n|) \in \varOmega (\varvec{v}_n(\mathsf {cost}(t))) = \varOmega (\frac{1}{8} n^4 + \frac{1}{4} n^3 + \frac{7}{8} n^2 + \frac{7}{4} n) = \varOmega (n^4)$.

Theorem 16

(Asymptotic Bounds for Simplified Programs). Given a transition $t$ of a simplified program $\mathcal {T}$ with $\mathsf {guard}(t) = a_1> 0 \wedge \dots \wedge a_k > 0$, let the family $\varvec{v}_n$ be a solution of an initial limit problem $\{a_1^{\bullet _1},\dots ,a_k^{\bullet _k}\}$ with $\bullet _i \in \{+, +_!\}$ for all $1 \le i \le k$. Then $\mathsf {rc}_{\mathcal {T}}(|\varvec{v}_n|) \in \varOmega (\varvec{v}_n(\mathsf {cost}(t)))$.

Of course, if $\mathcal {T}$ has several transitions, then we try to take the one which results in the highest lower bound. Moreover, one should extend the initial limit problem $\{a_1^{\bullet _1},\dots ,a_k^{\bullet _k}\}$ by $\mathsf {cost}(t)^+$. In this way, one searches for valuations $\varvec{v}_n$ where $\varvec{v}_n(\mathsf {cost}(t))$ depends on n, i.e., where the costs are not constant.

The costs are unbounded (i.e., they only depend on temporary variables) iff the initial limit problem $\{a_1^{\bullet _1},\dots ,a_k^{\bullet _k},\mathsf {cost}(t)^+\}$ has a solution $\varvec{v}_n$ where $\varvec{v}_n(x)$ is constant for all $x \in \mathcal {PV}$. Then we can even infer $\mathsf {rc}_{\mathcal {T}}(n) \in \varOmega (\omega )$. For instance, after chaining the transition $\overline{t}$ of Example 9 with the transition from the start location (see Example 5), the resulting initial limit problem $\{x^{+_!}, tv ^+, ( tv \cdot y + 1)^+\}$ has the solution $\varvec{v}_n$ with $\varvec{v}_n(x) = \varvec{v}_n(y) = 1$ and $\varvec{v}_n( tv ) = n$, which implies $\mathsf {rc}_\mathcal {T}(n) \in \varOmega (\omega )$.

If the costs are not unbounded, we say that they depend on $x \in \mathcal {PV}$ iff the initial limit problem $\{a_1^{\bullet _1},\dots ,a_k^{\bullet _k},\mathsf {cost}(t)^+\}$ has a solution $\varvec{v}_n$ where $\varvec{v}_n(y)$ is constant for all $y \in \mathcal {PV}\setminus \{x\}$. If x corresponds to a “secret”, then the program can be subject to side-channel attacks. For example, in Example 15 we have $\varvec{v}_n(\mathsf {cost}(t)) = \frac{1}{8} n^4 + \frac{1}{4} n^3 + \frac{7}{8} n^2 + \frac{7}{4} n$. Since $\varvec{v}_n$ maps all program variables except x to constants, the costs of our program depend on the program variable x. So if x is “secret”, then the program is not safe from side-channel attacks.

Theorem 16 results in bounds of the form “$\mathsf {rc}_{\mathcal {T}}(|\varvec{v}_n|) \in \varOmega (\varvec{v}_n(c))$”, which depend on the sizes $|\varvec{v}_n|$. Let $f(n) = \mathsf {rc}_\mathcal {T}(n)$, $g(n) = |\varvec{v}_n|$, and let $\varOmega (\varvec{v}_n(c))$ have the form $\varOmega (n^k)$ or $\varOmega (k^n)$ for a $k \in \mathbb {N}$. Moreover for all $x \in \mathcal {PV}$, let $\varvec{v}_n(x)$ be a polynomial of at most degree m, i.e., let $g(n) \in \mathcal {O}(n^m)$. Then the following observation from [15] allows us to infer a bound for $\mathsf {rc}_\mathcal {T}(n)$ instead of $\mathsf {rc}_{\mathcal {T}}(|\varvec{v}_n|)$.

Lemma 17

(Bounds for Function Composition). Let $f: \mathbb {N}\rightarrow \mathbb {R}_{\ge 0}$ and $g: \mathbb {N}\rightarrow \mathbb {N}$ where $g(n) \in \mathcal {O}(n^m)$ for some $m \in \mathbb {N}\setminus \{ 0 \}$. Moreover, let f(n) be weakly and let g(n) be strictly monotonically increasing for large enough n.

• If $f(g(n)) \in \varOmega (n^k)$ with $k \in \mathbb {N}$, then $f(n) \in \varOmega (n^{\frac{k}{m}})$.

• If $f(g(n)) \in \varOmega (k^n)$ with $k \in \mathbb {N}$, then $f(n) \in \varOmega (k^{\root m \of {n}})$.

Example 18

(Bound for Fig. 6 Continued). In Example 15, we inferred $\mathsf {rc}_\mathcal {T}(|\varvec{v}_n|) \in \varOmega (n^4)$ where $\varvec{v}_n(x) = n$ and $\varvec{v}_n(y) = \varvec{v}_n(z) = \varvec{v}_n(u) = 0$. Hence, we have $|\varvec{v}_n| = n \in \mathcal {O}(n^1)$. By Lemma 17, we obtain $\mathsf {rc}_\mathcal {T}(n) \in \varOmega (n^{\frac{4}{1}}) = \varOmega (n^4)$.

Example 19

(Non-Polynomial Bounds). Let $\mathcal {T}\!\!=\!\{(\ell _0,x=y^2,\mathsf {id},y,\ell )\}$. By Definition 14, the family $\varvec{v}_n$ with $\varvec{v}_n(x)=n^2$ and $\varvec{v}_n(y)=n$ is a solution of the initial limit problem $\{(x-y^2+1)^{+_!}, (y^2-x+1)^{+_!}, y^+\}$. Due to Theorem 16, this proves $\mathsf {rc}_\mathcal {T}(|\varvec{v}_n|) \in \varOmega (n)$. As $|\varvec{v}_n| = n^2 + n \in \mathcal {O}(n^2)$, Lemma 17 results in $\mathsf {rc}_\mathcal {T}(n) \in \varOmega (n^{\frac{1}{2}})$.

5.2 Transformation of Limit Problems

A limit problem S is trivial iff all terms in $S$ are variables and there is no variable $x$ with $x^{\bullet _1},x^{\bullet _2} \in S$ and $\bullet _1 \ne \bullet _2$. For trivial limit problems S we can immediately obtain a particular solution $\varvec{v}^{S}_n$ which instantiates variables “according to S”.

Lemma 20

(Solving Trivial Limit Problems). Let $S$ be a trivial limit problem. Then $\varvec{v}_n^{S}$ is a solution of S where for all $n \in \mathbb {N}$, $\varvec{v}_n^{S}$ is defined as follows:

For instance, if $\mathcal {V}_{\ell _0} = \{x,y, tv \}$ and $S=\{x^+,y^{-_!}\}$, then S is a trivial limit problem and $\varvec{v}_n^S$ with $\varvec{v}_n^S(x)=n, \varvec{v}_n^S(y)=-1$, and $\varvec{v}_n^S( tv )=0$ is a solution for $S$.

However, in general the initial limit problem $S = \{a_1^{\bullet _1},\dots ,a_k^{\bullet _k}, \mathsf {cost}(t)^+\}$ is not trivial. Therefore, we now define a transformation $\rightsquigarrow$ to simplify limit problems until one reaches a trivial problem. With our transformation, $S \rightsquigarrow S'$ ensures that each solution of $S'$ also gives rise to a solution of S.

If S contains $f(a_1,a_2)^\bullet$ for some standard arithmetic operation f like addition, subtraction, multiplication, division, and exponentiation, we use a so-called limit vector $(\bullet _1,\bullet _2)$ with $\bullet _i \in \{+,-,+_!,-_!\}$ to characterize for which kinds of arguments the operation f is increasing (if $\bullet = +$) resp. decreasing (if $\bullet = -$) resp. a positive or negative constant (if $\bullet = +_!$ or $\bullet = -_!$).⁶ Then S can be transformed into the new limit problem $S \setminus \{f(a_1,a_2)^{\bullet }\} \cup \{a_1^{\bullet _1},a_2^{\bullet _2}\}$.

For example, $(+,+_!)$ is an increasing limit vector for subtraction. The reason is that $a_1 - a_2$ is increasing if $a_1$ is increasing and $a_2$ is a positive constant. Hence, our transformation $\rightsquigarrow$ allows us to replace $(a_1 - a_2)^+$ by $a_1^+$ and $a_2^{+_!}$.

To define limit vectors formally, we say that $(\bullet _1,\bullet _2)$ is an increasing (resp. decreasing) limit vector for f iff the function $\lambda n. \; f(g(n),h(n))$ satisfies $+$ (resp. −) for any functions g and h that satisfy $\bullet _1$ and $\bullet _2$, respectively. Here, “$\lambda n. \; f(g(n), h(n))$” is the function from $\mathbb {N}\rightarrow \mathbb {R}$ that maps any $n \in \mathbb {N}$ to f(g(n), h(n)). Similarly, $(\bullet _1,\bullet _2)$ is a positive (resp. negative) limit vector for f iff $\lambda n. \; f(g(n),h(n))$ satisfies $+_!$ (resp. $-_!$) for any functions g and h that satisfy $\bullet _1$ and $\bullet _2$, respectively.

With this definition, $(+,+_!)$ is indeed an increasing limit vector for subtraction, since $\lim _{n \mapsto \omega } g(n) = \omega$ and $\lim _{n \mapsto \omega } h(n) = m$ with $m > 0$ implies $\lim _{n \mapsto \omega } (g(n) - h(n)) = \omega$. In other words, if g(n) satisfies $+$ and h(n) satisfies $+_!$, then $g(n) - h(n)$ satisfies $+$ as well. In contrast, $(+,+)$ is not an increasing limit vector for subtraction. To see this, consider the functions $g(n) = h(n) = n$. Both g(n) and h(n) satisfy $+$, whereas $g(n) - h(n) = 0$ does not satisfy $+$. Similarly, $(+_!,+_!)$ is not a positive limit vector for subtraction, since for $g(n) = 1$ and $h(n) = 2$, both g(n) and h(n) satisfy $+_!$, but $g(n) - h(n) = -1$ does not satisfy $+_!$.

Limit vectors can be used to simplify limit problems, cf. (A) in the following definition. Moreover, for numbers $m \in \mathbb {Z}$, one can easily simplify constraints of the form $m^{+_!}$ and $m^{-_!}$ (e.g., $2^{+_!}$ is obviously satisfied since $2 > 0$), cf. (B).

Definition 21

( $\rightsquigarrow$ ). Let $S$ be a limit problem. We have:

Example 22

(Bound for Fig. 6 Continued). For the initial limit problem from Example 15, we have $\{ tv ^+, (\frac{1}{2}x^2+\frac{1}{2}x- tv )^{+_!} \} \leadsto \{ tv ^+, (\frac{1}{2}x^2+\frac{1}{2}x)^{+_!}, tv ^{-_!}\} \leadsto \{ tv ^+, (\frac{1}{2}x^2)^{+_!}, (\frac{1}{2}x)^{+_!}, tv ^{-_!}\} \leadsto ^* \{ tv ^+, x^{+_!}, tv ^{-_!}\}$ using the positive limit vector $(+_!,-_!)$ for subtraction and the positive limit vector $(+_!,+_!)$ for addition.

The resulting problem in Example 22 is not trivial as it contains $tv ^{+}$ and $tv ^{-_!}$, i.e., we failed to compute an asymptotic lower bound. However, if we substitute $tv$ with its upper bound $\frac{1}{2}x^2 + \frac{1}{2} x - 1$, then we could reduce the initial limit problem to a trivial one. Hence, we now extend $\rightsquigarrow$ by allowing to apply substitutions.

Definition 23

( $\rightsquigarrow$ Continued). Let $S$ be a limit problem and let $\sigma :\mathcal {V}_{\ell _0} \rightarrow \mathcal {A}(\mathcal {V}_{\ell _0})$ be a substitution such that $x$ does not occur in $x\sigma$ and $\varvec{v}(x\sigma ) \in \mathbb {Z}$ for all valuations $\varvec{v}\in \mathcal {V}\! al _{\ell _0}$ and all $x \in \mathcal {V}_{\ell _0}$. Then we have⁷

Example 24

(Bound for Fig. 6 Continued). For the initial limit problem from Example 15, we now have⁸ $\{ tv ^+, (\frac{1}{2}x^2+\frac{1}{2}x- tv )^{+_!} \} \leadsto ^{[ tv / \frac{1}{2}x^2 + \frac{1}{2} x - 1]} \{ (\frac{1}{2}x^2 + \frac{1}{2} x - 1)^+, 1^{+_!} \} \leadsto \{ (\frac{1}{2}x^2 + \frac{1}{2} x - 1)^+\} \leadsto \{ (\frac{1}{2}x^2 + \frac{1}{2} x)^+, 1^{+_!}\} \leadsto ^* \{x^+\}$, which is trivial.

Although Definition 23 requires that variables may only be instantiated by integer terms, it is also useful to handle limit problems that contain non-integer terms.

Example 25

(Non-Integer Metering Functions Continued). After chaining the accelerated transition of Example 8 with the transition from the start location, for the resulting initial limit problem we get $\{ tv ^+, (\frac{1}{2}x - tv + 1)^{+_!}, ( tv + 1)^+ \} \leadsto ^2 \{ tv ^+, (\frac{1}{2}x - tv + 1)^{+_!}\} \leadsto ^{[x/2 tv -1]} \{ tv ^+, \frac{1}{2}^{+_!}\} \leadsto \{ tv ^+, 1^{+_!}, 2^{+_!}\} \leadsto ^2 \{ tv ^+\}$, using the positive limit vector $(+_!,+_!)$ for division. This allows us to infer $\mathsf {rc}_\mathcal {T}(n)\!\in \!\varOmega (n)$.

However, up to now we cannot prove that, e.g., a transition $t$ with $\mathsf {guard}(t) = x^2 - x > 0$ and $\mathsf {cost}(t) = x$ has a linear lower bound, since $(+,+)$ is not an increasing limit vector for subtraction. To handle such cases, the following rules allow us to neglect polynomial sub-expressions if they are “dominated” by other polynomials of higher degree or by exponential sub-expressions.

Definition 26

( $\rightsquigarrow$ Continued). Let $S$ be a limit problem, let $\pm \in \{+,-\}$, and let $a,b,e \in \mathcal {A}(\{x\})$ be (univariate) polynomials. Then we have:

Thus, $\{ (x^2 - x)^+ \} \leadsto \{ (x^2)^+ \} = \{ (x \cdot x)^+ \} \leadsto \{ x^+ \}$ by the increasing limit vector $(+, +)$ for multiplication. Similarly, $\{ (2^x - x^3)^+ \} \leadsto \{ (2-1)^{+_!}, x^+ \} \leadsto \{x^+ \}$. Rule (E) can also be used to handle problems like $(a^e)^+$ (by choosing $b = 0$).

Theorem 27 states that $\leadsto$ is indeed correct. When constructing the valuation from the resulting trivial limit problem, one has to take the substitutions into account which were used in the derivation. Here, $(\varvec{v}_n \circ \sigma )(x)$ stands for $\varvec{v}_n(\sigma (x))$.

Theorem 27

(Correctness of $\leadsto$ ). If $S \leadsto ^{\sigma } S'$ and the family $\varvec{v}_n$ is a solution of $S'$, then $\varvec{v}_n \circ \sigma$ is a solution of S.

Example 28

(Bound for Fig. 6 Continued). Example 24 leads to the solution $\varvec{v}'_n \circ \sigma$ of the initial limit problem for the program from Fig. 6 where $\sigma = [ tv /\frac{1}{2}x^2+\frac{1}{2}x-1]$, $\varvec{v}'_n(x) = n$, and $\varvec{v}'_n( tv ) = \varvec{v}'_n(y) = \varvec{v}'_n(z) = \varvec{v}'_n(u) = 0$. Hence, $\varvec{v}'_n \circ \sigma = \varvec{v}_n$ where $\varvec{v}_n$ is as in Example 15. As explained in Example 18, this proves $\mathsf {rc}_\mathcal {T}(n) \in \varOmega (n^4)$.

So we start with an initial limit problem $S=\{ a_1^{\bullet _1}, \ldots , a_k^{\bullet _k}, \mathsf {cost}(t)^+\}$ that represents $\mathsf {guard}(t)$ and requires non-constant costs, and transform S with $\rightsquigarrow$ into a trivial $S'$, i.e., $S \leadsto ^{\sigma _1} \ldots \leadsto ^{\sigma _m} S'$. For automation, one should leave the $\bullet _i$ in the initial problem S open, and only instantiate them by a value from $\{+, +_!\}$ when this is needed to apply a particular rule for the transformation $\rightsquigarrow$. Then the resulting family $\varvec{v}^{S'}_n$ of valuations gives rise to a solution $\varvec{v}^{S'}_n \circ \sigma _m \circ \ldots \circ \sigma _1$ of S. Thus, we have $\mathsf {rc}_\mathcal {T}(|\varvec{v}^{S'}_n \circ \sigma |) \in \varOmega (\varvec{v}^{S'}_n(\sigma (\mathsf {cost}(t))))$, where $\sigma = \sigma _m \circ \ldots \circ \sigma _1$, which leads to a lower bound for $\mathsf {rc}_\mathcal {T}(n)$ with Lemma 17.

Our implementation uses the following strategy to apply the rules from Definitions 21, 23, 26 for $\leadsto$. Initially, we reduce the number of variables by propagating bounds implied by the guard, i.e., if $\gamma \!\implies \!x \ge a$ or $\gamma \!\implies \!x \le a$ for some $a \in \mathcal {A}(\mathcal {V}_{\ell _0}\setminus \{x\})$, then we apply the substitution $[x / a]$ to the initial limit problem by rule (C). For example, we simplify the limit problem from Example 19 by instantiating $x$ with $y^2$, as the guard of the corresponding transition implies $x=y^2$. So here, we get $\{(x-y^2+1)^{+_!},(y^2-x+1)^{+_!}, y^+\} \leadsto ^{[x/y^2]} \{1^{+_!}, y^+\} \leadsto \{y^+\}$. Afterwards, we use (B) and (D) with highest and (E) with second highest priority. The third priority is trying to apply (A) to univariate terms (since processing univariate terms helps to guide the search). As fourth priority, we apply (C) with a substitution [x / m] if $x^{+_!}$ or $x^{-_!}$ in S, where we use SMT solving to find a suitable $m \in \mathbb {Z}$. Otherwise, we apply (A) to multivariate terms. Since $\leadsto$ is well founded and, except for (C), finitely branching, one may also backtrack and explore alternative applications of $\leadsto$. In particular, we backtrack if we obtain a contradictory limit problem. Moreover, if we obtain a trivial $S'$ where $\varvec{v}_n^{S'}(\sigma (\mathsf {cost}(t)))$ is a polynomial, but $\mathsf {cost}(t)$ is a polynomial of higher degree or an exponential function, then we backtrack to search for other solutions which might lead to a higher lower bound. However, our implementation can of course fail, since solvability of limit problems is undecidable (due to Hilbert’s Tenth Problem).

6 Experiments and Conclusion

We presented the first technique to infer lower bounds on the worst-case runtime complexity of integer programs, based on a modular program simplification framework. The main simplification technique is loop acceleration, which relies on recurrence solving and metering functions, an adaptation of classical ranking functions. By eliminating loops and locations via chaining, we eventually obtain simplified programs. We presented a technique to infer asymptotic lower bounds from simplified programs, which can also be used to find vulnerabilities.

Our implementation LoAT (“Lower Bounds Analysis Tool”) is freely available at [23]. It was inspired by KoAT [8], which alternates runtime- and size-analysis to infer upper bounds in a modular way. Similarly, LoAT alternates runtime-analysis and recurrence solving to transform loops to loop-free transitions independently. LoAT uses the recurrence solver PURRS [4] and the SMT solver Z3 [10].

We evaluated LoAT on the benchmarks [5] from the evaluation of [8]. We omitted 50 recursive programs, since our approach cannot yet handle recursion. As we know of no other tool to compute worst-case lower bounds for integer programs, we compared our results with the asymptotically smallest results of leading tools for upper bounds: KoAT, CoFloCo [14], Loopus [26], RanK [2]. We did not compare with PUBS [1], since the cost relations analyzed by PUBS significantly differ from the integer programs handled by LoAT. Moreover, as PUBS computes best-case lower bounds, such a comparison would be meaningless since the worst-case lower bounds computed by LoAT are no valid best-case lower bounds. We used a timeout of 60 s. In the following, we disregard 132 examples where $\mathsf {rc}_\mathcal {T}(n) \in \mathcal {O}(1)$ was proved since there is no non-trivial lower bound in these cases.

LoAT infers non-trivial lower bounds for 393 (78 %) of the remaining 507 examples. Tight bounds (i.e., the lower and the upper bound coincide) are proved in 341 cases (67 %). Whenever an exponential upper bound is proved, LoAT also proves an exponential lower bound (i.e., $\mathsf {rc}_\mathcal {T}(n) \in \varOmega (k^n)$ for some $k > 1$). In 173 cases, LoAT infers unbounded runtime complexity. In some cases, this is due to non-termination, but for this particular goal, specialized tools are more powerful (e.g., whenever LoAT proves unbounded runtime complexity due to non-termination, the termination analyzer T2 [7] shows non-termination as well). The average runtime of LoAT was 2.4 s per example. These results could be improved further by supplementing LoAT with invariant inference as implemented in tools like APRON [20]. For a detailed experimental evaluation of our implementation as well as the sources and a pre-compiled binary of LoAT we refer to [16].