Maroua Maalej

Vitor Paisante

Fernando Magno

Quintão Pereira

Laure Gonnord

Combining Range and Inequality Information for Pointer Disambiguation

Keywords: Points-to Analysis, Pentagons, Less-Than Check, Abstract Interpretation, Compiler Construction, Static Analysis

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Pointers are a staple feature in imperative programming languages. Among the many abstractions that exist around this notion, pointer arithmetics stands out. Although a popular feature, it yields programs that are particularly difficult to analyze statically. We call pointer arithmetics the ability to add an offset to a pointer, as in p[i], or *(p + i). Pointer arithmetics is A more precise alias analysis brings many advantages to programming language tools, including compilers. One of such benefits is optimizations: the extra precision gives compilers information to carry out more extensive transformations in programs. Figure 2 illustrates this benefit. The figure shows the result of applying Surendran's [START_REF] Surendran | Inter-iteration scalar replacement using array SSA form[END_REF]] interiteration scalar replacement on the insertion sort algorithm shown in Figure 1. Scalar replacement is a compiler optimization that consists in moving memory locations to registers as much as possible. This optimization tends to speed up programs because it removes memory accesses from their source code. In this example, if we can prove that v[i] and v[j] do not reference overlapping memory locations, we can move these locations to temporary variables. For instance, we have loaded location v[j] into tmp j at line 6. We update the value of v[i] at line 13.

for (j = i + 1; j < N; j++) { 5 if (v[i] > v[j]) { 6 int tmp = v[i]; 7 v[i] = v[j];
Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017 1 void ins sort goal(int * v, int N) { 2 int i, j,tmp i,tmp j,tmp; There exist points-to analyses designed specifically to deal with pointer arithmetics [START_REF] Balakrishnan | Analyzing memory accesses in x86 executables[END_REF]; [START_REF] Van Engelen | A unified framework for nonlinear dependence testing and symbolic analysis[END_REF]; [START_REF] Paisante | Symbolic range analysis of pointers[END_REF]; [START_REF] Rugina | Symbolic bounds analysis of pointers, array indices, and accessed memory regions[END_REF]]. Nevertheless, none of them works satisfactorily for the two examples seen in Figure 1 and thus fail to enable the optimization in Figure 2. The reason for this ineffectiveness lies on the fact that these analyses use range intervals to disambiguate pointers. In our examples, the ranges of integer variables i and j overlap. Therefore, any conservative range analysis, à la Cousot [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]], once applied on Figure 1a, will conclude that i exists on the interval [0, N -2], and that j exists on the interval [1, N -1]. Because these two intervals have non-empty intersections, points-to analyses based on the interval lattice will not be able to disambiguate the memory accesses at lines 6-8 of Figure 1a.

The techniques from this paper disambiguate v[i] and v [j] in both examples. Key to this ability is the observation that i < j at every program point where we access v. We conclude that i < j by means of a "less-than check". A less-than check is a relation between two variables, e.g., v 1 and v 2 , that is true whenever we can prove -statically -that one holds a value less than the value stored into the other. In Figure 1a, we know that i < j because of the way that j is initialized, within the for statement at line 4. In Figure 1b, we know that i < j due to the conditional check at line 7.

The design space of constructing less-than relations between program variables is large. In this paper, we chose to use the Pentagon lattice to Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017 build such relations. However, a straightforward application of Pentagons, as originally defined by Logozzo and Fähndrich, would not be able to deduce the disambiguation between v[i] and v [j]. The syntax v[i] denotes a memory address given by v + i. Pentagons combine range analysis with a less-than check. The range of v, a pointer, is [0, +∞]. Therefore, this will be also the range of v + i and v + j. In other words, even though we know that i < j, we cannot conclude that v + i < v + j. A way to solve this problem is to separate the analysis of pointers from the analysis of integers. In Section 4, we shall describe an abstract interpreter that does it.

In terms of implementation, our approach focuses on "top-level variables": variables that we can represent in Static Single Assignment (SSA) form [START_REF] Alpern | Detecting equality of variables in programs[END_REF]; [START_REF] Cytron | An efficient method of computing static single assignment form[END_REF]]. In this representation, each variable has a single definition site, and special instructions, the φ-functions, join the live ranges of names that, in the original program, represent the same variable. Compilers such as gcc, icc and clang represent pointers with offsets in this format. However, memory itself, i.e., regions pointed by pointers, are not in the SSA representation. Thus, the developments that we shall introduce in this paper do not disambiguate pointers to pointers: this problem pertains to the domain of standard alias analyses, à la Andersen [START_REF] Andersen | Program analysis and specialization for the c programming language[END_REF]]. This fact does not compromise our implementation in any way: range and inequality checks are only used to disambiguate pointers that belong into the same memory unit, such as an array or a C-like struct.

This Paper in Five Examples. This section has explained the need for techniques able to disambiguate pointers with offsets. The rest of this paper describes an implementation of such a technique. Our implementation involves several steps. Throughout the paper, we use five examples to illustrate each of these steps, when applied onto the program in Figure 1a. The first step consists in converting the program to a suitable intermediate representation.

Example 1 illustrates this step for function ins sort. From this representation we extract a data-structure called a Program Dependence Graph, as shown in Example 3. The main purpose of this graph is to give us the means to disambiguate non related pointers and to enable comparing related ones using the less-than relations. Such process is the subject of Example 4. The solution of this constraint system gives us, for each variable v, a set of other variables that are known to be less than v. Example 9 shows the sets that we obtain for Figure 1a's routine. Finally, we have different ways to perform queries on these "less-than" sets. Example 11 clarifies this usage of our analysis.

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

Program representation for sparsity and range pre-analysis

In this paper we shall work at a low-level representation of programs. The syntax of this assembly-like language is given in Figure 3. The figure also gives, informally, the semantics of each instruction. Throughout the paper, we shall return to the high-level C notation whenever necessary to explain examples; however, our formalization will happen onto the syntax in Figure 3. Most of that syntax bears an intuitive semantics, except for conditionals and φ-functions, which we use to make our analysis sparse, as we discuss in Section 3.1. The instruction p 0 = malloc(i 0 ) creates a block of i 0 bytes of memory, and assigns the address of the first byte to pointer p 0 . A load such as v = * p reads the contents of the memory cell pointed by p, and assigns that value to v. The store instruction * p = v puts the value of variable v into the address pointed by p. The notation v 0 = φ(v 1 : 1 , v 2 : 2 ) assigns either v 1 or v 2 to v 0 , depending on the program flow reaching this instruction through 1 or 2 , respectively. The syntax of branches is more convoluted, because it lets us infer "less-than" facts about the variables used in the conditional test. We shall provide more details about this syntax in the next section. [START_REF] Cytron | An efficient method of computing static single assignment form[END_REF]])

| v 0 = v 1 + i 0 ; Addition | v = * p ; Load | * p = v ; Store | v 0 = φ(v 1 : 1 , v 2 : 2 ) ; Phi-function (Phi ) (See
| (v 0 R v 1 ) ? S * B S * B ; Branch (R ∈ {<, ≤, =, =, >, ≥}) B ::= : Phi * I * ; Basic Block S ::= v 0 = σ(v 1 )
; Sigma-function (See [START_REF] Singer | Static program analysis based on virtual register renaming[END_REF]])

Figure 3: The syntax of our language of pointers. Whenever a variable must be explicitly a pointer, we name it p. Variables that need to be integers are named i. Variables that can be either an integer or a pointer are named v. We use the Kleene Star ( * ) to indicate zero or more repetitions of a non-terminal.

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

Sparse Analysis

The implementation that we discuss in this paper is a sparse analysis. According to [START_REF] Tavares | Parameterized construction of program representations for sparse dataflow analyses[END_REF]], a data-flow analysis is sparse if the abstract state associated with a variable is constant throughout the entire live range of that variable. Notice that this information might not be true for every program. As an example, consider the program in Figure 1b. We know that i < j within lines 8-10. However, this fact is false at line 7. To make a data-flow analysis sparse, we resort to live range splitting.

The live range of a variable v is the set of program points where v is alive. To split the live range of a variable v, at a program point x, we insert a new instruction v = v at x, where v is a fresh name. After that, we rename every use of v that is dominated by x to v . We say that a program point x dominates a program point y if every path from the program's entry point to y must go across x. Live range splitting is a well-known technique to sparsify data-flow analyses. There are several program representations that naturally implement this trick. The most celebrated among these representations is the Static Single Information form, which ensures that each variable has at most one definition point.

The SSA format is not enough to ensure sparsity to the analysis that we propose in this paper. Therefore, we use a different flavor of this program representation: the Extended Static Single Assignment form [START_REF] Bodik | ABCD: eliminating array bounds checks on demand[END_REF]] (e-SSA). The e-SSA form can be computed cheaply from an SSA form program. This extension introduces σ-functions to redefine program variables at split points such as branches and switches1 . These special instructions, the σ-functions, rename variables at the out-edges of conditional branches. They ensure that each outcome of a conditional is associated with a distinct name. In our case, this property lets us bind to each variable name the information that we learn about it as the result of comparisons performed in conditional statements.

