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

[Axel Simon]

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.