General choices

Interface levels
Programming language
Compatibility with threads
Interruptions
Memory management
Programming style
Number representation

Interface levels

There are two main goals for the APRON interface: efficiency of the implementations, and ease of use for the user. In addition, code duplication between libraries should be avoided. As a consequence, two levels were identified:

Level 0

Choices are guided by the efficiency and the precision of the operations;

Level 1

Choices are guided by ease of use, and code factorization.

The level 0 is directly connected to the underlying (existing) library. It includes all the operations that are specific to an abstract domain and whose code cannot be shared. The interface should be minimal, unless there is a strong algorithmical advantage to include a combination of more basic operations.

The higher levels offers additional functionalities that are shared by all the library connected to the level 0. For instance:

• managing correspondance between numerical dimensions and names (characters strings or more generally references);
• abstraction of non linear expressions in interval linear expressions;
• automatic call to redimensioning and permutation operations for computing P(x,y)/\Q(y,z).

Combination of abstract domain is possible at the level 0. One can implement for instance the cartesian or reduced product of two different abstract domains, the decomposition of abstract values into a product of values of smaller dimensionality, ...

Programming language

The reference version of the interface is the C version of the interface:

• C can be easily interfaced with most programming languages;
• Most of the existing libraries implementing abstract domains for numerical variables are programmed in C or C++.

An OCAML version is already available. The interface between OCaml and C is even generic and any libraries can benefit from it by providing the glue for just one function (see XX).

Compatibility with threads

In order to ensure compatibility with multithreading programming, a context is explicitly passed to functions in order to ensure the following points:

• the transmission of data specific to each library (non-standard options, workspace, ...);
• the transmission of standard options (selection of algorithms and their precision inside a library);
• the management of exceptions (implemented as error codes in the C interface) (not_implemented, invalid_argument, overflow, timeout, out_of_space).

Interruptions

Interruptions mechanism is have possible for different cases:

timeout

if the execution time for an operation exceeds some bound;

out_of_space

if the space consumption for an operation exceeds some bound;

overflow

if the magnitude or the space usage of manipulated numbers exceeds some bound;

not_implemented

if the operation is actually not implemented by the underlying library;

invalid_argument

if the arguments do not follow the requirements of an operation.

For instance, in a convex polyhedra library, the out_of_space exception allows to abort an operation is the result appears to have too many constraints and/or generators. If this happens, one can redo the operation with another (less precise) algorithm. The overflow may be useful when effective overflows are encountered with machine integers or when multiprecision rational numbers have too large numerators and denominators. The not_implemented exception allows for a library to be linked to the interface even if it does not provide some operation of the interface.

When an interruption occurs, the function should still return a correct result, in the abstract interpretation sense: it should be a correct approximation, usable for next operations in the program. The top value is always a correct approximation.

Memory management

Memory is managed differently depending on the programming language. Currently:

• No automatic garbage collection in the C interface
• Use of the OCAML runtime garbage collector in the OCAML interface

Programming style

Both functional and imperative (i.e., side-effect) signatures are supported for operations. This allows to optimize the memory allocation and to use whichever version is more convenient for an user and the used programming language.

Number representation

Inside a specific library, any number representation may be used (floating-point numbers, machine integers, multiprecision integers/rationals, ...). Existing libraries often offers the possibility to select different representations.

However, in the interface, this representation should be normalized and independent of underlying libraries, without being restrictive either. As a consequence, the interface offers the choiced between

• GMP multiprecision rationals (which implements exact arithmetic);
• and machine floating-point numbers (double).