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). 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. 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). 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? Thanks, Axel.
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@cs.unipr.it
On Wednesday, Aug 20, 2003, at 16:44 Europe/Paris, Roberto Bagnara wrote:
Hello Axel,
this is good news! What are you doing in Haskell with the PPL? A program analysis application? Something else?
I am trying to describe how to analyze floating point calculations with polyhedra. It's a last-minute project for a VMCAI paper.
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.
I don't think I do anything that could invalidate the iterator. Here is the Haskell code (and an explanation between the lines in C):
cs <- PPL.polyhedronMinimizedConstraints p cs=ppl_Polyhedron_minimized_constraints(p) cIt <- PPL.newConSysIterator cIt=ppl_new_ConSys_const_iterator() PPL.conSysBegin cs cIt ppl_ConSys_begin(cs,&cIt) end <- PPL.newConSysIterator ppl_new_ConSys_const_iterator() PPL.conSysEnd cs end ppl_ConSys_end(cs,&end) coeff <- PPL.newCoefficient ppl_new_Coefficient(&coeff) writeConstraints cIt end coeff env return $ Status () state where writeConstraints :: ConSysIterator -> ConSysIterator -> Coefficient -> Environment -> IO () writeConstraints cIt end coeff env = do eq <- PPL.conSysIteratorEqualTest cIt end eq=(bool) ppl_ConSys_iterator_equal_test(cIt,end) unless eq $ do if (eq) return; c <- PPL.conSysIteratorDereference cIt ppl_ConSys_iterator_dereference(&c, cIt) // this catches some bogus constraints when the equality test fails to work, just ignore dim <- PPL.constraintSpaceDimension c if (dim==0) then putStrLn "(bogus constraint)" else do // this just turns the constraint into a string and prints it str <- liftM concat $ mapM (printCoeff coeff c) env ty <- PPL.constraintType c PPL.constraintInhomogeneousTerm c coeff b <- PPL.coefficientToInteger coeff putStrLn (dropWhile (=='+') str++show ty++" "++show (-b)) PPL.conSysIteratorIncrement cIt ppl_ConSys_iterator_increment(cIt) writeConstraints cIt end coeff env // recursive call
The only thing which could make the test fail is the fact that I retrieve the end iterator before I actually iterate through the constraint system. The odd thing is that this function works 90% of the time. I would like to debug it but it is kind of hard since all interesting functions are in-line. It could be something with my binding to Haskell, but I just thought I ask if somebody has experienced the same problem with the C interface before going down that route.
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?
No, I would only be interested in the maximum (rational?) value. I think that is essential for analyzing non-linear expressions like x = e_1 *e_2 with \exists_x(P) \sqcup \{ x \leq \max(e_1,P)*e_1, x \leq \max(e_2,P)*e_1, x \geq \min(e_1,P)*e_2, x \geq \min(e_2,P)*e_1 \} where \min(e_1,P) gives smallest value of the expression e_1 in P. Cheers, Axel.
Axel Simon wrote:
I am trying to describe how to analyze floating point calculations with polyhedra. It's a last-minute project for a VMCAI paper.
Great! There is no much time though ;-)
The only thing which could make the test fail is the fact that I retrieve the end iterator before I actually iterate through the constraint system.
That would not be a problem, provided nothing happens to the constraint system before you actually iterate. If you can reproduce the problem in C or C++ we would be more than happy to help with debugging.
The odd thing is that this function works 90% of the time. I would like to debug it but it is kind of hard since all interesting functions are in-line. It could be something with my binding to Haskell, but I just thought I ask if somebody has experienced the same problem with the C interface before going down that route.
No, we are not aware of any problem of this kind. You will find similar code, iterating through a generator system, at lines 667 and following of interfaces/C/lpenum/lpenum.c.
Do you need only the maximum value of the expression or also one or all vertices where the maximum is attained?
No, I would only be interested in the maximum (rational?) value. I think that is essential for analyzing non-linear expressions like x = e_1 *e_2 with \exists_x(P) \sqcup \{ x \leq \max(e_1,P)*e_1, x \leq \max(e_2,P)*e_1, x \geq \min(e_1,P)*e_2, x \geq \min(e_2,P)*e_1 \} where \min(e_1,P) gives smallest value of the expression e_1 in P.
OK: we will try to add this functionality to the library in a couple of days or so. If this is too much time, you can look at the above mentioned lines 667 and following of interfaces/C/lpenum/lpenum.c: there, what is done is precisely to compute the rational maximum/minumum of a linear expression. Cheers Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it
Roberto Bagnara wrote:
Axel Simon wrote:
No, I would only be interested in the maximum (rational?) value. I think that is essential for analyzing non-linear expressions like x = e_1 *e_2 with \exists_x(P) \sqcup \{ x \leq \max(e_1,P)*e_1, x \leq \max(e_2,P)*e_1, x \geq \min(e_1,P)*e_2, x \geq \min(e_2,P)*e_1 \} where \min(e_1,P) gives smallest value of the expression e_1 in P.
OK: we will try to add this functionality to the library in a couple of days or so.
Hi Axel, there is now a snapshot of the PPL 0.6 development branch in http://www.cs.unipr.it/ppl/Download/ftp/snapshots/ppl-0.6pre2.tar.bz2 In the C interface you will find the function ppl_Polyhedron_maximize() that does what you need (and more). Beware: this new code is almost untested. Please let us know how it goes. Cheers Roberto P.S. Any progress in debugging the ConSys iteration problem? -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it
On Friday, Aug 22, 2003, at 22:45 Europe/Paris, Roberto Bagnara wrote:
Roberto Bagnara wrote:
Axel Simon wrote:
No, I would only be interested in the maximum (rational?) value. I think that is essential for analyzing non-linear expressions like x = e_1 *e_2 with \exists_x(P) \sqcup \{ x \leq \max(e_1,P)*e_1, x \leq \max(e_2,P)*e_1, x \geq \min(e_1,P)*e_2, x \geq \min(e_2,P)*e_1 \} where \min(e_1,P) gives smallest value of the expression e_1 in P. OK: we will try to add this functionality to the library in a couple of days or so.
Hi Axel,
there is now a snapshot of the PPL 0.6 development branch in
http://www.cs.unipr.it/ppl/Download/ftp/snapshots/ppl-0.6pre2.tar.bz2
In the C interface you will find the function ppl_Polyhedron_maximize() that does what you need (and more). Beware: this new code is almost untested. Please let us know how it goes.
Ok, thanks, I'll give it a go.
P.S. Any progress in debugging the ConSys iteration problem?
No, not yet. There reason might be that Haskell uses a pre-installed gmp package which is version 4.0.1. I compiled PPL against 4.2.1. Thus PPL used the headers and gmpxx.a of the newer version while the gmp.a is from Haskell. I know that it's asking for trouble, but the binary representation of mpz's haven't changed and I don't get any link errors. I'll try to build PPL against version 4.0.1 now. Is that possible? Axel.
Axel Simon wrote:
Roberto Bagnara wrote: there is now a snapshot of the PPL 0.6 development branch in
http://www.cs.unipr.it/ppl/Download/ftp/snapshots/ppl-0.6pre2.tar.bz2
In the C interface you will find the function ppl_Polyhedron_maximize() that does what you need (and more). Beware: this new code is almost untested. Please let us know how it goes.
Ok, thanks, I'll give it a go.
The snapshot mentioned above had bugs and an interface for the new mazimization and minimization methods that I did not like. A new snapshot is in http://www.cs.unipr.it/ppl/Download/ftp/snapshots/ppl-0.6pre3.tar.bz2
P.S. Any progress in debugging the ConSys iteration problem?
No, not yet. There reason might be that Haskell uses a pre-installed gmp package which is version 4.0.1. I compiled PPL against 4.2.1. Thus PPL used the headers and gmpxx.a of the newer version while the gmp.a is from Haskell. I know that it's asking for trouble, but the binary representation of mpz's haven't changed and I don't get any link errors. I'll try to build PPL against version 4.0.1 now. Is that possible?
Unfortunately not: we require GMP 4.1.2 (the latest release, as of today). -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it
On Monday, Aug 25, 2003, at 10:55 Europe/Paris, Roberto Bagnara wrote:
No, not yet. There reason might be that Haskell uses a pre-installed gmp package which is version 4.0.1. I compiled PPL against 4.2.1. Thus PPL used the headers and gmpxx.a of the newer version while the gmp.a is from Haskell. I know that it's asking for trouble, but the binary representation of mpz's haven't changed and I don't get any link errors. I'll try to build PPL against version 4.0.1 now. Is that possible?
Unfortunately not: we require GMP 4.1.2 (the latest release, as of today).
I successfully compiled PPL against 4.0.1. I can't claim that it works better, it's still the same. Since the interface obviously hasn't changed, why does PPL require 4.1.2? Axel.
Axel Simon wrote:
On Monday, Aug 25, 2003, at 10:55 Europe/Paris, Roberto Bagnara wrote:
we require GMP 4.1.2 (the latest release, as of today).
I successfully compiled PPL against 4.0.1. I can't claim that it works better, it's still the same.
Then I believe you have not compiled any Prolog interface.
Since the interface obviously hasn't changed, why does PPL require 4.1.2?
See http://www.cs.unipr.it/pipermail/ppl-devel/2002-June/001707.html and the thread of messages following that. That bug was fixed in GMP 4.1.2 and, since then, we assume it fixed. I know for sure we rely on the fix in the Prolog interfaces and it may be just by chance that the rest of the library is unaffected. Cheers Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it
Axel Simon wrote:
I don't think I do anything that could invalidate the iterator. Here is the Haskell code (and an explanation between the lines in C):
cs <- PPL.polyhedronMinimizedConstraints p
cs=ppl_Polyhedron_minimized_constraints(p)
[...]
time. I would like to debug it but it is kind of hard since all interesting functions are in-line. It could be something with my binding to Haskell, but I just thought I ask if somebody has experienced the same problem with the C interface before going down that route.
One simple test that you can do is to explicitly call function ppl_Polyhedron_OK() on polyhedron `p' just after retrieving its minimized constraint system. This will check if the (coded) polyhedron invariants are all valid (see documentation). I do not expect this call to fail, but if it does, then it will be an indication that the problem is caused somewhere else before this program point. Of course, the above test is already done implicitly (and it is thus redundant) if you have configured the PPL with assertions turned on, which I would recommend in such a debugging phase. Good luck and keep us informed, Enea.
participants (4)
-
Axel Simon -
Axel Simon
-
Enea Zaffanella -
Roberto Bagnara