Package apron

package apron

Java binding for the Apron library.

The binding is based on Apron 0.9.15.

Short introduction

To start with Apron, you should first choose a numerical abstract domain. i.e., any subclass of Manager. For instance, Polka corresponds to the convex polyhedra domain. The constructor Polka(boolean) allows you to construct one (or several, which is mainly useful in a multi-threaded application) abstract domain instance.

Then, you need choose whether to use level 0 or level 1 operations. In level 0 operations, abstract elements are sets of points in a Cartesian space Z^n * R^m, and all data-structures (expressions, constraints, etc.) consider variables as dimensions, indexed from 0. In level 1 operations, abstract elements are sets of points in an Environment (i.e., set of variables) and variables are abstract Var (possibly simple strings, using StringVar). The main advantage of level 1 is that you do not need to bother with the mapping from program variables to dimensions in your static analysis (which could be tricky if variables are not created and destroyed in a last in / first out manner): the library does it for you. Actually, the level 1 is a implemented fully in Java, on top of the native level 0 code. Apron checks that dimension spaces (in level 0) or environments (in level 1) for all the arguments are compatible.

With your Manager instance, you can now create and manipulate abstract elements using either the Abstract0 or the Abstract1 class, depending on which level you prefer. Note that the Manager needs to be passed as first argument of almost all functions in these classes as it points back to the actual abstract domain implementation instance.

To apply transfer functions such as assignments or constraint addition, you need to create extra objects to denote expressions and constraints. Apron has linear expressions and arbitrary expression trees, respectively Linexpr0, Linexpr1, Texpr0Intern, Texpr1Intern, depending on the level you chose. Linear expressions are akin arrays but, as they are backed by native Apron C objects, they must be accessed with a set/get paradigm. Expression trees are a bit more complex: the internal native C data-structures are a bit too complex to be accessed directly. Instead, the Java binding provides pure Java expression trees (Texpr0Node, Texpr1Node and subclasses), and wrappers for opaque Apron C expression trees (Texpr0Intern, Texpr1Intern). The later are used for Abstract0 and Abstract1 arguments and return values; and can be converted to and from the former for easier construction and inspection on the Java side. Each expression type (linear / tree, level 0 / level 1) has a corresponding constraint type, using the expression as left argument, 0 as right argument, and some comparison operator (plus an optional extra number to denote modulo).

All expressions and constraints use a generic Coeff class to denote constants. These can be simple scalars (Scalar), or intervals with constant scalar bounds (Interval). Scalars can in turn be either represented by machine floating-point numbers (DoubleScalar), arbitrary-precision fractions (MpqScalar), or arbitrary-precision floating-point numbers (MpfrScalar). You can choose whichever suites you to talk to Apron and, when Apron gives you back some Scalar, you can convert it back to a double, a Mpq, or a Mpfr.

Remember that abstract operations may be inexact and imprecise. The contract states that abstract domain implementations can perform approximations but must always respect soundness: a result abstract element or interval may be an over-approximation. Likewise, a predicate is definitely true if the function returns true, but is unknown if the function returns false.

Warning

The Apron library changes the FPU rounding-mode towards +oo, to ensure the soundness of all computations. This can confuse some JVMs. For instance, this causes an error on Sun's JDK 1.6 when the option -Xcheck:jni is used.

See Also:

• http://apron.cri.ensmp.fr/library

Class	Description
Abstract0	Class of level 0 numerical abstract values.
Abstract1	Class of level 1 numerical abstract values.
ApronException	Superclass of Apron-specific exceptions that can be thrown by numerical abstract domains.
Box	Manager factory for the interval abstract domain.
Coeff	Abstract class of constant coefficients that can appear in expressions.
Dimchange	Class of dimension change specifications for level 0 objects.
Dimension	Class of dimension specifications for level 0 objects.
Dimperm	Class of dimension permutations for level 0 objects.
DoubleScalar	Class of Scalar objects backed up by a double-precision floating-point number.
Environment	Class of environments for level 1 objects.
Generator0	Class of geometrical features of level 0 linear abstract elements.
Generator1	Class of geometrical features of level 1 linear abstract elements.
Interval	Class of intervals of reals, denoted by a lower and an upper Scalar bound.
Lincons0	Class of level 0 linear constraints.
Lincons1	Class of level 1 linear constraints.
Linexpr0	Class of level 0 linear expressions.
Linexpr1	Class of level 1 linear expressions.
Linterm0	Class of terms in level 0 linear expressions and constraints.
Linterm1	Class of terms in level 1 linear expressions and constraints.
Manager	Class of numerical abstract domain instances.
MpfrScalar	Class of Scalar objects backed up by a Mpfr multi-precision floating-point number.
MpqScalar	Class of Scalar objects backed up by a Mpq multi-precision rational.
NotImplementedException	Exception thrown when calling an abstract transfer function that is not implemented in the domain.
Octagon	Manager factory for the octagon abstract domain.
OutOfSpaceException	Exception thrown by an abstract transfer function when the maximum memory consumption is exceeded.
OverflowException	Exception thrown by an abstract transfer function in case of an arithmetic overflow.
Polka	Manager factory for the convex polyhedron abstract domain.
PolkaEq	Manager factory for the linear equalities domain.
PolkaGrid	Manager factory for the reduced product of the Polka convex polyhedra and PplGrid the linear congruence equalities domains.
PplGrid	Manager factory for the Parma Polyhedra Library linear congruence equalities domain.
Pplite	Manager factory for the PPLite domains.
PplPoly	Manager factory for the Parma Polyhedra Library convex polyhedra domain.
Scalar	Abstract class of coefficients that represent scalar real numbers.
StringVar
Tcons0	Class of level 0 constraints on arbitrary expressions.
Tcons1	Class of level 1 constraints on arbitrary expressions.
Test	Simple test for the Java Apron binding.
TestPplite	Test ad-hoc PPLite functionality in Java binding
Texpr0BinNode	Class of binary operator nodes in Texpr0Node level 0 expression trees.
Texpr0CstNode	Class of constant leaves in Texpr0Node level 0 expression trees.
Texpr0DimNode	Class of variable leaves in Texpr0Node level 0 expression trees.
Texpr0Intern	Class of level 0 expression trees in opaque Apron representation.
Texpr0Node	Class of level 0 concrete expression trees.
Texpr0UnNode	Class of unary operator nodes in Texpr0Node level 0 expression trees.
Texpr1BinNode	Class of binary operator nodes in Texpr1Node level 1 expression trees.
Texpr1CstNode	Class of constant leaves in Texpr1Node level 1 expression trees.
Texpr1Intern	Class of level 1 expression trees in opaque Apron representation.
Texpr1Node	Class of level 1 concrete expression trees.
Texpr1UnNode	Class of unary operator nodes in Texpr1Node level 1 expression trees.
Texpr1VarNode	Class of variable leaves in Texpr1Node level 1 expression trees.
TimeoutException	Exception thrown by an abstract transfer function when the timeout is exceeded.
Var	Abstract class for Variables for level 1.