Abstract
The top-down solver TD is a generic fixpoint algorithm that can be used to compute partial post-solutions of equation systems for abstract interpretation. We consider two extensions of the TD to deal with infinite strictly ascending chains. For the TD extended with warrowing, we formally prove that it always returns partial post-solutions, while for the TD extended with widening and narrowing in phases, we prove termination provided that the set of unknowns is finite. By proving the equivalence of the two extensions, we deduce the total correctness of both solvers. For the equivalence to hold, we in particular assume the equation system to have right-hand sides that are both monotonic and have monotonic dependencies. We demonstrate with counterexamples that the violation of any of the assumptions may compromise the equivalence. All proofs have been formalized using the interactive theorem prover Isabelle.
1 Introduction
Fixpoint engines are the algorithmic core of static program analyzers [1,2,3,4]. Such analyzers may, e.g., certify the absence of runtime errors such as integer overflows or null pointer dereferences. The computed results can, however, only be relied upon if the implementation of the analyzer is correct. Abstract interpretation provides a theory for reasoning about the correctness of analysis specifications [5]. In a nutshell, the analysis problem for a program is translated to computing a (post-)solution for an equation system that captures the relationships between program invariants at different program points. Program invariants are compiled into values of a partial order, and unknowns are introduced for points of interest in the program where invariants are sought.
A variety of fixpoint engines, i.e., solvers for such equation systems have been introduced [6,7,8,9,10,11]. Of these, the top-down solver TD is particularly interesting because it can handle both infinite and non-monotonic equation systems. As it dynamically detects dependencies between unknowns [10,11,12], no preprocessing of the equation system is required. While simple solvers such as round-robin iteration are easy to verify, the formal verification of TD poses a significant challenge. So far, a proof formalized in Isabelle/HOL only established the partial correctness of the vanilla version [13, 14]. When the analysis relies on partial orders with very long, if not infinite, strictly ascending chains, the vanilla TD may take very long or not even terminate. One idea is to speed up fixpoint iteration with widening [5, 15, 16]. The price to be paid is possibly unnecessarily imprecise invariants that are insufficient to prove the program property in question. Consecutive narrowing iterations may recover some lost precision [5, 15]. To further increase precision, widening and narrowing iterations may be restricted to a (sufficiently large) subset of unknowns, and also intertwined. Intertwining the widening and narrowing phases avoids the unnecessary spread of overly imprecise values of unknowns to other unknowns [17].
Two extensions of TD with widening and narrowing have been proposed. Apinis et al. [18] introduce a warrowing operator which combines widening and narrowing. This solver is claimed to always return partial post-solutions—provided that it terminates. Alternatively, TD can be equipped with one widening and narrowing phase per iteration for an unknown [11]. This solver has been claimed to terminate as long as only finitely many unknowns are encountered—but may not necessarily return partial post-solutions. Therefore, its results must be proven correct w.r.t. the corresponding concrete program semantics and the properties of the abstract interpretation. Both extensions intertwine widening and narrowing iterations [17] and maintain a set of dedicated unknowns where widening/narrowing is applied.
In this paper, we formalize both extensions of TD with the interactive theorem prover Isabelle—TD equipped with warrowing (\(\hbox {TD}_{\boxslash }\)) and an optimized version of TD with widening/narrowing phases per unknown (\(\hbox {TD}_{\text {w/n}}\)) [19]. After introducing basic notions in Sect. 2, we provide overviews of our formalized proofs for the partial correctness of \(\hbox {TD}_{\boxslash }\) (Sect. 3) and the termination of \(\hbox {TD}_{\text {w/n}}\) for finitely many unknowns (Sect. 4). As our key contribution, we formally prove that both solvers are equivalent, i. e., perform the same computations and return the same result (Sect. 6). For that equivalence to hold, we identify three assumptions, namely, that the widening operator is precise, and that all right-hand sides of the equation system are not only monotonic, but also have monotonic dependencies (for definitions see Sect. 5). While the assumption of monotonicity of right-hand sides has already been considered before, the assumption on monotonic dependencies is novel. We show by counterexamples that when any of the three assumptions are violated, \(\hbox {TD}_{\text {w/n}}\) not necessarily returns a partial post-solution (Sect. 5). For the assumption on the widening operator \(\nabla \), we provide a construction to turn any, possibly imprecise widening operator, into a precise widening operator. The equivalence of the two solvers implies total correctness of both, i. e., both terminate for finite sets of unknowns, and return partial post-solutions for the equation system in case the given assumptions hold.
2 Preliminaries
The following notations are used throughout the paper. The powerset of a set \(\mathcal {U}\) is denoted by \(\mathcal {P\left( \mathcal {U}\right) } \). The function notation \(\lambda \_.\,v\) describes a default mapping that maps every key to v. The update of mapping M for argument k with value v is denoted by \(M\oplus \{k\mapsto v\}\), and we write \(M^+\) for the transitive closure of a mapping M of type \(\mathcal {U}\rightarrow \mathcal {U}\ \texttt{list} \). A record value \(\llparenthesis {k_1 = v_1,...,k_n = v_n}\rrparenthesis \) is a named tuple where the fields \(k_i\) have value \(v_i\). The field names serve as access indices, i. e., \(r\!.k_i = v_i\) for a record r where field \(k_i\) has value \(v_i\). A record r where some field k is updated to hold value v is denoted as \(\llparenthesis {r\ \texttt{with}\ k:= v}\rrparenthesis \), multiple updates may be abbreviated by writing \(\llparenthesis {r\ \texttt{with}\ k_{i_1}:= v_{i_1},..., k_{i_n}:= v_{i_n}}\rrparenthesis \). We write \([\,]\) for the empty list, and \(x\#xs\) for the construction of a list from a head x and a tail xs. The function set returns the set of elements in a list.
The domain \(\mathbb D \) describes the set of possible values for unknowns. In static analysis, \(\mathbb D \) is often considered to be a complete lattice. Here, we just assume \(\mathbb D \) to be partially ordered by some relation \(\le \) with a least element \(\bot \). An equation system \({\mathcal {T}} \,\) is a mapping from the set \(\,\mathcal {U} \) of unknowns to their respective right-hand sides. For the solver TD, right-hand sides of equation systems are considered as black-box functions which are ignorant of the solver’s state. This is the case if the right-hand side \(f_u\) for an unknown u is of type \((\mathcal {U} \rightarrow \, \mathcal {M}_{S}(\mathbb D)) \rightarrow \, \mathcal {M}_{S}(\mathbb D)\) which is parametric in the state monad \(\mathcal {M}_S\) (using states from some set S). Such functions have been called pure [20]. A pure function can be represented as a strategy tree:
A strategy tree may either be an \(\texttt{Answer}\) containing a constant value from the domain, or a \(\texttt{Query}\) of an unknown y together with a continuation that provides a strategy tree for every possible value of y. Strategy trees thus make the order in which unknowns are accessed explicit. Since our proof arguments take the operational behavior during the evaluation of right-hand side functions into account, we assume w.l.o.g., that the equation system \({\mathcal {T}} \,:\mathcal {U} \rightarrow (\mathcal {U},\mathbb D)\ \mathtt {strategy\_tree} \) maps each unknown to a strategy tree. Generally, we assume strategy trees to be well-founded. This is ensured by defining strategy trees as an inductive type in Isabelle.
Example 1
(An Equation System for an Integer Upper Bound Analysis) Consider the following program on the left and its control-flow graph on the right. We construct an equation system for an upper bound analysis for program variable \(\texttt{i}\) to establish that \(\texttt{i} \le \texttt{100} \) holds after the loop.
The domain is the complete lattice \(\mathbb {Z_{-\infty }^{+\infty }}\). The ordering of integers and arithmetic operations are naturally extended to the least element \(-\infty \) and the greatest element \(+\infty \). The following (informal) equation system describes how the abstract value, i. e., an upper bound for variable \(\texttt{i}\), at some program point u can be computed from the abstract value at u’s immediate predecessors. A strategy tree for the right-hand side of y is shown on the right. The edges are labeled with conditions on the value returned for the queried unknown that determine the subtrees to continue evaluation with. If the value of a queried unknown is used subsequently in some answer node, we provide a name for it (always d in the examples), but leave it implicit otherwise.
Given some value mapping \({\sigma } :\mathcal {U} \rightarrow \mathbb D \), a strategy tree t can be evaluated with the function \(\texttt{eq}\), while the function \({\texttt{dep}}\) collects the dependencies, i. e., the set of unknowns queried when evaluating t:
A solution of the equation system \({\mathcal {T}} \,\) is a mapping \({\sigma } :\mathcal {U} \rightarrow \mathbb D \) that maps every unknown u to the result of the evaluation of u’s right-hand side with \({\sigma }\), i. e., \(\texttt{eq} \,({\mathcal {T}} \,u)\,{{\sigma }} = {\sigma } u\). Assuming that larger values are less precise but still sound, a static analyzer may be content to return post-solutions. A value mapping \({\sigma }\) is called post-solution for an equation system \({\mathcal {T}} \), if for every unknown u, the value \({\sigma } u\) subsumes the value of its right-hand side for \({\sigma }\), i. e., \({\texttt{eq} \,({\mathcal {T}} \,u)\,{{\sigma }}} \le {\sigma } u\). To deal with equation systems with a possibly infinite number of unknowns, local solvers only consider unknowns relevant for computing the value for some initially queried unknown. Thus, local solvers may compute partial post-solutions:
Definition 1
(Partial Post-Solution) A value mapping \({\sigma }\) is called partial post-solution for the equation system \({\mathcal {T}} \,\) and a set of unknowns \(s \subseteq \mathcal {U} \), if
-
1.
right-hand sides are subsumed: \(\forall u \in s.\ {\texttt{eq} \,({\mathcal {T}} \, u)\,{{\sigma }}} \le {\sigma } u\), and
-
2.
s is closed: \(\forall u \in s.\ {\texttt{dep}} \,({\mathcal {T}} \,u)\,{{\sigma }} \subseteq s\).
We call a solver partially correct if it returns a partial post-solution whenever it terminates, and totally correct if it is guaranteed to terminate and returns a partial post-solution.
If the domain \(\mathbb D \) has long or even infinite ascending chains, fixpoint iteration may be expensive or fail to terminate. Consider, e. g., a fixpoint iteration for unknown y in Example 1 when starting with the initial value \(\bot \). In the first iteration, y evaluates to 10. With every following iteration, its value is incremented by one until 100 is reached. To speed up iteration, a widening operator can be applied to extrapolate encountered values. The definition of a widening operator we use here is a weakened version of the definition in [5].
Definition 2
(Widening Operator) A binary operator \(\nabla :\mathbb D \rightarrow \mathbb D \rightarrow \mathbb D \) is called widening operator if
-
(i)
for all \(a,b \in \mathbb D \) it holds that \(b \le a\ \nabla \ b\) (i. e., in particular we do not require \(a \le a\ \nabla \ b\)), and
-
(ii)
for every sequence \((b_i)_{i \in \mathbb {N}}\), the sequence \((a_i)_{i \in \mathbb {N}}\) defined by \(a_1 = b_1\) and \(a_i = a_{i-1}\ \nabla \ b_i\) for \(i > 1\), is ultimately stable, i. e., there exists an n such that \(a_m = a_n\) for all \(m > n\).
As observed in [5], widening iterations may result in imprecise values for unknowns. Therefore, a subsequent iteration is proposed where a narrowing operator may regain precision from post-solutions while enforcing termination.
Definition 3
(Narrowing Operator) A binary operator \(\mathrm \Delta :\mathbb D \rightarrow \mathbb D \rightarrow \mathbb D \) is a narrowing operator [5] if
-
1.
for all \(a,b \in \mathbb D \) it holds that \(b \le a \implies b \le a\ \mathrm \Delta \ b \le a\), and
-
2.
for every sequence \((b_i)_{i \in \mathbb {N}}\), the sequence \((a_i)_{i \in \mathbb {N}}\) defined by \(a_1 = b_1\) and \(a_i = a_{i-1}\ \mathrm \Delta \ b_i\) for \(i > 1\), is ultimately stable, i. e., there exists an n such that \(a_m = a_n\) for all \(m > n\).
Example 2
(Widening and Narrowing Operator for the Integer Chain Lattice) A widening and a narrowing operator for the domain from Example 1 may be
Separating widening and narrowing into consecutive global phases may cause imprecision of one unknown to spread and irreversibly compromise the precision of other unknowns. Therefore, Amato et al. [17] suggest intertwining the two phases. In fact, both of the extensions of the vanilla TD that we consider implement intertwining.
3 Partial Correctness of TD with Warrowing
The first extension of TD with widening and narrowing that we consider here, is \(\hbox {TD}_{\boxslash }\). This solver employs a warrowing operator as proposed by Apinis et al. [8] to dynamically switch between widening and narrowing:
Definition 4
(Warrowing Operator) For a widening operator \(\nabla \) and a narrowing operator \(\mathrm \Delta \), the corresponding warrowing operator \(\boxslash :\mathbb D \rightarrow \mathbb D \rightarrow \mathbb D \) is defined by
In this section, we provide an introduction to \(\hbox {TD}_{\boxslash }\), and then present its proof of partial correctness. The code of \(\hbox {TD}_{\boxslash }\) is shown in Fig. 1. As other variants of TD, \(\hbox {TD}_{\boxslash }\) implements a recursive evaluation strategy. In general, unknowns occurring in the right-hand side of some unknown x are iterated to obtain their best value before computing the value for the right-hand side of x. To implement its evaluation strategy, \(\hbox {TD}_{\boxslash }\) maintains a state with the components \({\texttt{c}}\), \({\sigma }\), \({\texttt{infl}}\), \({\texttt{stable}}\), and \({\texttt{point}}\). Set \({\texttt{c}}\) collects all unknowns already called, i. e., unknowns for which an iteration has been started (and not yet completed). It is used to avoid infinite descent into cyclic dependencies. The mapping \({\sigma } \) stores for each unknown its current value from \(\mathbb D \). Function \(\mathtt {query_{\boxslash }}\) is a wrapper around \({\sigma } \): when the queried unknown \(\texttt{x}\) is already in \({\texttt{c}}\), its value is simply looked up in \({\sigma }\); otherwise, \(\mathtt {iterate_{\boxslash }}\) is called for \(\texttt{x}\) to determine its latest value. The unknown \(\texttt{x}\) is queried during the evaluation of the right-hand side of some unknown \(\texttt{y}\). This unknown \(\texttt{y}\) is passed as an additional argument to the function \(\mathtt {query_{\boxslash }}\)—allowing to record the influence of \(\texttt{x}\) onto \(\texttt{y}\) in the mapping \({\texttt{infl}}\). Function \(\mathtt {iterate_{\boxslash }}\) repeatedly evaluates the right-hand side of \(\texttt{x}\), and applies warrowing if \(\texttt{x}\) is in \({\texttt{point}}\), until stabilization.
Restricting the application of \(\boxslash \) to unknowns from the dedicated set \({\texttt{point}}\) may improve precision compared to unconditionally applying widening and narrowing at every unknown. The set \({\texttt{point}}\) is not statically given beforehand, but dynamically detected during the iteration. Thus, \(\hbox {TD}_{\boxslash }\) does not require insights into the application, or static preprocessing of the equation system. Unknowns are added to \({\texttt{point}}\) in \(\mathtt {query_{\boxslash }}\) when the queried unknown is already called, i. e., when it (indirectly) depends on itself. An unknown \(\texttt{x}\) is removed from \({\texttt{point}}\) again after stabilization in \(\mathtt {iterate_{\boxslash }}\). This removal from \({\texttt{point}}\) has been proposed by Tilscher et al. [21] as further enhancement of precision, e. g., when analyzing nested loops. In particular, it naturally solves the first motivating example of Halbwachs and Henry [22], while it is not sufficient to solve the second.
As an optimization, unknowns that need not be re-evaluated and whose value can instead simply be looked up in \({\sigma }\), are collected in the set \({\texttt{stable}}\). Unknowns are optimistically added to \({\texttt{stable}}\) before an evaluation of their right-hand side. Yet, if the value for some unknown x in \({\sigma } \) is updated in \(\mathtt {iterate_{\boxslash }}\), the values of all unknowns (directly or indirectly) influenced by x are potentially out-dated and must thus be removed from \({\texttt{stable}}\). This recursive removal is implemented by the function \(\texttt{destabilize}\) which also resets all processed influences.
Example 3
(A fixpoint computation of \(\hbox {TD}_{\boxslash }\)) Consider the equation system from Example 1 again, where unknowns x, y and z represent upper bound invariants of the loop counter \(\texttt{i}\) at the beginning of the program, the loop head and the end of the program, respectively. The widening and narrowing operators for the integer chain lattice shall be defined as in Example 2. Assume \(\hbox {TD}_{\boxslash }\) is executed to compute the invariant for unknown z and all unknowns it depends on. We visualize the recursive function calls occurring during the run of \(\hbox {TD}_{\boxslash }\) with a computation trace [13]. The tags \(\texttt{S}\), \(\texttt{I}\) and \(\texttt{Q}\) refer to calls of the functions \(\mathtt {solve_{\boxslash }}\), \(\mathtt {iterate_{\boxslash }}\), and \(\mathtt {query_{\boxslash }}\), respectively. The order in which the functions are called during the execution corresponds to a preorder traversal of the tree. Calls to function \(\mathtt {eval_{\boxslash }}\) occur between every \(\texttt{I}\) and \(\texttt{Q}\) node, but are not displayed for clarity. Each node also states the current unknown of focus, i. e., the first argument for \(\mathtt {solve_{\boxslash }}\) and \(\mathtt {iterate_{\boxslash }}\) calls and the second argument for \(\mathtt {query_{\boxslash }}\) calls, and the value returned for it. The superscript \(\texttt{W}\) or \(\texttt{N}\) of a node \(\texttt{I}\) indicates that widening, or narrowing respectively, is applied in this iteration.
\(\hbox {TD}_{\boxslash }\) ’s execution starts with the call to function \(\mathtt {solve_{\boxslash }}\) for unknown z shown at the top of the computation trace. This starts the iteration on unknown z, shown at the second level of the trace. When evaluating z’s right-hand side, \(\hbox {TD}_{\boxslash }\) descends into the queried unknowns, in this case y, and iterates them until stabilization before backtracking. The iteration on y evaluates y’s right-hand side repeatedly. When y is queried in y’s right-hand side, \(\hbox {TD}_{\boxslash }\) detects that it is already called, stops the recursive descend, adds y to the set of warrowing points, and continues evaluation with the latest value of y. Due to becoming a warrowing point in the first iteration, widening is applied to y’s increased value (note the superscript \(\texttt{W}\)) in the second iteration. In the following iterations, y’s value only improves, and thus narrowing (note the superscript \(\texttt{N}\)) is applied until stabilization. \(\hbox {TD}_{\boxslash }\) then backtracks to the iteration on z. Since z does not recursively depend on itself, it remains stable when updating its value, and its iteration finishes without another evaluation of its right-hand side.
For proving partial correctness of the vanilla TD, Stade et al. [13, 14] define two predicates for TD—an invariant characterizing well-formed solver states, and another predicate describing consistent updates from input to output solver states. The well-formedness of solver states ensures, e. g., that enough dependencies are recorded in \({\texttt{infl}}\), such that unknowns are indeed removed from \({\texttt{stable}}\) when affected by a change. Consistent updates, on the other hand, are essential for our proof that the well-formedness of solver states is preserved throughout the solver’s executions. In the subsequent Definitions 5 and 6, we identify those parts of the corresponding predicates in [13, 14] that still hold for \(\hbox {TD}_{\boxslash }\).
Definition 5
(Well-formed Stable Set and Influence Mapping) A solver state s has a well-formed stable set and influence mapping (denoted by \({\textsf {well} } s\)) if
-
(i)
\(s.\texttt{c} \subseteq s.\!{\texttt{stable}} \),
-
(ii)
\(\left\{ x \in \mathcal {U} \mid s.\!{\texttt{infl}}\ x\, \ne \, [\,] \right\} \subseteq s.\!{\texttt{stable}} \), and
-
(iii)
\(\forall y \in s.\!{\texttt{stable}} \, -\, s.\texttt{c}.\ \forall x \in {\texttt{dep}} \; s.\!{\sigma } \, y.\ y \in set\,(s.\!{\texttt{infl}}\ x)\).
Definition 6
(Consistent Updates of Stable Set and Influence Mapping) For \(x \in \mathcal {U} \), the stable set and influence mapping of a solver state s are consistently updated to those of a solver state \(s'\) (denoted by \({\textsf {update} } \, x\, s\, s'\)) if
-
(i)
\(s.\!{\texttt{stable}} \subseteq s'\!.\!{\texttt{stable}} \),
-
(ii)
\(\forall u \in \mathcal {U}.\ {\left( set\,(s'\!.\!{\texttt{infl}}\ u) -set\,(s.\!{\texttt{infl}}\ u) \right) } \cap {(s.\!{\texttt{stable}} -\left\{ x \right\} )} = \emptyset \), and
-
(iii)
\(\forall u \in \mathcal {U}.\ set\,(s.\!{\texttt{infl}}\ u) \subseteq set\,(s'\!.\!{\texttt{infl}}\ u)\).
We prove that all three recursive functions \(\mathtt {query_{\boxslash }}\), \(\mathtt {iterate_{\boxslash }}\) and \(\mathtt {eval_{\boxslash }}\) preserve the well-formedness of the stable set and influence mapping and only apply consistent updates to well-formed solver states:
Lemma 1
(Preservation of Well-formedness of Stable Set and Influence Mapping) Let \(\texttt{s} \) and \(\texttt{s} '\) be two solver states.
-
Assume \(\mathtt {query_{\boxslash }} \, \texttt{y} \, \texttt{x} \, \texttt{s} \) terminates and returns \(( \texttt{d} _{\texttt{x} },\texttt{s} ' )\) as result and \({\textsf {well} } \;\!\texttt{s} \) holds. Then
-
(i)
\({\textsf {well} } \texttt{s} '\),
-
(ii)
\({\textsf {update} } \texttt{y} \, \texttt{s} \, \texttt{s} '\), and
-
(iii)
\(\forall u \in \texttt{s}.\!{\texttt{stable}}.\,\ \texttt{s}.\!{\sigma } \; u\, =\, \texttt{s} '\!.\!{\sigma } \; u\) hold.
Furthermore, in this case (iv) \(\texttt{y} \in set\,(\texttt{s} '\!.\!{\texttt{infl}}\ \texttt{x} )\).
-
(i)
-
Assume \(\mathtt {iterate_{\boxslash }}\ \texttt{x} \ \texttt{s} \) terminates and returns \(( \texttt{d} _{\texttt{x} },\texttt{s} ' )\) as result, \(\texttt{x} \in \texttt{s}.\!{\texttt{c}} \) and \({\textsf {well} } \; \llparenthesis {\texttt{s}\ \texttt{with}\ {\texttt{c}}:= \texttt{s}.\!{\texttt{c}} -\left\{ \texttt{x} \right\} }\rrparenthesis \) hold. Then
-
(i)
\({\textsf {well} } \; \llparenthesis {\texttt{s} '\ \texttt{with}\ {\texttt{c}}:= \texttt{s} '\!.\!{\texttt{c}} -\left\{ \texttt{x} \right\} }\rrparenthesis \),
-
(ii)
\({\textsf {update} } \texttt{x} \, \texttt{s} \, \texttt{s} '\), and
-
(iii)
\(\forall u \in \texttt{s}.\!{\texttt{stable}}.\,\ \texttt{s}.\!{\sigma } \; u\, =\, \texttt{s} '\!.\!{\sigma } \; u\) hold.
Furthermore, in this case (iv) \(\texttt{x} \in \texttt{s} '\!.\!{\texttt{stable}} \).
-
(i)
-
Assume \(\mathtt {eval_{\boxslash }}\ \texttt{x} \ \texttt{t}\ \texttt{s} \) terminates and returns \(( \texttt{d} _{\texttt{x} },\texttt{s} ' )\) as result, and \({\textsf {well} } \;\! \texttt{s} \) holds. Then
-
(i)
\({\textsf {well} } \texttt{s} '\),
-
(ii)
\({\textsf {update} } \texttt{x} \, \texttt{s} \, \texttt{s} '\), and
-
(iv)
\(\forall u \in \texttt{s}.\!{\texttt{stable}}.\,\ \texttt{s}.{\sigma } \;u\, =\, \texttt{s} '\!.\!{\sigma }\ u\) hold.
Furthermore, in this case (iv) \(\forall u \in {\texttt{dep}}\ \texttt{s} '\!.\!{\sigma } \,\texttt{t}.\,\ \texttt{x} \in set\,(\texttt{s} '\!.\!{\texttt{infl}}\ u)\).
-
(i)
The proof resembles the partial correctness proof for TD [13]. We use conditional induction rules generated by Isabelle for the three mutual recursive functions to apply a computation induction [23] that follows their recursive structure. Additionally, we apply case distinctions for the branching decisions of the solver. Cases where no recursive function call occurs, such as a call of function \(\mathtt {iterate_{\boxslash }}\) for an unknown already in \({\texttt{stable}}\), constitute the base cases of the induction. In an induction step, each occurring recursive function call is described by an induction hypotheses. An example for an induction step is a call of function \(\mathtt {iterate_{\boxslash }}\) for an unknown \(\texttt{x} \) not in \({\texttt{stable}}\) and not in \({\texttt{point}}\) where the evaluation of \(\texttt{x} \) ’s right-hand side returns a changed value and iteration continues.
Based on the well-formedness of \({\texttt{stable}}\) and \({\texttt{infl}}\) we prove the partial correctness of \(\hbox {TD}_{\boxslash }\). The solver is partially correct if, in case of termination, the initially queried unknown is in \(\mathtt {{\texttt{stable}}}\) and the computed \({\sigma }\) is a partial post-solution (Definition 1) for \(\mathtt {{\texttt{stable}}}\) and the given equation system. Since \(\hbox {TD}_{\boxslash }\), similarly to TD, adds unknowns optimistically to \({\texttt{stable}}\), only truly stable unknowns, i. e., unknowns in \({\texttt{stable}} -{\texttt{c}} \), have been iterated up to termination. In contrast to TD, \(\hbox {TD}_{\boxslash }\) does not maintain a partial solution but a partial post-solution for truly stable unknowns. We prove that all three recursive functions \(\mathtt {query_{\boxslash }}\), \(\mathtt {iterate_{\boxslash }}\) and \(\mathtt {eval_{\boxslash }}\), preserve this similar, but different solver state invariant.
Lemma 2
(Preservation of Partial Post-Solution in \({\sigma }\)) Let \(\texttt{s}\) and \(\texttt{s} '\) be two solver states.
-
Assume \(\mathtt {query_{\boxslash }}\ \texttt{y} \ \texttt{x} \ \texttt{s} \) terminates and returns \(( \texttt{d} _{\texttt{x} },\texttt{s} ' )\) as result, and further \({\textsf {well} } \texttt{s} \), and \(\forall u \in \texttt{s}.\!{\texttt{stable}} -\ \texttt{s}.\!{\texttt{c}}.\ \texttt{eq}\ ({\mathcal {T}} \, u)\ \texttt{s}.\!{\sigma } \, \le \, \texttt{s}.\!{\sigma } \, u\) hold. Then \(\texttt{s} '\) stores a partial post-solution for all truly stable unknowns: \(\forall u \in \texttt{s} '\!.\!{\texttt{stable}} -\ \texttt{s} '\!.\!{\texttt{c}}.\,\ \texttt{eq}\ ({\mathcal {T}} \, u)\ \texttt{s} '\!.\!{\sigma } \, \le \, \texttt{s} '\!.\!{\sigma }\ u\).
-
Assume \(\mathtt {iterate_{\boxslash }}\ \texttt{x} \ \texttt{s} \) terminates and returns \(( \texttt{d} _{\texttt{x} },\texttt{s} ' )\) as result and further \(\texttt{x} \in \texttt{s}.\!{\texttt{c}} \), \({\textsf {well} } \; \llparenthesis {\texttt{s}\ \texttt{with}\ {\texttt{c}}:= \texttt{s}.\!{\texttt{c}} -\ \left\{ \texttt{x} \right\} }\rrparenthesis \), and \(\forall u \in \texttt{s}.\!{\texttt{stable}} -\ (\texttt{s}.\!{\texttt{c}} -\ \left\{ \texttt{x} \right\} ).\ \texttt{eq}\ ({\mathcal {T}} \, u)\ \texttt{s}.\!{\sigma } \, \le \, \texttt{s}.\!{\sigma } \, u\) hold. Then \(\texttt{s} '\) stores a partial post-solution for all truly stable unknowns: \(\forall u \in \texttt{s} '\!.\!{\texttt{stable}} -\ (\texttt{s} '\!.\!{\texttt{c}} -\ \left\{ \texttt{x} \right\} ).\,\ \texttt{eq}\ ({\mathcal {T}} \, u)\ \texttt{s} '\!.\!{\sigma } \, \le \, \texttt{s} '\!.\!{\sigma }\ u\).
-
Assume \(\mathtt {eval_{\boxslash }}\ \texttt{x} \ \texttt{t}\ \texttt{s} \) terminates and returns \(( \texttt{d} _{\texttt{x} },\texttt{s} ')\) as result and further \(\texttt{x} \in \texttt{s}.\!{\texttt{stable}} \), \({\textsf {well} } \texttt{s} \), and \(\forall u \in \texttt{s}.\!{\texttt{stable}} -\ \texttt{s}.\!{\texttt{c}}.\ \texttt{eq} \, ({\mathcal {T}} \, u)\, \texttt{s}.\!{\sigma } \, \le \, \texttt{s}.\!{\sigma } \, u\) hold. Then \(\texttt{s} '\) stores a partial post-solution for all truly stable unknowns: \(\forall u \in \texttt{s} '\!.\!{\texttt{stable}} -\ \texttt{s} '\!.\!{\texttt{c}}.\,\ \texttt{eq}\ ({\mathcal {T}} \, u)\ \texttt{s} '\!.\!{\sigma } \, \le \, \texttt{s} '\!.\!{\sigma }\ u\). Additionally, \(\texttt{eq}\ \texttt{t}\ \texttt{s} '\!.\!{\sigma } =\, \texttt{d} _{\texttt{x} }\) holds.
Again, the lemma is proven by induction on the computation trace. The new cases of \(\hbox {TD}_{\boxslash }\) compared to TD concern the application of the warrowing operator when the iterated unknown is in \({\texttt{point}}\). Here, we rely on the following two essential properties of warrowing:
Lemma 3
Let \(\boxslash :\mathbb D \rightarrow \mathbb D \rightarrow \mathbb D \) be a warrowing operator. Then for all \(a, b \in \mathbb {D}\),
-
(i)
\(b \le a \boxslash b\) (Warrowing Lower Bound)
-
(ii)
If \(a \boxslash b = a\), then \(b \le a\). (Warrowing Fixpoint Inequality)
With the initial solver state, i. e., the arguments with which \(\texttt{iterate} _{\!\!\boxslash }\) is called in function \(\texttt{solve} _{\!\!\boxslash }\), being well-formed, we then follow that TD returns a partial post-solution for all unknowns in \({\texttt{stable}}\) including the queried unknown.
Theorem 1
(Partial Correctness of \(\hbox {TD}_{\boxslash }\)) Assume that a call to \(\mathtt {solve_{\boxslash }} \,\texttt{x} \) terminates, and returns \(({\sigma }, {\texttt{stable}})\) as result. Then \({\sigma } \) is a partial post-solution for \({\texttt{stable}}\) and \(\texttt{x} \in {\texttt{stable}} \).
4 Termination of TD with Widening/Narrowing Phases
\(\hbox {TD}_{\boxslash }\) is guaranteed to return a partial post-solution—whenever it terminates. Seidl and Vogler [11] show with an example that it is, however, not guaranteed to terminate when right-hand sides may be non-monotonic. They therefore propose an alternative extension of TD where each encountered unknown is first iterated with widening, and then narrowed in a second phase.
Here, we consider an implementation of this phase solver \(\hbox {TD}_{\text {w/n}}\) that maintains a set \({\texttt{point}}\) like \(\hbox {TD}_{\boxslash }\). Its function \(\mathtt {iterate_{w/n}}\) (shown in Fig. 2) is equipped with an additional parameter \(\texttt{phase}\). In function \(\mathtt {solve_{w/n}}\) and \(\mathtt {query_{w/n}}\), the iteration of an unknown is always started with a widening phase. In \(\mathtt {iterate_{w/n}}\) the parameter \(\texttt{phase}\) then dictates for unknowns in \({\texttt{point}}\), whether widening or narrowing is applied. If the value of an iterated unknown \(\texttt{x}\) in \({\texttt{point}}\) stabilizes and the phase is \(\texttt{N}\), iteration terminates. If, on the other hand, the value of \(\texttt{x}\) in \({\texttt{point}}\) stabilizes and the phase is \(\texttt{W}\), \(\texttt{x}\) is destabilized and \(\mathtt {iterate_{w/n}\ x}\) is called with phase argument \(\texttt{N}\) to start the narrowing phase. Since \({\sigma }\) is unchanged, the evaluation of the right-hand side of \(\texttt{x}\) in the first narrowing iteration would return the same value as in the last widening iteration. Thus, we implement an extra optimization to avoid the unnecessary re-evaluation and immediately apply narrowing when the widening iteration stabilizes.
We prove that \(\hbox {TD}_{\text {w/n}}\) always terminates—as long as only finitely many unknowns are encountered. For this, we construct a well-founded relation \(<_{\textrm{term}}\) on the arguments of the mutual recursive functions. It is defined as lexicographic order on 5-tuples
where the 5-tuples are extracted from the arguments of the mutual recursive function calls with function \(t\!p\):
In the lexicographic order \(<_{\textrm{term}}\), the order of the first two components is simply the ordering of natural numbers. The partial orders for the last three components are defined as follows:
To prove the termination of \(\hbox {TD}_{\text {w/n}}\) we argue that the termination relation is well-founded and that for every occurring recursive function call, the arguments decrease with respect to \(<_{\textrm{term}}\) compared to the arguments of the surrounding function call. The underlined components extracted by \(t\!p\) sufficiently describe the decrease of the arguments for all occurring recursive calls. The restriction to two phases per unknown and the properties of the widening and narrowing operator ensure that the iteration of an unknown in \({\texttt{point}}\) terminates. The major challenge is to verify that the set \({\texttt{point}}\) maintains sufficiently many unknowns whose iteration is accelerated with widening and narrowing. Assume that the right-hand side of \(\texttt{x} \) is evaluated, and a new value is returned. We claim that, if \(\texttt{x} \) is destabilized and its iteration continues, \(\texttt{x} \) is guaranteed to be in \({\texttt{point}} \) for the next call to \(\mathtt {iterate_{w/n}}\). To prove this, we establish the following invariant:
Definition 7
(Well-formed Point Set) A solver state s has a well-formed set of widening/narrowing points (denoted by \({\textsf {well} _{{\texttt{point}}}} s\)) if
-
\(s.\!{\texttt{point}} \subseteq s.\!{\texttt{c}} \), and
-
\(\{u \in s.\!{\texttt{c}}\ \mid \ s.\!{\texttt{infl}}\ u\ \ne \ [\,]\} \subseteq s.\!{\texttt{point}} \).
An unknown \(\texttt{u}\) is only added to \({\texttt{point}}\) in function \(\mathtt {query_{w/n}}\) when it is already in \({\texttt{c}}\). This implies that an iteration on \(\texttt{u}\) is already on the way. When this iteration on \(\texttt{u}\) terminates, \(\texttt{u}\) is removed from \({\texttt{point}}\) and \({\texttt{c}}\) simultaneously—implying that the invariant \({\texttt{point}} \subseteq {\texttt{c}} \) is preserved. The second condition guarantees that all unknowns in \({\texttt{c}}\) for which influences are recorded in \({\texttt{infl}}\) are in \({\texttt{point}}\). Influences are recorded only when exiting from a call to \(\mathtt {query_{w/n}}\). When recording an influence for an unknown \(\texttt{x}\) in \({\texttt{c}}\), the function \(\mathtt {query_{w/n}}\) also adds \(\texttt{x}\) to \({\texttt{point}}\).
The initial solver state trivially has a well-formed set \({\texttt{point}}\). By induction on the computation trace, we prove that the well-formedness of \({\texttt{point}}\) is preserved by every call to \(\mathtt {iterate_{w/n}}\), \(\mathtt {query_{w/n}}\) and \(\mathtt {eval_{w/n}}\) as long as Definition 5 (i) and (ii) hold for the input solver state.
Lemma 4
(Preservation of Well-formedness of Point Set) Let \(\texttt{s}\) and \(\texttt{s} '\) be two solver states.
-
Assume \(\mathtt {query_{w/n}} \,\texttt{y} \,\texttt{x} \,\texttt{s} \) terminates and returns \((\texttt{d} _\texttt{x} ,\texttt{s} ')\) as result. Further, assume that \(\texttt{s}.\!{\texttt{c}} \subseteq \texttt{s}.\!{\texttt{stable}} \), \(\{u \in \mathcal {U} \mid \texttt{s}.\!{\texttt{infl}}\ u \ne [\,]\} \subseteq \texttt{s}.\!{\texttt{stable}} \) and \({\textsf {well} _{{\texttt{point}}}} \texttt{s} \) hold. Then \({\textsf {well} _{{\texttt{point}}}} \texttt{s} '\) follows.
-
Assume \(\mathtt {iterate_{w/n}} \,\texttt{x} \,\texttt{s} \) terminates and returns \((\texttt{d} _\texttt{x} ,\texttt{s} ')\) as result. Further, assume that \(\texttt{x} \in \texttt{s}.\!{\texttt{c}} \), \(\texttt{s}.\!{\texttt{c}}- \left\{ \texttt{x} \right\} \subseteq \texttt{s}.\!{\texttt{stable}} \), \(\{u \in \mathcal {U} \mid \texttt{s}.\!{\texttt{infl}}\ u \ne [\,]\} \subseteq \texttt{s}.{\texttt{stable}} \) and \({\textsf {well} _{{\texttt{point}}}} \,\llparenthesis {\texttt{s}\ \texttt{with}\ {\texttt{c}}:= \texttt{s}.\!{\texttt{c}}- \left\{ \texttt{x} \right\} ,\ {\texttt{point}}:= \texttt{s}.\!{\texttt{point}}- \left\{ \texttt{x} \right\} }\rrparenthesis \) hold. Then \({\textsf {well} _{{\texttt{point}}}} \,\llparenthesis {\texttt{s} '\ \texttt{with}\ {\texttt{c}}:= \texttt{s} '\!.\!{\texttt{c}}- \left\{ \texttt{x} \right\} ,\ {\texttt{point}}:= \texttt{s} '\!.\!{\texttt{point}}- \left\{ \texttt{x} \right\} }\rrparenthesis \) and \(\texttt{x} \notin \texttt{s} '\!.\!{\texttt{point}} \) follow.
-
Assume \(\mathtt {eval_{w/n}} \,\texttt{x} \,\texttt{t} \,\texttt{s} \) terminates and returns \((\texttt{d} _\texttt{x} ,\texttt{s} ')\) as result. Further, assume that \(\texttt{s}.\!{\texttt{c}} \subseteq \texttt{s}.\!{\texttt{stable}} \), \(\{u \in \mathcal {U} \mid \texttt{s}.\!{\texttt{infl}}\ u \ne [\,]\} \subseteq \texttt{s}.\!{\texttt{stable}} \) and \({\textsf {well} _{{\texttt{point}}}} \texttt{s} \) hold. Then \({\textsf {well} _{{\texttt{point}}}} \texttt{s} '\) follows.
The established properties of \({\texttt{point}}\) are then used for proving that an unknown not in \({\texttt{point}}\) is iterated at most once before being either stable or in \({\texttt{point}}\), and in the second case stays in \({\texttt{point}}\) until its iteration terminates. As a result, we obtain a termination proof for the mutual recursive functions \(\mathtt {query_{w/n}}\), \(\mathtt {iterate_{w/n}}\) and \(\mathtt {eval_{w/n}}\) for input solver states where the \({\texttt{point}}\) set is well-formed, and \({\texttt{c}}\), \({\texttt{stable}}\) and \({\texttt{infl}}\) fulfill conditions (i) and (ii) of Definition 5. Since the initial solver state fulfills these preconditions, definite termination follows for every call to \(\mathtt {solve_{w/n}}\).
Theorem 2
(Termination of \(\hbox {TD}_{\text {w/n}}\)) Assume that the set of unknowns \(\mathcal {U}\) is finite. Then the call \(\mathtt {solve_{w/n}\ x}\) terminates for every unknown \(\texttt{x}\) in \(\mathcal {U} \).
5 Need for Stronger Assumptions for Total Correctness
As we have proven in the last section, \(\hbox {TD}_{\text {w/n}}\) always terminates for arbitrary equation systems when the set of unknowns is finite. Under the assumption that the right-hand side evaluations of \(\hbox {TD}_{\text {w/n}}\) only decrease after reaching a (partial) post-solution, the properties of the narrowing operator guarantee that a (partial) post-solution is preserved. The specification of the narrowing operator provides no guarantees, though, for the case where its second operand, i. e., the right-hand side evaluation for some unknown, is incomparable or greater than its first operand, i. e., the unknown’s current value. Such incomparable or greater right-hand side evaluations during the narrowing phase may occur, e. g., due to right-hand sides being non-monotonic. Without non-monotonic right-hand sides \(\hbox {TD}_{\text {w/n}}\), thus, not necessarily computes a partial post-solutions.
Example 4
(No Partial Post-Solution for Non-Monotonic Right-Hand Sides) Let the domain be \(\mathbb {N} \cup \left\{ \infty \right\} \) equipped with the natural ordering, and widening and narrowing operators from Example 2. Consider the equation
\(\mathtt {x = (if\ x = 0\ then\ 1\ else\ if\ x = 2\ then\ 3\ else\ 2)}\)
adapted from [11] where it serves as an example for non-termination of \(\hbox {TD}_{\boxslash }\). The right-hand side is not monotonic. Consider an execution of \(\hbox {TD}_{\text {w/n}}\) for unknown \(\texttt{x}\), i. e., a call to \(\mathtt {{solve_{w/n}\ x}}\). We present the execution as computation trace, analogously to those for \(\hbox {TD}_{\boxslash }\) described in Example 3. The additional superscript \(\mathtt {W/N}\) for \(\texttt{I}\) nodes marks the last iteration of a widening phase where the widened value stabilizes and narrowing is applied before continuing iteration in the narrowing phase with a call to \(\mathtt {iterate_{w/n}}\).
In the first iteration, \(\texttt{x}\) is added to \({\texttt{point}}\) because it is queried within its right-hand side evaluation ( ). From the second iteration on, widening is applied and results in the value \(\top \) for \(\texttt{x}\). The third iteration subsequently applies narrowing. In the fourth iteration ( ), value 3 is computed for the right-hand side of \(\texttt{x}\), which exceeds the value 2 currently stored in \({\sigma }\). Since \({2\,\mathrm \Delta \,3} = 2\), iteration terminates—although the resulting mapping \(\mathtt {{\sigma }} = \{\texttt{x} \mapsto 2\}\) is not a post-solution.
Even in presence of monotonic right-hand sides, \(\hbox {TD}_{\text {w/n}}\) may not return partial post-solutions due to newly detected dependencies in a narrowing iteration.
Example 5
(No Partial Post-Solution for Non-Monotonic Dependencies) To construct a counterexample, it suffices to consider \(\mathcal {U} = \left\{ x,y,u \right\} \), \(\mathbb D = \left\{ 0,1,2,3,4 \right\} \) with the order \(<_\mathbb {N}\), and the widening and narrowing operators defined in Example 2. Figure 3 shows an equation system with monotonic right-hand sides and the computation trace of \(\hbox {TD}_{\text {w/n}}\) for unknown y.
During the last narrowing phase of unknown \(\texttt{y}\), \(\hbox {TD}_{\text {w/n}}\) discovers a new dependency on the fresh unknown \(\texttt{u}\) ( ). Iterating \(\texttt{u}\) for the first time increases its value ( ). This in turn, also increases the value of the unknown \(\texttt{x}\) that was fully iterated in \(\texttt{y}\) ’s final widening phase to value 3, and is now only re-iterated to possibly improve its value. While the monotonicity of the right-hand sides still guarantees that \(\texttt{x}\) ’s increasing values remain bounded by 3, an application of widening escalates the value of \(\texttt{x}\) beyond, namely to 4 ( ). With non-monotonic dependencies, it is thus not guaranteed that values only decrease after having reached a post-solution in the widening phase. With the increased value for \(\texttt{x}\) and the decreased value for \(\texttt{y}\), the final narrowing iteration for \(\texttt{y}\) may return any, in particular, a larger or incomparable value—despite monotonic right-hand sides. In our case, evaluation of the right-hand side for \(\texttt{y}\) returns 4, which is narrowed to 3 ( ). Thus, iteration on y terminates, but not with a partial post-solution.
As a dedicated property, we therefore introduce monotonicity of dependencies. In equation systems where dependencies of right-hand sides are independent of value mappings, this property is trivially satisfied.
Definition 8
(Monotonic Dependencies) A strategy tree t has monotonic dependencies if \(\forall {\sigma } _1, {\sigma } _2.\ {\sigma } _1 \le {\sigma } _2 \implies {\texttt{dep}}\ t\ {\sigma } _1 \subseteq {\texttt{dep}}\ t\ {\sigma } _2\).
We identify yet another obstacle for \(\hbox {TD}_{\text {w/n}}\) to return partial post-solutions, namely, widening operators which are not precise.
Definition 9
(Precise Widening Operator) A widening operator \(\nabla :\mathbb D \rightarrow \mathbb D \rightarrow \mathbb D \) is precise if for all \(a,b \in \mathbb D \), it holds that \(b \le a \implies a\ \nabla \ b = a\).
Even with monotonic right-hand sides and monotonic dependencies, \(\hbox {TD}_{\text {w/n}}\) is not guaranteed to return partial post-solutions when the widening operator is not precise.
Example 6
(No Partial Post-Solution with Non-Precise Widening) For \(\mathcal {U} = \{\texttt{x},\texttt{y} \}\) and \(\mathbb D = \left\{ 0,1,2,3,4,5 \right\} \) with the order \(<_\mathbb {N}\), consider the equation system \({\mathcal {T}} \,\) with monotonic right-hand sides as well as monotonic dependencies:
Let the widening and narrowing operators be defined as
The computation trace for a call to \(\mathtt {solve_{w/n}\ y}\) is shown below:
At the end of the widening phase of \(\texttt{y}\), the value of unknown \(\texttt{x}\) is 4 ( ). With the intent to improve its value, unknown \(\texttt{x}\) is destabilized to be re-iterated in following narrowing phase of \(\texttt{y}\). Since \(\hbox {TD}_{\text {w/n}}\) starts iterations always with a widening phase, the value of \(\texttt{x}\) is widened, although the value of its right-hand side decreased to 3 ( ). The given widening operator returns the large value 5 when computing \(3\ \nabla \ 3\) for \(\texttt{x}\). This value is not accounted for by \(\texttt{y}\), since \(\texttt{y}\) is already in the narrowing phase ( ). Thus, using widening operators that carelessly escalate values even if their second arguments are less or equal than their first, may ruin partial post-solutions found when a widening phase terminated.
Many widening operators used in practice are precise, e. g., the widening operator from Example 2, or the standard widening operators for intervals or polyhedra [5, 16, 24]. Moreover, a precise widening operator can be constructed from any, possibly non-precise, widening operator.
Lemma 5
(Construction of Precise Widening Operators) Let \(\nabla \) be some widening operator for \(\mathbb D \) as defined in Definition 2. Then, \(\nabla ^p\) defined as
is a precise widening operator.
Proof
First, we argue that \(\nabla ^p\) fulfills the termination property of widening operators (Definition 2 (ii)). Consider an arbitrary sequence \((b_i)_{i \in \mathbb {N}}\) of elements in \(\mathbb D \). Let \((a_i)_{i\in \mathbb {N}}\) be the sequence defined by \(a_1 = b_1\) and \(a_i = a_{i-1}\ \nabla ^p\ b_i\) for \(i > 1\). Let I denote the set of all k where \(a_k\ne a_{k-1}\). Then for every \(k\in I\), \(b_k \nleq a_{k-1}\), and therefore, \(a_k = a_{k-1} \nabla \ b_k\). The subsequence of \((a_i)_{i\in I}\), thus, is a sequence of applications of the \(\nabla \) operator for the subsequence \((b_i)_{i\in I}\), and is thus guaranteed to be finite. From this, we conclude that the sequence \((a_i)\) of precise widening operations stabilizes. The other properties demanded for precise widening operators follow directly from the construction and the properties of the underlying widening operator. \(\square \)
6 Total Correctness Through Equivalence
While \(\hbox {TD}_{\boxslash }\) is partially correct for arbitrary equation systems, but may not terminate with non-monotonic right-hand sides, \(\hbox {TD}_{\text {w/n}}\) has the opposite property: guaranteed to terminate, but not necessarily returning partial post-solutions. And yet, both solvers are surprisingly similar. Under the three extra assumptions that the widening operator is precise, and that input equation systems have right-hand sides which are monotonic with monotonic dependencies, we find that values of unknowns only decrease in narrowing iterations. This implies that the warrowing operator of \(\hbox {TD}_{\boxslash }\) will never apply widening to an unknown once having started to apply narrowing. Likewise, \(\hbox {TD}_{\text {w/n}}\) preserves partial post-solutions during the narrowing phase. Subsequently, we make this observation precise and prove equivalence of the two solvers. Our equivalence proof builds upon the partial correctness proof of \(\hbox {TD}_{\boxslash }\) and is structured into three parts: (i) We design ghost variables that describe the solver’s history in more detail than the solver state; (ii) we establish well-formedness invariants about these ghost variables and their relation to the solver state; and (iii) we derive the equivalence of the two solvers based on these strengthened well-formedness invariants.
Introducing ghost variables.
With the invariant from Definition 5 we have established that during a solver’s run, the current value mapping \({\sigma }\) generally contains a partial post-solution for all unknowns in \({\texttt{stable}}- {\texttt{c}} \). \(\hbox {TD}_{\boxslash }\) may, however, remove unknowns from \({\texttt{stable}}\) through destabilization and continue iteration on some \(\texttt{x}\) with narrowing—even though a partial post-solution for \(\texttt{x}\) has already been found. To describe such unknowns whose value is only improved and which are not captured by the solver state, we introduce three ghost variables:
-
\({\texttt{c}} _{{\texttt{post}}}\): unknowns in \({\texttt{c}}\) which are iterated with narrowing to improve their values,
-
\({\texttt{post}}\): a superset of \({\texttt{stable}}\) to additionally store unknowns for which a post-solution is found but which are destabilized by narrowed unknowns, and
-
\({\mathtt {infl_{post}}}\): a mapping tracking influences between unknowns from \({\texttt{post}}\) and preserving influences when destabilizing narrowed unknowns.
Figure 4 shows an extended definition of \(\hbox {TD}_{\boxslash }\) that additionally tracks these ghost variables as part of its solver state. It serves as explanation how the ghost variables conceptually evolve throughout \(\hbox {TD}_{\boxslash }\)’s computations. In the formalization, we forego such an explicit definition of \(\hbox {TD}_{\boxslash }\) extended with ghost variables. Instead, the ghost variables are additional variables in lemmas and proofs that describe the solver’s history beyond the abstractions of the solver state.
The design of \({\texttt{c}} _{{\texttt{post}}}\), \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\) closely aligns with their counterparts in the solver state, i. e., \({\texttt{c}}\), \({\texttt{stable}}\) and \({\texttt{infl}}\). In contrast to \({\texttt{c}}\), unknowns are added to \({\texttt{c}} _{{\texttt{post}}}\) not before starting their iteration, but only when their iteration reaches a partial post-solution (w.r.t. the values of other unknowns in \({\texttt{c}}\)) and continues to improve it. The difference between \({\texttt{post}}\)/\({\mathtt {infl_{post}}}\), and \({\texttt{stable}}\)/\({\texttt{infl}}\) lies in when and how they are pruned. Whenever the value of an iterated unknown \(\texttt{x}\) changes, destabilization removes all unknowns transitively influenced by \(\texttt{x}\), i. e., all unknowns in \({\texttt{infl}} ^+ \texttt{x} \), from \({\texttt{stable}}\) and resets their entries in \({\texttt{infl}}\). In contrast, \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\) are kept unchanged when \(\texttt{x}\) ’s value changes through narrowing, and are pruned only when \(\texttt{x}\) is not in \({\texttt{point}}\) or its value changes through widening. By keeping \({\mathtt {infl_{post}}}\) unchanged after narrowing iterations where the set of dependencies potentially decreases, entries in \({\mathtt {infl_{post}}}\) may become outdated, though. We call these left-over entries spurious dependencies and refer the reader to Appendix B for a concrete example of a \(\hbox {TD}_{\boxslash }\) run where spurious dependencies occur. Due to spurious dependencies, pruning based on \({\mathtt {infl_{post}}}\) would potentially remove more unknowns from \({\texttt{post}}\) than the destabilization with \({\texttt{infl}}\) removes from \({\texttt{stable}}\). To ensure that \({\texttt{stable}}\) remains a subset of \({\texttt{post}}\), the pruning of \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\) is thus restricted: Transitively influenced unknowns are removed only up to the unknowns still stable after the destabilization for \({\texttt{stable}}\) and \({\texttt{infl}}\). We denote the associated transitive closure of a map \(m: \mathcal {U} \rightarrow \mathcal {U}\ \texttt{list} \) up to but excluding a barrier set B as \(m^+_{|B}: \mathcal {U} \rightarrow \mathcal {P\left( \mathcal {U} \right) } \) and define it inductively:
The pruning of \({\mathtt {infl_{post}}} \) and \({\texttt{post}} \) for unknown \(\texttt{x}\) can then be described as
where the barrier set \({\texttt{stable}} '\) is the set of stable unknowns returned by the preceding call \(\mathtt {destabilize\ x\ state.\!{\texttt{infl}}\ state.\!{\texttt{stable}}}\) and where the notation \(m \oplus S\) for a set of updates S serves as abbreviation for multiple updates of mapping m.
Establishing well-formedness invariants for the ghost variables.
We define an invariant \({\textsf {well} _{{\texttt{post}}}} \) that characterizes well-formed ghost variables and relates them to the solver state components:
Definition 10
(Well-formed Post Data Structures) For a solver state s, the ghosts \({\texttt{c}} _{{\texttt{post}}},{\texttt{post}} \subseteq \mathcal {U} \), and \({\mathtt {infl_{post}}}: \mathcal {U} \rightarrow \mathcal {U}\ ~\texttt{list} \) are well-formed (denoted by \({\textsf {well} _{{\texttt{post}}}} \,s\,{\texttt{c}} _{{\texttt{post}}} \,{\texttt{post}} \,{\mathtt {infl_{post}}} \)) if
-
(i)
\({\texttt{c}} _{{\texttt{post}}} \subseteq s.\!{\texttt{c}} \),
-
(ii)
\(s.\!{\texttt{stable}} \subseteq {\texttt{post}} \),
-
(iii)
\(\forall u \in \mathcal {U}.\,\ set\,(s.\!{\texttt{infl}}\ u) \subseteq set\,({\mathtt {infl_{post}}}\ u)\)
-
(iv)
\(\left\{ u \in \mathcal {U} \mid {\mathtt {infl_{post}}}\ u\, \ne \, [\,] \right\} \subseteq {\texttt{post}} \),
-
(v)
\(\forall u \in {\texttt{post}} -\, (s.\!{\texttt{c}} -\, {\texttt{c}} _{{\texttt{post}}}).\,\ \forall v \in {\texttt{dep}} \; s.\!{\sigma } \; u.\,\ u \in set\,({\mathtt {infl_{post}}}\ v)\), and
-
(vi)
\(\forall u \in {\texttt{post}} -\, (s.\!{\texttt{c}} -\, {\texttt{c}} _{{\texttt{post}}}).\,\ \texttt{eq}\ ({\mathcal {T}} u)\ s.\!{\sigma } \, \le \, s.\!{\sigma }\ u\).
The first three items ensure that the introduced ghost variables \({\texttt{c}} _{{\texttt{post}}}\), \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\) are indeed a subset of \({\texttt{c}}\), a superset of \({\texttt{stable}}\), and a mapping with entries subsuming the entries in \({\texttt{infl}}\), respectively. Item (iv) and (v) define well-formedness criteria for \({\mathtt {infl_{post}}}\) and \({\texttt{post}}\) similar to the properties specified for \({\texttt{stable}}\) and \({\texttt{infl}}\) in Definition 5. While truly stable unknowns are all unknowns in \({\texttt{stable}} -{\texttt{c}} \), truly post unknowns are all unknowns in \({\texttt{post}} -({\texttt{c}} -{\texttt{c}} _{{\texttt{post}}})\). The last item states that for all truly post unknowns, a partial post-solution has already been found.
We complement the predicate \({\textsf {well} _{{\texttt{post}}}} \) and introduce an update predicate that relates ghosts before a function call to adapted ghosts after the function call.
Definition 11
(Consistent Post Data Structure Updates) Assume \(x \in \mathcal {U} \) and let s, \(s'\) be two solver states. Given \({\texttt{c}} _{{\texttt{post}}} \subseteq \mathcal {U} \), both \({\texttt{post}} \subseteq \mathcal {U} \) and \({\mathtt {infl_{post}}}: \mathcal {U} \rightarrow \mathcal {U}\ \texttt{list} \) are consistently updated to \({\texttt{post}} ' \subseteq \mathcal {U} \) and \({\texttt{infl}^{\prime }_\texttt{post}}: \mathcal {U} \rightarrow \mathcal {U} \,~~ \texttt{list} \) (denoted by \({\textsf {update} _{{\texttt{post}}}} \,x\,s\,s'\,{\texttt{c}} _{{\texttt{post}}} \,{\texttt{post}} \,{\mathtt {infl_{post}}} \,{\texttt{post}} '\,{\texttt{infl}^{\prime }_\texttt{post}} \)) if
-
(i)
\(\forall u \in {\texttt{post}}.\,\ s'\!.\!{\sigma }\ u \le s.\!{\sigma }\ u\),
-
(ii)
\({\texttt{post}} \subseteq {\texttt{post}} '\),
-
(iii)
\(\forall u \in \mathcal {U}.\,\ {\left( set\,({\texttt{infl}^{\prime }_\texttt{post}} \,u) {-} set\,({\mathtt {infl_{post}}} \,u) \right) } \cap {({\texttt{post}} {-} (\left\{ x \right\} {-} {\texttt{c}} _{{\texttt{post}}}))} = \emptyset \), and
-
(iv)
\(\forall u \in \mathcal {U}.\,\ set\,({\mathtt {infl_{post}}} u) \subseteq set\,({\texttt{infl}^{\prime }_\texttt{post}} u)\).
The first item specifies that values of unknowns already in \({\texttt{post}}\) may only decrease or stay unchanged. This is derived from the monotonicity assumptions and serves to ensure that \({\sigma } \) remains a partial post-solution for unknowns in \({\texttt{post}} -({\texttt{c}} -{\texttt{c}} _{{\texttt{post}}})\) (Definition 10 (vi)). While the other items of \({\textsf {update} _{{\texttt{post}}}} \) closely resemble those defined for \({\texttt{stable}}\) and \({\texttt{infl}}\) in Definition 6, there is a subtle but crucial difference between Definition 11 (iii) and Definition 6 (ii). Definition 6 (ii) is justified since the solver never descends to evaluate already stable unknowns, and thus, no new influences pointing to these are recorded. In contrast, \(\hbox {TD}_{\boxslash }\) may descend to re-iterate unknowns in \({\texttt{post}}\) and collect newly found influences in \({\texttt{infl}^{\prime }_\texttt{post}}\). The assumptions of monotonic right-hand sides and monotonic dependencies ensure, though, that the newly found influences pointing to unknowns already in \({\texttt{post}}\) are a subset of the previously found influences in \({\mathtt {infl_{post}}}\).
We show for \(\hbox {TD}_{\boxslash }\) that there exist well-formed post data structures satisfying Definition 10 throughout the solver’s computations and that they are updated consistently (Definition 11) by any occurring function call \(\mathtt {query_{\boxslash }}\), \(\mathtt {iterate_{\boxslash }}\) or \(\mathtt {eval_{\boxslash }}\). During the solver’s computations, function \(\mathtt {eval_{\boxslash }}\) is only called to evaluate strategy trees reachable when evaluating a right-hand side with \({\sigma }\) of the current solver state. To restrict our claim to these calls, we define a function \({\texttt{subt}}\) that partially descends into a strategy tree t with value mapping \({\sigma }\). Provided with a list of unknowns as second parameter, it checks that the list correctly describes a prefix of the unknowns queried when evaluating t with \({\sigma }\). In case the checks succeed, the reached subtree is returned.
By exhibiting the prefix of queried unknowns, we can also formulate further properties these unknowns fulfill at any occurring function call of \(\mathtt {eval_{\boxslash }}\), such as being stable.
Lemma 6
(Preservation of Well-formedness of Post Data Structures) Assuming the equation system has monotonic right-hand sides with monotonic dependencies, the following holds:
-
Assume \(\mathtt {query_{\boxslash }} \,\texttt{y} \,\texttt{x} \,\texttt{s} \) terminates and returns \(( \texttt{d} _{\texttt{x} },\texttt{s} ' )\) as result and \({\textsf {well} } \texttt{s} \), and \({\textsf {well} _{{\texttt{post}}}} \texttt{s} \,{\texttt{c}} _{{\texttt{post}}} \,{\texttt{post}} \,{\mathtt {infl_{post}}} \) hold for some post data structures \({\texttt{c}} _{{\texttt{post}}}\), \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\). Also, assume that \(\texttt{x} \in {\texttt{dep}}\ \texttt{s}.\!{\sigma }\ \texttt{y} \). Then there exist post data structures \({\texttt{post}} '\) and \({\texttt{infl}^{\prime }_\texttt{post}} \) such that
-
(i)
\({\textsf {well} _{{\texttt{post}}}} \,\texttt{s} '\,{\texttt{c}} _{{\texttt{post}}} \,{\texttt{post}} '\,{\texttt{infl}^{\prime }_\texttt{post}} \), and
-
(ii)
\({\textsf {update} _{{\texttt{post}}}} \,\texttt{y} \,\texttt{s} \,\texttt{s} '\,{\texttt{c}} _{{\texttt{post}}} \,{\texttt{post}} \,{\mathtt {infl_{post}}} \,{\texttt{post}} '\,{\texttt{infl}^{\prime }_\texttt{post}} \) hold.
-
(i)
-
Assume \(\mathtt {iterate_{\boxslash }} \,\texttt{x} \,\texttt{s} \) terminates and returns \(( \texttt{d} _{\texttt{x} },\texttt{s} ' )\) as result and \({\textsf {well} } \,\,\llparenthesis {\texttt{s} \,\texttt{with} \,{\texttt{c}}:= \texttt{s}.\!{\texttt{c}} -\left\{ \texttt{x} \right\} }\rrparenthesis \), and \({\textsf {well} _{{\texttt{post}}}} \,\llparenthesis {\texttt{s} \,\texttt{with} \,{\texttt{c}}:= \texttt{s}.\!{\texttt{c}} -\left\{ \texttt{x} \right\} }\rrparenthesis \,({\texttt{c}} _{{\texttt{post}}} -\left\{ \texttt{x} \right\} )\,{\texttt{post}} \,{\mathtt {infl_{post}}} \) hold for some post data structures \({\texttt{c}} _{{\texttt{post}}}\), \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\). Also, assume that \(\texttt{x} \in \texttt{s}.\!{\texttt{c}} \) and \((\texttt{x} \notin {\texttt{c}} _{{\texttt{post}}} \implies \texttt{x} \notin {\texttt{post}} -\texttt{s}.\!{\texttt{stable}}) \wedge (\texttt{x} \in {\texttt{c}} _{{\texttt{post}}} \implies \texttt{x} \in {\texttt{post}})\). Then there exist post data structures \({\texttt{post}} '\) and \({\texttt{infl}^{\prime }_\texttt{post}} \) such that
-
(i)
\({\textsf {well} _{{\texttt{post}}}} \,\llparenthesis {\texttt{s} '\ \texttt{with}\ {\texttt{c}}:= \texttt{s} '\!.\!{\texttt{c}} -\left\{ \texttt{x} \right\} }\rrparenthesis \,({\texttt{c}} _{{\texttt{post}}} -\left\{ \texttt{x} \right\} )\,{\texttt{post}} '\,{\texttt{infl}^{\prime }_\texttt{post}} \), and
-
(ii)
\({\textsf {update} _{{\texttt{post}}}} \,\texttt{x} \ \,\llparenthesis {\texttt{s}\ \texttt{with}\ {\texttt{c}} {:=\,} \texttt{s}.\!{\texttt{c}} -\left\{ \texttt{x} \right\} }\rrparenthesis \, \,\llparenthesis {\texttt{s} '\ \texttt{with}\ {\texttt{c}} {:=\,} \texttt{s} '\!.\!{\texttt{c}} -\left\{ \texttt{x} \right\} }\rrparenthesis \,\, ({\texttt{c}} _{{\texttt{post}}} \cup \left\{ \texttt{x} \right\} )\,{\texttt{post}} \,{\mathtt {infl_{post}}} \,\,{\texttt{post}} '\,{\texttt{infl}^{\prime }_\texttt{post}} \) hold.
-
(i)
-
Assume \(\mathtt {eval_{\boxslash }} \,\texttt{x} \,\texttt{t} \,\texttt{s} \) terminates and returns \(( \texttt{d} _{\texttt{x} },\texttt{s} ' )\) as result and \({\textsf {well} } \texttt{s} \), and \({\textsf {well} _{{\texttt{post}}}} \,\texttt{s} \,{\texttt{c}} _{{\texttt{post}}} \,{\texttt{post}} \,{\mathtt {infl_{post}}} \) hold for some post data structures \({\texttt{c}} _{{\texttt{post}}}\), \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\). Also, assume that \(\texttt{x} \in \texttt{s}.\!{\texttt{c}} \) and that there exists a list \(\texttt{pre} \) for which \(\texttt{subt}\ ({\mathcal {T}} ~ \texttt{x} )\ \texttt{s}.\!{\sigma }\ \texttt{pre} = \texttt{Some} \,\texttt{t} \) and \(\texttt{set}\ \texttt{pre} \subseteq \texttt{s}.\!{\texttt{stable}} \). Then there exist post data structures \({\texttt{post}} '\) and \({\texttt{infl}^{\prime }_\texttt{post}} \) such that
-
(i)
\({\textsf {well} _{{\texttt{post}}}} \,\texttt{s} '\,{\texttt{c}} _{{\texttt{post}}} \,{\texttt{post}} '\,{\texttt{infl}^{\prime }_\texttt{post}} \), and
-
(ii)
\({\textsf {update} _{{\texttt{post}}}} \,\texttt{x} \,\texttt{s} \,\texttt{s} '\,{\texttt{c}} _{{\texttt{post}}} \,{\texttt{post}} \,{\mathtt {infl_{post}}} \,\,{\texttt{post}} '\,{\texttt{infl}^{\prime }_\texttt{post}} \) hold.
-
(i)
An essential step in the proof is to show that the removal mechanism for \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\) only up to the barrier is extensive enough such that Definition 10 (v) and (vi) hold again after updating the value of the iterated unknown. For that, we argue that transitive influences recorded in \({\mathtt {infl_{post}}}\) that cross the barrier must be outdated.
Proving equivalence with the strengthened well-formedness invariants.
Based on \({\textsf {well} _{{\texttt{post}}}} \) and the existence of consistently updated post data structures fulfilling \({\textsf {update} _{{\texttt{post}}}} \), we prove the equivalence of the mutual recursive functions of \(\hbox {TD}_{\boxslash }\) and \(\hbox {TD}_{\text {w/n}}\) by induction on the computation traces:
Lemma 7
(Equivalence of Recursive Functions of \(\hbox {TD}_{\boxslash }\) and \(\hbox {TD}_{\text {w/n}}\)) Assume that the widening operator \(\nabla \) is precise and that the equation system has monotonic right-hand sides with monotonic dependencies. Let \(\texttt{s} \) be a solver state. Then the following holds.
-
Assume \({\textsf {well} } \texttt{s} \), and \({\textsf {well} _{{\texttt{post}}}} \,\texttt{s} \,{\texttt{c}} _{{\texttt{post}}} \,{\texttt{post}} \,{\mathtt {infl_{post}}} \) hold for some post data structures \({\texttt{c}} _{{\texttt{post}}}\), \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\). Further, assume that \(\texttt{x} \in {\texttt{dep}}\ \texttt{s}.\!{\sigma }\ \texttt{y} \). Then \(\mathtt {query_{\boxslash }} \,\texttt{y} \,\texttt{x} \,\texttt{s} \) terminates iff \(\mathtt {query_{w/n}} \,\texttt{y} \,\texttt{x} \,\texttt{s} \) terminates, and both calls return the same result.
-
Assume \({\textsf {well} } \,\llparenthesis {\texttt{s}\ \texttt{with}\ {\texttt{c}}:= \texttt{s}.\!{\texttt{c}} -\left\{ \texttt{x} \right\} }\rrparenthesis \), and \({\textsf {well} _{{\texttt{post}}}} \,\llparenthesis {\texttt{s}\ \texttt{with}\ {\texttt{c}}:= \texttt{s}.\!{\texttt{c}} -\left\{ \texttt{x} \right\} }\rrparenthesis \,({\texttt{c}} _{{\texttt{post}}} -\left\{ \texttt{x} \right\} )\,{\texttt{post}} \,{\mathtt {infl_{post}}} \) hold for some post data structures \({\texttt{c}} _{{\texttt{post}}}\), \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\). Further, assume that \(x \in \texttt{s}.\!{\texttt{c}} \), \((\texttt{x} \notin {\texttt{c}} _{{\texttt{post}}} \implies \texttt{x} \notin {\texttt{post}} -\, \texttt{s}.\!{\texttt{stable}}) \wedge (\texttt{x} \in {\texttt{c}} _{{\texttt{post}}} \implies \texttt{x} \in {\texttt{post}})\) and \(\texttt{wn} = N \implies \texttt{x} \in {\texttt{c}} _{{\texttt{post}}} \) for some phase parameter \(\texttt{wn}\). Then \(\mathtt {iterate_{\boxslash }} \,\texttt{x} \,\texttt{s} \) terminates iff \(\mathtt {iterate_{w/n}} \,\texttt{x} \,\texttt{wn} \,\texttt{s} \) terminates, and both calls return the same result.
-
Assume \({\textsf {well} } \,\texttt{s} \), and \({\textsf {well} _{{\texttt{post}}}} \,\texttt{s} \,{\texttt{c}} _{{\texttt{post}}} \,{\texttt{post}} \,{\mathtt {infl_{post}}} \) hold for some post data structures \({\texttt{c}} _{{\texttt{post}}}\), \({\texttt{post}}\) and \({\mathtt {infl_{post}}}\). Also, assume that \(\texttt{x} \in \texttt{s}.\!{\texttt{c}} \) and that there is some prefix \(\texttt{pre}\) such that \(\texttt{subt}\ ({\mathcal {T}} \, \texttt{x} )\ \texttt{s}.\!{\sigma }\ \texttt{pre} = \texttt{Some} \,\texttt{t} \) and \(\texttt{set}\ \texttt{pre} \subseteq \texttt{s}.\!{\texttt{stable}} \). Then \(\mathtt {eval_{\boxslash }} \,\texttt{x} \,\texttt{t} \,\texttt{s} \) terminates iff \(\mathtt {eval_{w/n}} \,\texttt{x} \,\texttt{t} \,\texttt{s} \) terminates, and both calls return the same result.
The extra assumption that widening is precise implies that when \(\hbox {TD}_{\text {w/n}}\) re-iterates an unknown already truly post in phase \(\texttt{W}\), widening has no effect and phase \(\texttt{N}\) is started immediately. As a consequence, we obtain equivalence of the solvers \(\hbox {TD}_{\boxslash }\) and \(\hbox {TD}_{\text {w/n}}\):
Theorem 3
(Equivalence of \(\hbox {TD}_{\text {w/n}}\) and \(\hbox {TD}_{\boxslash }\)) Assume that the widening operator is precise, and the equation system has monotonic right-hand sides with monotonic dependencies. Then \(\mathtt {solve_{\boxslash }}\) \(\texttt{x}\) terminates iff \(\mathtt {solve_{w/n}\ x}\) terminates, and both return identical results.
Theorem 3 allows us to transfer the results of the partial correctness proof for \(\hbox {TD}_{\boxslash }\) to \(\hbox {TD}_{\text {w/n}}\) and the results of the termination proof for \(\hbox {TD}_{\text {w/n}}\) to \(\hbox {TD}_{\boxslash }\) to obtain total correctness of both.
Corollary 1
(Total Correctness) With a precise widening and equation systems with monotonic right-hand sides and monotonic dependencies,
-
1.
\(\mathtt {solve_{\boxslash }}\) \(\texttt{x}\) always terminates for a finite set of unknowns; and
-
2.
\(\mathtt {solve_{w/n}\ x}\) computes a partial post-solution for the returned set of unknowns \({\texttt{stable}}\) where \(\texttt{x} \in {\texttt{stable}} \).
7 Related Work
Machine-checked proofs of soundness and termination have been provided for various data-flow analyzers with round-robin [25] or worklist iteration [26,27,28]. These data-flow analyzers implement neither widening nor narrowing. Instead, the termination proofs are based on the assumption that the value lattice has no infinite ascending chains.
De Vilhena et al. [9] formalize a generic, worklist based fixpoint solver that dynamically tracks the dependencies between unknowns, but applies no widening or narrowing. They provide machine-checked proofs for the solver’s partial correctness, apart from proofs about safety for its concurrent use and proofs about the optimality of the result when used repeatedly. The most intricate solver, perhaps, considered so far, is the local generic fixpoint solver RLD [29] which tracks dynamic dependencies between unknowns and uses the call-stack to implicitly realize a worklist. The TD is more intricate than RLD as it relies on non-local destabilization for updating the set of stable unknowns for which evaluation can be replaced with a look-up. A formal proof of partial correctness was only provided recently by Stade et al. [13, 14]. Extensions with widening and narrowing have, as far as we know, only been considered for round-robin iteration [30, 31].
Instead of verifying generic solvers for arbitrary equation systems, one may verify abstract interpreters where the iteration is over the syntax of the programming language. Cachera and Pichardie [32] develop abstract interpreters of a While language using widening/narrowing and formally verify claims regarding termination and soundness in Coq. A particularly compact formalization without narrowing in \(F^*\) is provided by Franceschino et al. [33]. As part of their didactic work, Nipkow et al. [34, 35] also formalize an abstract interpreter of a While language and prove its total correctness in Isabelle/HOL. Their analyzer consists of one global widening phase, followed by one global narrowing phase—which simplifies the termination proof considerably. The syntax-directed approach is also followed by Jourdan et al. [36, 37]. They design and verify Verasco, an abstract interpreter targeted at the CompCert subset of ISO C99. Termination of the analyzer is ensured by limiting the number of iterations. From a software engineering perspective it is beneficial to separate the algorithmic aspects of static analysis, i. e. the fixpoint engine, from the specification of the analysis itself. The separation of concerns is also convenient for the verification. Given a verified solver, it only remains to prove that the individual computation steps are correctly abstracted—which can be a complicated task in itself. The drawback of a generic solver is, that the dependencies are not directly accessible. The dynamic detection of dependencies and widening/narrowing points with which \(\hbox {TD}_{\boxslash }\) and \(\hbox {TD}_{\text {w/n}}\) are equipped, require no preprocessing and also work for equation systems with infinitely many unknowns. Alternatively to the verification of generic solvers or abstract interpreters, a verified validator can validate previously computed program invariants [38]. The overall analysis then returns provably correct results—without any guarantee, though, that it ever returns.
Previous work adapts the solver TD to domains with infinite ascending and/or descending chains. We build on and extend this work by formal verification. Warrowing has been introduced as an operator for intertwining widening and narrowing in solvers [8, 17]. Apinis et al. [18] show that the vanilla TD can also neatly be equipped with warrowing. They provide a pen-and-paper proof that, in case of finitely many encountered unknowns and monotonicity of right-hand sides, the solver terminates. It builds on the claim, however, that values only decrease in narrowing iterations, which does not necessarily hold in case of non-monotonic dependencies. Building on the work of Schulze Frielinghaus et al. [40], Seidl and Vogler [11] present a variant of the TD with phases and provide informal arguments that it will always terminate whenever the set of encountered unknowns is finite. Removal of widening/narrowing points has been added to this solver only in [21] without further proof arguments. To our knowledge we are the first to consider the equivalence of this solver with \(\hbox {TD}_{\boxslash }\).
8 Conclusion
We have considered two extensions of the top-down solver TD with widening and narrowing. We formally verified that the extension \(\hbox {TD}_{\boxslash }\) is guaranteed to return a partial post-solution—whenever it terminates, while the extension \(\hbox {TD}_{\text {w/n}}\) terminates whenever the set of encountered unknowns is finite. We have exhibited three assumptions under which we prove the equivalence of \(\hbox {TD}_{\boxslash }\) and \(\hbox {TD}_{\text {w/n}}\)—thus providing us a total correctness proof for both solvers. While monotonicity is often provided by sound abstractions of the concrete semantics, it may be violated for equation systems derived from certain intricate abstractions. A natural question therefore arises which variant of TD to use. Our suggestion would be to use \(\hbox {TD}_{\boxslash }\) as it provides partial correctness out of the box. To enforce termination also for non-monotonic systems, warrowing gas may be introduced which limits the number of switches from widening to narrowing inside the warrowing operator. Then monotonicity just guarantees that warrowing gas 1 would be sufficient. \(\hbox {TD}_{\text {w/n}}\) could also be applied in presence of non-monotonicity: the correctness argument, however, would then have to rely on properties of the abstraction. As the returned value mappings need not be partial post-solutions themselves, correctness can no longer be certified a posteriori by running a fixpoint checker. As future work, we would like to identify properties of these solvers that capture their efficiency and/or precision behavior for dedicated classes of equation systems.
Data Availability
The proofs of this work are available at: https://doi.org/10.5281/zenodo.15240888
References
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ analyzer. In: Sagiv, M. (ed.) Programming Languages and Systems, pp. 21–30. Springer, Berlin, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31987-0_3
Hermenegildo, M.V., Bueno, F., Carro, M., López-García, P., Haemmerlé, R., Mera, E., Morales, J.F., Puebla, G.: An overview of the Ciao system. In: Bassiliades, N., Governatori, G., Paschke, A. (eds.) Rule-Based Reasoning, Programming, and Applications, pp. 2–2. Springer, Berlin, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22546-8_2
Vojdani, V., Apinis, K., Rõtov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the Goblint approach. In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering. ASE ’16, pp. 391–402. Association for Computing Machinery, New York, NY, USA (2016). https://doi.org/10.1145/2970276.2970337
Monat, R., Ouadjaout, A., Miné, A.: Mopsa-C: Modular domains and relational abstract interpretation for C programs (competition contribution). Tools and Algorithms for the Construction and Analysis of Systems. (2023). https://doi.org/10.1007/978-3-031-30820-8_37
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. POPL ’77, pp. 238–252. Association for Computing Machinery, New York, NY, USA (1977). https://doi.org/10.1145/512950.512973
Hecht, M.S., Ullman, J.D.: Analysis of a simple algorithm for global data flow problems. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. POPL ’73, pp. 207–217. Association for Computing Machinery, New York, NY, USA (1973). https://doi.org/10.1145/512927.512946
Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. POPL ’73, pp. 194–206. Association for Computing Machinery, New York, NY, USA (1973). https://doi.org/10.1145/512927.512945
Apinis, K., Seidl, H., Vojdani, V.: How to combine widening and narrowing for non-monotonic systems of equations. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI ’13, pp. 377–386. Association for Computing Machinery, New York, NY, USA (2013). https://doi.org/10.1145/2491956.2462190
Vilhena, P.E., Pottier, F., Jourdan, J.-H.: Spy game: verifying a local generic solver in Iris. In: Proc. ACM Program. Lang. 4(POPL), (2019). https://doi.org/10.1145/3371101
Charlier, L., Van Hentenryck, B., P.: A universal top-down fixpoint algorithm, University of Namur and Brown University (1992). (CS-92-25 Technical Report)
Seidl, H., Vogler, R.: Three improvements to the top-down solver. Math. Struct. Comput. Sci. 31(9), 1090–1134 (2021). https://doi.org/10.1017/S0960129521000499
Fecht, C., Seidl, H.: A faster solver for general systems of equations. Sci. Comput. Program. 35(2), 137–161 (1999). https://doi.org/10.1016/S0167-6423(99)00009-X
Stade, Y., Tilscher, S., Seidl, H.: The top-down solver verified: Building confidence in static analyzers. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification, pp. 303–324. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-65627-9_15
Stade, Y., Tilscher, S., Seidl, H.: Partial correctness of the top-down solver. Archive of Formal Proofs (2024). https://isa-afp.org/entries/Top_Down_Solver.html Formal proof development
Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput. 2(4), 511–547 (1992). https://doi.org/10.1093/LOGCOM/2.4.511
Cousot, P.: Abstracting induction by extrapolation and interpolation. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 19–42. Springer, Berlin, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46081-8_2
Amato, G., Scozzari, F., Seidl, H., Apinis, K., Vojdani, V.: Efficiently intertwining widening and narrowing. Sci. Comput. Program. 120, 1–24 (2016). https://doi.org/10.1016/j.scico.2015.12.005
Apinis, K., Seidl, H., Vojdani, V.: Enhancing Top-Down Solving with Widening and Narrowing. Semantics, Logics, and Calculi. (2016). https://doi.org/10.1007/978-3-319-27810-0_14
Tilscher, S., Graß, A., Seidl, H., Stade, Y.: Correctness proofs for top-down solvers with widening and narrowing in Isabelle. Zenodo (2026). https://doi.org/10.5281/zenodo.15240888
Hofmann, M., Karbyshev, A., Seidl, H.: What is a pure functional? In: Abramsky, S., Gavoille, C., Kirchner, C., Heide, F., Spirakis, P.G. (eds.) Automata, Languages and Programming, pp. 199–210. Springer, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14162-1_17
Tilscher, S., Stade, Y., Schwarz, M., Vogler, R., Seidl, H.: The top-down solver—an exercise in A2I. In: Arceri, V., Cortesi, A., Ferrara, P., Olliaro, M. (eds.) Challenges of Software Verification vol. 238, pp. 157–179. Springer, Singapore (2023). https://doi.org/10.1007/978-981-19-9601-6_9
Halbwachs, N., Henry, J.: When the decreasing sequence fails. In: Miné, A., Schmidt, D. (eds.) Static Analysis, pp. 198–213. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33125-1_15
Nipkow, T., Klein, G.: Programming and Proving. In: Concrete Semantics. pp. 5–25. Springer (2014). https://doi.org/10.1007/978-3-319-10542-0_2
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. POPL ’78, pp. 84–96. Association for Computing Machinery, New York, NY, USA (1978). https://doi.org/10.1145/512760.512770
Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. In: Schmidt, D. (ed.) Programming Languages and Systems, pp. 385–400. Springer, Berlin, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24725-8_27
Nipkow, T.: Verified bytecode verifiers. In: Honsell, F., Miculan, M. (eds.) Foundations of Software Science and Computation Structures, pp. 347–363. Springer, Berlin, Heidelberg (2001). https://doi.org/10.1007/3-540-45315-6_23
Coupet-Grimal, S., Delobel, W.: A uniform and certified approach for two static analyses. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) Types for Proofs and Programs, pp. 115–137. Springer, Berlin, Heidelberg (2006). https://doi.org/10.1007/11617990_8
Bertot, Y., Grégoire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) Types for Proofs and Programs, pp. 66–81. Springer, Berlin, Heidelberg (2006). https://doi.org/10.1007/11617990_5
Hofmann, M., Karbyshev, A., Seidl, H.: Verifying a local generic solver in Coq. In: Cousot, R., Martel, M. (eds.) Static Analysis, pp. 340–355. Springer, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15769-1_21
Pichardie, D.: Interprétation abstraite en logique intuitionniste : extraction d’analyseurs Java certifiés. Thèse de doctorat, Universite de Rennes 1-Rennes I (2005). http://www.theses.fr/2005REN1S183
Besson, F., Cachera, D., Jensen, T., Pichardie, D.: Certified Static Analysis by Abstract Interpretation. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) Foundations of Security Analysis and Design, pp. 223–257. Springer, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03829-7_8
Cachera, D., Pichardie, D.: A certified denotational abstract interpreter. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, pp. 9–24. Springer, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_3
Franceschino, L., Pichardie, D., Talpin, J.-P.: Verified functional programming of an abstract interpreter. In: Drăgoi, C., Mukherjee, S., Namjoshi, K. (eds.) Static Analysis, pp. 124–143. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-88806-0_6
Nipkow, T.: Abstract interpretation of annotated commands. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving, pp. 116–132. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_9
Nipkow, T., Klein, G.: Abstract Interpretation. In: Concrete Semantics. pp. 219–280. Springer (2014). https://doi.org/10.1007/978-3-319-10542-0_13
Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’15, pp. 247–259. Association for Computing Machinery, New York, NY, USA (2015). https://doi.org/10.1145/2676726.2676966
Jourdan, J.: Verasco: a formally verified C static analyzer. PhD thesis, Paris Diderot University, France (2016). https://tel.archives-ouvertes.fr/tel-01327023
Blazy, S., Laporte, V., Maroneze, A., Pichardie, D.: Formal verification of a C value analysis based on abstract interpretation. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis, pp. 324–344. Springer, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38856-9_18
Bertot, Y.: In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) Structural Abstract Interpretation: A Formal Study Using Coq, pp. 153–194. Springer, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03153-3_4
Schulze Frielinghaus, S., Seidl, H., Vogler, R.: Enforcing termination of interprocedural analysis. In: Rival, X. (ed.) Static Analysis, pp. 447–468. Springer, Berlin, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_22
Acknowledgements
This work was supported in part by the German Research Foundation (DFG) - 378803395/2428 ConVeY.
Funding
Open Access funding enabled and organized by Projekt DEAL.
Author information
Authors and Affiliations
Contributions
All authors were involved in the conceptualization and contributed to writing and editing the manuscript. The formal proofs were written by S.T. (termination of the two-phase solver and the proof of equivalence of both solvers) and A.G. (partial correctness of the warrowing solver). S.T. provided the examples illustrating the necessity of the given assumptions for the equivalence of both solvers.
Corresponding author
Ethics declarations
Competing interests
The authors declare no competing interests.
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Appendices
Appendix A: TD with Widening/Narrowing Phases
Figure 2 shows only the \({\mathtt {iterate_{w/n}}}\) function, as it implements the most significant differences of \(\hbox {TD}_{\text {w/n}}\) compared to \(\hbox {TD}_{\boxslash }\). The other functions of \(\hbox {TD}_{\text {w/n}}\) differ only little from those of \(\hbox {TD}_{\boxslash }\). Figure 5 shows all function definitions of \(\hbox {TD}_{\text {w/n}}\) and highlights the differences from \(\hbox {TD}_{\boxslash }\).
Appendix B: Spurious Dependencies in \({\mathtt {infl_{post}}}\)
We construct an example where some entries in \({\mathtt {infl_{post}}}\) reflect outdated dependencies. It suffices to consider a set of unknowns \(\mathcal {U} = \left\{ x,y,z \right\} \) and the domain \(\mathbb D = \left\{ 0,1,2,3,4 \right\} \) with order \(<_\mathbb {N}\) and the widening and narrowing operators as defined in Example 2. Figure 6 shows an equation system together with the computation trace of \(\hbox {TD}_{\boxslash }\) for x.
During the third iteration on unknown \(\texttt{y}\) ( ), unknowns \(\texttt{y}\), \(\texttt{z}\) and \(\texttt{x}\) are queried while evaluating \({\texttt{y}}\) ’s right-hand side. As \(\texttt{y}\) is iterated with narrowing, collected influences, in particular \({\texttt{z}}\) \(\rightarrow \) y, remain in \({\mathtt {infl_{post}}}\), but are removed from \({\texttt{infl}}\) through destabilization. In the subsequent narrowing iteration of \(\texttt{y}\) ( ) fewer dependencies are encountered. Thus, \(\texttt{z}\) \(\rightarrow \) \(\texttt{y}\) earlier left in \({\mathtt {infl_{post}}}\) becomes outdated and is now a spurious dependency. Further up the call-stack, \(\texttt{x}\) is destabilized because its value changes ( ). Pruning \({\mathtt {infl_{post}}}\) and \({\texttt{post}}\) only up to the barrier of unknowns still stable after destabilization, avoids removing \(\texttt{y}\) from \({\texttt{post}}\) only based on the outdated dependency \(\texttt{z}\) \(\rightarrow \) \(\texttt{y}\) and although it is stable.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/
About this article
Cite this article
Tilscher, S., Graß, A., Seidl, H. et al. Proving Total Correctness of Top-Down Solvers with Widening and Narrowing. J Autom Reasoning 70, 15 (2026). https://doi.org/10.1007/s10817-026-09756-x
Received:
Accepted:
Published:
Version of record:
DOI: https://doi.org/10.1007/s10817-026-09756-x