[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

Functionalities of the interface at level 0

Representation of an abstract value  
Semantics of an abstract value  
Dimensions  
Other datatypes  
Control of internal representation  
Printing  
Serializaton/Deserialization  
Constructors  
Tests  
Property extraction  
Lattice operations  
Assignement and Substitutions  
Operations on dimensions  
Other operations  

Representation of an abstract value

At the level 0 of the interface, an abstract value is a structure @verbatim struct ap_abstract0_t { ap_manager_t *manager; /* Explicit context */ void *value; /* Abstract value representation (only known by the underlying library) */ } The context is allocated by the underlying library, and contains an array of function pointers pointing to the function of the underlying library. Hence, it indicates the effective type of an abstract value.

The validity of the arguments of the functions called through the interface is checked before the call to effective functions. In case of problem, an invalid_argument exception is raised.

Semantics of an abstract value

The semantics of an abstract value is a subset

X of N^p x R^q

Abstract values are typed according to their dimensionality (p,q).

Dimensions

Dimensions are numbered from 0 to p+q-1 and are typed either as integer or real, depending on their rank w.r.t. the dimensionality of the abstract value.

Taking into account or not the fact that some dimensions are integers is left to underlying libraries. Treating them as real is still a correct approximation. The behaviour of the libraries in this regard may also depend on some options.

Other datatypes

In addition to abstract values, the interface also manipulates the following main datatypes:

scalar (number)
Either GMP multiprecision rationals or C double.
interval
composed of 2 scalar numbers. With rationals, plus (resp minus) infinity is represented by 1/0 (resp -1/0). With double, the IEEE754 is assumed and the corresponding standard representation is used.
coefficient
which is either a scalar or an interval.
(interval) linear expression
The term linear is used even if the proper term should rather be affine. A linear expression is a linear expression in the common sense, using only scalar numbers. A quasi-linear expression is a linear expression where the constant coefficient is an interval. An interval linear expression is a linear expression where any coefficient may be an interval. In order to have a unique datatype for these variations, we introduced the notion of coefficient described above.
"linear" constraints
"Linear" constraints includes proper linear constraints, linear constraints in which the expression can be possibly an interval linear expression, linear equalities modulo a number, and linear disequalities.
generators
A generator system for a subset of X\subseteq R^n is a finite set of vectors, among which one distinguishes points p_0,\ldots,p_m and rays r_0,\ldots,r_n, that generates X:
X = { lambda0 p0 +...+ lambdaM pM + mu0 r0 +...+ muN rN | lambda0 +...+ lambdaN = 1 and forall J : muJ >= 0 }
The APRON datatype for generators distinguishes points (sum of coefficients equal to one), rays (positive coefficients), lines (or bidirectional rays, with unconstrainted coefficients), integer rays (integer positive coefficients) and integer lines (integer coefficients).

Control of internal representation

We identified several notions:

Printing

There are two printing operations:

The printing format is library dependent. However, the conversion of abstract values to constraints (see below) allows a form of standardized printing for abstract values.

Serializaton/Deserialization

Serialization and deserialization of abstract values to a memory buffer is offered. It is entirely managed by the underlying library. In particular, it is up to it to check that a value read from the memory buffer has the right format and has not been written by a different library.

Serialization is done to a memory buffer instead of to a file descriptor because this mechanism is more general and is needed for interfacing with languages like OCAML.

Constructors

Four basic constructors are offered:

Tests

Predicates are offered for testing

Property extraction

Some properties may be inferred given an abstract values:

Notice that the second operation implements linear programming if it is exact. The third operation is not minimal, as it can be implemented using the first one, but it was convenient to include it. But the fourth operation is minimal and cannot be implemented using the second one, as the number of linear expression is infinite.

Lattice operations

Assignement and Substitutions

Parallel assignement and substitution ar enot minimal operations, but for some abstract domains implementing them directly results in more efficient or more precise operations.

Operations on dimensions

Other operations

Widening, either simple or with threshold, is offered. A generic widening with threshold function is offered in the interface.

Topological closure (i.e., relaxation of strict inequalities) is offered.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

This document was generated on September, 10 2009 using texi2html