Example 1. Figure 4 shows the Control Flow Graph (CFG) of the program seen in Figure 1a, in e-SSA form. The σ-functions rename every variable used in a comparison. Renaming lets us, for instance, infer that x iT > x jT , Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017 1a. i T = σ(i) denotes the "true" version of i after the test i < N . i = φ(i 0 , i 1 ) denotes the value of i inside the first loop, its value is i 0 if the flow comes from the first block, or i 1 if the flow comes from the returning edge i 1 = i T + 1.

i 0 = 0 N = N -1 i = φ(i 0 , i 1 ) i < N ? i T = σ(i) N T = σ(N ) j 0 = i T + 1 N F = σ(N ) i F = σ(i ) halt j = φ(j 0 , j 1 ) j < N ? j F = σ(j) N F = σ(N ) i 1 = i T + 1 j T = σ(j) N T = σ(N ) v i = v + i T v j = v + j T x i = * v i x j = * v j x i > x j ? x iT = σ(x i ) x jT = σ(x j ) v i = v + i T v j = v + j T tmp = * v i * v i = * v j * v j = * tmp j 1 = j T + 1 Figure 4: Control Flow Graph of program in Figure
because: (i) these variables are copies of x i and x j ; and (ii) they only exist in the true side of the test x i > x j .

Range Analysis for integer variables

A core component of our pointer disambiguation method is a range analysis for scalar variables, which can be symbolic or numeric. In this context, a symbol is any name in the program syntax that cannot be built as an expression of other names. Range analysis is not a contribution of this work. There are several different implementations already described in the compiler-related literature [START_REF] Alves | Runtime pointer disambiguation[END_REF]; [START_REF] Blume | Symbolic range propagation[END_REF]; [START_REF] Nazaré | Validation of memory accesses through symbolic analyses[END_REF]; [START_REF] Rodrigues | A fast and low overhead technique to secure programs against integer overflows[END_REF]; [START_REF] Rugina | Symbolic bounds analysis of pointers, array indices, and accessed memory regions[END_REF]]. In this paper, we have adopted a non-relational range analysis [START_REF] Rodrigues | A fast and low overhead technique to secure programs against integer overflows[END_REF]] on the classic integer interval [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]]. A nonrelational range analysis associates variable names with ranges that are not function of other variables. Relational analyses, on the other hand, associate sets of variable names with ranges. As an example, Miné's Octagons create Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017 relations between pairs of variables and range information [START_REF] Miné | The octagon abstract domain[END_REF]]. Our approach to build this range analysis is less precise than a relational approach, but has lower asymptotic complexity. In the sequel, we let R(v) = [l, u] be the (symbolic) range of variable v computed by any range analysis.

Example 2. Considering the program in Figure 4, the analysis of Blume et al. [START_REF] Blume | Symbolic range propagation[END_REF]] finds the following ranges for the variables in that program:

R(i 0 ) = [0, 0], R(i 1 ) = [1, N -1], R(i) = [0, N -1], R(j 0 ) = [1, N -1], R(j 1 ) = [2, N ], R(j) = [1, N ].
The ranges of integer variables given by Rodrigues et al. [START_REF] Rodrigues | A fast and low overhead technique to secure programs against integer overflows[END_REF]

] are R(i 0 ) = [0, 0], R(i 1 ) = [1, +∞], R(i) = [0, +∞], R(j 0 ) = [1, +∞], R(j 1 ) = [2, +∞], R(j) = [1, +∞].
We would like to emphasize that the range analysis that we shall use to obtain intervals for integer variables is immaterial for the correctness of our work. The only difference they make is in terms of precision and scalability. The more precise the range analysis that we use, the more precise the pointer analysis that we produce, as we will see in Section 5.3. However, precision has an impact on the runtime of the analysis. Given that range analysis is not a contribution of this work, we shall omit details related to its implementation, and refer the reader to the original discussion about our particular choice [START_REF] Rodrigues | A fast and low overhead technique to secure programs against integer overflows[END_REF]].

Pointer Disambiguation Based on Strict Inequalities

The technique that we introduce in this paper to disambiguate pointers is semi-relational, i.e., it maps variables to ranges that might contain other variables as symbolic limits; however, contrary to relational analysis, it does not map groups of variables to abstract states. Our analysis lets us compare two pointers, p 1 and p 2 , and show that they are different, whenever we can prove a core property, which we define below:

Definition 1 (The Strict Inequality Property). We say that two pointers, p 1 and p 2 are strictly different whenever we can prove that either p 1 < p 2 , or p 2 < p 1 , at every program point where these two pointers are simultaneously alive.

Definition 1 touches several concepts pertaining to the vocabulary of compilation theory. A program point is a region between two consecutive instructions in assembly code. We say that a variable v is alive at a program point Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

x if, and only if, there exists a path from x to another program point where v is used, and this path does not cross any redefinition of v. Computing live ranges of variables is a classical dataflow analysis (Nielson et al., 2005, Sec-2.1.4).

We call the alias analysis approach we describe in this paper "staged", because it works in successive stages. It consists of the following four parts, which we describe in the rest of the paper:

1. Group pointers related to the same memory location. We describe this step in Section 4.1 2. Collect constraints by traversing the program's control flow graph. Section 4.3 provides more details about this stage. 3. Solve the constraints produced in phase 3. Section 4.4 explains this phase of our approach. 4. Answer pointer disambiguation queries. We describe our method of answering queries in Section 5.

Grouping Pointers in Pointer Digraphs

Recalling Definition 1, we know that we can disambiguate two pointers, p 1 and p 2 , whenever we can prove that p 1 < p 2 . This relation is only meaningful for pointers that are offsets from the same base pointer2 . A base pointer is a reference to the beginning of a memory block (address zero). As an example, a statement like "u = malloc(4)" will create a base pointer referenced by u. Formal arguments of functions, such as v in Figure 1a, are also base-pointers.

We call a Pointer Dependence Digraph (PDD) a directed acyclic graph (DAG) with origin at one or more base-pointers. All other nodes in this datastructure that are not base-pointers are variables that can be defined by an offset o from the base pointers. We let o be a symbol, such as a constant or the name of a variable, as defined in Section 3.2. For instance, the relation p = p 0 + o is represented, in the PDD, by an edge from the node p to the node p 0 labeled by ω p,p0 = o. We denote this edge by p → o p 0 .

When analyzing a program, we build as many PDDs as the number of pointer definition sites in the program. Notice that this number is a static concept. A memory allocation site within a loop still gives us only one allocation site, even if the loop iterates many times. Such a data-structure is constructed according to the rules in Figure 5, during a traversal of the program's control flow graph. Notice that we have a special treatment for φ-functions. A φ-function is a special instruction used in the SSA format to join the live ranges of variables that represent the same name in the original program, before the SSA transformation. We mark nodes created by φfunctions as dashed edges in the PDD. In this way, we ensure that a PDD has no cycles, because in an SSA-form program, the only way a variable can update itself is through a φ-function.

p = malloc() p p = p 0 + x p 0 p p = σ(p 0 ) p 0 p p = φ(p 0 , p 1 ) p 0 p 1 p x 0
Example 3. The rules seen in Figure 5, once applied onto the control flow graph given in Figure 4, give us the PDD shown in Figure 6.

v v i v j v iT v jT i T j T 0 0

Constraint System

We solve the less-than analysis via a constraint system. This constraint system is formed by five different kinds of constraints, which involve two variables, and a relational operator. Valid relational operators are R ∈ {= , <≤, ≥, >}, each one giving origin to one of the five types of constraints. If Prog is a program formed according to the syntax seen in Figure 3, and {v 1 , v 2 } ∈ Prog are two variables, then we let v 1 R v 2 be a constraint. We use the same names to denote program variables and constraint variables. Program variables are elements that exist in the syntax of Prog; constraint variables are symbols, which, as we shall see in Section 4.4, are mapped to "less-than" information. Because it is always possible to know which entity we refer to, given the context of the discussion, we shall not use any notation to distinguish them.

To explain the semantics of constraints, we describe the semantics of programs. A program Prog is formed by instructions, which operate on states σ : Var → Int. We say that a variable v is defined at a state σ, if σ(v) = n; otherwise, the variable is undefined at that state, a fact that we denote by σ(v) = ⊥. Constraints determine relations between defined variables, given a state σ. Definition 2 express this notion.

Definition 2 (Intuitive Semantics). We say that a constraint v 1 R v 2 satisfies a state σ if σ(v 1 ) R σ(v 2 ) whenever v 1 and v 2 are defined for σ.

Collecting Constraints

During this phase, we collect a set C of constraints according to the rules in Figure 7. Recall that R(v) denotes the numeric range of variable v given by a pre-analysis. We let R(v) ↓ and R(v) ↑ be the lower and upper bounds of interval R(v), respectively. All the constraints that we produce in this stage follow the template p 1 Rp 2 , where R ∈ {<, ≤, =}. The rules in Figure 7 are syntax-directed. For instance, an assignment p=q+v lets us derive the fact p > q, if the range analysis of Section 3.2 is capable of proving that v is always strictly greater than zero. The "=" equality models set inclusion, and is asymmetric as we shall explain in details in Section 4.4.

