[PPL-devel] Bugs in OCaml interface

[Enea Zaffanella]

Kenneth MacKenzie wrote:
> 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.

Hi Kenneth.

The snapshot with the corrections is now ready:
   ftp://ftp.cs.unipr.it/pub/ppl/snapshots/
or
   http://www.cs.unipr.it/ppl/Download/ftp/snapshots/

We would really appreciate if you could download and test it to see if 
any of the issues you were reporting (or even brand new ones) is still 
there. Please do not hesitate to come back to us if you see anything 
suspicious. Here below I briefly comment on the points you reported.

> --------------------------------------------------------------------------------
> 
> 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.
[...]
> 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.

This should be fixed now (I counted and corrected 520 occurrences, if I 
remember well.)

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

This should be fixed too: we are now almost systematic in registering 
values to the GC ... even when there is no actual need (up to my 
understanding).

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

In this case I am not sure it was a problem of the OCaml interface.

Depending on the input polyhedra (hence, not easily predictable), the 
BHRZ03 widening might bump into an exponential computation that is 
avoided by the H79 widening: it that is the case, you could observe wild 
variations on the overall computation times. Note that even the opposite 
case is possible (even though it should occur much less often), since a 
chain of widening computations does not respect the usual monotonicity 
properties, so that a more precise widening could result in a less 
precise final post-fixpoint and computation times become quite 
unpredictable.

Now that we also have the timeout functions available, I can suggest the 
following approach:

   1) copy the polyhedron ph to be widened to ph_copy;
   2) set a timeout;
   3) try using the BHRZ03 widening on ph;
   4) if the computation stops before the timeout expires, reset the 
timeout and get rid of the previous copy (now useless);
   5) otherwise, if the timeout expires, you will obtain a 
PPL_timeout_exception; you can then replace the polyhedron ph with the 
copy you saved in step 1 and re-try using the H79 widening.

We tried this (in C++) and in our context was working fairly well.

The code for using the timeout is similar to the following
(apologies for the awfully looking and untested OCaml code ... I never 
coded in OCaml before):

     print_string "Set timeout and use BHRZ03\n";
     ppl_set_timeout 100; (* 100 hsec *)
     try
       compute_something_using_BHRZ03 ph;
       ppl_reset_timeout ();
       print_string "BHRZ03 computation succeeded\n"
     with
     | PPL_timeout_exception ->
       ppl_reset_timeout ();
       print_string "Timeout expired: retrying using H79\n";
       ppl_Polyhedron_swap ph, ph_copy;
       compute_something_using_H79 ph
     | _ ->
       print_string "Unexpected exception\n"

Also see PPL test file interfaces/OCaml/tests/test1.ml, looking for the
code below the comment (* Testing timeouts *).


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

Should be fixed (thanks a lot for the detailed explanation).


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

I have added a note to the manual in this respect.
Briefly, since we do not want to force people to install the OCaml 
tools, we have two manuals: a configuration dependent and a 
configuration independent one. In the configuration independent one we 
only list those features that are available no matter what domain 
instances are selected (when the Ocaml interface is enabled): this also 
includes MIP_Problem. Hence, I suggest you look to the configuration 
dependent manual. In order to build it, you should cd into the ppl/doc 
directory and issue

   make ppl-user-configured-ocaml-interface-0.10.1pre10-html

Also note that the Ppl_ocaml_globals module is automatically included in 
module 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-html/ )
> 
> refers to a number of functions such as ppl_reset_timeout which 
> don't actually occur in the interface.

You are right, these were missing.
We now have added them (together with a few others).

Let us know how it goes.

Cheers,
Enea.


> 
> --------------------------------------------------------------------------------
> 
> Best wishes,
> 
> Kenneth MacKenzie
>