Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis

TL;DR

This paper introduces a general-purpose control-flow refinement technique using partial evaluation of Horn clauses, enhancing program analysis precision, termination proofs, and complexity inference for integer transition systems.

Contribution

It presents a novel application of partial evaluation for control-flow refinement, ensuring soundness and enabling termination and complexity analysis for challenging programs.

Findings

Effective control-flow refinement improves analysis precision.

The technique proves termination and infers complexity where other tools fail.

Integration with analyzers demonstrates practical benefits.

Abstract

Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precision. Several techniques have been suggested for different programming models, typically tailored to improving precision for a particular analysis. In this paper we explore the use of partial evaluation of Horn clauses as a general-purpose technique for control-flow refinement for integer transitions systems. These are control-flow graphs where edges are annotated with linear constraints describing transitions between corresponding nodes, and they are used in many program analysis tools. Using partial evaluation for control-flow refinement has the clear advantage over other approaches in that soundness follows from the general properties of partial evaluation; in particular, properties such as termination and complexity are preserved. We use a partial evaluation algorithm incorporating property-based abstraction, and show how the right choice of properties allows us to prove termination and to infer complexity of challenging programs that cannot be handled by state-of-the-art tools. We report on the integration of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers. Under consideration for acceptance in TPLP.

Tables

Table 1. Table 1: Termination benchmarks

	LRF			LLRF
Props	${\mathrm{𝙲𝙵𝚁}}_{𝙱}$	${\mathrm{𝙲𝙵𝚁}}_{𝚂}$	${\mathrm{𝙲𝙵𝚁}}_{𝙰}$	${\mathrm{𝙲𝙵𝚁}}_{𝙱}$	${\mathrm{𝙲𝙵𝚁}}_{𝚂}$	${\mathrm{𝙲𝙵𝚁}}_{𝙰}$
$P_1$	36 (34.36, 22.22%)	38 (27.72, 14.51%)	39 (32.24, 17.59%)	8 (32.15, 7.42%)	7 (35.35, 3.72%)	9 (32.96, 3.49%)	SET-1 LRFs =(106,8.10) LLRFs =(36,14.61)
$P_2$	11 (25.35, 23.41%)	15 (23.01, 9.77%)	14 (26.75, 13.88%)	7 (26.94, 8.81%)	4 (32.61, 2.24%)	7 (31.78, 2.97%)
$P_3$	36 (34.08, 22.27%)	38 (27.71, 14.59%)	39 (32.21, 17.64%)	8 (31.52, 6.67%)	7 (35.03, 3.46%)	9 (33.64, 3.68%)
$P_4$	37 (72.97, 42.16%)	39 (44.81, 26.28%)	40 (51.64, 30.21%)	8 (42.45, 14.72%)	7 (38.64, 10.04%)	9 (35.99, 7.95%)
$P_5$	27 (38.65, 35.86%)	28 (28.32, 18.68%)	30 (31.95, 21.84%)	7 (35.17, 9.20%)	4 (37.06, 4.53%)	8 (37.84, 4.07%)
$P_6$	37 (43.77, 30.39%)	39 (33.40, 21.38%)	40 (37.95, 23.87%)	8 (40.10, 8.89%)	7 (40.50, 4.90%)	9 (40.75, 4.55%)
$P_7$	27 (41.32, 38.83%)	28 (28.98, 19.99%)	30 (32.94, 23.42%)	7 (36.52, 9.60%)	4 (37.15, 4.88%)	8 (37.86, 4.32%)
$P_1$	134 (323.64, 9.15%)	153 (313.34, 5.60%)	145 (318.82, 5.98%)	17 (262.02, 1.05%)	14 (271.65, 0.56%)	18 (264.59, 0.68%)	SET-2 LRFs =(338,159.57) LLRFs =(82,216.96)
$P_2$	28 (267.62, 9.34%)	131 (267.23, 3.86%)	96 (289.86, 5.21%)	3 (255.07, 0.59%)	3 (256.33, 0.41%)	4 (257.88, 0.36%)
$P_3$	134 (322.07, 9.07%)	153 (298.56, 5.13%)	145 (343.52, 7.00%)	17 (262.39, 1.14%)	14 (268.12, 0.59%)	18 (265.39, 0.64%)
$P_4$	139 (397.58, 17.17%)	162 (331.17, 12.23%)	155 (385.73, 13.94%)	22 (252.21, 3.05%)	16 (266.69, 1.16%)	20 (268.29, 1.63%)
$P_5$	63 (333.06,12.54%)	151 (306.14, 8.52%)	123 (348.52, 8.57%)	19 (243.81, 2.55%)	13 (254.39, 1.07%)	17 (248.11, 1.04%)
$P_6$	159 (369.12, 12.08%)	178 (334.32, 9.12%)	167 (386.57, 9.52%)	23 (255.62, 2.42%)	19 (261.76, 1.37%)	23 (254.75, 1.12%)
$P_7$	64 (335.33, 12.72%)	150 (307.83, 8.51%)	123 (349.56, 9.29%)	19 (243.97, 2.65%)	13 (255.42, 1.13%)	18 (248.11, 1.08%)
$P_1$	26 (15.27, 23.67%)	21 (14.56, 19.99%)	25 (14.35, 20.18%)	9 (7.78, 6.25%)	7 (9.11, 3.66%)	11 (7.55, 6.35%)	SET-3 LRFs =(112,4.99) LLRFs =(25,2.30)
$P_2$	4 (11.21, 24.49%)	2 (10.60, 16.68%)	3 (11.11, 17.53%)	6 (4.12, 17.92%)	2 (8.67, 2.73%)	6 (7.17, 6.18%)
$P_3$	25 (15.13, 24.75%)	22 (13.18, 20.75%)	24 (14.83, 21.19%)	9 (7.68, 5.94%)	7 (9.12, 3.71%)	10 (9.09, 4.39%)
$P_4$	30 (25.45, 27.80%)	26 (17.33, 29.18%)	29 (22.59, 35.19%)	12 (5.00, 31.22%)	9 (8.69, 5.04%)	12 (9.11, 6.15%)
$P_5$	20 (14.58, 31.77%)	17 (14.45, 29.05%)	20 (15.30, 28.09%)	9 (3.89, 28.00%)	6 (8.07, 12.94%)	10 (7.68, 11.45%)
$P_6$	33 (21.34, 33.30%)	29 (16.65, 29.77%)	33 (19.18, 29.75%)	12 (4.79, 26.38%)	9 (8.63, 14.17%)	13 (7.34, 13.01%)
$P_7$	21 (15.05, 32.35%)	18 (13.27, 28.77%)	20 (14.95, 27.28%)	9 (3.35, 33.08%)	6 (8.78, 5.40%)	10 (7.46, 10.07%)

Equations

$$\begin{array}[]{r@{}l}\varphi_{0}\equiv&\mathtt{ID}({x,y,z})\\ \varphi_{1}\equiv&x>0{\wedge}\mathtt{ID}({x,y,z})\\ \varphi_{2}\equiv&x\leq 0{\wedge}\mathtt{ID}({x,y,z})\\ \varphi_{3}\equiv&y<z{\wedge}y^{\prime}=y+1{\wedge}\mathtt{ID}({x,z})\\ \varphi_{4}\equiv&y\geq z{\wedge}x^{\prime}=x-1{\wedge}\mathtt{ID}({y,z})\\ \end{array}$$

$$\begin{array}[]{r@{}l}\varphi_{5}\equiv&x>0{\wedge}y<z{\wedge}y^{\prime}=y+1{\wedge}\mathtt{ID}({x,z})\\ \varphi_{6}\equiv&x>0{\wedge}y\geq z{\wedge}x^{\prime}=x-1{\wedge}\mathtt{ID}({y,z})\\ \varphi_{7}\equiv&x>0{\wedge}y\geq z{\wedge}\mathtt{ID}({x,y,z})\\ \varphi_{8}\equiv&x\leq 0{\wedge}y\geq z{\wedge}\mathtt{ID}({x,y,z})\\ \end{array}$$

$$\begin{array}[]{r@{}l}\\ \varphi_{0}\equiv&h\geq 0{\wedge}h<n{\wedge}t\geq 0{\wedge}t<n{\wedge}n>0{\wedge}\mathtt{ID}({h,t,n})\\ \varphi_{1}\equiv&h>t{\wedge}\mathtt{ID}({h,t,n})\\ \varphi_{2}\equiv&h<t{\wedge}\mathtt{ID}({h,t,n})\\ \varphi_{6}\equiv&h<n-1{\wedge}h>t{\wedge}h^{\prime}=h+1{\wedge}\mathtt{ID}({t,n})\\ \end{array}\begin{array}[]{r@{}l}\\ \varphi_{3}\equiv&h<n-1{\wedge}h^{\prime}=h+1{\wedge}\mathtt{ID}({t,n})\\ \varphi_{4}\equiv&h\geq n-1{\wedge}h^{\prime}=0{\wedge}\mathtt{ID}({t,n})\\ \varphi_{5}\equiv&h=t{\wedge}\mathtt{ID}({h,t,n})\\ \varphi_{7}\equiv&h=n-1{\wedge}h^{\prime}=0{\wedge}\mathtt{ID}({t,n})\\ \end{array}$$

