May 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Added draft implementation for wrap_assign() for the grid domain.
by Patricia Hill 07 May '09

07 May '09

Module: ppl/ppl Branch: master Commit: ddecda47e763c5759190b167be835c9b77c82b49 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ddecda47e763… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Thu May 7 17:55:07 2009 +0100 Added draft implementation for wrap_assign() for the grid domain. --- src/Grid.defs.hh | 47 ++++++++++++++++ src/Grid_public.cc | 81 ++++++++++++++++++++++++++++ tests/Grid/Makefile.am | 5 ++- tests/Grid/wrap1.cc | 137 ++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 269 insertions(+), 1 deletions(-) diff --git a/src/Grid.defs.hh b/src/Grid.defs.hh index 0d3745f..1045bfa 100644 --- a/src/Grid.defs.hh +++ b/src/Grid.defs.hh @@ -1478,6 +1478,53 @@ public: */ void time_elapse_assign(const Grid& y); + /*! \brief + \ref Wrapping_Operator "Wraps" the specified dimensions of the + vector space. + + \param vars + The set of Variable objects corresponding to the space dimensions + to be wrapped. + + \param w + The width of the bounded integer type corresponding to + all the dimensions to be wrapped. + + \param s + The signedness of the bounded integer type corresponding to + all the dimensions to be wrapped. + + \param o + The overflow behavior of the bounded integer type corresponding to + all the dimensions to be wrapped. + + \param pcs + Possibly null pointer to a constraint system. + This argument is for compatibility with wrap_assign() + for the other domains and is ignored. + + \param complexity_threshold + A precision parameter of the \ref Wrapping_Operator "wrapping operator". + This argument is for compatibility with wrap_assign() + for the other domains and is ignored. + + \param wrap_individually + <CODE>true</CODE> if the dimensions should be wrapped individually. + As wrapping dimensions collectively does not improve the precision, + this argument is ignored. + + \exception std::invalid_argument + Thrown if \p *this is dimension-incompatible with one of the + Variable objects contained in \p vars or with <CODE>*pcs</CODE>. + */ + void wrap_assign(const Variables_Set& vars, + Bounded_Integer_Type_Width w, + Bounded_Integer_Type_Signedness s, + Bounded_Integer_Type_Overflow o, + const Constraint_System* pcs = 0, + unsigned complexity_threshold = 16, + bool wrap_individually = true); + //! Assigns to \p *this its topological closure. void topological_closure_assign(); diff --git a/src/Grid_public.cc b/src/Grid_public.cc index cfc3d31..1f2cda5 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -2639,6 +2639,87 @@ PPL::Grid::external_memory_in_bytes() const { + gen_sys.external_memory_in_bytes(); } +void +PPL::Grid::wrap_assign(const Variables_Set& vars, + Bounded_Integer_Type_Width w, + Bounded_Integer_Type_Signedness s, + Bounded_Integer_Type_Overflow o, + const Constraint_System*, + unsigned, + bool) { + + // If overflow is impossible do nothing. + if (o == OVERFLOW_IMPOSSIBLE) + // FIXME: CHECKME: 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. + return; + + // Wrapping no variable is a no-op. + if (vars.empty()) + return; + + const dimension_type space_dim = space_dimension(); + // Dimension-compatibility check of `vars'. + if (space_dim < vars.space_dimension()) { + std::ostringstream s; + s << "PPL::Grid::wrap_assign(vars, ...):" << std::endl + << "this->space_dimension() == " << space_dim + << ", required space dimension == " << vars.space_dimension() << "."; + throw std::invalid_argument(s.str()); + } + + // Wrapping an empty polyhedron is a no-op. + if (marked_empty()) + return; + if (!generators_are_up_to_date() && !update_generators()) + // Updating found `this' empty. + return; + + // Generators are up-to-date. + const Grid gr = *this; + + // If overflow is undefined, then all we know is that the variable + // will be integral. + 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(x, "wrap_assign(...)")) { + if (gr.constrains(x)) + // We know that x is not a constant, + // so x may wrap to any integral value. + add_grid_generator(parameter(x)); + } + } + return; + } + + // Overflow wraps. + assert(o == OVERFLOW_WRAPS); + // Set the wrap frequency for variables of width `w' and signedness `s'. + PPL_DIRTY_TEMP_COEFFICIENT(wrap_frequency); + if (s == UNSIGNED) + mul_2exp_assign(wrap_frequency, Coefficient_one(), w); + else { + assert(s == SIGNED_2_COMPLEMENT); + mul_2exp_assign(wrap_frequency, Coefficient_one(), w-1); + } + + 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(x, "wrap_assign(...)")) { + if (gr.constrains(x)) + // We know that x is not a constant, so x may wrap. + add_grid_generator(parameter(wrap_frequency * x)); + } + } +} + /*! \relates Parma_Polyhedra_Library::Grid */ std::ostream& PPL::IO_Operators::operator<<(std::ostream& s, const Grid& gr) { diff --git a/tests/Grid/Makefile.am b/tests/Grid/Makefile.am index 2291f76..7189082 100644 --- a/tests/Grid/Makefile.am +++ b/tests/Grid/Makefile.am @@ -117,7 +117,8 @@ topclosed1 \ topclosure1 \ unconstrain1 \ upperbound1 upperbound2 \ -widening1 widening2 widening3\ +widening1 widening2 widening3 \ +wrap1 \ writecongruencesystem XFAIL_TESTS = @@ -280,6 +281,8 @@ widening3_SOURCES = widening3.cc writecongruencesystem_SOURCES = writecongruencesystem.cc +wrap1_SOURCES = wrap1.cc + check_PROGRAMS = $(TESTS) MOSTLYCLEANFILES = \ diff --git a/tests/Grid/wrap1.cc b/tests/Grid/wrap1.cc new file mode 100644 index 0000000..1a810dc --- /dev/null +++ b/tests/Grid/wrap1.cc @@ -0,0 +1,137 @@ +/* Test Grid::wrap_assign(). + Copyright (C) 2001-2009 Roberto Bagnara <bagnara(a)cs.unipr.it> + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#include "ppl_test.hh" + +namespace { + +bool +test01() { + Variable x(0); + Variable y(1); + Grid gr(2); + gr.add_congruence((x + 24 %= 8*y) / 2); + gr.add_congruence((y %= 1) / 3); + + print_congruences(gr, "*** gr ***"); + + Variables_Set vars(x, y); + + gr.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + + Grid known_result(2); + known_result.add_congruence((x + 24 %= 8*y) / 2); + known_result.add_congruence((y %= 0) / 1); + + bool ok = (gr == known_result); + + print_congruences(gr, "*** gr.wrap_assign(...) ***"); + + return ok; +} + +bool +test02() { + Variable x(0); + Variable y(1); + Variable z(2); + + Grid gr(3); + gr.add_congruence(x + 24 %= 8*y); + gr.add_congruence((y %= 1) / 2); + + print_congruences(gr, "*** gr ***"); + + Variables_Set vars(x, y); + + gr.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED); + + Grid known_result(3); + known_result.add_congruence(x %= 0); + known_result.add_congruence(y %= 0); + + bool ok = (gr == known_result); + + print_congruences(gr, "*** gr.wrap_assign(...) ***"); + + return ok; +} + +bool +test03() { + Variable x(0); + Variable y(1); + Grid gr(2); + gr.add_congruence((x + 24 %= 8*y) / 255); + gr.add_congruence(x %= 0); + + print_congruences(gr, "*** gr ***"); + + Variables_Set vars(x, y); + + gr.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_IMPOSSIBLE); + + Grid known_result(2); + known_result.add_congruence(x %= 0); + known_result.add_congruence((x + 24 %= 8*y) / 255); + + bool ok = (gr == known_result); + + print_congruences(gr, "*** gr.wrap_assign(...) ***"); + + return ok; +} + +bool +test04() { + Variable x(0); + Variable y(1); + Variable z(2); + Variable w(3); + + Grid gr(4); + gr.add_congruence((x %= 255) / 0); + + print_congruences(gr, "*** gr ***"); + + Variables_Set vars(x, w); + + gr.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + + Grid known_result(4); + known_result.add_congruence((x %= 255) / 0); + + bool ok = (gr == known_result); + + print_congruences(gr, "*** gr.wrap_assign(...) ***"); + + return ok; +} + +} // namespace + +BEGIN_MAIN + DO_TEST(test01); + DO_TEST(test02); + DO_TEST(test03); + DO_TEST(test04); +END_MAIN

