Bugs in OCaml interface

25 Mar 2009


      Hello there,
I've been using the PPL OCaml interface to carry out some program
analysis within a compiler.  It's been working pretty well, but I've
come across a number of bugs.
--------------------------------------------------------------------------------
1. The OCaml 'unit' type has only a single value, denoted (); this is
represented internally by a pointer to a single preallocated value.
However, many of the functions in the PPL interface return the wrong value.
Here's an example from an OCaml top level built with PPL
$ ocamlppl
         Objective Caml version 3.11.0
# let p = Ppl_ocaml.ppl_new_C_Polyhedron_from_constraints [];;
 val p : Ppl_ocaml.polyhedron = <abstr>
# let u = Ppl_ocaml.ppl_Polyhedron_add_constraints p [];;
 val u : unit = <unknown constructor>
# u = ();;
 - : bool = false
 #
The <unknown constructor> thing is something you should never see.
Here's the defintion of the ppl_Polyhedron_add_constraints function from
interfaces/OCaml/ppl_ocaml_Polyhedron.cc:
extern "C"
 void
 ppl_Polyhedron_add_constraints(value ph, value cs) try {
   CAMLparam2(ph, cs);
   Polyhedron& pph = *p_Polyhedron_val(ph);
   Constraint_System pcs = build_ppl_Constraint_System(cs);
   pph.add_constraints(pcs);
   CAMLreturn0;
 }
 CATCH_ALL
This has void return type, but should actually return a pointer to the 
preallocated unit value.  I think the correct code should look like
extern "C"
 CAMLprim value
 ppl_Polyhedron_add_constraints(value ph, value cs) try {
   CAMLparam2(ph, cs);
   Polyhedron& pph = *p_Polyhedron_val(ph);
   Constraint_System pcs = build_ppl_Constraint_System(cs);
   pph.add_constraints(pcs);
   CAMLreturn(Val_unit);
 }
 CATCH_ALL
Every function returning a unit value (it looks like there are 509 of
them) should look like this.  I don't think this bug is very harmful
unless one uses unit values in unusual ways.
----------------------------------------------------------------------
2.  Certain functions can lead to segmentation errors.  Here's a
program which creates a polyhedron and then loops round adding
constraints one by one.  The call to ppl_Polyhedron_get_constraints
sometimes causes a segmentation fault; if you remove it then the
program runs OK.  (Presumably it eventually runs out of memory, but
I've run it for a very long time (millions of iterations) without this
happening.)
$ cat tst.ml
open Ppl_ocaml
let itoz = Gmp.Z.of_int
let f n = (* Generate a constraint nx + (n+1)y <= n+2 *)
   Less_Or_Equal 
     (Plus (Times (itoz n, Variable 0), 
            Times (itoz (n+1), Variable 1)),
              Coefficient (itoz (n+2)))
let p = ppl_new_C_Polyhedron_from_space_dimension 2 Universe
let rec g n =
   let () = ppl_Polyhedron_add_constraint p (f n)
   in let l = ppl_Polyhedron_get_constraints p
   in let () = Printf.printf "%d\n" n
   in let () = flush stdout
   in g (n+1)
let _ = g 0
Here's what happens when you run it:
$ ocamlppl
 # #use "tst.ml";;
 val itoz : int -> Gmp.Z.t = <fun>
 val f : int -> Ppl_ocaml.linear_constraint = <fun>
 val p : Ppl_ocaml.polyhedron = <abstr>
 File "tst.ml", line 12, characters 9-10:
 Warning Y: unused variable l.
 val g : int -> 'a = <fun>
 0
 1
 2
 3
 .
 .    <output deleted>
 . 
 1654
 1655
 1656
 Segmentation fault
I think that the problem here is in the function
build_ocaml_constraint_system in interfaces/OCaml/ppl_ocaml_common.cc:
value
 build_ocaml_constraint_system(const Constraint_System& ppl_cs) {
   // This code builds a list of constraints starting from bottom to
   // top. A list on OCaml must be built like a sequence of Cons and Tail.
   // The first element is the Nil list (the Val_int(0)).
   value result = Val_int(0);
   for (Constraint_System::const_iterator v_begin = ppl_cs.begin(),
      v_end = ppl_cs.end(); v_begin != v_end; ++v_begin) {
     value new_tail = caml_alloc_tuple(2);
     Field(new_tail, 0) = build_ocaml_constraint(*v_begin);
     Field(new_tail, 1) = result;
     result = new_tail;
   }
   return result;
 }
