4. Missing Operators

In this section, we list the operators that are available in some implementations but not in other implementations, as well as some recently proposed operators. In general we do not know why they are not available, except some special cases. We explain why some operators are important so that we suggest to implement them.

Since $C^3$, New POLKA and Octagon are libraries that are developed closely and used alongside with their analyzers, some operators which are not yet needed are not implemented. PPL library however proposes a very complete interface, which is designed for general purposes. For example, the operators corresponding to the int is_disjoint_from test, int expand_dimension and int fold_dimensions operators are available only in PPL.

For debugging purposes, only PPL and $C^3$ offer functions for the consistency check int is_OK operator, which is necessary. The mapping function that swaps dimensions is not available in Octagon. Also, polyhedral common objects such as the constraint and generating systems are not available in Octagon. Only in Octagon do we have low level access functions to its elements, which are octagonal constraints; although there are no generating systems, we can always compute them in theory.

Not available in $C^3$'s interface are the operators with _and_minimized, or _lazy versions, which perform the minimization inside the main operator. This is important at the algorithmic level since the minimization itself is an expensive operation which strongly depends on the size of its input. Let us consider an example by comparing the two approaches with the intersection operator: the first one computes the intersection of two given polyhedra to obtain a new polyhedron, then applies the minimization on this polyhedron; the second one applies the minimization on each of the two polyhedra, then computes the intersection of two minimized polyhedra. In the first case, if the result is a very large polyhedron, the minimization may need a very long time to execute, or exceptions may appear. The second case gives a more stable running time for average size inputs since they can be minimized faster.

At the same time, the absence of a version supporting a list of arguments for operators such as the projection or the convex hull in $C^3$, PPL and Octagon can penalize the performance of their implementation. For efficiency reasons, this is necessary since the computation of convex hulls is as follows: Consider three constraint systems $A, B$ and $C$. If we compute the convex hull of $A$ and $B$ to obtain a constraint system $D$, in order to pass it and $C$ to the same operator, we have to compute two more conversions to generating systems, which is not necessary because we can indeed merge several generating systems together into the final one, and then convert it to constraint system form. Moreover, since it is an expensive operator, we can have several possible approximations, thus we have to decide how to choose a specific version, for example, with an additional argument.

It is worse for with the widening operator, where a standard version is proposed in [HAL79], and another version is proposed later in [CH78]. These two versions are semantically different. In the PPL library, we have two other versions whose names are used in the signature of their function.

Moreover, we prefer having access to the numbers of equations and the numbers of inequalities by getNbInequalities and getNbEquations operators as in $C^3$ instead of having access only to the numbers of constraints as in PPL and New POLKA, since experience shows that heuristics can be based both on the numbers of equations or/and the numbers of inequalities.

We also propose new operators such as getAbstractSize or getAbstractWeight for the HQSet objects, which should be used to predict the running time of main operators on these objects. We also need to unify the printing functions, as well as the format conversion functions between different abstract domains and between different implementations of the same domain. New operators such as weak_update (see 4_sec:related_work), elapsed_time operator (see [MIN,MIN01] and [PAR,BRZaH02]) should be available in our interface.