1 0

[GIT] ppl/ppl(master): Added basic timeout support to the Java library interface.
by Enea Zaffanella 07 May '09

07 May '09

Module: ppl/ppl Branch: master Commit: 14da854b5b2b1476c7eb46988cec83b29c4081fc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=14da854b5b2b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue May 5 23:36:20 2009 +0200 Added basic timeout support to the Java library interface. --- NEWS | 2 + interfaces/C/ppl_c_header.h | 2 +- interfaces/Java/jni/Makefile.am | 8 ++ interfaces/Java/jni/ppl_java_common.cc | 27 +++++ interfaces/Java/jni/ppl_java_common.defs.hh | 29 +++++- interfaces/Java/jni/ppl_java_globals.cc | 39 +++++++ .../Java/parma_polyhedra_library/Makefile.am | 2 + .../Parma_Polyhedra_Library.java | 27 +++++ .../parma_polyhedra_library/Timeout_Exception.java | 32 ++++++ interfaces/Java/tests/Makefile.am | 11 ++- .../Java/tests/Parma_Polyhedra_Library_test2.java | 105 ++++++++++++++++++++ 11 files changed, 281 insertions(+), 3 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=14da854b…

1 0

[GIT] ppl/w3ppl(master): Added LeconteB06.
by Roberto Bagnara 07 May '09