$$\begin{array}[]{r@{}l}\varphi_{0}\equiv&i^{\prime}=1{\wedge}w^{\prime}=1{\wedge}z^{\prime}=n{\wedge}c^{\prime}=0{\wedge}\mathtt{ID}({n})\\ \varphi_{1}\equiv&w\leq 2{\wedge}\mathtt{ID}({c,i,n,w,z})\\ \varphi_{2}\equiv&w\geq 1{\wedge}c^{\prime}\geq 0{\wedge}c^{\prime}\leq 1{\wedge}\mathtt{ID}({i,n,w,z})\\ \varphi_{3}\equiv&z<1{\wedge}\mathtt{ID}({c,i,n,w,z})\\ \varphi_{4}\equiv&z\geq 1{\wedge}z^{\prime}=z-1{\wedge}\mathtt{ID}({c,i,n,w})\\ \varphi_{5}\equiv&i\geq 1{\wedge}c\leq 0{\wedge}i^{\prime}=i-1{\wedge}\mathtt{ID}({c,n,w,z})\\ \end{array}$$

$$\begin{array}[]{r@{}l}\varphi_{6}\equiv&i\leq 0{\wedge}i^{\prime}=2{\wedge}z^{\prime}=n{\wedge}\mathtt{ID}({c,n,w})\\ \varphi_{7}\equiv&c\leq 0{\wedge}w^{\prime}=w-1{\wedge}\mathtt{ID}({c,i,n,z})\\ \varphi_{8}\equiv&c>0{\wedge}w^{\prime}=w+1{\wedge}\mathtt{ID}({c,i,n,z})\\ \varphi_{9}\equiv&i\geq 1{\wedge}c>0{\wedge}\mathtt{ID}({c,i,n,w,z})\\ \varphi_{10}\equiv&w>2{\wedge}\mathtt{ID}({c,i,n,w,z})\\ \varphi_{11}\equiv&w<1{\wedge}\mathtt{ID}({c,i,n,w,z})\\ \end{array}$$

$$\begin{array}[]{r@{}l}\varphi_{0}\equiv&\mathtt{ID}({x,y,z})\\ \varphi_{2}\equiv&x<0{\wedge}\mathtt{ID}({x,y,z})\\ \varphi_{3}\equiv&z\geq 0{\wedge}\mathtt{ID}({x,y,z})\\ \varphi_{4}\equiv&z<0{\wedge}y\geq 0{\wedge}\mathtt{ID}({x,y,z})\\ \varphi_{1}\equiv&x\geq 0{\wedge}x^{\prime}=x+y{\wedge}y^{\prime}=y+z{\wedge}z^{\prime}=z-1\\ \end{array}$$

$$\begin{array}[]{r@{}l}\varphi_{5}\equiv&z<0{\wedge}y<0{\wedge}x\geq 0{\wedge}\mathtt{ID}({x,y,z})\\ \varphi_{6}\equiv&z<0{\wedge}y<0{\wedge}x<0{\wedge}\mathtt{ID}({x,y,z})\\ \end{array}$$

$$\begin{array}[]{llllll}q_{\mathtt{n_{0}}}(\bar{x})\leftarrow\varphi_{0},q_{\mathtt{n_{1}}}(\bar{x}^{\prime}).&~{}~{}q_{\mathtt{n_{1}}}(\bar{x})\leftarrow\varphi_{1},q_{\mathtt{n_{2}}}(\bar{x}^{\prime}).&~{}~{}q_{\mathtt{n_{1}}}(\bar{x})\leftarrow\varphi_{2},q_{\mathtt{n_{3}}}(\bar{x}^{\prime}).\\ q_{\mathtt{n_{2}}}(\bar{x})\leftarrow\varphi_{3},q_{\mathtt{n_{1}}}(\bar{x}^{\prime}).&~{}~{}q_{\mathtt{n_{2}}}(\bar{x})\leftarrow\varphi_{4},q_{\mathtt{n_{1}}}(\bar{x}^{\prime}).\\ \end{array}$$

$$\begin{array}[]{l}q_{\mathtt{n_{2}}}(x,y,z)\leftarrow x>0,z>y,y^{\prime}=y-1,q_{\mathtt{n_{1}}}(x,y^{\prime},z)\\ q_{\mathtt{n_{2}}}(x,y,z)\leftarrow x>0,y\geq z,x^{\prime}=x-1,q_{\mathtt{n_{1}}}(x^{\prime},y,z).\end{array}$$

$$\begin{array}[]{lcl}\alpha(x>0)=x>0&{}{}{}{}{}{}{}{}{}{}\hfil&\alpha(x>-1\wedge y\geq z)=y\geq z.\end{array}$$

$$\begin{array}[]{lll|lll}\langle q_{\mathtt{n_{1}}}(x,y,z),\mathit{true}\rangle&\Rightarrow&q_{\mathtt{n_{1}^{3}}}(x,y,z)&~{}~{}\langle q_{\mathtt{n_{2}}}(x,y,z),x>0\rangle&\Rightarrow&q_{\mathtt{n_{2}^{2}}}(x,y,z)\\ \langle q_{\mathtt{n_{1}}}(x,y,z),x>0\rangle&\Rightarrow&q_{\mathtt{n_{1}^{2}}}(x,y,z){}{}&~{}~{}\langle q_{\mathtt{n_{2}}}(x,y,z),x>0\wedge y\geq z\rangle&\Rightarrow&q_{\mathtt{n_{1}^{2}}}(x,y,z)\\ \langle q_{\mathtt{n_{1}}}(x,y,z),y\geq z\rangle&\Rightarrow&q_{\mathtt{n_{1}^{1}}}(x,y,z)&~{}~{}\langle q_{\mathtt{n_{3}}}(x,y,z),x\leq 0\rangle&\Rightarrow&q_{\mathtt{n_{3}^{2}}}(x,y,z)\\ &&&~{}~{}\langle q_{\mathtt{n_{3}}}(x,y,z),x\leq 0,y\geq z\rangle&\Rightarrow&q_{\mathtt{n_{3}^{1}}}(x,y,z)\end{array}$$

$$\begin{array}[]{llllll}q_{\mathtt{n_{0}}}(\bar{x})\leftarrow\varphi_{0},q_{\mathtt{n_{1}^{3}}}(\bar{x}).&~{}~{}q_{\mathtt{n_{1}^{3}}}(\bar{x})\leftarrow\varphi_{2},q_{\mathtt{n_{3}^{2}}}(\bar{x}).&~{}~{}q_{\mathtt{n_{1}^{3}}}(\bar{x})\leftarrow\varphi_{1},q_{\mathtt{n_{2}^{2}}}(\bar{x}).\\ q_{\mathtt{n_{2}^{2}}}(\bar{x})\leftarrow\varphi_{5},q_{\mathtt{n_{1}^{2}}}(\bar{x}).&~{}~{}q_{\mathtt{n_{2}^{2}}}(\bar{x})\leftarrow\varphi_{6},q_{\mathtt{n_{1}^{1}}}(\bar{x}).&~{}~{}q_{\mathtt{n_{1}^{2}}}(\bar{x})\leftarrow\varphi_{1},q_{\mathtt{n_{2}^{2}}}(\bar{x}).\\ q_{\mathtt{n_{1}^{1}}}(\bar{x})\leftarrow\varphi_{8},q_{\mathtt{n_{3}^{1}}}(\bar{x}).&~{}~{}q_{\mathtt{n_{1}^{1}}}(\bar{x})\leftarrow\varphi_{7},q_{\mathtt{n_{2}^{1}}}(\bar{x}).&~{}~{}q_{\mathtt{n_{2}^{1}}}(\bar{x})\leftarrow\varphi_{6},q_{\mathtt{n_{1}^{1}}}(\bar{x}).\\ \end{array}$$

$$\begin{array}[]{ll@{}l}\mathtt{PR_{h}}(q_{\mathtt{n_{i}}})&=&~{}\{\psi\mid q_{\mathtt{n_{i}}}(\bar{x})\leftarrow\varphi,q_{\mathtt{n_{j}}}(\bar{x}^{\prime})\in\mathtt{HC}({{\cal T}}),\psi=\mathtt{proj}_{\bar{x}}(\varphi)\}\\ \mathtt{PR_{hv}}(q_{\mathtt{n_{i}}})&=&~{}\{x_{\ell}\diamond c\mid q_{\mathtt{n_{i}}}(\bar{x})\leftarrow\varphi,q_{\mathtt{n_{j}}}(\bar{x}^{\prime})\in\mathtt{HC}({{\cal T}}),\ell\in[1..n],\diamond\in\{\leq,\geq\},\varphi\models x_{\ell}\diamond c\}\\ \mathtt{PR_{c}}(q_{\mathtt{n_{i}}})&=&~{}\{\psi[\bar{x}^{\prime}/\bar{x}]\mid q_{\mathtt{n_{j}}}(\bar{x})\leftarrow\varphi,q_{\mathtt{n_{i}}}(\bar{x}^{\prime})\in\mathtt{HC}({{\cal T}}),\psi=\mathtt{proj}_{\bar{x}^{\prime}}(\varphi)\}\\ \mathtt{PR_{cv}}(q_{\mathtt{n_{i}}})&=&~{}\{x_{\ell}\diamond c\mid q_{\mathtt{n_{j}}}(\bar{x})\leftarrow\varphi,q_{\mathtt{n_{i}}}(\bar{x}^{\prime})\in\mathtt{HC}({{\cal T}}),\ell\in[1..n],\diamond\in\{\leq,\geq\},\varphi\models x^{\prime}_{\ell}\diamond c\}\\ \end{array}$$

