C Programming Guidelines

C Headers and Libraries

Declarations needed to use an underlying library via APRON are collected in the C include files ap_global0.h and ap_global1.h. They respectively refer to the level 0 and the level 1 of the interface. One can also refer to single APRON modules with their corresponding include files ap_dimension.h, ap_lincons0.h, ... Header files <stdio.h>, stdlib.h and <stdarg.h> will be required.

Then, you should also include the header files of the underlying libraries you want to use it via APRON (for instance, box.h, pk.h, ap_ppl.h).

All programs using APRON must link against the libapron, libmpfr and libgmp libraries, and the underlying libraries you want to use it via APRON:

1. If some file test.c uses the POLKA library via APRON, the compilation command should look like ‘gcc -I$ITV/include -I$MPFR/include -I$GMP/include -I$APRON/include -L$MPFR/lib -L$GMP/lib -L$APRON/lib -o test test.c -lpolkaMPQ -lapron -lmpfr -lgmp’, assuming that the POLKA library is used in its ’MPQ’ version (internal number representation is GMP rationals) and resides in $APRON/include and $APRON/lib directories.

   The libpolkaMPQ.a library is of course needed, libapron.a contains all the code common to all APRON library (manipulation of expressions, environments, ...), as well as ITV functions (quasi)linearisation facilities of APRON,...), last the libraries libmpfr.a and libgmp.a are required both by NEWPOLKA and APRON .

2. If some file test.c uses the PPL library via APRON, the compilation command should look like ‘g++ -I$ITV/include -I$MPFR/include -I$GMP/include -I$APRON/include -I$PPL/include -L$ITV/lib -L$MPFR/lib -L$GMP/lib -L$APRON/lib -L$PPL/lib -o test test.c -la_ppl -lppl -lgmpxx -lapron -lmpfr -lgmp’, assuming that PPL resides in $PPL and PPL APRON interface in $APRON/include and $APRON/lib directories.

   Notice that the PPL library (libppl.a) is a C++ library, you need to use ‘g++’ instead of ‘gcc’ for linking. You also need the C++ layer on top of GMP (libgmpxx.a). The libap_ppl.a library contains the layer on top of PPL which implements the APRON interface.

You should look at the specific documentation of the libraries for more details.

Naming conventions and Allocation/Deallocation schemes

The general rule is that all type and function names defined by the library are prefixed with ap_, in order to prevent name conflicts with other libraries. Moreover, functions operating on objects of type ap_typ_t are usually prefixed with ap_typ_op.

Given an object of datatype ap_typ_t*, two kinds of allocation/deallocation pairs of functions may be defined:

1. variable declaration: ap_typ_t obj;
   • Initialization: void typ_init(ap_typ_t* arg, ...) or ap_typ_t ap_typ_make(...)
   • Finalization: void ap_typ_clear(ap_typ_t* arg)

   this pair of functions follows the semantics used in the GMP library. The first function initializes the object of type ap_typ_t pointed to by arg, and fills it with a valid content. The second function deallocates the memory possibly pointed to by fields of the object *arg, but do not attempt to deallocate the memory pointed by arg.

2. variable declaration: ap_typ_t* obj;
   • Allocation ap_typ_t* ap_typ_alloc(...)
   • Deallocation void ap_typ_free(ap_typ_t* arg)

   the first function allocates an object of type typ_t and then calls a ap_typ_init-like function on the result; the second functions first call a ap_typ_clear-like function and then deallocate the memory pointed by arg.

Allocating managers and setting options

From the user point of view, the benefit of using the APRON interface is to restrict the place where the user is aware of the real library in use to the code initializing the manager, as illustrated by the following example:

#include "ap_global1.h"
#include "pk.h"

/* Allocating a Polka manager, for polyhedra with strict constraints */
manager_t* man = pk_manager_alloc(true);
/* Setting options offered by the common interface,
   but with meaning possibly specific to the library */
manager_set_abort_if_exception(man,EXC_OVERFLOW,true);
{
  funopt_t funopt;
  funopt_init(&funopt);
  funopt.algorithm = 1; /* default value is 0 */
  manager_set_funopt(man,fun_widening,&funopt); /* Setting options for widening */
}
{
  funopt_t funopt = manager_get_funopt(man,fun_widening);
  funopt.timeout = 30;
  manager_set_funopt(man,fun_widening,&funopt);
}
/* Obtaining the internal part of the manager and setting specific options */
pk_internal_t* pk = manager_get_internal(man);
pk_set_max_coeff_size(pk,size);