07 May '09

Module: ppl/w3ppl Branch: master Commit: a58127ff189a18f2ebaf4a97fe82a3b5a6cfe9c8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=a58127ff18… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu May 7 09:36:49 2009 +0200 Added LeconteB06. --- htdocs/Documentation/ppl_citations.bib | 89 ++++++++++++++++++++++---------- 1 files changed, 61 insertions(+), 28 deletions(-) diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib index 37eb18f..580609f 100644 --- a/htdocs/Documentation/ppl_citations.bib +++ b/htdocs/Documentation/ppl_citations.bib @@ -279,34 +279,6 @@ proved with classical linear invariants." } -@Inproceedings{BramanM08, - Title = "Safety Verification of Fault Tolerant Goal-based Control Programs - with Estimation Uncertainty", - Author = "J. M. B. Braman and R. M. Murray", - Booktitle = "Proceedings of the 2008 American Control Conference", - Address = "Seattle, Washington, USA", - Publisher = "IEEE Press", - Year = 2008, - Pages = "27--32", - ISSN = "0743-1619", - ISBN = "978-1-4244-2078-0", - Abstract = "Fault tolerance and safety verification of control - systems that have state variable estimation uncertainty - are essential for the success of autonomous robotic - systems. A software control architecture called mission - data system, developed at the Jet Propulsion Laboratory, - uses goal networks as the control program for autonomous - systems. Certain types of goal networks can be converted - into linear hybrid systems and verified for safety using - existing symbolic model checking software. A process for - calculating the probability of failure of certain - classes of verifiable goal networks due to state - estimation uncertainty is presented. A verifiable - example task is presented and the failure probability of - the control program based on estimation uncertainty is - found." -} - @Techreport{BagnaraR-CZ05TR, Author = "R. Bagnara and E. Rodr{\'\i}guez-Carbonell and E. Zaffanella", Title = "Generation of Basic Semi-algebraic Invariants @@ -374,6 +346,34 @@ a basis for an implementation of our representation." } +@Inproceedings{BramanM08, + Title = "Safety Verification of Fault Tolerant Goal-based Control Programs + with Estimation Uncertainty", + Author = "J. M. B. Braman and R. M. Murray", + Booktitle = "Proceedings of the 2008 American Control Conference", + Address = "Seattle, Washington, USA", + Publisher = "IEEE Press", + Year = 2008, + Pages = "27--32", + ISSN = "0743-1619", + ISBN = "978-1-4244-2078-0", + Abstract = "Fault tolerance and safety verification of control + systems that have state variable estimation uncertainty + are essential for the success of autonomous robotic + systems. A software control architecture called mission + data system, developed at the Jet Propulsion Laboratory, + uses goal networks as the control program for autonomous + systems. Certain types of goal networks can be converted + into linear hybrid systems and verified for safety using + existing symbolic model checking software. A process for + calculating the probability of failure of certain + classes of verifiable goal networks due to state + estimation uncertainty is presented. A verifiable + example task is presented and the failure probability of + the control program based on estimation uncertainty is + found." +} + @Techreport{CacheraM-A05, Author = "D. Cachera and K. Morin-Allory", Title = "Proving Parameterized Systems: The Use of a Widening Operator @@ -1668,6 +1668,39 @@ Polyhedra." } +@Inproceedings{LeconteB06, + Author = "M. Leconte and B. Berstel", + Title = "Extending a {CP} Solver with Congruences + as Domains for Program Verification", + Booktitle = "Proceedings of the 1st workshop on Constraints + in Software Testing, Verification and Analysis (CSTVA '06)", + Address = "Nantes, France", + Editor = "B. Blanc and A. Gotlieb and C. Michel", + Publisher = "IEEE Computer Society Press", + Pages = "22--33", + Year = 2006, + Abstract = "Constraints generated for Program Verification tasks + very often involve integer variables ranging on all the + machine-representable integer values. Thus, if the + propagation takes a time that is linear in the size of + the domains, it will not reach a fix point in practical + time. Indeed, the propagation time needed to reduce the + interval domains for as simple equations as $x = 2y + 1$ + and $x = 2z$ is proportional to the size of the initial + domains of the variables. To avoid this \emph{slow + convergence} phenomenon, we propose to enrich a + Constraint Programming Solver (CP Solver) with + \emph{congruence domains}. This idea has been introduced + by [Granger, P.: Static analysis of arithmetic congruences. + International Journal of Computer Math (1989) 165--199] + in the abstract interpretation community and we show how + a CP Solver can benefit from it, for example in + discovering immediately that $12x + |y| = 3$ and + $4z + 7y = 0$ have no integer solution.", + Note = "Available at + \url{http://www.irisa.fr/manifestations/2006/CSTVA06/}." +} + @Inproceedings{LogozzoF08, Author = "F. Logozzo and M. F{\"a}hndrich", Title = "Pentagons: A Weakly Relational Abstract Domain for the

1 0

[GIT] ppl/w3ppl(master): Added SenS07TR.
by Roberto Bagnara 07 May '09

07 May '09

Module: ppl/w3ppl Branch: master Commit: d6ac343c8a01664da0a95ed69d262bf81f80d13c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=d6ac343c8a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu May 7 08:04:15 2009 +0200 Added SenS07TR. --- htdocs/Documentation/ppl.bib | 27 +++++++++++++++++++++++++++ 1 files changed, 27 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index 3d81fc5..5a52eec 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -2322,6 +2322,33 @@ number of static objects being tracked." } +@Techreport{SenS07TR, + Author = "R. Sen and Y. N. Srikant", + Title = "Executable Analysis with Circular Linear Progressions", + Number = "IISc-CSA-TR-2007-3", + Institution = "Department of Computer Science and Automation, + Indian Institute of Science", + Address = "Bangalore, India", + Year = 2007, + Abstract = "We propose a new abstract domain for static analysis of + executable code. Concrete state is abstracted using + Circular Linear Progressions (CLPs). CLPs model + computations using a finite word length as is seen in + any real life processor. The finite abstraction allows + handling overflow scenarios in a natural and + straight-forward manner. Abstract transfer functions + have been defined for a wide range of operations which + makes this domain easily applicable for analysing code + for a wide range of ISAs. CLPs combine the scalability + of interval domains with the discreteness of linear + congruence domains. We also present a novel, lightweight + method to track linear equality relations between static + objects that is used by the analysis to improve + precision. The analysis is efficient, the total space + and time overhead being quadratic in the number of + static objects being tracked." +} + @Article{Shostak81, Author = "R. E. Shostak", Title = "Deciding Linear Inequalities by Computing Loop Residues",

1 0

[GIT] ppl/ppl(master): Fixed result check for ThrowNew.
by Abramo Bagnara 06 May '09

06 May '09

Module: ppl/ppl Branch: master Commit: 9381e735bd8858563a577503cdccea25041d96d2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9381e735bd88… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Wed May 6 19:54:16 2009 +0200 Fixed result check for ThrowNew. --- interfaces/Java/jni/ppl_java_common.cc | 16 ++++++++-------- interfaces/Java/jni/ppl_java_common.defs.hh | 20 ++++++++++---------- 2 files changed, 18 insertions(+), 18 deletions(-) diff --git a/interfaces/Java/jni/ppl_java_common.cc b/interfaces/Java/jni/ppl_java_common.cc index 1e45bb0..bea6bc7 100644 --- a/interfaces/Java/jni/ppl_java_common.cc +++ b/interfaces/Java/jni/ppl_java_common.cc @@ -190,7 +190,7 @@ handle_exception(JNIEnv* env, const std::overflow_error& e) { = env->FindClass("parma_polyhedra_library/Overflow_Error_Exception"); CHECK_RESULT_ASSERT(env, newExcCls); jint ret = env->ThrowNew(newExcCls, e.what()); - CHECK_RESULT_ABORT(env, ret); + CHECK_RESULT_ABORT(env, ret == 0); } void @@ -199,7 +199,7 @@ handle_exception(JNIEnv* env, const std::invalid_argument& e) { = env->FindClass("parma_polyhedra_library/Invalid_Argument_Exception"); CHECK_RESULT_ASSERT(env, newExcCls); jint ret = env->ThrowNew(newExcCls, e.what()); - CHECK_RESULT_ABORT(env, ret); + CHECK_RESULT_ABORT(env, ret == 0); } void @@ -208,7 +208,7 @@ handle_exception(JNIEnv* env, const std::logic_error& e) { = env->FindClass("parma_polyhedra_library/Logic_Error_Exception"); CHECK_RESULT_ASSERT(env, newExcCls); jint ret = env->ThrowNew(newExcCls, e.what()); - CHECK_RESULT_ABORT(env, ret); + CHECK_RESULT_ABORT(env, ret == 0); } void @@ -217,7 +217,7 @@ handle_exception(JNIEnv* env, const std::length_error& e) { = env->FindClass("parma_polyhedra_library/Length_Error_Exception"); CHECK_RESULT_ASSERT(env, newExcCls); jint ret = env->ThrowNew(newExcCls, e.what()); - CHECK_RESULT_ABORT(env, ret); + CHECK_RESULT_ABORT(env, ret == 0); } void @@ -226,7 +226,7 @@ handle_exception(JNIEnv* env, const std::domain_error& e) { = env->FindClass("parma_polyhedra_library/Domain_Error_Exception"); CHECK_RESULT_ASSERT(env, newExcCls); jint ret = env->ThrowNew(newExcCls, e.what()); - CHECK_RESULT_ABORT(env, ret); + CHECK_RESULT_ABORT(env, ret == 0); } void @@ -235,7 +235,7 @@ handle_exception(JNIEnv* env, const std::bad_alloc&) { = env->FindClass("java/lang/RuntimeException"); CHECK_RESULT_ASSERT(env, newExcCls); jint ret = env->ThrowNew(newExcCls, "Out of memory"); - CHECK_RESULT_ABORT(env, ret); + CHECK_RESULT_ABORT(env, ret == 0); } void @@ -243,7 +243,7 @@ handle_exception(JNIEnv* env, const std::exception& e) { jclass newExcCls = env->FindClass("java/lang/RuntimeException"); CHECK_RESULT_ASSERT(env, newExcCls); jint ret = env->ThrowNew(newExcCls, e.what()); - CHECK_RESULT_ABORT(env, ret); + CHECK_RESULT_ABORT(env, ret == 0); } void @@ -251,7 +251,7 @@ handle_exception(JNIEnv* env) { jclass newExcCls = env->FindClass("java/lang/RuntimeException"); CHECK_RESULT_ASSERT(env, newExcCls); jint ret = env->ThrowNew(newExcCls, "PPL bug: unknown exception raised"); - CHECK_RESULT_ABORT(env, ret); + CHECK_RESULT_ABORT(env, ret == 0); } jobject diff --git a/interfaces/Java/jni/ppl_java_common.defs.hh b/interfaces/Java/jni/ppl_java_common.defs.hh index 1d66c20..72f2d1c 100644 --- a/interfaces/Java/jni/ppl_java_common.defs.hh +++ b/interfaces/Java/jni/ppl_java_common.defs.hh @@ -75,26 +75,26 @@ site: http://www.cs.unipr.it/ppl/ . */ if (env->ExceptionOccurred()) \ return; \ } while (0) -#define CHECK_RESULT_ABORT(env, result) \ +#define CHECK_RESULT_ABORT(env, cond) \ do { \ - if (!result) \ + if (!(cond)) \ abort(); \ } while (0) -#define CHECK_RESULT_ASSERT(env, result) \ - assert(result) -#define CHECK_RESULT_THROW(env, result) \ +#define CHECK_RESULT_ASSERT(env, cond) \ + assert(cond) +#define CHECK_RESULT_THROW(env, cond) \ do { \ - if (!result) \ + if (!(cond)) \ throw Java_ExceptionOccurred(); \ } while (0) -#define CHECK_RESULT_RETURN(env, result, val) \ +#define CHECK_RESULT_RETURN(env, cond, val) \ do { \ - if (!result) \ + if (!(cond)) \ return val; \ } while (0) -#define CHECK_RESULT_RETURN_VOID(env, result) \ +#define CHECK_RESULT_RETURN_VOID(env, cond) \ do { \ - if (!result) \ + if (!(cond)) \ return; \ } while (0)

1 0

[GIT] ppl/ppl(master): test03() fails also with 16-bit coefficients when assertions are enabled.
by Roberto Bagnara 06 May '09

06 May '09

Module: ppl/ppl Branch: master Commit: 41aeb3ccffeba265b3b0458070936d5eab562ace URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=41aeb3ccffeb… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed May 6 16:06:29 2009 +0200 test03() fails also with 16-bit coefficients when assertions are enabled. --- tests/Polyhedron/wrap1.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index d1c9516..97beb08 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -436,7 +436,7 @@ test14() { BEGIN_MAIN DO_TEST_F16(test01); DO_TEST_F16(test02); - DO_TEST_F8(test03); + DO_TEST_F16A(test03); DO_TEST_F8(test04); DO_TEST_F16(test05); DO_TEST_F16(test06);

1 0

Re: [PPL-devel] Problems with in-tree host libraries (gmp, ppl, etc)
by Roberto Bagnara 06 May '09

06 May '09

Kaveh R. GHAZI wrote: > On Sat, 2 May 2009, Anthony Green wrote: > >> The top level configury suggests that you can simply drop gmp, ppl, etc >> into the top level source dir and they will get configured and used. >> Does this really work? > > It is supposed to. I haven't worked on or tested the ppl machinery so I > don't know what shape it is in. > > >> Index: Makefile.def >> =================================================================== >> --- Makefile.def (revision 146995) >> +++ Makefile.def (working copy) >> @@ -60,7 +60,7 @@ >> host_modules= { module= gawk; }; >> host_modules= { module= gettext; }; >> host_modules= { module= gmp; lib_path=.libs; bootstrap=true; >> - extra_configure_flags='--disable-shared'; >> + extra_configure_flags='--disable-shared --enable-cxx'; >> no_install= true; >> host="none-${host_vendor}-${host_os}"; >> target="none-${host_vendor}-${host_os}"; }; > > > I would only pass in this flag if ppl is being used. Look at what I did > with extra_mpfr_configure_flags in the top level directory. You can use a > similar mechanism to have a flag passed in to the gmp build conditionally. > > >> Even then, the ppl configury isn't detecting the gmp we just built. It >> seems as though we should install gmp in a local temporary install tree >> and point ppl at that. See below for a trace of the ppl configury as it >> attempts to detect an in-tree gmp (after applying the patch above). >> AG > > I don't know if ppl was ever setup to detect/use an in-tree gmp. It would > need to be able to specify --with-gmp-build= or something equivalent to > get the header and library from a build tree rather than an install tree. > They're laid out slightly differently. The PPL configure script offers the following options: --with-libgmp-prefix[=DIR] search for libgmp in DIR/include and DIR/lib --without-libgmp-prefix don't search for libgmp in includedir and libdir --with-libgmpxx-prefix[=DIR] search for libgmpxx in DIR/include and DIR/lib --without-libgmpxx-prefix don't search for libgmpxx in includedir and libdir If the C and the C++ interface of GMP have been installed in the same places, specifying --with-libgmp-prefix[=DIR] is enough. If you think that being able to use a non-installed GMP build tree is important, we can add an option to that effect. -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

2 1

PPL Library capabilities
by Vladimir Koshelev 06 May '09

06 May '09

Hello. We have polyhedral representation in our research work and use your library(PPL) through Java interface. We have the following problem: We have matrix *A(n, m)* with *rank(A)* < *min(n, m).* Also we have system of equations *Ax = 0*. We need to find *x = Uy*, where *U* is integer upper triangular matrix, *x* is an integer solution of previous system and* y* is a vector of arbitrary integer constants. Can we solve this problem, using your library(Java interface)? We need only integer solutions.

2 1

[GIT] ppl/ppl(master): test07() only fails if assertions are enabled.
by Roberto Bagnara 05 May '09

05 May '09

Module: ppl/ppl Branch: master Commit: 02f325cfd0097877d6e5d8f5db768666ba733c9c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=02f325cfd009… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue May 5 20:59:10 2009 +0200 test07() only fails if assertions are enabled. --- tests/Polyhedron/wrap1.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index 7114e88..d1c9516 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -440,7 +440,7 @@ BEGIN_MAIN DO_TEST_F8(test04); DO_TEST_F16(test05); DO_TEST_F16(test06); - DO_TEST_F16(test07); + DO_TEST_F16A(test07); DO_TEST_F8(test08); DO_TEST_F16(test09); DO_TEST_F16(test10);

1 0

[GIT] ppl/ppl(master): Spurious parentheses removed.
by Roberto Bagnara 05 May '09

05 May '09

Module: ppl/ppl Branch: master Commit: eb174e19d377d1cc1022c3d791f9be95fbdbe833 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eb174e19d377… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue May 5 19:50:08 2009 +0200 Spurious parentheses removed. --- interfaces/Java/jni/ppl_java_common.cc | 14 +++++++------- interfaces/OCaml/ppl_ocaml_common.cc | 2 +- src/BD_Shape.templates.hh | 2 +- src/Checked_Number.templates.hh | 2 +- src/Grid_public.cc | 2 +- src/Interval_Info.defs.hh | 3 ++- src/MIP_Problem.cc | 2 +- src/OR_Matrix.inlines.hh | 2 +- src/Octagonal_Shape.templates.hh | 2 +- src/Polyhedron_nonpublic.cc | 2 +- src/Polyhedron_public.cc | 6 +++--- tests/BD_Shape/affinedimension1.cc | 2 +- tests/BD_Shape/containsintegerpoint1.cc | 2 +- tests/Box/affinedimension1.cc | 2 +- tests/Octagonal_Shape/containsintegerpoint1.cc | 2 +- .../partiallyreducedproduct2.cc | 4 ++-- tests/Polyhedron/dualhypercubes.cc | 2 +- tests/Polyhedron/generators1.cc | 2 +- tests/Polyhedron/maxspacedim1.cc | 2 +- tests/Polyhedron/polyhull1.cc | 2 +- tests/Polyhedron/relations1.cc | 2 +- 21 files changed, 31 insertions(+), 30 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=eb174e19…

1 0