Full text

1 Introduction

Control-flow refinement (CFR) is used in program analysis to make the implicit control-flow of a given program explicit. Consider for example the program on the left:

⬇

while ( x > 0 )

if ( y < z ) y++; else x--;

⬇

while (x > 0 && y < z) y++;

while (x > 0 && y >= z) x--;

Its execution has two implicit phases: in the first one, $\mathtt{y}$ is incremented until it reaches the value of $\mathtt{z}$, and in the second phase $\mathtt{x}$ is decremented until it reaches $\mathtt{0}$. CFR techniques transform this program into the one on the right, in which the two phases are explicit. For termination analysis, the transformation simplifies the termination proof; while the original program requires a lexicographic termination argument, the transformed one requires only linear ones. There are also cases where it is not possible to prove termination without such transformations. For cost analysis, tools based on bounding loop iterations using linear ranking functions fail to infer the cost of the first program, while a linear upper-bound can be inferred for the second. CFR also helps in inferring more precise invariants, without the need for disjunctive abstract domains.

\citeN

GulwaniJK09 and \citeNFlores-MontoyaH14 used CFR to improve the precision of cost analysis. Roughly, they explore different combinations of the paths of a given loop in order to discover execution patterns, and then transform the loop to follow these patterns. \citeNSharmaDDA11 used CFR to improve invariants in order to prove assertions. Their technique is based on finding a splitter predicate such that when it holds one part of the loop is executed and when it does not hold another part is executed. The loop is then rewritten as two consecutive loops, where the predicate is required to hold in one and not to hold in the other. For the loop above, $y<z$ is a splitter predicate.

Since CFR is, in principle, a program transformation that specializes a programs to distinguish different execution scenarios, a natural question to ask is whether such a specialization can be achieved by partial evaluation, which is a general-purpose specialization technique. Using partial evaluation for CFR has the advantage that soundness comes for free, and that it is not tailored for a particular purpose but rather can be tuned depending on the application domain. In this paper we apply partial evaluation for CFR of integer transition systems, which are control-flow graphs where edges are annotated with formulas describing transitions, and can be represented as Horn clause programs. This is a very popular model that is often used in static analysis, and thus many tools would benefit from a CFR procedure for this setting. We use the partial evaluation technique of \citeNGallagher19 that specializes Horn clause programs with respect to a set of predefined properties. For example, partial evaluation of the loop discussed above using the properties $x>0$ and $y<z$ automatically discovers the two phases. Note that the right choice of properties is crucial for achieving the desired refinements.

The contributions are: (1) we suggest heuristics for inferring properties for partial evaluation automatically; (2) we discuss the use of CFR for termination analysis, using an algorithm that applies CFR only when needed, and for cost analysis as a preprocessing step; (3) we suggest the use of termination witnesses (ranking functions) as properties for CFR in order to improve precision of cost analysis; and (4) we provide a publicly available implementation and corresponding experimental evaluation that demonstrates the usefulness of our CFR procedure.

Sect. 2 gives some necessary background; Sect. 3 describes a CFR procedure that is based on using partial evaluation; Sect. 4 discusses the use of our CFR procedure in the context of termination and cost analyses; Sect. 5 discusses an implementation and experimental evaluation, and Sect. 6 concludes and discusses related and future work.

2 Preliminaries

In this section we define the programming model, integer transition systems, that we will use throughout this paper and provide some necessary related background.

We let $V$ be a fixed set of integer-valued variables $\{x_{1},\ldots,x_{n}\}$. A linear constraint $\psi$ is of the form $a_{0}+a_{1}x_{1}+\cdots+a_{n}x_{n}\diamond 0$ where $\diamond\in\{>,<,\geq,\leq,=\}$, $a_{i}$ are integer coefficients, and $x_{i}\in V$. An assignment $\sigma:V\mapsto\mathds{Z}$ is a mapping that assigns integer values to variables. We say that $\sigma$ is a solution for $\psi$ if $a_{0}+\sum_{i}a_{i}\sigma(x_{i})\diamond 0$ is $\mathit{true}$. The set of all solutions for $\psi$ is denoted by $[\![{\psi}]\!]$. A formula $\varphi$ is a conjunction of linear constraints of the form $\psi_{1}\wedge\cdots\wedge\psi_{k}$, and its set of solutions is $[\![{\varphi}]\!]=[\![{\psi_{1}}]\!]\cap\cdots\cap[\![{\psi_{k}}]\!]$. We write $\varphi_{1}\models\varphi_{2}$ for $[\![{\varphi_{1}}]\!]\subseteq[\![{\varphi_{2}}]\!]$. The projection of a formula $\varphi$ onto variables $X\subseteq V$, denoted as $\mathtt{proj}_{X}(\varphi)$, is a formula $\varphi^{\prime}$ such that $[\![{\varphi^{\prime}}]\!]$ coincide with $\{\sigma|_{X}\mid\sigma\in[\![{\varphi}]\!]\}$ where $\sigma|_{X}$ restricts the domain of $\sigma$ to $X$. For example, restricting $x_{1}\leq x_{2}\wedge x_{2}\leq 100\wedge x_{3}=x_{2}+10$ to $\{x_{1},x_{3}\}$ results in $x_{1}\leq 100\wedge x_{3}\leq 110$. Note that $\varphi^{\prime}$ can be effectively computed using off-the-shelf libraries for manipulating linear constraints [Bagnara et al. (2008)]. We use $\varphi[x_{i}/x_{j}]$ to denote the formula obtained from $\varphi$ by renaming variable $x_{i}$ to $x_{j}$.

An integer transition system ${\cal T}$ (ITS for short) is a control-flow graph where edges are labeled with formulas. Formally, ${\cal T}=\langle{V,N,\mathtt{n_{0}},E}\rangle$ where $V$ is a set of program variables, $N$ is a set of nodes, $\mathtt{n_{0}}\in N$ is the entry node, and $E$ is a set of labeled edges. An edge is of the form ${\mathtt{n_{i}}}\stackrel{{\scriptstyle\varphi}}{{\rightarrow}}{\mathtt{n_{j}}}$ such that $\mathtt{n_{i}},\mathtt{n_{j}}\in N$ and $\varphi$ is formula over variables $V\cup V^{\prime}$ where $V^{\prime}=\{x_{i}^{\prime}\mid x_{i}\in V\}$. We assume that the entry node $\mathtt{n_{0}}$ has no incoming edges. We write $\mathtt{ID}({x_{1},\ldots,x_{n}})$ for $x_{1}=x_{1}^{\prime}\wedge\ldots\wedge x_{n}=x_{n}^{\prime}$, to indicate that variables $x_{1},\ldots,x_{n}$ do not change their values in a given edge.

A program state is a pair $(\mathtt{n_{i}},\sigma)$, where $\mathtt{n_{i}}\in N$ and $\sigma:V\mapsto\mathds{Z}$ is an assignment. There is a transition (i.e. a valid execution step) from $s_{1}=(\mathtt{n_{i}},\sigma)$ to $s_{2}=(\mathtt{n_{j}},\sigma^{\prime})$, denoted as $s_{1}\rightarrow s_{2}$, if there is an edge ${\mathtt{n_{i}}}\stackrel{{\scriptstyle\varphi}}{{\rightarrow}}{\mathtt{n_{j}}}\in E$ such that $\wedge_{x_{i}\in V}(x_{i}=\sigma(x_{i})\wedge x_{i}^{\prime}=\sigma^{\prime}(x_{i}))\models\varphi$. The primed variables $V^{\prime}$ in $\varphi$ refer to the program state following the transition.

A trace is a sequence of states $s_{0}\rightarrow s_{1}\rightarrow\cdots$ such that $s_{i}\rightarrow s_{i+1}$ is a transition. We write $s_{i}\rightarrow^{*}s_{j}$ to indicate that state $s_{j}$ is reachable from state $s_{i}$. An invariant (wrt. an initial state $s_{0}$) for a given node $\mathtt{n_{i}}\in N$ is a formula $\varphi$ over the program variables, and is guaranteed to holds whenever the execution reaches $\mathtt{n_{i}}$, i.e., if $s_{0}\rightarrow^{*}(\mathtt{n_{i}},\sigma)$ then $\sigma\in[\![{\varphi}]\!]$. An ITS is terminating if there are no traces of infinite length starting in $(\mathtt{n_{0}},\sigma)$.

The complexity (also called cost) of an ITS is typically defined in terms of the length of its traces. In order to model cost in a way that is amenable to program transformations, we can add an extra special variable $x_{n+1}$ whose value is [math] in the initial state and which is incremented by $1$ in every transition ($x_{n+1}$ can be modified in other ways to capture different cost models). A function $f:\mathds{Z}^{n}\mapsto\mathds{R}_{+}$ is an upper-bound on the cost of ${\cal T}$ if for any trace $(\mathtt{n_{0}},\sigma)\rightarrow^{*}(\mathtt{n},\sigma^{\prime})$, we have $f(\sigma(x_{1}),\ldots,\sigma(x_{n}))\geq\sigma^{\prime}(x_{n+1})$.

3 Partial Evaluation of Integer Transition Systems

