In subsection 6.3.2, we saw that solutions of Constraint System 6.5 w.r.t. S∞ enjoy the same correctness and precision results as the functional approaches. Unfortunately, Constraint System 6.5 is not *e*ff*ective*. For one, Constraint System 6.5 w.r.t. S∞ is infinite. Secondly, the complete lattice that forms the solution space of Constraint System 6.5 is

$$N \times N \times S^{\infty} \to F\_{\mathbb{E}\_{\Delta'}}$$

which does not satisfy the ascending chain condition. Particularly this second fact makes it impossible to use algorithms such as Algorithm 8, which rely on the ascending chain condition for termination.

However, in Example 6.13 I showed the family of (S*k* )*k*∈**N** of stack spaces that lead to finite versions of Constraint System 6.5 and to solution spaces that satisfy the ascending chain condition. Hence algorithms like Algorithm 8 are applicable to Constraint System 6.5 w.r.t. S*k* . The idea of S*k* , which is at least since the work of Sharir and Pnueli [154] well-known in the literature, is to only consider the *k* topmost stack elements, so that all stacks are *k*-bounded. As Example 6.30 showed, S∞ and S*k* are connected via a stack abstraction, where the abstraction function projects a stack to the *k* topmost items.

Consequently, the main result Theorem 6.31 from the last subsection enables me to transfer the correctness result for S∞ to S*k* .

**Corollary 6.33.** *1. Let* S *be a stack space such that there is a stack abstraction between* S∞ *and* S*. Then the following statements hold:*

$$\text{(6.23)}\qquad\qquad\forall \text{s}, t \in \text{N}. \text{ } VP(\text{s}, t) \subseteq AP\_{\mathcal{S}}(\text{s}, t)$$

$$(6.24)\qquad\forall s, t\_\prime \in \mathcal{N}.\ \text{MO} \\ VP(s, t) \le \text{MO} \\ AP(s, t)$$

*2. Let k*, *l* ∈ **N** ∪ {∞} *with l* ≤ *k. Then the following statements hold:*

$$\text{(6.25)}\tag{6.25} \qquad \qquad \qquad \text{MOVP} \leq \text{MOAP}\_{\mathcal{S}\_{kl}}$$

$$\text{(6.26)}\tag{6.26} \\ \text{W} \text{O} \\ \text{OP}\_{\text{S}\_k} \leq \text{MO} \\ \text{AP}\_{\text{S}\_l}$$

*Proof.* 1. (6.23) follows from Theorem 6.31 and Theorem 6.25. The second statement (6.24) is an easy consequence of (6.23).

2. In Example 6.30 we have seen that (S*k* , α*k*,*l* , γ*k*,*l* , S*l* ) is a stack abstraction if *k*, *l* ∈ **N** ∪ {∞} with *l* ≤ *k*. This means that we can apply (6.23) and (6.24) to obtain the desired statements. □

Together with Theorem 7.34, this entails that solutions of Constraint System 6.5 w.r.t. S*k* are *VP*-correct. Hence, using *k*-bounded stacks in the call-strings approach is indeed correct. This is a generalization of the corresponding result that was obtained by Sharir and Pnueli for classical data-flow analyses on interprocedural control-flow graph [154, Theorem 7- 6.5]. For one, my assumptions about the given graph and its valid paths are weaker (as I already explained in chapter 5). Moreover, there may be other stack spaces than S*k* that can be obtained from S∞ via a stack abstraction and lead to an effective version of Constraint System 6.5. The theory that I developed in this section provides a way to prove *VP*-correctness for all these stack spaces.

*I have su*ff*ered for this book; now it's your turn.* George Harrison **7**

# **A Common Generalization of Interprocedural Data-Flow Analysis and Slicing**

After chapter 6 introduced constraint systems for the functional and the callstring approach to interprocedural data-flow analysis for interprocedural graphs, this chapter is concerned with the effective solution of meaningful portions of these constraint systems in order to compute correct and possibly precise approximations to MO*VP*.

In chapter 3, I compared slicers such as Algorithm 5 and Algorithm 6 with algorithms to solve data-flow problems, such as Algorithm 3. My conclusion was that although both algorithm groups are worklist-based, they differ in what I coined as *worklist policy*. While the slicers usually assume that worklist items just have been updated, update the values of their successors and put them on the worklist if their value has changed, Algorithm 3 acts on the assumption that worklist items have to be updated, updates them using all their predecessors and then puts all successors on the worklist. This difference becomes obvious if one considers how the two approaches handle reachability. While slicers are reachability analyses and naturally explore graphs iteratively using a reachability frontier, Algorithm 3 is geared towards situations where the goal is to compute values for every variable and the usual assumption is that every variable is reachable. Hence, Algorithm 3 proceeds rather clumsily if the analysis information to be computed is reachability itself: It uses the rule "this variable is reachable if one of its predecessors is reachable" and not – like it is natural – "if this variable is reachable, then all its successors are reachable". It *is possible* to use Algorithm 3 for data-flow problems where reachability is part of the analysis result, even without modifications. However, this necessitates modifications of the data-flow problems. Moreover, the initial loop, which iterates through *all* variables cannot be eliminated – its task is to assess that all unreachable variables are indeed unreachable because all their predecessors are. I take a different path to integrate reachability and data-flow analysis and modify Algorithm 3 in such a way that it is geared towards reachability and computes the actual analysis result for reachable variables as a side-product. Particularly, Algorithm 8, my modified version of Algorithm 3, does not need to visit every variable at least once but only the reachable variables.

The presentation and analysis of Algorithm 8 will be the subject of section 7.1.

Moreover, section 7.1 considers reachability and partial solution on the level of constraint systems. This is particularly necessary to be able to make statements about the properties of Algorithm 8. Moreover, I investigate under which circumstances the least solution of the restricted constraint system coincides with the least solution of the full constraint system on the reachable variables. This can also be seen as *slicing of constraint systems*. It turns out that the modified version of Algorithm 3 is indeed capable of computing such partial solutions.

Subsequently, I apply the theory developed in section 7.1 to the constraint systems given in chapter 6 in order to obtain algorithms that compute correct data-flow solutions on forward slices. Section 7.2 lays out the setup and gives an overview of the general scheme. Then, section 7.3 and section 7.4 consider the functional approach and the call-string approach, respectively.

# **7.1 Integrating Reachability Into the Solution Process**

As was already mentioned at the very beginning of this chapter, the goal of this section is to present Algorithm 8, a variant of Algorithm 3 that additionally takes a set *X*0 of initial variables and solves only the part of the given constraint system that is *reachable* from this initial set of variables. This set cannot be chosen arbitrarily: The properties that *X*0 has to satisfy in order for Algorithm 8 are one of the topics of this section. How *X*0 is chosen concretely is dependent on the context and will be discussed in later sections of this chapter.

In the following, I consider a complete lattice *L* that satisfies the ascending chain condition. The idea behind Algorithm 8 is that it starts with applying the defining constraints of *X*0 and then proceeds by applying all constraints that use variables from *X*0. Then it considers the variables whose values have changed in the same way and continues this procedure until no more value is changed. In the end, Algorithm 8 has computed a partial solution of the given constraint system and explored the variables and constraints that are reachable from *X*0 using a chain of def-use relations.

To make this idea work, I need a way to distinguish variables that have been explored and whose solution value may be ⊥*L* from those which have not yet been explored and never will be34. For this purpose, I introduce a fresh value ⊠ that represents undefinedness and extend *L* to *L*⊠. Moreover, I also extend the interpretation so that it can also take ⊠ as input and assume that the extended interpretation has the properties (7.1) and (7.2). Remember from chapter 2 that *FV*(*t*) denotes the set of variables occurring in *t*.

(7.1) ∀*x* ∈ *L*. ⊠ ≤ *x*

$$\begin{aligned} \text{(7.2)}\\ \qquad \qquad \forall \mathfrak{x} \geq t \in \mathcal{C}. \,\forall \psi: X \to L\_{\mathfrak{B}}. \qquad \qquad \qquad \|t\|(\psi) = \mathfrak{B} \\ \qquad \qquad \qquad \Longleftrightarrow \exists \mathfrak{x}' \in FV(t). \,\psi(\mathfrak{x}') = \mathfrak{B}. \end{aligned}$$

These two properties ensure that reachable variables which are set to the ordinary ⊥ element of *L* can be distinguished from those variables which have not been reached yet or will never be reached. Particularly, the second property ensures that reachability is maintained.

Also, the extension of *L* to *L*⊠ is always possible without destroying important properties of *L*. *L*⊠ is still complete lattice that satisfies the ascending chain condition.

Note that in general (7.2) restricts the possible interpretations, since (7.2) essentially enforces that a constraint can be omitted if not all variables on its right-hand side have defining constraints.

34Note that the unreachable variables do not actually exist in the memory of a machine executing Algorithm 8. In practice, the reachability of a variable can be assessed by evaluating whether Algorithm 8 already has assigned a value to this variable. Nevertheless, I need this additional element ⊠ to reason theoretically about unreachable variables.

However, the semantics functional ⟦·⟧ : *Expr*(F ⊠ , *X*) → *F*⊠ that corresponds to a data-flow framework instance F = (*G*, *L*, *F*, ρ) and that I specified in section 6.1 satisfies both (7.1) and (7.2): (7.1) follows from (5.12) and (5.13), while (7.2) can be shown by induction with the help of (5.16) and (5.15).

 For motivation, I give an example. Consider the constraint system C that consists of the constraints

$$\begin{aligned} c\_1 &: v\_1 \ge f(v\_2, v\_3) \\ c\_2 &: v\_2 \ge g(v\_3) \\ c\_3 &: v\_3 \ge a \\ c\_4 &: v\_4 \ge h(v\_3, v\_5) \\ c\_5 &: v\_4 \ge b \end{aligned}$$

where *f*, *g*, *h*, *a*, *b* are function symbols with appropriate interpretations and the *vi* are variables.

If we start with *v*3 and follow the def-use chains in C, we see that *c*1 , *c*2, *c*3 and *c*4 are the constraints from C that are reachable from *v*3. Moreover, the reachable variables are *v*1 , *v*2 and *v*3.

Also note that *c*4 is not really useful as it uses the variable *v*5, which does not have any defining constraints in C. Hence, no solution of C needs to assign *v*5 any defined value. Particularly, the least solution *l f p*(*F*C) must map *v*4 to ⊠, which implies that *l f p*(*F*C)(*v*4 ) = *l f p*(*F*C\{*c*4 } )(*v*4 ). Similarly, we can conclude that it is not really useful to start with variables that have defining constraints with non-constant right-hand side, if one wants to preserve the least solution for the reachable variables. For example, if we start with *v*2, then we get the reachable constraints *c*1 and *c*2, but both use *v*3, which is defined by neither *c*1 nor *c*2, so that *l f p*(*F*C)(*v*1 ) and *l f p*(*F*C)(*v*2) both become ⊠ if we restrict C to {*c*1 , *c*2}.

Given a variable set *X*0 ⊆ *X*, the following definition introduces the sets Core(C, *X*0) and CoreVars(C, *X*0). The former captures the set of constraints that are obtained by starting at *X*0 and following the defuse chains in C, while the latter characterizes the variables defined by constraints from Core(C, *X*0).

Remember from chapter 2 that *Vars*(C) is the set of variables that occur on the left-hand sides of constraints in C and that *De f*(*x*) is the set of constraints for which *x* occurs on the left-hand side, respectively.

**Definition 7.1** (core and core variables of a constraint system)**.** *Let* C *be a constraint system and X*0 ⊆ *X be a set of variables.*

*1.* Core(C, *X*0)*, the* core *of* C *with respect to X*0*, is defined as the least subset* C0 ⊆ C *with the following closure properties:*

(C-Base) ∀*x*≥*t* ∈ C. *FV*(*t*) = ∅ ∧ *x* ∈ *X*0 =⇒ *x* ≥ *t* ∈ C0 (C-Step) ∀*x*≥*t* ∈ C. *FV*(*t*) ≠ ∅ ∧∀*x* ′ ∈ *FV*(*t*). *De f*(*x* ′ ) ∩ C0 ≠ ∅ =⇒ *x*≥*t* ∈ C0

*2.* CoreVars(C, *X*0)*, the* core variables *of* C*, is defined as the least subset Xc* ⊆ *Vars*(C) *that has the following closure properties:*

The following two lemmas shed some light on the properties of Core and CoreVars and will be of great use later.

### **Lemma 7.2.**

*Vars*(Core(C, *X*0)) = CoreVars(C, *X*0)

*Proof.* ⊇: Show that *Vars*(Core(C, *X*0)) has the closure properties of CoreVars(C, *X*0):

1. Let *x*≥*t* ∈ C with *FV*(*t*) = ∅ and *x* ∈ *X*0. Then *x*≥*t* ∈ Core(C, *X*0), i.e. *x* ∈ *Vars*(Core(C, *X*0)).

2. Let *x*≥*t* ∈ C with *FV*(*t*) ≠ ∅ and *FV*(*t*) ⊆ *Vars*(Core(C, *X*0)). Then for every *x* ′ ∈ *FV*(*t*), *De f*(*x* ′ ) ∩ Core(C, *X*0) ≠ ∅. Hence, *x*≥*t* ∈ Core(C, *X*0), which means that *x* ∈ *Vars*(Core(C, *X*0)).

⊆: Define

$$\mathcal{C}\_0 \stackrel{def}{=} \{ \mathfrak{x} \succeq t \in \mathcal{C} \mid \mathfrak{x} \in \mathsf{CoreVars}(\mathcal{C}\_\prime X\_0) \}$$

Then

$$(\star) \qquad \qquad Var(\mathcal{C}\_0) = \text{CoreVars}(\mathcal{C}\_\prime X\_0) . \tag{4}$$

This can be seen as follows:

Next we show that Core(C, *X*0) ⊆ C0. From this, it follows that

$$\operatorname{Vars}(\operatorname{Core}(\mathcal{C}\_{\prime}X\_{0})) \subseteq \operatorname{Vars}(\mathcal{C}\_{0}) = \operatorname{CoreVars}(\mathcal{C}\_{\prime}X\_{0}).$$

To prove Core(C, *X*0) ⊆ C0, we show that C0 has the closure properties (C-Base) and (C-Step).

1. If *x*≥*t* ∈ C, *FV*(*t*) = ∅ and *x* ∈ *X*0, we have *x* ∈ CoreVars(C, *X*0) by (V-Base), hence *x*≥*t* ∈ C0 by definition.

2. Let *x*≥*t* ∈ C with *FV*(*t*) ≠ ∅ and

$$\forall \mathfrak{x'} \in FV(t). \, Def(\mathfrak{x'}) \cap \mathcal{C}\_0 \neq \emptyset.$$

Then

$$FV(t) \subseteq Vars(\mathcal{C}\_0) \stackrel{(\star)}{=} \mathcal{C} \text{coreVars}(\mathcal{C}\_\prime X\_0) . .$$

Hence, *x* ∈ CoreVars(C, *X*0) by property (V-Step), which means that *x*≥*t* ∈ C0 by definition of C0.

□

**Lemma 7.3.** *Let* C *be a constraint system and X*0 ⊆ *X be a set of variables. Then the following statements are equivalent:*

(1) *x*≥*t* ∈ Core(C, *X*0)

$$(\mathcal{Q}) \quad (FV(t) = \emptyset \land \mathbf{x} \in \mathcal{X}\_0) \lor (FV(t) \neq \emptyset \land FV(t) \subseteq \text{CoreVars}(\mathcal{C}, \mathcal{X}\_0)))$$

*Proof.* (1) =⇒ (2) Assume *x*≥*t* ∈ Core(C, *X*0). Then either *FV*(*t*) = ∅ and *x* ∈ *X*0 or *FV*(*t*) ≠ ∅ and ∀*x* ′ ∈ *FV*(*t*). *De f*(*x* ′ ) ∩ Core(C, *X*0) ≠ ∅. In the former case, (2) holds trivially. In the latter case, we conclude

$$\forall \mathbf{x'} \in FV(t). \; \mathbf{x'} \in Vars(\mathbf{Core}(\mathbf{C}, X\_0))\_{\mathbf{Y}}$$

which is, due to Lemma 7.2, equivalent to

$$\forall \mathbf{x'} \in FV(t). \,\,\mathfrak{x} \in \text{CoreVars}(\mathcal{C}\_{\prime}\mathbf{X}\_{0}).$$

(2) =⇒ (1) We prove the claim by case distinction.

1. Assume that

$$\alpha \in \mathcal{X}\_0 \land FV(t) = \emptyset.$$

Then *x*≥*t* ∈ Core(C, *X*0) by (C-Base).

2. Assume that

$$FV(t) \neq \emptyset \land FV(t) \subseteq \text{CoreVars}(\mathcal{C}\_{\prime}X\_{0})\dots$$

With the definition of *Vars* and Lemma 7.2, this implies

$$\forall \mathbf{x'} \in FV(t). \, Def(\mathbf{x'}) \cap \text{Core}(\mathcal{C}, \mathbf{X}\_0) \neq \emptyset.$$

Thus *x*≥*t* ∈ Core(C, *X*0) by (C-Step).

Core(C, *X*) only eliminates useless constraints. Therefore, the least solution of Core(C, *X*) must coincide with the least solution of C on the whole variable set.

**Lemma 7.4.** Core(C, *X*) *has the same least solution as* C*.*

*Proof.* First, we show that the two least solutions must coincide on *Vars*(Core(C, *X*)). It is clear that *l f p*(*F*Core(C,*X*) ) ≤ *l f p*(*F*C), since Core(C, *X*) ⊆ C. Next, we observe

$$(\text{7.3})\qquad \forall \mathbf{x} \in X \mid Var(\text{Core}(\mathbf{C}, X)). \newline 1. \newline f(F\_{\text{Core}(\mathbf{C}, X)})(\mathbf{x}) = \mathbf{z}. \newline \dots$$

□

The reason is that by definition, Core(C, *X*) has no defining constraints for variables outside of *Vars*(Core(C, *X*)). Finally, we show

$$(7.4)\tag{7.4}$$

$$\text{(7.4)}\tag{7.5}\text{(}\text{(F}\_{\text{C}}\text{)}\leq \text{lfp}(\text{F}\_{\text{C}\text{ore}(\text{C},X)})\text{)}$$

by fixed-point induction (cf. Corollary 2.7). Let

$$\mathcal{P} \stackrel{def}{=} \{ \psi : X \to L \mid \psi \le lfp(F\_{\text{Core}(\mathcal{C},X)}) \}.$$