Constraints are simple, the syntax of the constraints is self-explanatory using standard semantics ; however, some comments follow. Firstly, the difference between add and gep 3 is the fact that the latter represents an addition on a pointer p plus an offset v 1 , whereas the former represents general integer arithmetics. We distinguish both because the C standard forbids any arithmetic operation on pointers other than adding or subtracting an integer to it. Therefore, to avoid comparing a pointer to an Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017 integer variable, the constraints that we produce for arithmetic operations involving pointers are different from those we produce for similar instructions that involve only integers, as Figure 7 shows.

p F 1 } if R = " ", then C ∪ = {p T 1 p T 2 } ∪ {p F 2 < p F 1 } C ∪ = {p T 1 = p 1 } ∪ {p F 1 = p 1 } ∪ {p T 2 = p 2 } ∪ {p F 2 = p 2 } union : v = φ(v i ) ⇒ C ∪ = {v = φ(v i )} v = c -v 1 , c ∈ N q = * p * q = p ⇒ nothing
A second aspect of our constraint system, which is worth mentioning, is the fact that we do not try to track less-than information throughout pointers. Hence, as Figure 7 shows, we do not generate constraints for loads and stores, which means that we do not build less-than relations for data stored in memory. Consequently, our current implementation of the less-than lattice misses opportunities to disambiguate second-order pointers, i.e., pointers to pointers. This omission is not a limitation of the theory that we present in this paper. Rather, it is an implementation decision, which we took to simplify the design of our algorithm. Handling pointers to pointers is possible in different ways. For instance, we can use some pre-analysis, à la Andersen [START_REF] Andersen | Program analysis and specialization for the c programming language[END_REF]] or à la [START_REF] Steensgaard | Points-to analysis in almost linear time[END_REF]], to group memory references into single locations. After this bootstrapping phase, we can treat these memory locations as variables, and extract constraints for them using the rules in Figure 7.

The construction of constraints for tests is more involved. The e-SSA form, which we have discussed in Section 4, provides us explicit new versions of variables, e.g.: p T , q T , p F , q F , after a test such as p < q. We use T as a subscript for the new variable name created at the true branch; F has similar use for the false branch. Thus, this conditional test for instance gives us two constraints: p T < q T and p F ≥ q F . Example 4. The rules in Figure 7, when applied onto the CFG seen in Figure 4, give us that

C = {N < N , i = φ(i 0 , i 1 ), i T < N T , N F ≤ i F ; i T < j 0 , j = φ(j 0 , j 1 ), i T = i, j T = j, j T < N T , N F ≤ j F , v ≤ v i , v < v j , v ≤ v i , v < v j , j T < j 1 , i T < i 1 , x jT < x iT , x iF ≤ x jF }
The Relation between PDDs and Constraints. The purpose of the PDDs of Section 4.1 is to avoid comparing pointers that are not related by C-style arithmetics. They do not bear influence on the production of constraints; rather, they are only used in the queries that we shall describe in Section 4.4. This fact means that the grouping of pointers in digraphs is not an essential part of the idea of using strict inequalities to disambiguate pointers. However, PDDs are important from an operational standpoint: they provide a way of separating pointers that are not related by arithmetic operations; hence, are incomparable. Thus, the phases described in Section 4.1 and in this section are independent, and can be performed in any order.

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

strict less than : x < y ⇒ LT(y) ∪ = LT(x) ∪ {x} GT(x) ∪ = GT(y) ∪ {y} less than : x y ⇒ LT(y) ∪ = LT(x) GT(x) ∪ = GT(y) non ref lexive eq : x = y ⇒ LT(x) ∪ = LT(y) GT(x) ∪ = GT(y)

Solving Constraints

The objective of this phase is to obtain Pentagon-like abstract values for each variable or pointer of the target program. Henceforth, we shall call the set of program variables V. The product of solving constraints is a relation LT. Given v ∈ V, LT(v) will keep track of all the variables that are strictly less than v. In addition to LT, we build an auxiliary set GT. Set GT(v) keeps track of all the variables that are strictly greater than v. Ordering relations are reflexive; hence, if x < y, then y > x. This fact means that we can build GT from LT, or vice-versa; hence, we could write our solver with only one of these relations. However, using just one of them would result in an unnecessarily heavy notation. Consequently, throughout the rest of this section we shall assume that the following two equations are always true:

GT(v) = {v i | v ∈ LT(v i )} ∧ LT(v) = {v i | v ∈ GT(v i )}
Figures 8 and 10 contain the definition of our constraint solver. Constraints are solved via chaotic iterations: we compute for each program variable a sequence of abstract values until reaching a fixpoint. The non-reflexive equal is used to model relations that are known to be true before sigma nodes. A given relational information which is true about variables before a conditional branch continues to hold also in the "then" and "else" paths that sprout from that branch. Example 5 illustrates this fact:

Example 5. If the relation (x < y) holds before a conditional node that uses the predicate (x < z?), then these two relations are also true: (x T < y and Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

x F < y), where x T is the new name of x in the "then" branch of the conditional, and x F is the new name of x in the "else" branch.

Dealing with φ-functions. Join nodes are program points that denote loops and conditional branches. In SSA-form programs, these nodes are created by φ-functions. These instructions give us special constraints, as Figure 7 shows.

A φ-function such as v = φ(v 1 , v 2 ) yields the constraint {v = φ(v i )}, 1 ≤ i ≤ 2.
When used in the head of loops, φ-functions may join variables that represent initialization values and loop variant values for a given variable v.

To build a less-than relation between these variables, we must find out how the value of v evolves during the execution of the program. It might increase, it might decrease, or it might oscillate. If v only decreases, then it will be less than or equal to the maximum among its initialization values. In the opposite case, in which v only increases, the variable produced by the φ-function will be greater than or equal to the minimum among its initialization values.

To infer relations between the variable defined by a φ-function, and the variables used as arguments of that φ-function, we perform a growth check. On the resolution of each join constraint such as x = φ(x 1 , . . . , x n ), we check if x is present in the LT or GT sets of some x i which is loop variant. If x is present in the LT of each loop-variant right-side operand, then the program contains only execution paths in which x grows. That is to say that x is always receiving a value that is greater than itself. Dually, if x is present in the GT of each loop-variant x i , then there exist only paths in the program along which x decreases.

In order to detect if a given x i is loop-variant, we use the dominance information: if the definition of a φ-function, e.g., x, dominates the definition point of one of its arguments, e.g., x i , then we know that this φ-function occurs in a loop, and we say that x i is loop-variant. This observation holds for the so called natural loops, which characterize reducible control flow graphs. For the definition of these concepts, we refer the reader to the work of Ferrante et al. [START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF]]. Example 6 illustrates these observations. Example 6. Variable x in Figure 9

x 1 = z + 1 x 2 = z + 4
x =ϕ (x 1 , x 2 , x 3 )

x 3 = x + 1 LT(z) = {} LT(x 1 ) = {z} LT(x 2 ) = {z} LT(x) = {z} LT(x 3 ) = {x, z} z = 1 x 1 = z + 1 x =ϕ (x 1 , x 2 , x 3 ) x 2 = x + 1 LT(z) = {} LT(x 1 ) = {z} 1 LT(x 2 ) = {x} 1 LT(x) = {x 3 } LT(x 3 ) = {} GT(z) = {x 1 } GT(x 1 ) = {} 1 GT(x 2 ) = {} 1 GT(x) = {x 2 } GT(x 3 ) = {x} 1 x 3 = x -1 (a) (b)
Figure 9: Less-than and greater-than sets built by our analysis.

formed by a trigger T and an action a, denoted by the notation T ⇒ a. The action a is evaluated only if the trigger T is true. The constraint x = φ(x i ) has three different triggers, and at any moment, at least one of them is true. Triggers check if particular LT and GT sets contain specific variables.

Example 7 explains how we compute the less-than set of x.

join

: x = φ(x i ) 0 i n ⇒                                i : A ⇒ LT(x) ∪ = LT(x j )
x j / ∈Dom(x)

ii : B ⇒ GT(x) ∪ = GT(x j )

x j / ∈Dom(x) iii : Otherwise ⇒      LT(x) ∪ = n i=0 LT(x i ) GT(x) ∪ = n i=0
GT(x i )

Figure 10: Solving constraints for φ-functions. We let x ∈ {x, x T , x F } and Dom(x) = {x i s.th. x dominates x i }, A ≡ ∀x j ∈ Dom(x), x ∈ LT(x j ) and B ≡ ∀x j ∈ Dom(x), x ∈ GT(x j ). A indicates that x increases in the loop, and B indicates that x decreases. Variables x T and x F are new names of x created by σ-functions after conditional branches.

Example 7. Variable x, defined in Figure 9 (a) has increasing value, because it belongs into LT (x 3 ) and Dom(x) = {x 3 }. Therefore, trigger i,

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

in Figure 10 applies, and we know that LT(x) = LT(x) ∪ (LT(x 1 ) ∩ LT(x 2 )).

Thus, LT(x) = LT(x) ∪ ({z} ∩ {z}) = {z}.
Implementation of the Constraint Solver. We solve the constraint set C via the method of Chaotic Iterations (Nielson et al., 2005, p-176). We repeatedly insert constraints into a worklist W , and solve them in the order they are inserted. The evaluation of a constraint might lead to the insertion of other constraints into W . This insertion is guided by a Constraint Dependence Graph (CDG). Each vertex v of the CDG represents a constraint, and we have an edge from v 1 to v 2 if, and only if, the constraint represented by v 2 reads a set produced by the constraint represented by v 1 . Upon popping a constraint such as x < y, we verify if its resolution changes the current state of LT sets. If it does, then we insert back into the worklist every constraint that depends on y, i.e., that reads LT(y). This algorithm has asymptotic complexity O(n 3 ). However, in practice our implementation runs in time linear on the number of constraints, as we show empirically in Section 7.

