Module: ppl/ppl Branch: master Commit: c3d6b3d44df422a2683d7b2abd313d670123910b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c3d6b3d44df42... Author: Patricia Hill <p.m.hill@leeds.ac.uk> Date: Mon May 11 21:32:32 2009 +0100 Improved code for wrap_assign() for grids for constant values. If the value for a variable is already constant, and the constant is outside the range for the bounded integr type, then the outcome depends on the kind of overflow: - if `impossible', then the grid is set empty; - if `undefined', then the variable is set to take any integral value; - if `wraps', then the value is wrapped by the wrap_frequency to a value in the range for the bounded integer type. Comments improved. --- src/Grid.defs.hh | 6 ++-- src/Grid_public.cc | 79 ++++++++++++++++++++++++++++++++++++++++++++------ tests/Grid/wrap1.cc | 77 ++++++++++++++++++++++++++++++++++++++++++++++++- 3 files changed, 147 insertions(+), 15 deletions(-) diff --git a/src/Grid.defs.hh b/src/Grid.defs.hh index bfb6d12..b8b37ee 100644 --- a/src/Grid.defs.hh +++ b/src/Grid.defs.hh @@ -2135,14 +2135,14 @@ private: /*! \brief Returns <CODE>true</CODE> if and only if \p *this is not empty and - \p expr can takes discrete values in \p *this, in which case the maximum - frequency and minimal value for \p expr in \p *this is computed. + \p expr is discrete in \p *this, in which case the maximum frequency + and the value for \p expr that is closest to zero are computed. \param expr The linear expression for which the frequency is needed; \param freq_n - The numerator of the maximum frequency; + The numerator of the maximum frequency of \p expr; \param freq_d The denominator of the maximum frequency of \p expr; diff --git a/src/Grid_public.cc b/src/Grid_public.cc index be66a1a..1e181b2 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -2675,11 +2675,26 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, // This is independent of the signedness `s'. PPL_DIRTY_TEMP_COEFFICIENT(wrap_frequency); mul_2exp_assign(wrap_frequency, Coefficient_one(), w); + // Set `min_value' and `max_value' to the minimum and maximum values + // a variable of width `w' and signedness `s' can take. + PPL_DIRTY_TEMP_COEFFICIENT(min_value); + PPL_DIRTY_TEMP_COEFFICIENT(max_value); + if (s == UNSIGNED) { + min_value = 0; + mul_2exp_assign(max_value, Coefficient_one(), w); + --max_value; + } + else { + assert(s == SIGNED_2_COMPLEMENT); + mul_2exp_assign(max_value, Coefficient_one(), w-1); + neg_assign(min_value, max_value); + --max_value; + } // Generators are up-to-date and minimized. const Grid gr = *this; - // Overflow is impossible. So check if value might be constant. + // Overflow is impossible. So check if value might become constant. if (o == OVERFLOW_IMPOSSIBLE) { PPL_DIRTY_TEMP_COEFFICIENT(f_n); PPL_DIRTY_TEMP_COEFFICIENT(f_d); @@ -2688,13 +2703,23 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, for (Variables_Set::const_iterator i = vars.begin(), vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); - // If the grid frequency for `x' in `vars' is more than half the wrap - // frequency, then `x' can only take a unique (ie constant) value. + // If the grid frequency for `x' in `vars' is more than half the + // `wrap_frequency', then `x' can only take a unique (ie constant) + // value. if (!gr.frequency_no_check(x, f_n, f_d, v_n, v_d)) continue; + if (f_n == 0) { + // `x' is a constant in `gr'. + if ((v_n > max_value * v_d) || (v_n < min_value * v_d)) { + // If the value is outside the range of the bounded integer type, + // then `x' has no possible value and hence `gr' is set empty. + set_empty(); + return; + } + } if (2*f_n > f_d * wrap_frequency) { if (s == UNSIGNED) { - // `v_n' is the value closest to 0 and may be negatve. + // `v_n' is the value closest to 0 and may be negative. if (v_n < 0) { v_n *= f_d; add_mul_assign(v_n, f_n, v_d); @@ -2711,18 +2736,32 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, return; } // If overflow is undefined, then all we know is that the variable - // can take any integer between the wrap bounds. + // may take any integer within the range of the bounded integer type. if (o == OVERFLOW_UNDEFINED) { for (Variables_Set::const_iterator i = vars.begin(), vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); - // If `x' is a constant, do nothing. if (!gr.bounds_no_check(x)) { + // `x' is not a constant in `gr'. if (gr.constrains(x)) - // We know that `x' is not a constant, - // so `x' may wrap to any integral value. + // We know that `x' is not a constant, so `x' may wrap to any + // integral value. add_grid_generator(parameter(x)); } + else { + // `x' is a constant in `gr'. + PPL_DIRTY_TEMP_COEFFICIENT(coeff_x); + PPL_DIRTY_TEMP_COEFFICIENT(div_x); + coeff_x = gen_sys[0].coefficient(x); + div_x = gen_sys[0].divisor(); + // If the value of `x' is not within the range for the bounded + // integer type, then `x' can take any integral value; + // otherwise `x' is unchanged. + if (coeff_x > max_value * div_x || coeff_x < min_value * div_x) { + unconstrain(x); + add_congruence(x %= 0); + } + } } return; } @@ -2733,13 +2772,33 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, for (Variables_Set::const_iterator i = vars.begin(), vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); - // If `x' is a constant, do nothing. if (!gr.bounds_no_check(x)) { + // `x' is not a constant in `gr'. if (gr.constrains(x)) - // We know that `x' is not a constant, so `x' may wrap. + // We know that `x' is not a constant, so `x' may wrap + // to a value modulo the `wrap_frequency'. add_grid_generator(parameter(wrap_frequency * x)); } + else { + // `x' is a constant in `gr'. + PPL_DIRTY_TEMP_COEFFICIENT(coeff_x); + PPL_DIRTY_TEMP_COEFFICIENT(f_x); + coeff_x = gen_sys[0].coefficient(x); + f_x = gen_sys[0].divisor(); + // If the value of `x' is not within the range for the bounded + // integer type, then `x' will wrap modulo the `wrap_frequency'; + // otherwise `x' is unchanged. + if (coeff_x > max_value * f_x || coeff_x < min_value * f_x) { + f_x *= wrap_frequency; + coeff_x %= f_x; + if (s == UNSIGNED && coeff_x < 0) + coeff_x += f_x; + unconstrain(x); + add_constraint(x == coeff_x); + } + } } + return; } /*! \relates Parma_Polyhedra_Library::Grid */ diff --git a/tests/Grid/wrap1.cc b/tests/Grid/wrap1.cc index bc78243..235ba02 100644 --- a/tests/Grid/wrap1.cc +++ b/tests/Grid/wrap1.cc @@ -200,7 +200,7 @@ test07() { return ok; } -// Expression of a greater space dimension than the grid. +// Expression with a greater space dimension than the grid. bool test08() { Variable x(0); @@ -226,7 +226,7 @@ test08() { return false; } -// Expression of a greater space dimension than the grid. +// Constraint with a greater space dimension than the grid. bool test09() { Variable x(0); @@ -283,6 +283,76 @@ test10() { return ok; } +bool +test11() { + Variable x(0); + Variable y(1); + Grid gr(2); + gr.add_congruence((x %= 256) / 0); + gr.add_congruence(y %= 0); + + Variables_Set vars(x); + + gr.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED); + + Grid known_result(2); + known_result.add_congruence((x %= 0) / 1); + known_result.add_congruence(y %= 0); + + bool ok = (gr == known_result); + + print_congruences(gr, "*** gr.wrap_assign(...) ***"); + + return ok; +} + +bool +test12() { + Variable x(0); + Variable y(1); + Grid gr(2); + gr.add_congruence((x %= 256) / 0); + gr.add_congruence(y %= 0); + + Variables_Set vars(x); + + gr.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + + Grid known_result(2); + known_result.add_congruence((x %= 0) / 0); + known_result.add_congruence(y %= 0); + + bool ok = (gr == known_result); + + print_congruences(gr, "*** gr.wrap_assign(...) ***"); + + return ok; +} + +bool +test13() { + Variable x(0); + Variable y(1); + Grid gr(2); + gr.add_congruence((x %= 25) / 0); + gr.add_congruence(y %= 0); + + Variables_Set vars(x); + + gr.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED); + + Grid known_result(2); + known_result.add_congruence((x %= 25) / 0); + known_result.add_congruence(y %= 0); + + bool ok = (gr == known_result); + + print_congruences(gr, "*** gr.wrap_assign(...) ***"); + + return ok; +} + + } // namespace BEGIN_MAIN @@ -296,4 +366,7 @@ BEGIN_MAIN DO_TEST(test08); DO_TEST(test09); DO_TEST_F8(test10); + DO_TEST_F8(test11); + DO_TEST_F8(test12); + DO_TEST_F8(test13); END_MAIN