- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Dense_Matrix, Sparse_Matrix: remove useless typedefs for row_type.
by Marco Poletti 03 Oct '10

03 Oct '10

Module: ppl/ppl Branch: master Commit: e9f743717517f834912473cf77d05db585b5e4e9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e9f743717517… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Oct 3 09:24:55 2010 +0200 Dense_Matrix, Sparse_Matrix: remove useless typedefs for row_type. --- src/Dense_Matrix.defs.hh | 2 -- src/Sparse_Matrix.defs.hh | 2 -- 2 files changed, 0 insertions(+), 4 deletions(-) diff --git a/src/Dense_Matrix.defs.hh b/src/Dense_Matrix.defs.hh index 2f082b6..1bf916e 100644 --- a/src/Dense_Matrix.defs.hh +++ b/src/Dense_Matrix.defs.hh @@ -44,8 +44,6 @@ site: http://www.cs.unipr.it/ppl/ . */ class Parma_Polyhedra_Library::Dense_Matrix { public: - typedef Dense_Row row_type; - //! Returns the maximum number of rows of a Dense_Matrix. static dimension_type max_num_rows(); diff --git a/src/Sparse_Matrix.defs.hh b/src/Sparse_Matrix.defs.hh index 5331f74..9f6c2d7 100644 --- a/src/Sparse_Matrix.defs.hh +++ b/src/Sparse_Matrix.defs.hh @@ -54,8 +54,6 @@ site: http://www.cs.unipr.it/ppl/ . */ class Parma_Polyhedra_Library::Sparse_Matrix { public: - typedef Sparse_Row row_type; - typedef std::vector<Sparse_Row>::iterator iterator; typedef std::vector<Sparse_Row>::const_iterator const_iterator;

1 0

my problem with using ppl
by saber mirzaei 02 Oct '10

02 Oct '10

Dear PPL Developers, I am currently working on my master thesis that applies abstract model checking of software systems. For implementing an abstract domain, I plan to use PPL for the handling of Polyhedra. Right now my problem is how to inlcude the PPL classes in my C++ project. I am using Ubuntu 10.04 and i'm working with Code Blocks.I installed PPL library by using synaptic and it went well and i have related files in my lib and include directories now. However now I am unsure about how to actually include PPL classes (e.g. "Polyhedron") in a C++ project and also could find no further instructions in the user manual or the README and INSTALL files, provided. Maybe you can help me answering this question: - What is the intended usage of PPL? Should one just include "ppl.hh" and the created libraries? Right now, this yields error messages like:"... undefined reference to `Parma_Polyhedra_Library::Init::Init...." it seems the linker is unable to find the used library functions. Your help will be much appreciated! With best regards, Saber MirzaeiSharif University OF science and technologyComputer department.

2 1

[GIT] ppl/ppl(master): CO_Tree: fix comment.
by Marco Poletti 01 Oct '10

01 Oct '10

Module: ppl/ppl Branch: master Commit: 58d73240616250bff7ab3afa63e102b9bd21d30f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=58d732406162… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Fri Oct 1 15:34:50 2010 +0200 CO_Tree: fix comment. --- src/CO_Tree.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/CO_Tree.defs.hh b/src/CO_Tree.defs.hh index 7eb4ce0..76ff01c 100644 --- a/src/CO_Tree.defs.hh +++ b/src/CO_Tree.defs.hh @@ -74,8 +74,8 @@ namespace Parma_Polyhedra_Library { available caches. Assuming \p n is the number of elements in the tree and \p B is the number - of <dimension_type,Coefficient> pairs that fit in cache, the time and - cache misses complexities are the following: + of <dimension_type,Coefficient> pairs that fit in a cache line, the + time and cache misses complexities are the following: - Insertions/Queries/Deletions: \f$O(\log^2 n)\f$ time, \f$O(\log \frac{n}{B}))\f$ cache misses.

1 0

[GIT] ppl/ppl(floating_point): Always use marked_empty() instead of is_empty() after
by Fabio Bossi 29 Sep '10

29 Sep '10

