5. A Forth Issue: Variable Assignment

In this section, we present an example that shows one of the difficulties encoutered to use the Octagon library in the PIPS analyzer. We consider two interfaces, one of PIPS's $C^3$ library and the other of the octagon library [MIN,MIN01].

In order to keep a generic architecture for PIPS, the oct_t* oct_assign_variable() operator which models the assignment command should belong to a higher level than the intersection or union of octagons. It is because the assignment command is independent from the abstract domain used, which can be, for instance, octagonal or polyhedral.

Moreover, a wrapping for octagon is preferable to modification of the existing interface. Accordingly, we have tried to implement the operator oct_t* oct_assign_variable() from octagon's lower level primitives, i.e. from the API of the library without oct_t* oct_assign_variable() itself. Retrospectively, it is not the best approach to deal with the problem since there are other operators in PIPS that are more interesting to implement using the octagons, but it is already complex. In fact, we encounter three problems:

• If we encode $I:=1$ and $J:=2$ independently, as we do in PIPS's bottom-up approach for transformers, $I$ and $J$ are represented by the first dimension in their corresponding octagon. Therefore, when we want to combine these two, we have to modify the binding of variable names to dimensions and to modify at least one octagon.

  It is even worse when we have to translate a function call like $I = f(K)$, assuming $f$'s transformer known.

• If we want to combine $I:=I+1$ with the transformer for $I:=1$ (the author's thesis for transformers), we have to play, at least temporarily, with the number of dimensions by adding something to represent the old value, the temporary intermediate value and the new value of $I$.

• In the operator oct_t* oct_assign_variable() of the octagon library, sometime non-octagonal constraints may appear. In this case they are approximated by their interval bounds. This kind of heuristics should not appear at a high level, which stops us from rewriting oct_t* oct_assign_variable() in a generic way.

To make it short, we need an operator to rename variables to solve the first two problems. For the third problem, we should find another way to approximate the result using only the API.

Finally, we notice that though POLYLIB is used in $C^3$, the only used part is the implementation of the Chernikova algorithm. The variable assignment is one of reasons that stop us from exploiting more effectively this library.