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.