Module Introduction


module Introduction: sig .. end


This package is an OCaml interface for the APRON library/interface. The interface is accessed via the module Apron, which is decomposed into 15 submodules, corresponding to C modules, and which can be organized in 4 groups

  1. Coefficients: scalar numbers, intervals, ...
  2. Managers and Abstract Domains
  3. Level 1 of the interface (user-level): manipulation of generic datatypes (expressions, constraints, ..., and generic abstract domain interface)
  4. Level 0 of the interface (lower-level): manipulation of generic datatypes (expressions, constraints, ..., and generic abstract domain interface)


Requirements and installation



(See README of general APRON distribution for more details)

For compiling from repository (strongly recommended):

It is important to have the GNU versions !

Installation





Hints on programming idioms



Allocating managers



The user might have some difficulties to exploit the genericity of the interface at first glance (it was actually my case).

Assume your main analysis function looks like:

let analyze_and_display equations (man : 'Apron.Manager.t) : unit =
  ... 

where equations is the equation system, man the APRON manager, and 'a the effective abstract domain/implementation to be used in the analysis.

  1. You might want to write code like

    let manager_alloc option = match option with
      | `Box -> Box.manager_alloc ()
      | `Oct -> Oct.manager_alloc ()
    ;;
    let main option equations =
      let man = manager_alloc opt in
      analyze_and_display man equations
    ;;
    
    

    but this does not work because manager_alloc cannot be typed (the types of (Box.manager_alloc ()) : Box.t Apron.Manager.t and (Oct.manager_alloc ()) : Oct.t Apron.Manager.t cannot be unified).

  2. Using continuations does not work either:

    let manager_alloc_and_continue option (continuation:'Apron.Manager.t -> 'b) =
      match option with
      | `Box -> continuation (Box.manager_alloc ())
      | `Oct -> continuation (Oct.manager_alloc ())
    ;;
    let main option equations =
      manager_alloc_and_continue option
        (fun apron -> analyze_and_display equations equations apron)
    ;;
    
    

    but this does not work because the argument continuation is monomorphic inside the body of manager_alloc_and_continue (i.e, it is not generalized):

    let manager_alloc_and_continue option (continuation:'Apron.Manager.t -> 'b) =
        match option with
        | `Box -> continuation (Box.manager_alloc ())
        | `Oct -> continuation (Oct.manager_alloc ())
    ;;                          ^^^^^^^^^^^^^^^^^^^^
    ErrorThis expression has type Oct.t Apron.Manager.t
           but an expression was expected of type Box.t Apron.Manager.t
    
    You can read detailed explanations about this issue on
    OCaml FAQ.
    

I can suggest 3 solutions:

  1. Following OCaml FAQ, you can modify attempt 2 above as follows:

    let manager_alloc_and_continue option equations =
      match option with
      | `Box -> analyze_and_display equations (Box.manager_alloc ())
      | `Oct -> analyze_and_display equations (Oct.manager_alloc ())
    ;;
    let main option equations =
      manager_alloc_and_continue option equations
    ;;
    
    

    Now this can be type-checked:

    val manager_alloc_and_continue : [< `Box | `Oct ] -> '-> unit = <fun>
    
    

    This is not very elegant: the call to analyze_and_display is hard-coded in manager_alloc_and_continue, and one has to pass all its arguments (like equations) to manager_alloc_and_continue.

  2. It is possible to not give up with continuations by encapsulating them into a record (resp. an immediate object), because record fields (resp. methods) may be polymorphic.

  3. A last possibility is to use the type conversion functions provided in Box and Oct (as well as in the other domain modules). One can modify attempt 1 as follows:

    let manager_alloc option = match option with
      | `Box -> Box.manager_of_box (Box.manager_alloc ())
      | `Oct -> Oct.manager_of_oct (Oct.manager_alloc ())
    ;;
    let main option equations =
      let man = manager_alloc opt in
      analyze_and_display man equations
    ;;
    
    

    val manager_alloc : [< `Box | `Oct ] -> 'Apron.Manager.t = <fun>
    
    

    The purpose of functions Box.manager_of_box and Oct.manager_of_oct is to generalize the type of their arguments (this is implemented with the Obj.magic function... but this is safe).

    This is the most simple and flexible way.



Breaking (locally) genericity



Assume that you are inside the body of the same

analyze_and_display: equations -> 'Apron.Manager.t -> unit

function and that you want at some point

You can modify the solution 1 above so as to pass a modify: 'a Apron.Manager.t -> unit function to analyze_and_display:
let analyze_and_display equations 
      (man : 'Apron.Manager.t) 
      (modify : 'Apron.Manager.t -> unit) 
  =
  ... 
;;
let manager_alloc_and_continue option equations =
  match option with
  | `Box -> analyze_and_display equations (Box.manager_alloc ()) box_modify
  | `Oct -> analyze_and_display equations (Oct.manager_alloc ()) oct_modify
;;
let main option equations =
  manager_alloc_and_continue option equations
;;

The most flexible way however is to use the ``dynamic cast'' functions Box.manager_to_box, Box.Abstract0.to_box, Oct.manager_to_oct, Oct.Abstract0.to_oct. These functions raise a Failure exception in case of (dynamic) typing error, but this can be avoided by the test functions Box.manager_is_box and Oct.manager_is_oct

Compiling and linking client programs against APRON



To make things clearer, we assume an example file mlexample.ml which uses both NewPolka (convex polyhedra) and Box (intervals) libraries, in their versions where rationals are GMP rationals (which is the default). We assume that C and OCaml interface and library files are located in directory $APRON/lib.

The native-code compilation command looks like

 ocamlopt -I $APRON/lib -o mlexample.opt \
   bigarray.cmxa gmp.cmxa apron.cmxa boxMPFR.cmxa polkaMPQ.cmxa mlexample.ml

Comments:
  1. You need at least the libraries bigarray (standard OCaml distribution), gmp, and apron (standard APRON distribution), plus the one implementing an effective abstract domains: here, boxMPFR, and polkaMPQ.
  2. The C libraries associated to those OCaml libraries (e.g., gmp_caml, boxMPFR_caml, \ldots) are automatically looked for, as well as the the libraries implementing abstract domains (e.g., polkaMPQ, boxMPFR).

    If other versions of abstract domains library are wanted, you should use the -noautolink option as explained below.

  3. If in Makefile.config, the HAS_SHARED variable is set to a non-empty value, dynamic versions of those libraires are also available, but makes sure that all the needed libraries are in the dynamic search path indicated by $LD_LIBRARY_PATH.

If dynamic libraries are available, the byte-code compilation process looks like

 ocamlc -I $MLGMPIDL/lib -I $APRON/lib -o mlexample.byte \
   bigarray.cma gmp.cma apron.cma boxMPFR.cma polkaMPQ.cma mlexample.ml 

Comments:
  1. The ocamlrun bytecode interpreter will automatically load the dynamic libraries, using environment variables $LD_LIBRARY_PATH (and possibly $CAML_LD_LIBRARY_PATH, see OCaml documentation, section on OCaml/C interface).
  2. You can very easily use the interactive toplevel interpreter: type 'ocaml -I $MLGMPIDL/lib -I $APRON/lib' and then enter:

        #load "bigarray.cma";;
        #load "gmp.cma";;
        #load "apron.cma";;
        #load "polkaMPQ.cma";;
        ... 
    
    
  3. This is also the only way to load and use in the OCaml debugger pretty-printers depending on C code, like

        #load "bigarray.cma";;
        #load "gmp.cma";;
        #load "apron.cma";;

        #installl_printer Apron.Abstract1.print;; 
    
    

If only static libraries are available, you can:

  1. Create a custom runtime and use it as follows:

         ocamlc -I $MLGMPIDL/lib -I $APRON/lib -make-runtime -o myrun \
           bigarray.cma gmp.cma apron.cma boxMPFR.cma polkaMPQ.cma
    
         ocamlc -I $MLGMPIDL/lib -I $APRON/lib -use-runtime myrun -o \mlexample.byte \
           bigarray.cma gmp.cma apron.cma box.cma polka.cma mlexample.ml 
    
      Comments:
      
    1. One first build a custom bytecode interpreter that includes the new native-code needed;
    2. One then compile the mlexample.ml file, using the generated bytecode interpreter.
  2. If you want to use the interactive toplevel interpreter, you have to generate a custom toplevel interpreter using the ocamlmktop command (see OCaml documentation, section on OCaml/C interface):

         ocamlmktop -I $MLGMPIDL/lib -I $APRON/lib -o mytop \
           bigarray.cma gmp.cma apron.cma boxMPFR.cma polkaMPQ.cma 
    
    

The automatic search for C libraries associated to these OCaml libraries can be disabled by the option -noautolink supported by both ocamlc and ocamlopt commands. For instance, the command for native-code compilation can alternatively looks like:

  ocamlopt -I $MLGMPIDL/lib -I $APRON/lib -noautolink -o mlexample.opt \
    bigarray.cmxa gmp.cmxa apron.cmxa boxMPFR.cmxa polkaMPQ.cmxa mlexample.ml \
    -cclib "-L$MLGMPIDL/lib -L$APRON/lib \
	    -lpolkaMPQ_caml_debug -lpolkaMPQ_debug \
	    -lboxMPFR_caml_debug -lboxMPFR_debug \
	    -lapron_caml_debug -lapron_debug \
	    -lgmp_caml -L$MPFR -lmpfr -L$GMP/lib -lgmp \
	    -L$CAMLIDL/lib/ocaml -lcamlidl \
	    -lbigarray" 

or more simply, if dynamic libraries are available (because some
dynamic libraries are automatically referenced by others):

  ocamlopt -I $MLGMPIDL/lib -I $APRON/lib -noautolink -o mlexample.opt \
    bigarray.cmxa gmp.cmxa apron.cmxa boxMPFR.cmxa polkaMPQ.cmxa mlexample.ml \
    -cclib "-L$MLGMPIDL/lib -L$APRON/lib \
	    -lpolkaMPQ_caml_debug \
	    -lboxMPFR_caml_debug \
	    -lapron_caml_debug \
	    -lgmp_caml \
	    -lbigarray" 

This is mandatory if you want to use non-default versions of
libraries (here, debug versions).

The option -verbose helps to understand what is happening in case of problem.

More details are given in the modules implementing a specific abstract domain.