In this section we give a brief description of the partial evaluation technique (for Horn clauses) of \citeNGallagher19, and discuss its use for CFR of ITSs. A constrained Horn clause (CHC) has the form $q_{0}(\bar{x}_{0})\leftarrow\varphi,q_{1}(\bar{x}_{1}),\ldots,q_{k}(\bar{x}_{k})$, where $q_{i}$ are predicate names (all of arity $n$ for simplicity) and $\varphi$ is a constraint. Here we assume that the $\bar{x}_{i}$ are tuples of integer variables, and $\varphi$ is a formula over these variables, where the formula is a conjunction of linear constraints as defined in Sect. 2. We call $q_{0}(\bar{x}_{0})$ the head, and “$\varphi,q_{1}(\bar{x}_{1}),\ldots,q_{k}(\bar{x}_{k})$” the body. We say that the set of CHCs with head predicate $q_{0}$ defines $q_{0}$. A CHC program is a set of CHCs such that one predicate is marked as the entry. The call graph induced by a CHC program is a directed graph whose nodes are the predicate names, and there is an edge from $q_{i}$ to $q_{j}$ if $q_{i}$ is defined by a CHC including $q_{j}$ in its body. We say that $q_{i}$ is a loop head if it has a back edge in the corresponding call-graph wrt. depth-first traversal from the entry predicate.

The technique of \citeNGallagher19 takes as input a CHC program and a constraint on the entry predicate, and returns a partially evaluated CHC program that preserves the computational behavior of the original program with the given entry. In particular, it preserves termination and complexity of the original. It is an online partial evaluation algorithm, meaning that control decisions are made on the fly, and it yields a polyvariant partially evaluated program, meaning that a single predicate $q_{i}$ from the input program can result in several “versions” of $q_{i}$ in the output program.

It is not possible to create versions for all reachable contexts as there may be infinitely many. During partial evaluation, when reaching a call $q(\bar{x})$ with a context $\varphi$ (i.e. constraints on variables $\bar{x}$) the algorithm decides whether to create a version of $q(\bar{x})$ for this context, and replace the corresponding call by one to this version, or to abstract the context.

\citeN

Gallagher19 suggests the use of property-based abstraction in order to guarantee the generation of a finite number of versions. For a predicate $q(\bar{x})$ it assigns beforehand a finite set of properties $\{\varphi_{1},\ldots,\varphi_{k}\}$, where each $\varphi_{i}$ is a formula over $\bar{x}$, and when reaching $q(\bar{x})$ with a context $\varphi$, instead of creating a version for $\varphi$ it creates one for $\alpha(\varphi)=\wedge\{\varphi_{i}\mid\varphi\models\varphi_{i}\}$. This guarantees that there are at most $2^{k}$ versions for $q(\bar{x})$. For example, if predicate $p(x,y,z)$ is assigned properties $x>0$ and $y\geq z$, it would then have up to $4$ versions corresponding to (abstract) contexts $x>0$, $y\geq z$, $x>0\wedge y\geq z$ and $\mathit{true}$. In practice, it is enough to apply property-based abstraction to loop head predicates as they cut all cycles; other predicates can be specialized wrt. to all contexts that are encountered during the evaluation. In addition, partial evaluation might unfold deterministic sequences of calls into a single CHC.

An ITS ${\cal T}$ can be translated into a CHC program $\mathtt{HC}({{\cal T}})$ by translating each edge ${\mathtt{n_{i}}}\stackrel{{\scriptstyle\varphi}}{{\rightarrow}}{\mathtt{n_{j}}}$ into a CHC $q_{\mathtt{n_{i}}}(\bar{x})\leftarrow\varphi,q_{\mathtt{n_{j}}}(\bar{x}^{\prime})$, and marking $q_{\mathtt{n_{0}}}$ as the entry. Note that the control-flow graph of ${\cal T}$ is equivalent to the call-graph of $\mathtt{HC}({{\cal T}})$. Observe that $\mathtt{HC}({{\cal T}})$ is linear, that is, each clause has only one call in the body. Linearity guarantees that the specialized version is also linear, and thus can be converted back into an ITS ${\cal T}_{pe}$ in a similar way. Soundness of partial evaluation guarantees equivalence between the traces of ${\cal T}$ and ${\cal T}_{pe}$, in particular, there is a infinite trace in ${\cal T}$ iff there is one in ${\cal T}_{pe}$. The complexity is preserved as well (when modeled as discussed in Sect. 2).

Example 3.1

We now describe the partial evaluation algorithm for Horn clauses using a worked example, assuming that the clauses are linear, as they are generated from an ITS as just described.

Consider the method phases1 of Fig. 1(a) and its corresponding ITS ${\cal T}$. As discussed in Sect. 1, the execution of this loop has two phases. Our aim is to use partial evaluation to split the loop into two explicit phases (see the corresponding ${\cal T}_{pe}$ of Fig. 1(a)). Translating this ITS into a CHC program results in:

[TABLE]

where $\bar{x}=\langle{x,y,z}\rangle$, $\bar{x}^{\prime}=\langle{x^{\prime},y^{\prime},z^{\prime}}\rangle$, and each $\varphi_{i}$ is as in Fig. 1(a). Note that the only loop head predicate is $q_{\mathtt{n_{1}}}$ ($\mathtt{n_{1}}$ has a back edge when traversing in ${\cal T}$ starting at $\mathtt{n_{0}}$). Let us fix the properties of $q_{\mathtt{n_{1}}}(x,y,z)$ to be $\Psi=\{x>0,y<z,y\geq z\}$, which are the properties of the variables at loop entry that determine which loop path or loop exit is taken.

The partial evaluation algorithm performs a sequence of iterations. The input to each iteration is a set of “versions” of predicates, where each version is a pair $\langle q(\bar{x}),\varphi\rangle$, where $q$ is a program predicate and $\varphi$ is a constraint on its arguments. Each iteration performs an unfolding for each version, followed by a property-based abstraction of the resulting calls using $\Psi$, yielding a new set of versions that is input to the following iteration. The iterations end when no new versions are produced by an unfolding. The unfold operation for a version $\langle q(\bar{x}),\varphi\rangle$ consists of expanding calls in the body of clauses with head $q(\bar{x})$, so long as the call is deterministic and not a loop head, and the constraint $\varphi$ is satisfied.

Let the initial version be $\langle q_{\mathtt{n_{0}}}(x,y,z),\mathit{true}\rangle$. Then the iterations of the algorithm yield the following sequence of new versions.

$\{\langle q_{\mathtt{n_{1}}}(x,y,z),\mathit{true}\rangle\}$. 2. 2.

$\{\langle q_{\mathtt{n_{2}}}(x,y,z),x>0\rangle,\langle q_{\mathtt{n_{3}}}(x,y,z),x\leq 0\rangle\}$. 3. 3.

$\{\langle q_{\mathtt{n_{1}}}(x,y,z),x>0\rangle,\langle q_{\mathtt{n_{1}}}(x,y,z),y\geq z\rangle\}$. 4. 4.

$\{\langle q_{\mathtt{n_{2}}}(x,y,z),x>0\wedge y\geq z\rangle,\langle q_{\mathtt{n_{3}}}(x,y,z),x\leq 0,y\geq z\rangle\}\}$. 5. 5.

$\emptyset$.

We look in detail at iteration 3; the versions $\langle q_{\mathtt{n_{2}}}(x,y,z),\mathit{x>0}\rangle$ and $\langle q_{\mathtt{n_{3}}}(x,y,z),x\leq 0\rangle$ resulting from iteration 2 are unfolded. The latter yields no clauses since there is no clause with head predicate $q_{\mathtt{n_{3}}}$. The version $\langle q_{\mathtt{n_{2}}}(x,y,z),\mathit{x>0}\rangle$ is unfolded giving the clauses

[TABLE]

The constraints on the body calls are then collected. The constraints on $q_{\mathtt{n_{1}}}(x,y^{\prime},z)$, projected onto $\{x,y^{\prime},z\}$, are $x>0$. The constraints on $q_{\mathtt{n_{1}}}(x^{\prime},y,z)$, projected onto $\{x^{\prime},y,z\}$, are $x^{\prime}>-1,y\geq z$. Using property-based abstraction with $\Psi$, the set of properties for $q_{\mathtt{n_{1}}}$, we obtain (after renaming $x^{\prime}$ to $x$)

[TABLE]

Note that the constraint $x>-1\wedge y\geq z$ entails $y\geq z$ but no other member of $\Psi$ and hence the constraint $x>-1$ is abstracted away. This yields the two versions $\langle q_{\mathtt{n_{1}}}(x,y,z),x>0\rangle$ and $\langle q_{\mathtt{n_{1}}}(x,y,z),y\geq z\rangle$ that are shown as the result of iteration 3. Note that without abstraction, an infinite number of iterations could result. In this example, versions $\langle q_{\mathtt{n_{1}}}(x,y,z),x>-1,y\geq z\rangle,\langle q_{\mathtt{n_{1}}}(x,y,z),x>-2,y\geq z\rangle,\ldots$ would be generated.

For each version, a new predicate is generated. We use predicate names that carry information on the different versions: $q_{\mathtt{n_{i}^{j}}}$ is the $j$th version of predicate $q_{\mathtt{n_{i}}}$.The entry predicate $q_{\mathtt{n_{0}}}$ is not renamed. For our example a suitable renaming is as follows.

[TABLE]