It is easy to see that *const*(⊠) ∈ P and that P is closed under arbitrary joins. It remains to show that P is also closed under *F*C. For this, it suffices to show

$$\forall \psi \in \mathcal{P}. \,\forall \mathfrak{x} \ge t \in \mathcal{C}. \,\|\mathfrak{f}\|(\psi) \le lfp(F\_{\text{Core}(\mathcal{C},\mathcal{X})})(\mathfrak{x})$$

So let ψ ∈ P and *x*≥*t* ∈ C. We have to show that

$$(\text{7.5})\qquad \|t\| (\psi) \le \|t\| (lfp(F\_{\text{Core}(\mathcal{C},X)})) \le lfp(F\_{\text{Core}(\mathcal{C},X)}) (\text{x})\,.$$

This follows from the two properties

$$(7.6)\tag{7.6} \qquad \qquad \|t\| (\psi) \le \|t\| (lfp(F\_{\text{Core}(\mathcal{C}, \mathcal{X})})) $$

and

$$(\text{7.7})\qquad\qquad\|\mathbb{I}\|\|(\text{lfp}(\text{F}\_{\text{Core}(\text{C},\text{X})}))\leq\text{lfp}(\text{F}\_{\text{Core}(\text{C},\text{X})})(\text{x})\_{\text{M}}$$

which we are going to show in the following.

(7.6) By our assumption that ψ ∈ P, we have in particular

