4. A Third Issue: Octagons vs Polyhedra

The octagonal domain is recent [MIN04], although similar ideas were used to speed up convex array region analysis [HK91]. It was introduced to avoid the high complexity of polyhedral operators without losing too much accuracy. Because it is a simpler domain, it is less precise but offers a shorter run time when used in static analyzers. Indeed, its operators execute faster with polynomial instead of exponential complexity.

The current implementation of the octagon library has an interface that is incompatible to existing polyhedral interfaces, even though this library is used in ASTREE [AST,BCC$^$03] in order to replace the more expensive polyhedral domain. However, since every octagon is also a polyhedron , we expect to use the octagonal domain instead of polyhedral one without major difficulties.

While the dual conversion with Minkowski representation is very important for polyhedral implementations, e.g. the most efficient algorithm for the convex hull operator implements this approach, it is not vital for the octagonal domain. We can compute the generating system of an octagon, by some algorithm derived from Chernikova's one, for example, but it does not imply a better performance.

When we study some missing operators, i.e. the functions that are available in the polyhedral interface but not in the octagonal interface, e.g. the dimension permutation operators, fortunately no algorithmic problem has been found yet: we can implement these missing operators without difficulty. Nonetheless, for some operators such as the closure operator, implementation efficiency suggests some differences in levels for these interfaces, since low-level oparations are required.

In fact, we can find some similarities between the Octagon library's interface and New POLKA's, since the former was built based on the latter. We even find the operators that convert an octagon to a polyhedron, and vice versa, which indeed help the move towards a common interface. But it is hardly enough: we cannot use them interchangeably, thus they are not compatible. Fortunately, the participation of the two groups in APRON project (4_sec:related_work) will make it easier to adapt to a new common interface.

We consider in the next section a problem with the Octagon library's interface, because dimension permutation operators are not available .