The problem is in the way that allocation in the ocaml heap is
handled.  The function loops round allocating list cells in the heap,
but the ocaml garbage collector doesn't know what's going on.
Eventually caml_alloc_tuple is called when there isn't enough free
space: this triggers garbage collection, and the memory occupied by
the partially built list is reclaimed; the loop then continues,
allocating a new list cell whose tail points to some garbage-collected
memory which will later be occupied by something else allocated in the
heap.  The function finally returns a malformed list to the ocaml
system, eventually leading to a crash.  To overcome this the CAMLlocal
macro should be used to tell the ocaml garbage collector to leave the
partially-allocated list alone:
CAMLprim
 value
 build_ocaml_constraint_system(const Constraint_System& ppl_cs) {
   // This code builds a list of constraints starting from bottom to
   // top. A list on OCaml must be built like a sequence of Cons and Tail.
   // The first element is the Nil list (the Val_int(0)).
   CAMLlocal2 (result, new_tail);
   result = Val_emptylist;  // Synonymous with Val_int(0);
   for (Constraint_System::const_iterator v_begin = ppl_cs.begin(),
      v_end = ppl_cs.end(); v_begin != v_end; ++v_begin) {
     new_tail = caml_alloc_tuple(2);
     Field(new_tail, 0) = build_ocaml_constraint(*v_begin);
     Field(new_tail, 1) = result;
     result = new_tail;
   }
   CAMLreturn (result);
 }
I haven't actually tested this since it would require too much
rebuilding, but I've written similar code which worked OK.  I'm not
sure whether "CAMLprim" is in fact necessary, but I don't think it
does any harm.
Again, there are a number of functions which should be amended in a 
similar way:  I think that in any C function which uses a caml_alloc*
function, every local variable which may point to a value allocated in
the ocaml heap should be protected by a CAMLlocal* macro.
--------------------------------------------------------------------------------
3.  I've also had problems with ppl_Polyhedron_BHRZ03_widening_assign.
Occasionally my compiler locks up with a lot of CPU usage when
ppl_Polyhedron_BHRZ03_widening_assign is called.  I didn't have any
probelms using the H79 widening instead.  I'm not sure what's causing
this: ppl_Polyhedron_BHRZ03_widening_assign does have the problem with
units mentioned in (1) above, but I don't think that should do any
damage.  It's possible that I have some malformed data structures from
(2) which are causing problems.
--------------------------------------------------------------------------------
4.  While looking at the code for
ppl_Polyhedron_BHRZ03_widening_assign I noticed a bug in
ppl_Polyhedron_BHRZ03_widening_assign_with_tokens, which is repeated
in all the widening-with-tokens functions:
CAMLprim value
 ppl_Polyhedron_BHRZ03_widening_assign_with_tokens
 (value ph1, value ph2, value integer) try {
   CAMLparam3(ph1, ph2, integer);
   Polyhedron& pph1 = *p_Polyhedron_val(ph1);
   Polyhedron& pph2 = *p_Polyhedron_val(ph2);
   int cpp_int = Val_int(integer);
   check_int_is_unsigned(cpp_int);
   unsigned int unsigned_value = cpp_int;
   pph1.BHRZ03_widening_assign(pph2, &unsigned_value);
   CAMLreturn(Int_val(unsigned_value));
 }
Val_int and Int_val should be interchanged here.  The 
current version will calculate the number of remaining 
tokens incorrectly.
--------------------------------------------------------------------------------
5.  It's not really a bug,  but I'm a little confused by the way
the code is divided into modules.  Ppl_ocaml_globals contains
the type definitions for various datatypes,  but why does it also
contain all the MIP functions?  I see that the OCamldoc-generated 
documentation only contains information about Ppl_ocaml_globals,
but Ppl_ocaml is missing,  so there's no information available
about the types of the polyhedron functions and other things
in Ppl_ocaml.
Also, the documentation for the OCaml interface (for example, at
http://www.cs.unipr.it/ppl/Documentation/user/ppl-user-ocaml-interface-0.10-... )
refers to a number of functions such as ppl_reset_timeout which 
don't actually occur in the interface.
--------------------------------------------------------------------------------
Best wishes,
Kenneth MacKenzie
-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Kenneth MacKenzie

Roberto Bagnara

Roberto Bagnara

Enea Zaffanella

Kenneth MacKenzie

Enea Zaffanella

Kenneth MacKenzie

Enea Zaffanella

tags (0)

participants (3)