The head and body calls of the unfolded clauses for each version are then renamed, yielding the following set of clauses as the result of partial evaluation ($\varphi_{i}$ are as in Fig. 1(a)):

[TABLE]

Translating these CHCs back to an ITS results in ${\cal T}_{pe}$, depicted in Fig. 1(a). $\Box$

Choice of properties.

In the above example, the properties were chosen manually to give the appropriate versions and achieve CFR. While any choice of properties gives a sounds partial evaluation, heuristics are needed to infer appropriate properties automatically. We observe that properties relevant to CFR are closely related to the conditions in the loop head and within the loop body. This leads to the following heuristics that extract properties of $q_{\mathtt{n_{i}}}$ from the constraints of incoming and outgoing edges of node $\mathtt{n_{i}}$:

[TABLE]

$\mathtt{PR_{h}}$ infers properties by extracting conditions from the CHCs defining $q_{\mathtt{n_{i}}}$ (i.e., outgoing edge of $\mathtt{n_{i}}$); this is done by projecting the corresponding constraints on $\bar{x}$. Note that this also captures implicit conditions that do not appear syntactically in $\varphi$. $\mathtt{PR_{hv}}$ infers properties by extracting bounds, for each variable $x_{i}$, from the CHCs defining $q_{\mathtt{n_{i}}}$, inferring the minimal/maximal value for $x_{i}$ is done in practice using linear programming. $\mathtt{PR_{c}}$ and $\mathtt{PR_{cv}}$ are similar but use calls to $q_{\mathtt{n_{i}}}$ (i.e., incoming edge of $\mathtt{n_{i}}$).

Example 3.2

Let us compute properties for $\mathtt{q_{n_{1}}}$. The corresponding node $\mathtt{n_{1}}$ has outgoing edges labeled with $\varphi_{1}$ and $\varphi_{2}$ and incoming edges labeled with $\varphi_{0}$, $\varphi_{3}$ and $\varphi_{4}$. $\mathtt{PR_{h}}(q_{\mathtt{n_{1}}})=\{\mathtt{proj}_{\bar{x}}(\varphi_{1}),\mathtt{proj}_{\bar{x}}(\varphi_{2})\}=\{x\geq 1,x\leq 0\}$, which is also what we get for $\mathtt{PR_{hv}}$ in this case. $\mathtt{PR_{c}}(q_{\mathtt{n_{1}}})=\{\mathtt{proj}_{\bar{x}^{\prime}}(\varphi_{0}),\mathtt{proj}_{\bar{x}^{\prime}}(\varphi_{3}),\mathtt{proj}_{\bar{x}^{\prime}}(\varphi_{4})\}[\bar{x}^{\prime}/\bar{x}]=\{y\leq z,y\geq z\}$ and $\mathtt{PR_{cv}}=\emptyset$. $\Box$

The above heuristics suffice for many cases in practice, but they may be inadequate when conditions in a loop body are not directly implied by the formulas of incoming/outgoing edges of the loop head. E.g., assume method phase1 has an additional statement w=w+1 at the end of the loop body. In this case, the outgoing edges of $\mathtt{n_{2}}$ will not go directly to $\mathtt{n_{1}}$, but to a new node connected to $\mathtt{n_{1}}$ with the formula $w^{\prime}=w+1\wedge\mathtt{ID}({x,y,z})$. Thus, $y<z$ and $z\geq y$ are not implied by the constraints of incoming/outgoing edges of $\mathtt{n_{1}}$.

To overcome this limitation, we developed a new heuristic $\mathtt{PR_{h}^{d}}$ that propagates all constraints in the loop bodies backwards to loop heads as follows: (1) we remove all back-edges (in $\mathtt{HC}({{\cal T}})$), that is, we replace each “$q_{\mathtt{n_{j}}}(\bar{x})\leftarrow\varphi,q_{\mathtt{n_{i}}}(\bar{x}^{\prime})\in\mathtt{HC}({{\cal T}})$” by “$q_{\mathtt{n_{j}}}(\bar{x})\leftarrow\varphi$” if $q_{\mathtt{n_{i}}}$ is a loop head, which results in a recursion-free CHC program; (2) we compute the set of answers (the minimal model) of the resulting CHC program and take them as properties, i.e., if $\varphi_{1},\ldots,\varphi_{l}$ are the answers for $q_{\mathtt{n_{i}}}(\bar{x})$, we define $\mathtt{PR_{h}^{d}}(q_{\mathtt{n_{i}}})=\{\varphi_{1},\ldots,\varphi_{l}\}$. For the modification of the program of Fig. 1(a) just described, we would get $\mathtt{PR_{h}^{d}}=\{y<z,y\geq z,x>0\}$. We could propagate conditions in the loop bodies forwards as well; however, we do not do it since in practice we add invariants to all transitions (which has the effect of propagating conditions forward) before inferring properties.

In the rest of this article, we assume that we have a procedure PE that receives an ITS ${\cal T}$ and applies CFR via partial evaluation as follows:

(1) optionally, it computes invariants for all nodes, and adds them to their outgoing edges, which makes more properties visible in the incoming edges of nodes as discussed above;

(2) generates the CHC program $\mathtt{HC}({{\cal T}})$;

(3) computes properties for each loop head;

(4) applies partial evaluation as described above;

(5) translates the specialized CHCs into a new ITS;

(6) optionally, computes invariants again in order to eliminate unreachable nodes in the new ITS; and

(7) returns the new ITS.

For simplicity, we assume that the choice of properties is provides via global configuration, and not received as a parameter. We might also call PE with a list of nodes $N$ as a second argument to indicate that properties should be assigned to a loop head $q_{\mathtt{n_{i}}}$ only if $\mathtt{n_{i}}\in N$, this is used to apply CFR only to a subset of the ITS. Finally, procedure PE can be applied iteratively on its output, which might achieve further refinements.

4 Application to Termination and Cost Analysis

In this section we discuss how CFR via partial evaluation can improve the precision of termination and cost analysis of ITSs. After a high-level description of a typical termination analyzer (based on iRankFinder [iRank (2019)]), we present an algorithm for termination analysis incorporating the CFR procedure of Sect. 3, and finally discuss some representative examples. At the end of the section we discuss cost analysis.

A termination analyzer receives an input ITS ${\cal T}$, and separately proves termination of each its strongly connected components (SCCs) using a procedure that we call TerminSCC. Proving termination of an SCC $S$ is done by inferring a ranking function $f_{\mathtt{n_{i}}}:\mathds{Z}^{n}\mapsto D$ for each node $\mathtt{n_{i}}$ mapping program states into a set $D$ ordered by a well-founded relation $>$, such that if ${\mathtt{n_{i}}}\stackrel{{\scriptstyle\varphi}}{{\rightarrow}}{\mathtt{n_{j}}}$ is an edge of $S$ then $\varphi\models f_{\mathtt{n_{i}}}(\bar{x})>f_{\mathtt{n_{j}}}(\bar{x}^{\prime})$. Well-foundedness of $>$ guarantees the absence of infinite traces. In practice, we require $f_{\mathtt{n_{i}}}(\bar{x})>f_{\mathtt{n_{j}}}(\bar{x}^{\prime})$ to hold only on a subset of the edges that break all cycles; for other edges it is enough that $f_{\mathtt{n_{i}}}(\bar{x})\geq f_{\mathtt{n_{j}}}(\bar{x}^{\prime})$. Even if TerminSCC fails to prove termination of $S$, it might prove that some of its edges cannot be taken infinitely, and thus that any infinite trace has a suffix that uses only the other edges (which are returned by TerminSCC in such case). TerminSCC makes use of invariants as well, as they can increase its precision. For simplicity we assume that invariants are added to the input ITS and that procedure PE adds such invariants to the refined ITS as well.

The effectiveness of TerminSCC is affected by the kind of ranking functions and invariants used. Probably the best known kinds of ranking function are linear ranking functions (LRFs), which have the form $f(\bar{x})=a_{0}+\sum_{i=1}^{n}a_{i}x_{i}$; there are efficient algorithms for inferring them [Podelski and Rybalchenko (2004), Bagnara et al. (2012)]. However, LRFs do not suffice for all terminating programs; in such cases TerminSCC resorts to combinations of linear functions, e.g. lexicographic ranking functions (LLRFs)  [Alias et al. (2010), Ben-Amram and Genaim (2014)]. Apart from performance, LRFs have the advantage that they induce bounds on the length of traces, and are thus suitable for complexity analysis. For invariants, analyzers often use abstract domains such as convex polyhedra [Cousot and Halbwachs (1978)], which cannot capture more expressive, but expensive disjunctive invariants.

CFR can improve termination analysis by (1) enabling the inference of LRFs where without CFR one would need LLRFs; and (2) enabling automatic termination proof where without CFR it is not possible. We suggest the following schemes for adding CFR to a termination analyzer, trading off ease of implementation with performance and precision.

• •

($\mathtt{CFR_{B}}$): in this scheme CFR is applied directly to the input ITS. This is easy to implement but can perform unnecessary refinements that cause overhead in analysis.

• •

($\mathtt{CFR_{S}}$): in this scheme, when TerminSCC fails to prove termination of a SCC, CFR is applied only to the part of the SCC that it could not prove terminating.

• •

($\mathtt{CFR_{A}}$): this scheme first collects all edges (from all SCCs) on which TerminSCC has failed, and applies CFR to the input ITS taking into account only those edges.

