August 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Updated and typo fixed.
by Patricia Hill 03 Aug '10

03 Aug '10

Module: ppl/ppl Branch: master Commit: 984d8ba3c2d7d9e2302d7f369d07ca50c72c7351 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=984d8ba3c2d7… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Aug 3 20:49:26 2010 +0100 Updated and typo fixed. --- CREDITS | 10 +++++----- 1 files changed, 5 insertions(+), 5 deletions(-) diff --git a/CREDITS b/CREDITS index c797359..c047e89 100644 --- a/CREDITS +++ b/CREDITS @@ -58,7 +58,7 @@ Past Contributors: ------------------ Roberto Amadini (student of the University of Parma) - did some working on the PPL support for the + did some work on the PPL support for the approximation of floating point computations. Irene Bacchi (former student of the University of Parma) worked @@ -88,10 +88,10 @@ Past Contributors: solver, and also most of the Java and OCaml interfaces. - Katy Dobson [6] (University of Leeds) worked on the - formalization and definition of algorithms for - rational grids and products of grids and - polyhedra. + Katy Dobson [6] (former student of the University of Leeds) + worked on the formalization and definition of + algorithms for rational grids and products + of grids and polyhedra. Giordano Fracasso (University of Parma) wrote the initial version of the support for native and checked integer

1 0

[GIT] ppl/w3ppl(master): Updated and fixed a few bugs.
by Patricia Hill 03 Aug '10

03 Aug '10

Module: ppl/w3ppl Branch: master Commit: c401e378d113c3df2c1bf87c5ab2313d7f03d35b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=c401e378d1… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Aug 3 20:47:13 2010 +0100 Updated and fixed a few bugs. --- htdocs/Credits/Credits.raw | 16 ++++++++-------- 1 files changed, 8 insertions(+), 8 deletions(-) diff --git a/htdocs/Credits/Credits.raw b/htdocs/Credits/Credits.raw index 4081601..0ee838f 100644 --- a/htdocs/Credits/Credits.raw +++ b/htdocs/Credits/Credits.raw @@ -92,8 +92,8 @@ maintained and improved by the following people: <LI> Roberto Amadini (student of the University of Parma) - is working on the PPL support for the approximation - of floating point computations. + did some work on the PPL support for the + approximation of floating point computations. </LI> <LI> Irene Bacchi @@ -106,8 +106,8 @@ maintained and improved by the following people: <LI> Fabio Biselli (student of the University of Parma) - is working on the PPL support for the approximation - of floating point computations. + did some work on the PPL support for the + approximation of floating point computations. </LI> <LI> @@ -135,10 +135,10 @@ maintained and improved by the following people: </LI> <LI> <A HREF="http://www.comp.leeds.ac.uk/katyd">Katy Dobson</A> - (University of Leeds) is working on the - formalization and definition of algorithms - for rational grids and products of grids - and polyhedra. + (former student of the University of Leeds) + worked on the formalization and definition of + algorithms for rational grids and products + of grids and polyhedra. </LI> <LI> Giordano Fracasso

1 0

[GIT] ppl/w3ppl(master): Updated paragraph about the University of Leeds.
by Patricia Hill 03 Aug '10

03 Aug '10