$$\forall \mathbf{x'} \in FV(t). \; \psi(\mathbf{x'}) \le lfp(F\_{\text{Core}(\mathcal{C}\_l X)})(\mathbf{x'}).\;$$

From this, (7.6) can be shown using Lemma 2.10.

(7.7) We distinguish two cases:

1. *x*≥*t* ∈ Core(C, *X*): Then (7.7) holds because *l f p*(*F*Core(C,*X*) ) is a solution of Core(C, *X*).

2. *x*≥*t* ∉ Core(C, *X*). Then it must be the case that

$$FV(t) \neq \emptyset \land \exists \mathbf{x'} \in FV(t) . \mathbf{x'} \in X \backslash Vars(\mathbf{Core}(\mathbf{C}, X)) . \prime$$

since otherwise the closure properties of Core(C, *X*) would immediately imply *x*≥*t* ∈ Core(C, *X*).

But then, due to (7.3), there must be one *x* ′ ∈ *FV*(*t*) with

$$\operatorname{lfp}(F\_{\text{Core}(\mathcal{C},\mathcal{X})})(\mathfrak{x}') = \mathfrak{a}.$$

Now, (7.7) follows with (7.2) and (7.1).

Now I want to consider how Core behaves for *X*0 ≠ *X*.

The following lemma shows that Core(C, *X*0) can be obtained by first computing Core(C, *X*) and then restricting the variables to *X*0. The first step eliminates all constraints that do not contribute anything, while the second step eliminates all constraints that may contribute to the solution but depend on variables not in *X*0.

**Lemma 7.5.** *Applying* Core(*\_*, *X*0)*to* C *is the same as applying it to* Core(C, *X*)*:*

$$\text{(7.8)}\qquad\text{Core}(\mathcal{C}, X\_0) = \text{Core}(\text{Core}(\mathcal{C}, X), X\_0).$$

*Proof.* First, we observe that Core(C, *X*) is a subset of C and Core is monotone in its first argument. This implies

$$\text{Core}(\mathcal{C}, X\_0) \supseteq \text{Core}(\text{Core}(\mathcal{C}, X), X\_0) \dots$$

It remains to show "⊆". For this, we show that Core(Core(C, *X*), *X*0) has the properties (C-Base) and (C-Step) with respect to C and *X*0.

1. Let *x*≥*t* ∈ C with *FV*(*t*) = ∅ and *x* ∈ *X*0. Then in particular *x* ∈ *X*. Hence, by applying (C-Base) to *x*≥*t* ∈ C and *x* ∈ *X*, we get

$$
\alpha \ge t \in \text{Core}(\mathcal{C}, X).
$$

Then we apply (C-Base) to *x* ∈ *X*0 and *x*≥*t* ∈ Core(C, *X*) and get our desired result

$$
\alpha \ge t \in \text{Core}(\text{Core}(\mathsf{C}, X), X\_0).
$$

2. Let *x*≥*t* ∈ C with *FV*(*t*) ≠ ∅ and

∀*x* ′ ∈ *FV*(*t*). *De f*(*x* ′ ) ∩ Core(Core(C, *X*), *X*0) ≠ ∅.

Since Core(C, *X*) ⊆ C and *X*0 ⊆ *X*, and due to the monotonicity of Core, we have

Core(Core(C, *X*), *X*0) ⊆ Core(C, *X*),

so that we can weaken the second condition to

∀*x* ′ ∈ *FV*(*t*). *De f*(*x* ′ ) ∩ Core(C, *X*) ≠ ∅.

With (C-Step) for C and *X*, we conclude

$$
\alpha \ge t \in \text{Core}(\mathsf{C}, \mathsf{X}).
$$

Another application of (C-Step), this time for Core(C, *X*) and *X*0, finally yields

$$\forall x \ge t \in \text{Core}(\text{Core}(\mathcal{C}, X), X\_0)$$

□

The intuition of Core is that the least solution of Core(C, *X*0) coincides with C on a relevant part of *X*, namely CoreVars(C, *X*0). But this is not true for every choice of *X*0.

**Example 7.6.** *Assume that Expr*(F , X) *contains appropriate function symbols for expressing subsets of* {*a*, *b*} *and set constraints over these sets. Moreover, assume an appropriate interpretation.*

*1. Consider the following constraint system* C*:*

$$\begin{aligned} \mathfrak{x} &\supseteq y \\ \mathfrak{x} &\supseteq \{a\} \\ y &\supseteq \{b\} \end{aligned}$$

*Now consider X*0 = {*x*}*. Then we get*

$$\begin{aligned} \text{Core}(\mathcal{C}, \mathcal{X}\_0) &= \{\mathfrak{x} \supseteq \{a\}\} \\ \text{CoreVars}(\mathcal{C}, \mathcal{X}\_0) &= \{\mathfrak{x}\} \\ lfp(F\_{\text{Core}(\mathcal{C}, \mathcal{X}\_0)})(\mathfrak{x}) &= \{a\} \\ lfp(F\_{\mathcal{C}})(\mathfrak{x}) &= \{a, b\} \end{aligned}$$

282

*2. Consider the following constraint system* C ′ *.*

$$y \supseteq \ge \mathbf{x}$$

$$\mathfrak{x} \supseteq \{a\}$$

$$y \supseteq \{b\}$$

*Now consider X*′ 0 = {*x*}*. Then we get*

$$\begin{aligned} \text{Core}(\mathcal{C}', X\_0') &= \{ \mathfrak{x} \supseteq \{a\}, y \supseteq \mathfrak{x} \} \\ \text{CoreVars}(\mathcal{C}', X\_0') &= \{ \mathfrak{x}, y \} \\ lfp(F\_{\text{Core}(\mathcal{C}', X\_0')})(y) &= \{ a \} \\ lfp(F\_{\mathcal{C}'})(y) &= \{ a, b \} \end{aligned}$$

The two examples each highlight a characteristic problem that prevents Core(C, *X*0) from exhibiting the same least solution as C, if *X*0 is not chosen appropriately.

In the first example, the problem is that the constraint *x* ⊇ *y* is not contained in Core(C, *X*0), as it does not depend on a constant constraint that defines *x* (or, more generally, a variable from *X*0).

In the second example, *y* ⊇ {*b*} is not included in Core(C ′ , *X* ′ 0 ) because *y* does not belong to *X* ′ 0 .

An appropriate choice of *X*0 hence ensures two things:

1. Every constraint in Core(C, *X*0) transitively depends on a constant constraint defining some variable from *X*0.

2. If a variable *v* ∈ CoreVars(C, *X*0), then all constant constraints defining *v* are contained in Core(C, *X*0).

In the following, I introduce *definition-completeness* as a property of constraint systems that ensures the coincidence of least solutions. After that, I consider conditions on variable sets that ensure the definition-completeness of the corresponding Core set.

**Definition 7.7.** C0 ⊆ C *is called* definition-complete *if it has the property*

$$\forall \mathbf{x} \ge t \in \mathcal{C}. \; Def(\mathbf{x}) \cap \mathcal{C}\_0 \ne \emptyset \implies Def(\mathbf{x}) \subseteq \mathcal{C}\_0.$$

Definition-completeness is indeed sufficient for the coincidence of the least solutions on the core-variables. This is formally stated by Theorem 7.9. Before I can prove that, I need a technical lemma that enables me to perform the fundamental proof steps.

**Lemma 7.8.** *If* C0 *de f* = Core(C, *X*0) *is definition-complete, then* ψ ≤*Vars*(C0 ) *l f p*(*F*C0 ) =⇒ *F*C(ψ) ≤*Vars*(C0 ) *F*C(*l f p*(*F*C0 (7.9) )) *l f p*(*F*C) ≤*Vars*(C0 ) *l f p*(*F*C0 (7.10) )

*Proof.* First, assume that (7.9). Then we can show (7.10) by fixed-point induction (Corollary 2.7). Let

$$\mathcal{P} \stackrel{d\varepsilon f}{=} \{ \psi : X \to L \mid \psi \leq\_{\operatorname{Vars}(\mathcal{C}\_0)} \operatorname{lfp}(\mathcal{F}\_{\mathcal{C}\_0}) \}.$$

We need to show that *const*(⊠) ∈ P, that P is closed under arbitrary joins and that P is closed under *F*C. The first two statements can easily be seen and the third claim is proven by (7.9).

Now we prove (7.9). Assume ψ ≤*Vars*(C0 ) *l f p*(*F*C0 ). We need to show that *F*C(ψ) ≤*Vars*(C0 ) *F*C(*l f p*(*F*C0 )) and for this it is enough to show

$$\forall \mathbf{x} \ge t \in \mathcal{C}. \,\mathbf{x} \in Vars(\mathcal{C}\_0) \implies \|t\|(\psi) \le lfp(F\_{\mathcal{C}\_0})(\mathbf{x}).$$

So let *x*≥*t* ∈ C with *x* ∈ *Vars*(C0). SinceC0 is definition-complete, it must be *x*≥*t* ∈ C0. By Lemma 7.2 and Lemma 7.3, it follows that *FV*(*t*) ⊆ *Vars*(C0). But according to our assumption this means that

$$\forall \mathbf{x'} \in FV(t). \; \psi(\mathbf{x'}) \le lfp(F\_{C\_0})(\mathbf{x'}).$$

Using Lemma 2.10, this entails

$$(\star) \qquad \qquad \qquad \|t\| (\psi) \le \|t\| (lfp(F\_{\mathcal{C}\_0}))\_{\star}$$

and because *l f p*(*F*C0 ) satisfies *x* ≥ *t* we have

$$(\star \star) \qquad \qquad \|t\| (lf p(F\_{\mathcal{C}\_0})) \le lfp(F\_{\mathcal{C}\_0})(\mathbf{x}).$$

From (⋆) and (⋆⋆) we get

$$\|t\| (\psi) \le lfp(F\_{C\_0})(\mathbf{x}),$$

as desired. □

**Theorem 7.9.** *If* Core(C, *X*0) *is definition-complete, then*

$$\text{(7.11)}\qquad lfp(F\_{\mathcal{C}}) =\_{\text{CoreValues}(\mathcal{C}, \mathcal{X}\_0)} lfp(F\_{\text{Core}(\mathcal{C}, \mathcal{X}\_0)})$$

*Proof.* With C0 *de f* = Core(C, *X*0), we need show

*l f p*(*F*C) ≤*Vars*(C0 ) *l f p*(*F*C0 (7.12) )

$$\text{(7.13)}\qquad\qquad lfp(F\_{\mathcal{C}\_{0}}) \leq\_{Vars(\mathcal{C}\_{0})} lfp(F\_{\mathcal{C}})$$

With the given assumptions, (7.12) follows directly from Lemma 7.8. Hence, it remains to show (7.13), which can be justified as follows.

Core(C, *X*0) is a subset of C. Therefore, every solution of C is a solution of Core(C, *X*0). Hence, *l f p*(*F*C) is a solution of Core(C, *X*0). Since *l f p*(*F*Core(C,*X*0 ) ) is the least solution of Core(C, *X*0), this implies *l f p*(*F*Core(C,*X*0 ) ) ≤ *l f p*(*F*C). Clearly, this also holds when restricting to CoreVars(C, *X*0). □

Theorem 7.10 states conditions on *X*0 that characterize definitioncompleteness. This is basically a formalization of the intuition given in Example 7.6.

**Theorem 7.10.** Core(C, *X*0) *is definition-complete if and only if it satisfies the following two conditions:*

$$\begin{aligned} \text{(i)} \qquad & \forall x \ge t \in \mathcal{C}. \ x \in \text{CoreValues}(\mathcal{C}, X\_0) \land FV(t) = \emptyset \\ & \implies x \in X\_0 \end{aligned}$$

∀*x*≥*t* ∈ C. ∀*x* ′ (ii) ∈ *FV*(*t*). *x* ∈ CoreVars(C, *X*0) =⇒ *x* ′ ∈ CoreVars(C, *X*0)

*Proof.* We show the two directions separately.

1. Assume that Core(C, *X*0) is definition-complete and let *x*≥*t* ∈ C and *x* ∈ CoreVars(C, *X*0). Then *x* ∈ *Vars*(Core(C, *X*0)) by Lemma 7.2, which means that *De f*(*x*) ∩ Core(C, *X*0) ≠ ∅. Since Core(C, *X*0) is definitioncomplete, this entails that *x*≥*t* ∈ Core(C, *X*0).

Now we can show (i) and (ii) by considering the two cases *FV*(*t*) = ∅ and *FV*(*t*) ≠ ∅:

$$Def(\mathfrak{x}) \cap \text{Core}(\mathcal{C}, X\_0) \neq \emptyset \land \mathfrak{x} \ge t \in Def(\mathfrak{x}).$$

Together with Lemma 7.2, this implies *x* ∈ CoreVars(C, *X*0).

Now we show *x*≥*t* ∈ Core(C, *X*0) by case distinction on whether *FV*(*t*) = ∅ or not.

$$\forall \mathbf{x'} \in FV(t). \; \mathbf{x'} \in \mathbf{CoreVars}(\mathbf{C}\_{\prime}X\_{0}).$$

by (ii). But by definition and Lemma 7.2 this is the same as

$$\forall \mathbf{x'} \in FV(t). \; Def(\mathbf{x}) \cap \text{Core}(\mathbf{C}\_{\prime}X\_{0}) \neq \emptyset.$$

This implies *x*≥*t* ∈ Core(C, *X*0) by (C-Step).

Now I am ready to present Algorithm 8, a variant of Algorithm 3 that also uses a worklist approach to compute the solution of a given constraint system, but at the same time also performs a reachability analysis. More specifically, Algorithm 8 takes a set *X*0 of variables and, starting with *X*0, traverses the constraint dependency graph from usage to definition.

In the following, I state and prove a correctness result for Algorithm 8. This proof is a a variation of the correctness proof for the ordinary worklist algorithm [130] that I already mentioned in chapter 2. This proof is combined with correctness arguments for the reachability parts taken from Takai [160]35 .

35Tamai [160] also considers integrating reachability into graph problems that can be encoded as constraint systems. They propose an algorithm whose worklist policy is the same as the one for Algorithm 8 and their correctness proof works similarly as the proof of Theorem 7.11. However, Tamai does not encode unreachability explicitly into the lattice.

**Algorithm 8:** A variant of the worklist algorithm where the items taken off the worklist have just been updated but changes have not been propagated yet

```
Input: a monotone constraint system C with interpretation over
        the variables X, a set X0 ⊆ X of initial variables
  Result: a function X → L with properties as stated in The-
         orem 7.11
1 A ← const(⊠)
2 foreach x≥t ∈ C s.t. x ∈ X0 ∧ FV(t) = ∅ do
3 A(x) ← A(x) ⊔ ⟦t⟧(A)
4 W ← W ∪ {x}
5 while W ≠ ∅ do
6 x ← remove(W)
7 foreach x
             ′ ≥ t ∈ C such that x ∈ FV(t) do
8 if ∀y ∈ FV(t). y ≠ x =⇒ A(y) ≠ ⊠ then
9 old ← A(x
                     ′
                     )
10 A(x
               ′
                ) ← A(x
                        ′
                        ) ⊔ ⟦t⟧(A)
11 if A(x
                 ′
                  ) ≠ old then
12 W ← W ∪ {x
                         ′
                          }
13 return A
```
For abbreviation, I define

$$\begin{aligned} \mathcal{C}\_0 & \stackrel{def}{=} \text{Core}(\mathcal{C}\_\prime X\_0), \\ \mathcal{V}\_0 & \stackrel{def}{=} Var(\mathcal{C}\_0) \end{aligned}$$

**Theorem 7.11.** *Algorithm 8 always terminates and upon termination, we have*

$$\text{(7.14)}\qquad\qquad\mathcal{A}(\mathbf{x}) = \begin{cases} \operatorname{lfp}(\mathcal{F}\_{\mathcal{C}\_{0}})(\mathbf{x}) & \text{if } \mathbf{x} \in \mathcal{V}\_{0} \\ \mathbb{E} & \text{otherwise} \end{cases}$$

*Moreover, if* C0 *is definition-complete with respect to* Core(C, *X*)*, then*

$$\text{(7.15)}\qquad\qquad\mathcal{H}=\_{\mathcal{V}\_0} \operatorname{lfp}(F\_{\text{Core}(\mathcal{C},\text{X})}) = \operatorname{lfp}(F\_{\mathcal{C}})$$

*Proof.* First, assume that (7.14) has been shown and that C0 is definitioncomplete with respect to Core(C, *X*). Then

$$\begin{aligned} \mathcal{A} &= \mathsf{V}\_0 \, \, lfp(\mathsf{F}\_{\mathsf{C}\_0}) & \{\,\, \mathsf{(7.14)}\} \\ &= \mathsf{V}\_0 \, \, lfp(\mathsf{F}\_{\mathsf{C} \mathsf{ore}(\mathsf{C}, \mathsf{X})}) & \{\,\, \mathsf{Theorem} \, \, \mathsf{7.9}\} \\ &= lfp(\mathsf{F}\_{\mathsf{C}}) . \end{aligned}$$

It remains to show (7.14). This follows from the following three statements:

$$\{\mathfrak{x} \in X \mid \mathcal{A}(\mathfrak{x}) \neq \mathfrak{x}\} \subseteq \mathcal{V}\_0$$

and upon termination, we have

$$\langle \mathfrak{x} \in X \mid \mathcal{R}(\mathfrak{x}) \neq \mathfrak{B} \rangle = \mathcal{V}\_0.$$

(C) Algorithm 8 maintains the invariant

$$\mathcal{H} \le lfp(F\_{C\_0})$$

and upon termination, we have

$$\mathcal{A} = \nu\_0 \, \_{lf} p(F\_{C\_0}) \, \_{\ast}$$

For a proof of (A), see Lemma 7.12. (B) is going to be shown in Lemma 7.13 and, finally, I will prove (C) in Lemma 7.14. □

The remainder of this section consists of the three statements (A), (B), and (C) that were left to show in the proof of Theorem 7.11.

**Lemma 7.12.** *Algorithm 8 terminates.*

*Proof.* It is sufficient to show that the main loop in the lines 5–13 is only traversed finitely often. For this purpose, we define *T de f* = (*X* → *L*) × 2 *X*. Elements of *T* can be used to represent the state which is maintained by the algorithm: The first component is the currently computed solution and the second component is the current worklist. Moreover, define on *T* the relation

$$(A\_1, W\_1) \leq\_T (A\_2, W\_2) \overset{def}{\Longleftrightarrow} A\_1 >\_{\left(X \to L\right)} A\_2 \lor \left(A\_1 = A\_2 \land W\_1 \subseteq W\_2\right))$$

Then ≤*T* is a partial order and satisfies the descending chain condition, since *X* → *L* satisfies the ascending chain condition and 2 *X* is finite. Let (A, *W*) ∈ *T* be the state of the algorithm at any time.

Now consider an iteration of the main loop. Let (A*old*, *Wold*) and (A*new*, *Wnew*) be the state at the beginning and end of this iteration, respectively. Now two cases are possible and we show that (A*new*, *Wnew*) <*T* (A*old*, *Wold*) must hold in either case.

First, assume that A*old* has not been changed in the iteration. Then we have A*new* = A*old* and the iteration has removed exactly one element of *Wold* and did not add any elements to it, i.e. *Wnew* ⊊ *Wold*, which means that

$$(\mathcal{H}\_{\text{new}}, \mathcal{W}\_{\text{new}}) \prec\_T (\mathcal{H}\_{\text{old}}, \mathcal{W}\_{\text{old}})$$

in this case.

Now assume that A*old* has indeed been touched. Then this can only have happened by executing line 10, which changes A*old* upwards. Hence, we have A*old*(*x*) < A*new*(*x*) for some *x* ∈ *X*. This entails

$$(\mathcal{H}\_{new}, \mathcal{W}\_{new}) \prec\_T (\mathcal{H}\_{old}, \mathcal{W}\_{old})\_{\prime\prime}$$

as desired.

Now we have seen that (A, *W*) becomes strictly smaller in each iteration of the main loop. Hence, since the partial order (*T*,≤*T*) satisfies the descending chain condition, the main loop can only be traversed finitely often, as desired. □

**Lemma 7.13.** *1. Algorithm 8 maintains the invariant*

$$\{\mathfrak{x}\in X \mid \mathcal{R}(\mathfrak{x}) \neq \mathfrak{B}\} \subseteq \mathcal{V}\_{0}.$$

### *2. Upon termination, we have*

$$\{\mathfrak{x}\in X \mid \mathcal{H}(\mathfrak{x}) \neq \mathfrak{B}\} = \text{CoreVars}(\mathcal{C}\_{\prime}X\_{0})\dots$$

*Proof.* 1. For ψ : *X* → *L* define

$$dom(\psi) \stackrel{def}{=} \{ \mathfrak{x} \in \mathcal{X} \mid \psi(\mathfrak{x}) \neq \mathfrak{B} \}.$$

Then we have to show that

(Inv) *dom*(A) ⊆ V0

holds after the execution of each statement in Algorithm 8. We only need to consider executions of line 3 or 10, since all the other statements leave A unchanged and therefore maintain (Inv) trivially.

So consider any execution of line 3 or 10 for a given constraint *x* ≥ *t*. Let A*old* be the value of A before this execution, A*new* be the value of A after this execution.

Assume that (Inv) holds for A*old*.

If the considered execution does not change A, (Inv) is maintained trivially. So assume that the considered execution indeed changes A. In this case we have

$$\operatorname{dom}(\mathcal{R}\_{new}) = \operatorname{dom}(\mathcal{R}\_{old}) \cup \{\mathfrak{x}\}\_{\mathsf{x}}$$

i.e. we must show that *x* ∈ V0.

For an execution of line 3, this is indeed the case: This follows by (V-Base), because line 3 is executed only if *x* ∈ *X*0 and *FV*(*t*) = ∅.

Next consider any execution of line 10. Then it must be the case that *FV*(*t*) is not empty. Moreover, since the considered execution of line 10 changes A, it cannot be the case that A*old*(*x*) = ⊠. Otherwise, ⟦*t*⟧(A*old*) would be ⊠ in the case that *x* ∈ *FV*(*t*), because of (7.2). Together with line 8, this ensures that *FV*(*t*) ⊆ *dom*(A*old*). By (Inv), this means that

$$\forall y \in FV(t). \, y \in \mathcal{V}\_0.$$

By Lemma 7.3, this entails *x* ≥ *t* ∈ C0, or, equivalently, *x* ∈ V0.

2. By induction on *x* ∈ V0, we show that for every *x* ∈ V0, A(*x*) is written to at some point in Algorithm 8.

(V-Base) The initial loop applies every constraint *x* ≥ *t* with *x* ∈ *X*0 and no variables on the right-hand side. Since A is only changed upwards, and because of (7.2), this guarantees that upon termination, we have A(*x*) ≠ ⊠ for every *x* ∈ *X*0 for which there is a constraint *x* ≥ *t* with *FV*(*t*) = ∅.

(V-Step) Consider a constraint *x* ≥ *t* such that

$$
\emptyset \neq FV(t) \subseteq \mathcal{V}\_0.
$$

By induction hypothesis, we may assume that for all *y* ∈ *FV*(*t*), A(*y*) is written to for the first time at some point in Algorithm 8. Since *FV*(*t*) ≠ ∅, we may further assume that there is an iteration in which this happens for the last *y*0 ∈ *FV*(*t*). Particularly, at the beginning of this iteration, A(*y*) ≠ ⊠ for all *y* ∈ *FV*(*t*) \ {*y*0} and A(*y*0) = ⊠ and at the end of this iteration A(*y*) ≠ ⊠ for all *y* ∈ *FV*(*t*). This means that A(*y*0) is changed in this iteration and since *y*0 ∈ *FV*(*t*), *x* is added to *W*. Hence, at the end of the iteration, *x* ∈ *W*. Since Algorithm 8 terminates (Lemma 7.12), *x* is eventually considered in some later iteration. We may assume that A(*x*) = ⊠ at the beginning of this iteration, since otherwise our claim follows trivially. Furthermore, we notice that

$$\forall y \in FV(t) . \mathcal{A}(y) \neq \mathbb{B}$$

is maintained until Algorithm 8 terminates. So, this property holds particularly in the iteration in which *x* is removed from the worklist. During this iteration, *x* ≥ *t* is eventually considered. Again, we assume that A(*x*) = ⊠ until *x* ≥ *t* is considered, since otherwise there is nothing to show. Now, when *x* ≥ *t* is eventually processed, the check in line 8 passes and A(*x*) is written to for the first time.

□

**Lemma 7.14.** *1. Algorithm 8 maintains the invariant*

$$\mathcal{H} \le lfp(F\_{\mathcal{C}\_0})\,.$$

*2. Upon termination, we have*

$$\mathcal{A} =\_{\mathcal{V}\_0} \operatorname{lfp}(F\_{\mathcal{C}\_0}) \dots$$

*Proof.* We show the two statements separately.

1. We have to show that

$$\text{(Inv)}\tag{1\text{nv}} \qquad\qquad\qquad\qquad\qquad\mathcal{R}\leq \operatorname{lfp}(\mathcal{F}\_{\mathcal{C}\_{0}})\_{\mathcal{F}}$$

is maintained by every execution of each statement in Algorithm 8. We only need to consider executions of line 3 or 10, since all the other statements leave A unchanged and therefore maintain (Inv) trivially.

So consider any execution of 3 or 10. Let *x* ≥ *t* be the constraint that is applied. First, we notice that line 3 is only executed if *x* ∈ *X*0 and *t* contains no variables. Hence, *x*≥*t* ∈ C0. Secondly, we see that line 10 is only executed if

$$\forall y \in FV(t) . \mathcal{R}(y) \neq \mathbb{B}\_{\prime}$$

and this implies, according to the invariant in Lemma 7.13, that *FV*(*t*) ⊆ V0. Hence, in both lines 3 and 10 we have *x*≥*t* ∈ C0 and therefore

$$l(\star) \qquad \qquad lfp(F\_{\mathcal{C}\_0})(x) \ge \|t\| (lfp(F\_{\mathcal{C}\_0})) .$$

Let A*old* be the value of A before the execution and A*new* be the value of A after the execution of line 3 or 10. Then we have

$$(\star \star) \qquad \qquad \mathcal{A}\_{\text{new}}(\mathfrak{x}) = \mathcal{A}\_{\text{old}}(\mathfrak{x}) \sqcup \llbracket t \rrbracket(\mathcal{A}\_{\text{old}}) .$$

Now assume that (Inv) holds for A*old*. To show (Inv) for A*new*, we only need to consider A*new*(*x*) since the rest is left unchanged.

Then, we can argue as follows:

$$\begin{aligned} &\mathcal{A}\_{new}(\mathbf{x})\\ &=\mathcal{A}\_{old}(\mathbf{x})\sqcup\llbracket\!\!\!\!f(\mathcal{A}\_{old})\\ &\leq\inf\_{\mathbf{f}}(\mathbf{F}\_{\mathbf{C}\_{0}})(\mathbf{x})\sqcup\llbracket\!\!\!f(\mathbf{f}\!p(\mathbf{F}\_{\mathbf{C}\_{0}})) & &\{\}(\text{Inv}),\text{Lemma 2.10 }\}\\ &=\ulcorner{\mathcal{J}}{\scriptstyle\!f}(\mathbf{F}\_{\mathbf{C}\_{0}})(\mathbf{x}) & &\{\}(\star)\nmid\end{aligned}$$

2. We show that the main loop of Algorithm 8 maintains the invariant

$$\begin{aligned} (\text{Inv}) \quad & \forall \mathfrak{x} \succeq \mathfrak{t} \in \mathcal{C}. \quad \mathfrak{x} \in \text{dom}(\mathcal{R})\\ & \qquad \land \, FV(t) \subseteq \text{dom}(\mathcal{R})\\ & \qquad \land \, FV(t) \cap \mathcal{W} = \emptyset\\ & \Longrightarrow \mathcal{A}(\mathfrak{x}) \ge \|\mathfrak{t}\|(\mathcal{A}). \end{aligned}$$

292

This is sufficient: Upon termination, *W* is empty. Hence, the following property holds:

$$\forall \mathbf{x} \ge t \in \mathcal{C}. \,\mathbf{x} \in dom(\mathcal{H}) \land FV(t) \subseteq dom(\mathcal{H}) \implies \mathcal{R}(\mathbf{x}) \ge \|t\|(\mathcal{R}).$$

Using Lemma 7.13, this is equivalent to

$$\forall \text{7.16} \qquad \forall \mathbf{x} \in \mathcal{V}\_{0}. \; \forall \mathbf{x} \ge t \in \mathcal{C}. \; FV(t) \subseteq \mathcal{V}\_{0} \implies \mathcal{R}(\mathbf{x}) \ge \|t\|(\mathcal{R}).$$

Now consider any constraint *x*≥*t* ∈ Core(C, *X*0). If *x* ∈ *X*0 and *FV*(*t*) = ∅, then (7.16) trivially implies that A satisfies *x* ≥ *t*. Next, consider the case that *FV*(*t*) ≠ ∅ and

$$\forall y \in FV(t). \; Def(y) \cap \mathcal{C}\_0 \neq \emptyset.$$

ByLemma 7.3 and Lemma 7.2, it follows that *FV*(*t*) ⊆ V0. Again, by application of (7.16) we see that *x* ≥ *t* is satisfied by A.

It remains to show that (Inv) holds at the beginning of the main loop and is maintained by each of its iterations.

(Inv) **holds just before the first iteration of the main loop:** In the initialization loop, A was only updated for *x* ∈ *X*0 and only for those constraints *x* ≥ *t* where *FV*(*t*) = ∅. Hence, if *x*≥*t* ∈ C with *FV*(*t*) ∩ *W* = ∅ and A(*x*) ≠ ⊠ and ∀*y* ∈ *FV*(*t*). A(*y*) ≠ ⊠, it must be the case that *x* ∈ *X*0 and *FV*(*t*) = ∅. Due to the initialization, A(*x*) ≥ ⟦*t*⟧(A) holds since this was ensured by the assignment in line 3 and could not be invalidated by any other execution of this line.

(Inv) **is maintained by any iteration:** Let *i* be some iteration of the main loop. Let A*old* and *Wold* be the values of A and *W* at the beginning of this iteration and A*new* and *Wnew* the respective values at the end. Assume that (Inv) holds at the beginning of *i*:

$$\begin{aligned} (\text{Inv}\_{pre}) \quad & \quad \forall \mathfrak{x} \ge t \in \mathcal{C}. \quad \mathfrak{x} \in \text{dom}(\mathcal{A}\_{old})\\ & \quad \land FV(t) \subseteq \text{dom}(\mathcal{A}\_{old})\\ & \quad \land FV(t) \cap \mathcal{W}\_{old} = \emptyset\\ & \implies \mathcal{R}\_{old}(\mathfrak{x}) \ge \|t\|(\mathcal{A}\_{old}). \end{aligned}$$

Now consider a constraint *x*≥*t* ∈ C with A*new*(*x*) ≠ ⊠ and *FV*(*t*) ∩ *Wnew* = ∅ and *FV*(*t*) ⊆ *dom*(A*new*). We have to show A*new*(*x*) ≥ ⟦*t*⟧(A*new*).

First, we make two important observations: Firstly, it must be the case that

$$\text{(7.17)}\tag{7.17}$$

$$\mathcal{H}\_{\text{new}} \ge \mathcal{H}\_{\text{old}}.$$

Secondly, from *FV*(*t*) ∩ *Wnew* = ∅, we can conclude

$$(7.18) \qquad \forall y \in FV(t). \; \mathcal{R}\_{new}(y) = \mathcal{R}\_{old}(y).$$

Now we make a case distinction:

a) A*old*(*x*) ≥ ⟦*t*⟧(A*old*). Then we can show our claim as follows:

b) A*old*(*x*) ̸≥ ⟦*t*⟧(A*old*). Then because of (Inv*pre*), one of the following statements must be true:

We consider each of these cases separately.

• For (7.19), we argue as follows:

$$\begin{aligned} & \quad \|t\| (\mathcal{H}\_{\text{new}})\\ &= \|t\| (\mathcal{H}\_{old})\\ &= \mathbb{E} & \qquad \qquad \qquad \qquad \{\text{(7.18)}\}\\ &\leq \mathcal{H}\_{\text{new}}(\mathbf{x}) & \qquad \qquad \{\text{(7.1)}\} \end{aligned}$$

• If (7.20) holds, then line 10 must have been executed for *x* ≥ *t*. Afterwards, A(*x*) could only have changed upwards, so we can conclude:

A*new*(*x*)

• If (7.21) is true, then a variable *x* ′′ was removed from *W* and every *x* ′ ≥ *t* ′ with *x* ′′ ∈ *FV*(*t* ′ ) was considered and A(*x* ′ ) was updated if needed. Since *x* ′′ ∈ *Wold* and *FV*(*t*) ∩ *Wold* ≠ ∅ and *FV*(*t*) ∩ *Wnew* = ∅ and *x* ′′ was the only element which was removed from *W*, it must be *x* ′′ ∈ *FV*(*t*). Hence, line 10 was particularly executed for *x* ≥ *t*. Now we can argue just as in case (7.20).

□

# **7.2 Integration of Interprocedural Slicing and Interprocedural Data-Flow Analysis**

This section gives an outline of sections 7.3 and 7.4, in which I am going to apply the results from section 7.1 to the constraint systems that I showed and discussed in chapter 6.

Section 7.3 is dedicated to the functional approach, while section 7.4 considers the call-string approach.

For my purposes, I fix a data-flow framework F = (*G*, *L*, *F*, ρ). Moreover, I fix a set *Src* ⊆ *N* of *source nodes*.

The goal of the following sections is to derive algorithms that compute a *VP*-correct solution on the forward slice of *Src*. I do this by instantiating Algorithm 8 for solving relevant parts of the constraint systems that we saw in chapter 6.

To be able to handle unreachability, I adjoin F with an element ⊠ and extend *F* and ⟦.⟧ like outlined in section 5.3 and section 6.1, respectively. In particular, this is compatible with (7.1) and (7.2), so that I can actually apply the results from section 7.1 to the constraint systems chapter 6.

Next, I want to describe a recurring theme of the following sections. For simplicity, I exclude the call-string approach for the moment. I will handle its specifics in section 7.4.

Consider a constraint system CP corresponding to a set of paths P ⊆ *PathsG*. Then I want to use an instantiation of Algorithm 8 to compute a solution AP along the paths from P such that

$$\forall (\mathbf{s}, t) \in \mathcal{V}\_0^{(\mathcal{P})} . \mathcal{R}\rho(\mathbf{s}, t) = lfp(\mathbf{C}p)(\mathbf{s}, t) .$$

where

$$\mathcal{V}\_0^{(\mathcal{P})} \stackrel{def}{=} \{ (\mathbf{s}, t) \in \mathcal{N} \times \mathcal{N} \mid \text{Paths}\_{\mathcal{G}}(\mathbf{s}, t) \cap \mathcal{P} \neq \emptyset \}.$$

According to Theorem 7.11, Algorithm 8 computes such an AP for V (P) 0 = CoreVars(CP, *X*0), where *X*0 ⊆ *X* is chosen appropriately andCore(CP, *X*0) is definition-complete in Core(CP, *X*). Hence, the general steps of the following sections will be

$$\text{CoreVars}(\mathsf{C}\_{\mathcal{P}}, X\_0) = \{ (\mathsf{s}, t) \in \mathsf{N} \times \mathsf{N} \mid \mathsf{Paths}\_{\mathcal{G}}(\mathsf{s}, t) \cap \mathcal{P} \neq \emptyset \}$$

and, finally,

4. show that Core(CP, *X*0) is definition-complete in Core(CP, *X*).

# **7.3 Functional Approach**

I want to remind the reader of Constraint System 6.4, which was defined as follows:

$$\begin{pmatrix} \text{vALup-son} \\ \text{vALup-son} \end{pmatrix} \begin{array}{l} \text{X}\_{\text{ASC}}(s,n) \neq \texttt{\texttt{\texttt{\\_}}} \qquad \begin{array}{l} \text{X}\_{\text{DECSC}}(n,t) \neq \texttt{\texttt{\\_}} \end{array} \\\begin{array}{l} \text{X}\_{\text{VP}}(s,t) \geq \texttt{\\_}\_{\text{DECSC}}(n,t) \odot \text{X}\_{\text{ASC}}(s,n) \\\text{\\_} \quad \begin{array}{l} \text{\\_} \ \text{\\_} \end{array} \qquad \begin{array}{l} \text{\\_} \end{array} \} \end{array}$$

Given *XASC* and *XDESC*, a valid-paths solution *XVP* could be obtained by evaluating the equation

$$\text{(7.22)}\qquad\qquad\text{X}\_{VP}(\mathbf{s},t)=\bigsqcup\_{n\in\mathcal{N}}\text{X}\_{\text{DESC}}(n,t)\circ\text{X}\_{\text{ASC}}(\mathbf{s},n).$$

One direct and naive strategy would be to first compute both *XASC* and *XDESC* on the whole set *N* × *N* and then use these functions to evaluate (7.22). However, such an approach would perform a lot of unnecessary work: In fact, one only needs to compute *XDESC*(*n*, *t*) ◦ *XASC*(*s*, *n*) for those *s*, *n*, *t* ∈ *N* for which *s* ∈ *Src*, *XASC*(*s*, *n*) ≠ ⊠ and *XDESC*(*n*, *t*) ≠ ⊠.

We can reduce the amount of unnecessary work by first computing *XASC* on *dom*(*ASC*) and then use *XASC* to compute an integral part of *XVP*. Roughly, the idea is to compute a solution *XNASC* such that *XVP* can be written as *XASC* ⊔ *XNASC*. For this, I need to introduce another set of paths, the *non-ascending* paths.

**Definition 7.15.** π ∈ *PathsG*(*s*,*t*) *is called* non-ascending *if* π *can be written as* π1 · π2 *such that*

$$\text{(i)}\tag{1}$$

$$\pi\_1 \in \text{ASC}(\text{s}, n)$$

(ii) π2 ∈ *DESC*(*n*, *t*)

$$\text{(iii)}\tag{iii}$$

π1 (iv) · π2 ∉ *ASC*(*s*, *t*)

*I denote the set of non-ascending paths from s to t with NASC*(*s*, *t*)*.*

Definition 7.15 is motivated by the fact that any valid path is either ascending or non-ascending. This is formalized by Lemma 7.16 and Remark 7.17.

**Lemma 7.16.** *If* π ∈ *VP*(*s*, *t*)*, then either of the following is true:*

*1.* π ∈ *ASC*(*s*, *t*)

*2. There are c* ∈ *Ncall,* π1 ∈ *ASC*(*s*, *c*) *and* π2 ∈ *DESC*(*c*,*t*) *such that* π = π1 · π2

*Proof.* Let π ∈ *VP*(*s*,*t*) \ *ASC*(*s*,*t*). By Theorem 5.22 there is *i* ∈ *range*(π) such that π <*i* ∈ *Le f t*(*E*), π ≥*i* ∈ *Right*(*E*) and π *i* ∈ *Ecall*. Define

$$c \stackrel{def}{=} src(\pi^i)\_{\prime}$$

$$\pi\_1 \stackrel{def}{=} \pi^{
$$\pi\_2 \stackrel{def}{=} \pi^{\ge i}.$$
$$

Then *c* ∈ *Ncall*, since π *i* is an outgoing call edge of π *i* . Moreover, because π ∈ *PathsG*(*s*, *t*), we have π1 ∈ *PathsG*(*s*, *c*) and π2 ∈ *PathsG*(*c*, *t*). Lastly, by Theorem 5.39, we have π1 ∈ *Val*(*E*) and π2 ∈ *Val*(*E*). In summary, π1 , π2 and *c* have the desired properties. □ **Remark 7.17.** π ∈ *NASC*(*s*, *t*) *if and only if* π ∈ *VP*(*s*, *t*) \ *ASC*(*s*, *t*)*.*

*Proof.* " ⇐= " is covered by Lemma 7.16. So let π ∈ *NASC*(*s*,*t*). Then π ∈ *VP*(*s*,*t*) by Theorem 5.30 and since π ∈ *PathsG*(*s*, *t*). Furthermore, π ∉ *ASC*(*s*, *t*) by Definition 7.15. □

Lemma 7.16 can be applied as follows: Since any valid path is either ascending or non-ascending, we can obtain a valid-paths solution by joining an ascending-paths solution with a solution *XNASC* that merges over all *non-*ascending paths.

The rest of this section is dedicated to computing a valid-paths-solution using the approach that I just sketched. First, subsection 7.3.1 considers the computation of the least same-level solution A(*SL*) . Then, subsection 7.3.2 shows how to use a same-level solution such as A(*SL*) to compute the least ascending-paths solution A(*ASC*) . After that, subsection 7.3.3 is dedicated to the extension of a given ascending-paths solution like A(*ASC*) along the descending paths to obtain the least non-ascending-paths-solution: First, a constraint system is given that characterizes non-ascending-paths solutions and then the usual scheme is used to compute the least nonascending-paths solution A(*NASC*) .

The last three subsections consider the combination of A(*ASC*) and A(*NASC*) . Subsection 7.3.4 shows that joining A(*ASC*) and A(*NASC*) actually yields a valid-paths-correct solution, provided that A(*ASC*) and A(*NASC*) are correct relative to their respective path sets. Moreover, it compares the solution obtained by this approach with the original least valid-paths solution. After that, subsection 7.3.5 integrates all the sections before in a simple algorithm and shows its correctness. This algorithm uses the same ideas as the two-phase slicer by Horwitz et al. that I already discussed in chapter 3, however there are still some differences. Subsection 7.3.6 explores these differences, modifies the algorithm from subsection 7.3.5 in such a way that it essentially becomes the two-phase slicer and sketches a correctness proof.

# **7.3.1 Computing the Same-Level Solution**

In the following, I consider the constraint system from Constraint System 6.1, which I denote with C (*SL*) .

I define

$$\{\text{7.23}\} \qquad \qquad \begin{array}{c} \text{X}\_0^{(\text{SL})} \stackrel{def}{=} \{\text{(s,s)} \mid s \in \text{N}\_{\text{entry}}\}. \end{array}$$

$$\text{(7.24)}\qquad\qquad\mathcal{C}\_0^{(SL)} \stackrel{def}{=} \text{Core}(\mathcal{C}^{(SL)}, \mathcal{X}\_0^{(SL)})$$

$$(\text{7.25}) \qquad \qquad \mathcal{V}\_0^{(SL)} \stackrel{def}{=} \text{CoreVars}(\mathcal{C}^{(SL)}, X\_0^{(SL)})$$

Algorithm 9 is an instantiation of Algorithm 8 for the constraint system C (*SL*) , using *X* (*SL*) as set of initial variables.

0 The loop in lines 2–4 corresponds to the initialization loop in Algorithm 8. It processes all constant constraints in Constraint System 6.1 whose left-hand side is in *X* (*SL*) .

0 The loop in lines 5–18 corresponds to the main loop Algorithm 8. All constraints *x* ≥ *u* with (*s*,*t*) ∈ *FV*(*u*) are enumerated and the respective A(*SL*) (*x*) is updated, just like in Algorithm 8. However, the constraint enumeration loop in Algorithm 9 is split into three parts.

The first of these parts, in lines 7–9, enumerates all constraints of the form sl-sol-(ii).

The other two parts are dedicated to constraint sl-sol-(iii). This is because Algorithm 9 propagates from the right-hand side of a constraint to its left-hand side. In contrast to sl-sol-(ii), there are *two* free variables on the right-hand side of sl-sol-(iii)-constraints, so that (*s*,*t*) can occur at two positions. To illustrate this, let us take a look at such a constraint. It has the form

$$X\_{SL}(s, t) \ge f\_{\mathfrak{e}\_{\text{ret}}} \circ X\_{SL}(\mathfrak{m}\_0 \cdot \mathfrak{n}\_1) \circ f\_{\mathfrak{e}\_{\text{call}}} \circ X\_{SL}(s, \mathfrak{n})$$

with *n ecall* → *n*0, *n*1 *eret* → *t* and (*ecall*,*eret*) ∈ Φ.

Hence, each of the two variables on the right-hand side of a rule have to be considered separately.

The loop in lines 10–13 takes care of the case that the variable currently processed is (*s*, *n*) in the above situation, whereas the loop in lines 15–18 takes care of the other case: Here, the variable currently processed is (*n*0, *n*1 ) in the above situation.

In summary, the two loops enumerate all constraints *c* of the form sl-sol-(iii) with (*s*, *t*) ∈ *FV*(*rhs*(*c*)).

**Algorithm 9:** Algorithm for computing the least same-level solution

```
Input: a data-flow framework instance F = (G, L, F⊠, ρ) as de-
         scribed on page 295
  Result: least same-level solution for F , as stated in Theorem 7.18
1 A(SL) ← const(⊠)
2 foreach s ∈ Nentry do
3 A(SL)
            (s,s) ← id
4 W = W ∪ {(s,s)}
5 while W ≠ ∅ do
6 (s, t) ← remove(W)
7 foreach t
               ′ ∈ N s.t. t e→ t
                             ′ ∧ e ∈ Eintra do
8 A(SL)
               (s, t
                   ′
                   ) ← A(SL)
                              (s, t
                                 ′
                                  ) ⊔ fe ◦ A(SL)
                                               (s, t)
9 W ← W ∪ {(s, t
                        ′
                         )} if A(SL)
                                   (s, t
                                       ′
                                       ) has changed
10 foreach (ec,er)∈Φ s.t. t ec → n0 ∧ n1
                                        er → t
                                            ′ ∧ A(SL)
                                                     (n0, n1
                                                            ) ≠ ⊠ do
11 slSol ← fer
                    ◦ A(SL)
                            (n0, n1
                                  ) ◦ fec
12 A(SL)
               (s, t
                   ′
                   ) ← A(SL)
                              (s, t
                                 ′
                                  ) ⊔ s ◦ A(SL)
                                              (s, t)
13 W ← W ∪ {(s, t
                        ′
                         )} if A(SL)
                                   (s, t
                                       ′
                                       ) has changed
14 foreach (ec,er)∈Φ s.t. a ec → s ∧ t
                                      er → b do
15 foreach u ∈ Nentry s.t. A(SL)
                                     (u, a)≠⊠ do
16 slSol ← fer
                        ◦ A(SL)
                               (s, t) ◦ fec
17 A(SL)
                   (u, b) ← A(SL)
                                 (u, b) ⊔ slSol ◦ A(SL)
                                                     (u, a)
18 W ← W ∪ {(u, b)} if A(SL)
                                      (u, b) has changed
19 return A(SL)
```
Now that the reader is convinced that Algorithm 9 is an instantiation of Algorithm 8, I want to instantiate the correctness result of Algorithm 8 for Algorithm 9.

For the moment, I assume that C (*SL*) 0 is definition-complete with respect to C (*SL*) . Then I can use Theorem 7.11 to prove the following correctness result.

**Theorem 7.18.** *The following statements hold:*

*1. Algorithm 9 always terminates and upon termination, we have*

$$(\text{7.26})\qquad\qquad\mathcal{H}^{(SL)}(\text{s},t)=\begin{cases}lfp(\text{F}\_{\text{C}^{(SL)}})(\text{s},t) & \text{if } (\text{s},t) \in \mathcal{V}\_{0}^{(SL)}\\ \boxtimes & \text{otherwise} \end{cases}$$

Two things are left to do. Firstly, we have to characterize V (*SL*) 0 appropriately and secondly, we have to show that C (*SL*) 0 is indeed definitioncomplete with respect to C (*SL*) .

We start with the characterization of V (*SL*) 0 . Ideally, considering the fact that C (*SL*) is defined along the same-level paths of *G*, same-level reachability should be the right property to characterize C (*SL*) 0 . Moreover, taking *X* (*SL*) 0 into account, we can only expect (*s*, *t*) ∈ V(*SL*) 0 if *s* ∈ *Nentry*.

Lemma 7.19 formally confirms that V (*SL*) 0 indeed has the desired characterization.

**Lemma 7.19.**  The claim (7.29) follows directly from (7.27).

It remains to show (7.27) and (7.28). We only show (7.27), since the proof for (7.28) is very similar.

We prove (7.27) by showing the two subset relations separately.

# 1. In order to prove "⊇", we show

$$\begin{aligned} \forall \pi \in SL. \mathsf{V}(s, t) \in \mathsf{N}\_{entry} \times \mathsf{N}. \,\,\pi \in SL(s, t) \\ \implies (s, t) \in \mathsf{V}^{(SL)}\_{0} \end{aligned}$$

by induction on π ∈ *SL*. So let π ∈ *SL* and (*s*,*t*) ∈ *Nentry* × *N* such that π ∈ *SL*(*s*, *t*).

a) Suppose that π = ϵ. Then we have *s* = *t* and *s* ∈ *Nentry*, so that (*s*, *t*) = (*s*,*s*) ∈ *X* (*SL*) 0 . By sl-sol-(i), C (*SL*) contains the constraint

$$X(s,s) \ge id\_{\prime\prime}$$

which does not have variables on the right-hand side. Hence, (*s*,*s*) ∈ CoreVars(C (*SL*) , *X* (*SL*) 0 ) by (V-Base).

b) Assume that π = π ′ ·*e*, where *e* ∈ *Eintra*, *t* ′ *e*→ *t* and π ′ ∈ *SL*(*s*, *t* ′ ). Since π ′ ∈ *SL*(*s*,*t* ′ ), we can apply the induction hypothesis to π ′ : *s* ∈ *Nentry* implies that

$$(s, t') \in \mathcal{V}\_0^{(SL)}.$$

By sl-sol-(ii), C (*SL*) contains the constraint

$$X(s, t) \ge f\_{\varepsilon} \circ X(s, t').$$

Since (*s*, *t* ′ ) ∈ V(*SL*) 0 we may apply (V-Step) and conclude

$$(\mathbf{s}, t) \in \mathcal{V}\_0^{(SL)}.$$

c) Suppose that

$$
\pi = \pi' \cdot e\_{call} \cdot \pi'' \cdot e\_{ret}
$$

with π ′ ∈ *SL*(*s*, *n*), π ′′ ∈ *SL*(*n*0, *n*1 ), *n ecall* → *n*0, *n*1 *eret* → *t* and (*ecall*,*eret*) ∈ Φ. We apply the induction hypothesis to π ′ ∈ *SL*(*s*, *n*) and conclude from *s* ∈ *Nentry* that

$$(\text{7.30})\tag{7.30}$$

302

Moreover, note that *n*0 has an incoming call edge. Hence, we have *n*0 ∈ *Nentry*. With π ′′ ∈ *SL*(*n*0, *n*1 ) we can apply the induction hypothesis to π ′′ and obtain

$$(\text{7.31})\qquad\qquad(\boldsymbol{\eta}\_{0},\boldsymbol{\eta}\_{1})\in\mathsf{CoreVars}(\mathcal{C}^{(SL)},\boldsymbol{X}\_{0}^{(SL)})\,.$$

Moreover, by sl-sol-(iii), C (*SL*) contains the constraint

$$X(s, t) \ge f\_{\varepsilon\_{ret}} \circ X(n\_0, n\_1) \circ f\_{\varepsilon\_{call}} \circ X(s, n).$$

With (V-Step), we conclude (*s*, *t*) ∈ V(*SL*) 0 from (7.30) and (7.31).

2. For "⊆", we show

$$(s,t)\in \mathcal{V}\_0^{(SL)} \implies SL(s,t) \neq \emptyset \land s \in \mathcal{N}\_{\textit{entry}}$$

by induction over V (*SL*) 0 = CoreVars(C (*SL*) , *X* (*SL*) 0 ).

Let (*s*,*t*) ∈ V(*SL*) 0 . Let *c* ∈ C(*SL*) 0 with *lhs*(*c*) = (*s*,*t*). Our induction hypothesis states

$$\forall (\mathbf{x}, \mathbf{y}) \in FV(\text{rhs}(\mathbf{c})). \ SL(\mathbf{x}, \mathbf{y}) \neq \emptyset \land \mathbf{s} \in \mathcal{N}\_{entry}$$

a) Suppose that *FV*(*rhs*(*c*)) = ∅. Then *c* must be of the form

$$\mathbf{x}\_{SL}(s,s) \ge id$$

Clearly, *SL*(*s*,*s*) ≠ ∅, since ϵ ∈ *SL*(*s*,*s*).

b) Suppose that *FV*(*rhs*(*c*)) ≠ ∅. Then *c* is either of the form sl-sol-(ii) or sl-sol-(iii). We only consider sl-sol-(iii), since sl-sol-(ii) is similar. So assume that *c* has the form

