The APRON project provides a common interface for various numerical abstract domains with various expressiveness and cost versus precision trade-offs. This document describes the octagon domain implementation available within APRON. The octagon domain allows manipulating and representing conjunctions of invariants of the form ±x ±y ≤ c, where x and y range among a finite set of numerical program variables. In two dimensions, such invariants have an octagonal shape, hence the name.
Familiarity is assumed with the generic APRON framework as well as the octagon abstract domain (see external links).
Please see the
README file included in the
distribution for installation instructions.
Your C or C++ program must be linked with the following libraries:
Xdenotes the chosen numeric set;
The standard way to access to the octagon library is through an APRON manager. The manager is created as follows:
ap_manager_t* man = oct_manager_alloc();
ap_abstract0.hare available on octagons through
Note that, when using a floating-point implementation of the octagon library,
creating a manager will automatically put the floating-point unit into
rounding towards +oo mode
ap_fpu_init provided by APRON),
as it is required to ensure the soundness of the transfer functions.
Beware that this setting is global: it affects all the computations of the
process, not only those occurring in the octagon library.
The octagon library is compiled with a variety of underlying numeric set, distinguished using a suffix:
I: integers with a plain "long int" representation;
Ill: integers with a "long long int" representation;
MPZ: arbitrary precision integers using GMP;
Rl: rationals with a "long int" representation;
Rll: rationals with a "long long int" representation;
MPQ: arbitrary precision rationals using GMP;
D: reals with a "double" representation;
Dl: reals with a "long double" representation.
The choice of this numeric set affects the soundness, precision, and efficiency of the analysis:
longtypes are subject to overflows, which may result in unsound results (no overflow checking is performed for efficiency reasons),
long doubletypes are subject to rounding, which may result in some loss of precision; rounding is always performed towards +oo, which ensures soundness;
Z, which results in some loss of precision;
GMPtypes are much slower than native types.
MPQis recommended. For a fast and versatile yet sound analysis,
Note that the underlying numeric set chosen for octagons is not
related to the choice of
ap_scalar_t types used as arguments in transfer functions.
Type mismatches may result in extra over-approximation (but always in a
Exact transfer functions are provided for the class of operations that are closed under octagons. These include:
Best transfer functions are provided in the following cases:
The following transfer functions use some approximate polynomial algorithms and have no precision guarantees:
Additionally, the exactness or best-precision feature of an abstract transfer
function is often lost when the
MPQ underlying numeric set
is not used, or the arguments have integer dimensions, or the user sets
algorithm parameter to a strictly negative value.
Finally, the exactness or best-precision feature can be lost due to
conversion between the underlying numeric type and
The octagon library will set the
flag_best manager flags accordingly in all cases.
Note that, due to interval coefficients, expressions may be non-deterministic, that is, correspond to a bunch of expressions. In case of assignments, substitutions, or bound determinations of non-deterministic expressions, or conjunctions with non-deterministic constraints, we considers the join of all results, when ranging over the non-deterministic set.
The following predicates are exact, i.e., they always return
algorithm is greater than or equal to 0,
that the octagon has no integer dimension, and that the
MPQ underlying domain is selected):
Note that, for non-deterministic expressions,
returned as long as the saturation is not satisfied for at least one expression.
Testing for the saturation by an arbitrary expression is very imprecise.
It always return
algorithm is set to a strictly negative value, the
octagon has an integer dimension, the
MPQ underlying domain is
selected, or the conversion from user-specified
to internal types resulted in an over-approximation, the predicate is sound
but not exact: it is a semi-test.
That is, it mainly returns either
It can conclude that the predicate is definitively
only in very rare cases.
The octagon library will set the
flag_best manager flags accordingly in all cases.
algorithm field in the manager provides an
implementation-specific parameter to set the required level of precision
for transfer functions.
In the octagon domain, only two precision levels are recognised. They correspond to (with the exception of the widening):
algorithm ≥ 0is the normal precision: a transitive closure algorithm is used pervasively to achieve best precision transfer functions and results in transfer functions that have a cubic worst-case cost (in the number of variables),
algorithm < 0is the low precision: the transitive closure algorithm is not used, the best precision feature is not guaranteed, and transfer functions have a quadratic worst-case cost (many actually have a linear cost).
Depending on the
algorithm flag, one of the following widening
algorithm is used:
algorithm = 0: the right argument is closed, the standard widening is used: unstable constraints are forgotten. Thus, it converges in a quadratic number of steps, at worse.
algorithm < 0: the standard widening algorithm is used but the right argument is not closed.
algorithm = oct_pre_widening: this special value corresponds to a pre-widening. It does not enforce the convergence by itself but can be safely intermixed with a regular widening to improve the precision of the sequence, without jeopardizing the overall convergence. As long as a regular widening is applied infinitely often, the sequence will converge in finite time. (Note that intermixing a regular widening with a join operator will result in a diverging sequence. Thus, the join is not a pre-widening. Our pre-widening is actually a join without the closure application.) Use with care!
ap_abstract0_oct_widening_thresholds provides a widening
with scalar thresholds.
For each constraint of the form
±x ±y ≤ c or
±x ≤ c where the bound c is not stable,
the widening replaces c with the scalar immediately greater in
the user-supplied list, or +oo if it is greater than the greatest supplied
The list must be sorted in strictly increasing order.
(Note that this operator is not exactly the same as the generic
ap_abstract0_widening_threshold function which is synthesized
ap_abstract0_oct_narrowing function implements the
standard narrowing: it refines only those constraints that have
no finite bound.
Thus, it converges in a quadratic number of steps, at worse.
The octagon library provides a few functions not generic enough to be
included in the APRON library.
They share the
Additionally to the widening with thresholds and narrowing functions described in the preceding section, the octagon domain provides the following extra function:
ap_abstract0_oct_of_generator_arrayconverts a generator set to an octagon, with best-precision.
ap_abstract0_oct_add_epsilonenlarges each constraint bound by a user-specified factor of the maximum finite bound present in the octagon.
The following are not implemented and will raise an exception:
In order to ensure the best precision, the following conversion procedures are recommended:
ap_abstract0_to_generator_arrayon the polyhedra and then
ap_abstract0_oct_of_generator_arrayon the result.
ap_abstract0_to_lincons_arrayon the octagon and then
ap_abstract0_of_lincons_arrayon the result.
Do not extract the generators of an octagon or build an octagon from arbitrary linear constraints as these are not best-precision operators.
The distribution provides a fully automatic test suite with
It compares the result of all transfer functions in the octagon and polyhedron
domains, checking for soundness, best-precision and exactness properties.
oct/oct_fun.h provides a direct access to all the
octagon functions, without the abstraction provided by the manager.
Note that these functions perform less sanity checks, and so, may not be
Wrapping and unwrapping a
oct_t* pointer within a
ap_abstract0_t* is done using the
oct/oct_internal.h must be included to access to the
low-level representation of octagons
struct oct_t and manager-specific data
Direct access to private fields is not recommended.
Your OCaml program must be linked with the following modules, in order:
-I, depending on your installation.
ocamlc -I $HOME/lib gmp.cma apron.cma oct.cma mltest.ml -cclib -loctMPQ -cclib -lapron
ocamlopt -I $HOME/lib gmp.cmxa apron.cmxa oct.cmxa mltest.ml -cclib -loctMPQ -cclib -lapron
The octagon library provides an
Oct OCaml module
There is no numeric suffix here: the OCaml wrapper is independent from the
chosen numerical type.
Oct.manager_alloc function returns a new manager that can
then be used with the standard
Apron.Abstract0 module provided by
Oct module also provides some implementation-specific functions:
of_generator_arrayto convert from a set of generators to an octagon, with best abstraction,
The octagon abstract domain: