2. A First Issue: $C^3$, New POLKA, PPL and POLYLIB - Different Contexts

Being the most used abstract domain for advanced static program analyses, the polyhedral domain is implemented by several libraries containing many algorithmic improvements introduced over the years. However, existing polyhedral interfaces are not compatible as shown later in 4_subsec:incompatibility_important_operators. Different choices were made by developers such as naming conventions, algorithms, exception handlers, etc. Due to their completeness, we choose to compare four polyhedral libraries namely $C^3$ [PIPa,CAI00], New POLKA [JEA,JEA00], PPL [PAR,BRZaH02] and POLYLIB [LOE,Wil].

These four polyhedral libraries were designed and developed in different contexts for different languages C, C++, CAML. New POLKA and $C^3$ have been developed and used closely with their static analyzers, respectively NBAC and PIPS, as fundamental algebraic engines, while POLYLIB and PPL libraries are somehow independently developed. This leads to some particularities. For example, the PIPS analyzer does not use any widening operator, therefore its $C^3$ library does not implement this operator .

New POLKA was formerly based on POLKA and POLYLIB implementation; however its interface and memory management is different from POLYLIB's. POLYLIB, designed for automatic parallelization, code transformations and code synthesis, used as a part of the $C^3$ library, does not provide a complete interface for static analyzers. For example, neither the manipulation of the dimensions of polyhedra nor the widening operator are not present in its interface. It however implements the computation of symbole Ehrhart polynomials and Z-polyhedra manipulations, which can be used for specific purposes.

In fact, the Ehrhart polynomials, which are a special kind of polynomials, form another abstract domain, where the set of integer points to be counted lies inside a union of rational convex polytopes, thus the number of points can be formulated by an Ehrhart polynomial. The Z polyhedra which are intersections of polyhedra with the integer lattice also form an abstract domain. In our work, we do not study explicitly these domains because of their given lower priority.

The PPL library, while being used by different projects such as the CHINA project [CHI,PAR,BRZaH02], the Action Language Verifier [ALV,BYK01], etc., will not have its final interface before version $1.0$, according to the authors [PAR,BRZaH02]. Version $0.7$ is the most recent version we had access to.

As a result, to construct a common interface for the above libraries, adaptations must be made for each and every library. In the next section, we consider a problem concerning not only the polyhedral implementations but all abstract domain implementations used in static analyzers.