Module: ppl/w3ppl Branch: master Commit: 93834253f0d6cc13c9ea2b42bcc2985c86372a3d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=93834253f0… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Aug 3 14:05:38 2010 +0100 Updated paragraph about the University of Leeds. --- htdocs/Contribute/Contribute.raw | 9 +++------ 1 files changed, 3 insertions(+), 6 deletions(-) diff --git a/htdocs/Contribute/Contribute.raw b/htdocs/Contribute/Contribute.raw index dc18070..417c153 100644 --- a/htdocs/Contribute/Contribute.raw +++ b/htdocs/Contribute/Contribute.raw @@ -186,12 +186,9 @@ progetto a Leeds sotto la direzione di Patricia Hill (vedi oltre). <IMG SRC="../images/en" ALT="English"> -If you are a student of the University of Leeds and you think that a -thesis or project may interest you, please get in touch with -<A HREF="http://www.cs.unipr.it/~hill/">Patricia M. Hill</A>. -If you would like to spend some time abroad, then why not consider a year -in Parma? -There is now an Erasmus link between the Universities of +If you are a student of the University of Leeds and would like to +spend some time abroad, then why not consider a year in Parma? +There is an Erasmus link between the Universities of Leeds and Parma so that undergraduates in Computing-related programmes at Leeds can spend an extra (third year) of study at Parma. Project work on the PPL (while on this programme) would be particularly

1 0

[GIT] ppl/w3ppl(master): Updated following the CREDITS file in the ppl.
by Patricia Hill 03 Aug '10

03 Aug '10

Module: ppl/w3ppl Branch: master Commit: 2e771410e35c08c580c156d0c55bf7b653eee84a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=2e771410e3… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Aug 3 12:08:43 2010 +0100 Updated following the CREDITS file in the ppl. --- htdocs/Credits/Credits.raw | 55 ++++++++++++++++++++++--------------------- 1 files changed, 28 insertions(+), 27 deletions(-) diff --git a/htdocs/Credits/Credits.raw b/htdocs/Credits/Credits.raw index 8365976..4081601 100644 --- a/htdocs/Credits/Credits.raw +++ b/htdocs/Credits/Credits.raw @@ -44,12 +44,6 @@ maintained and improved by the following people: <UL> <LI> - Roberto Amadini - (student of the University of Parma) - is working on the PPL support for the approximation - of floating point computations. - </LI> - <LI> Abramo Bagnara (Opera Unica) rewrote and generalized the support for checked coefficients. He also @@ -59,33 +53,12 @@ maintained and improved by the following people: design and implementation issues. </LI> <LI> - Fabio Biselli - (student of the University of Parma) - is working on the PPL support for the approximation - of floating point computations. - - </LI> - <LI> Fabio Bossi (student of the University of Parma) is working on the PPL support for the approximation of floating point computations. </LI> <LI> - Andrea Cimino - (former student of the University of Parma) - wrote most of the mixed - integer programming solver, and also most of - the Java and OCaml interfaces. - </LI> - <LI> - <A HREF="http://www.comp.leeds.ac.uk/katyd">Katy Dobson</A> - (University of Leeds) is working on the - formalization and definition of algorithms - for rational grids and products of grids - and polyhedra. - </LI> - <LI> <A HREF="http://www.prism.uvsq.fr/~fgalea/">François Galea</A> (University of Versailles) is working at the implementation of the Parametric Integer @@ -115,6 +88,13 @@ maintained and improved by the following people: <UL> + + <LI> + Roberto Amadini + (student of the University of Parma) + is working on the PPL support for the approximation + of floating point computations. + </LI> <LI> Irene Bacchi (former student of the University of Parma) @@ -124,6 +104,13 @@ maintained and improved by the following people: of two polyhedra is the same as their poly-hull. </LI> <LI> + Fabio Biselli + (student of the University of Parma) + is working on the PPL support for the approximation + of floating point computations. + + </LI> + <LI> Danilo Bonardi (former student of the University of Parma) worked on a development branch where he experimented @@ -140,6 +127,20 @@ maintained and improved by the following people: project started. </LI> <LI> + Andrea Cimino + (former student of the University of Parma) + wrote most of the mixed + integer programming solver, and also most of + the Java and OCaml interfaces. + </LI> + <LI> + <A HREF="http://www.comp.leeds.ac.uk/katyd">Katy Dobson</A> + (University of Leeds) is working on the + formalization and definition of algorithms + for rational grids and products of grids + and polyhedra. + </LI> + <LI> Giordano Fracasso (University of Parma) wrote the initial version of the support for native and checked integer