$$X\_{SL}(\mathbf{s}, t) \ge f\_{\mathbf{c}\_{\text{ret}}} \circ X\_{SL}(n\_0, n\_1) \circ f\_{\mathbf{c}\_{\text{call}}} \circ X\_{SL}(\mathbf{s}, n)$$

such that *n ecall* → *n*0, *n*1 *eret* → *t* and (*ecall*,*eret*) ∈ Φ. From *c* ∈ C(*SL*) 0 , we conclude (*s*, *n*) ∈ V(*SL*) 0 and (*n*0, *n*1 ) ∈ V(*SL*) 0 . Hence, we can apply the induction hypothesis to (*s*, *n*) and (*n*0, *n*1 ) and yield *s* ∈ *Nentry*, π ′ ∈ *SL*(*s*, *n*) and π ′′ ∈ *SL*(*n*0, *n*1 ). These two paths can be used to obtain

$$
\pi \stackrel{def}{=} \pi' \cdot e\_{call} \cdot \pi'' \cdot e\_{ret} \in SL(s, t)\_{\prime \prime}
$$

as desired.

□

In order to complete the proof of Theorem 7.18, we show the definitioncompleteness of C (*SL*) 0 with respect to Core(C (*SL*) , *N* × *N*).

**Lemma 7.20.** C (*SL*) 0 *is definition-complete with respect to its superset*

