[PPL-devel] a Bug, a Beg and a Binding

[Roberto Bagnara]

Axel Simon wrote:
 > Hi,
 >
 > c) I have written a binding for the functional language Haskell to the
 > C-interface of the PPL. I basically parse the C header file and generate
 > the Haskell functions. Thus there might still be some functions which
 > have an incorrect type. I'll contact you after I checked those (and
 > adjusted the documentation which is much more work).

Hello Axel,

this is good news!  What are you doing in Haskell with the PPL?
A program analysis application?  Something else?

 > b) I have severe problems with the ppl_ConSys_const_Iterator_equal_test
 > function. It works most of the times, but then it doesn't and my loop
 > iterates on and on until I get a Bus Error or a Segmentation fault. I
 > just wondered if anyone has experienced this kind of behavior or if it's
 > my binding that is at fault.

Without seeing an example exhibiting the problem it is difficult to
say what the problem is.  What is more likely is that you keep an
iterator to the ConSys and that this iterator is invalidated by
something you are doing (explicitely or implicitely) to the ConSys
itself or to the polyhedon to which it belongs; if you use the
invalidated iterator further, undefined behavior is what you get.  If
you show us the loop in question we can be more precise.

The fact that iterators can be invalidated by several operations is
perhaps not well explained in our documentation.  We will rectify this
situation in the next release.

 > c) There is a but in ppl_c.cc in version 0.5 of PPL. In class PIFunc the
 > variable empty is not initialized. I changed the constructor (line 1584)
 > to:
 >
 >   PIFunc(dimension_type* v, size_t n)
 >     : vec(v), vec_size(n), max_in_codomain_(not_a_dimension()),
 >     empty(-1) {
 >   }
 >
 > which makes the ppl_Polyhedron_map_dimensions function work (instead of
 > giving me the empty polyhedron all the time).

Thanks!
And welcome to our "credits" page!

 > Oh, and another question: I didn't find any functions to calculate the
 > maximum of a linear expression within a given polyhedron (i.e. do a
 > simplex). I think this function is essential in abstract interpretation
 > when I need to approximate a non linear expression. Did I miss it?

This has been in the queue for quite some time.  The reason is not that
it is difficult to implement (it is in fact quite easy) but we were unsure
about the interface.  Do you need only the maximum value of the expression
or also one or all vertices where the maximum is attained?
Cheers

     Roberto

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it