December 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Expected failured revised.
by Roberto Bagnara 29 Dec '09

29 Dec '09

Module: ppl/ppl Branch: master Commit: 4fa0f5b2b45fcb1db161490fae10827d864b32b4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4fa0f5b2b45f… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Dec 29 21:21:48 2009 +0100 Expected failured revised. --- tests/Floating_Point_Expression/polyhedron1.cc | 2 +- tests/Floating_Point_Expression/polyhedron2.cc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/Floating_Point_Expression/polyhedron1.cc b/tests/Floating_Point_Expression/polyhedron1.cc index 323f672..8d2be03 100644 --- a/tests/Floating_Point_Expression/polyhedron1.cc +++ b/tests/Floating_Point_Expression/polyhedron1.cc @@ -260,7 +260,7 @@ BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); DO_TEST(test03); - DO_TEST_F16(test04); + DO_TEST_F32A(test04); DO_TEST_F32(test05); DO_TEST(test06); DO_TEST(test07); diff --git a/tests/Floating_Point_Expression/polyhedron2.cc b/tests/Floating_Point_Expression/polyhedron2.cc index 4175882..1b21f16 100644 --- a/tests/Floating_Point_Expression/polyhedron2.cc +++ b/tests/Floating_Point_Expression/polyhedron2.cc @@ -223,5 +223,5 @@ BEGIN_MAIN DO_TEST(test02); DO_TEST(test03); DO_TEST_F32(test04); - DO_TEST_F16(test05); + DO_TEST_F64A(test05); END_MAIN

1 0

[GIT] ppl/ppl(master): Typo fixed.
by Roberto Bagnara 29 Dec '09

29 Dec '09