For $\mathtt{CFR_{S}}$ and $\mathtt{CFR_{A}}$ schemes, CFR can be applied iteratively so that refinement is interleaved with termination proofs attempts. In this way, each step might introduce further refinements that could not be done in previous steps. The precision and performance of these schemes are compared experimentally in Sect. 5. Alg. 1 shows the pseudocode of a termination analysis algorithm that uses the above schemes for CFR. It consists of two procedures Termin and TerminITS, and uses TerminSCC as a black box. It also uses some auxiliary procedures that we explain below.

Termin receives an ITS ${\cal T}$, a Boolean $\mathtt{CFR_{B}}$ indicating whether $\mathtt{CFR_{B}}$ should be applied, and integers $\mathtt{CFR_{A}}$ and $\mathtt{CFR_{S}}$ giving the number of times that the respective schemes can be applied. At Line 1 (L1 for short) it calls $\textnormal{{{\sc PE}}}({\cal T})$ if $\mathtt{CFR_{B}}$ is True, and at L1 it calls TerminITS to analyze the SCCs of ${\cal T}$ for the first time. TerminITS returns the set $F$ of edges for which it failed to show termination. If $F=\emptyset$ it halts, otherwise, it enters a loop as long as $\mathtt{CFR_{A}}$ can be applied ($\mathtt{CFR_{A}}>0$) and termination has not been proven ($F\neq\emptyset$). At L1 it returns True if $F=\emptyset$, showing that ${\cal T}$ is terminating, and False otherwise.

In each iteration of the refine/analyze loop (L1-1) it applies CFR only to the parts corresponding to $F$. At L1 it computes the set of nodes $N$ in $F$; at L1 it removes from ${\cal T}$ nodes that do not reach nodes in $N$ (since those parts of ${\cal T}$ have been proven terminating and they do not affect the CFR of any node in $N$); at L1 it applies CFR considering only loop heads in $N$; at L1 it removes from ${\cal T}$ nodes not in $N$ as they have been proven terminating already; at L1 it decreases the $\mathtt{CFR_{A}}$ scheme counter; and finally at L1 it calls TerminITS again to analyze ${\cal T}^{\prime}$. Note that the nodes removed at L1 are not removed before at L1 in order to

(a) guarantee soundness, as CFR must consider all possible ways in which nodes in $N$ are reached;

(b) allow CFR to benefit from context information; and

(c) allow other parts reachable from nodes in $N$ to benefit from refinements.

TerminITS analyzes the SCCs of ${\cal T}$, and applies CFR at the level of SCCs if needed. At L1 it initializes local variables $F$ and $Q$, where $F$ is used to accumulate the edges that it fails to prove terminating (returned at the end at L1), and $Q$ is a queue of pending (sub) ITSs to be analyzed. The elements of $Q$ are pairs $\langle{{\cal T}^{\prime},i}\rangle$, where ${\cal T}^{\prime}$ is an ITS to be analyzed and $i$ is the number of times left to apply CFR to its SCCs. The while loop is executed as long as there are pending ITSs in $Q$: at L1 it takes an ITS ${\cal T}^{\prime}$ from $Q$, and at L1-1 tries to prove termination of its SCCs. This is done by calling TerminSCC on $S$ at L1, and if it fails ($F_{S}\neq\emptyset$) it applies CFR at L1-1 to the problematic part $F_{S}$ if possible ($i>0$), otherwise it adds $F_{S}$ to $F$ at L1. Applying CFR to $F_{S}$ is done as follows: at L1 it builds a new ITS from $F_{S}$, by calling ConITS($F_{S}$), and applies CFR to it. ConITS builds an ITS that consists of the nodes and edges of $F_{S}$, together with a new entry node that has edges to all nodes of $F_{S}$ that are reachable from nodes not in $F_{S}$. This is because CFR must consider all possible ways in which nodes of $F_{S}$ are reached (we assume that ConITS has global access to the original ITS); and at L1 it adds the refined ITS to $Q$ (${\cal T}^{\prime\prime}$ might have several SCCs now).

Next we show some examples of how Alg. 1, can benefit termination analysis, using the different CFR schemes. For all examples we give programs and ITSs, but we omit CHCs as they are similar to ITSs. ITSs are sometimes simplified (e.g. by joining chains of nodes) for presentation; however, they are very similar to what we get in practice – see Sect. 5.

CFR can simplify the termination witness from LLRFs to LRFs, which is useful if the underlying analyzer does not use LLRFs, and can help in making cost analysis feasible as well. For example, consider again method phases1 of Fig. 1(a) and its corresponding ITS ${\cal T}$. It is easy to prove that ${\cal T}$ terminates using the LLRF $\langle{z-y,x}\rangle$ for nodes $\mathtt{n_{1}}$ and $\mathtt{n_{2}}$, but it is not possible if we restrict ourselves to the use of LRFs. Calling $\textnormal{{{\sc Termin}}}({\cal T},\mathit{true},0,0)$ applies CFR at L1 before trying to prove termination, yielding the ITS ${\cal T}_{pe}$ of Fig. 1(a). The two loop phases are now explicit: nodes $\mathtt{n_{1}^{2}}$ and $\mathtt{n_{2}^{2}}$ correspond to the first phase, and nodes $\mathtt{n_{1}^{1}}$ and $\mathtt{n_{2}^{1}}$ to the second phase. Using this refined ITS, TerminITS finds LRFs $z-y$ and $x$ for the corresponding SCCs. The next example discusses cases for which CFR is essential for proving termination, not only for simplifying the form of the witness.

Example 4.1

Consider method search of Fig. 1(b). It receives an array $q$ representing a circular queue, the size of the array $n$, the indexes $h$ and $t$ of the head and tail, and a value $v$ to search for. The loop first (if $h>t$) searches for $v$ in the interval $[h..n-1]$ and then in $[0..t]$. This defines two phases where moving from the first to the second is done by setting $h$ to [math]. It is easy to see that (a) in the first phase, $n-h$ is non-negative and decreasing in all iterations except the last, i.e., when setting $h$ to [math] and (b) in the second phase, $n-h$ is decreasing and non-negative. The last iteration of the first phase makes automatic proofs subtle, because it breaks the conditions that a LRF or a LLRF has to satisfy as function $n-h$ increases when setting $h$ to [math]. If we succeed in splitting these phases into separate loops, such that the last iteration of the first phase is a transition that connects them, then proving termination should be possible with LRFs only. Unlike method phases1 of Fig. 1(a), in this one the two phases execute the same code, i.e., the then branch at PP4 (short for program point 4).

The ITS ${\cal T}$ of this program is shown in Fig. 1(b). Node $\mathtt{n_{1}}$ corresponds to the loop head, and $\mathtt{n_{2}}$ to the if statement. Assume that this loop is the only loop in a larger program that we cannot prove terminating, so as to take advantage of applying CFR at the level of SCCs. Calling $\textnormal{{{\sc Termin}}}({\cal T},\textit{false},0,1)$ we eventually reach L1 with SCC $S$ containing nodes $\mathtt{n_{1}}$ and $\mathtt{n_{2}}$. $\textnormal{{{\sc TerminSCC}}}(S)$ fails to prove termination of any edge of $S$ and returns the set of edges of $S$. The new ITS ${\cal T}^{\prime\prime}$ at L1 is like the ITS ${\cal T}$ of Fig. 1(b), but without the exit node $\mathtt{n_{3}}$. Applying CFR at L1 using properties $\{h=0,h\leq t\}$ (or $\mathtt{PR_{cv}}$ and $\mathtt{PR_{c}}$) we obtain ${\cal T}_{pe}$ shown in Fig. 1(b), which is added at L1 to $Q$ in order to analyze it again. Node $\mathtt{n_{1}}$ of ${\cal T}$ now has $2$ versions in ${\cal T}_{pe}$: $\mathtt{n_{1}^{2}}$ is for the first phase which excludes the last step that sets $h$ to [math], which is now handled by the edge ${\mathtt{n_{2}^{2}}}\stackrel{{\scriptstyle\varphi_{7}}}{{\rightarrow}}{\mathtt{n_{1}^{1}}}$; and node $\mathtt{n_{1}^{1}}$ is for the second phase. When ${\cal T}_{pe}$ is analyzed, TerminSCC finds LRFs for both SCCs of ${\cal T}_{pe}$. $\Box$

The next example shows (1) how CFR is useful for inferring precise invariants, without using disjunctive abstract domains; and (2) the importance of the scheme $\mathtt{CFR_{A}}$.

Example 4.2

Let us modify method search (and its ITS ${\cal T}$) to include another variable $w$, that is initialized to $t-h+1$ before the loop and is set to $1$ in the else branch at PP4. The initial value of $w$ is at least $1$ if $h\leq t$, and it is at most [math] if $h>t$. However, in the later case the execution eventually passes through the else branch and sets $w$ to $1$. This means that $w\geq 1$ holds after the loop. Using the ITS ${\cal T}$ of this program, invariant generators would fail to infer this information without relying on disjunctive invariants, e.g. $(h\leq t\wedge w\geq 1)\vee(h>t\wedge w\leq 0)$ for node $\mathtt{n_{1}}$. However, when using ${\cal T}_{pe}$ they succeed because in ${\cal T}_{pe}$ it is explicit that the second phase is reached, in either way, with $w\geq 1$.