The process of constraint resolution is guaranteed to terminate as shown in Theorem 1. Example 8 illustrates this approach.

Example 8. We let C = {x < y, y < z}. The result of solving C to build LT sets is given in Figure 11. Our worklist is initialized to the constraint set C. Each variable v is bound to an abstract state LT(v) = ∅ and GT(v) = ∅.

Resolution reaches a fixpoint when the worklist is empty. In each iteration, a constraint is popped, and abstract states are updated following the rules in Figures 8 and10. We also update the worklist according to the constraint dependence graph. Proof: The proof of Theorem 2 consists in a case analysis on the different constraints that can create the relation v 1 ∈ LT(v 2 ) in Figure 8 and 10. We go over a few cases. The proof goes by induction on the size of LT; if LT is empty, the property is trivially verified.

W L i pop(W L i ) LT(x) LT(y) LT(z) {x < y, y < z} - ∅ ∅ ∅ {x < y, y < z} x < y ∅ {x} ∅ {y < z, y < z} y < z ∅ {x} {y, x} {y < z} y < z ∅ {x} {y, x} {} - ∅ {x} {y, x} x < y y < z
• The constraint Strict less than x < v 2 updates the strict less than set of

v 2 . LT(v 2 ) = LT(v 2 ) ∪ LT(x) ∪ {x}.
For the sake of clarity, we let LT (v 2 ) be the strict less than set of v 2 before the update introduced by the constraint x < v 2 . Henceforth,

v 1 ∈ LT(v 2 ) if v 1 ∈ LT (v 2 ) or v 1 ∈ LT(x), or v 1 = x. If v 1 =
x, then we are done, due to the constraint x < v 2 . Otherwise, if v 1 ∈ LT(x), by induction, v 1 < x, and by transitivity we get v 1 < v 2 . In case

v 1 ∈ LT (v 2 ), by induction on LT (v 2 ), v 1 < v 2 .
In fact, since the strict less than set of v 2 is only growing up if updated, then if a property holds for its members once, it holds even after updates.

In other words, LT (v 2 ) may be an update of LT (v 2 ) in which we have inserted v 1 after resolving a constraint. In this case,

LT (v 2 ) ⊆ LT (v 2 ) ⊆ LT(v 2 ) with v 1 ∈ LT (v 2 ).
In the remaining of the proof, we shall be interested only on elements updating LT(v 2 ).

• The constraint non reflexive equal v 2 = x, updates LT(v 2 ) with LT(x): LT(v 2 ) = LT(v 2 ) ∪ LT(x). We focus on v 1 ∈ LT(x). By induction, we get v 1 < x. From Figure 7 we know that the constraint comes from a test. Thus, w.l.o.g, we can assume that this constraint is x T 1 = x, coming from a test x < x 2 . The condition v 1 < x is true before the test. Because the e-SSA conversion does not change the semantics of the target program, the condition is still true after renaming the operands of the test, thus v 1 < x T 1 = v 2 . • The constraint x = φ(x i ). We show the proof for the first case of Figure 10, the second one is similar and the third one is straightforward. In this case we have ∀x j ∈ Dom(x), x ∈ LT(x j ) implying LT(x) ∪ = LT(x j )

x j / ∈Dom(x)

.

x ∈ {x, x T , x F }. In the general case we would have:

LT(x) ∪ = n i=0
LT(x i ) that we can write

LT(x) ∪ = LT(x j ) x j / ∈Dom(x)
LT(x j )

x j ∈Dom(x) since x may take any of x i values. We want to prove that if

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017 y ∈ LT(x j )

x j / ∈Dom(x)

, then y < x under condition A. We let x j 0 ∈ Dom(x) such that x ∈ LT(x j 0 ). This means that x j 0 is defined as follows: x j 0 = x + a; a > 0. Hence, there exists a redefinition x i of x among φ operands such that x = x i and x j 0 = x i + a.

Since a > 0 we obtain x i < x j 0 with two possible situations for x i :

-x i ∈ Dom(x), then x ∈ LT(x i ) which gives again ∃x i such that x i < x i < x j 0 . -x i /
∈ Dom(x), then y ∈ LT(x i ). As there cannot be any infinite descending sequence of φ redefinitions, all instances of variable x are greater than x i . By induction on LT, y ∈ LT(x i ) gives y < x i and therefore y < x.

Answering Alias Queries

The final product of the techniques discussed in the previous section, is a table that associates each variable v with a set LT(v) of other variables that are less than v. This table gives us the means to prove that some pairs of pointers cannot dereference overlapping memory regions. We call this process pointer disambiguation. We use three different tests to show that pointers cannot alias each other. We define a query as the process of applying such test on a given pair of pointers.

Figure 12 illustrates the relationship between the three tests that we use to answer queries. If we cannot conclude that two pointers always refer to distinct regions, then we say -conservatively -that they may alias. Currently, we do not use our infra-structure to prove that two pointers must alias each other. The three pointer disambiguation checks that Figure 12 outlines are complementary and definitive. By complementary, we mean that none of them subsumes the others. By definitive, we mean that they all are conservatively safe: if any of these checks reports that pointers p 1 and p 2 do not alias, then this information, regardless of the results produced by the other checks, is enough to ensure that p 1 and p 2 refer to different locations. In the rest of this section, we provide further details about the three pointer disambiguation tests that we use. Briefly, we summarize them as follows, assuming that we want to disambiguate pointers p 1 and p 2 : PDD: If p 1 and p 2 belong into different pointer dependence digraphs, then they are said to be unrelated. PDDs are described in Section 4.1.

Less-Than: We consider two disambiguation criteria:

1. If p 1 ∈ LT(p 2 ), or vice-versa, then these pointers cannot point to overlapping memory regions.

2. Memory locations p 1 = p + x 1 and p 2 = p + x 2 will not alias if x 1 ∈ LT(x 2 ) or x 2 ∈ LT(x 1 ).

Ranges: If we can reconstruct the ranges covered by p 1 and p 2 , and these ranges do not overlap, then p 1 and p 2 cannot alias each other.

The Digraph Test

We have seen, in Section 4.1, how to group pointers that are related by C-style pointer arithmetics into digraphs. Pointers that belong to the same PDD can dereference overlapping memory regions. However, pointers that are in different digraphs cannot alias, because they reference different memory allocation blocks. Memory blocks are different if they have been allocated at different program sites. Example 10 illustrates this observation. We do not track abstract information that flows through memory locations (cf. Section 4.3). In other words, we do not generate constraints for information that comes out of load and store instructions. Similarly, our current implementation of the Digraph Test also does not consider pointers to pointers when building PDDs. Thus, our PDDs contain vertices that represent only top-level variables, e.g., variables that our baseline compiler, LLVM, represents in Static Single Assignment form. The consequence of this implementation decision is that currently we do not disambiguate pointers p1 and p2 in the following code snippet: {p1 = v + 4; *x = v; p2 = *x + 8;}, because we forgot the fact that v and *x represent the same memory location.

The Less-Than Test

The less-than test relies on the relations constructed in Section 4.4 to disambiguate pointers. This test is only applied onto pointers that belong to the same pointer dependence digraph. From Theorem 2, we know that if p 1 ∈ LT(p 2 ), then p 1 < p 2 whenever these two variables exist in the program. Along similar lines, we have p 1 < p 2 if x < y with p 1 = p + x and p 2 = p + y. Therefore, they cannot dereference aliasing locations. Example 11 illustrates the application of this test.

Example 11. We want to show that locations v[i] and v[j] in Figure 1a cannot alias each other. The CFG of function ins sort appears in Figure 4. In the for Pointer Disambiguation », accepted in Science of Computer Programming, 2017 CFG's low-level representation, v[i] corresponds to v i , and v[j] corresponds to v j . We know that LT(j T ) = {j 0 , i T } (as seen in Example 9) and v i = v + i T and v j = v + j T . Therefore, we can conclude that these two pointers v i and v j do not alias.

The Ranges Test

The so called Ranges test is a byproduct of the key components of the previous PDD test. This test consists in determining an expression of the range of intervals covered by two pointers, p 1 and p 2 , which share the same pointer digraph. If these two ranges do not intersect, then we can conclude that p 1 and p 2 do not alias. Algorithmically, this test proceeds as follows:

1. Find the closest common ancestor p a of p 1 and p 2 . We say that p a is the closest common ancestor of these pointers if, and only if, (i) it is an ancestor, e.g., dominates both p 1 and p 2 ; and (ii) for any other pointer p = p a that dominates p 1 and p 2 , we have that p dominates p a .

2. Rewrite p 1 and p 2 as function of p a . To this end, we repeat the following re-writing rule:

(a) If p x → e p i , i ∈ {1, 2} in the pointer dependence digraph, then we replace p i by p x + e.

(b) If p x = p a , then repeat step 2a.