The standard operations can then be used and will have the semantics defined in the interface. Notice however that some generic functions are not formally generic: abstract_fprint, abstract_fdump, abstract_approximate. At any point, options may be modified in the same way as during the initialization.

Sequel of the small example

An environment can be created as follows:

/* Create an environment with 6 real variables */
ap_var_t name_of_dim[6] = {
  "x","y","z","u","w","v"
};
ap_environment_t* env = ap_environment_alloc(NULL,0,name_of_dim,6);

Then, we build an array of constraints. At level 1, an array of constraints is an abstract datatype, which requires careful manipulation w.r.t. memory management.

/* Create an array of constraints of size 2 */
ap_lincons1_array_t array = ap_lincons1_array_make(env,2);

/* 1.a Creation of an inequality constraint */
ap_linexpr1_t expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,1);
ap_lincons1_t cons = ap_lincons1_make(AP_CONS_SUP,&expr,NULL);
    /* Now expr is memory-managed by cons */
/* 1.b Fill the constraint */
ap_lincons1_set_list(&cons,
		     AP_COEFF_S_INT,"x",
		     AP_CST_S_FRAC,1,2,
		     AP_END);
/* 1.c Put in the array */
ap_lincons1_array_set(&array,0,&cons);
    /* Now cons is memory-managed by array */

/* 2.a Creation of an inequality constraint */
expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
    /* The old cons is not lost, because it is stored in the array.
       It would be an error to clear it (same for expr). */
/* 2.b Fill the constraint */
ap_lincons1_set_list(&cons,
		     AP_COEFF_S_INT,1,"x",
		     AP_COEFF_S_INT,1,"y",
		     AP_COEFF_S_INT,1,"z",
		     AP_END);
/* 2.c Put in the array */
ap_lincons1_array_set(&array,1,&cons);

Last we can build an abstract value.

/* Creation of an abstract value defined by the array of constraints */
ap_abstract1_t abs = ap_abstract1_of_lincons_array(man,env,&array);

fprintf(stdout,"Abstract value:\n");
ap_abstract1_fprint(stdout,man,&abs);

We now deallocate everything:

/* deallocation */
ap_lincons1_array_clear(&array);
ap_abstract1_clear(&abs);
ap_environment_free(env);
ap_manager_free(man);

Typing issue in C

The use of several libraries at the same time via the common interface and the managers associated to each library raises the problem of typing. Look at the following code:

ap_manager_t* manpk = pk_manager_alloc(true); /* manager for Polka */
ap_manager_t* manoct = oct_manager_alloc();    /* manager for octagon */

ap_abstract0_t* abs1 = ap_abstract_top(manpk,3,3);
ap_abstract0_t* abs2 = ap_abstract_top(manoct,3,3);
bool b = ap_abstract0_is_eq(manoct,abs1,abs2);
  /* Problem: the effective function called (octagon_is_eq) expects
     abs1 to be an octagon, and not a polyhedron ! */

ap_abstract0_t* abs3 = ap_abstract_top(manoct,3,3);
abstract0_meet_with(manpk,abs2,abs3);
  /* Problem: the effective function called (pk_meet_with) expects
     abs2 and abs3 to be polyhedra, but they are octagons */

There is actually no static typing, as abstract0_t* and manager_t are abstract types shared by the different libraries. Types are thus dynamically checked by the interface. Notice that the use of C++ and inheritance would not solve directly the problem, if functions of the interface are methods of the manager; one would have:

ap_manager_t* manpk = pk_manager_alloc(true);
  /* manager for Polka, effective type pk_manager_t* */
ap_manager_t* manoct = oct_manager_alloc();
  /* manager for octagon, effective type oct_manager_t* */

ap_abstract0_t* abs1 = manpk->abstract_top(3,3);
  /* effective type: poly_t */
ap_abstract0_t* abs2 = manoct->abstract_top(3,3);
  /* effective type: oct_t */
bool b = manoct->abstract0_is_eq(abs1,abs2);
  /* No static typing possible:
     manpk->abstract0_is_eq and manoct->abstract0_is_eq should have the same
     signature (otherwise one cannot interchange manpk and manoct in the code),
     which means that abs1 and abs2 are supposed to be of type abstract0_t* */
*/

Currently, only the OCaml polymorphic type system allows to solve elegantly this problem.