$$\text{Core}(\mathcal{C}^{(SL)}, \mathcal{N} \times \mathcal{N}).$$

*Proof.* We use Theorem 7.10. Let *c* ∈ Core(C (*SL*) , *N* × *N*) with *lhs*(*c*) ∈ V (*SL*) 0 . Then we have to show

$$(7.32) \qquad \qquad FV(rhs(c)) = \emptyset \implies lhs(c) \in X\_0^{(SL)}$$

*FV*(*rhs*(*c*)) ≠ ∅ ∧ *x* ∈ *FV*(*rhs*(*c*)) =⇒ *x* ∈ CoreVars(C (*SL*) , *X* (*SL*) 0 (7.33) )

• For (7.32), assume that *FV*(*rhs*(*c*)) = ∅. Then *c* is of the form

*XSL*(*s*,*s*) ≥ *id*

From *lhs*(*c*) = (*s*,*s*) ∈ V(*SL*) 0 we get *s* ∈ *Nentry* by (7.27). Hence, (*s*,*s*) ∈ *X* (*SL*) 0 .

	- 1. Let *c* be of the form sl-sol-(iii), i.e.

$$X\_{SL}(s, t) \ge f\_{\varepsilon\_{\rm ret}} \circ X\_{SL}(n\_0, n\_1) \circ f\_{\varepsilon\_{\rm call}} \circ X\_{SL}(s, n)$$

with *n ecall* → *n*0, *n*1 *eret* → *t* and (*ecall*,*eret*) ∈ Φ. From *lhs*(*c*) = (*s*,*t*) ∈ V(*SL*) 0 , we conclude *s* ∈ *Nentry* by (7.27). Since *c* ∈ C(*SL*) 0 , we have

$$(\star) \qquad \qquad X\_{SL}(\mathbf{s}, n) \in \mathsf{CoreVars}(\mathcal{C}^{(SL)}, N \times N) \text{, and } n$$

$$(\star \star) \qquad \quad X\_{SL}(n\_0, n\_1) \in \text{CoreVars}(\mathcal{C}^{(SL)}, N \times N).$$

We apply (7.29) and conclude from *s* ∈ *Nentry*, (⋆) and (⋆⋆) that *XSL*(*s*, *n*) ∈ CoreVars(C (*SL*) , *X* (*SL*) 0 ). Moreover, note that *n*0 ∈ *Nentry*, since it has an incoming call edge. Hence, *XSL*(*n*0, *n*1 ) ∈ V(*SL*) 0 by (7.29).

With (C-Step), it follows from (⋆) and (⋆⋆) that *c* ∈ C(*SL*) 0 , and, with (V-Step), (*s*, *t*) ∈ V(*SL*) 0 . This concludes the proof of (7.33) for *c*.

2. The argument for the form sl-sol-(ii) is very similar.

□

# **7.3.2 Computing the Ascending Solution**

In the following, I consider the constraint system from Constraint System 6.2, which I denote with C (*ASC*) . I define

$$(\text{7.34})\qquad\qquad X\_0^{(\text{ASC})\ d} \stackrel{def}{=} \{(s,s) \mid s \in \text{Src}\}$$

$$\text{(7.35)}\qquad\qquad\mathcal{C}\_{0}^{(\text{ASC})} \stackrel{def}{=} \text{Core}(\mathcal{C}^{(\text{ASC})}, X\_{0}^{(\text{ASC})})$$

$$(\text{7.36}) \qquad \qquad \mathcal{V}\_0^{(\text{ASC})} \stackrel{def}{=} \text{CoreVars}(\mathcal{C}^{(\text{ASC})}, X\_0^{(\text{ASC})})$$

Algorithm 10 is a straight-forward instantiation of Algorithm 8 to solve Constraint System 6.2 with respect to a function

$$
\mathbb{X}\_{\mathrm{SL}} : \mathrm{N} \times \mathrm{N} \to F\_{\mathbb{B}}.
$$

This function could have been computed by Algorithm 9, but can also have been obtained in any other way.

Theorem 7.21 gives a correctness result for Algorithm 10. Similar to Theorem 7.18, the first item in Theorem 7.21 directly follows from the generic result Theorem 7.11, once I have shown that C (*ASC*) 0 is definitioncomplete with respect to C (*ASC*) . However, this first item only is concerned with the relation between the result of Theorem 7.18 and the least solution of C (*ASC*) . In order to get full correctness and precision results, I need additional requirements for *XSL*, relative to a set Ψ ⊆ *N* × *N*.

In principle, there are multiple choices for Ψ. I just need to ensure that (a) Ψ is large enough so that C (*ASC*) and Algorithm 10 never access *XSL* outside of Ψ and that (b) the output of Algorithm 9 is indeed (*SL*, Ψ)-correct. The following choice of Ψ has both properties:

$$\begin{aligned} (\mathsf{T}.\mathsf{37}) \quad (n\_0, n\_1) \in \mathsf{Y} \stackrel{def}{\Leftrightarrow} \quad (n\_0, n\_1) \in \mathsf{N}\_{\mathsf{entity}} \times \mathsf{N}\_{\mathsf{exit}}\\ \wedge \exists n, t \in \mathsf{N}. \; \exists (e\_{\mathsf{call}}, e\_{\mathsf{ret}}) \in \mathsf{Φ}. \; n \stackrel{e\_{\mathsf{call}}}{\rightarrow} n\_0 \land n\_1 \stackrel{e\_{\mathsf{ret}}}{\rightarrow} t. \end{aligned}$$

Property (a) can be seen by inspection of C (*ASC*) and Algorithm 10. Moreover, Ψ also has property (b). (*SL*, Ψ)-correctness of A(*SL*) follows from the (*SL*, V (*SL*) 0 )-correctness of A(*SL*) and the fact that Ψ ⊆ *Nentry* × *N*, which entails

$$\left\{\Psi \cap \left\{ (\mathbf{s}, t) \mid SL(\mathbf{s}, t) \neq \emptyset \right\} \subseteq \mathrm{N}\_{entry} \times \mathrm{N} \cap \left\{ (\mathbf{s}, t) \mid SL(\mathbf{s}, t) \neq \emptyset \right\} \stackrel{\left(\mathbf{7.27}\right)}{=} \mathcal{V}\_{0}^{(\mathrm{SL})}.\right\}$$

Thus, if (*s*,*t*) ∈ Ψ with π ∈ *SL*(*s*,*t*), then (*s*,*t*) ∈ V(*SL*) 0 and hence, by Theorem 7.18, *f*π ≤ A(*SL*) (*s*, *t*).

A similar argument shows that (*SL*, V (*SL*) 0 )-precision of A(*SL*) implies (*SL*, Ψ)-precision of A(*SL*) for universally distributive frameworks.

Using an appropriate choice of Ψ and assuming that C (*ASC*) 0 is definitioncomplete with respect to C (*ASC*) , I can state the correctness property of Theorem 7.21.

**Theorem 7.21.** *Let XSL* : *N* × *N* → *F*⊠ *be a function and let* C (*ASC*) *the set of constraints in Constraint System 6.2 with respect to XSL. Consider XSL as input for Algorithm 10.*

*1. Algorithm 10 terminates and upon termination, we have*

$$\text{(7.38)}\qquad \mathcal{H}(\mathbf{s},t) = \begin{cases} \text{lfp}(\mathcal{F}\_{\mathcal{C}^{(\text{ASC})}})(\mathbf{s},t) & \text{if } (\mathbf{s},t) \in \mathcal{V}\_0^{(\text{ASC})}\\ \mathbb{B} & \text{otherwise} \end{cases}$$

*2. If XSL is* (*SL*, Ψ)*-correct, then* A *is* (*ASC*, V (*ASC*) 0 )*-correct.*

*3. If XSL is* (*SL*, Ψ)*-precise and* F *is universally distributive, then* A *is* (*ASC*, V (*ASC*) 0 )*-precise.*

In the following, I am going to prove Theorem 7.21. Firstly, I assume that item 1 is proven and consider items 2 and 3. In order to prove item 2, I need to generalize Theorem 6.7: Remember that Theorem 6.7 states that *l f p*(*F* C(*ASC*)) is *ASC*-correct if *XSL* is *SL*-correct. But an inspection of its proof shows that actually (*SL*, Ψ)-correctness of *XSL* is sufficient for the *ASC*-correctness of *l f p*(*F* C(*ASC*)). Hence, the proof of Theorem 6.7 actually shows the following statement:

*If XSL is* (*SL*, Ψ)*-correct, then l f p*(*F* C(*ASC*)) *is* (*ASC*, V (*ASC*) 0 )*-correct.*

With (7.38), this shows item 2. With a similar argument, item 3 can be shown.

Two things are left to be done. In order to complete the proof of Theorem 7.21, I need to show that C (*ASC*) 0 is definition-complete with respect to C (*ASC*) . Moreover, I need to characterize V (*ASC*) 0 appropriately, to be sure that Theorem 7.21 indeed proves Algorithm 10 correct.

Lemma 7.22 gives a characterization of CoreVars(C (*ASC*) , *N* × *N*) and V (*ASC*) 0 . Analogously to Lemma 7.19, it provides a strong connection to *ASC*-reachability. Since C (*ASC*) is defined with respect to *XSL*, Lemma 7.22 has to make additional assumptions about *XSL*. However, for Lemma 7.22 to be valid, full *SL*-correctness or *SL*-precision of *XSL* is not neccessary. It suffices to require that *XSL* ≠ ⊠ for the right points.

**Lemma 7.22.** *Define dom*(*ASC*) *de f* = {(*s*, *t*) ∈ *N* × *N* | *ASC*(*s*, *t*) ≠ ∅}*. Then the following statements are true:*

*1. If XSL is* (*SL*, Ψ)*-domain-correct, then we have*

$$(\mathsf{T}.\mathsf{39})\qquad\qquad\text{dom}(\mathsf{A}\mathsf{SC})\cap\mathsf{S}\mathsf{rc}\times\mathsf{N}\subseteq\mathsf{V}\_{0}^{(\mathsf{A}\mathsf{SC})}$$

**Algorithm 10:** Given a function *XSL* : *N* × *N* → *F*⊠, computes the least ascending solution with respect to *XSL*

**Input:** a data-flow framework instance F = (*G*, *L*, *F*⊠, ρ) as described on page 295, a function *XSL* : *N* × *N* → *F*⊠ **Result:** the least ascending solution with respect to *XSL*, as stated in Theorem 7.21 **1** A ← *const*(⊠) **2 foreach** *s* ∈ *Src* **do 3** A(*s*,*s*) ← *id* **4** *W* ← *W* ∪ {(*s*,*s*)} **5 while** *W* ≠ ∅ **do 6** (*s*, *t* ′ ) ← *remove*(*W*) **7 foreach** *e* ∈ *Eintra* ∪ *Eret such that t*′ *e*→ *t* **do 8** A(*s*, *t*) ← A(*s*, *t*) ⊔ *fe* ◦ A(*s*, *t* ′ ) **9** *W* ← *W* ∪ {(*s*, *t*)} if A(*s*, *t*) has changed **10 foreach** (*ecall*,*eret*) ∈ Φ *such that t* ′ *ecall* → *n*0 ∧ *n*1 *eret* → *t* ∧ *XSL*(*n*0, *n*1 ) ≠ ⊠ **do 11** *sameLevelIn f o* ← *feret* ◦ *XSL*(*n*0, *n*1 ) ◦ *fecall* **12** A(*s*, *t*) ← A(*s*, *t*) ⊔ *sameLevelIn f o* ◦ A(*s*, *t* ′ ) **13** *W* ← *W* ∪ {(*s*, *t* ′ )} if A(*s*, *t*) has changed

$$\text{и } \texttt{return } \mathcal{R}$$

$$(\text{7.40})\qquad\qquad\text{dom}(\text{ASC})\subseteq\text{CoreValues}(\mathcal{C}^{(\text{ASC})}, \mathcal{N}\times\mathcal{N})$$

*2. If XSL is* (*SL*, Ψ)*-domain-precise, then we have*

$$(7.41)\tag{7.41} \qquad \qquad \mathcal{V}\_0^{(\text{ASC})} \subseteq \text{dom}(\text{ASC}) \cap \text{Src} \times N$$

$$(7.42)\qquad \text{CoreVars}(\mathcal{C}^{(ASC)}, N \times N) \subseteq \text{dom}(\text{ASC})$$

$$\text{3. } \mathcal{V}\_0^{(\text{ASC})} \text{ and } \mathsf{CoreValues}(\mathcal{C}^{(\text{ASC})}, \mathsf{N} \times \mathsf{N}) \text{ have the following connection:} $$

$$(7.43)\qquad\mathcal{V}\_0^{(ASC)} = \text{CoreVars}(\mathcal{C}^{(ASC)}, N \times N) \cap \text{Src} \times N.$$

*Proof.* Regarding the first two items, we only show (7.39) and (7.41), since (7.40) and (7.42) can be proven using very similar arguments.

1. Assume that *XSL* is (*SL*, Ψ)-domain-correct. Then (7.39) is implied by the statement

$$(7.44) \quad \forall \pi \in A \text{SC. } \forall (s, t) \in \text{Src} \times \text{N. } \pi \in A \text{SC}(s, t) \implies (s, t) \in \mathcal{V}\_0^{(A \text{SC})}.$$

We prove this statement by induction on π ∈ *ASC*. The proof is largely similar to the corresponding part of the proof of Lemma 7.19. We only highlight the parts where the assumptions about *XSL* are used. Hence, we only consider the case that π = π ′ · *ecall* · π ′′ · *eret* with *n ecall* → *n*0, *n*1 *eret* → *t*, π ′ ∈ *ASC*(*s*, *n*), π ′′ ∈ *SL*(*n*0, *n*1 ) and (*ecall*,*eret*) ∈ Φ. Note that (*n*0, *n*1 ) ∈ Ψ. With the (*SL*, Ψ)-domain-correctness of *XSL* this means that *XSL*(*n*0, *n*1 ) ≠ ⊠. Hence, by asc-sol-(iii), C (*ASC*) contains a constraint

$$X(s, t) \ge f\_{\varepsilon\_{ret}} \circ X(n\_0, n\_1) \circ f\_{\varepsilon\_{call}} \circ X(s, n).$$

By induction hypothesis, we get (*s*, *n*) ∈ V(*ASC*) 0 . We conclude

$$X(s,t) \in \mathcal{V}\_0^{(A\mathcal{SC})}$$

by (V-Base).

2. Assume that *XSL* is (*SL*, Ψ)-domain-precise. In order to show (7.42), we prove

$$(7.45) \qquad \qquad \forall (s, t) \in \mathcal{V}\_0^{(ASC)}.\newline ASC(s, t) \neq \emptyset$$

by induction on (*s*, *t*) ∈ V(*ASC*) 0 = CoreVars(C (*ASC*) , *X* (*ASC*) 0 ). So let (*s*, *t*) ∈ V (*ASC*) 0 . Then there is *c* ∈ C(*ASC*) 0 with *lhs*(*c*) = (*s*,*t*). Because the other cases are similar to the proof of Lemma 7.19, we only consider the case that *c* is of the form

$$X\_{\rm{ASC}}(s, t) \ge f\_{\varepsilon\_{\rm{rel}}} \circ X\_{\rm{SL}}(n\_0, n\_1) \circ f\_{\varepsilon\_{\rm{call}}} \circ X\_{\rm{ASC}}(s, n)$$

with (*ecall*,*eret*) ∈ Φ, *n ecall* → *n*0, *n*1 *eret* → *t* and *XSL*(*n*0, *n*1 ) ≠ ⊠. Then we have (*n*0, *n*1 ) ∈ Ψ. Since *XSL* is (*SL*, Ψ)-domain-precise, *XSL*(*n*0, *n*1 ) ≠ ⊠ implies that there is π ′′ ∈ *SL*(*n*0, *n*1 ). Furthermore, we may apply the induction hypothesis to (*s*, *n*) and get π ′ ∈ *ASC*(*s*, *n*). Together with the assumptions about *ecall* and *eret*, we get π ′ ·*ecall* · π ′′ ·*eret* ∈ *ASC*(*s*, *t*), as desired.

	- For ⊆, it is clear that

$$\mathcal{V}\_0^{(A\text{SC})} \subseteq \text{CoreVars}(\mathcal{C}^{(A\text{SC})}, N \times N)\_{\prime \prime}$$

since *Src* × *N* ⊆ *N* × *N* and CoreVars(C (*ASC*) , \_) is monotone.

It remains to show

$$\forall (\mathbf{s}, t) \in \mathcal{V}\_0^{(A \mathbf{S} \mathbf{C})}. (\mathbf{s}, t) \in \mathbf{S} \mathbf{c} \times \mathbf{N}.$$

The proof is a straight-forward induction along V (*ASC*) 0 , where the induction steps work by noticing that the first components of the variables on the left-hand and right-hand sides of constraints in V (*ASC*) 0 are the same.

• For ⊇, induction on (*s*, *t*) ∈ CoreVars(C (*ASC*) , *N* × *N*) shows that

$$\begin{aligned} \mathsf{V}(s,t) \in \mathsf{CoreVars}(\mathsf{C}^{(\text{ASC})}, \mathsf{N} \times \mathsf{N}). \ (s,t) \in \mathsf{Src} \times \mathsf{N} \\ \implies (s,t) \in \mathsf{V}\_0^{(\text{ASC})}. \end{aligned}$$

□

With Lemma 7.22, I can provide the last puzzle piece to the proof of Theorem 7.21: The definition-completeness of C (*ASC*) 0 with respect to Core(C (*ASC*) , *N* × *N*).

**Lemma 7.23.** C (*ASC*) 0 *is definition-complete with respect to its superset*

$$\text{Core}(\mathcal{C}^{(A\mathcal{C})}, \mathcal{N} \times \mathcal{N})\text{.}$$

*Proof.* Like in the proof of Lemma 7.20, we use Theorem 7.10. Consider *c* ∈ Core(C (*ASC*) , *N* × *N*) with (*s*,*t*) = *lhs*(*c*) ∈ V(*ASC*) 0 . Then we have to show

$$(7.46)\newline\qquad FV(rhs(c)) = \emptyset \implies (s,t) \in X\_{0}^{(ASC)}$$

$$(7.47) \quad (s', t') \in FV(rhs(c)) \implies (s', t') \in \text{CoreVars}(\mathcal{C}^{(\text{ASC})}, X\_0^{(\text{ASC})})$$

As the other cases are very similar, we only consider the case that *c* ∈ Core(C (*ASC*) , *N* × *N*) is of the form