Module: ppl/ppl Branch: floating_point Commit: 8d8b45e65ab5caadd86a5fd193318de4c84094e7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8d8b45e65ab5… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 29 19:10:03 2010 +0200 Always use marked_empty() instead of is_empty() after a closure. --- src/BD_Shape.templates.hh | 2 +- src/Octagonal_Shape.templates.hh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 112047a..1223515 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4491,7 +4491,7 @@ BD_Shape<T> // Expose all the interval constraints. shortest_path_closure_assign(); - if (is_empty()) { + if (marked_empty()) { dest.set_empty(); PPL_ASSERT(OK()); return; diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index b9674f0..4695d59 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -7665,7 +7665,7 @@ Octagonal_Shape<T> strong_closure_assign(); - if (is_empty()) { + if (marked_empty()) { dest.set_empty(); return; }

1 0

[GIT] ppl/ppl(master): New commits
by Roberto Bagnara 29 Sep '10

29 Sep '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3e80dc1425eb… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Mon Sep 27 10:51:10 2010 +0200 CO_Tree: rename the size field into size_, and add a size() method. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3cb542d4fe76… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Mon Sep 27 10:50:20 2010 +0200 CO_Tree: avoid shadowing a field with a local variable, in external_memory_in_bytes(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6475eea32239… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Sep 26 14:51:09 2010 +0200 Dense_Row: mark the constructor from a Sparse_Row as explicit. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d1088ad4fc32… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Sep 26 14:50:32 2010 +0200 Sparse_Row: add an assignment operator from a Dense_Row. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9707c1e408c1… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Sep 26 14:45:16 2010 +0200 Sparse_Row: copy flags too, in the constructor from a Dense_Row. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5b123a9d2528… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Sep 26 14:44:35 2010 +0200 Dense_Row: add a constructor and an assignment operator that take a Sparse_Row. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3426ae69e61c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Sep 26 14:43:53 2010 +0200 CO_Tree: fix bug in the constructor from a sequence and remove its second argument, it is used in assertions only.

1 0

[GIT] ppl/ppl(floating_point): Added generalized_refine_with_linear_form_inequality.
by Fabio Bossi 29 Sep '10

29 Sep '10

Module: ppl/ppl Branch: floating_point Commit: 7d65c1696bed13d29185ce2b078d558188b81d45 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7d65c1696bed… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 29 18:20:41 2010 +0200 Added generalized_refine_with_linear_form_inequality. --- src/BD_Shape.defs.hh | 34 ++++++++++++++++++++++++++++++++++ src/BD_Shape.inlines.hh | 28 ++++++++++++++++++++++++++++ 2 files changed, 62 insertions(+), 0 deletions(-) diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh index 0ad832c..cd8147f 100644 --- a/src/BD_Shape.defs.hh +++ b/src/BD_Shape.defs.hh @@ -1037,6 +1037,40 @@ public: const Linear_Form< Interval<T, Interval_Info> >& left, const Linear_Form< Interval<T, Interval_Info> >& right); + /*! \brief + Refines the system of BD_Shape constraints defining \p *this using + the constraint expressed by \p left \f$\relsym\f$ \p right, where + \f$\relsym\f$ is the relation symbol specified by \p relsym. + + \param left + The linear form on intervals with floating point boundaries that + is at the left of the comparison operator. All of its coefficients + MUST be bounded. + + \param right + The linear form on intervals with floating point boundaries that + is at the right of the comparison operator. All of its coefficients + MUST be bounded. + + \param relsym + The relation symbol. + + \exception std::invalid_argument + Thrown if \p left (or \p right) is dimension-incompatible with \p *this. + + \exception std::runtime_error + Thrown if \p relsym is not a valid relation symbol. + + This function is used in abstract interpretation to model a filter + that is generated by a comparison of two expressions that are correctly + approximated by \p left and \p right respectively. + */ + template <typename Interval_Info> + void generalized_refine_with_linear_form_inequality( + const Linear_Form< Interval<T, Interval_Info> >& left, + const Linear_Form< Interval<T, Interval_Info> >& right, + Relation_Symbol relsym); + //! Applies to \p dest the interval constraints embedded in \p *this. /*! \param dest diff --git a/src/BD_Shape.inlines.hh b/src/BD_Shape.inlines.hh index 275b0df..9fe4f7b 100644 --- a/src/BD_Shape.inlines.hh +++ b/src/BD_Shape.inlines.hh @@ -839,6 +839,34 @@ BD_Shape<T>::hash_code() const { template <typename T> template <typename Interval_Info> inline void +BD_Shape<T>::generalized_refine_with_linear_form_inequality( + const Linear_Form< Interval<T, Interval_Info> >& left, + const Linear_Form< Interval<T, Interval_Info> >& right, + const Relation_Symbol relsym) { + switch (relsym) { + case EQUAL: + // TODO: see if we can handle this case more efficiently. + refine_with_linear_form_inequality(left, right); + refine_with_linear_form_inequality(right, left); + break; + case LESS_THAN: + case LESS_OR_EQUAL: + refine_with_linear_form_inequality(left, right); + break; + case GREATER_THAN: + case GREATER_OR_EQUAL: + refine_with_linear_form_inequality(right, left); + break; + case NOT_EQUAL: + break; + default: + throw std::runtime_error("PPL internal error"); + } +} + +template <typename T> +template <typename Interval_Info> +inline void BD_Shape<T>::refine_fp_interval_abstract_store( Box< Interval<T, Interval_Info> >& store) const {

