- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(bounded_arithmetic): Added into the function of the bitwise operators shift,
by Alberto Gioia 14 Sep '11

14 Sep '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: c1d77c82dcad2f0652be3b072e93a9e6e5a90f6d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c1d77c82dcad… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Wed Sep 14 12:53:57 2011 +0200 Added into the function of the bitwise operators shift, another check on the second operand. --- src/Linear_Form.templates.hh | 6 ++++++ 1 files changed, 6 insertions(+), 0 deletions(-) diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index 928ec11..15fd3b3 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -431,6 +431,7 @@ template <typename C> Linear_Form<C>& operator<<(Linear_Form<C>& f, const C& n) { C zero(0); + C one(1); dimension_type f_size = f.size(); @@ -438,6 +439,8 @@ operator<<(Linear_Form<C>& f, const C& n) { f = Linear_Form<C>(zero); return f; } + else if (n == one) + return f; else if (f >= zero || f < zero) { for (dimension_type i = f_size; i-- > 0; ) f[i] << n; @@ -453,6 +456,7 @@ template <typename C> Linear_Form<C>& operator>>(Linear_Form<C>& f, const C& n) { C zero(0); + C one(1); dimension_type f_size = f.size(); @@ -460,6 +464,8 @@ operator>>(Linear_Form<C>& f, const C& n) { f = Linear_Form<C>(zero); return f; } + if (n == one) + return f; else if (f >= zero || f < zero) { for (dimension_type i = f_size; i-- > 0; ) f[i] >> n;

1 0

[GIT] ppl/ppl(bounded_arithmetic): Changed order of linearization functions for bitwise operators,
by Alberto Gioia 14 Sep '11

14 Sep '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: c84524e70682abb2c80936b4d9c5b0283eeeea46 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c84524e70682… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Wed Sep 14 12:38:57 2011 +0200 Changed order of linearization functions for bitwise operators, moved linearization function about bitwise operator AND before the linearization function about bitwise operator OR. --- src/linearize_integer.hh | 308 +++++++++++++++++++++++----------------------- 1 files changed, 154 insertions(+), 154 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=c84524e7…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Corrected definition of approximation for the shift bitwise operators.
by Alberto Gioia 14 Sep '11

