June 2011 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(bounded_arithmetic): Adjusted definition of the class Test_Oracle, after new definition for class Oracle.
by Alberto Gioia 24 Jun '11

24 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 85fcc769e398169735fc0e352797cb1a4193362f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=85fcc769e398… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Fri Jun 24 17:48:12 2011 +0200 Adjusted definition of the class Test_Oracle, after new definition for class Oracle. --- tests/Concrete_Expression/digitalfilters1.cc | 10 +++++----- 1 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/Concrete_Expression/digitalfilters1.cc b/tests/Concrete_Expression/digitalfilters1.cc index b2e4741..d0fcf3e 100644 --- a/tests/Concrete_Expression/digitalfilters1.cc +++ b/tests/Concrete_Expression/digitalfilters1.cc @@ -43,13 +43,13 @@ public: return true; } - bool get_int_constant_value(const Int_Constant<C_Expr>& expr, - FP_Interval& result) const { + bool get_int_constant_value(const Int_Constant<C_Expr>&, + FP_Interval&) const { return false; } - bool get_integer_constant_value(const Integer_Constant<C_Expr>& expr, - FP_Interval& result) const { + bool get_integer_constant_value(const Integer_Constant<C_Expr>&, + FP_Interval&) const { return false; } @@ -76,7 +76,7 @@ public: result = expr.dimensions; return true; } - + FP_Interval_Abstract_Store int_store; };

1 0

[GIT] ppl/ppl(bounded_arithmetic): Added the definition of the class Int_Constant<C_Expr>, defined on a Intero_Interval.
by Alberto Gioia 24 Jun '11

24 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 0c26e9823dc777cf9f38045115b647e4c525017f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0c26e9823dc7… Author: Alberto Gioia <alberto.gioi1(a)studenti.unipr.it> Date: Fri Jun 24 17:32:56 2011 +0200 Added the definition of the class Int_Constant<C_Expr>, defined on a Intero_Interval. --- tests/Concrete_Expression/C_Expr.defs.hh | 13 +++++-------- tests/Concrete_Expression/C_Expr.inlines.hh | 16 ++++------------ 2 files changed, 9 insertions(+), 20 deletions(-) diff --git a/tests/Concrete_Expression/C_Expr.defs.hh b/tests/Concrete_Expression/C_Expr.defs.hh index c3beaf8..5b4adb5 100644 --- a/tests/Concrete_Expression/C_Expr.defs.hh +++ b/tests/Concrete_Expression/C_Expr.defs.hh @@ -36,7 +36,7 @@ enum C_Expr_Kind { INT_CON, INTEGER_CON, FP_CON, - APPROX_REF + APPROX_REF, }; //! Toy class for testing analysis of floating point computations. @@ -185,7 +185,7 @@ class Integer_Constant<C_Expr> public: //! Constructor from type and value. Integer_Constant<C_Expr>(Concrete_Expression_Type type, - const Integer_Interval& val); + const Integer_Interval& val); //! Do-nothing destructor. ~Integer_Constant<C_Expr>(); @@ -206,9 +206,8 @@ class Int_Constant<C_Expr> public Int_Constant_Common<C_Expr> { public: //! Constructor from value. - Int_Constant<C_Expr>(//Concrete_Expression_Type type, - const char* value_string, - unsigned int string_size); + Int_Constant<C_Expr>(Concrete_Expression_Type type, + const Intero_Interval& val); //! Do-nothing destructor. ~Int_Constant<C_Expr>(); @@ -220,10 +219,8 @@ public: enum { KIND = INTEGER_CON }; //! The Integer constant as written. - //char* value_bin - char* value; + Intero_Interval value; -// int value_dec; }; diff --git a/tests/Concrete_Expression/C_Expr.inlines.hh b/tests/Concrete_Expression/C_Expr.inlines.hh index 949a0a4..dc5b3b4 100644 --- a/tests/Concrete_Expression/C_Expr.inlines.hh +++ b/tests/Concrete_Expression/C_Expr.inlines.hh @@ -145,22 +145,14 @@ Integer_Constant<C_Expr>::~Integer_Constant<C_Expr>() { inline Int_Constant<C_Expr>:: -Int_Constant(//Concrete_Expression_Type type, - const char* value_string, - const unsigned int string_size) - : Concrete_Expression<C_Expr>(Concrete_Expression_Type::bounded_integer(BITS_8, SIGNED_2_COMPLEMENT, OVERFLOW_WRAPS), INTEGER_CON), - value(new char[string_size]) { - strcpy(value, value_string); +Int_Constant(Concrete_Expression_Type type, + const Intero_Interval& val) + : Concrete_Expression<C_Expr>(type, INTEGER_CON), + value(val) { } inline Int_Constant<C_Expr>::~Int_Constant<C_Expr>() { - delete[] value; -} - -inline Concrete_Expression_Type -Int_Constant<C_Expr>::type() const { - return expr_type; } inline

