Information about http://apron.cri.ensmp.fr/library/flyer.pdf
The APRON library for Numerical Abstract Domains …
Tags: abstract domain, abstract domains, abstract interpretation, apron, bertrand, client tools, cnrs, common interface, cri, ecole des mines, ecole normale suprieure, ecole polytechnique, experimental comparison, figs, generic services, level interface, numerical variables, static analysis, tures, uniform api,Pages: 2
Language: english
Display cached document
Page 1
Page 2
The APRON library for Numerical Abstract
Domains
Bertrand Jeannet1 , Antoine Min´2 , and al 3
e
1
INRIA
2 ´
Ecole Normale Sup´rieure
e
3 ´ ´
CRI/Ecole des Mines, Ecole Polytechnique, V´rimag/CNRS
e
The APRON library is dedicated to the static analysis of the numerical variables
of a program by Abstract Interpretation [1]. The aim of such an analysis is to
infer invariants about the values of numerical variables, like "at control point k,
variables x, y and z satisfy the property 1 x + y z".
In this context, the APRON library provides a common interface to various
libraries implementing numerical abstract domains.
Motivation and Principles. Many abstract domains have been designed and
implemented for analysing the possible values of numerical variables during the
execution of a program, cf. Figs. 12. Their implementations usually provides a
set of core functionalities. However their API diverge largely (datatypes, signa-
tures, . . . ), which does not facilitate their diffusion and experimental comparison
w.r.t. efficiency and precision aspects. The APRON library aims to provide:
A uniform API for existing numerical abstract domains;
A higher-level interface to the client tools, by factorizing functionalities that
are largely independent of abstract domains.
From an abstract domain implementor point of view, the benefits of the APRON
library are:
The ability to focus on core, low-level functionalities;
The help of generic services adding higher-level services for free.
For the client static analysis community, the benefits are an unified, higher-level
interface, allows experimenting, comparing and combining abstract domains.
(Rn )
Program
polynomial inequalities [2]
Front-end polynomial equalities [8]
linear inequalities [3]
(convex polyhedra) linear congruences [10]
Semantic Equations
linear equalities [9]
octahedra [4] 2-vars inequalities [5]
Abstract
Solver octagons [6]
Domain
simple congruences [11]
intervals [7]
Fig. 1. Typical static Fig. 2. Some abstract domains for numerical variables, par-
analyser tially ordered w.r.t. their expressiveness.
Underlying libraries & abstract domains
box
NewPolka PPL + Wrapper
intervals
convex polyhedra convex polyhedra
octagons
linear equalities linear congruences
octagons
Generic Services Developper interface
Linearisation of expressions Datatypes
Semantics: A (Rn )
Floating-point semantics Coefficients dimensions and space dimensionality
over exact arithmetics Expressions
Constraints Variables and Environments
C API Generators
Abs. values Semantics: A (V R)
OCaml binding C++ binding User interface
Fig. 3. Organisation of the APRON library
Implementation. Fig. 3 depicts the organisation of the APRON library. The
existing underlying libraries connect to the developper interface, using domain-
independent datatypes, and exploiting common services. Independent libraries
like PPL [12] can be connected using a wrapper. Client tools connect to the
higher-level user interface, where variables (or addresses) and environments re-
place geometrical notions like dimensions and space dimensionality.
The APRON library is written in C ANSI, with an object-oriented and thread-
safe design. Both multi-precision and floating-point numbers are supported. A
wrapper for the OCaml language is available, and a C++ wrapper is on the way.
It is distributed under the LGPL license and available at http://apron.cri.
ensmp.fr/. Future plan includes the connection of other abstract domains, as
well as a generic combinator for the reduced product of abstract domains.
References
1. Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of
Logic Programming 13(23) (1992)
2. Bagnara, R., Rodr´ iguez-Carbonell, E., Zaffanella, E.: Generation of basic semi-algebraic invari-
ants using convex polyhedra. In: SAS'05. Volume 3148 of LNCS.
3. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a pro-
gram. In: POPL'78,
4. Claris´, R., Cortadella, J.: The octahedron abstract domain. In: SAS'04. Volume 3148 of LNCS.
o
5. Simon, A., King, A., Howe, J.: Two variables per linear inequality as an abstract domain. In:
LOPSTR'02. Volume 2664 of LNCS.
6. Min´, A.: The octagon abstract domain. In: AST'01 in Working Conference on Reverse Engi-
e
neering 2001
7. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: 2nd Int.
Symp. on Programming, Dunod, Paris (1976)
8. M¨ ller-Olm, M., Seidl, H.: Program analysis through linear algebra. In: POPL'04.
u
9. Karr, M.: Affine relationships among variables of a program. Acta Informatica 6 (1976)
10. Granger, P.: Static analysis of linear congruence equalities among variables of a program. In:
TAPSOFT'91. Volume 493 of LNCS.
11. Granger, P.: Static analysis of arithmetical congruences. Int. Journal on Computer Mathematics
30 (1989) 165190
12. Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the
Parma Polyhedra Library. In: SAS'02. Volume 2477 of LNCS.