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

Roberto Bagnara bagnara at cs.unipr.it
Mon Feb 19 21:47:43 CET 2007

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
> \$ ./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);
>
>
>      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

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

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,
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"
}

`