1 0

[GIT] ppl/ppl(floating_point): Added missing emptiness checks.
by Fabio Bossi 29 Sep '10

29 Sep '10

Module: ppl/ppl Branch: floating_point Commit: b39ec7c81e536c991c43e395147ca92b8d2a4b44 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b39ec7c81e53… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 29 14:27:43 2010 +0200 Added missing emptiness checks. --- src/BD_Shape.templates.hh | 6 ++++-- 1 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 57e0672..112047a 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4503,13 +4503,15 @@ BD_Shape<T> // Set the upper bound. const N& u = dbm_0[i+1]; if (!is_plus_infinity(u)) - dest.restrict_upper(i, u.raw_value()); + if (!dest.restrict_upper(i, u.raw_value())) + return; // Set the lower bound. const N& negated_l = dbm[i+1][0]; if (!is_plus_infinity(negated_l)) { neg_assign_r(tmp, negated_l, ROUND_DOWN); - dest.restrict_lower(i, negated_l.raw_value()); + if (!dest.restrict_lower(i, negated_l.raw_value())) + return; } }

1 0

[GIT] ppl/ppl(floating_point): Implemented export_interval_constraints.
by Fabio Bossi 29 Sep '10

29 Sep '10

Module: ppl/ppl Branch: floating_point Commit: 2407bd5aa082844784918b237282e7cf3ed94f61 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2407bd5aa082… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 29 14:00:23 2010 +0200 Implemented export_interval_constraints. --- src/BD_Shape.defs.hh | 33 +++++++++++++++++++++++++++++++++ src/BD_Shape.templates.hh | 38 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+), 0 deletions(-) diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh index 3413c35..0ad832c 100644 --- a/src/BD_Shape.defs.hh +++ b/src/BD_Shape.defs.hh @@ -1037,6 +1037,39 @@ public: const Linear_Form< Interval<T, Interval_Info> >& left, const Linear_Form< Interval<T, Interval_Info> >& right); + //! Applies to \p dest the interval constraints embedded in \p *this. + /*! + \param dest + The object to which the constraints will be added. + + \exception std::invalid_argument + Thrown if \p *this is dimension-incompatible with \p dest. + + The template type parameter U must provide the following methods. + \code + dimension_type space_dimension() const + \endcode + returns the space dimension of the object. + \code + void set_empty() + \endcode + sets the object to an empty object. + \code + bool restrict_lower(dimension_type dim, const T& lb) + \endcode + restricts the object by applying the lower bound \p lb to the space + dimension \p dim and returns <CODE>false</CODE> if and only if the + object becomes empty. + \code + bool restrict_upper(dimension_type dim, const T& ub) + \endcode + restricts the object by applying the upper bound \p ub to the space + dimension \p dim and returns <CODE>false</CODE> if and only if the + object becomes empty. + */ + template <typename U> + void export_interval_constraints(U& dest) const; + /*! \brief Computes the \ref Cylindrification "cylindrification" of \p *this with respect to space dimension \p var, assigning the result to \p *this. diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index bbb5e1b..57e0672 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4479,6 +4479,44 @@ void BD_Shape<T>::refine_with_linear_form_inequality( } // end of refine_with_linear_form_inequality template <typename T> +template <typename U> +void +BD_Shape<T> +::export_interval_constraints(U& dest) const { + const dimension_type space_dim = space_dimension(); + if (space_dim > dest.space_dimension()) + throw std::invalid_argument( + "BD_Shape<T>::export_interval_constraints"); + + // Expose all the interval constraints. + shortest_path_closure_assign(); + + if (is_empty()) { + dest.set_empty(); + PPL_ASSERT(OK()); + return; + } + + PPL_DIRTY_TEMP(N, tmp); + const DB_Row<N>& dbm_0 = dbm[0]; + for (dimension_type i = space_dim; i-- > 0; ) { + // Set the upper bound. + const N& u = dbm_0[i+1]; + if (!is_plus_infinity(u)) + dest.restrict_upper(i, u.raw_value()); + + // Set the lower bound. + const N& negated_l = dbm[i+1][0]; + if (!is_plus_infinity(negated_l)) { + neg_assign_r(tmp, negated_l, ROUND_DOWN); + dest.restrict_lower(i, negated_l.raw_value()); + } + } + + PPL_ASSERT(OK()); +} + +template <typename T> template <typename Interval_Info> void BD_Shape<T>::left_inhomogeneous_refine(const dimension_type& right_t,