$$X\_{\rm ASC}(s, t) \ge f\_{\varepsilon\_{\rm ret}} \circ X\_{\rm SL}(n\_0, n\_1) \circ f\_{\varepsilon\_{\rm call}} \circ X\_{\rm ASC}(s, n)$$

with (*ecall*,*eret*) ∈ Φ, *n ecall* → *n*0, *n*1 *eret* → *t*, *XSL*(*n*0, *n*1 ) ≠ ⊠, and (*s*,*t*) ∈ CoreVars(C (*ASC*) , *X* (*ASC*) 0 ). We need to show

$$(s, n) \in \text{CoreVars}(\mathcal{C}^{(A\text{SC})}, X\_0^{(A\text{SC})}) .$$

But note that

(*s*, *n*) ∈ CoreVars(C (*ASC*) , *N* × *N*), and(1)

*s* ∈ *Src*.(2)

Statement (1) is implied by *c* ∈ Core(C (*ASC*) , *N* × *N*), while statement (2) follows, by application of Lemma 7.22, from (*s*,*t*) ∈ V(*ASC*) 0 . Both statements together imply (*s*, *n*) ∈ V(*ASC*) 0 by Lemma 7.22. □

# **7.3.3 Extending the Solution Along the Non-Ascending Paths**

Constraint System 7.1 is a modified version of Constraint System 6.3 that describes the data flows along the non-ascending paths.

The constant constraints of Constraint System 7.1 use the values *XASC*(*s*, *c*) with *XASC*(*s*, *c*) ≠ ⊠ to initialize the solution. Note that *c* can be restricted to *Ncall* according to Lemma 7.16. The non-constant constraints then extend the solution along the descending paths.

**Constraint System 7.1.** *Given functions XASC*, *XSL* : *N* × *N* → *F*⊠*, the function*

$$\chi\_{\text{NASC}} : N \times N \to F\_{\mathbf{E}}$$

*is a* non-ascending solution *with respect to XASC and XSL if it satisfies all constraints from the following system:*