Module: ppl/ppl Branch: master Commit: 90e5cd14f89dcc75409daa72a744d565f82c599d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=90e5cd14f89d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Dec 29 21:11:08 2009 +0100 Typo fixed. --- tests/Floating_Point_Expression/digitalfilters1.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 3313a13..dfd87c4 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -52,7 +52,7 @@ set_M(Coefficient& M, int m) { if (greater_than(std::numeric_limits<Coefficient>::min(), std::numeric_limits<ANALYZER_FP_FORMAT>::min()) || less_than(std::numeric_limits<Coefficient>::max(), - std::numeric_limits<ANALYZER_FP_FORMAT>::min())) { + std::numeric_limits<ANALYZER_FP_FORMAT>::max())) { // This may still provoke an arithmetic overflow exception: // no problem. assign_r(M, m, ROUND_DOWN);

1 0

[GIT] ppl/ppl(master): Renamed affine_image on Linear Forms into affine_form_image.
by Roberto Amadini 29 Dec '09

29 Dec '09

Module: ppl/ppl Branch: master Commit: 17ee1020a0d93e9dfd71a4f27669e8385d5e241e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=17ee1020a0d9… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Dec 29 20:05:29 2009 +0100 Renamed affine_image on Linear Forms into affine_form_image. --- src/BD_Shape.defs.hh | 43 +++--- src/BD_Shape.templates.hh | 26 ++-- src/Box.defs.hh | 7 +- src/Box.templates.hh | 13 +- src/Octagonal_Shape.defs.hh | 7 +- src/Octagonal_Shape.templates.hh | 10 +- src/Polyhedron.defs.hh | 5 +- src/Polyhedron.templates.hh | 8 +- tests/Floating_Point_Expression/bdshape1.cc | 64 ++++---- tests/Floating_Point_Expression/digitalfilters1.cc | 166 ++++++++++---------- tests/Floating_Point_Expression/octagonalshape1.cc | 64 ++++---- tests/Floating_Point_Expression/polyhedron1.cc | 48 +++--- tests/Floating_Point_Expression/polyhedron2.cc | 4 +- 13 files changed, 237 insertions(+), 228 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=17ee1020…

1 0

[GIT] ppl/ppl(master): Use the general assignment and comparison functions.
by Roberto Bagnara 29 Dec '09

29 Dec '09

Module: ppl/ppl Branch: master Commit: 755fc746e12a3526f1f14e6737f378dbcd15eb9a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=755fc746e12a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Dec 29 17:56:47 2009 +0100 Use the general assignment and comparison functions. --- tests/Floating_Point_Expression/digitalfilters1.cc | 12 ++++++------ 1 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index c9ec1c2..ae1473d 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -49,17 +49,17 @@ for (n = 0; n < N; ++n) { void set_M(Coefficient& M, int m) { if (std::numeric_limits<Coefficient>::is_bounded) { - if (std::numeric_limits<Coefficient>::min() - > std::numeric_limits<ANALYZER_FP_FORMAT>::min() - || std::numeric_limits<Coefficient>::max() - < std::numeric_limits<ANALYZER_FP_FORMAT>::min()) { + if (greater_than(std::numeric_limits<Coefficient>::min(), + std::numeric_limits<ANALYZER_FP_FORMAT>::min()) + || less_than(std::numeric_limits<Coefficient>::max(), + std::numeric_limits<ANALYZER_FP_FORMAT>::min())) { // This may still provoke an arithmetic overflow exception: // no problem. - M = m; + assign_r(M, m, ROUND_DOWN); return; } } - M = std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + assign_r(M, std::numeric_limits<ANALYZER_FP_FORMAT>::max(), ROUND_DOWN); } // Tests rate limiter using boxes and ignoring rounding errors.

1 0

[GIT] ppl/ppl(master): Merge branch 'master' into floating_point
by Roberto Bagnara 28 Dec '09

28 Dec '09

Module: ppl/ppl Branch: master Commit: f62e48e207097b1ca5b7d2542c968f500d850a81 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f62e48e20709… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Dec 28 20:27:49 2009 +0100 Merge branch 'master' into floating_point ---

1 0

[GIT] ppl/ppl(master): Improved Multiplication_Floating_Point_Expression:: linearize.
by Roberto Amadini 28 Dec '09

28 Dec '09

Module: ppl/ppl Branch: master Commit: 7bfd19aec5b224dab0d853f4904f5118e8c77fde URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7bfd19aec5b2… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Dec 28 14:21:22 2009 +0100 Improved Multiplication_Floating_Point_Expression::linearize. --- ...lication_Floating_Point_Expression.templates.hh | 33 ++++++++++++++------ 1 files changed, 23 insertions(+), 10 deletions(-) diff --git a/src/Multiplication_Floating_Point_Expression.templates.hh b/src/Multiplication_Floating_Point_Expression.templates.hh index fdda55e..f1fc29f 100644 --- a/src/Multiplication_Floating_Point_Expression.templates.hh +++ b/src/Multiplication_Floating_Point_Expression.templates.hh @@ -55,19 +55,32 @@ void Multiplication_Floating_Point_Expression<FP_Interval_Type, FP_Format> boundary_type first_interval_size, second_interval_size; // FIXME: we are not sure that what we do here is policy-proof. - if (intervalized_first_operand.is_bounded() - && intervalized_second_operand.is_bounded()) { - first_interval_size = intervalized_first_operand.upper() - - intervalized_first_operand.lower(); - second_interval_size = intervalized_second_operand.upper() - - intervalized_second_operand.lower(); - if (first_interval_size <= second_interval_size) + if (intervalized_first_operand.is_bounded()) { + if (intervalized_second_operand.is_bounded()) { + first_interval_size = intervalized_first_operand.upper() - + intervalized_first_operand.lower(); + second_interval_size = intervalized_second_operand.upper() - + intervalized_second_operand.lower(); + if (first_interval_size <= second_interval_size) + intervalize_first = true; + else + intervalize_first = false; + } + else { + if (this->overflows(linearized_second_operand)) + throw Linearization_Failed(); intervalize_first = true; - else + } + } + else { + if (intervalized_second_operand.is_bounded()) { + if (this->overflows(linearized_first_operand)) + throw Linearization_Failed(); intervalize_first = false; + } + else + throw Linearization_Failed(); } - else - throw Linearization_Failed(); // Here we do the actual computation. // For optimizing, we store the relative error directly into result.

1 0

[GIT] ppl/ppl(master): Implemented Box<ITV>:: affine_image on Interval Linear Forms.
by Roberto Amadini 28 Dec '09

28 Dec '09

Module: ppl/ppl Branch: master Commit: 9b8c9752949ee6b96518f7009a290b64c86b35cc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9b8c9752949e… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Sat Dec 26 18:20:50 2009 +0100 Implemented Box<ITV>::affine_image on Interval Linear Forms. Tests in tests/Floating_Point_Expression actually use only IEEE754 floating point format. --- src/Box.defs.hh | 30 ++++++ src/Box.templates.hh | 47 ++++++++++ src/Octagonal_Shape.templates.hh | 2 +- tests/Floating_Point_Expression/Makefile.am | 7 +- tests/Floating_Point_Expression/digitalfilters1.cc | 98 +++++++------------- .../floatingpointexpr1.cc | 2 +- 6 files changed, 115 insertions(+), 71 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=9b8c9752…

1 0

[GIT] ppl/ppl(floating_point): New commits
by Roberto Bagnara 28 Dec '09

28 Dec '09

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f62e48e20709… Merge: 7bfd19aec5b224dab0d853f4904f5118e8c77fde e86e2471429982e8141789e4adeb6ddd0cc1e326 Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Dec 28 20:27:49 2009 +0100 Merge branch 'master' into floating_point URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e86e24714299… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Dec 28 20:26:04 2009 +0100 Fixed several bugs. These consisted in using *_r() checked-number functions without actually checking the result. Factorized the code to set the M parameter. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e8fa0e1fbc06… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Dec 22 19:25:39 2009 +0100 Version number bumped. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9e4dbdd8255a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Dec 22 19:20:54 2009 +0100 Updated. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2cda93e86a8b… Merge: 1242e420c15da5fa9f671f4d93227ced7272f035 4e2145f8d498bc3ea055a06a1244de677b7bbab5 Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Dec 22 09:33:21 2009 +0100 Merge branch 'floating_point' URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1242e420c15d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Dec 21 18:28:30 2009 +0100 Never leave operators at end of line.

1 0

[GIT] ppl/ppl(master): Fixed several bugs.
by Roberto Bagnara 28 Dec '09

28 Dec '09

Module: ppl/ppl Branch: master Commit: e86e2471429982e8141789e4adeb6ddd0cc1e326 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e86e24714299… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Dec 28 20:26:04 2009 +0100 Fixed several bugs. These consisted in using *_r() checked-number functions without actually checking the result. Factorized the code to set the M parameter. --- tests/Floating_Point_Expression/digitalfilters1.cc | 81 +++++++++---------- 1 files changed, 38 insertions(+), 43 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index ffd5c11..f356ca8 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -46,6 +46,22 @@ for (n = 0; n < N; ++n) { } */ +void +set_M(Coefficient& M, int m) { + if (std::numeric_limits<Coefficient>::is_bounded) { + if (std::numeric_limits<Coefficient>::min() + > std::numeric_limits<ANALYZER_FP_FORMAT>::min() + || std::numeric_limits<Coefficient>::max() + < std::numeric_limits<ANALYZER_FP_FORMAT>::min()) { + // This may still provoke an arithmetic overflow exception: + // no problem. + M = m; + return; + } + } + M = std::numeric_limits<ANALYZER_FP_FORMAT>::max(); +} + // Tests rate limiter using boxes and ignoring rounding errors. bool test01() { @@ -67,11 +83,8 @@ test01() { FP_Interval_Abstract_Store as_begin; Constraint_System cs; - PPL_DIRTY_TEMP_COEFFICIENT(M); - - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - assign_r(M, max_analyzer, ROUND_DOWN); + Coefficient M; + set_M(M, 144); cs.insert(Y <= M); cs.insert(Y >= -M); @@ -160,10 +173,8 @@ test02() { FP_BD_Shape bd_begin; Constraint_System cs; - PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - assign_r(M, max_analyzer, ROUND_DOWN); + Coefficient M; + set_M(M, 144); cs.insert(Y <= M); cs.insert(Y >= -M); @@ -250,12 +261,10 @@ test03() { FP_Octagonal_Shape oc_begin; Constraint_System cs; - PPL_DIRTY_TEMP_COEFFICIENT(M); - PPL_DIRTY_TEMP_COEFFICIENT(N); - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - assign_r(M, max_analyzer, ROUND_DOWN); - div_2exp_assign_r(N, M, 1, ROUND_DOWN); + Coefficient M; + Coefficient N; + set_M(M, 272); + div_2exp_assign(N, M, 1); // FIXME: By inserting the constraints Y <= M and Y >= -M, we obtain // Y + Y <= 2 * M = +inf and -Y - Y <= -2 * M = +inf. // For a more precise analysis, it is better to insert the @@ -344,11 +353,9 @@ test04() { NNC_Polyhedron ph_begin; Constraint_System cs; - PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - assign_r(M, max_analyzer, ROUND_DOWN); - // FIXME: we could take any value of M >= 128. + Coefficient M; + // Note: we can take any value of M >= 128 here. + set_M(M, 128); cs.insert(Y <= M); cs.insert(Y >= -M); @@ -447,13 +454,9 @@ test05() { FP_Linear_Form lr; FP_Linear_Form lk; - PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - assign_r(M, max_analyzer, ROUND_DOWN); - // We have to check that Y not overflows. - // FIXME: We could take any value of M >= 144. Constraint_System cs; + Coefficient M; + set_M(M, 144); cs.insert(Y <= M); cs.insert(Y >= -M); @@ -626,20 +629,16 @@ test06() { FP_Linear_Form lr; FP_Linear_Form lk; - PPL_DIRTY_TEMP_COEFFICIENT(M); - PPL_DIRTY_TEMP_COEFFICIENT(N); - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - assign_r(M, max_analyzer, ROUND_DOWN); - + Constraint_System cs; + Coefficient M; + Coefficient N; + set_M(M, 288); + div_2exp_assign(N, M, 1); // FIXME: By inserting the constraints Y <= M and Y >= -M, we obtain // Y + Y <= 2 * M = +inf and -Y - Y <= -2 * M = +inf. // For a more precise analysis, it is better to insert the // constraints Y <= N and Y >= -N, where N = M / 2. // However, we could take any value of N such that 144 <= N <= M / 2. - div_2exp_assign_r(N, M, 1, ROUND_DOWN); - // We have to check that Y not overflows. - Constraint_System cs; cs.insert(Y <= N); cs.insert(Y >= -N); @@ -812,13 +811,9 @@ test07() { FP_Linear_Form lr; FP_Linear_Form lk; - PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - assign_r(M, max_analyzer, ROUND_DOWN); - // We have to check that Y not overflows. - // FIXME: We could take any value of M >= 144. Constraint_System cs; + Coefficient M; + set_M(M, 144); cs.insert(Y <= M); cs.insert(Y >= -M); @@ -964,8 +959,8 @@ test07() { } // namespace BEGIN_MAIN - DO_TEST(test01); - DO_TEST(test02); + DO_TEST_F8(test01); + DO_TEST_F8(test02); DO_TEST_F8(test03); DO_TEST_F64(test04); DO_TEST_F8(test05);

1 0

[GIT] ppl/ppl(floating_point): Improved Multiplication_Floating_Point_Expression::linearize.
by Roberto Amadini 28 Dec '09

28 Dec '09

Module: ppl/ppl Branch: floating_point Commit: 7bfd19aec5b224dab0d853f4904f5118e8c77fde URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7bfd19aec5b2… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Dec 28 14:21:22 2009 +0100 Improved Multiplication_Floating_Point_Expression::linearize. --- ...lication_Floating_Point_Expression.templates.hh | 33 ++++++++++++++------ 1 files changed, 23 insertions(+), 10 deletions(-) diff --git a/src/Multiplication_Floating_Point_Expression.templates.hh b/src/Multiplication_Floating_Point_Expression.templates.hh index fdda55e..f1fc29f 100644 --- a/src/Multiplication_Floating_Point_Expression.templates.hh +++ b/src/Multiplication_Floating_Point_Expression.templates.hh @@ -55,19 +55,32 @@ void Multiplication_Floating_Point_Expression<FP_Interval_Type, FP_Format> boundary_type first_interval_size, second_interval_size; // FIXME: we are not sure that what we do here is policy-proof. - if (intervalized_first_operand.is_bounded() - && intervalized_second_operand.is_bounded()) { - first_interval_size = intervalized_first_operand.upper() - - intervalized_first_operand.lower(); - second_interval_size = intervalized_second_operand.upper() - - intervalized_second_operand.lower(); - if (first_interval_size <= second_interval_size) + if (intervalized_first_operand.is_bounded()) { + if (intervalized_second_operand.is_bounded()) { + first_interval_size = intervalized_first_operand.upper() - + intervalized_first_operand.lower(); + second_interval_size = intervalized_second_operand.upper() - + intervalized_second_operand.lower(); + if (first_interval_size <= second_interval_size) + intervalize_first = true; + else + intervalize_first = false; + } + else { + if (this->overflows(linearized_second_operand)) + throw Linearization_Failed(); intervalize_first = true; - else + } + } + else { + if (intervalized_second_operand.is_bounded()) { + if (this->overflows(linearized_first_operand)) + throw Linearization_Failed(); intervalize_first = false; + } + else + throw Linearization_Failed(); } - else - throw Linearization_Failed(); // Here we do the actual computation. // For optimizing, we store the relative error directly into result.

1 0