1 0

[GIT] ppl/ppl(floating_point): Do not use log2 to compute the base 2 logarithm of
by Fabio Bossi 03 Aug '10

03 Aug '10

Module: ppl/ppl Branch: floating_point Commit: f6167277a1078a7891e62097d4e034830001f373 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f6167277a107… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Aug 3 11:09:28 2010 +0200 Do not use log2 to compute the base 2 logarithm of an integer. --- src/Float.defs.hh | 9 +++++++++ src/Float.inlines.hh | 33 +++++++++++++++++++++++++++++++++ src/Float.templates.hh | 3 +-- src/Linear_Form.templates.hh | 3 +-- 4 files changed, 44 insertions(+), 4 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index 4e66c05..b437184 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -369,6 +369,15 @@ public: }; #endif +// FIXME: is this the right place for this function? +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +//! Returns the position of the most significative bit in \p a. +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) +unsigned int ld2(unsigned long long a); + +/* FIXME: some of the following documentation should probably be + under PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS */ + /*! \brief Returns <CODE>true</CODE> if and only if there is some floating point number that is representable by \p f2 but not by \p f1. diff --git a/src/Float.inlines.hh b/src/Float.inlines.hh index 219797b..2b9c3f2 100644 --- a/src/Float.inlines.hh +++ b/src/Float.inlines.hh @@ -451,6 +451,39 @@ is_less_precise_than(Floating_Point_Format f1, Floating_Point_Format f2) { return f1 < f2; } +#if defined(__GNUC__) +inline unsigned int ld2(unsigned long long a) { + return __builtin_clzll(a) ^ (sizeof(a)*8 - 1); +} +#else +unsigned int ld2(unsigned long long v) { + unsigned r = 0; + if (v >= 0x100000000ULL) { + v >>= 32; + r += 32; + } + if (v >= 0x10000) { + v >>= 16; + r += 16; + } + if (v >= 0x100) { + v >>= 8; + r += 8; + } + if (v >= 0x10) { + v >>= 4; + r += 4; + } + if (v >= 4) { + v >>= 2; + r += 2; + } + if (v >= 2) + r++; + return r; +} +#endif + template <typename FP_Interval_Type> inline void affine_form_image(std::map<dimension_type, diff --git a/src/Float.templates.hh b/src/Float.templates.hh index f062fde..287fb4f 100644 --- a/src/Float.templates.hh +++ b/src/Float.templates.hh @@ -113,8 +113,7 @@ const FP_Interval_Type& compute_absolute_error( // We assume that f_base is a power of 2. analyzer_format omega; - int power = static_cast<int>(log2(f_base)) * - (1 - f_exponent_bias - f_mantissa_bits); + int power = ld2(f_base) * (1 - f_exponent_bias - f_mantissa_bits); omega = std::max(static_cast<analyzer_format>(ldexpl(1.0, power)), std::numeric_limits<analyzer_format>::denorm_min()); diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index 5bb64c0..596e095 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -419,8 +419,7 @@ Linear_Form<C>::relative_error( C error_propagator; // We assume that f_base is a power of 2. - int power = static_cast<int>(log2(f_base)) * - (-f_mantissa_bits); + int power = ld2(f_base) * (-f_mantissa_bits); analyzer_format lb = -static_cast<analyzer_format>(ldexpl(1.0, power)); error_propagator.build(i_constraint(GREATER_OR_EQUAL, lb),

1 0

[GIT] ppl/w3ppl(master): Updated.
by Roberto Bagnara 03 Aug '10

03 Aug '10