Precise invariants are essential for the precision of termination analysis. Assume that the loop of method search is followed by a second loop “while (x>=1) x=x-w;”, then termination analysis of this loop would fail without the invariant $w\geq 1$ since the loop is non-terminating for $w\leq 0$. Note that in order to propagate $w\geq 1$ from the first loop to the second, we cannot use the scheme $\mathtt{CFR_{S}}$ since it analyzes the SCCs independently, and thus after applying CFR to the SCC of the first loop the new invariants are not propagated to the SCC of the second loop. Instead, we can use $\mathtt{CFR_{A}}$ by calling $\textnormal{{{\sc Termin}}}({\cal T},\textit{false},1,0)$. In this case, the first call to TerminITS at L1 fails to prove any of the two loops terminating, and then CFR at L1 is applied on both loops together and now the constraint $w\geq 1$ is propagated to the second loop. One could also use $\mathtt{CFR_{B}}$, but it might be less efficient if the program is part of a larger one that does not need CFR to handle other SCCs. $\Box$

Next we discuss one of the examples that no tool could handle in the last termination competition [TERMCOMP (2019)], except iRankFinder when using CFR.

Example 4.3

Consider method randomwalk of Fig. 1(c). It simulates a random walk where $w$ is repeatedly increased or decreased at PP9 depending on the random choice for $c$ at PP4. The code at PP5-8 ensures termination. Assuming that $n\geq 1$, the loop passes through the following phases: (a) $z\geq 1$, so $z$ is decremented at PP5 until it reaches [math]; (b) since $z=0$ and $i=1$ now, it either executes PP8 and exits the loop, or executes PP7 which decrements $i$ to [math] and in the next iteration executes PP5 and sets $i$ to $2$ and $z$ back to $n$; (c) since $z\geq 1$ now, it is decremented at PP5 until it reaches [math]; (d) since $z=0$ and $i=2$ now, it either executes PP7 twice, which means that $c=0$ and thus at PP9 $w$ is decremented twice to [math] and exits the loop, or it executes PP8 at least once and exits the loop. The case of $n\leq 0$ passes in steps (b) and (d) only. Applying CFR to ${\cal T}$ of Fig. 1(c), e.g. using properties $\mathtt{PR_{cv}}$ and $\mathtt{PR_{h}^{d}}$, we obtain the ITS ${\cal T}_{pe}$ sketched in Fig. 1(c) (each box is an SCC with several nodes and a single cycle that decrements $z$). Calling Termin on ${\cal T}$ with any of the schemes refines the graph to something like ${\cal T}_{pe}$, and then proves termination with LRF $z$ for both SCCs. $\Box$

Cost analysis.

In the rest of this section we discuss the use of CFR for cost analysis, namely the inference of upper-bound functions on the length of traces (see Sect. 2). There are several cost analysis tools for (variants of) ITSs, and they are based on similar techniques to those used in termination analysis. In particular, they use ranking functions to infer visit-bounds, which are upper-bounds on the number of visits to edges in the ITS.

KoAT [Brockschmidt et al. (2016)] is a tool that works directly on ITSs as defined in Sect. 2 and uses quasi-LRFs [Alias et al. (2010)] to infer visit-bounds. CoFloCo [Flores-Montoya (2017)] is a tool that works on a form of ITSs that is called cost relations (CRSs), which are similar to recurrence relations. It mainly uses LRFs to infer visit-bounds, and it applies CFR (directly to CRSs) to increase precision. The CFR techniques of CoFloCo are very similar to those of \citeNGulwaniJK09. PUBs [Albert et al. (2011)] is the first tool to infer upper-bounds for CRSs. It uses LRFs to infer visit-bounds and it does not apply any kind of CFR. In terms of precision, CoFloCo can handle anything that PUBs can, and it is not directly comparable to KoAT as there are cases where one succeed and the other fail to infer upper-bounds.

In the context of cost analysis, CFR can improve the precision of inferring visit-bounds in a way that is similar to simplifying the witness of a termination proof. The next example shows this for all examples that we have discusses so far. For CFR in this context we simply apply procedure PE of Sect. 3 to the input ITS.

Example 4.4

For Fig 1(a), KoAT infers a linear upper-bound without CFR thanks to the use of quasi-LRFs, which allow the inference of $x$ and $z-y$ as visit-bounds for ${\mathtt{n_{2}}}\stackrel{{\scriptstyle\varphi_{4}}}{{\rightarrow}}{\mathtt{n_{1}}}$ and ${\mathtt{n_{2}}}\stackrel{{\scriptstyle\varphi_{3}}}{{\rightarrow}}{\mathtt{n_{1}}}$, respectively; CoFloCo infers a linear upper-bound since it applies CFR that splits the loop into phases; PUBs fails to infer any upper-bound, however, it infers a linear upper-bound when applied to the ITS after CFR. For Ex. 4.1, KoAT and PUBs fail to infer any upper-bound, but they infer a linear upper-bound after applying CFR; CoFloCo infers a linear upper-bound since it applies its own CFR that splits the loop into two phases. For Ex. 4.2, all tools fail to infer an upper-bound, and all infer a linear upper-bound after applying CFR (note that CoFloCo’s own CFR is insufficient here). For Ex. 4.3, all tools fail to infer any upper-bound, and they infer a linear upper-bound for the refined ITS. $\Box$

Next we discuss another direction where ranking functions are used as properties for CFR. Sometimes we can prove termination of an ITS but cannot infer an upper-bound on its cost. One reason is that in termination analysis we can use ranking functions that do not necessarily imply an upper-bound on the length of traces, e.g. LLRFs. However, for some kind of LLRFs, even if they do not imply an upper-bound, they provide useful information about loop control flow. Our goal is to use these ranking functions to help CFR to make this control flow explicit, which helps cost analysis to infer upper-bounds.

Example 4.5

Consider method phases2 of Fig 1(d) and its ITS ${\cal T}$. Termination analysis succeeds in proving termination, assigning node $\mathtt{n_{1}}$ the LLRF $\langle{z,y,x}\rangle$. This LLRF is in a sub-class called multi-phase linear ranking functions (M$\Phi$RFs) [Ben-Amram and Genaim (2017)]; it has the following properties (considering consecutive visits to $\mathtt{n_{1}}$): $z$ decreases, and when it becomes negative $y$ starts to decrease, and when $y$ becomes negative $x$ starts to decrease. This means that on reaching $\mathtt{n_{1}}$ one of the following must hold: $z\geq 0$, $z<0\wedge y\geq 0$, $z<0\wedge y<0\wedge x\geq 0$ or $z<0\wedge y<0\wedge x<0$. The ITS ${\cal T}^{\prime}$ of Fig 1(d) is a modification of ${\cal T}$ making this information explicit: we added a new node $\mathtt{n_{1a}}$, changed all incoming edges of $\mathtt{n_{1}}$ to go to $\mathtt{n_{1a}}$, and added $4$ edges from $\mathtt{n_{1a}}$ to $\mathtt{n_{1}}$, each annotated with one of the above constraints. Applying CFR to ${\cal T}^{\prime}$ results in the ITS ${\cal T}^{\prime}_{pe}$ in which the phases are explicit (nodes $\mathtt{n_{1a}^{1}}$, $\mathtt{n_{1a}^{2}}$, and $\mathtt{n_{1a}^{3}}$). Cost analysis tools can infer a linear upper-bound for ${\cal T}^{\prime}_{pe}$. Note that the addition of node $\mathtt{n_{1a}}$ is essential, applying CFR directly to ${\cal T}$ would not do any refinement.

The above example can be generalized as follows. If a loop-head node $\mathtt{n_{i}}$ is assigned a M$\Phi$RF $\langle{f_{1},\ldots,f_{k}}\rangle$ during termination analysis: we add a new node $\mathtt{n_{ia}}$ and change all incoming edges of $\mathtt{n_{i}}$ to $\mathtt{n_{ia}}$; and add $k+1$ edges from $\mathtt{n_{ia}}$ to $\mathtt{n_{i}}$ where the $i$th edge has the constraints $f_{1}(\bar{x})<0\wedge\cdots\wedge f_{i-1}(\bar{x})<0\wedge f_{i}(\bar{x})\geq 0\wedge\mathtt{ID}({\bar{x}})$. Applying CFR to the new ITS takes advantage of the new edges, and splits the loop into corresponding phases.

5 Implementation and Experimental Evaluation

In this section we discuss implementation and experimental evaluation of the ideas discussed in this article. More details are available in A and at the companion website http://irankfinder.loopkiller.com/papers/extra/iclp19.

We provide a standalone tool that receives an ITS (in several formats) and generates an ITS after applying CFR using partial evaluation [Gallagher (2019)]. It accepts any of the properties discussed in Sect. 3 (the user selects the heuristics, and then they are inferred automatically), as well as user-supplied properties and can be applied to a subset of the ITS. In addition, it includes an invariants generator that can be optionally used. Apart from the standalone tool, we modified iRankFinder to incorporate Alg. 1.

