Next: Functionalities of the interface at level 1, Previous: General choices, Up: APRON Rationale and Functionalities
Next: Semantics of an abstract value, Previous: Functionalities of the interface at level 0, Up: Functionalities of the interface at level 0
At the level 0 of the interface, an abstract value is a structure
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.
Next: Dimensions, Previous: Representation of an abstract value, Up: Functionalities of the interface at level 0
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).
Next: Other datatypes, Previous: Semantics of an abstract value, Up: Functionalities of the interface at level 0
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.
Note: 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.
Next: Control of internal representation, Previous: Dimensions, Up: Functionalities of the interface at level 0
In addition to abstract values, the interface also manipulates the following main datatypes:
Either GMP multiprecision rationals or C double.
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.
which is either a scalar or an interval.
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 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.
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).
Next: Printing, Previous: Other datatypes, Up: Functionalities of the interface at level 0
We identified several notions:
Next: Serializaton/Deserialization, Previous: Control of internal representation, Up: Functionalities of the interface at level 0
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.
Next: Constructors, Previous: Printing, Up: Functionalities of the interface at level 0
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.
Next: Tests, Previous: Serializaton/Deserialization, Up: Functionalities of the interface at level 0
Four basic constructors are offered:
Next: Property extraction, Previous: Constructors, Up: Functionalities of the interface at level 0
Predicates are offered for testing
Next: Lattice operations, Previous: Tests, Up: Functionalities of the interface at level 0
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.
Next: Assignement and Substitutions, Previous: Property extraction, Up: Functionalities of the interface at level 0
Next: Operations on dimensions, Previous: Lattice operations, Up: Functionalities of the interface at level 0
Parallel assignement and substitution ar enot minimal operations, but for some abstract domains implementing them directly results in more efficient or more precise operations.
Next: Other operations, Previous: Assignement and Substitutions, Up: Functionalities of the interface at level 0
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.