Module: ppl/w3ppl Branch: master Commit: d62335323d3e4593666c4009e1af47a8efde0ffb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=d62335323d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Aug 3 09:15:46 2010 +0200 Updated. --- htdocs/FAQ.raw | 6 ++---- 1 files changed, 2 insertions(+), 4 deletions(-) diff --git a/htdocs/FAQ.raw b/htdocs/FAQ.raw index 4c9ec50..04baed2 100644 --- a/htdocs/FAQ.raw +++ b/htdocs/FAQ.raw @@ -456,10 +456,8 @@ they can choose among the C, C++, Java, OCaml and Prolog interfaces. A: -For PPL 0.11 we are adding new operations and numerical abstractions -that allow to approximate the result of bounded integer computations. If all goes well, PPL 0.12 will be focused on facilities to support -the analysis of floating point computations. +the analysis of floating point and machine integer computations. For the same release we hope to add serialization for all PPL objects. @@ -469,4 +467,4 @@ For the same release we hope to add serialization for all PPL objects. A: -It is difficult to say. We hope to release PPL 0.11 in May/June 2009. +It is difficult to say. We hope to release PPL 0.12 in January/February 2011.

1 0

[GIT] ppl/w3ppl(master): There are no known bugs in PPL 0.11.
by Roberto Bagnara 03 Aug '10

03 Aug '10

Module: ppl/w3ppl Branch: master Commit: 343e44d343e12fd0af3c7513ab8bf99633f6ebdd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=343e44d343… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Aug 3 09:04:24 2010 +0200 There are no known bugs in PPL 0.11. --- htdocs/Bugs/Bugs.raw | 7 +++---- 1 files changed, 3 insertions(+), 4 deletions(-) diff --git a/htdocs/Bugs/Bugs.raw b/htdocs/Bugs/Bugs.raw index 4b2bd94..727d624 100644 --- a/htdocs/Bugs/Bugs.raw +++ b/htdocs/Bugs/Bugs.raw @@ -32,16 +32,14 @@ to Report Bugs Effectively</A>, by Simon Tatham. <H2>Known Bugs in PPL @PPL_VERSION@</H2> - +

1 0

