3. Implementation-related Problems

Exception handlers in the four libraries are different, since PPL uses $C++$, and the others use $C$ or $Ocaml$. Even with the $C$ language, we have totally different ways of handling exceptions. Sub-libraries used in the four libraries are also different: we have for example the GNU multi-precision with floating point and integer versions. The control of memory space used by a Max Object Size is different.

For debugging purposes, variable names (strings) are preferable to numerical dimension, i.e. $0 \rightarrow (n-1)$ or $1 \rightarrow n$, but their use in some libraries is not supported. Furthermore, when the objects, which are passed to the abstract domain engine by the analyzer, are lost by side effects, we cannot debug them inside the engine, i.e. the abstract domain library, itself . If every operator made backups of those objects, it would reduce the overall performance. If not, since exceptions are unpredictably raised, we might not be able to restore the objects for debugging. We then suggest the use of two versions for every operator that modifies its inputs. The debugging version should make copies of the inputs, so that in case of exceptions, it can restore the original ones.

As we have seen in 4_subsec:polyhedra_implementation, POLYLIB's implementation for timeout management was refused. However, it is important since our examples in the author's thesis demonstrate that most of the polyhedral operators can be blocking. Each operator has its own complexity, hence a different value of timeout. It is then required to use an additional argument for every operator or a timeout field of values. We propose to use only one parameter $p$ to define the timeout value, under user control, and a field of heuristic coefficients, since it is simple and flexible enough. For example, the emptiness test could require a timeout value of $2p$, the union operator $5p$, the projection $3p$, and so on. Notice that the values of heuristic parameters need to be defined throughout experiments.

In HQ, we decided to support the automatic selection by default and overridden selection by user, for algorithm selection, i.e. which algorithm to use among several algorithms. We also decide to interface explicitly the integer and rational algorithms. The minimized/lazy versions are made automatically without any additional user input. Memory management issues such as version recycle, reference counter and control of used memory space are explicit.

The problems raised by differences of 32-bit, 64-bit, 128-bit and gmp (GNU multi-precision) computation are not dealt with in our interface, but at compilation time, we study the arithmetic differences in more details with the polyhedral domain. In HQ, we use an abstract type HQValue for numerical values, which hides these problems. Thus, this is an open problem. The approach that uses two arithmetics at the same time, implemented in LRS library, is not taken into account. We do not discuss the approach using product of abstract domains in this work, as well as recent approaches to speed up polyhedral operators such as Cartesian factorization, or dedicated servers for expensive operations that permit execution of several algorithms in parallel.