March 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(termination): Completed a couple of comment blocks.
by Roberto Bagnara 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: termination Commit: 8680f29d7d3d4170b90f55cf6d2becf27db33d1f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8680f29d7d3d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Mar 7 20:42:21 2010 +0400 Completed a couple of comment blocks. --- src/termination.cc | 70 ++++++++++++++++++++++++++------------------------- 1 files changed, 36 insertions(+), 34 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index 4e24f98..47314e7 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -61,7 +61,15 @@ assign_all_inequalities_approximation(const C_Polyhedron& ph, The input constraint system, where variables indices are allocated as follows: - \f$ x'_1, \ldots, x'_n \f$ go onto \f$ 0, \ldots, n-1 \f$; - - \f$ x_1, \ldots, x_n \f$ go onto \f$ n, \ldots, 2n-1 \f$; + - \f$ x_1, \ldots, x_n \f$ go onto \f$ n, \ldots, 2n-1 \f$. + . + The system does not contain any equality. + + \param n + The number of loop-relevant variables in the analyzed loop. + + \param m + The number of inequalities in \p cs. \param cs_out1 The first output constraint system. @@ -149,6 +157,14 @@ fill_constraint_systems_MS(const Constraint_System& cs, as follows: - \f$ x'_1, \ldots, x'_n \f$ go onto \f$ 0, \ldots, n-1 \f$; - \f$ x_1, \ldots, x_n \f$ go onto \f$ n, \ldots, 2n-1 \f$; + . + The system does not contain any equality. + + \param n + The number of loop-relevant variables in the analyzed loop. + + \param m + The number of inequalities in \p cs. \param cs_out The output constraint system, where variables indices are allocated @@ -187,9 +203,15 @@ fill_constraint_systems_MS(const Constraint_System& cs, + \vect{v}_3^\transpose (A_C+A_C') &= \vect{0}^\transpose, \\ \vect{v}_2 \vect{b}_B + \vect{v}_3 \vect{b}_C - &< 0. + &< 0, \end{aligned} \f] + where \f$ \vect{v}_1 \f$, \f$ \vect{v}_2 \f$ and \f$ \vect{v}_3 \f$ + are constrained to be nonnegative. + The space of ranking functions is then spanned by + \f$ \vect{v}_3^\transpose A_C' \vect x \f$. + + The ranking functions are expressed by L2 * A' * x, In contrast, our encoding is of the form \f[ @@ -209,44 +231,24 @@ fill_constraint_systems_MS(const Constraint_System& cs, \f] where \f$ {E}_B = -{A}_B \f$, \f$ {E}_C = -{A}_C \f$, \f$ {E}'_C = -{A}'_C \f$, \f$ \vect{d}_B = \vect{b}_B \f$ - and \f$ \vect{d}_B = \vect{b}_B \f$. + and \f$ \vect{d}_C = \vect{b}_C \f$. The corresponding system is: \f[ \begin{aligned} - (\vect{v}_1-\vect{v}_2)^\transpose A_B - - \vect{v}_3^\transpose A_C + (\vect{u}_1-\vect{u}_2)^\transpose E_B + - \vect{u}_3^\transpose E_C &= \vect{0}^\transpose, \\ - \vect{v}_2^\transpose A_B - + \vect{v}_3^\transpose (A_C+A_C') + \vect{u}_2^\transpose E_B + + \vect{u}_3^\transpose (E_C+E_C') &= \vect{0}^\transpose, \\ - \vect{v}_2 \vect{b}_B + \vect{v}_3 \vect{b}_C - &< 0. + \vect{u}_2 \vect{b}_B + \vect{u}_3 \vect{b}_C + &> 0, \end{aligned} \f] - -% parts. -% Loop is encoded as (A|A') * (x|x') <= b and the system is: -% L1 * A' = 0, (L1-L2) * A = 0, L2 * (A+A') = 0, L2 * b < 0. -% Here we reuse as much as possible from the SVG-MS method, so our loop -% comes in encoded as (C'|C) * (x'|x) + d >= 0 -% where the primed part comes first due to an implementation choice. -% We then have A' = -C', A = -C, b = d and the system becomes: -% L1 * C' = 0, (L1-L2) * C = 0, L2 * (C+C') = 0, L2 * d < 0. -% Note the change in the last inequality. -% But, instead of looking for L1 and L2, we look for N1=-L1 and N2=-L2. -% So the final system becomes -% N1 * C' = 0, (N1-N2) * C = 0, N2 * (C+C') = 0, N2 * d > 0. -% Note the change (again) in the last inequality. -% In addition to that, nonnegativity constraints on L1 and L2 are now -% expressed as nonpositivity constraints on N1 and N2. - -% The ranking functions are expressed by L2 * A' * x, which -% becomes L2 * (-C') * x, which becomes N2 * C' * x. - -% Variables have numbers between 0 and N-1 included, i.e., we have -% N duplicate (primed) variables numbered 0, ..., N-1 and N original -% (unprimed) variables numbered N, ..., 2*N-1. - + where \f$ \vect{u}_1 \f$, \f$ \vect{u}_2 \f$ and \f$ \vect{u}_3 \f$ + are constrained to be nonpositive. + The space of ranking functions is then spanned by + \f$ \vect{u}_3^\transpose E_C' \vect x \f$. */ void fill_constraint_systems_PR(const Constraint_System& cs, @@ -254,7 +256,7 @@ fill_constraint_systems_PR(const Constraint_System& cs, const dimension_type m, Constraint_System& cs_out) { // Determine the partitioning of the m rows into the r rows - // of A_B and the s rows of A_C|A'_C (see the paper). + // of E_B and the s rows of E_C|E'_C. std::deque<bool> in_A_B(m, true); dimension_type r = m; for (Constraint_System::const_iterator i = cs.begin(),

1 0

[GIT] ppl/w3ppl(master): Added BozgaGI09.
by Roberto Bagnara 07 Mar '10

07 Mar '10

Module: ppl/w3ppl Branch: master Commit: dfd311c0b0b53006516613b7fac94d7cfbb4ce00 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=dfd311c0b0… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Mar 7 19:23:29 2010 +0400 Added BozgaGI09. --- htdocs/Documentation/ppl_citations.bib | 38 ++++++++++++++++++++++++++++++++ 1 files changed, 38 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib index a83eb79..e51ce00 100644 --- a/htdocs/Documentation/ppl_citations.bib +++ b/htdocs/Documentation/ppl_citations.bib @@ -346,6 +346,44 @@ a basis for an implementation of our representation." } +@Inproceedings{BozgaGI09, + Author = "M. Bozga and C. G\^{\i}rlea and R. Iosif", + Title = "Iterating Octagons", + Booktitle = "Proceedings of the 15th International Conference on + Tools and Algorithms for the Construction and Analysis + of Systems (TACAS 2009)", + Address = "York, UK", + Editor = "S. Kowalewski and A. Philippou", + Publisher = "Springer-Verlag, Berlin", + Series = "Lecture Notes in Computer Science", + Volume = 5505, + Pages = "337-351", + Year = 2009, + ISBN = "978-3-642-00767-5", + Abstract = "In this paper we prove that the transitive closure of a + nondeterministic octagonal relation using integer + counters can be expressed in Presburger arithmetic. The + direct consequence of this fact is that the reachability + problem is decidable for flat counter automata with + octagonal transition relations. This result improves the + previous results of Comon and Jurski [Hubert Comon and + Yan Jurski. Multiple counters automata, safety analysis + and presburger arithmetic. In \emph{CAV}, LNCS 1427, pages + 268–279, 1998] and Bozga, Iosif and Lakhnech [Marius Bozga, + Radu Iosif, and Yassine Lakhnech. Flat parametric counter + automata. In \emph{ICALP}, LNCS 4052, pages 577–588. + Springer-Verlag, 2006] concerning the computation of + transitive closures for difference bound relations. + The importance of this result is justified by the wide + use of octagons to computing sound abstractions of + real-life systems [A. Min\'e. The octagon abstract domain. + \emph{Higher-Order and Symbolic Computation}, 19(1):31–100, + 2006]. We have implemented the octagonal transitive closure + algorithm in a prototype system for the analysis of counter + automata, called FLATA, and we have experimented with a + number of test cases." +} + @Inproceedings{BramanM08, Title = "Safety Verification of Fault Tolerant Goal-based Control Programs with Estimation Uncertainty",

1 0

[GIT] ppl/ppl(termination): Documented the interfaces of the termination analysis functions.
by Roberto Bagnara 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: termination Commit: 5356f0d0a51259885b184650032e3bfae6963a6f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5356f0d0a512… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Mar 7 18:39:34 2010 +0400 Documented the interfaces of the termination analysis functions. --- doc/devref.doxyconf-html.in | 3 + doc/devref.doxyconf-latex.in | 3 + src/termination.cc | 54 ++++++++++---------- src/termination.defs.hh | 114 ++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 147 insertions(+), 27 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=5356f0d0…

1 0

[GIT] ppl/ppl(termination): LaTeX inconsistency removed.
by Roberto Bagnara 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: termination Commit: 0a94878edd54ed691374f0f61b7c35fb3d642caf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0a94878edd54… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Mar 7 16:34:38 2010 +0400 LaTeX inconsistency removed. --- doc/definitions.dox | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 7862099..9d8c2b5 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2302,14 +2302,14 @@ overflow behavior. \f$v_j\f$ in the grid \f$\cL\f$, the wrapped value can be any value \f$a + z \in R\f$ where \f$z \in \Zset\f$. Therefore \f$\cL'\f$ is obtained by adding the parameter - \f$(0, \ldots, 0, v_j, 0, \dots, 0)\f$, + \f$(0, \ldots, 0, v_j, 0, \ldots, 0)\f$, where \f$v_j = 1\f$, to the generator system for \f$\cL\f$. - Overflow wraps. In this case, if \f$\cL\f$ already satisfies the congruence \f$v_j = a \mod 2^w\f$, for some \f$a \in \Rset\f$, then \f$v_j\f$ is set equal to \f$a'\f$ where \f$a' = a \mod 2^w\f$ and \f$a'\in R\f$. Otherwise, \f$\cL'\f$ is obtained by adding the - parameter \f$(0, \ldots, 0, v_j, 0, \dots, 0)\f$, where + parameter \f$(0, \ldots, 0, v_j, 0, \ldots, 0)\f$, where \f$v_j = 2^w\f$, to the generator system for \f$\cL\f$. \subsection Grid_Widening Widening Operators

1 0

[GIT] ppl/ppl(termination): Moved the utilities for termination analysis to their final destination.
by Roberto Bagnara 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: termination Commit: ef46f1fa94c83138cedfd584654ba41684ef43d6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ef46f1fa94c8… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Mar 7 15:52:03 2010 +0400 Moved the utilities for termination analysis to their final destination. --- src/Makefile.am | 3 + src/termination.cc | 278 +++++++++++++++++++++ src/termination.defs.hh | 59 +++++ src/termination.templates.hh | 358 +++++++++++++++++++++++++++ tests/Polyhedron/termination1.cc | 498 -------------------------------------- 5 files changed, 698 insertions(+), 498 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=ef46f1fa…

1 0

[GIT] ppl/ppl(termination): Several improvements. Changed the encoding of the input systems. Started drafting the implementation of the method of Podelski and Rybalchenko .
by Roberto Bagnara 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: termination Commit: 5d2d2e0aa6341133e05220f4892e4c853693608b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5d2d2e0aa634… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Mar 7 14:32:06 2010 +0400 Several improvements. Changed the encoding of the input systems. Started drafting the implementation of the method of Podelski and Rybalchenko. --- tests/Polyhedron/termination1.cc | 263 +++++++++++++++++++++++++++---------- 1 files changed, 192 insertions(+), 71 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=5d2d2e0a…

1 0

[GIT] ppl/ppl(sparse_matrices): Temporarily add unneeded includes to please KDevelop4.
by Marco Poletti 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: ec1ceeb8dffde588e0f407486dacb5781c8c1ac5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ec1ceeb8dffd… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Mar 7 10:36:30 2010 +0100 Temporarily add unneeded includes to please KDevelop4. --- src/Sparse_Matrix.inlines.hh | 4 ++++ src/Sparse_Row.inlines.hh | 4 ++++ src/Unlimited_Sparse_Row.inlines.hh | 4 ++++ ...ited_Sparse_Row_Custom_Slist_Backend.inlines.hh | 3 +++ 4 files changed, 15 insertions(+), 0 deletions(-) diff --git a/src/Sparse_Matrix.inlines.hh b/src/Sparse_Matrix.inlines.hh index 9642ebe..94f15bf 100644 --- a/src/Sparse_Matrix.inlines.hh +++ b/src/Sparse_Matrix.inlines.hh @@ -23,6 +23,10 @@ site: http://www.cs.unipr.it/ppl/ . */ #ifndef PPL_Sparse_Matrix_inlines_hh #define PPL_Sparse_Matrix_inlines_hh 1 +// FIXME: Remove this. +// It's needed only to please KDevelop4. +#include "Sparse_Matrix.defs.hh" + namespace Parma_Polyhedra_Library { inline diff --git a/src/Sparse_Row.inlines.hh b/src/Sparse_Row.inlines.hh index 61e72fa..4d15e42 100644 --- a/src/Sparse_Row.inlines.hh +++ b/src/Sparse_Row.inlines.hh @@ -23,6 +23,10 @@ site: http://www.cs.unipr.it/ppl/ . */ #ifndef PPL_Sparse_Row_inlines_hh #define PPL_Sparse_Row_inlines_hh 1 +// FIXME: Remove this. +// It's needed only to please KDevelop4. +#include "Sparse_Row.defs.hh" + namespace Parma_Polyhedra_Library { inline diff --git a/src/Unlimited_Sparse_Row.inlines.hh b/src/Unlimited_Sparse_Row.inlines.hh index 268ef17..3ec0bd7 100644 --- a/src/Unlimited_Sparse_Row.inlines.hh +++ b/src/Unlimited_Sparse_Row.inlines.hh @@ -29,6 +29,10 @@ site: http://www.cs.unipr.it/ppl/ . */ #include <limits> #include <algorithm> +// FIXME: Remove this. +// It's needed only to please KDevelop4. +#include "Unlimited_Sparse_Row.defs.hh" + namespace Parma_Polyhedra_Library { inline diff --git a/src/Unlimited_Sparse_Row_Custom_Slist_Backend.inlines.hh b/src/Unlimited_Sparse_Row_Custom_Slist_Backend.inlines.hh index aa222fd..e7b19d0 100644 --- a/src/Unlimited_Sparse_Row_Custom_Slist_Backend.inlines.hh +++ b/src/Unlimited_Sparse_Row_Custom_Slist_Backend.inlines.hh @@ -23,6 +23,9 @@ site: http://www.cs.unipr.it/ppl/ . */ #ifndef PPL_Unlimited_Sparse_Row_Custom_Slist_Backend_inlines_hh #define PPL_Unlimited_Sparse_Row_Custom_Slist_Backend_inlines_hh 1 + +// FIXME: Remove this. +// It's needed only to please KDevelop4. #include "Unlimited_Sparse_Row_Custom_Slist_Backend.defs.hh" namespace Parma_Polyhedra_Library {

1 0

[GIT] ppl/ppl(sparse_matrices): Unlimited_Sparse_Row_Custom_Slist_Backend: fix splice() so assert() does not fail.
by Marco Poletti 07 Mar '10

07 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: 22b762aa0e5a8a19a7e16c830a31f4018e5b165f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=22b762aa0e5a… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Mar 7 10:22:49 2010 +0100 Unlimited_Sparse_Row_Custom_Slist_Backend: fix splice() so assert() does not fail. --- ...ited_Sparse_Row_Custom_Slist_Backend.inlines.hh | 10 ++++++++-- 1 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/Unlimited_Sparse_Row_Custom_Slist_Backend.inlines.hh b/src/Unlimited_Sparse_Row_Custom_Slist_Backend.inlines.hh index 730a5d6..aa222fd 100644 --- a/src/Unlimited_Sparse_Row_Custom_Slist_Backend.inlines.hh +++ b/src/Unlimited_Sparse_Row_Custom_Slist_Backend.inlines.hh @@ -181,8 +181,11 @@ Unlimited_Sparse_Row_Custom_Slist_Backend::splice( x.last = i.p; to_move->next = *(position.p); *(position.p) = to_move; - // i_itr points to the moved element. dangerous_iterator i_itr = position; +#ifndef NDEBUG + i_itr.q = *(i_itr.p); +#endif + // i_itr points to the moved element. position.p = &(to_move->next); #ifndef NDEBUG position.q = *(position.p); @@ -219,8 +222,11 @@ Unlimited_Sparse_Row_Custom_Slist_Backend::splice( // We moved some elements from the end of x, so x.last must be updated. x.last = first1.p; *(last1.p) = tail; - // first_itr points to the first added element dangerous_iterator first_itr = position; +#ifndef NDEBUG + first_itr.q = *(first_itr.p); +#endif + // first_itr points to the first added element position.p = last1.p; #ifndef NDEBUG position.q = *(position.p);

1 0

[GIT] ppl/ppl(termination): Added functions for termination analysis following the approach of Mesnard and Serebrenik .
by Roberto Bagnara 06 Mar '10

06 Mar '10

Module: ppl/ppl Branch: termination Commit: e66a1705f54a53ea33fa8ba0164fe10518da1093 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e66a1705f54a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Mar 6 21:46:52 2010 +0400 Added functions for termination analysis following the approach of Mesnard and Serebrenik. --- tests/Polyhedron/Makefile.am | 3 + tests/Polyhedron/termination1.cc | 465 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 468 insertions(+), 0 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=e66a1705…

1 0

[GIT] ppl/ppl(termination): Added method bool Constraint_System:: has_equalities() const.
by Roberto Bagnara 06 Mar '10

06 Mar '10

Module: ppl/ppl Branch: termination Commit: c6433c0db9272e38f2a0d01cb50a23b8f5b0f554 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c6433c0db927… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Mar 5 22:18:05 2010 +0400 Added method bool Constraint_System::has_equalities() const. --- src/Constraint_System.cc | 10 ++++++++++ src/Constraint_System.defs.hh | 6 ++++++ 2 files changed, 16 insertions(+), 0 deletions(-) diff --git a/src/Constraint_System.cc b/src/Constraint_System.cc index 2e6444a..5658058 100644 --- a/src/Constraint_System.cc +++ b/src/Constraint_System.cc @@ -206,6 +206,16 @@ adjust_topology_and_space_dimension(const Topology new_topology, } bool +PPL::Constraint_System::has_equalities() const { + const Constraint_System& cs = *this; + // We verify if the system has equalities also in the pending part. + for (dimension_type i = cs.num_rows(); i-- > 0; ) + if (cs[i].is_equality()) + return true; + return false; +} + +bool PPL::Constraint_System::has_strict_inequalities() const { if (is_necessarily_closed()) return false; diff --git a/src/Constraint_System.defs.hh b/src/Constraint_System.defs.hh index 008eac1..7ce79ef 100644 --- a/src/Constraint_System.defs.hh +++ b/src/Constraint_System.defs.hh @@ -152,6 +152,12 @@ public: /*! \brief Returns <CODE>true</CODE> if and only if \p *this + contains one or more equality constraints. + */ + bool has_equalities() const; + + /*! \brief + Returns <CODE>true</CODE> if and only if \p *this contains one or more strict inequality constraints. */ bool has_strict_inequalities() const;

1 0