1 0

Fwd: Re: compiler warnings ppl-0.10
by Roberto Bagnara 29 Sep '10

29 Sep '10

-------- Original Message -------- Subject: Re: [PPL-devel] compiler warnings ppl-0.10 Date: Wed, 29 Sep 2010 12:28:56 +0200 From: Dieter Demerre <ddemerre(a)gmail.com> To: Roberto Bagnara <bagnara(a)cs.unipr.it> On 29 Sep 2010, at 11:01, Roberto Bagnara wrote: > On 09/28/10 15:51, Dieter Demerre wrote: >> A quick walkthrough directed me to: >> - cc1: Unrecognized option `-frounding-math' >> - cc1plus: Unrecognized option `-frounding-math' >> the -frounding-math option option that's probably new.... (in more >> recent gcc) >> (not yet present in gcc-2.95,...). Is this option required ? (at this >> level ?) >> which would explain the failure on the header file check / compilation. > > Dear Dieter, > > please see README.configure, where is says: > > It should be noted that no version of GCC prior to 4.0.3 is known to > reliably compile PPL 0.10. > > I can strengthen this by saying that really there is no way > to compile the PPL with GCC 2.95. > > > Currently,... I'm (attempting) to compile gcc-4.5.0 without ppl support, > > and after this was successful (hope, hope),... try to compile the ppl > > library again, and compile gcc again too. > > Yes, this is the right thing to do. > Friendly regards, > > Roberto Thanks for the response, and my apologies for not reading the documentation. In my defense,... this documentation more regularly than not only contains the "general" instructions "execute ./configure followed by make and make install" and stuff. Hence I refrained from reading it. I should make a habit of - if the first attempt fails - first read more documentation instead of thinking: "Now that is something these developers didn't think about". Greetings. dd

1 0

Re: [PPL-devel] compiler warnings ppl-0.10
by Roberto Bagnara 29 Sep '10

29 Sep '10

On 09/28/10 15:51, Dieter Demerre wrote: > A quick walkthrough directed me to: > - cc1: Unrecognized option `-frounding-math' > - cc1plus: Unrecognized option `-frounding-math' > the -frounding-math option option that's probably new.... (in more > recent gcc) > (not yet present in gcc-2.95,...). Is this option required ? (at this > level ?) > which would explain the failure on the header file check / compilation. Dear Dieter, please see README.configure, where is says: It should be noted that no version of GCC prior to 4.0.3 is known to reliably compile PPL 0.10. I can strengthen this by saying that really there is no way to compile the PPL with GCC 2.95. > Currently,... I'm (attempting) to compile gcc-4.5.0 without ppl support, > and after this was successful (hope, hope),... try to compile the ppl > library again, and compile gcc again too. Yes, this is the right thing to do. Friendly regards, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0