[PPL-devel] [GIT] ppl/ppl(floating_point): Fixed bug in BD_Shape<T>:: two_variables_affine_image.
Roberto Amadini
r.amadini at virgilio.it
Thu Oct 1 18:18:43 CEST 2009
Module: ppl/ppl
Branch: floating_point
Commit: 0ca73838e132e6f1f80de75ece6312aba89fa878
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0ca73838e132e6f1f80de75ece6312aba89fa878
Author: Roberto Amadini <r.amadini at 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.
More information about the PPL-devel
mailing list