[GIT] ppl/w3ppl(master): Better explained how to check whether SSH connection to git.cs.unipr. it works.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/w3ppl Branch: master Commit: d28caceb2637b3d8128c2a2a05c55dab4c93cfe1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=d28caceb26… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 22:59:35 2010 +0200 Better explained how to check whether SSH connection to git.cs.unipr.it works. --- htdocs/Download/Git.raw | 15 +++++++++++++-- 1 files changed, 13 insertions(+), 2 deletions(-) diff --git a/htdocs/Download/Git.raw b/htdocs/Download/Git.raw index 24f4af4..273729b 100644 --- a/htdocs/Download/Git.raw +++ b/htdocs/Download/Git.raw @@ -149,8 +149,19 @@ issue the command <CODE>ssh git.cs.unipr.it -l myusername</CODE> </BLOCKQUOTE> -If this does not work there is no point in reading further: -solve this problem first. +If you have been granted full access to <CODE>git.cs.unipr.it</CODE> +you should obtain a shell prompt. Otherwise, if SSH connection works, +you will get the following message +<BLOCKQUOTE> +<PRE> +fatal: What do you think I am? A shell? +Connection to git.cs.unipr.it closed. +</PRE> +</BLOCKQUOTE> +In both cases (i.e., you obtain either a shell prompt or the message +<CODE>What do you think I am? A shell?</CODE>) +connection to <CODE>git.cs.unipr.it</CODE> via SSH works. +Otherwise there is no point in reading further: solve this problem first.

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Updated.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/ppl Branch: ppl-0_11-branch Commit: cfffb8ba3ff211dcf46d8fc927278c58cb444cbf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cfffb8ba3ff2… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 21:55:08 2010 +0200 Updated. --- ChangeLog | 8 ++++++++ 1 files changed, 8 insertions(+), 0 deletions(-) diff --git a/ChangeLog b/ChangeLog index 77daa9e..1171405 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2010-08-02 Roberto Bagnara <bagnara(a)cs.unipr.it> + * src/checked_int.inlines.hh: Added missing conversions. + +2010-08-02 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * ChangeLog, Watchdog/ChangeLog: Updated. + +2010-08-02 Roberto Bagnara <bagnara(a)cs.unipr.it> + * Makefile.am, README, Watchdog/Makefile.am, Watchdog/README: Distribute all READMEs and ChangeLogs.

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Added missing conversions.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/ppl Branch: ppl-0_11-branch Commit: b397097be829089e5306d0fda548ca097f1483e7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b397097be829… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 19:45:48 2010 +0200 Added missing conversions. --- src/checked_int.inlines.hh | 28 ++++++++++++++++++++-------- 1 files changed, 20 insertions(+), 8 deletions(-) diff --git a/src/checked_int.inlines.hh b/src/checked_int.inlines.hh index 79985cd..465dfcf 100644 --- a/src/checked_int.inlines.hh +++ b/src/checked_int.inlines.hh @@ -1178,7 +1178,8 @@ add_2exp_unsigned_int(Type& to, const Type x, unsigned int exp, } if (exp >= sizeof(Type) * CHAR_BIT) return set_pos_overflow_int<To_Policy>(to, dir); - return add_unsigned_int<To_Policy, From_Policy, void>(to, x, Type(1) << exp, dir); + Type n = Type(1) << exp; + return add_unsigned_int<To_Policy, From_Policy, void>(to, x, n, dir); } template <typename To_Policy, typename From_Policy, typename Type> @@ -1191,9 +1192,14 @@ add_2exp_signed_int(Type& to, const Type x, unsigned int exp, } if (exp >= sizeof(Type) * CHAR_BIT) return set_pos_overflow_int<To_Policy>(to, dir); - if (exp == sizeof(Type) * CHAR_BIT - 1) - return sub_signed_int<To_Policy, From_Policy, void>(to, x, -2 * (Type(1) << (exp - 1)), dir); - return add_signed_int<To_Policy, From_Policy, void>(to, x, Type(1) << exp, dir); + if (exp == sizeof(Type) * CHAR_BIT - 1) { + Type n = -2 * (Type(1) << (exp - 1)); + return sub_signed_int<To_Policy, From_Policy, void>(to, x, n, dir); + } + else { + Type n = Type(1) << exp; + return add_signed_int<To_Policy, From_Policy, void>(to, x, n, dir); + } } template <typename To_Policy, typename From_Policy, typename Type> @@ -1206,7 +1212,8 @@ sub_2exp_unsigned_int(Type& to, const Type x, unsigned int exp, } if (exp >= sizeof(Type) * CHAR_BIT) return set_neg_overflow_int<To_Policy>(to, dir); - return sub_unsigned_int<To_Policy, From_Policy, void>(to, x, Type(1) << exp, dir); + Type n = Type(1) << exp; + return sub_unsigned_int<To_Policy, From_Policy, void>(to, x, n, dir); } template <typename To_Policy, typename From_Policy, typename Type> @@ -1219,9 +1226,14 @@ sub_2exp_signed_int(Type& to, const Type x, unsigned int exp, } if (exp >= sizeof(Type) * CHAR_BIT) return set_neg_overflow_int<To_Policy>(to, dir); - if (exp == sizeof(Type) * CHAR_BIT - 1) - return add_signed_int<To_Policy, From_Policy, void>(to, x, -2 * (Type(1) << (exp - 1)), dir); - return sub_signed_int<To_Policy, From_Policy, void>(to, x, Type(1) << exp, dir); + if (exp == sizeof(Type) * CHAR_BIT - 1) { + Type n = -2 * (Type(1) << (exp - 1)); + return add_signed_int<To_Policy, From_Policy, void>(to, x, n, dir); + } + else { + Type n = Type(1) << exp; + return sub_signed_int<To_Policy, From_Policy, void>(to, x, n, dir); + } } template <typename To_Policy, typename From_Policy, typename Type>

1 0