$$\begin{aligned} \text{(\text{NON-ASC-(t)})} & \frac{t' \xrightarrow{\varepsilon} t \qquad e \in E\_{\text{call}} & X\_{\text{ASC}}(s, t') \neq \mathtt{E}}{X\_{\text{NASC}}(s, t) \ge f\_{\varepsilon} \circ X\_{\text{ASC}}(s, t')} \\\\ & \text{(\text{NON-asc-(n)})} \frac{t' \xrightarrow{\varepsilon} t \qquad e \in E\_{\text{intrta}} \cup E\_{\text{call}}}{X\_{\text{NASC}}(s, t) \ge f\_{\varepsilon} \circ X\_{\text{NASC}}(s, t')} \end{aligned}$$

$$\varepsilon\_{\text{call}} \qquad \varepsilon\_{\text{ret}, \varepsilon\_{\text{act}}}(\varepsilon\_{\text{act}}, \varepsilon\_{\text{act}}, \varepsilon\_{\text{act}}, \varepsilon\_{\text{act}})$$

$$\left(\text{(non-asc-(un))}\right) \frac{n \stackrel{\mathcal{e\_{call}}}{\rightarrow} n\_0}{\text{X}\_{\text{NASC}}(s, t) \ge f\_{\mathcal{E}\_{\text{rt}}} \circ \text{X}\_{\text{SL}}(n\_0, n\_1) \circ \mathbb{1}} \left(\text{>} \frac{1}{n}\right) \to \mathbb{1}$$

Using a similar argument as in Theorem 6.7, I can prove that Constraint System 7.1 indeed describes *NASC*-correct solutions, provided that *XSL* and *XASC* enjoy their respective correctness properties.

**Theorem 7.24.** *Let XSL* : *N* × *N* → *F*⊠ *be SL-correct, XASC* : *N* × *N* → *F*⊠ *be ASC-correct and let XNASC be a NASC-solution with respect to XSL and XASC. Then XNASC is NASC-correct.*

*Proof.* Let *s* ∈ *N*, *c* ∈ *Ncall* and π1 ∈ *ASC*(*s*, *c*). Using a straight-forward induction along π2 ∈ *DESC* with arguments similar to the ones in the proof of, e.g., Theorem 6.6, we show

$$\begin{aligned} \forall \pi\_2 \in \text{DECC. } \forall t \in \mathsf{N}. \\ \pi\_2 \in \text{DECC}(\mathsf{c}, t) \land \pi\_1 \cdot \pi\_2 \notin \text{ASC}(\mathsf{s}, t) \\ \implies f\_{\pi\_1 \cdot \pi\_2} \le \mathsf{X}\_{\text{NASC}}(\mathsf{s}, t). \end{aligned}$$

Using Definition 7.15, this shows that

$$\forall \pi \in \text{NASC}. \,\forall s, t \in \text{N}. \pi \in \text{NASC}(s, t) \implies f\_{\pi} \le \text{X}\_{\text{NASC}}(s, t)\_{\prime t}$$

as desired. □

Moreover, for universally distributive frameworks and with the respective precision requirements satisfied for *XASC* and *XSL*, the least solution of Constraint System 7.1 coincides with *MONASC*. The proof is very similar to the proof of Theorem 6.10 and is not repeated here.

**Algorithm 11:** computes the least non-ascending solution on

```
V
  (NASC)
  0
         with respect to XASC and XSL
```

```
Input: a data-flow framework instance F = (G, L, F⊠, ρ) as de-
         scribed on page 295, functions XSL, XASC : N × N → F⊠
  Result: the least non-ascending solution with respect to XSL, as
          stated in Theorem 7.26
1 A ← const(⊠)
2 foreach (s, c) ∈ Src × N with XASC(s, c) ≠ ⊠ do
3 foreach e ∈ Ecall, t ∈ N such that c e→ t do
4 A(s, t) ← A(s, t) ⊔ fe ◦ XASC(s, c)
5 W ← W ∪ {(s, t)}
6 while W ≠ ∅ do
7 (s, t) ← remove(W)
8 foreach e ∈ Eintra ∪ Ecall such that t e→ t
                                            ′ do
9 A(s, t
               ′
                ) ← A(s, t
                          ′
                           ) ⊔ fe ◦ A(s, t)
10 W ← W ∪ {(s, t
                        ′
                         )} if A(s, t
                                   ′
                                    ) has changed
11 foreach (ecall,eret) ∈ Φ such that t
                                          ecall → n0 ∧ n1
                                                       eret → t
                                                            ′ ∧
       XSL(n0, n1
                 ) ≠ ⊠ do
12 sumIn f o ← feret ◦ XSL(n0, n1
                                     ) ◦ fecall
13 A(s, t
               ′
                ) ← A(s, t
                          ′
                           ) ⊔ sumIn f o ◦ A(s, t)
14 W ← W ∪ {(s, t
                        ′
                         )} if A(s, t
                                   ′
                                    ) has changed
15 return A
```
**Theorem 7.25.** *Let* F *be universally distributive. Furthermore, let XSL be SL-precise and XASC be ASC-precise. Then* MO*NASC is a NASC-solution with respect to XSL and XASC. In particular, l f p*(*F*C*NASC*) *is NASC-precise, if* C*NASC is defined with respect to XASC and XSL.*

All that remains to do is to instantiate Algorithm 8 appropriately and prove the usual correctness result. The instantiation can be seen in Algorithm 11. I fix two functions

$$X\_{A \to \prime} X\_{SL} : N \times N \to F\_{\mathbb{E} \mathcal{A}}$$

and let C (*NASC*) be the set of constraints defined by Constraint System 7.1, with respect to *XSL* and *XASC*. I define

$$(7.48)\qquad X\_0^{(NASC)} \stackrel{def}{=} \{ (\text{s.c}) \mid \text{s} \in \text{Src} \land \text{c} \in \text{N}\_{\text{call}} \land X\_{A \text{SC}}(\text{s}, \text{c}) \neq \text{B} \}$$

$$(7.49)\qquad \mathcal{C}\_0^{(NASC)} \stackrel{def}{=} \text{Core}(\mathcal{C}^{(NASC)}, X\_0^{(ASC)})^\dagger$$

V (*NASC*) 0 *de f* = CoreVars(C (*NASC*) , *X* (*ASC*) 0 (7.50) )

Like before, an inspection of Constraint System 7.1 shows that Algorithm 11 is indeed an instance of Algorithm 8. Thus, assuming definitioncompleteness of C (*NASC*) 0 in Core(C (*NASC*) , *N* × *N*), I can give the following correctness result for Algorithm 11.

**Theorem 7.26.** *Let XSL*, *XASC* : *N* × *N* → *F*⊠ *be two functions and let* C*NASC be the instance of Constraint System 7.1 with respect to XSL and XASC. Consider XSL and XASC as input for Algorithm 11.*

*1. Algorithm 11 terminates and upon termination, we have*

$$\text{(7.51)}\qquad \mathcal{A}(\mathbf{s},t) = \begin{cases} lfp(\mathcal{F}\_{\mathcal{C}\_{\text{NASC}}})(\mathbf{s},t) & \text{if } \mathbf{s} \in \mathcal{V}\_0^{(\text{NASC})}\\ \boxtimes & \text{otherwise.} \end{cases}$$

*2. If XSL is* (*SL*, Ψ)*-correct and XASC is* (*ASC*, *Src* × *N*)*-correct, then* A *is* (*NASC*, V (*NASC*) 0 )*-correct.*

*3. If* F⊠ *is u.d., XSL is* (*SL*, Ψ)*-precise, and XASC is* (*ASC*, *Src* × *N*)*-precise, then* A *is* (*NASC*, V (*NASC*) 0 )*-precise.*

In the following, I sketch a proof for Theorem 7.26. First, assume that the first item is shown. Then the second item follows if I can show that *l f p*(*F* C(*NASC*)) is (*NASC*, V (*NASC*) 0 )-correct. But this can be concluded from the (*SL*, Ψ)-correctness of *XSL* and the (*ASC*, *Src* × *N*)-correctness of *XASC* with a similar argument as in the proof of Constraint System 7.1.

The third item in Theorem 7.26 can be shown similarly by adapting Theorem 7.25 appropriately.

It remains to characterize the variableV (*NASC*) 0 and to prove the definition-completeness of C (*NASC*) 0 in Core(C (*NASC*) , *N* × *N*). Lemma 7.27 gives a characterization of V (*NASC*) 0 that is analogous to Lemma 7.22.

**Lemma 7.27.** *Define dom*(*NASC*) *de f* = {(*s*, *t*) ∈ *N* × *N* | *NASC*(*s*, *t*) ≠ ∅}*. Then the following statements are true:*

*1. If XSL is*(*SL*, Ψ)*-domain-correct and XASC is*(*ASC*, *Src*×*N*)*-domain-correct, then we have*

$$(7.52) \qquad dom(\text{NASC}) \cap \text{Src} \times \text{N} \subseteq \mathcal{V}\_0^{(\text{NASC})}$$

*dom*(*NASC*) ⊆ CoreVars(C (*NASC*) (7.53) , *N* × *N*)

*2. If XSL is* (*SL*, Ψ)*-domain-precise and XASC is* (*ASC*, *Src*×*N*)*-domain-precise, then we have*

$$(7.54) \qquad \qquad \mathcal{V}\_0^{(NASC)} \subseteq dom(NASC) \cap src \times N$$

$$(7.55)\qquad \text{CoreVars}(\mathcal{C}^{(NASC)}, N \times N) \subseteq dom(\text{NASC})$$

$$\text{3. } \mathcal{V}\_0^{(\text{NASC})} \text{ and } \text{CoreVars}(\mathcal{C}^{(\text{NASC})}, \text{N} \times \text{N}) \text{ have the following connection:} $$

$$(7.56)\qquad \mathcal{V}\_0^{(NASC)} = \text{CoreVars}(\mathcal{C}^{(NASC)}, N \times N) \cap \text{Src} \times N.$$

*Proof.* 1. We only consider (7.52), since the proof of (7.53) is very similar. Assume that *XSL* is (*SL*, Ψ)-domain-correct and that *XASC* is (*ASC*, *Src*×*N*) domain-correct. Let *s*, *c* ∈ *N* and π1 ∈ *ASC*(*s*, *c*). Then, we can show

$$\begin{aligned} \forall \pi\_2 \in \text{DECC. } \forall t \in \text{N. } \pi\_2 \in \text{DECC}(c, t) \land \pi\_1 \cdot \pi\_2 \notin \text{ASC}(s, t) \\ \implies (s, t) \in \mathcal{V}\_0^{(\text{NASC})} \end{aligned}$$

by induction on π2 ∈ *DESC*. The details are very similar to the corresponding part of the proof of Lemma 7.22 and are omitted here. By Definition 7.15, this implies (7.52).

2. Assume that *XSL* is (*SL*, Ψ)-domain-precise and, moreover, that *XASC* is (*ASC*, *Src* × *N*)-domain-precise. Then we can show

$$\forall (\mathbf{s}, t) \in \mathcal{V}\_0^{(\text{NASC})} . (\mathbf{s}, t) \in dom(\text{NASC}) \cap \mathbf{Src} \times \mathbf{N}$$

by induction on (*s*,*t*) ∈ V(*NASC*) 0 . For each case, the argument uses a combination of the respective induction hypothesis and the assumptions about *XSL* and *XASC* to obtain an appropriate non-ascending path. The details are very similar to Lemma 7.22 and I do not repeat them here. The proof of (7.54) is similar.

3. This is completely analogous to the proof of (7.43).

Using Lemma 7.27, the definition-completeness of C (*NASC*) 0 with respect to its superset Core(C (*NASC*) , *N* × *N*) can be shown. The proof is completely analogous to the proofs of Lemma 7.23 and Lemma 7.20 and is omitted here.

□

**Lemma 7.28.** Core(C (*ASC*) , *X*0) *is definition-complete with respect to its superset* Core(C*NASC*, *N* × *N*)*.*

# **7.3.4 Combining the Ascending Solution and the Non-Ascending Solution**

Constraint System 7.2 combines two given functions *XASC* and *XNASC* by simply joining them.

**Constraint System 7.2.** *Given functions XASC*, *XNASC* : *N* × *N* → *F*⊠*, the function*

$$X\_{VP'}: N \times N \to F\_{\mathbb{E}}$$

*is an* alternative valid-paths-solution *with respect to XASC and XNASC if it satisfies all constraints from the following system:*

$$\left(\text{vp}\,'\text{-(t)}\right)\,\frac{\text{X}\_{\text{ASC}}(\text{s},t)\neq\mathbb{B}}{\text{X}\_{\text{VP}'}(\text{s},t)\geq\text{X}\_{\text{ASC}}(\text{s},t)}\qquad\left(\text{vp}\,'\text{-(tu)}\right)\,\frac{\text{X}\_{\text{NASC}}(\text{s},t)\neq\mathbb{B}}{\text{X}\_{\text{VP}'}(\text{s},t)\geq\text{X}\_{\text{NASC}}(\text{s},t)}$$

Constraint System 7.2 is so simple that I can give a clear and direct characterization of *l f p*(*F* C(*VP*′)), which is easy to see:

$$\text{(7.57)}\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\text{!}\\fp(F\_{C^{(VP')}}) = X\_{A\text{SC}} \sqcup X\_{NA\text{SC}}.$$

Alternative valid-paths solutions are indeed *VP*-correct, if *XASC* and *XDESC* satisfy their respective correctness conditions. This is an easy consequence of Remark 7.17, which is why I omit the proof.

**Theorem 7.29.** *Let XASC*, *XNASC* : *N* × *N* → *F*⊠ *be two functions. Then the following statements hold:*

*1. Let XVP*′ *be an alternative valid-paths solution with respect to XASC and XNASC. If XASC is ASC-correct and XNASC is NASC-correct, then XVP*′ *is VP-correct.*

*2. If XASC is ASC-precise and XNASC is NASC-precise, then l f p*(*F*C*VP*′ ) *is VP-precise.*

In chapter 6, we considered Constraint System 6.4 as a characterization for valid-paths solutions. For the following considerations, let C (*VP*) be the set of constraints from Constraint System 6.4.

Note that Theorem 7.29 does not say anything about the relation of *l f p*(*F* C(*VP*)) and *l f p*(*F* C(*VP*′)) in general, even if they are considered with respect to the same helper solutions. As C (*VP*) and C (*VP*′ ) make different choices about when they join and when they compose, we cannot expect in general that they coincide36. In general, C (*VP*) and C (*VP*′ ) can simply be seen as alternative approaches to characterize an over-approximation to *MOVP*. This is especially relevant if F is not distributive and the helper solutions are correct and as precise as possible (e.g. if they were obtained using the algorithms from the previous sections), but also if the helper solutions themselves are only over-approximations, even for the distributive case.

36My conjecture is (a) that *l f p*(*F*C(*VP*) ) ≤ *l f p*(*F*C(*VP*′) ) under relatively general assumptions and (b) that, under the same assumptions, there are examples for which *l f p*(*F*C(*VP*′) ) ̸≤ *l f p*(*F*C(*VP*) ), since C (*VP*) "joins later" than C (*VP*′ ) . I will however not attempt to prove this within the scope of this thesis.

For distributive frameworks and the most precise helper solutions, *l f p*(*F* C(*VP*′)) can be shown to coincide with *l f p*(*F* C(*VP*)).

**Corollary 7.30.** *Assume that* F *is universally-distributive. Consider the following constraint systems:*

$$\begin{aligned} &\mathcal{C}^{(ASC)} \text{ with respect to } lfp(\mathcal{F}\_{\mathcal{C}^{(SL)}})\\ &\mathcal{C}^{(DESC)} \text{ with respect to } lfp(\mathcal{F}\_{\mathcal{C}^{(SL)}})\\ &\mathcal{C}^{(NASC)} \text{ with respect to } lfp(\mathcal{F}\_{\mathcal{C}^{(SL)}}) \text{ and } lfp(\mathcal{F}\_{\mathcal{C}^{(ASC)}})\\ &\mathcal{C}^{(VP)} \text{ with respect to } lfp(\mathcal{F}\_{\mathcal{C}^{(ASC)}}) \text{ and } lfp(\mathcal{F}\_{\mathcal{C}^{(DESC)}}), \text{and}\\ &\mathcal{C}^{(VP')} \text{ with respect to } lfp(\mathcal{F}\_{\mathcal{C}^{(ASC)}}) \text{ and } lfp(\mathcal{F}\_{\mathcal{C}^{(NASC)}}). \end{aligned}$$

*Then l f p*(*F* C(*VP*)) = *l f p*(*F* C(*VP*′))*.*

*Proof.* By Theorem 6.7 and Theorem 6.10, *l f p*(*F* C(*ASC*)) is both *ASC*-correct and *ASC*-precise. Moreover, Theorem 7.24 and Theorem 7.25 imply that *l f p*(*F* C(*NASC*)) is both *NASC*-correct and *NASC*-precise. Hence, Theorem 7.29 implies that *l f p*(*F* C(*VP*′)) is both *VP*-correct and *VP*-precise, i.e.

$$lfp(F\_{\mathcal{C}^{(VP')}}) = MOVP.$$

Analogously, using Theorem 6.7, Theorem 6.8, Theorem 6.10 and Theorem 6.9, one can conclude

$$lfp(F\_{\mathcal{C}^{(VP)}}) = MOVP.$$

□

Lastly, I want to consider the connection between the domain of *l f p*(*F*C*VP*′ ) and forward slices. Remember that the forward slice *FS*(*s*) of a given node *s* ∈ *N* is the set of nodes *t* ∈ *N* such that *VP*(*s*, *t*) ≠ ∅.

**Theorem 7.31.** *Let XASC*, *XNASC* : *N* × *N* → *F*⊠ *be two functions. Then the following statements hold:*

*1. Let XVP*′ *be an alternative valid-paths solution with respect to XASC and XNASC. If XASC is ASC-domain-correct and XNASC is NASC-domain-correct, then XVP*′ *is VP-domain-correct. In particular, we have*

(7.58) ∀*s* ∈ *N*. *FS*(*s*) ⊆ {*t* ∈ *N* | *l f p*(*F*C*VP*′ )(*s*, *t*) ≠ ⊠}.

*2. If XASC is ASC-domain-precise and XNASC is NASC-domain-precise, then l f p*(*F*C*VP*′ ) *is VP-domain-precise. In particular, we have*

$$(7.59) \qquad \forall s \in N. \ (t \in N \mid lfp(F\_{C\_{VP'}})(s, t) \neq \mathbb{B}) \subseteq FS(s).$$

*Proof.* For given *s* ∈ *N*, we define

$$\begin{aligned} \text{FS}\_{\text{ASC}}(\mathbf{s}) & \stackrel{def}{=} \{ t \in \mathbb{N} \mid \text{ASC}(\mathbf{s}, t) \neq \emptyset \}, \text{ and} \\ \text{FS}\_{\text{NASC}}(\mathbf{s}) & \stackrel{def}{=} \{ t \in \mathbb{N} \mid \text{NASC}(\mathbf{s}, t) \neq \emptyset \}. \end{aligned}$$

By Lemma 7.16, we have *FS*(*s*) = *FSASC*(*s*) ∪ *FSNASC*(*s*) for all *s* ∈ *N*. Moreover, by definition we have

From this, all claimed statements can be shown using (7.57). □

# **7.3.5 Putting It All Together**

In this section, I combine the algorithms from the previous sections to yield algorithms that compute the least alternative valid-paths solution with the most precise helper solutions.

First, I show a simple algorithm that is always correct and then I consider a variant that works for distributive frameworks.

The simple approach, which can be seen in Algorithm 12, takes the set *Src* ⊆ *N* of source nodes as input and uses the pre-computed result A(*SL*) of running Algorithm 9 on *X* (*SL*) 0 .

As its first step, Algorithm 12 invokes Algorithm 10 to compute the least ascending-paths solution A(*ASC*) with respect to A(*SL*) . After that, it runs Algorithm 11 to obtain the least non-ascending solution A(*NASC*) with respect to A(*SL*) and A(*ASC*) . Finally, it joins A(*ASC*) and A(*NASC*) to obtain its result A(*VP*′ ) .

For Algorithm 12 I can give the following simple correctness result.

**Theorem 7.32.** *Consider*

$$\begin{aligned} & \mathcal{C}^{(VP')} \text{ with respect to } lfp(\mathcal{C}^{(ASC)}) \text{ and } lfp(\mathcal{C}^{(NASC)})\\ & \mathcal{C}^{(NASC)} \text{ with respect to } lfp(\mathcal{C}^{(ASC)}) \text{ and } lfp(\mathcal{C}^{(SL)}), and\\ & lfp(\mathcal{C}^{(ASC)}) \text{ with respect to } lfp(\mathcal{C}^{(SL)}). \end{aligned}$$

*Then Algorithm 12 has the following properties:*

*1. Algorithm 12 always terminates and upon termination, we have*

$$(\mathsf{T}.60)\qquad\mathscr{A}^{(VP')}(\mathsf{s},t) = \begin{cases} \mathit{lfp}(\mathsf{F}\_{\mathscr{C}^{(VP')}})(\mathsf{s},t) & \mbox{if } t \in \mathsf{V}\_{0}^{(A\mathcal{C})} \cup \mathsf{V}\_{0}^{(NASC)}\\ \mathsf{B} & \mbox{otherwise} \end{cases}$$

*2. Define F de f* = ⋃ *s*∈*Src FS*(*s*)*. If* F *is universally distributive, then*

$$\text{(7.61)}\tag{7.61} = \text{ } \space \text{//}\space \text{V}^{\prime P^{\prime}}\text{)}=\_{\text{F}}\text{ MOVP.}$$

**Algorithm 12:** Computes the least alternative valid-paths solution on *Src* × *N* with respect to the most precise helper functions

**Input:** a data-flow framework instance F = (*G*, *L*, *F*⊠, ρ) as described on page 295, least same-level solution A(*SL*) , node set *Src* ⊆ *N*

**Result:** least alternative valid-paths solution, as stated in Theorem 7.32

**1** A(*ASC*) ← *ComputeAscendingSolution*(*Src*, A(*SL*) )

$$\text{2. } \mathcal{R}^{(\text{NASC})}\_{\text{........}} \leftarrow \text{ComputeNonAscending Solution} (\mathcal{R}^{(\text{SL})}, \mathcal{R}^{(\text{ASC})})$$

$$\text{a. } \mathcal{H}^{(VP')} \leftarrow \mathcal{H}^{(AS\dot{C})}\_{\cdot} \sqcup \mathcal{H}^{(DESC)}$$

$$\mathfrak{a} \text{ течип } \mathcal{R}^{(VP')}$$

*Proof.* 1. (7.60) is an easy consequence of (7.57), considering the final value of A(*VP*′ ) in Algorithm 12.

2. Assume that F is universally distributive. Then (7.61) is an easy consequence of

*l f p*(*F* C(*VP*′)) = *MOVP*, and(7.62)

$$(7.63) \qquad \qquad \mathcal{V}\_0^{(ASC)} \cup \mathcal{V}\_0^{(NASC)} = \bigcup\_{s \in Scc} FS(s).$$

These two facts follow from the universal distributivity of F , Theorem 7.29 and Theorem 7.31.

□

# **7.3.6 Towards the Two-Phase Slicer**

Remember that Algorithm 6 works in two phases: The first visits all nodes that are *ASC*-reachable from the given start nodes. It uses summary edges to skip call edges and instead collects the call nodes on a second worklist *W*2. The second phase starts with *W*2 and extends the set of visited nodes along the descending paths of the given graph, using summary edges to skip return edges.

I can employ this pattern in my more general setting. The result is Algorithm 13, a variant of Algorithm 12 that integrates the two main steps of Algorithm 12 and offers large similarities to Algorithm 6. This variant also computes the alternative valid-paths solution on the forward slice of *Src*, provided that the given framework F is distributive.

Like Algorithm 12, Algorithm 13 proceeds in two steps.

The first step, which is implemented by Algorithm 14, is a variant of Algorithm 10 that computes the least ascending solution A(*ASC*) with respect to the pre-computed least same-level solution and additionally collects all (*s*, *c*) ∈ *Src* × *Ncall* such that *ASC*(*s*, *c*) ≠ ∅ in a set *W*2, which it also returns. It can easily be verified that Algorithm 14 has the same properties as Algorithm 10 but additionally has the property that, upon termination, *W*2 contains the set of *all* (*s*, *c*) ∈ *Src* × *N* such that *c* ∈ *Ncall* and *ASC*(*s*, *c*) ≠ ∅.

The second step, which is implemented by Algorithm 15, then takes A(*ASC*) and *W*2 and executes a variant of Algorithm 11. Algorithm 15 differs from **Algorithm 13:** Computes the least alternative valid-paths solution on *Src* × *N* with respect to the most precise helper functions

Algorithm 11 in two key aspects: Firstly, it does not initialize the solution with *const*(⊠), but rather initializes it with A(*ASC*) and secondly, it does not have an initial loop. However, it also starts with a non-empty worklist that, by the additional correctness property of Algorithm 15, contains all (*s*, *c*) ∈ *Src* × *N* such that *n* ∈ *Ncall* and *ASC*(*s*, *c*) ≠ ⊠. It can be verified that the initial loop is actually integrated in the main loop.

Assuming the distributivity of F , we can show that Algorithm 15 indeed computes *l f p*(C*VP*′). The proof is analogous to the proof of Theorem 7.11 and proceeds in three steps, which I state here but omit the proofs.

$$\{(s,t)\in \mathcal{S}rc \times N \mid \mathcal{A}^{(VP')}(s,t) \neq \mathbb{B}\} \subseteq \mathcal{V}\_0^{(A\mathcal{SC})} \cup \mathcal{V}\_0^{(NA\mathcal{SC})}$$

and upon termination, we have

$$\{(\mathbf{s},t)\in \mathbf{S}\mathbf{r}\mathbf{c}\times\mathbf{N} \mid \mathcal{A}^{(VP')}(\mathbf{s},t)\neq\mathbf{s}\} = \mathcal{V}\_0^{(A\mathbf{S}\mathbf{C})} \cup \mathcal{V}\_0^{(NA\mathbf{C})}$$

3. Algorithm 15 maintains the invariant

$$\mathcal{H}^{(VP')} \le lfp(F\_{\mathcal{C}^{(ASC)}}) \sqcup lfp(F\_{\mathcal{C}^{(NASC)}}),$$

and upon termination, we have

$$\mathcal{R}^{(VP')} = \operatorname{lfp}(\mathcal{F}\_{\mathcal{C}^{(A\text{SC})}}) \sqcup \operatorname{lfp}(\mathcal{F}\_{\mathcal{C}^{(NA\text{SC})}}) = \operatorname{lfp}(\mathcal{F}\_{\mathcal{C}^{(VP')}}) . $$

322

The invariant in the last step actually uses the distributivity of F . My conjecture, which I will not prove within the scope of this thesis is that (a) Algorithm 13 always computes an over-approximation *l f p*(C*VP*′) and that (b) there are non-distributive frameworks for which A(*VP*′ ) > *l f p*(C*VP*′).

# **7.4 Call-String Approach**

This section is dedicated to computing a *VP*-correct solution using a callstring-based constraint system. The general pattern is the same as in the

**Algorithm 14:** Implementation of ComputeAscendingSolution' **Input:** a data-flow framework instance F = (*G*, *L*, *F*⊠, ρ) as described on page 295, least same-level solution A(*SL*) , node set *Src* ⊆ *N* **Result:** Ascending solution A set *W*2 ⊆ *Src* × *N* such that (*s*, *n*) ∈ *W*2 implies that *n* ∈ *Ncall* and *n* is *ASC*-reachable from *Src* **1** A ← *const*(⊠) **2 foreach** *s* ∈ *Src* **do 3** A(*s*,*s*) ← *id* **4** *W* ← *W* ∪ {(*s*,*s*)} **5 while** *W* ≠ ∅ **do 6** (*s*, *t* ′ ) ← *remove*(*W*) **7 foreach** *e* ∈ *Eintra* ∪ *Eret such that t*′ *e*→ *t* **do 8** A(*s*, *t*) ← A(*s*, *t*) ⊔ *fe* ◦ A(*s*, *t* ′ ) **9** *W* ← *W* ∪ {(*s*, *t*)} if A(*s*, *t*) has changed **10 foreach** (*ecall*,*eret*) ∈ Φ *such that t* ′ *ecall* → *n*0 ∧ *n*1 *eret* → *t* ∧ *XSL*(*n*0, *n*1 ) ≠ ⊠ **do 11** *sumIn f o* ← *feret* ◦ *XSL*(*n*0, *n*1 ) ◦ *fecall* **12** A(*s*, *t*) ← A(*s*, *t*) ⊔ *sumIn f o* ◦ A(*s*, *t* ′ ) **13** *W*2 ← *W*2 ∪ {(*s*, *t* ′ )} **14** *W* ← *W* ∪ {(*s*, *t* ′ )} if A(*s*, *t*) has changed **15 return** A

**Algorithm 15:** Implementation of ExtendAlongNonAscSolution'

```
Input: a data-flow framework instance F = (G, L, F⊠, ρ) as
          described on page 295, least same-level solution A(SL)
                                                                    ,
          node set Src ⊆ N, ascending solution A(ASC)
                                                         , set W of call
          nodes that are ASC-reachable from Src
  Result: alternative valid-paths solution A(VP′
                                                   )
1 A(VP′
         ) ← A(ASC)
2 while W ≠ ∅ do
3 (s, t) ← remove(W)
4 foreach e ∈ Eintra ∪ Ecall such that t e→ t
                                              ′ do
 5 A(VP′
                )
                 (s, t
                     ′
                      ) ← A(VP′
                                 )
                                  (s, t
                                     ′
                                      ) ⊔ fe ◦ A(VP′
                                                    )
                                                     (s, t)
 6 W ← W ∪ {(s, t
                         ′
                          )} if A(VP′
                                     )
                                      (s, t
                                          ′
                                          ) has changed
7 foreach (ecall,eret) ∈ Φ such that t
                                           ecall → n0 ∧ n1
                                                         eret → t
                                                              ′ ∧
       XSL(n0, n1
                  ) ≠ ⊠ do
 8 sumIn f o ← feret ◦ XSL(n0, n1
                                       ) ◦ fecall
 9 A(VP′
                )
                 (s, t
                     ′
                      ) ← A(VP′
                                 )
                                  (s, t
                                     ′
                                      ) ⊔ sumIn f o ◦ A(VP′
                                                           )
                                                            (s, t)
10 W ← W ∪ {(s, t
                         ′
                          )} if A(VP′
                                     )
                                      (s, t
                                          ′
                                          ) has changed
11 return A(VP′
                )
```
last sections. First, I am going to instantiate Algorithm 8 so that it solves a sufficient portion of Constraint System 6.5. After that, I will state an appropriate instance of Theorem 7.11. Lastly, I give a characterize the core variables of the subsystem solved by the algorithm and convince myself that the algorithm indeed solves a definition-complete subsystem.

I fix a stack space S = (*Ecall*, *S*, ≤, ϵ, *push*, *pop*, *top*) such that *S* is finite. The finiteness of *S* ensures that the complete lattice

$$N \times N \times S \to\_{mon} F\_{\boxtimes}$$

satisfies the ascending chain condition.

Before I am able to instantiate Algorithm 8 to compute the least solution of Constraint System 6.5, I need to modify Constraint System 6.5 a bit: In Algorithm 8, constraints are applied by updating the left-hand sides for given updated right-hand sides. However, Constraint System 6.5 does not present all constraints in such a form. Particularly, ret (2) S needs to be transformed.

The ret (2) S -constraints have the form

$$(\mathsf{nerr}\_{\mathcal{S}}^{(2)}) \xrightarrow{\mathsf{t}' \xrightarrow{\mathcal{C}\_{\text{ret}}} \mathsf{t} \ (\mathsf{e}\_{\text{call}}, \mathsf{e}\_{\text{ret}}) \in \mathsf{\Phi} \ \mathsf{pop}(\mathsf{push}(\mathsf{e}\_{\text{call}}, \sigma)) = \sigma \ \mathsf{push}(\mathsf{e}\_{\text{call}}, \sigma) \neq \mathsf{e}\_{\text{set}} }$$

$$\underline{\mathcal{X}\_{\mathcal{S}}(\mathsf{s}, \mathsf{t}, \sigma) \ge f\_{\mathsf{cret}} \circ \underline{\mathcal{X}\_{\mathcal{S}}(\mathsf{s}, \mathsf{t}', \texttt{push}(\mathsf{e}\_{\text{call}}, \sigma))}$$

I fix *ecall* ∈ *Ecall* and consider the following two sets:

$$\begin{aligned} A &= \{ (\sigma, push(e\_{call}, \sigma)) \mid \sigma \in \mathcal{S} \\ &\qquad \land pop(push(e\_{call}, \sigma)) = \sigma \\ &\qquad \land push(e\_{call}, \sigma) \neq \epsilon \} \\ B &= \{ (pop(\sigma), \sigma) \mid \sigma \in \mathcal{S} \land \sigma \neq \epsilon \land top(\sigma) = e\_{ call} \} \end{aligned}$$

The elements of *A* describe the relation between the two stacks appearing on the left-hand side and the right-hand side of a ret (2) S -rule involving *ecall*, whereas the elements of *B* describe this relation for a respective transformed rule.

In the following, I am going to show that *A* = *B* by proving that they are contained in each other.

So let (σ, *push*(*ecall*, σ)) ∈ *A*. Then we have

$$pop(push(e\_{call}, \sigma)) = \sigma \qquad \qquad \text{and} \qquad push(e\_{call}, \sigma) \neq \epsilon.$$

Define σ̃ *de f* = *push*(*ecall*, σ). Then σ̃ ≠ ϵ, *top*(σ̃) = *ecall* and

$$pop(\tilde{\sigma}) = pop(push(e\_{call}, \sigma)) = \sigma.$$

This means that

$$(\sigma \, \_\prime push(e\_{\text{call} \, \_\prime} \sigma)) = (pop(\vec{\sigma}) \, \_\prime \vec{\sigma}) \in B.$$

Conversely, let (*pop*(σ), σ) ∈ *B*. Then σ ≠ ϵ and *top*(σ) = *ecall*. Define σ̃ *de f* = *pop*(σ). Then

$$push(e\_{call\prime}\sigma) = push(e\_{call\prime}pop(\sigma)) = \sigma \neq \epsilon$$

325

and

$$pop(push(e\_{call}\,\tilde{\sigma})) = pop(\sigma) = \tilde{\sigma}.$$

This means that

$$(pop(\sigma), \sigma) = (\mathfrak{d} \, \_\primepush(e\_{call} \, \mathfrak{d} \,)) \in A.$$

The equality of *A* and *B* implies that the ret (2) S -constraints from Constraint System 6.5 can be replaced by the following equivalent ret' (2) S -constraints:

$$(\mathsf{n} \mathsf{n} \mathsf{r} \mathsf{r}'^{(2)}\_{\mathcal{S}}) \frac{e\_{\mathsf{ret}} \in \mathsf{E}\_{\mathsf{ret}} \quad t' \stackrel{\mathcal{E}\_{\mathsf{ret}}}{\to} t \quad (e\_{\mathsf{call}}, e\_{\mathsf{ret}}) \in \Phi \quad \sigma \neq \varepsilon \quad top(\sigma) = e\_{\mathsf{call}}}{\mathsf{X}\_{\mathcal{S}}(s, t, top(\sigma)) \ge f\_{\mathsf{ret}} \circ \mathsf{X}\_{\mathcal{S}}(s, t', \sigma)}$$

The replacement of ret (2) S by ret' (2) S in Constraint System 6.5 leads to Constraint System 7.3.

**Constraint System 7.3.** *Let* S = (*Ecall*, *S*, ≤, ϵ, *push*, *pop*, *top*) *be a stack space over Ecall. Then X*S : *N* × *N* × *S* →*mon F is an* S*-solution if it satisfies the following constraints:*

$$\begin{pmatrix} \text{(\text{EMTT}\_{S})} \frac{s \in N}{X\_{\mathcal{S}}(s, s, \epsilon) \ge id} \text{(\text{NTRA}\_{\mathcal{S}})} \frac{e \in E\_{\text{intrra}} \quad t' \stackrel{\varepsilon}{\to} t}{X\_{\mathcal{S}}(s, t, \sigma) \ge f\_{\mathbf{c}} \circ X\_{\mathcal{S}}(s, t', \sigma)} \end{pmatrix}$$

$$\begin{pmatrix} \text{cAL}\_{\mathcal{S}} \end{pmatrix} \frac{e\_{\text{call}} \in E\_{\text{call}} \quad t' \stackrel{\varepsilon\_{\text{cell}}}{\to} t}{X\_{\mathcal{S}}(s, t, \text{push}(e\_{\text{call}}, \sigma')) \ge f\_{\mathbf{c}} \circ X\_{\mathcal{S}}(s, t', \sigma')}$$

$$\begin{pmatrix} \text{Rev}^{(1)}\_{\mathcal{S}} \end{pmatrix} \frac{e\_{\text{ret}} \in E\_{\text{ret}} \quad t' \stackrel{\varepsilon\_{\text{ret}}}{\to} t}{X\_{\mathcal{S}}(s, t, \epsilon) \ge f\_{\mathbf{c}rt} \circ X\_{\mathcal{S}}(s, t', \epsilon)}$$

$$\begin{pmatrix} \text{Rev}^{(2)}\_{\mathcal{S}} \end{pmatrix} \frac{e\_{\text{ret}} \in E\_{\text{ret}} \quad t' \stackrel{\varepsilon\_{\text{ret}}}{\to} t \quad (e\_{\text{call}}, e\_{\text{ret}}) \in \Phi \quad \sigma \neq \epsilon \quad \text{top}(\sigma) = e\_{\text{call}}$$

$$X\_{\mathcal{S}}(s, t, \text{pop}(\sigma)) \ge f\_{\mathbf{c}rt} \circ X\_{\mathcal{S}}(s, t', \sigma)$$

**Lemma 7.33.** *Constraint System 6.5 and Constraint System 7.3 are equivalent: X is a solution of Constraint System 6.5 if and only if it is a solution of Constraint System 7.3.*

*Proof.* See the previous considerations. □

Now let C (S) be the set of constraints from Constraint System 7.3 with respect to the abstract stack space S. Furthermore, I define

*X* (S) 0 *de f* (7.64) = {(*s*,*s*, ϵ) | *s* ∈ *Src*}

$$\text{(7.65)}\qquad\qquad\mathcal{C}\_0^{(\mathcal{S})} \stackrel{def}{=} \text{Core}(\mathcal{C}^{(\mathcal{S})}, X\_0^{(\mathcal{S})})$$

$$(\text{7.66}) \qquad \qquad \mathcal{V}\_0^{(\mathcal{S})} \stackrel{def}{=} \text{CoreVars}(\mathcal{C}^{(\mathcal{S})}, X\_0^{(\mathcal{S})})$$

Algorithm 16 is an instantiation of Algorithm 8 that is supposed to solve C (S) 0 . The initialization loop can be seen in lines 2–4 and the main loop in lines 5–11. The body of the main loop enumerates all constraints *c* with (*s*, *t*, σ) ∈ *FV*(*rhs*(*c*)) by inspecting the stack σ and the outgoing edge *e* and determining which constraint to apply.

Assuming that C (S) 0 is definition-complete in Core(C (S) , *N* × *N* × *S*), we get the following correctness result for Algorithm 16.

**Theorem 7.34.** *Algorithm 16 always terminates and upon termination, we have*

$$(\mathsf{T}.6\mathsf{T})\qquad\mathcal{H}\_{\mathsf{S}}(\mathsf{s},t,\sigma)=\begin{cases}\operatorname{lfp}(\mathsf{F}\_{\mathsf{C}\_{0}^{(\mathsf{S})}})(\mathsf{s},t,\sigma) & \text{if } (\mathsf{s},t,\sigma)\in\mathsf{V}\_{0}^{(\mathsf{S})}\\\mathsf{B} & \text{otherwise}\end{cases}$$

*Moreover, we have*

$$\text{(7.68)}\qquad \mathcal{A}\_{\mathcal{S}} = \prescript{}{\mathcal{V}\_0^{(\mathcal{S})}}{\mathcal{V}\_0^{(\mathcal{S})}} \, \text{lfp}(\mathcal{F}\_{\text{Core}(\mathcal{C}^{(\mathcal{S})}, \mathcal{N} \times \mathcal{N} \times \mathcal{S})}) = \, \text{lfp}(\mathcal{F}\_{\mathcal{C}^{(\mathcal{S})}}) \, \text{l}$$

To fully establish the correctness and meaningfulness of Theorem 7.34, it remains to show that C (S) 0 is definition-complete in Core(C (S) , *N* × *N* × *S*) and give an appropriate characterization of V (S) 0 . I start with the latter. The following lemma does not fully solve this task, but at least shows that V (S) 0 is large enough37 .

37My conjecture is that an appropriate converse can also be shown, once a suitable formalization of reachability on *N* × *N* × *S* is available. I will however not consider this within the scope of this thesis.

**Algorithm 16:** Algorithm for computing the least S-solution

**Input:** a data-flow framework instance F = (*G*, *L*, *F*⊠, ρ) as described on page 295, set *Src* ⊆ *N* of sources **Result:** the least S-solution, as stated in Theorem 7.34 **1** AS ← *const*(⊠) **2 foreach** *s* ∈ *Src* **do 3** AS(*s*,*s*, ϵ) ← *id* **4** *W* ← {(*s*,*s*, ϵ)} **5 while** *W* ≠ ∅ **do 6** (*s*, *t*, σ) ← *remove*(*W*) **7 foreach** *e* ∈ *E such that t e*→ *t* ′ **do 8** σ ′ ← ⎧ ⎪⎪⎪⎪⎪⎪⎨ ⎪⎪⎪⎪⎪⎪⎩ σ if *e* ∈ *Eintra* ∨ *e* ∈ *Eret* ∧ σ = ϵ *push*(*e*, σ) if *e* ∈ *Ecall pop*(σ) if σ ≠ ϵ ∧ (*top*(σ),*e*) ∈ Φ ▼ otherwise **9 if** σ ′ ≠ ▼ **then 10** AS(*s*, *t* ′ , σ ′ ) ← AS(*s*, *t* ′ , σ ′ ) ⊔ *fe* ◦ AS(*s*, *t*, σ) **11** *W* ← *W* ∪ {(*s*, *t* ′ , σ ′ )} if AS(*s*, *t* ′ , σ ′ ) has changed **12 return** AS

**Lemma 7.35.** *For all s*, *t* ∈ *N, we have*

$$AP\_{\mathcal{S}}(\mathbf{s}, t) \neq \emptyset \land \mathbf{s} \in \text{Src} \implies \exists \sigma \in \text{S. } (\mathbf{s}, t, \sigma) \in \text{CoreVars}(\mathcal{C}\_{\mathcal{S}}, X\_0)$$

*Proof.* We show the statement

$$\begin{aligned} \forall \pi \in \text{Paths}\_G. \; \forall s, t \in \text{N}. \; \pi \in \text{Paths}\_G(s\_\prime t) \land s \in \text{Src} \land cs(\pi) \neq \bullet \\ \implies (s\_\prime t, cs(\pi)) \in \text{CoreVars}(\mathcal{C}\_\mathcal{S}, X\_0) \end{aligned}$$

by induction on π ∈ *PathsG*. So let π ∈ *PathsG* be a path with π ∈ *PathsG*(*s*, *t*), *s* ∈ *Src* and *cs*(π) ≠ ▼.

1. Assume that π = ϵ. Then *s* = *t* and (*s*,*t*, ϵ) = (*s*,*t*, *cs*(π)) ∈ *X*0 since *s* ∈ *Src*. Furthermore, CS contains a constraint

$$X\_{\mathcal{S}}(s, s, \epsilon) \ge id$$

by emptyS. Thus, (*s*, *t*, ϵ) ∈ CoreVars(CS, *X*0).

2. Assume that π = π ′ ·*e* with π ′ ∈ *PathsG*(*s*, *t* ′ ) and *t* ′ *e*→ *t*. By definition of *cs*, *cs*(π) ≠ ⊠ implies that *cs*(π ′ ) ≠ ⊠. Hence by induction hypothesis we may assume

$$(s, t', cs(\pi')) \in \text{CoreVars}(\mathcal{C}\_{\mathcal{S}'}X\_0).$$

We observe that CS contains the constraint

$$(\star) \qquad \qquad X\_{\mathcal{S}}(s, t, \operatorname{cs}(\pi)) \ge f\_{\mathcal{E}} \circ X\_{\mathcal{S}}(s, t', \operatorname{cs}(\pi')) . \mathbb{R}$$

To see this, we make a case distinction on *e*.

*e* ∈ *Eintra*: Then *cs*(π) = *cs*(π ′ ) and we obtain the constraint by intraS. *e* ∈ *Ecall*: Then *cs*(π) = *push*(*ecall*, *cs*(π ′ )) and we obtain the constraint by

callS.

*e* ∈ *Eret*: Then one of the following statements holds:

$$\text{(1)}\qquad\text{cs}(\pi) = \text{cs}(\pi') = \epsilon$$

$$\text{(2)}\qquad \text{cs}(\pi') \neq \epsilon \land (\text{top}(\text{cs}(\pi')) , \epsilon) \in \Phi \land \text{cs}(\pi) = \text{pop}(\text{cs}(\pi')) .$$

In case (1), we obtain the constraint by ret (1) S and in case (2) by ret' (2) S .

Since (*s*,*t* ′ , *cs*(π ′ )) ∈ CoreVars(CS, *X*0), constraint (⋆) is contained in Core(CS, *X*0) and we obtain

$$(\mathbf{s}, t, cs(\pi')) \in \mathbf{CoreVars}(\mathbf{C}\_{\mathbf{S'}} \mathbf{X}\_0)\_{\mathbf{s'}}$$

as desired.

□

To prove the definition-completeness, I need a connection between V (S) 0 and CoreVars(CS, *N* × *N* × *S*). Its proof is analogous to the proof of, e.g., (7.43) in Lemma 7.22.

**Lemma 7.36.** *For all s*, *t* ∈ *N and* σ ∈ *S, we have*

$$\mathcal{V}\_0^{(\mathcal{S})} = \text{CoreVars}(\mathcal{C}\_{\mathcal{S}'}N \times N \times \mathcal{S}) \cap \mathcal{S}rc \times N \times \mathcal{S}$$

Now I can give the proof of the definition-completeness of V (S) 0 in CoreVars(CS, *N* × *N* × *S*).

**Lemma 7.37.** Core(CS, *X*0) *is definition-complete with respect to its superset* Core(CS, *N* × *N* × *S*)*.*

*Proof.* We use Theorem 7.10. Let *c* ∈ Core(CS, *N* × *N* × *S*) with *lhs*(*c*) ∈ CoreVars(CS, *X*0). Then we have to show

$$(7.69) \qquad \qquad FV(rhs(c)) = \emptyset \implies lhs(c) \in X\_0$$

(7.70) *FV*(*rhs*(*c*)) ≠ ∅ ∧ *x* ∈ *FV*(*rhs*(*c*)) =⇒ *x* ∈ CoreVars(CS, *X*0)

We show the two claims separately.

(7.69)**:** If *FV*(*rhs*(*c*)) = ∅, then *c* is of the form

$$X\_{\mathcal{S}}(s, s, \epsilon) \ge id$$

Since (*s*,*s*, ϵ) = *lhs*(*c*) ∈ CoreVars(CS, *X*0), it must be the case that (*s*,*s*, ϵ) ∈ *X*0 by Lemma 7.36.

(7.70)**:** Let *FV*(*rhs*(*c*)) ≠ ∅. Inspection of Constraint System 7.3 shows that *c* is of the form

$$X\_{\mathcal{S}}(s, t, \sigma) \ge f\_{\mathfrak{e}} \circ X\_{\mathcal{S}}(s, t', \sigma')$$

where *t* ′ *e*→ *t* and (*s*,*t*, σ) = *lhs*(*c*). Note that the *s* on the right-hand side is the same as on the left-hand side. Since *c* ∈ Core(CS, *N* × *N* × *S*), we have (*s*,*t* ′ , σ ′ ) ∈ CoreVars(CS, *N* × *N* × *S*). Moreover, since (*s*,*t*, σ) ∈ CoreVars(CS, *X*0), we get *s* ∈ *Src* by Lemma 7.36. Thus (*s*, *t* ′ , σ ′ ) ∈ CoreVars(CS, *X*0) by Lemma 7.36.

□

Theorem 7.34 states that Algorithm 16 solves C (S) for an appropriate subset of *N* × *N* × *S*. In particular, for every (*s*, *t*) ∈ *Src* × *N* such that *AP*(*s*, *t*) ≠ ∅, there is some σ ∈ *S* such that the result AS(*s*,*t*, σ) = *l f p*(*F* C(S))(*s*,*t*, σ). It remains to establish a connection between *l f p*(*F* C(S)) and *MOVP* to be fully convinced that Algorithm 16 indeed yields a (*VP*, *Src* × *N*)-correct solution.

Now define

$$\mathcal{A}(s,t) \stackrel{def}{=} \bigsqcup\_{\sigma \in S} \mathcal{A}\_{\mathcal{S}}(s,t,\sigma).$$

Then the above considerations and Theorem 6.16 entail that

$$\text{(7.71)}\qquad\qquad\text{AP(s,t)}\neq\emptyset\implies\mathcal{R}(\mathbf{s},t)\geq\text{MOAP}(\mathbf{s},t).$$

Moreover, if F is distributive, then by Theorem 6.18, I can refine this to

$$AP(s, t) \neq \emptyset \implies \mathcal{R}(s, t) = MOAP(s, t)$$

Finally, if S is chosen appropriately, it follows from Corollary 6.33 that Algorithm 16 can be used to compute a (*VP*, *Src* × *N*)-correct solution.

**Theorem 7.38.** *Assume that there is a stack abstraction between* S∞ *and* S*. Let* AS *be the result of Algorithm 16 and define*

$$\mathcal{A}(s,t) \stackrel{def}{=} \bigsqcup\_{\sigma \in \mathcal{S}} \mathcal{A}\_{\mathcal{S}}(s,t,\sigma).$$

*Then* A *is* (*VP*, *Src* × *N*)*-correct.*

*Proof.* Assume (*s*,*t*) ∈ *Src* × *N*. Then we have to show *MOVP*(*s*,*t*) ≤ A(*s*,*t*). For *VP*(*s*,*t*) = ∅, there is nothing to show, so we may assume *VP*(*s*,*t*) ≠ ∅. Because of our assumption about S, we may apply Corollary 6.33 and yield *VP*(*s*, *t*) ⊆ *AP*(*s*, *t*) and

$$\text{(7.72)}\qquad\qquad\qquad\text{MOVP}(\mathbf{s},t)\leq\text{MOAP}(\mathbf{s},t).$$

Because *VP*(*s*, *t*) ≠ ∅, we get *AP*(*s*, *t*) ≠ ∅. Hence, we may apply (7.71) and get

$$\text{(7.73)}\qquad\qquad\qquad\qquad\qquad\text{MOAP}(s,t)\leq\mathcal{H}(s,t)\text{)}$$

(7.72) and (7.73) imply *MOVP*(*s*, *t*) ≤ A(*s*, *t*), as desired. □

*And I think it's gonna be a long long time.*

# Elton John **8**

# **Implementation and Evaluation**

In the previous chapters, I theoretically developed and examined various algorithms to conduct generalized interprocedural data-flow analysis on interprocedural graphs. The purpose of this chapter is to demonstrate that these theoretically stated algorithms also work in practice. To this end, I implemented the algorithms in the Joana framework and conducted an evaluation of both performance and precision.

This chapter is organized as follows. First, I am going to give an overview of my implementation in section 8.1. The other sections are dedicated to the evaluation.

Section 8.2 describes several aspects on the setup of my evaluation, particularly which samples and instances I chose. Then, I describe and discuss the results of the performance evaluation in section 8.3. Lastly, section 8.4 is dedicated to the precision evaluation.

# **8.1 Notes on the Implementation**

My implementation allows for arbitrary data-flow framework instances. In order to enable evaluations and comparison with Joana's summary edge computation and slicers, my implementation works on Joana's graph data structure.

In the next subsections, I am going to consider several aspects of my implementation in more detail. Subsection 8.1.1 is dedicated to my implementation of the functional approach and subsection 8.1.2 considers my implementation of the call string approach. Finally, in subsection 8.1.3, I will conduct a worst-case complexity analysis on all implemented algorithms.

# **8.1.1 Functional Approach**

As we still remember from previous chapters, the functional approach consists of a preprocessing phase that computes same-level information, and a two-phase algorithm that computes the actual data-flow analysis solution using the same-level information. In the following, I will give a brief overview of my implementations of both steps, in this order.

I implemented two variants of the same-level info computations, which I will elaborate on in subsubsection <IP_ADDRESS> and subsubsection <IP_ADDRESS>, respectively. Before that, in subsubsection <IP_ADDRESS> I give some general hints on how my implementations represent same-level information.

After having described my summary info computation implementations, I consider my implementation of the actual two-phase data-flow analysis in subsubsection <IP_ADDRESS>.

# **<IP_ADDRESS> Representing Same-Level Information**