APRON Library - Octagon Domain Implementation

Table of Contents

  1. Introduction
  2. Installation
  3. Access to the Library from C and C++
  4. Underlying Numeric Set
  5. Precision of the Transfer Functions
  6. Precision of the Predicates
  7. The algorithm parameter
  8. Widenings and Narrowing
  9. Additional Transfer Functions
  10. Unimplemented Features
  11. Conversion with Polyhedra
  12. Tools
  13. Low-level Access
  14. Access to the Library from OCaml
  15. Links
  16. Contact

Introduction

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 ±yc, 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).

Installation

Please see the README file included in the distribution for installation instructions.

Access to the Library from C and C++

Your C or C++ program must be linked with the following libraries:

It is possible to use additional libraries, such as the POLKA module -lpolkaMPQ.

The standard way to access to the octagon library is through an APRON manager. The manager is created as follows:

All standard APRON functions from ap_abstract0.h are available on octagons through man.

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 (using 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.

Underlying Numeric Set

The octagon library is compiled with a variety of underlying numeric set, distinguished using a suffix:

The choice of this numeric set affects the soundness, precision, and efficiency of the analysis:

For best precision, MPQ is recommended. For a fast and versatile yet sound analysis, D is recommended.

Note that the underlying numeric set chosen for octagons is not related to the choice of double or GMP for ap_scalar_t types used as arguments in transfer functions. Type mismatches may result in extra over-approximation (but always in a sound way).

Precision of the Transfer Functions

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 the 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 user-provided ap_scalar_t types. The octagon library will set the flag_exact and 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.

Precision of the Predicates

The following predicates are exact, i.e., they always return either tbool_true or tbool_false (provided that 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, tbool_false is 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 tbool_top.

When 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 ap_scalar_t types 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 tbool_true or tbool_top. It can conclude that the predicate is definitively tbool_false only in very rare cases. The octagon library will set the flag_exact and flag_best manager flags accordingly in all cases.

The algorithm parameter

The 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):

Widenings and Narrowing

Depending on the algorithm flag, one of the following widening algorithm is used:

The ap_abstract0_oct_widening_thresholds provides a widening with scalar thresholds. For each constraint of the form ±x ±yc or ±xc 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 scalar. 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 from ap_abstract0_sat_lincons and ap_abstract0_meet_lincons_array.)

The 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.

Additional Transfer Functions

The octagon library provides a few functions not generic enough to be included in the APRON library. They share the ap_abstract0_oct_ prefix.

Additionally to the widening with thresholds and narrowing functions described in the preceding section, the octagon domain provides the following extra function:

Unimplemented Features

The following are not implemented and will raise an exception:

Conversion with Polyhedra

In order to ensure the best precision, the following conversion procedures are recommended:

Do not extract the generators of an octagon or build an octagon from arbitrary linear constraints as these are not best-precision operators.

Tools

The distribution provides a fully automatic test suite with octtest. It compares the result of all transfer functions in the octagon and polyhedron domains, checking for soundness, best-precision and exactness properties.

Low-level Access

The file 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 as safe. Wrapping and unwrapping a oct_t* pointer within a generic ap_abstract0_t* is done using the abstract0_of_oct and oct_of_abstract0 functions.

The file oct/oct_internal.h must be included to access to the low-level representation of octagons struct oct_t and manager-specific data struct _oct_internal_t. Direct access to private fields is not recommended.

Access to the Library from OCaml

Your OCaml program must be linked with the following modules, in order:

You may need the specify the include path with -I, depending on your installation.

Examples:

The octagon library provides an Oct OCaml module There is no numeric suffix here: the OCaml wrapper is independent from the chosen numerical type. The Oct.manager_alloc function returns a new manager that can then be used with the standard Apron.Abstract0 module provided by APRON.

The Oct module also provides some implementation-specific functions:

Links

APRON

The octagon abstract domain:

Contact

Main developer: Antoine Miné mine@di.ens.fr.