[PPL-devel] Bugs in OCaml interface

[Enea Zaffanella]

Kenneth MacKenzie wrote:
> Enea Zaffanella writes:

[...snip...]

>  > b) What is the output of the command
>  >     echo $LD_LIBRARY_PATH
>  > on your machine? Does it include the path to your installation place, 
>  > that is /afs/inf.ed.ac.uk/user/k/kwxm/libraries/lib ?
>  > 
>  > Let us know if either a) or b) solves the problem.
>  > 
> 
>    I have to admit that I'm very confused by this.  I don't have
> LD_LIBRARY_PATH set, and you're correct in suggesting that if I set it
> to point to the location of my libraries then the test works OK.

Good.

> However, I've been able to compile and link my own programs without
> the use of LD_LIBRARY_PATH with no problems, and I can also compile
> your test program without using it.

The LD_LIBRARY_PATH environment variable has not much to do with 
compilation and (compile-time) linking. Rather, it comes into play when 
you run your program and it needs to link dynamically to a shared library.

> Here are the commands which
> interfaces/OCcaml/tests/Makefile executes when it's compiling test1:
> 
> OCAMLRUNPARAM='l=1M' ocamlc -o test1.cmo -c -I /home/kwxm/libraries/lib -I .. -ccopt -g test1.ml
> OCAMLRUNPARAM='l=1M' ocamlc -o test1 \
> 		-cc "g++" -I /home/kwxm/libraries/lib -I .. -ccopt -g \
> 		-cclib ../../../src/.libs/libppl.so -cclib ../../../Watchdog/src/.libs/libpwl.so -cclib -lmlgmp -cclib -lmpfr `echo " -lm -L/home/kwxm/libraries/lib -lgmpxx -L/home/kwxm/libraries/lib -lgmp -R/home/kwxm/libraries/lib -R/home/kwxm/libraries/lib " | /bin/sed -e "s/ -R[^ ]*//g" -e "s/ -/ -cclib -/g"` \
> 		ppl_ocaml.cma test1.cmo
> 
> Note that the second command, which does the linking, explicitly
> mentions things like libppl.so and -lgmpxx.
> 
> If you run the above commands and then use ldd, you get the following:
> 
>  ldd test1
> 	linux-gate.so.1 =>  (0xb7fc4000)
> 	libgmpxx.so.4 => not found
> 	libgmp.so.3 => /usr/lib/libgmp.so.3 (0xb7f4e000)
> 	libppl.so.7 => not found
> 	libpwl.so.4 => not found
> 	libmpfr.so.1 => /usr/lib/libmpfr.so.1 (0xb7f0b000)
>         ...

That is ok : it can't find libgmpxx.so.4 because the corresponding 
directory is not listed in LD_LIBRARY_PATH.

On the other hand, it can't find the ppl and pwl .so files because these 
libraries have not been installed yet (and they too are in a directory 
which is not listed in LD_LIBRARY_PATH).

In fact, when we *run* the OCaml tests, the command that gets actually 
executed looks like the following (to be run from path 
interfaces/Ocaml/tests):

../../../libtool --mode=execute -dlopen ../../../src/libppl.la -dlopen 
../../../Watchdog/src/libpwl.la ./test1

Note that here we are dlopen-ing the just built ppl and pwl libraries, 
because we want to link with *THESE* libraries and not any other 
previously installed ppl library (which might be a different version).

On the other hand, we do not dl-open libgmpxx, because this is the 
library which is installed in your system ... i.e., this is the one that 
should be normally accessible using ld and LD_LIBRARY_PATH.


> So in spite of all the options, it still doesn't know where to find
> libgmpxx.so.  It turns out that if you make a directory containing
> only libgmpxx.so.4 and point LD_LIBRARY_PATH to it, then test1 still
> fails because it can't find libppl.so.7, and similarly for libpwl.so.4.
> Once it's got all of these it works OK though.
> 
> I spent some time experimenting and found that I could do the
> compilation with much simpler commands.  To avoid the danger of
> interacting with my own previously-compiled version of PPL and other
> libraries, I made a directory called ~/gmp containing libgmp.a and
> libgmp.so*, together with the files gmp.a, gmp.cma and gmp.cmxa from
> mlgmp.  I can compile test1.ml by saying
> 
> ocamlc -c -o test1.cmo -I ~/gmp -I .. test1.ml
> 
> This is pretty much the same as what's in the makefile.  I think that
> at this stage it just needs to be able to find the .cma files for the
> OCaml modules used by test1.
> 
> 
> After this, I can link test1 with
> 
> ocamlc -o test1 ../ppl_ocaml.cma ~/gmp/gmp.cma test1.cmo  \
> -cclib -lppl -cclib -lpwl
> 
> (instead of using ../ppl_ocaml.cma you can also say
> -I .. ppl_ocaml.cma,  and similarly for gmp)
> 
> After this test1 runs successfully.
> 
> Note that I don't have to refer to -lgmp or any of the other libraries
> (but you can't leave out -lppl or -lpwl).  If you type 
> "strings ../ppl_ocaml.cma" then at the very end you see some strings which
> mention stuff like -L/home/kwxm/libraries/lib and -lgmpxx, so I think
> the ocaml compiler records some of the information that's necessary for
> the final linking.
 >
> 
> [Some time later...]
> 
> Ah, now I see that what makes the difference is including gmp.cma in
> the linking command.  If you insert it just after libppl.so in the
> makefile then everything works OK, and I think most of the other
> options are unnecessary.  I still don't understand exactly what's
> going on though.  :(

That is interesting info. However, since you are not definitely sure 
that the thing above will always work and given that we are near to the 
release of ppl-0.10.1, I prefer to leave things as they are (having more 
link options than strictly needed should make no arm).

> 
> 
> Kenneth
> 
> 
> PS:  my problematic BHRZ03 widening just finished, after 31 hours and
> 40 minutes.  The result was the same as that of the H79 widening.

There is nothing really surprising ... that's life.

The BHRZ03 widening is meant to try and apply a whole range of 
heuristics to improve the precision of the H79 widening. It might fail 
to achieve such an improvement, in which case it falls back to the H79 
widening.

As far as efficiency is concerned, as said earlier, whenever convex 
polyhedra come into play you need to keep an eye on the possibility of 
bumping into exponential behavior. Fortunately, the PPL library provides 
you with the tools (timeout and exception safety) needed to first 
identify the problem and then let the application skip to an alternative 
plan.

Cheers,
Enea.