Implémentation du domaine asbtrait numérique TVPI pour APRON
Résumé
This paper extends the work of Simon, King, and M. Howe and proposes an implementation of the relational numerical abstract domain TVPI (Two Variables Per Inequality) for the APRON library. This domain expresses invariants of the form ax + by ≤ c, for any a, b and c. The interest of this domain lies in its attractive cost/accuracy ratio due mainly to three points: (1) its convenient representation (2) the relatively low cost of its operations (3) the existence of effective geometric algorithms specific to the TVPI case. In the implementation, we had to deal with some issues that have not been addressed in detail in Simon, King, and Howe , and to make technical choices in order to achieve the theoretical running-time. We also had to make choices on how to approximate test and assignment operations (two basic operations in a static analyzer) when the number of variables in a linear expression is greater than two.
Ce document étend le travail effectué par Simon, King, et M. Howe et propose une implémentation du domaine abstrait numérique relationnel TVPI (Two Variables Per Inequality) dans la bibliothèque APRON. Ce domaine permet d'exprimer des invariants de la forme ax + by ≤ c pour a, b, et c quelconques. L'intérêt de son implémentation réside dans son rapport coût/précision convenable. Ce dernier est dû à sa représentation avantageuse sur machine, au coût relativement modeste de ses opérations, et aussi à certains outils algorithmiques et géométriques spécifiques au cas de deux variables par inégalité. Dans l'implémentation, nous avons eu à traiter certains points qui n'ont pas été décrits en détail dans Simon, King, et Howe, ainsi que de faire des choix techniques afin de respecter la complexité prouvée pour le TVPI. Nous avons aussi eu à faire des choix d'approximations pour implémenter les opérations de test et d'affectation (deux opérations de base dans un analyseur statique) dans le cas où le nombre de variables dans une expression linéaire est supérieur à deux.