[GIT] ppl/ppl(floating_point): Improved test01, ..., test04.
Module: ppl/ppl Branch: floating_point Commit: a75d238a6bafe710454001b182151566a87e6e10 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a75d238a6bafe... Author: Roberto Amadini <r.amadini@virgilio.it> Date: Fri Dec 11 14:26:56 2009 +0100 Improved test01, ..., test04. --- tests/Floating_Point_Expression/digitalfilters1.cc | 130 +++++++++++--------- 1 files changed, 69 insertions(+), 61 deletions(-) diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index fb841f2..e5f4fa7 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -66,6 +66,20 @@ test01() { FP_Interval y_begin(1); FP_Interval_Abstract_Store as_begin; + Constraint_System cs; + PPL_DIRTY_TEMP_COEFFICIENT(M); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); + cs.insert(Y <= M); + cs.insert(Y >= -M); + // Y = 0; abstract_store.set_interval(Y, y); Box<FP_Interval> box(abstract_store); @@ -111,19 +125,7 @@ test01() { "*** after if (R >= D) Y = S + D; ***"); abstract_store.upper_bound_assign(as_begin); - Constraint_System cs; - PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZER_FP_FORMAT max_analyzed = - (2 - pow(2, - -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) - * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) - - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - max_analyzer = std::min(max_analyzer, max_analyzed); - assign_r(M, max_analyzer, ROUND_DOWN); - cs.insert(Y <= M); - cs.insert(Y >= -M); + abstract_store.limited_CC76_extrapolation_assign(as_begin, cs); box = Box<FP_Interval>(abstract_store); print_constraints(box, "*** end loop ***"); @@ -155,6 +157,20 @@ test02() { FP_Interval y(0); FP_BD_Shape bd_begin; + Constraint_System cs; + PPL_DIRTY_TEMP_COEFFICIENT(M); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); + cs.insert(Y <= M); + cs.insert(Y >= -M); + // Y = 0; bd.affine_image(Y, FP_Linear_Form(y)); Box<FP_Interval> box(bd); @@ -205,19 +221,7 @@ test02() { "*** after if (R >= D) Y = S + D; ***"); bd.upper_bound_assign(bd_begin); - Constraint_System cs; - PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZER_FP_FORMAT max_analyzed = - (2 - pow(2, - -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) - * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) - - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - max_analyzer = std::min(max_analyzer, max_analyzed); - assign_r(M, max_analyzer, ROUND_DOWN); - cs.insert(Y <= M); - cs.insert(Y >= -M); + bd.limited_BHMZ05_extrapolation_assign(bd_begin, cs); box = Box<FP_Interval>(bd); print_constraints(box, "*** end loop ***"); @@ -249,6 +253,27 @@ test03() { FP_Interval y_begin(1); FP_Octagonal_Shape oc_begin; + Constraint_System cs; + PPL_DIRTY_TEMP_COEFFICIENT(M); + PPL_DIRTY_TEMP_COEFFICIENT(N); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); + div_2exp_assign_r(N, M, 1, ROUND_DOWN); + // 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 >= 136. + cs.insert(Y <= N); + cs.insert(Y >= -N); + // Y = 0; oc.affine_image(Y, FP_Linear_Form(y)); Box<FP_Interval> box(oc); @@ -297,26 +322,7 @@ test03() { "*** after (R >= D) Y = S + D; ***"); oc.upper_bound_assign(oc_begin); - Constraint_System cs; - PPL_DIRTY_TEMP_COEFFICIENT(M); - PPL_DIRTY_TEMP_COEFFICIENT(N); - ANALYZER_FP_FORMAT max_analyzed = - (2 - pow(2, - -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) - * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) - - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - max_analyzer = std::min(max_analyzer, max_analyzed); - assign_r(M, max_analyzer, ROUND_DOWN); - div_2exp_assign_r(N, M, 1, ROUND_DOWN); - // 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 >= 136. - cs.insert(Y <= N); - cs.insert(Y >= -N); + oc.limited_BHMZ05_extrapolation_assign(oc_begin, cs); box = Box<FP_Interval>(oc); print_constraints(box, "*** end loop ***"); @@ -348,6 +354,21 @@ test04() { FP_Interval y_begin(1); NNC_Polyhedron ph_begin; + Constraint_System cs; + PPL_DIRTY_TEMP_COEFFICIENT(M); + ANALYZER_FP_FORMAT max_analyzed = + (2 - pow(2, + -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) + * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) + - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); + ANALYZER_FP_FORMAT max_analyzer = + std::numeric_limits<ANALYZER_FP_FORMAT>::max(); + max_analyzer = std::min(max_analyzer, max_analyzed); + assign_r(M, max_analyzer, ROUND_DOWN); + // FIXME: we could take any value of M >= 128. + cs.insert(Y <= M); + cs.insert(Y >= -M); + // Y = 0; ph.affine_image(Y, FP_Linear_Form(y)); Box<FP_Interval> box(ph); @@ -402,20 +423,7 @@ test04() { "*** after if (R >= D) Y = S + D; ***"); ph.upper_bound_assign(ph_begin); - Constraint_System cs; - PPL_DIRTY_TEMP_COEFFICIENT(M); - ANALYZER_FP_FORMAT max_analyzed = - (2 - pow(2, - -static_cast<ANALYZER_FP_FORMAT>(ANALYZED_FP_FORMAT::MANTISSA_BITS))) - * pow(2, pow(2, ANALYZED_FP_FORMAT::EXPONENT_BITS) - - (ANALYZED_FP_FORMAT::EXPONENT_BIAS) - 2); - ANALYZER_FP_FORMAT max_analyzer = - std::numeric_limits<ANALYZER_FP_FORMAT>::max(); - max_analyzer = std::min(max_analyzer, max_analyzed); - assign_r(M, max_analyzer, ROUND_DOWN); - // FIXME: we could take any value of M >= 128. - cs.insert(Y <= M); - cs.insert(Y >= -M); + ph.limited_BHRZ03_extrapolation_assign(ph_begin, cs); box = Box<FP_Interval>(ph); print_constraints(box, "*** end loop ***"); @@ -601,7 +609,7 @@ test05() { bd.limited_BHMZ05_extrapolation_assign(bd_begin, cs); abstract_store.limited_CC76_extrapolation_assign(as_begin, cs); - print_constraints(abstract_store,"*** end loop ***"); + print_constraints(abstract_store, "*** end loop ***"); y = abstract_store.get_interval(Y); }
participants (1)
-
Roberto Amadini