We have evaluated the effect of Alg. 1 on iRankFinder using standard sets of benchmarks [TPDB (2019), Flores-Montoya (2017)]. We analyzed all benchmarks (except those known to be nonterminating) in two settings, using LRFs and LLRFs, and using different schemes and properties. Out of $556$ (resp. $143$) ITSs that it cannot handle using LRFs (resp. LLRFs) without CFR, it can handle $251$ (resp. $48$) with CFR. As expected, CFR has performance overhead that depends on the scheme and the kind of properties used. Experiments show that properties $\mathtt{PR_{h}^{d}}$ and $\mathtt{PR_{c}}$ are important for precision, and that using them with $\mathtt{CFR_{S}}$ provides the best performance/precision trade-off. The time spent on CFR can be up to $42\%$ of the total time, depending on the scheme and properties used (as expected, $\mathtt{CFR_{B}}$ takes more time than $\mathtt{CFR_{A}}$ and $\mathtt{CFR_{S}}$).

We have also analyzed this set of benchmarks using other termination analyzers of ITSs: VeryMax [Borralleras et al. (2017)] and T2 [Brockschmidt et al. (2016)]. There are 8 (resp. 14) examples that we can handle due to the use of CFR and VeryMax (resp. T2) cannot handle without CFR. For benchmarks where VeryMax (resp. T2) failed, we have applied them again on the ITSs after CFR (using scheme $\mathtt{CFR_{B}}$) and it could prove termination of $6$ (resp. $39$) more benchmarks and nontermination of $80$ (resp. $40$) benchmarks.

For cost analysis, we applied KoAT on a set of $200$ benchmarks. With CFR we got tighter upper-bounds for $15$ benchmarks. Using $\mathtt{PR_{h}^{d}}$ and $\mathtt{PR_{c}}$ gave the best precision. We did not run PUBs on this set since it is not directly designed for ITSs, and more work is required to transform ITSs to CRSs without losing precision (i.e., inferring loop summaries which is usually done by the frontend that uses PUBs). We did not run CoFloCo on this set since it includes a CFR component for CRSs. However, as we have seen in the examples of Sect. 4, our CFR procedure can improve the precision of both PUBs and CoFloCo.

We used the invariant generator of iRankFinder to prove the assertions in $13$ programs from \citeNSharmaDDA11. Without CFR, it proved the assertions for $5$ of them, and with CFR it did so for all benchmarks. Also here, $\mathtt{PR_{h}^{d}}$ and $\mathtt{PR_{c}}$ provided the most precise results. We have also evaluated our CFR procedure on all examples of Fig. 1 and Fig. 2 of \citeNGulwaniJK09, and got similar refinements. The tools of \citeNSharmaDDA11 and \citeNGulwaniJK09 are not available so we cannot experimentally compare to them.

6 Conclusions, Related and Future Work

In this work we proposed the use of partial evaluation as a general purpose technique to achieve CFR. Our CFR procedure is developed for ITSs, and used a partial evaluation technique for Horn clause programs based on specializing programs wrt. a set of supplied properties. The right choice of properties is a key factor for achieving the desired CFR, and we suggested several heuristics for inferring properties automatically. We provide an implementation that can be used as a preprocessing step for any static analysis tool that uses ITSs, and integrated it in iRankFinder in a way that allows application of CFR only if needed. Experimental evaluation demonstrated that our CFR procedure enables termination proofs and cost inference of many ITSs that we could not handle before.

Closely related work has been discussed in Sect. 1. The use of partial evaluation for CFR is not directly comparable to these works; however, experiments show that we achieve similar results. In particular in the examples of Sect. 4 we discussed some cases that \citeNFlores-MontoyaH14 cannot handle, and in Sect. 5 we have seen that we achieve similar refinements for the examples of \citeNGulwaniJK09. In addition, we could handle all examples of \citeNSharmaDDA11. We conjecture that the partial evaluation algorithm achieves the same refinement as the technique of \citeNSharmaDDA11, provided that the splitter predicates (or their negations) are among the properties provided to the algorithm. Sharma et al. generate candidate splitter predicates from the conditions occurring in loops, using the weakest precondition operator to project them onto the loop head, which corresponds closely to our property generation $\mathtt{PR_{h}^{d}}$.

There is a close relationship between partial evaluation of logic programs (sometimes called partial deduction) and abstract interpretation of logic program with respect to a goal (top-down abstract interpretation); both can be expressed in a single generic framework parameterised by an abstract domain and an unfolding strategy [Puebla et al. (1999), Leuschel (2004), Puebla et al. (2006)]. The combination of the two techniques can be mutually beneficial, as shown in [Puebla et al. (2006)]. In top-down abstract interpretation, the aim is to derive call- and answer-patterns, which are described by abstract substitutions over program variables, whereas in partial evaluation, the aim is to unfold parts of the computation and derive a program specialised for the given goal. The versions in a polyvariant partial evaluation correspond to multiple call-patterns in top-down abstract interpretation. Viewing CFR as an instance of a generic framework, the choice of abstract domain and unfolding strategy are crucial, and therefore this paper focusses on those aspects. There are many ways to achieve polyvariance in partial evaluation, and obtaining a good set of versions leading to useful refinements requires careful choice of the abstract domain, which in our case is the power set of the given set of properties. The control of unfolding is also critical, as unfolding choice predicates leads to a trade-off between specialisation and blow-up in the size of the specialised program.

Logic program specialisation has been previously applied as a component in program verification tools, with a goal similar to the one in this paper. Namely, the specialisation of a program with respect to a goal (corresponding to a property to be proved) can enable the derivation of more precise invariants, contributing to a proof of the property [Leuschel and Massart (2000), De Angelis et al. (2012), Fioravanti et al. (2012), Kafle et al. (2018)]. Polyvariant specialisation is often crucial, allowing (in effect) the inference of disjunctive invariants. Again, for CFR the choices for abstraction and unfolding strategy are important, to achieve the right balance between precision and the size of the specialised programs. In [De Angelis et al. (2012)], an operation called constrained generalisation is used; this identifies constraints on a predicate that determine control flow. A generalisation operator on constraints is designed to preserve the control flow. This has a relation to property-based abstraction but we find it more natural and controllable to let the properties determine the control flow rather than the other way round. However, further evaluation of different abstractions is needed. We performed some experiments on examples from this paper using a general-purpose logic program specialiser (ECCE [Leuschel et al. (2006)]) but the abstraction used in that tool did not result in any useful CFR.

For future work, we plan to explore further the automatic inference of properties, in particular the use of ranking functions as discussed in Sect. 4. Moreover, we want to explore the use of CFR for other static analysis tools, where the data is not numerical. It is also worth investigating whether the insights from CFR could be used to improve general-purpose specialisation tools.

Appendix A More details on experiments

The purpose of this appendix is to provide the reader with extra information on the experimental evaluation – all is available at http://irankfinder.loopkiller.com/papers/extra/iclp19 as well.

For termination analysis, we have experimentally evaluated the effect of Alg. 1 on iRankFinder using $3$ sets of standard benchmarks:

• •

(SET-1) is a set of $416$ ITSs coming from Java programs (directory From_Aprove_2014 of \citeNtpdb);

• •

(SET-2) is a set of $806$ ITSs coming not necessarily from structured programs (directory From_T2 off \citeNtpdb); and

• •

(SET-3) is a set of $200$ ITSs coming mainly from Java and C programs used by \citeNMontoya17 for experimental evaluation of cost analysis.

Set SET-1 (resp. SET-2) includes $159$ (resp. $348$) ITS known to be non-terminating, and thus we exclude them from the experiments. We first analyzed all benchmarks for termination without CFR in two settings, using LRFs and using LLRFs, and for those on which iRankFinder failed, we analyzed them again with CFR using different schemes and properties.

The results are summarized at Table. 1. There are $3$ (horizontal) blocks, each corresponding to a set of benchmarks. On the side of each block, we indicate the total number of benchmarks on which iRankFinder failed without CFR (excluding non-terminating ones) and the total time (in minutes) it took to analyze them, for both LRFs and LLRFs. For each set, there are two (vertical) blocks corresponding to the two settings, using LRFs and using LLRFs. Columns correspond to different CFR schemes, and rows to properties used for CFR (subsets of those defined in Sect. 3). Each entry in the table includes the number of benchmarks that iRankFinder can now prove terminating and the total time it took to analyze all benchmarks, using the scheme and properties as indicated in the corresponding row and column, and the percentage of the total time spend on CFR. Each benchmark was given a $5$min time limit.

In terms of precision:

• •

For SET-1: without using CFR we prove termination of $159$ (resp. $229$) ITSs when using LRFs (resp. LLRFs), and with CFR we can handle $40$ (resp. $9$) more ITSs.

• •

For SET-2: without using CFR we prove termination of $120$ (resp. $376$) ITSs when using LRFs (resp. LLRFs), and with CFR we can handle $178$ (resp. $26$) more ITSs.

• •

For SET-3: without using CFR we prove termination of $88$ (resp. $175$) ITSs when using LRFs (resp. LLRFs), and with CFR we can handle $33$ (resp. $13$) more ITSs.

In total, we improve for $251$ bechmarks when using LRFs only, and $48$ when using LLRFs. Times in the table should be interpreted carefully, since when analyzing without CFR and when using $\mathtt{CFR_{B}}$ the analysis stops as soon as it fails to prove termination of a SCC, while when using $\mathtt{CFR_{S}}$ and $\mathtt{CFR_{A}}$ it keeps trying to prove termination of all SCCs.

For cost analysis, we have applied the tool KoAT to estimate the effect of CFR on precision. We have analyzed set SET-3 without and with CFR with different properties. CFR improved (by inferring a tighter upper-bound) the precision for $15$ benchmarks.