3. Let p a + e 1 and p a + e 2 be the final expressions that we obtain for pointers p 1 and p 2 . If R(e 1 ) ∩ R(e 2 ) = ∅, then we report that p 1 and p 2 do not alias. Otherwise, we report that these pointers might alias.

Step 2 above is collapsing a path P(p i , p a ) = (p i , . . . , p a ) in the pointer digraph into a single edge p i → p a . This technique relies on the same ideas introduced by Paisante et al [START_REF] Paisante | Symbolic range analysis of pointers[END_REF]] to disambiguate pointers: if two pointers cover non-overlapping ranges, then they cannot alias. However, in terms of implementation, we use range analysis on the integer interval lattice. Paisante et al. use a symbolic range analysis. There is no theoretical limitation that prevents us from using a symbolic lattice to reuse Paisante et al.'s test. We have opted to use the simpler interval lattice because it is already available in LLVM, the compiler that we have used to implement our alias analysis. Example 12 shows how the range test works concretely.

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

Example 12. Consider the program in Figure14a. Our goal in this example is to disambiguate pointers p 2 and p 3 . We have that LT(p 0 ) = ∅, LT(p 1 ) = {p 0 }, LT(p 2 ) = {p 0 , p 1 } and LT(p 3 ) = {p 0 }. p 2 / ∈ LT(p 3 ) and p 3 / ∈ LT(p 2 ). The simple less than check is not able to disambiguate these pointers; hence, we resort to the range test. The dependence graph of Figure14a reveals that the lowest common ancestor of p 3 and p 2 is p 0 . P(p 2 , p 0 ) = (p 2 , p 1 , p 0 ) P(p 3 , p 0 ) = (p 3 , p 0 ). Our re-writing algorithm gives us that p 2 = p 0 +y+x, and p 3 = p 0 +z. Using range information, we get that: R(y 5,7]. These ranges do not intersect; therefore, p 2 and p 3 do not alias. The impact of range analysis on the precision of our method. In Section 3.2 we emphasized that the more precise the range analysis for integer variables that we use, the more precise the pointer analysis that we produce. Let us now detail how the difference in precision affects our analysis of pointers.

+ x) = R(y) + R(x) = [3, 4] and R(z) = [
1 void pdd ex(int N){ 2 if (N>0){
In Figure 15, we give a simple program where our goal is to disambiguate memory locations p[i] and p[i + 1]. Suppose that we have renamed variable i to i 0 at line 3 and to i 1 at 4 and memory locations p[i] and p[i + 1] to respectively p 0 and p 1 . We have P(p 0 , p) = (p 0 , p) and P(p 1 , p) = (p 1 , p).

The re-writing algorithm gives us that p 0 = p + i 0 and p 1 = p + i 1 .

The range analysis we use gives: R(i 0 ) = [0, N -1] and R(i 1 ) = [1, N ]. These ranges are over-approximated and make i 0 and i 1 possibly have the same value. Therefore, pointers p 0 and p 1 may dereference overlapping memory regions which is clearly not the case. However, if we adopt a more

Complexity of our Analysis

Our analysis can be divided into preprocessing steps and the actual alias tests. The first step in the preprocessing phase is the collection of constraints. It runs in linear time on the number of program instructions (O(i)), because it traverses the code, verifying if each instruction defines constraints. The second step of the preprocessing phase consists in building a pointer dependence graph. Additionally, pointer attributes are propagated along the graph. This step's complexity is O(i + p + e), with i being the number of program instructions, p the number of pointers and e the number of edges in the dependence graph. The final preprocessing step consists in running the work-list algorithm, and is equivalent to the problem of building transitive closures of graphs. Its worst case complexity is O(c 3 * v); c being the number of constraints and v the number of variables. Nevertheless, we have not observed this complexity empirically. The experiments that we perform in Section 7.2 will demonstrate that our algorithm runs in O(c) in general. This lower complexity is justified by a simple observation: a program variable tends to interact with only a handful of other variables. Thus, the number of possible dependencies between variables, in practice, is limited by their scope in the source code of programs that we analyze.

After all the preprocessing, each of our three alias tests has constant complexity. In other words, the relevant computations have been already performed on the preprocessing steps. Thus, each test just checks pointers attributes in a table. Keeping this table requires O(v 2 ) space, as the number of possible relations between variables is quadratic in the worst case. However, usually this table shall demand linear space. Figure 17: Comparison between three different alias analyses. We let s + b be the combination of our technique and the basic alias analysis of LLVM. Numbers in basicaa, sraa, s+b, and CF show percentage of queries that answer "no-alias". The X sign indicates that the exhaustive evaluator could not run with Andersen's analysis and aborted.

of alias queries. We notice that, even though the basic alias analysis disambiguates more pointers in several programs, our approach surpasses it in some benchmarks. It does better than basicaa on lbm and bzip2. Moreover, we improve basicaa's results considerably when both analyses run together on gobmk. Visual inspection of lbm's code reveals a large number of hardcoded constants. These constants, which are used to index memory, give our analysis the ability to go beyond what basicaa can do. This fact shows that LLVM still lacks the capacity to benefit from the presence of constants in the target code to disambiguate pointers. LLVM 3.9.0 uses the basic alias analysis by default, in contrast to LLVM 3.7.1, which does not use any pointer disambiguation strategy by default. Therefore, to fairly compare against CF, we consider numbers that both analyses get when combined with basicaa. This experiment reveals that there is no clear winner between our analysis and CF. In terms of total number of pointers disambiguated, our analysis is slightly more precise than Andersen's. We did not combine the two analyses, because they do not run in the same version of LLVM. However, we expect our analysis to increase the precision of Andersen's, as the latter does not deal with pointers with offsets. benchmarks. The Y-axis shows the number of queries answering no alias. The higher the bar, the better for the algorithm that we introduce in this paper.

ers. We say that an analysis solves a query if it is able to answer no alias for the pair of pointers that the query represents. When applied onto the programs available in SPEC CPU2006, both analyses, basicaa and sraa, are able to solve several queries. There is no clear winner in this competition, because each analysis outperforms the other in some benchmarks. However, in absolute terms, sraa is able to solve about twice more queries (3.6 10 7 vs 1.9 10 7 ) than basicaa. Because neither analysis is a superset of the other, when combined they deliver even more precision. The obvious conclusion of this experiment is that sraa adds a non-trivial amount of precision on top of basicaa. A measure of this precision is the number of queries missed by the latter analysis, and solved by the former.

Similar numbers are produced by benchmarks other than SPEC CPU2006. For instance, Figure 19 Each tick in the X-axis represents one benchmark. The Y-axis represents total number of queries (one query per pair of pointers), and number of queries in which each algorithm got a no-alias response.

sraa, this time on the 100 largest benchmarks available in the LLVM's test suite. Nevertheless, the results found in Figure 19 are similar to those found in Figure 18. Our sraa outperforms basicaa in the majority of the tests, and their combination outperforms each of these analyses separately in every one of the 100 samples. We have included the total number of queries in Figure 19, to show that, in general, the number of queries that we solve is proportional to the total number of queries found in each benchmark.

The Role of the Three Disambiguation Tests. Figure 20 shows how effective is each one of the three disambiguation tests that we have discussed in Section 5. In our staged approach, these tests work in succession: given a query q, first we use the PDD test of Section 5.1 to solve it. If this test fails, then we use the less-than test of Section 5.2 to solve q. If this second method still fails to disambiguate that pair of pointers, then we invoke the third test, based on range analysis and discussed in Section 5.3. As Figure 20 shows, most of the queries can be answered by simply checking that different pointers belong into different pointer dependence digraphs (PDDs). We should remind the reader that, out of our three checks, only PDD can disambiguate pointers to pointers: the other two checks are applied only on top-level variables, e.g., pointers allocated on the stack, which are represented in SSA form. Thus, it is expected that they will be less effective, as they have a more constrained data space to operate. Yet, the algebraic rules present in these two tests are essential in some benchmarks. In particular, the less-than check improves the PDD test by more than 30% on average, and in some cases, such as SPEC's lbm, it more than doubles its precision. In some cases, e.g., astar, perlbench and lbm, it is thanks to this test that we outperform basicaa.

Author

Figure 20 shows that the range analysis test is not very effective when compared to the other two tests. This behavior is due to two reasons. First, the range test is based solely on a numeric range analysis. Even though a numeric range analysis is enough to distinguish p 1 and p 2 defined as p 1 = p+1 and p 2 = p + 2, usually most of the offsets are symbols, not constants. The ability to use symbols to distinguish pointers is one of the key factors that led us to use a less-than check in this work. Second, the range test is the last one to be applied. Therefore, most of the queries have already been solved by the other two approaches by the time the range test is called. Specifically, there is a large overlap between the less-than test and the range test. We have observed that 11.97% of all the queries solved by the less-than check could also be solved by the range test. To fundament this last point, Figure 21 shows the total number of queries solved by each test. In this experiment, we run each test independently; hence, the success of one resolution strategy does not prevent the others from being applied. Nevertheless, the range test of Section 5.3 is still the least effective of the three approaches that we have discussed in this paper.

Runtime experiments

Figure 22 shows the runtime of our alias analysis on the 100 largest benchmarks in the LLVM test suite. As the figure shows, we are able to run our three tests for all the benchmarks, but eleven, in less than one second. Nevertheless, we observe a linear behavior. In Figure 22, the coefficient of determination (R 2 ) between the number of instructions and the runtime of our analysis is 0.8284. The closer to 1.0 is this metric, the more linear is the correlation between these two quantities.

Figure 23 discriminates the runtime of each disambiguation test. Our largest benchmark, 403.gcc, took about 200 seconds to finish. Such long time happens because, in the process of solving constraints, we build the variables. The figure also shows the total time taken by our alias analysis, which includes the time to construct the transitive closure of the pointer dependence digraph and collecting constraints. The LTC test accounts for most of the execution time within the pointer disambiguation phase of this experiment. This behavior is due to the growth check that we use to solve φ-functions. The range and PDD tests take similar runtimes. In Figure 24, the less-than check runs only if the PDD test fails. Once we have built LT relations, this test amounts to consulting hash-tables. As a final observation, we notice that the range test tends to be the least time-intensive among the three disambiguation strategies that we have. It takes less time because it only runs on pairs of pointers within the same PDD.

Figure 25 compares the time to run the three disambiguation tests in a staged fashion against the time to run these tests independently. The nonstaged approach is theoretically slower, because it always runs 3 × Q tests, whereas the staged approach runs Q + (Q -S 1 ) + (Q -S 1 -S 2 ), where S 1 are the queries solved by the first test, and S 2 are the queries solved by the second. Nevertheless, Figure 25

Related Work

Although alias analysis is an old subject in the compiler literature, it still draws the attention of researchers, who are interested in extending it to new domains [START_REF] Petrashko | Call graphs for languages with parametric polymorphism[END_REF]], making it yet more efficient [START_REF] Dietrich | Giga-scale exhaustive points-to analysis for java in under a minute[END_REF]], or using it as a fundamental building block of new optimizations [START_REF] Alves | Runtime pointer disambiguation[END_REF]] and static analyses [START_REF] Johnson | Exploring and enforcing security guarantees via program dependence graphs[END_REF]]. In such context, this work has the goal of designing a more precise alias analysis for languages with pointer arithmetics. To this end, we join two techniques that compilers use to understand programs: alias and less-than analyses. Both these techniques have spurred a long string of publications within the programming languages literature. We do not know of another work that joins both these research directions into a single path, except for the two papers that we have recently published, and that this document expands [START_REF] Maalej | Pointer disambiguation via strict inequalities[END_REF]; [START_REF] Paisante | Symbolic range analysis of pointers[END_REF]]. In the rest of this section we discuss how we extend that previous work or ours, and how we differ from the current state-of-the-art literature on alias and less-than analyses.

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

