4. Conclusion

In this chapter, we have presented our approach to deal with compatibility problems in the context of static analyzers. The incompatibility of existing proving engines, i.e. existing abstract domain libraries, stop us from effectively using them.

Our proposition for a common interface for abstract set manipulation engines, described in 4_sec:HQ_interface, helps to identify the problems, and presents our very first solutions.

It consists of a prototype for a common interface, and practical issue-related documents that reveal different approaches in existing implementations, from which concrete decisions can be made. We have also introduced the state of the art of the APRON project, which is strongly related to this dissertation, in 4_sec:related_work.

We compare our HQ approach and the APRON approach at the end of 4_sec:related_work. In fact, the HQ interface was presented in APRON meetings, and helped starting deeper discussions on the subject. Our proposition is divided into two parts.

The first part directly addresses the interface with imperative signatures, which should describe what we need, how to present, introduce and expose it as clearly as possible. We discuss the name of operators, what this function does, why we need other versions of it, when we apply approximation, whether we should have a list of arguments instead of only one argument, etc. the level of this function, etc. These problems are already complex, thus they should be separated from the second part.

The second part, which is as important as the first part, is where we discuss implementation issues such as how we handle exceptions, how we manage the memory, etc. In fact, there are many ways to deal with this kind of problems, so finally we just have to pick one that is the most appropriate. For example, from the initial HQ's signatures, we can use the JNI (Java Native Interface) tool to generates its C signatures. However, this approach is not satisfying since the generated code is not easy to understand, so we can consider building a set of rules for this conversion. Other problems such as memory management, destructive functions, destructive arguments are described in order to be decided later.

Recent developments show that current polyhedral libraries such as POLYLIB, PPL and APRON, as well as polyhedra-related libraries such as Octagon library, are being worked on their interfaces. Likewise, new abstract domains are introduced, e.g. in [FER05], which may have an important impact on our common interface. For the time being, the very first common interface is defined by the APRON project.

Some complex problems such as product of domains or the Presburger domain are not dealt with. At first, the implementation of the common interface will help the three static analyzers described in the author's thesis to profit from those abstract domains. Then, given the compatibility among the libraries, other analyzers using abstract interpretation can use them, too.

We intend to continue working on the HQ interface, where the compatibility problems are documented , and some adaptations from the APRON's prototype are also encouraged. In the next chapter, we study the interface of the polyhedral domain, the underlying algorithms and related problems.