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