1 0

[GIT] ppl/ppl(bounded_arithmetic): Added declaration and definition of the functions for bitwise operators applied to Linear_Form .
by Alberto Gioia 24 Jun '11

24 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 46e7b546afe08a9ea5b86c05ca8de6d5209505b2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=46e7b546afe0… Author: Alberto Gioia <alberto.gioi1(a)studenti.unipr.it> Date: Fri Jun 24 17:29:15 2011 +0200 Added declaration and definition of the functions for bitwise operators applied to Linear_Form. --- src/Linear_Form.defs.hh | 82 +++++++++ src/Linear_Form.templates.hh | 407 ++++++++++++++++++++++++++++++++---------- 2 files changed, 392 insertions(+), 97 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=46e7b546…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Added definition of inline functions for bitwise operators.
by Alberto Gioia 24 Jun '11

24 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 2ff6c38751ea720fbf7e42049d800291dd3218a7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2ff6c38751ea… Author: Alberto Gioia <alberto.gioi1(a)studenti.unipr.it> Date: Fri Jun 24 17:23:34 2011 +0200 Added definition of inline functions for bitwise operators. --- src/Interval.inlines.hh | 776 ++++++++++++++++++++++++++-------------------- 1 files changed, 439 insertions(+), 337 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=2ff6c387…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Removed unnecessary and incorrect file.
by Alberto Gioia 24 Jun '11

24 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 9d341a874d7d1deb8bb58ab5950f755531df96fa URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9d341a874d7d… Author: Alberto Gioia <alberto.gioi1(a)studenti.unipr.it> Date: Fri Jun 24 17:19:26 2011 +0200 Removed unnecessary and incorrect file. --- tests/Concrete_Expression/Number_Conversion.cc | 28 ------------------------ tests/Concrete_Expression/Number_Convertion.cc | 28 ------------------------ 2 files changed, 0 insertions(+), 56 deletions(-) diff --git a/tests/Concrete_Expression/Number_Conversion.cc b/tests/Concrete_Expression/Number_Conversion.cc deleted file mode 100644 index 2d87e49..0000000 --- a/tests/Concrete_Expression/Number_Conversion.cc +++ /dev/null @@ -1,28 +0,0 @@ -void reverse(char *reversed) { - char tmp; - for (int i = 0, j = strlen(reversed)-1; i<j; i++, j--) { - tmp = reversed[i]; - reversed[i] = reversed[j]; - reversed[j] = tmp; - } -} - -char *itoa(int number) { - bool neg=number<0?true:false; - number=number<0?-number:number; - int length = (int)(log10(number))+1; - int i=0; - char *s = new char[length]; - do { - s[i++] = number % 10 + '0'; - } while ((number /= 10) > 0); - if (neg){ - s[i] = '-'; - s[++i] = '\0'; - } - else - s[i] = '\0'; - reverse(s); - return s; -} - diff --git a/tests/Concrete_Expression/Number_Convertion.cc b/tests/Concrete_Expression/Number_Convertion.cc deleted file mode 100644 index 2d87e49..0000000 --- a/tests/Concrete_Expression/Number_Convertion.cc +++ /dev/null @@ -1,28 +0,0 @@ -void reverse(char *reversed) { - char tmp; - for (int i = 0, j = strlen(reversed)-1; i<j; i++, j--) { - tmp = reversed[i]; - reversed[i] = reversed[j]; - reversed[j] = tmp; - } -} - -char *itoa(int number) { - bool neg=number<0?true:false; - number=number<0?-number:number; - int length = (int)(log10(number))+1; - int i=0; - char *s = new char[length]; - do { - s[i++] = number % 10 + '0'; - } while ((number /= 10) > 0); - if (neg){ - s[i] = '-'; - s[++i] = '\0'; - } - else - s[i] = '\0'; - reverse(s); - return s; -} -

1 0

[GIT] ppl/ppl(bounded_arithmetic): Added definitions of the functions for operators Bitwise.
by Alberto Gioia 24 Jun '11

