March 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(termination): Added the new termination functions to Prolog interface and
by Patricia Hill 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: 07ba164136b4181c4e51b1994eb2b858c692814f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=07ba164136b4… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon Mar 8 12:39:37 2010 +0000 Added the new termination functions to Prolog interface and the termination_test_MS only to the C interface. --- interfaces/C/ppl_interface_generator_c_cc_code.m4 | 12 ++++ interfaces/C/ppl_interface_generator_c_h_code.m4 | 9 +++ ...l_interface_generator_c_procedure_generators.m4 | 1 + .../ppl_interface_generator_prolog_cc_code.m4 | 55 ++++++++++++++++++++ .../ppl_interface_generator_prolog_hh_code.m4 | 20 +++++++ ...erface_generator_prolog_procedure_generators.m4 | 8 +++- interfaces/ppl_interface_generator_common_dat.m4 | 6 ++- 7 files changed, 109 insertions(+), 2 deletions(-) diff --git a/interfaces/C/ppl_interface_generator_c_cc_code.m4 b/interfaces/C/ppl_interface_generator_c_cc_code.m4 index 6f5b80d..22ddd23 100644 --- a/interfaces/C/ppl_interface_generator_c_cc_code.m4 +++ b/interfaces/C/ppl_interface_generator_c_cc_code.m4 @@ -1156,6 +1156,18 @@ CATCH_ALL ') +m4_define(`ppl_@CLASS@_termination_test_MS_code', +`dnl +int +ppl_@CLASS@_termination_test_MS +(ppl_const_@CLASS@_t x) try { + const @CPP_CLASS@& xx = *to_const(x); + return termination_test_MS(xx); +} +CATCH_ALL + +') + m4_define(`ppl_@CLASS@_wrap_assign_code', `int ppl_@CLASS@_wrap_assign diff --git a/interfaces/C/ppl_interface_generator_c_h_code.m4 b/interfaces/C/ppl_interface_generator_c_h_code.m4 index 861af48..39f717e 100644 --- a/interfaces/C/ppl_interface_generator_c_h_code.m4 +++ b/interfaces/C/ppl_interface_generator_c_h_code.m4 @@ -34,6 +34,15 @@ dnl There is no code at present for these procedures in the C interface. dnl Remove the macro if its definition is added. dnl +m4_define(`ppl_@CLASS@_termination_test_MS_code', +`dnl +/*! \relates ppl_@CLASS@_tag */ +int +ppl_@CLASS@_termination_test_MS +PPL_PROTO((ppl_const_@CLASS@_t x)); + +') + m4_define(`ppl_@CLASS@_linear_@PARTITION@_code', `dnl /*! \relates ppl_@CLASS@_tag */ diff --git a/interfaces/C/ppl_interface_generator_c_procedure_generators.m4 b/interfaces/C/ppl_interface_generator_c_procedure_generators.m4 index 9aa2a19..7f590d7 100644 --- a/interfaces/C/ppl_interface_generator_c_procedure_generators.m4 +++ b/interfaces/C/ppl_interface_generator_c_procedure_generators.m4 @@ -44,5 +44,6 @@ ppl_new_@TOPOLOGY@@CLASS@_recycle_@BUILD_REPRESENT@s +simple, ppl_assign_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@ +simple, ppl_@CLASS@_add_recycled_@CLASS_REPRESENT@s +simple, ppl_@CLASS@_wrap_assign +simple, +ppl_@CLASS@_termination_test_MS +simple, ) ') diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 index cd1f2f7..0fd0510 100644 --- a/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 +++ b/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 @@ -1228,6 +1228,61 @@ m4_define(`ppl_@CLASS@_bounded_@AFFIMAGE@_code', ') +m4_define(`ppl_@CLASS@_termination_test_@TERMINATION_ID@_code', + `extern "C" Prolog_foreign_return_type + ppl_@CLASS@_termination_test_@TERMINATION_ID@ + (Prolog_term_ref t_ph) { + static const char* where = "ppl_@CLASS@_termination_test_@TERMINATION_ID@/1"; + try { + @CPP_CLASS@* ph = term_to_handle<@CPP_CLASS@ >(t_ph, where); + PPL_CHECK(ph); + if (Parma_Polyhedra_Library::termination_test_@TERMINATION_ID@(*ph)) + return PROLOG_SUCCESS; + } + CATCH_ALL; +} + +') + +m4_define(`ppl_@CLASS@_one_affine_ranking_function_@TERMINATION_ID@_code', + `extern "C" Prolog_foreign_return_type + ppl_@CLASS@_one_affine_ranking_function_@TERMINATION_ID@ + (Prolog_term_ref t_x, + Prolog_term_ref t_g) { + static const char* where = "ppl_@CLASS@_one_affine_ranking_function_@TERMINATION_ID@/2"; + try { + @CPP_CLASS@* x = term_to_handle<@CPP_CLASS@ >(t_x, where); + Generator gg(point()); + PPL_CHECK(x); + if (Parma_Polyhedra_Library::one_affine_ranking_function_@TERMINATION_ID@(*x, gg) + && Prolog_unify(t_g, generator_term(gg))) + return PROLOG_SUCCESS; + } + CATCH_ALL; +} + +') + +m4_define(`ppl_@CLASS@_all_affine_ranking_functions_@TERMINATION_ID@_code', + `extern "C" Prolog_foreign_return_type + ppl_@CLASS@_all_affine_ranking_functions_@TERMINATION_ID@ + (Prolog_term_ref t_x, + Prolog_term_ref t_ph) { + static const char* where = + "ppl_@CLASS@_all_affine_ranking_functions_@TERMINATION_ID@/2"; + try { + @CPP_CLASS@* x = term_to_handle<@CPP_CLASS@ >(t_x, where); + C_Polyhedron* ph = term_to_handle<C_Polyhedron >(t_ph, where); + PPL_CHECK(x); + Parma_Polyhedra_Library::all_affine_ranking_functions_@TERMINATION_ID@(*x, + *ph); + return PROLOG_SUCCESS; + } + CATCH_ALL; +} + +') + m4_define(`ppl_@CLASS@_@WIDEN@_widening_assign_with_tokens_code', `extern "C" Prolog_foreign_return_type ppl_@CLASS@_@WIDEN@_widening_assign_with_tokens diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4 index f1667b9..bc50e6b 100644 --- a/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4 +++ b/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4 @@ -510,3 +510,23 @@ m4_define(`ppl_@CLASS@_@MEMBYTES@_code', Prolog_term_ref t_m); ') + +m4_define(`ppl_@CLASS@_termination_test_MS_code', + `extern "C" Prolog_foreign_return_type + ppl_@CLASS@_termination_test_MS(Prolog_term_ref t_x); + +') + +m4_define(`ppl_@CLASS@_one_affine_ranking_function_MS_code', + `extern "C" Prolog_foreign_return_type + ppl_@CLASS@_one_affine_ranking_function_MS(Prolog_term_ref t_x, + Prolog_term_ref t_g); + +') + +m4_define(`ppl_@CLASS@_all_affine_ranking_functions_MS_code', + `extern "C" Prolog_foreign_return_type + ppl_@CLASS@_all_affine_ranking_functions_MS(Prolog_term_ref t_x, + Prolog_term_ref t_g); + +') diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 index 3105be7..08798d0 100644 --- a/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 +++ b/interfaces/Prolog/ppl_interface_generator_prolog_procedure_generators.m4 @@ -85,4 +85,10 @@ ppl_MIP_Problem_OK/1 ppl_MIP_Problem_ascii_dump/1`'dnl ') -m4_define(`m4_procedure_list', `m4_common_procedure_list') +m4_define(`m4_procedure_list', + `m4_echo_unquoted(`m4_common_procedure_list', +ppl_@CLASS@_termination_test_MS/1 +simple, +ppl_@CLASS@_one_affine_ranking_function_MS/2 +simple, +ppl_@CLASS@_all_affine_ranking_functions_MS/2 +simple, +) +') diff --git a/interfaces/ppl_interface_generator_common_dat.m4 b/interfaces/ppl_interface_generator_common_dat.m4 index ca20896..64ae91f 100644 --- a/interfaces/ppl_interface_generator_common_dat.m4 +++ b/interfaces/ppl_interface_generator_common_dat.m4 @@ -530,7 +530,8 @@ point, constrainer, disjunct, disjunct_topology, -disjunct_extrapolation') +disjunct_extrapolation, +termination_id') dnl --------------------------------------------------------------------- dnl Define the replacement macros for all patterns @@ -984,3 +985,6 @@ m4_define(`m4_membytes_replacements', `external_memory_in_bytes, total_memory_in_bytes') m4_define(`m4_Pointset_Powerset_membytes_replacements', `m4_membytes_replacements, size') + +dnl The termination algorithms are either sourced from MS or PR. +m4_define(`m4_termination_id_replacements', `MS, PR')

1 0

[GIT] ppl/ppl(sparse_matrices): New commits
by Roberto Bagnara 08 Mar '10

08 Mar '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4d6afbff3e99… Merge: ec1ceeb8dffde588e0f407486dacb5781c8c1ac5 54bf68f9ee93822f8792c0d89d45ebd0b5823aee Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Mon Mar 8 13:30:30 2010 +0100 Merge branch 'master' into sparse_matrices URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=54bf68f9ee93… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Mar 8 16:24:38 2010 +0400 Use \link ... \endlink consistently. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d054a83797b9… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Mar 7 11:36:11 2010 +0100 Corrected an invalid reference bug in PIP_Solution_Node::update_tableau(). The addition of tableau rows invalidates previously computed references. Thanks to Marco Poletti for reporting this. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fad4a942862… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Mar 7 21:13:37 2010 +0100 Eventually perform solution tree simplifications after incremental addition of parameter constraints. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f010ef5edd82… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Mar 7 20:27:09 2010 +0100 Moved the compatibility_check static methods to PIP_Tree_Node. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a7af846ade60… Author: François Galea <francois.galea(a)uvsq.fr> Date: Sun Mar 7 20:25:00 2010 +0100 Added one more test for incremental solving. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=22d7dc4353fc… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 6 09:23:32 2010 +0100 Corrected a couple of typos in the documentation. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6ed63be5fa24… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Mar 6 08:31:33 2010 +0100 Test 4 in digitalfilers1.cc overflows with 64-bits if assertions are on. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fa2669e96e9… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Mar 5 18:09:15 2010 +0100 Tests 20, 21 and 22 overflow on 8-bit coefficients (derived from test02). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=be7b34ac1879… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Mar 4 17:57:23 2010 +0100 Encoded custom overflow conditions for digitalfilters1.cc tests 5 and 6. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c4b4cb73d97d… Author: François Galea <francois.galea(a)uvsq.fr> Date: Thu Mar 4 14:14:05 2010 +0100 Added a test for problem feasibility when incrementally adding parameter constraints. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9a06b9697b65… Author: François Galea <francois.galea(a)uvsq.fr> Date: Thu Mar 4 13:59:59 2010 +0100 Added two tests for incremental addition of parametric constraints. Even though correct, the resulting solution trees can be simplified. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e961e540b837… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Mar 4 10:09:37 2010 +0400 Replaced using directives by using declarations. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8ca010b524e4… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Mar 3 22:13:57 2010 +0400 Apparently GNU Hurd only supports ITIMER_REAL. (Thanks to Michael Tautschnig: http://www.cs.unipr.it/pipermail/ppl-devel/2010-March/016072.html). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=aeb2709a41cb… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Mar 3 22:07:01 2010 +0400 Proper spacing added to throw_syscall_error(). (Thanks to Michael Tautschnig.) URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e9c769a3992b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Mar 2 22:09:29 2010 +0100 Detected several overflows in tests 5 and 6 of digitalfilters1.cc. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b72c39080c69… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Mar 2 22:07:29 2010 +0100 Adopted a more flexible implementation for the DO_TEST* macros. (Based on a set of macros provided by Abramo Bagnara.) URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6503e77440bc… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Mar 2 14:59:10 2010 +0100 Made a pass on the documentation of class PIP_Problem. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=802e03131e75… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Mar 1 23:58:07 2010 +0100 Method PIP_Tree_Node::solve() now checks context feasibility when needed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=893ad34ee7a5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Mar 1 23:57:03 2010 +0100 Corrected typo in test19(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8daf23edd9ad… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Mar 1 23:43:41 2010 +0100 Several minor improvements to the PIP_Problem resolution process. Reorganized helper functions update_context() and compatibility_check(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=90f18fa7da95… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon Mar 1 11:05:37 2010 +0000 The wrap_assign has only been added to the C interface so the procedure must be local to the C interface. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0a65a2985d7b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Mar 1 11:15:05 2010 +0100 Completed removal of support for circular intervals. Removed now ambiguous method CC76_narrowing_assign(). While at it, also wrapped a few long lines. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=57c7504c6e09… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon Mar 1 08:45:34 2010 +0000 Added C interface for wrap_assign. Minor NELS improvements to documentation describing Wrapping Operator (should be checked by the author of these notes).

1 0

[GIT] ppl/ppl(termination): Merge branch 'master' into termination
by Roberto Bagnara 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: e804f7e233464910224f77941ed59355abb504f1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e804f7e23346… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Mar 8 16:25:15 2010 +0400 Merge branch 'master' into termination ---

1 0

[GIT] ppl/ppl(termination): Use \link ... \endlink consistently.
by Roberto Bagnara 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: 54bf68f9ee93822f8792c0d89d45ebd0b5823aee URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=54bf68f9ee93… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Mar 8 16:24:38 2010 +0400 Use \link ... \endlink consistently. --- doc/definitions.dox | 38 +++++++++++++++----------------------- 1 files changed, 15 insertions(+), 23 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 7862099..1563ff1 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -105,7 +105,7 @@ Other semantic GDs, the compound classes, can be constructed These include: - \link Parma_Polyhedra_Library::Pointset_Powerset \c Pointset_Powerset\<PS\> \endlink, - \link Parma_Polyhedra_Library::Partially_Reduced_Product <CODE>Partially_Reduced_Product\<D1, D2, R\></CODE> \endlink, - + . where \c PS, \c D1 and \c D2 can be any semantic GD classes and \c R is the reduction operation to be applied to the component domains of the product class. @@ -2634,28 +2634,20 @@ include the infinities \f$-\infty\f$ and \f$+\infty\f$. \subsection interval_linear_forms Linear forms with interval coefficients Generic concrete floating point expressions on \f$\mathbb{F}_t\f$ are -represented by the \link Parma_Polyhedra_Library::Floating_Point_Expression -\c Floating_Point_Expression \endlink abstract class. Its concrete derivate -classes are: - - \link Parma_Polyhedra_Library::Constant_Floating_Point_Expression \c - Constant_Floating_Point_Expression \endlink, - - \link Parma_Polyhedra_Library::Variable_Floating_Point_Expression \c - Variable_Floating_Point_Expression \endlink, - - \link Parma_Polyhedra_Library::Opposite_Floating_Point_Expression \c - Opposite_Floating_Point_Expression \endlink, that is the negation - (unary minus) of a floating point expression, - - \link Parma_Polyhedra_Library::Sum_Floating_Point_Expression \c - Sum_Floating_Point_Expression \endlink, that is the sum of two floating - point expressions, - - \link Parma_Polyhedra_Library::Difference_Floating_Point_Expression \c - Difference_Floating_Point_Expression \endlink, that is the difference of - two floating point expressions, - - \link Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression \c - Multiplication_Floating_Point_Expression \endlink, that is the product of - two floating point expressions, and - - \link Parma_Polyhedra_Library::Division_Floating_Point_Expression \c - Division_Floating_Point_Expression \endlink, that is the division of - two floating point expressions. +represented by the \link Parma_Polyhedra_Library::Floating_Point_Expression \c Floating_Point_Expression \endlink +abstract class. Its concrete derivate classes are: + - \link Parma_Polyhedra_Library::Constant_Floating_Point_Expression \c Constant_Floating_Point_Expression \endlink, + - \link Parma_Polyhedra_Library::Variable_Floating_Point_Expression \c Variable_Floating_Point_Expression \endlink, + - \link Parma_Polyhedra_Library::Opposite_Floating_Point_Expression \c Opposite_Floating_Point_Expression \endlink, + that is the negation (unary minus) of a floating point expression, + - \link Parma_Polyhedra_Library::Sum_Floating_Point_Expression \c Sum_Floating_Point_Expression \endlink, + that is the sum of two floating point expressions, + - \link Parma_Polyhedra_Library::Difference_Floating_Point_Expression \c Difference_Floating_Point_Expression \endlink, + that is the difference of two floating point expressions, + - \link Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression \c Multiplication_Floating_Point_Expression \endlink, + that is the product of two floating point expressions, and + - \link Parma_Polyhedra_Library::Division_Floating_Point_Expression \c Division_Floating_Point_Expression \endlink, + that is the division of two floating point expressions. The set of all the possible values in \f$\mathbb{F}_t\f$ of a floating point expression at a given program point in a given abstract store can be

1 0

[GIT] ppl/ppl(master): Use \link ... \endlink consistently.
by Roberto Bagnara 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: master Commit: 54bf68f9ee93822f8792c0d89d45ebd0b5823aee URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=54bf68f9ee93… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Mar 8 16:24:38 2010 +0400 Use \link ... \endlink consistently. --- doc/definitions.dox | 38 +++++++++++++++----------------------- 1 files changed, 15 insertions(+), 23 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 7862099..1563ff1 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -105,7 +105,7 @@ Other semantic GDs, the compound classes, can be constructed These include: - \link Parma_Polyhedra_Library::Pointset_Powerset \c Pointset_Powerset\<PS\> \endlink, - \link Parma_Polyhedra_Library::Partially_Reduced_Product <CODE>Partially_Reduced_Product\<D1, D2, R\></CODE> \endlink, - + . where \c PS, \c D1 and \c D2 can be any semantic GD classes and \c R is the reduction operation to be applied to the component domains of the product class. @@ -2634,28 +2634,20 @@ include the infinities \f$-\infty\f$ and \f$+\infty\f$. \subsection interval_linear_forms Linear forms with interval coefficients Generic concrete floating point expressions on \f$\mathbb{F}_t\f$ are -represented by the \link Parma_Polyhedra_Library::Floating_Point_Expression -\c Floating_Point_Expression \endlink abstract class. Its concrete derivate -classes are: - - \link Parma_Polyhedra_Library::Constant_Floating_Point_Expression \c - Constant_Floating_Point_Expression \endlink, - - \link Parma_Polyhedra_Library::Variable_Floating_Point_Expression \c - Variable_Floating_Point_Expression \endlink, - - \link Parma_Polyhedra_Library::Opposite_Floating_Point_Expression \c - Opposite_Floating_Point_Expression \endlink, that is the negation - (unary minus) of a floating point expression, - - \link Parma_Polyhedra_Library::Sum_Floating_Point_Expression \c - Sum_Floating_Point_Expression \endlink, that is the sum of two floating - point expressions, - - \link Parma_Polyhedra_Library::Difference_Floating_Point_Expression \c - Difference_Floating_Point_Expression \endlink, that is the difference of - two floating point expressions, - - \link Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression \c - Multiplication_Floating_Point_Expression \endlink, that is the product of - two floating point expressions, and - - \link Parma_Polyhedra_Library::Division_Floating_Point_Expression \c - Division_Floating_Point_Expression \endlink, that is the division of - two floating point expressions. +represented by the \link Parma_Polyhedra_Library::Floating_Point_Expression \c Floating_Point_Expression \endlink +abstract class. Its concrete derivate classes are: + - \link Parma_Polyhedra_Library::Constant_Floating_Point_Expression \c Constant_Floating_Point_Expression \endlink, + - \link Parma_Polyhedra_Library::Variable_Floating_Point_Expression \c Variable_Floating_Point_Expression \endlink, + - \link Parma_Polyhedra_Library::Opposite_Floating_Point_Expression \c Opposite_Floating_Point_Expression \endlink, + that is the negation (unary minus) of a floating point expression, + - \link Parma_Polyhedra_Library::Sum_Floating_Point_Expression \c Sum_Floating_Point_Expression \endlink, + that is the sum of two floating point expressions, + - \link Parma_Polyhedra_Library::Difference_Floating_Point_Expression \c Difference_Floating_Point_Expression \endlink, + that is the difference of two floating point expressions, + - \link Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression \c Multiplication_Floating_Point_Expression \endlink, + that is the product of two floating point expressions, and + - \link Parma_Polyhedra_Library::Division_Floating_Point_Expression \c Division_Floating_Point_Expression \endlink, + that is the division of two floating point expressions. The set of all the possible values in \f$\mathbb{F}_t\f$ of a floating point expression at a given program point in a given abstract store can be

1 0

[GIT] ppl/ppl(termination): Comments improved.
by Roberto Bagnara 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: c59646077762fcf090705ece6876b8ef35623c8b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c59646077762… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Mar 8 15:41:23 2010 +0400 Comments improved. --- src/termination.cc | 49 +++++++++++++++++++++++++++++-------------------- 1 files changed, 29 insertions(+), 20 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index d0d1909..a643997 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -60,8 +60,10 @@ assign_all_inequalities_approximation(const C_Polyhedron& ph, \param cs 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 space dimensions + \f$ 0, \ldots, n-1 \f$, + - \f$ x_1, \ldots, x_n \f$ go onto space dimensions + \f$ n, \ldots, 2n-1 \f$, . The system does not contain any equality. @@ -80,17 +82,20 @@ assign_all_inequalities_approximation(const C_Polyhedron& ph, The allocation of variable indices in the output constraint systems \p cs_out1 and \p cs_out2 is as follows: - - \f$ \mu_1, \ldots, \mu_n \f$ go onto \f$ 0, \ldots, n-1 \f$; - - \f$ \mu_0\f$ goes onto \f$ n \f$; - - \f$ y_1, \ldots, y_m \f$ go onto \f$ n+1, \ldots, n+m \f$; - + - \f$ \mu_1, \ldots, \mu_n \f$ go onto space dimensions + \f$ 0, \ldots, n-1 \f$; + - \f$ \mu_0\f$ goes onto space dimension \f$ n \f$; + - \f$ y_1, \ldots, y_m \f$ go onto space dimensions + \f$ n+1, \ldots, n+m \f$; + . if we use the same constraint system, that is <CODE>&cs_out1 == &cs_out2</CODE>, then - - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ - go onto \f$ n+m+1, ..., n+2*m+2 \f$; - + - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ go onto space dimensions + \f$ n+m+1, ..., n+2*m+2 \f$; + . otherwise - - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ go onto \f$ n+1, ..., n+m+2 \f$. + - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ go onto space dimensions + \f$ n+1, ..., n+m+2 \f$. */ void fill_constraint_systems_MS(const Constraint_System& cs, @@ -155,8 +160,10 @@ fill_constraint_systems_MS(const Constraint_System& cs, \param cs 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 space dimensions + \f$ 0, \ldots, n-1 \f$, + - \f$ x_1, \ldots, x_n \f$ go onto space dimensions + \f$ n, \ldots, 2n-1 \f$, . The system does not contain any equality. @@ -169,11 +176,13 @@ fill_constraint_systems_MS(const Constraint_System& cs, \param cs_out The output constraint system, where variables indices are allocated as follows: - - \f$ \mu_1, \ldots, \mu_n \f$ go onto \f$ 0, \ldots, n-1 \f$; - - \f$ \mu_0\f$ goes onto \f$ n \f$; - - \f$ y_1, \ldots, y_m \f$ go onto \f$ n+1, \ldots, n+m \f$; - - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ - go onto \f$ n+m+1, ..., n+2*m+2 \f$. + - \f$ \mu_1, \ldots, \mu_n \f$ go onto space dimensions + \f$ 0, \ldots, n-1 \f$; + - \f$ \mu_0\f$ goes onto space dimension \f$ n \f$; + - \f$ y_1, \ldots, y_m \f$ go onto space dimensions + \f$ n+1, \ldots, n+m \f$; + - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ go onto space dimensions + \f$ n+m+1, ..., n+2*m+2 \f$. The improved Podelski-Rybalchenko method described in the paper is based on a loop encoding of the form @@ -250,9 +259,9 @@ fill_constraint_systems_MS(const Constraint_System& cs, The allocation of variable indices in the output constraint system \p cs_out is as follows: - - \f$ u_3 \f$ goes onto \f$ 0, \ldots, s-1 \f$; - - \f$ u_2 \f$ goes onto \f$ s, \ldots, s+r-1 \f$; - - \f$ u_1 \f$ goes onto \f$ s+r, \ldots, s+2r-1 \f$. + - \f$ u_3 \f$ goes onto space dimensions \f$ 0, \ldots, s-1 \f$; + - \f$ u_2 \f$ goes onto space dimensions \f$ s, \ldots, s+r-1 \f$; + - \f$ u_1 \f$ goes onto space dimensions \f$ s+r, \ldots, s+2r-1 \f$. */ void fill_constraint_systems_PR(const Constraint_System& cs,

1 0

[GIT] ppl/ppl(termination): Added a couple of missing constraints.
by Roberto Bagnara 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: cda8c51361f8f975d725c240160b2339471d3fbb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cda8c51361f8… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Mar 8 15:16:40 2010 +0400 Added a couple of missing constraints. --- tests/Polyhedron/termination1.cc | 2 ++ 1 files changed, 2 insertions(+), 0 deletions(-) diff --git a/tests/Polyhedron/termination1.cc b/tests/Polyhedron/termination1.cc index be706f7..4d2fb4e 100644 --- a/tests/Polyhedron/termination1.cc +++ b/tests/Polyhedron/termination1.cc @@ -35,6 +35,7 @@ test01() { ph.add_constraint(2*xp1 + 1 >= x1); ph.add_constraint(2*xp1 <= x1); ph.add_constraint(xp2 == x2 + 1); + ph.add_constraint(xp2 >= 1); C_Polyhedron mu_space; all_affine_ranking_functions_MS(ph, mu_space); @@ -69,6 +70,7 @@ test02() { ph.add_constraint(2*xp1 + 1 >= x1); ph.add_constraint(2*xp1 <= x1); ph.add_constraint(xp2 == x2 + 1); + ph.add_constraint(xp2 >= 1); return termination_test_MS(ph); }

1 0

[GIT] ppl/ppl(termination): Fixed the input polyhedra for test01() and test02().
by Roberto Bagnara 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: 5e848582e1152915695a686a3c13693d497a73b3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5e848582e115… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Mar 8 14:22:41 2010 +0400 Fixed the input polyhedra for test01() and test02(). --- tests/Polyhedron/termination1.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/Polyhedron/termination1.cc b/tests/Polyhedron/termination1.cc index 1484392..be706f7 100644 --- a/tests/Polyhedron/termination1.cc +++ b/tests/Polyhedron/termination1.cc @@ -34,7 +34,7 @@ test01() { ph.add_constraint(x1 >= 2); ph.add_constraint(2*xp1 + 1 >= x1); ph.add_constraint(2*xp1 <= x1); - ph.add_constraint(xp2 + 1 == x2); + ph.add_constraint(xp2 == x2 + 1); C_Polyhedron mu_space; all_affine_ranking_functions_MS(ph, mu_space); @@ -68,7 +68,7 @@ test02() { ph.add_constraint(x1 >= 2); ph.add_constraint(2*xp1 + 1 >= x1); ph.add_constraint(2*xp1 <= x1); - ph.add_constraint(xp2 + 1 == x2); + ph.add_constraint(xp2 == x2 + 1); return termination_test_MS(ph); }

1 0

[GIT] ppl/ppl(termination): Added stub implementations for one_affine_ranking_function_PR() and all_affine_ranking_functions_PR().
by Roberto Bagnara 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: 7bf82f6ed4a2435e5cab78a397340d7ec4accceb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7bf82f6ed4a2… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Mar 8 13:53:49 2010 +0400 Added stub implementations for one_affine_ranking_function_PR() and all_affine_ranking_functions_PR(). --- src/termination.templates.hh | 18 ++++++++++++++++++ 1 files changed, 18 insertions(+), 0 deletions(-) diff --git a/src/termination.templates.hh b/src/termination.templates.hh index ae36551..d7b775e 100644 --- a/src/termination.templates.hh +++ b/src/termination.templates.hh @@ -353,6 +353,24 @@ termination_test_PR(const PSET& pset) { return mip.is_satisfiable(); } +template <typename PSET> +bool +one_affine_ranking_function_PR(const PSET& pset, Generator& mu) { + return false; +} + +template <typename PSET> +void +all_affine_ranking_functions_PR(const PSET& pset, C_Polyhedron& mu_space) { + using namespace Implementation::Termination; + Constraint_System cs; + dimension_type n; + dimension_type m; + prepare_input_MS_PR(pset, cs, n, m, "all_affine_ranking_functions_MS"); + + mu_space = C_Polyhedron(n+1, EMPTY); +} + } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_termination_templates_hh)

1 0

[GIT] ppl/ppl(termination): Merge branch 'master' into termination
by Roberto Bagnara 08 Mar '10

08 Mar '10

Module: ppl/ppl Branch: termination Commit: 0a21fe775ff710ea781ce7d6c751aaacf3615bb2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0a21fe775ff7… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Mar 8 10:44:11 2010 +0100 Merge branch 'master' into termination ---

1 0