A Comparison Against our Previous Work

As we have mentioned before, this paper extends two previous publications of ours. We believe that the current materialization of our ideas is more solid than our first two endeavors in the field of pointer disambiguation. To fundament this claim, in what follows we describe our previous work, and explain how we have extended it.

Symbolic Range Analysis of Pointers. Our first attempt to disambiguate pointers with offsets appeared in CGO'16 [START_REF] Paisante | Symbolic range analysis of pointers[END_REF]]. In that work, we have used a symbolic range analysis to place bounds on memory regions. Here, we use a combination of numeric range analysis and a less-than analysis to achieve such a goal. Therefore, whereas in [START_REF] Paisante | Symbolic range analysis of pointers[END_REF]] we have adopted an algebraic implementation, based on symbolic ranges, to associate pointers with allocation sites, in this work we provide a geometric interpretation of such relations. Hence, we build the pointer dependence digraph to track relations between pointers and offsets. The experiments seen in Section 7 indicate that the Less-Than and Ranges checks, described in Section 5, are not only enough to solve every query that our previous implementation could handle, but lets us go beyond it. In Example 14 we show how the geometric formalization allows us to disambiguate some pairs of pointers that our previous art would not handle.

Example 14. Consider the control flow graph in Figure 26 in which our goal is to disambiguate pointers c 1 and d 1 . The allocation site loc 1 , associated to a 1 is unique in this program. It is created at a 1 = malloc() and propagated to other pointers. Using the analysis that we have introduced in [START_REF] Paisante | Symbolic range analysis of pointers[END_REF]] we would conclude that c 1 and d 1 "may alias" since GR(c 1 ) = loc 1 + [2, 4] and GR(d 1 ) = loc 1 + [4, 5], and the two ranges have a non-null intersection. The Ranges test that we have developed in this work, on the other hand, is able to disambiguate pointers c 1 and d 1 , because their common immediate ancestor is a 3 . Rewriting the pointers based on a 3 gives: c 1 = a 3 +2 or c 1 = a 3 + 3, and

d 1 = a 3 + 4. Since [2, 3] ∩ [4, 4] = ∅, then c 1 and d 1 cannot alias.
Pointer Disambiguation via Strict Inequalities. A precursor of our Less-Than check is described in our previous work [START_REF] Maalej | Pointer disambiguation via strict inequalities[END_REF]]. Our past experience has let us evolve that disambiguation technique along three different directions: for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

Example 15. In this example we illustrate the difference in precision between our current and previous work. We consider the program snippet in figure 27. In [START_REF] Maalej | Pointer disambiguation via strict inequalities[END_REF]

Algebraic Pointer Disambiguation Techniques

We call algebraic alias analyses the many techniques that use arithmetics to disambiguate pointers. Much of the work on algebraic pointer disambiguation had its origins on the needs of automatic parallelization. For instance, several automatic parallelization techniques rely on some way to associate symbolic offsets, usually loop bounds, with pointers. Michael Wolfe [ (Wolfe, 1996, Ch.7)] and Aho et al. [(Aho et al., 2006, Ch.11)] have entire chapters devoted to this issue. The key difference between our work and this line of research is the algorithm to solve pointer relations: they resort to integer linear programming (ILP) or the Greatest Common Divisor test to solve diophantine equations, whereas we do abstract interpretation. Even Rugina and Rinard [START_REF] Rugina | Symbolic bounds analysis of pointers, array indices, and accessed memory regions[END_REF]], who we believe is the state-of-the-art approach in the field today, use integer linear programming to solve symbolic Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

Less-Than Relations

The insight of using a less-than dataflow analysis to disambiguate pointers is an original contribution of this paper. However, such a static analysis is not new, having been used before to eliminate array bound checks. know of two different approaches to build less-than relations: Logozzo's [START_REF] Logozzo | Pentagons: a weakly relational abstract domain for the efficient validation of array accesses[END_REF]; [START_REF] Logozzo | Pentagons: A weakly relational abstract domain for the efficient validation of array accesses[END_REF]] and Bodik's [START_REF] Bodik | ABCD: eliminating array bounds checks on demand[END_REF]]. Additionally, there exist non-relational analyses that produce enough information to solve less-than equations [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]; [START_REF] Miné | The octagon abstract domain[END_REF]]. In the rest of this section we discuss the differences between such work and ours.

The ABCD Algorithm. The work that most closely resembles ours is Bodik et al.'s ABCD (short for Array Bounds Checks on Demand) algorithm [START_REF] Bodik | ABCD: eliminating array bounds checks on demand[END_REF]]. Similarities stem from the fact that Bodik et al. also build a new program representation to achieve a sparse less-than analysis. However, there are some key differences between that approach and ours. The first difference is a matter of presentation: Bodik et al. provide a geometric interpretation to the problem of building less-than relations, whereas we adopt an algebraic formalization. Bodik et al. keep track of such relations via a data-structure called the inequality graph. This graph is akin to the pointer dependence graph that we have used in this paper.

Bodik et al.'s technique, in principle could be used to implement our lessthan check; however, they use a different algorithm to prove that a variable is less than another. In the absence of cycles in the inequality graph, their approach works like ours: a positive path between v i to v j indicates that x i < x j . This path is implicit in the transitive closure that we produce after solving constraints. However, they use an extra step to handle cycles, which, in our opinion, makes their algorithm difficult to reason about. Upon finding a cycle in the inequality graph, Bodik et al. try to mark this cycle as increasing or decreasing. Cycles always exist due to φ-functions. Decreasing cycles cause φ-functions to be abstractly evaluated with the minimum operator applied on the weights of incoming edges; increasing cycles invoke maximum instead. Third, Bodik et al. do not use range analysis, because ABCD has been designed for just-in-time compilers, where runtime is an issue. Nevertheless, this limitation prevents ABCD from handling instructions such as x 1 = x 2 + x 3 if neither x 2 nor x 3 are constants. Finally, we chose to compute a transitive closure of less-than relations, whereas ABCD works on demand. This point is a technicality. In our experiments, we had to deal with millions of queries. If

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

For instance, our new algorithm handles some programming constructions that the original description of Pentagons did not touch, such as operations involving two variables on the right side, e.g., v = v 1 + v 2 .