14 Sep '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 0bacc94a40b5d713d68911f506cfeb7bc53f1e12 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0bacc94a40b5… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Wed Sep 14 12:32:40 2011 +0200 Corrected definition of approximation for the shift bitwise operators. --- doc/definitions.dox | 16 ++++++++-------- 1 files changed, 8 insertions(+), 8 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index e48e010..52b0e23 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2867,11 +2867,11 @@ The interval bitwise operators are defined as follow: \bigl[\bigl(a / 2^{\left|a'\right|}\bigr, \bigl(b / 2^{\left|b'\right|}\bigr)\bigr], & \text{if $a \geq 0$ and $b' < 0$}; \\ - \bigl[\bigl(a \times 2^{a'}\bigr), - \bigl(b \times 2^{b'}\bigr)\bigr], + \bigl[\bigl(a \times 2^{b'}\bigr), + \bigl(b \times 2^{a'}\bigr)\bigr], & \text{if $b < 0$ and $a' \geq 0$}; \\ - \bigl[\bigl(a / 2^{\left|a'\right|}\bigr), - \bigl(b / 2^{\left|b'\right|}\bigr)\bigr], + \bigl[\bigl(a / 2^{\left|b'\right|}\bigr), + \bigl(b / 2^{\left|a'\right|}\bigr)\bigr], & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} \f] @@ -2879,11 +2879,11 @@ The interval bitwise operators are defined as follow: \f[ [a,b] \ogreaterthan ^{\#} [a',b'] \approx \begin{cases} - \bigl[\bigl(a / 2^{a'}\bigr), - \bigl(b / 2^{b'}\bigr)\bigr], + \bigl[\bigl(a / 2^{b'}\bigr), + \bigl(b / 2^{a'}\bigr)\bigr], & \text{if $a \geq 0$ and $a' \geq 0$}; \\ - \bigl[\bigl(a \times 2^{\left|a'\right|}\bigr), - \bigl(b \times 2^{\left|b'\right|}\bigr)\bigr], + \bigl[\bigl(a \times 2^{\left|b'\right|}\bigr), + \bigl(b \times 2^{\left|a'\right|}\bigr)\bigr], & \text{if $a \geq 0$ and $b' < 0$}; \\ \bigl[\bigl(a / 2^{a'}\bigr), \bigl(b / 2^{b'}\bigr)\bigr],

1 0

[GIT] ppl/ppl(bounded_arithmetic): Changed the management of the intervals not bounded, into the functions of bitwise operator.
by Alberto Gioia 06 Sep '11

06 Sep '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 15cae680af1340ccceecb9135e53ce1a41931354 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=15cae680af13… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Tue Sep 6 19:56:50 2011 +0200 Changed the management of the intervals not bounded, into the functions of bitwise operator. --- src/Interval.inlines.hh | 246 +++++++++++++++++++++++++---------------------- 1 files changed, 129 insertions(+), 117 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=15cae680…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Minor changes.
by Alberto Gioia 06 Sep '11

06 Sep '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 4d23f26eb45bb2f189717092a3fefade56a60b45 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4d23f26eb45b… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Tue Sep 6 18:59:21 2011 +0200 Minor changes. --- src/linearize_integer.hh | 4 ++-- tests/Concrete_Expression/linearize_int.cc | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/linearize_integer.hh b/src/linearize_integer.hh index 2cf8646..53990dc 100644 --- a/src/linearize_integer.hh +++ b/src/linearize_integer.hh @@ -1885,7 +1885,7 @@ linearize_int typedef std::map<dimension_type, Linear_Form> Linear_Form_Abstract_Store; PPL_ASSERT(expr.type().is_bounded_integer()); - switch(expr.kind()){ + switch(expr.kind()) { case Int_Constant<Target>::KIND: { const Int_Constant<Target>* intc_expr = expr.template as<Int_Constant>(); @@ -1896,7 +1896,7 @@ linearize_int return true; } - case Binary_Operator<Target>::KIND:{ + case Binary_Operator<Target>::KIND: { const Binary_Operator<Target>* bop_expr = expr.template as<Binary_Operator>(); switch (bop_expr->binary_operator()) { diff --git a/tests/Concrete_Expression/linearize_int.cc b/tests/Concrete_Expression/linearize_int.cc index 2b0c1ad..c3e52f7 100644 --- a/tests/Concrete_Expression/linearize_int.cc +++ b/tests/Concrete_Expression/linearize_int.cc @@ -1200,7 +1200,7 @@ test09(){ if (!linearize_int(lshift, oracle, Integer_Linear_Form_Abstract_Store(), result_lshift)) { nout << "*** Linearization failed, intervalize second linear form " - << "contain infinity *** " << endl << endl; + << "is not bounded *** " << endl << endl; failed_lshift = true; } @@ -1208,7 +1208,7 @@ test09(){ if (!linearize_int(rshift, oracle, Integer_Linear_Form_Abstract_Store(), result_rshift)) { nout << "*** Linearization failed, intervalize second linear form " - << "contain infinity *** " << endl << endl; + << "is not bounded *** " << endl << endl; failed_rshift = true; } @@ -1353,7 +1353,7 @@ test10(){ if (!linearize_int(lshift, oracle, Integer_Linear_Form_Abstract_Store(), result_lshift)) { nout << "*** Linearization failed, intervalize second linear form " - << "contain infinity *** " << endl << endl; + << "is not bounded *** " << endl << endl; failed_lshift = true; } @@ -1361,7 +1361,7 @@ test10(){ if (!linearize_int(rshift, oracle, Integer_Linear_Form_Abstract_Store(), result_rshift)) { nout << "*** Linearization failed, intervalize second linear form " - << "contain infinity *** " << endl << endl; + << "is not bounded *** " << endl << endl; failed_rshift = true; }

1 0

[GIT] ppl/ppl(bounded_arithmetic): Minor changes to the code.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 20d6899edb2b8be27a6f04e7ddacd37d6b4df964 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=20d6899edb2b… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 18:12:17 2011 +0200 Minor changes to the code. --- tests/Concrete_Expression/linearize_int.cc | 83 ++++++++++++++-------------- 1 files changed, 42 insertions(+), 41 deletions(-) diff --git a/tests/Concrete_Expression/linearize_int.cc b/tests/Concrete_Expression/linearize_int.cc index 6bf18cc..2b0c1ad 100644 --- a/tests/Concrete_Expression/linearize_int.cc +++ b/tests/Concrete_Expression/linearize_int.cc @@ -135,13 +135,6 @@ test01(){ known_result_lshift = known_result_or; known_result_rshift = known_result_or; - linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), result_or); - nout << "*** " << known_result_or << " | " << lf << " ***" << endl - << "*** result_or *** " << endl - << result_or << endl; - known_result_or |= lf; - nout << endl; - linearize_int(band, oracle, Integer_Linear_Form_Abstract_Store(), result_and); nout << "*** " << known_result_and << " & " << lf << " ***" << endl << "*** result_and *** " << endl @@ -149,6 +142,13 @@ test01(){ known_result_and &= lf; nout << endl; + linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), result_or); + nout << "*** " << known_result_or << " | " << lf << " ***" << endl + << "*** result_or *** " << endl + << result_or << endl; + known_result_or |= lf; + nout << endl; + linearize_int(bxor, oracle, Integer_Linear_Form_Abstract_Store(), result_xor); nout << "*** " << known_result_xor << " ^ " << lf << " ***" << endl << "*** result_xor *** " << endl @@ -175,10 +175,10 @@ test01(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -312,9 +312,9 @@ test02(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) + && + (result_or == known_result_or) && (result_xor == known_result_xor) && @@ -457,10 +457,10 @@ test03(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -593,10 +593,10 @@ test04(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -740,10 +740,10 @@ test05(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -832,10 +832,10 @@ test06(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -896,20 +896,23 @@ test07(){ bool failed_or = false; bool failed_xor = false; - if (!linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), - result_or)) { + nout << "*** " << known_result_and << " << " << lf << " ***" << endl; + if (!linearize_int(band, oracle, Integer_Linear_Form_Abstract_Store(), + result_and)) { nout << "*** Linearization failed, the two linear forms have " << "different size *** " << endl << endl; - failed_or = true; + failed_and = true; } - if (!linearize_int(band, oracle, Integer_Linear_Form_Abstract_Store(), - result_and)) { + nout << "*** " << known_result_or << " << " << lf << " ***" << endl; + if (!linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), + result_or)) { nout << "*** Linearization failed, the two linear forms have " << "different size *** " << endl << endl; - failed_and = true; + failed_or = true; } + nout << "*** " << known_result_xor << " << " << lf << " ***" << endl; if (!linearize_int(bxor, oracle, Integer_Linear_Form_Abstract_Store(), result_xor)) { nout << "*** Linearization failed, the two linear forms have " @@ -934,10 +937,10 @@ test07(){ nout << endl; bool ok = - (failed_or) - && (failed_and) && + (failed_or) + && (failed_xor) && (result_lshift == known_result_lshift) @@ -1017,13 +1020,6 @@ test08(){ known_result_lshift = known_result_or; known_result_rshift = known_result_or; - linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), result_or); - nout << "*** " << known_result_or << " | " << lf << " ***" << endl - << "*** result_or *** " << endl - << result_or << endl; - known_result_or |= lf; - nout << endl; - linearize_int(band, oracle, Integer_Linear_Form_Abstract_Store(), result_and); nout << "*** " << known_result_and << " & " << lf << " ***" << endl << "*** result_and *** " << endl @@ -1031,6 +1027,13 @@ test08(){ known_result_and &= lf; nout << endl; + linearize_int(bor, oracle, Integer_Linear_Form_Abstract_Store(), result_or); + nout << "*** " << known_result_or << " | " << lf << " ***" << endl + << "*** result_or *** " << endl + << result_or << endl; + known_result_or |= lf; + nout << endl; + linearize_int(bxor, oracle, Integer_Linear_Form_Abstract_Store(), result_xor); nout << "*** " << known_result_xor << " ^ " << lf << " ***" << endl << "*** result_xor *** " << endl @@ -1058,10 +1061,10 @@ test08(){ nout << endl; bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && (result_lshift == known_result_lshift) @@ -1168,6 +1171,7 @@ test09(){ known_result_xor = known_result_and; known_result_lshift = known_result_and; known_result_rshift = known_result_and; + linearize_int(band, oracle, Integer_Linear_Form_Abstract_Store(), result_and); nout << "*** " << known_result_and << " & " << lf << " ***" << endl << "*** result_and *** " << endl @@ -1189,9 +1193,6 @@ test09(){ known_result_xor ^= lf; nout << endl; - // b1 *= tmp1; - //inh_term1 += b1; - bool failed_lshift = false; bool failed_rshift = false; @@ -1212,10 +1213,10 @@ test09(){ } bool ok = - (result_or == known_result_or) - && (result_and == known_result_and) && + (result_or == known_result_or) + && (result_xor == known_result_xor) && failed_lshift

1 0

[GIT] ppl/ppl(bounded_arithmetic): Added to the bitwise functions, a check for the existence of the infinite.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 91d973104574475fec53561a5d8dfc0e901050b8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=91d973104574… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 18:09:12 2011 +0200 Added to the bitwise functions, a check for the existence of the infinite. --- src/Interval.inlines.hh | 38 ++++++++++++++++++++++++++++++++++++++ 1 files changed, 38 insertions(+), 0 deletions(-) diff --git a/src/Interval.inlines.hh b/src/Interval.inlines.hh index 54d7231..fa70325 100644 --- a/src/Interval.inlines.hh +++ b/src/Interval.inlines.hh @@ -1089,6 +1089,16 @@ Interval<To_Boundary, To_Info>::and_assign(const From1& x, const From2& y) { if (check_empty_arg(x) || check_empty_arg(y)) return assign(EMPTY); + int inf = Parma_Polyhedra_Library::is_infinity(x); + if (inf) { + if (Parma_Polyhedra_Library::is_infinity(y) == -inf) + return assign(NOT_A_NUMBER); + } + else + inf = Parma_Polyhedra_Library::is_infinity(y); + if (inf) + return assign(NOT_A_NUMBER); + Interval<To_Boundary, To_Info> x1; Interval<To_Boundary, To_Info> x2; Interval<To_Boundary, To_Info> zero(0); @@ -1184,6 +1194,16 @@ Interval<To_Boundary, To_Info>::or_assign(const From1& x, const From2& y) { if (check_empty_arg(x) || check_empty_arg(y)) return assign(EMPTY); + int inf = Parma_Polyhedra_Library::is_infinity(x); + if (inf) { + if (Parma_Polyhedra_Library::is_infinity(y) == -inf) + return assign(NOT_A_NUMBER); + } + else + inf = Parma_Polyhedra_Library::is_infinity(y); + if (inf) + return assign(NOT_A_NUMBER); + Interval<To_Boundary, To_Info> x1; Interval<To_Boundary, To_Info> x2; Interval<To_Boundary, To_Info> neg_one(-1); @@ -1280,6 +1300,16 @@ Interval<To_Boundary, To_Info>::xor_assign(const From1& x, const From2& y) { if (check_empty_arg(x) || check_empty_arg(y)) return assign(EMPTY); + int inf = Parma_Polyhedra_Library::is_infinity(x); + if (inf) { + if (Parma_Polyhedra_Library::is_infinity(y) == -inf) + return assign(NOT_A_NUMBER); + } + else + inf = Parma_Polyhedra_Library::is_infinity(y); + if (inf) + return assign(NOT_A_NUMBER); + Interval<To_Boundary, To_Info> x1; Interval<To_Boundary, To_Info> zero(0); Interval<To_Boundary, To_Info> neg_one(-1); @@ -1378,6 +1408,10 @@ Interval<To_Boundary, To_Info>::lshift_assign(const From1& x, const From2& y) { if (check_empty_arg(x) || check_empty_arg(y)) return assign(EMPTY); + int inf = Parma_Polyhedra_Library::is_infinity(x); + if (inf) + return assign(NOT_A_NUMBER); + Interval<To_Boundary, To_Info> x1; Interval<To_Boundary, To_Info> z; Interval<To_Boundary, To_Info> @@ -1459,6 +1493,10 @@ Interval<To_Boundary, To_Info>::rshift_assign(const From1& x, const From2& y) { if (check_empty_arg(x) || check_empty_arg(y)) return assign(EMPTY); + int inf = Parma_Polyhedra_Library::is_infinity(x); + if (inf) + return assign(NOT_A_NUMBER); + Interval<To_Boundary, To_Info> x1; Interval<To_Boundary, To_Info> z; Interval<To_Boundary, To_Info>

1 0

[GIT] ppl/ppl(bounded_arithmetic): Minor changes to the code.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 25b80bc7ca0e0e921fcbb502a23bfbc0a70a3e91 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=25b80bc7ca0e… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 17:34:01 2011 +0200 Minor changes to the code. --- tests/Concrete_Expression/linearize_int.cc | 272 ++++++++++++++++------------ 1 files changed, 157 insertions(+), 115 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=25b80bc7…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Changed the documentation of the functions bitwise.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: aaca7bfedc40309394045897d3d7513a6db5e6c9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=aaca7bfedc40… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 17:32:06 2011 +0200 Changed the documentation of the functions bitwise. --- src/linearize_integer.hh | 331 ++++++++-------------------------------------- 1 files changed, 56 insertions(+), 275 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=aaca7bfe…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Small changes in the definition of functions and two additional functions: bool check_totaly which returns true only if
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 1aeb2d0117f75efed305c80a6598e49e1e869df7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1aeb2d0117f7… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 17:27:56 2011 +0200 Small changes in the definition of functions and two additional functions: bool check_totaly which returns true only if the linear forms are totally greater than or equal to zero or less than zero, and function bool incomplete which returns true if the two linear form have coefficients associated with the same variables, different from zero. --- src/Linear_Form.defs.hh | 22 ++- src/Linear_Form.templates.hh | 450 ++++++++---------------------------------- 2 files changed, 101 insertions(+), 371 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=1aeb2d01…

1 0