[PPL-devel] PPL: Problem with Checked-Ints

[Roberto Bagnara]

Didier Lime wrote:
> I am currently using the PPL to do some formal verification on Time  
> Petri Nets. You might be interested in knowing that the next release  
> of Romeo (http://romeo.rts-software.org/) should rely on it for all  
> its "hybrid" computations.

Dear Didier,

this is good news!  Please let us know when the release is out.

> Anyway, I have a strange "positive overflow" with the code below. The  
> complete error message reads:
> $ ./test_ppl
> terminate called after throwing an instance of 'std::overflow_error'
>    what():  Positive overflow.
> Abort trap
> 
> Info that should be useful:
> - I run this code on an Apple MacBook Pro with an Intel Core 2 Duo  
> processor
> - I compiled the PPL seamlessly with options --enabled- 
> optimization=speed and --enable-coefficients=checked-int32
> - g++ --version  reads: i686-apple-darwin8-g++-4.0.1 (GCC) 4.0.1  
> (Apple Computer, Inc. build 5367)
> 
> My sample code :
> #include <iostream>
> using namespace std;
> 
> #include <ppl.hh>
> using namespace PPL;
> using namespace PPL::IO_Operators;
> 
> int main()
> {
>      NNC_Polyhedron P(2);
>      Variable A(0);
>      Variable B(1);
> 
>      P.add_constraint(B == 46342);
>      P.add_constraint(A >= 0);
>      P.add_constraint(A <= 1);
> 
>      Linear_Expression expr = B - A;
>      P.affine_image(B, expr);
> 
>      cout << P << endl;
> 
>      return 0;
> }
> 
> I compile it with g++ -o test_ppl test_ppl.cc -lppl -lgmp and get the  
> above exception when executing it.

I have checked.  The overflow is genuine: the statement `cout << P << endl;'
checks whether `P' is empty in order to print `false' in case it is.
To do so, it calls a conversion routine that, at some stage, multiplies
46342 by 46341, and this gives an overflow on 32-bit integers
(46342*46341 = 2147534622 > 2147483647).

> Now, if I compile the PPL with --enable-coefficients=native-int32, it  
> just runs fine and gives the intended result:
> A + B = 46342, -A >= -1

With native integers the PPL is, in practice, just a generator of random
behavior.  In this particular case, perhaps the right thing happens by chance.
Notice though that the right result is

     A + B = 46342, A >= 0, -A >= -1

> Also it runs fine with checked ints and B being below or equal to 46341.

No wonder (46341*46340 = 2147441940 < 2147483647).

> I hope it is not just a misuse from me... Please ask if you need some  
> more information.

I think your surprise is due to the PPL internal computations: your
problem does no seem to have big enough coefficients to justify an
overflow with 32-bit integers, but in fact it has.

A few further annotations: I had to change two `using' directives
in your program so as to read

     using namespace Parma_Polyhedra_Library;
     using namespace Parma_Polyhedra_Library::IO_Operators;

If you change the output statement to

     cout << P.constraints() << endl;

the conversion routine is not called and you will see the right
result being printed.
Note also that C_Polyhedron objects are significantly more efficient
than NNC_Polyhedron objects: so, if you don't need to work with
non-closed polyhedra (i.e., don't need strict inequalities) you may
consider to use the former for efficiency.  Finally, the new paper
BagnaraHZ06TR (BibTeX enty below the signature) can give you
other indications about how to best use the PPL.
Please do not hesitate to come back to us: your feedback is
highly appreciated.
All the best,

     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

@TechReport{BagnaraHZ06TR,
   Author = "R. Bagnara and P. M. Hill and E. Zaffanella",
   Title = "The {Parma Polyhedra Library}: Toward a Complete Set of Numerical
            Abstractions for the Analysis and Verification
            of Hardware and Software Systems",
   Number = 457,
   Type = "Quaderno",
   Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy",
   Year = 2006,
   Note = "Available at \url{http://www.cs.unipr.it/Publications/}.
           Also published as {\tt arXiv:cs.MS/0612085},
           available from \url{http://arxiv.org/}.",
   Abstract = "Since its inception as a student project in 2001,
               initially just for the handling (as the name implies) of
               convex polyhedra, the \emph{Parma Polyhedra Library} has
               been continuously improved and extended by joining
               scrupulous research on the theoretical foundations of
               (possibly non-convex) numerical abstractions to a total
               adherence to the best available practices in software
               development.  Even though it is still not fully mature
               and functionally complete, the Parma Polyhedra Library
               already offers a combination of functionality,
               reliability, usability and performance that is not
               matched by similar, freely available libraries.  In this
               paper, we present the main features of the current
               version of the library, emphasizing those that
               distinguish it from other similar libraries and those
               that are important for applications in the field of
               analysis and verification of hardware and software
               systems.",
   URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ06TR.pdf"
}