Fully-Relational Our less-than analysis, ABCD and Pentagons are said to be semi-relational, meaning that they associate single program variables with sets of other variables. Fully-relational analysis, such as Octagons [START_REF] Miné | The octagon abstract domain[END_REF]] or Polyhedrons [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]], associate tuples of variables with abstract information. For instance, Miné's Octagons build relations such as x 1 + x 2 ≤ 1, where x 1 and x 2 are variables in the target program. As an example, Polly-LLVM6 uses fully-relational techniques to analyze loops. Polly's dependence analysis is able to distinguish v[i] and v[j] in Figure 1 (a), given that ji ≥ 1. Nevertheless, there are situations in which we are still more precise than Polly: for instance, it cannot disambiguate v[i] and v[j] in Figure 1 (b). These analyses are very powerful; however, they face scalability problems when dealing with large programs. Whereas a semi-relational sparse analysis generates O(|V|) constraints, |V| being the number of program variables, a relational one might produce O(|V| k ), k being the number of variables used in relations. As an example, current state-of-the art static analyzers such as Astrée [START_REF] Cousot | The ASTR ÉE analyzer[END_REF]] or Pagai [START_REF] Henry | Succinct representations for abstract interpretation: Combined analysis algorithms and experimental evaluation[END_REF]] assign unknown values for base addresses. These values permit such tools to derive relation between pointers, treating them as numerical values. In practice, these analyses work because they handle programs with very few pointers, like safety critical code.

Conclusion

This paper has described a novel algebraic method to disambiguate pointers. The technique that we have introduced in this paper uses a combination of less-than analysis and classical range analysis to show that two pointers cannot dereference the same memory location. We have demonstrated that our technique is effective and useful: its implementation on LLVM lets us increase the ability of this compiler to separate pointers by almost four times in some cases. And, contrary to previous algebraic approaches, our analysis scales up to very large programs, with millions of assembly instructions. We

  sort1 void partition(int * v, int N) { 2 int i, j, p, tmp; 3 p = v[N/2]; 4 for (i = 0, j = N -1;; i++, j--) { 5 while (v[i] < p) i++; 6 while (p < v[j]) j--;

Figure 1 :

 1 Figure 1: Two programs that challenge traditional pointer disambiguation analyses.

Figure 2 :

 2 Figure 2: Scalar replacement applied on Figure 1a. This kind of optimization is enabled by more precise alias analyses.

Figure 5 :

 5 Figure 5: Rules to generate the pointer dependence digraph.

Figure 6 :

 6 Figure 6: Pointer dependence graph of program in Figure 1a.

Figure 7 :

 7 Figure 7: Constraints produced for different statements in our language. The notation C ∪ = S is a shorthand for C = C ∪ S. v 1 and v 2 are constants or scalar variables.

Figure 8 :

 8 Figure 8: Rules to solve constraints.

  (a) increases along the execution of the program. Differently, variable x in Figure 9 (b) oscillates: it might increase or decrease, depending on the path along which the program flows. Both φ-functions exist in natural loops.

Figure 10

 10 Figure10illustrates the use of constraints imposed by φ-functions. We use conditional constraints to deal with them. A conditional constraint is

Figure 11 :

 11 Figure 11: Resolution of the constraints produced in Example 8. The order in which we solve constraints is dictated by their dependences in the CDG shown on the right. Each line depicts one step of the algorithm. WL i shows the worklist before we pop it.

Figure 12 :

 12 Figure 12: Steps used in the resolution of pointer disambiguation queries.

Example 10 .Figure 13 :

 1013 Figure13: Program that contains two different memory locations, which will give origin to two unconnected pointer dependence digraphs. For the sake of brevity, the program is kept in high level language.

Figure 14 :

 14 Figure 14: Disambiguating pointers with PDD and Ranges

AuthorFigure 16 :

 16 Figure16: Our analysis reports that pointers p2 and p3 may alias.

Figure 18 :

 18 Figure18: Comparison between SRAA and LLVM's basic alias analysis, showing how it increases LLVM's capacity to disambiguate pointers. The X-axis shows SPEC CPU2006 benchmarks. The Y-axis shows the number of queries answering no alias. The higher the bar, the better for the algorithm that we introduce in this paper.

Figure 19 :

 19 Figure19: Effectiveness of our alias analysis (SRAA), when compared to LLVMs basic alias analysis on the 100 largest benchmarks in the LLVM test suite (TSCV removed). Each tick in the X-axis represents one benchmark. The Y-axis represents total number of queries (one query per pair of pointers), and number of queries in which each algorithm got a no-alias response.

Figure 20 :

 20 Figure 20: How the three tests in SRAA compete to disambiguate pairs of pointers. The Y-axis denotes the number of disambiguated pairs of pointers.

AuthorFigure 21 :

 21 Figure 21: How three tests in SRAA separately compete to disambiguate pairs of pointers. The Y-axis denotes the number of disambiguated pairs of pointers.

Figure 22 :Figure 23 :Figure 24 :

 222324 Figure22: Comparison between the number of queries and total runtime (3 tests) per benchmark. X-axis represents LLVM benchmarks, sorted by number of instructions. We measure the SRAA runtime in seconds.

Figure 25 :

 25 Figure 25: Comparison between time (in seconds) needed to run SRAA selectively (non overlapping tests) and separately (disjoint tests)

  ], since x2 = x1 -4 is a subtraction, we rename variable x1 to x1 , where x1 is a fresh name. The final result of the analysis gives:LT(x1) = {x0}, LT(x1 ) = {x0, x2}, LT(x2) = {}, LT(x3) = {x0, x1 , x2}.Using the rules of Figure7and Figure8, we generate and solve constraints which gives us:LT(x1) = {x0, x2}, LT(x2) = {}, LT(x3) = {x0, x1, x2}.We want to disambiguate pointers p1 and p3 which are both defined from the same base pointer p. Our previous disambiguation check would answer "may alias" for those two pointers: however, this work we answer "no alias". The imprecision in our previous technique happens because we lost the relation between x1 and x3 after the renaming at the split point.

Figure 27 :

 27 Figure27: Illustration of the difference of precision between[START_REF] Maalej | Pointer disambiguation via strict inequalities[END_REF]] and the Less-Than test of this work.

The original description of e-SSA form uses the name π-function. We have adopted the name σ-functions, instead, following the work of Jeremy Singer on Static Single Information (SSI) form[START_REF] Singer | Static program analysis based on virtual register renaming[END_REF]]. Both notations define live range splitting instructions, which work for the same purpose

The ISO C Standard forbids relational comparisons between pointers that refer to different allocation blocks, even if said pointers have the same type (ISO, 9899:2011, Sec-6.5.8p5).

The name gep is a short form for get element pointer, the expression used to define a new pointer address in the LLVM compiler.

We have not mechanized any of the proofs we present in this paper; hence, they remain mostly informal. However, we believe that the intuition they provide helps readers to understand the essential components of our technique.

This list has been taken from the LLVM documentation, available at http://llvm.org/docs/AliasAnalysis.html in November 2016

Available at http://polly.llvm.org/

Acknowledgments

This project is supported by CNPq, Intel (The eCoSoC grant), FAPEMIG (The Prospiel project), by the French National Research Agency -ANR (LABEX MILYON of Université de Lyon, within the program "Investissement d'Avenir" (ANR-11-IDEX-0007)).

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

Theorem 1 (Termination). Constraint resolution always terminates.

Proof: 4

The worklist based solver reaches a fixpoint, because of two reasons. First, the updating of abstract states is monotonic. The inspection of Figures 8 and10 shows that the abstract state of variable v, e.g., LT(v) and GT(v) is only updated via union with itself plus extra information, if available. Second, abstract states are represented by points in a lattice of finite height: at most the less-than or greater-than set of a variable will contain all the other variables in the program.

Example 9. Example 4 showed us the constraints that we produce for the program in Figure 4. The solution that we find for that constraint system is the following:

For brevity, we omit GT sets.

Valid Solutions. We say that LT is a valid solution for a constraint system C, which models a program Prog if it meets the requirements in Definition 3. Program states, i.e., σ, are defined in Section 4.2.

Definition 3 (Valid Solution). We say that LT |= σ if, for any v 1 and v 2 , well-defined at σ, we have that:

Theorem 2 states that the solution that we find for a constraint system is valid. The proof of the theorem relies on the semantics of instructions. Each instruction I transforms a state σ into a new state σ . We shall not provide transition rules for these instructions, because they have an obvious semantics, which has been described elsewhere [ (Nazaré et al., 2014, Fig.3)].

Theorem 2 (Correctness of the Strict Less-Than Relations). Our algorithm produces valid solutions to the constraint system.

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017 precise abstract interpretation to generate i 0 and i 1 possible values such as We close this section with an example in which all the three tests that we have fail. In this case, we say that pointers may alias. In Example 13, below, we fail to disambiguate pointers, but they alias indeed. We might also fail to disambiguate pointers that do not alias. This type of omission is called a false positive.

Example 13. The program in Figure 16 is the same as the program in Figure 14a, except that the ranges of variables x, y and z have been modified. Due to this modification, none of our three previous tests can prove that p 2 and p 3 do not alias. The tests fail for the following reasons:

• Pointers p 2 and p 3 are derived from the same base pointer p 0 ; hence, they may alias due to Section 5.1's test.

• Neither p 3 ∈ LT(p 2 ) nor p 2 ∈ LT(p 3 ). Variables y and z, p 2 and p 3 'offsets, are not compared since the pointers are not directly related to the same base pointer; hence, p 2 and p 3 may alias according to the less-than check of Section 5.2.

• The range test of Section 5.3 does not fare better. We have that p 2 = p 0 + x + y and 3,7]. These two intervals intersect; hence, the range test reports that p 2 and p 3 may alias.

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

Evaluation