24 Jun '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: fb91863a113480321fc0b9ea90de94f134cc2c9c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fb91863a1134… Author: Alberto Gioia <alberto.gioi1(a)studenti.unipr.it> Date: Fri Jun 24 17:09:45 2011 +0200 Added definitions of the functions for operators Bitwise. --- src/Interval.defs.hh | 18 +++++++++++++----- 1 files changed, 13 insertions(+), 5 deletions(-) diff --git a/src/Interval.defs.hh b/src/Interval.defs.hh index afaeccf..19a438c 100644 --- a/src/Interval.defs.hh +++ b/src/Interval.defs.hh @@ -853,27 +853,27 @@ public: template <typename From1, typename From2> typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value) - && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type + && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), void>::type or_assign(const From1& x, const From2& y); template <typename From1, typename From2> typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value) - && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type + && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), void>::type and_assign(const From1& x, const From2& y); template <typename From1, typename From2> typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value) - && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type + && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), void>::type xor_assign(const From1& x, const From2& y); template <typename From1, typename From2> typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value) - && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type + && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), void>::type lshift_assign(const From1& x, const From2& y); template <typename From1, typename From2> typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value) - && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type + && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), void>::type rshift_assign(const From1& x, const From2& y); template <typename From1, typename From2> @@ -891,6 +891,14 @@ public: && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type div_assign(const From1& x, const From2& y); + template <typename From> + typename Enable_If<((Is_Singleton<From>::value || Is_Interval<From>::value)), void>::type + max(const From& x); + + template <typename From> + typename Enable_If<((Is_Singleton<From>::value || Is_Interval<From>::value)), void>::type + min(const From& x); + template <typename From, typename Iterator> typename Enable_If<Is_Interval<From>::value, void>::type CC76_widening_assign(const From& y, Iterator first, Iterator last);

1 0

'Reply to' header issue
by rafael ff1 20 Jun '11

20 Jun '11

Roberto, This might not be news for you, but I guess it won't hurt asking: I can't see a "Reply To:" header set in the header of emails sent to this mail list, which seems be causing users to send replies to your address. Isn't it possible to set the default "reply to" address as ppl-devel(...) for emails sent to this list? Cheers, -- Rafael

2 1

Fwd: Re: Widening operation in Powerset
by Roberto Bagnara 19 Jun '11

19 Jun '11

-------- Original Message -------- Subject: Re: [PPL-devel] Widening operation in Powerset Date: Mon, 20 Jun 2011 00:52:47 +0530 From: Gokul Ramaswamy <gokulhcramaswamy(a)gmail.com> To: Roberto Bagnara <bagnara(a)cs.unipr.it> Prof. Roberto Bagnara, I need your help again. I have an example (the attached file). It gives the following output : { A - C = 0, -A >= -9, A >= 1 }, { B = 63 } But I was expecting the answer : { A - C = 0, A >= 1 }, { B = 63 } as the constraint A<=9 is violated by A==10 in the powerset poly3. I may be wrong as I am still learning Powerset Abstraction. On Sat, Jun 18, 2011 at 12:32 PM, Roberto Bagnara <bagnara(a)cs.unipr.it <mailto:bagnara@cs.unipr.it>> wrote: On 06/17/11 21:22, Gokul Ramaswamy wrote: I have understood that, in the polyhedron class, there is a BHRZ03_widening_assign() function which basically does the widening operation. But I am dealing with set of Polyhedrons, so I am using a Powerset class for it. But in the powerset class, I cannot find any widening operator. I want to do widening on my set of polyherdrons. Can someone please point me in the right direction in this regard. Hi Gokul. for the Pointset_Powerset (applied to any class of polyhedra) you can use BHZ03_widening_assign(). If an extrapolation operator (as opposed to a proper widening operator) is OK for you, there is also BGP99_extrapolation_assign(). Notice though that widening powersets of polyhedra is a rather advanced topic: you really have to read the library documentation. Cheers, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~__bagnara/ <http://www.cs.unipr.it/%7Ebagnara/> mailto:bagnara@cs.unipr.it <mailto:bagnara@cs.unipr.it> _________________________________________________ PPL-devel mailing list PPL-devel(a)cs.unipr.it <mailto:PPL-devel@cs.unipr.it> http://www.cs.unipr.it/__mailman/listinfo/ppl-devel <http://www.cs.unipr.it/mailman/listinfo/ppl-devel> -- Regards, Gokul Ramaswamy, Graduate Student, Department of CSE, IIT Bombay +919757417460 http://www.cse.iitb.ac.in/~ramaswamy <http://www.cse.iitb.ac.in/%7Eramaswamy>

1 1

Widening operation in Powerset
by Gokul Ramaswamy 18 Jun '11

18 Jun '11

Hello, I have understood that, in the polyhedron class, there is a BHRZ03_widening_assign() function which basically does the widening operation. But I am dealing with set of Polyhedrons, so I am using a Powerset class for it. But in the powerset class, I cannot find any widening operator. I want to do widening on my set of polyherdrons. Can someone please point me in the right direction in this regard. -- Regards, Gokul Ramaswamy, Graduate Student, Department of CSE, IIT Bombay +919757417460 http://www.cse.iitb.ac.in/~ramaswamy

2 1

Feasibility of Octagons in PPL
by Ramakrishna Upadrasta 17 Jun '11

17 Jun '11

Hello All, I would like to know if there is any feasibility test developed specifically of octagons in PPL. I am looking for a solution to the following problem: given a set of octagonal constraints, determine if the system is empty or not. If so, what are its details (method followed, complexity etc.)? Thanks Ramakrishna

2 3