Module: ppl/ppl Branch: floating_point Commit: 0ca73838e132e6f1f80de75ece6312aba89fa878 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0ca73838e132e...
Author: Roberto Amadini r.amadini@virgilio.it Date: Thu Oct 1 18:17:27 2009 +0200
Fixed bug in BD_Shape<T>::two_variables_affine_image. Added a first implementation of test02.
---
src/BD_Shape.templates.hh | 33 ++++++----- tests/Floating_Point_Expression/digitalfilters1.cc | 59 +++++++++++++++++++- 2 files changed, 76 insertions(+), 16 deletions(-)
diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index a1f5694..47e74af 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4237,10 +4237,13 @@ void BD_Shape<T> const Linear_Form< Interval<T, Interval_Info> >& lf, const dimension_type& space_dim) {
- // Shortest-path closure is preserved, but not reduction. + // Remove all constraints on 'var'. + forget_all_dbm_constraints(var_id); + // Shortest-path closure is maintained, but not reduction. if (marked_shortest_path_reduced()) reset_shortest_path_reduced();
+ reset_shortest_path_closed();
Linear_Form< Interval<T, Interval_Info> > minus_lf(lf); minus_lf.negate(); @@ -4332,9 +4335,9 @@ void BD_Shape<T>::refine_with_linear_form_inequality( right_w_id = i; }
- const FP_Interval_Type& left_w_coeff = + const FP_Interval_Type& left_w_coeff = left.coefficient(Variable(left_w_id)); - const FP_Interval_Type& right_w_coeff = + const FP_Interval_Type& right_w_coeff = right.coefficient(Variable(right_w_id));
// FIXME: there is plenty of duplicate code in the following lines. We could @@ -4378,7 +4381,7 @@ BD_Shape<T>::left_inhomogeneous_refine(const dimension_type& right_t, const Linear_Form< Interval<T, Interval_Info> >& right) {
typedef Interval<T, Interval_Info> FP_Interval_Type; - + if (right_t == 1) { // The constraint has the form [a-;a+] <= [b-;b+] + [c-;c+] * x. // Reduce it to the constraint +/-x <= b+ - a- if [c-;c+] = +/-[1;1]. @@ -4418,7 +4421,7 @@ BD_Shape<T> const Linear_Form< Interval<T, Interval_Info> >& right) {
typedef Interval<T, Interval_Info> FP_Interval_Type; - + if (right_t == 0) { // The constraint has the form [b-;b+] + [c-;c+] * x <= [a-;a+] // Reduce it to the constraint +/-x <= a+ - b- if [c-;c+] = +/-[1;1]. @@ -4445,7 +4448,7 @@ BD_Shape<T> return; } } // fi right_t == 0 - + if(right_t == 1) { // The constraint has the form: // [a-;a+] + [b-;b+] * x <= [c-;c+] + [d-;d+] * y. @@ -4475,8 +4478,8 @@ BD_Shape<T> const FP_Interval_Type& right_a = right.inhomogeneous_term(); sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), ROUND_UP); - div_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, - ROUND_UP); + div_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, + ROUND_UP); add_dbm_constraint(0, left_w_id+1, a_plus_minus_b_minus); return; } @@ -4488,14 +4491,14 @@ BD_Shape<T> const FP_Interval_Type& right_a = right.inhomogeneous_term(); sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), ROUND_UP); - div_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, + div_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, ROUND_UP); add_dbm_constraint(right_w_id+1, 0, a_plus_minus_b_minus); return; } } else if (is_left_coeff_minus_one && is_right_coeff_one) { - // if right and left coefficents are negative the constraint + // if right and left coefficents are negative the constraint // - x - y <= b // is ignored;
@@ -4511,7 +4514,7 @@ BD_Shape<T> // where k is an overaproximation of b - y return; } - if (is_left_coeff_one && is_right_coeff_one) { + if (is_left_coeff_one && is_right_coeff_one) { PPL_DIRTY_TEMP(N, c_plus_minus_a_minus); const FP_Interval_Type& left_a = left.inhomogeneous_term(); const FP_Interval_Type& right_c = right.inhomogeneous_term(); @@ -4550,9 +4553,9 @@ BD_Shape<T> PPL_DIRTY_TEMP(N, low_coeff); PPL_DIRTY_TEMP(N, high_coeff); PPL_DIRTY_TEMP(N, upper_bound); - + dimension_type max_w_id = std::max(left_w_id, right_w_id); - + for (dimension_type first_v = 0; first_v < max_w_id; ++first_v) { for (dimension_type second_v = first_v+1; second_v <= max_w_id; ++second_v) { @@ -4597,7 +4600,7 @@ BD_Shape<T> } } } - + if (do_update) { Variable first(first_v); Variable second(second_v); @@ -4642,7 +4645,7 @@ BD_Shape<T> add_dbm_constraint(n_var, 0, upper_bound); } } - + }
template <typename T> diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc index 9405d22..4f444cd 100644 --- a/tests/Floating_Point_Expression/digitalfilters1.cc +++ b/tests/Floating_Point_Expression/digitalfilters1.cc @@ -108,8 +108,65 @@ test01() { // tests rate limiter using bounded differences abstract domain. bool test02() { + Variable X(0); //input + Variable D(1); //input + Variable Y(2); //output + Variable S(3); //last output + Variable R(4); //actual rate + FP_Interval_Abstract_Store abstract_store(5); + FP_BD_Shape bd(abstract_store); + FP_Interval tmp(0); + FP_BD_Shape bd_begin; + + // Y = 0; + bd.affine_image(Y, FP_Linear_Form(tmp)); + + for(unsigned int n = 0; bd_begin != bd; ++n) { + + nout << "*** n = " << n << " ***" << endl; + bd_begin = bd; + + //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X; + tmp.lower() = -128; + tmp.upper() = 128; + bd.affine_image(X, FP_Linear_Form(tmp)); + tmp.lower() = 0; + tmp.upper() = 16; + bd.affine_image(D, FP_Linear_Form(tmp)); + bd.affine_image(S, FP_Linear_Form(Y)); + bd.affine_image(R, FP_Linear_Form(X - S)); + bd.affine_image(Y, FP_Linear_Form(X)); + + //if (R <= -D) Y = S - D; + FP_BD_Shape bd_then(bd); + bd_then.refine_with_linear_form_inequality(FP_Linear_Form(R), + -FP_Linear_Form(D)); + bd_then.affine_image(Y, FP_Linear_Form(S - D)); + + bd.refine_with_linear_form_inequality(-FP_Linear_Form(D), + FP_Linear_Form(R)); + bd.upper_bound_assign(bd_then); + print_constraints(Box<FP_Interval>(bd) , + "*** if (R <= -D) Y = S - D; ***"); + + //if (R >= D) Y = S + D; + bd_then = bd; + bd_then.refine_with_linear_form_inequality(FP_Linear_Form(D), + FP_Linear_Form(R)); + bd_then.affine_image(Y, FP_Linear_Form(S + D));
- return true; + bd.refine_with_linear_form_inequality(FP_Linear_Form(R), + FP_Linear_Form(D)); + + bd.upper_bound_assign(bd_then); + print_constraints(Box<FP_Interval>(bd) , + "*** if (R >= D) Y = S + D; ***"); + } + + bd.refine_fp_interval_abstract_store(abstract_store); + tmp = abstract_store.get_interval(Y); + nout << "*** Y in " << tmp << " ***" << endl; + return tmp.is_bounded(); }
// tests rate limiter using octagons abstract domain.