Representation: Summaries

We represent each array access by a system of integer linear inequalities. An array summary is a set of such systems. For example, consider the following loop nest.

The region of array A written by a single execution of the statement is represented by set containing one system of inequalities, parameterized by the program variables M and N, and normalized loop index variables i and j:

The included contextual constraints on program variables and loop indices are provided by the scalar context analysis.

Intuitively, a set is necessary because different accesses to an array may refer to distinctly different regions of the array. Mathematically, many of the operators applied to array summaries result in non-convex regions, which cannot be precisely described with a single system of inequalities. To maintain efficiency, we merge systems of inequalities whenever we can guarantee no loss of information will result. The following basic operations are defined on array summaries. Operations marked are not exact.

Empty? . A set of systems is empty iff all systems in the set are empty. A system of inequalities is empty if there are no integer solutions that satisfy the system. We use a Fourier-Motzkin pair-wise elimination technique with branch-and-bound to check for the existence of an integer solution to a system of inequalities. If no solution exists, the system is empty.

Contained? ). A set of systems is contained in another, iff each system in the first set is contained in a single system in the other set. This is conservative as it may return a false negative. A system of inequalities a is contained in a system of inequalities b if and only if a combined with the negation of any single inequality of b is empty.

Union . The union of two sets of systems simply unions the two sets, then simplifies the set using the following two heuristics:

• If there are two systems a and b in the set such that , then a is removed from the set.

• If two systems are rectilinear and adjacent, they are combined to form a single system.

In practice, these heuristics keep the sets a manageable size and increase the precision of the Contained? operator. Since the union of two convex regions can result in a non-convex region, a set is necessary to maintain the precision of the union operator.

Intersection . The intersection of two sets of systems is the set of all non-empty pairwise intersections of their elements. Intersection of two systems of inequalities simply concatenates the inequalities of the two systems.

Subtraction .
The subtraction of two sets of systems subtracts all systems of the second set from each system in the first. Two systems are subtracted using a heuristic: is exact when or or both are simple rectilinear systems; otherwise it is approximated as a.

Projections eliminates the variable v from the constraints of all the systems in set A by applying the Fourier-Motzkin elimination technique to each system. Each system can be viewed as the integer points inside a n-dimensional polytope whose dimensions are the variables of a and whose bounds are given by the inequalities of a; this polytope is projected into a lower-dimensional (n-1) space where the integer solutions of all remaining dimensions remain unchanged.

One use of projection is to summarize the effects of array accesses within a loop. For example, for the system of inequalities representing the access to array A shown above, projections are used to generate systems of inequalities representing the array accesses for each loop in the nest. In some cases, eliminating a variable may result in a larger region than the actual region. In the example, eliminating the constraint will lose the information that must be even. For this reason, analysis introduces an auxiliary x in to retain this constraint.