1. Motivation: Impact of exceptions on accuracy

The polyhedral interface consists of several operators namely satisfiability test, inclusion test, projection, minimization, dual conversion, convex hull, intersection, difference and widening/narrowing. To perform each operator, many algorithms have been implemented. They can be used on integer or on rational domains to prove properties of programs. These algorithms often have a polynomial complexity but the worst-case exponential complexity hits sometimes. Unfortunately, this worse-case exponential complexity can block an analysis, especially when memory space and time are limited.

Adding information about a program should always result in more accurate analyses. It is however not true when 32-bit or 64-bit integers are used. When information is added, more overflows may occur in the linear algebra algorithms, then approximations must be made, resulting in longer and less accurate analyses. We take an example of a simple FORTRAN code, the polynomial in 6_fig:example_Polynomial03, and use PIPS to analyze this example.

Figure 1: Example: Polynomial code

Figure 2: Evolution of preconditions for Polynomial code over four iterations

Figure 3: Example: Evolution of transformers for Polynomial code

The preconditions and transformers are computed to obtain information about each variable $I,J,K$ independently for the tests on uninitialized variables. A technique used in PIPS in order to obtain more information is to compute several times the preconditions and transformers using their previously computed results. It is illustrated by the evolutions of transformers and preconditions in 6_fig:example_Polynomial03_pre and 6_fig:example_Polynomial03_tra where the results of four iterations are displayed for one of the statement in 6_fig:example_Polynomial03 (see the author's thesis for PIPS's transformers and preconditions analyses).

In 6_fig:example_Polynomial03_tra, we can see that the first transformer only contains information about the variable $I$ and its initial value: $I\char93 init \leq I$. The second transformer computed with the first precondition gives information not only about the variable $I$, but also the variable $J$: $I\char93 init \leq I, I + J\char93 init \leq I\char93 init + J$. In the same way, the transformer computed the fourth time seems richer of information than any previous one. However, if we look at the 6_fig:example_Polynomial03_pre, everything seems to be fine until the fourth loop: the information at the third loop, $6 \leq J, J \leq 300$, is lost at the fourth loop. It is because an overflow/magnitude exception has occurred.

Let us take another example. With a hardware configuration PC $2.4$GHz, $2$GB RAM, we analyze the program ocean.f with size of $4373$ LOC from the PerfectClub benchmark. We have $11916$ calls to satisfiability test and $424$ overflows; $3521$ calls last longer than three seconds and the largest constraint system contains $906530$ constraints. In fact, the computation on polyhedra can be very expensive: the larger the size of analyses becomes, the more problems appear. Our motivation is to quantify these problems.

Firstly, the operators manipulating the polyhedra at the lowest level should be the most efficient as possible. Note that in a typical program analysis section, an analyzer can call up to a hundred thousand elementary operations, or even more. Experiment shows that the impact is significant. It is however difficult to tell whether the implementations of these operators are efficient or not.

Secondly, heuristic-based approaches are thus needed to avoid infinite precision arithmetic and to maintain an execution speed fast enough to process large real applications reaching $100,000$ lines of code, with hundreds of variables linked by hundreds of constraints. The problem of time and memory space must then be reduced as much as possible. Moreover, constraint coefficient magnitude is also a complexity issue. Sub-optimal or heuristic solutions must be found when arithmetic overflows occur, in order to limit or control the information loss. Heuristics can only be found and validated through experimentation.

Finally, the dynamic behavior of programs is often controlled by integers, boolean variables and character strings. They can all be mapped on integers whereas linear algebra is mostly based on real and rational numbers, and linear algebra does not provide exact set operators very often. Different implementations of set operators by linear algebra algorithms can be exact, over- or under-approximation. Thus, accuracy and speed comparisons should be made.