In this section, we discuss the empirical evaluation of our analysis and its implementation in the LLVM compiler, version 3.7.

All our experiments have been performed on an Intel i7-5500U, with 16GB of memory, running Ubuntu 15.10. The goal of these experiments is to show that: (i) our alias analysis increases the capacity of LLVM to disambiguate pointers; (ii) the asymptotic complexity of our algorithm is linear in practice and (iii) the three pointer disambiguation tests are useful.

Evaluation of the Precision of our Analysis

In this section, we compare our analysis against a pointer analysis that is available in LLVM 3.7: the so called basic alias analysis, or basicaa for short. This algorithm is currently the most effective alias analysis in LLVM, and is the default choice at the -O3 optimization level. It relies on a number of heuristics to disambiguate pointers 5 :

• Distinct globals, stack allocations, and heap allocations can never alias.

• Globals, stack allocations, and heap allocations never alias the null pointer.

• Different fields of a structure do not alias.

• Indexes into arrays with statically distinct subscripts cannot alias.

• Many common standard C library functions never access memory or, if they do it, then these accesses are read-only. • Stack allocations which never escape the function that allocates them cannot be referenced outside said function. Figure 17 shows how the LLVM's basic alias analysis, Andersen's inclusionbased analysis [And94], and our approach fare when applied on the integer programs in SPEC CPU2006 [START_REF] Henning | Spec cpu2006 benchmark descriptions[END_REF]]. Henceforth, we shall call our analysis sraa, to distinguish it from LLVM's basicaa and Andersen's analysis called CF (because it uses context free languages (CFL) to model the inclusion-based resolution of constraints). Our algorithm sraa is implemented in LLVM 3.7.1. However, CF is distributed in LLVM 3.9.0. Thus, in Figure 17, CF's numbers have been produced via LLVM 3.9.0. We emphasize that both versions of this compiler produce exactly the same number Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

Figure 26: Illustration of the difference in precision between [START_REF] Paisante | Symbolic range analysis of pointers[END_REF]] and the Ranges test of this work: the program in SSA form (left) and its PDD (right)

• Given the instruction v = v 1 + v 2 , plus the facts: v 1 > 0 and v 2 > 0, the final knowledge we obtain is different: in [START_REF] Maalej | Pointer disambiguation via strict inequalities[END_REF]], we only generate the constraint LT(v) = {v 1 } ∪ LT(v 1 ). In this work, we also generate the constraint v 2 < v (which is equivalent to LT(v) = {v 2 } ∪ LT(v 2 ). • In [START_REF] Maalej | Pointer disambiguation via strict inequalities[END_REF]] we consider integers and pointers as variables of scalar type while in the present implementation we differentiate the two types and handle separately the add and gep instructions present in the LLVM IR. This approach lets us avoid performing unnecessary comparisons. Hence, if v and v 1 are pointers and v 2 is an integer in v = v 1 + v 2 , then following the C standard, the comparison between v and v 2 is not allowed. • The third difference refers to the way we obtain a sparse implementation. In [START_REF] Maalej | Pointer disambiguation via strict inequalities[END_REF]], the new information associated with a variable is created at definition sites and is invariant throughout the analysis. In this work we update the abstract state of a variable whenever new facts are available in the program code. The main benefit of this approach is precision. Because we compute a transitive closure for the less-than relations that we collect, we can disambiguate more pointers. Example 15 illustrates this improvement.

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017 relations between variables. We speculate that the ILP approach is too expensive to be used in large programs; hence, concessions must be made for the sake of speed. For instance, whereas the previous literature that we know their experiments to pointers within loops, we can analyze programs with over one million assembly instructions.

There exist several different pointer disambiguation strategies that associate ranges with pointers [START_REF] Balakrishnan | Analyzing memory accesses in x86 executables[END_REF]; [START_REF] Balatsouras | Structure-sensitive points-to analysis for C and C++[END_REF]; [START_REF] Alves | Runtime pointer disambiguation[END_REF]; van Engelen et al. ( 2004 2016); [START_REF] Wilson | Efficient context-sensitive pointer analysis for c programs[END_REF]]. They all share a common idea: two memory addresses p 1 + [l 1 , u 1 ] and p 2 + [l 2 , u 2 ] do not alias if the intervals [p 1 + l 1 , p 1 + u 1 ] and [p 2 + l 2 , p 2 + u 2 ] do not overlap. These analyses differ in the way they represent intervals, e.g., with holes [START_REF] Balakrishnan | Analyzing memory accesses in x86 executables[END_REF]; [START_REF] Sui | Loop-oriented array-and fieldsensitive pointer analysis for automatic SIMD vectorization[END_REF]] or contiguously [START_REF] Alves | Runtime pointer disambiguation[END_REF]; [START_REF] Rus | Hybrid analysis: Static and dynamic memory reference analysis[END_REF]]; with symbolic bounds [START_REF] Nazaré | Validation of memory accesses through symbolic analyses[END_REF]; [START_REF] Paisante | Symbolic range analysis of pointers[END_REF]; [START_REF] Rugina | Symbolic bounds analysis of pointers, array indices, and accessed memory regions[END_REF]] or with numeric bounds [START_REF] Balakrishnan | Analyzing memory accesses in x86 executables[END_REF]; [START_REF] Balatsouras | Structure-sensitive points-to analysis for C and C++[END_REF]; [START_REF] Sui | Loop-oriented array-and fieldsensitive pointer analysis for automatic SIMD vectorization[END_REF]], etc. None of these previous work is strictly better than ours. For instance, none of them can disambiguate v[i] and v[j] in Figure 1 (b), because these locations cover regions that overlap, albeit not at the same time. Nevertheless, range based disambiguation methods can solve queries that a simple less-than approach cannot. As an example, strict inequalities are unable to disambiguate p 1 and p 2 , given these definitions: p 1 = p + 1 and p 2 = p + 2. We know that p < p 1 and p < p 2 , but we do not relate p 1 and p 2 . This observation has led us to incorporate a range-based disambiguation test in our framework.

Notice that there exists a vast literature on non-algebraic pointer disambiguation techniques. Our work does not compete against them; rather, it complements them. In other words, our representation of pointers can be used to enhance the precision of algorithms such as Steensgard's [START_REF] Steensgaard | Points-to analysis in almost linear time[END_REF]], [START_REF] Andersen | Program analysis and specialization for the c programming language[END_REF]], or even the state-of-the-art technique of Hardekopf and Lin [START_REF] Hardekopf | Flow-sensitive pointer analysis for millions of lines of code[END_REF]]. These techniques map pointers to sets of locations, but they could be augmented to map pointers to sets of locations plus ranges. Furthermore, the use of our approach does not prevent the employment of acceleration techniques such as lazy cycle detection [START_REF] Hardekopf | The ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code[END_REF]], or wave propagation [START_REF] Pereira | Wave propagation and deep propagation for pointer analysis[END_REF]].

Author Version of «Combining Range and Inequality Information for Pointer Disambiguation », accepted in Science of Computer Programming, 2017

we tried to answer them on demand, like ABCD does, then said experiments would take too long. We build the transitive closure to answer queries in O(1) in practice.

The Pentagon Lattice. Since their debut [START_REF] Logozzo | Pentagons: a weakly relational abstract domain for the efficient validation of array accesses[END_REF]; Logozzo and (2010)], Pentagons have been used in several different ways. For instance, Logozzo and Fähndrich have employed this domain to eliminate array bound checks in strongly typed programming languages, and to ensure absence of division by zero or integer overflows in programs. Moreover, [START_REF] Nazaré | Validation of memory accesses through symbolic analyses[END_REF]] have used Pentagons to reduce the overhead imposed by AddressSanitizer [START_REF] Serebryany | Addresssanitizer: a fast address sanity checker[END_REF]] to guard C against out-of-bounds memory accesses. The appeal of Pentagons comes from two facts. First, this abstract domain can be computed efficiently -in quadratic time on the number of program variables. Second, as an enabler of compiler optimizations, Pentagons have been proven to be substantially more effective than other forms of abstract interpretation of similar runtime [START_REF] Fähndrich | Static contract checking with abstract interpretation[END_REF]].

Pentagon, when seen as an algebraic object, is the combination of the lattice of integer intervals and the less-than lattice. Pentagons, like the ABCD algorithm, could be used to disambiguate pointers, similarly to the method we propose in this paper. Nevertheless, there are differences between our algorithm and Logozzo's. First, it is necessary to separate pointers from integer offsets in the resolution of the constraints that build less-than relations between variables. Second, the original work on Pentagons describe a dense analysis, whereas we use a different program representation to achieve sparsity. Therefore, the constraints that we produce to analyze programs are very different from in the original description of this lattice.

Third, Logozzo and Fähndrich build less-than and range relations together, whereas our analysis first builds range information, then uses it to compute less-than relations. That is to say, we have opted for decoupling the range analysis from the less-than analysis that forms the Pentagons' abstract domain. This choice was motivated more by engineering pragmatism, than by a need for precision or efficiency: it lets us combine different implementations of these static analyses more modularly. We have not found thus far examples in which one approach yields better results than the other; however, we believe that, from an engineering point of view, decoupling both analyses leads to simpler implementations. Finally, from a technical standpoint, we have added minor improvements on the original description of Pentagons.