- PPL-devel - BUGSENG Mailman

[GIT] ppl/w3ppl(master): Added link to SpaceEx.
by Roberto Bagnara 19 Aug '11

19 Aug '11

Module: ppl/w3ppl Branch: master Commit: 7b8df5899045579e4d9e24594a48d66f46452ce0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=7b8df58990… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Aug 19 08:45:14 2011 +0200 Added link to SpaceEx. --- htdocs/Applications/Applications.raw | 5 +++++ 1 files changed, 5 insertions(+), 0 deletions(-) diff --git a/htdocs/Applications/Applications.raw b/htdocs/Applications/Applications.raw index 3980cb9..00c429c 100644 --- a/htdocs/Applications/Applications.raw +++ b/htdocs/Applications/Applications.raw @@ -10,6 +10,11 @@ Here are the ones we are aware of. <UL> <LI> + The <A HREF="http://spaceex.imag.fr/">SpaceEx</A> tool platform + facilitates the implementation of algorithms related to reachability + and safety verification. + </LI> + <LI> <A HREF="http://gcc.gnu.org/wiki/Graphite">Graphite</A> (Gimple Represented as Polyhedra), a framework for high-level loop optimizations that is now part of

1 0

Re: [PPL-devel] Fwd: PPL and FPU rounding mode
by Roberto Bagnara 13 Aug '11

13 Aug '11

On 08/10/11 21:18, Benjamin Hiller wrote: > Dear Prof. Roberto, > > thank you very much for your quick reply. > > Am 10.08.2011 18:38, schrieb Roberto Bagnara: >> If you call restore_pre_PPL_rounding() reset the rounding mode to its >> default (typically round-to-nearest) AND you use a PPL abstraction >> based on floating point numbers without first calling >> set_rounding_for_PPL() then the result computed by PPL will be bogus. >> For example, you may have a non-empty box be mistaken for empty. Of >> course, you may be lucky, but I would not count on that. > > Our data should be such that each polyhedron is far from being > degenerated so I don't think they will become empty due to rounding. > >> Which PPL classes are you using? Many PPL classes are not based on >> floating point numbers. If you only use those, then there is no problem >> at all, whatever rounding mode is in effect. > > So far we are using the classes Variable, Variable_Set, > Generator_System, Linear_Expression, Generator, C_Polytope, > Constraint_System, Constraint. I'm not sure whether this is the > information you need. As far as I know (I did not do the > implementation myself), we scale everything such that we have > integer points/constraint coefficients. If by C_Polytope you mean C_Polyhedron and if the list of classes above is otherwise complete, then your usage of the PPL does not depend on the floating point rounding mode in effect. So you should not worry. > In any case, it is only slightly more inconvenient to turn on the > appropriate rounding mode for PPL before using it so we might better > do that. This might be a wise thing if there is the danger that someone, one day, may use other PPL abstractions based on machine floating-point numbers. > Best regards, > > Benjamin Cheers, Roberto P.S. Please direct all messages concerning the PPL to ppl-devel(a)cs.unipr.it -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

2 2

the latest ppl git configure script has something wrong
by PcX 11 Aug '11

11 Aug '11

Hi, all When I configure the latest ppl git, some strange errors come out, but the ppl git at 6.10 has no problem. Full log is in the attachment. First, I type autoreconf -i. My configure is : ./configure --prefix=/mingw --enable-static --disable-shared The errors are: checking for the GMP library version 4.1.3 or above... ./configure: line 9983: cat: No such file or directory ./configure: line 2292: sed: No such file or directory ./configure: line 2296: rm: No such file or directory no ./configure: line 10052: rm: No such file or directory ./configure: eval: line 10172: syntax error near unexpected token `(' ./configure: eval: line 10172: `PATH=.:/usr/local/bin:/mingw/bin:/bin:/e/mypack/mingw-eq/bin:/e/mypack/mingw-eq/libexec/gcc/i686-pc-mingw32/4.7.0:/e/mingw32/bin:/e/mingw32/libexec/gcc/i686-pc-mingw32/4.7.0:/c/Program Files (x86)/NVIDIA Corporation/PhysX/Common:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/intel64/mpirt:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/intel64/compiler:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/ia32/mpirt:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/ia32/compiler:/d/Program Files (x86)/Intel/ComposerXE-2011/compiler/lib:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/intel64/tbb/vc10:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/ia32/tbb/vc10:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/intel64/ipp:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/ia32/ipp:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/intel64/mkl:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/ia32/mkl:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/intel64/compiler:/d/Program Files (x86)/Intel/ComposerXE-2011/redist/ia32/compiler:/d/Program Files (x86)/Intel/ComposerXE-2011/compiler/lib:/c/Windows/system32:/c/Windows:/c/Windows/System32/Wbem:/c/Windows/System32/WindowsPowerShell/v1.0/:/f/Backup/SystemTools/MaintenanceTools/Windows7Master:/c/Program Files (x86)/Common Files/Thunder Network/KanKan/Codecs:/c/Program Files/Lenovo/Bluetooth Software/:/c/Program Files/Lenovo/Bluetooth Software/syswow64:/c/Program Files/Intel/WiFi/bin/:/c/Program Files/Common Files/Intel/WirelessCommon/:/e/MyPack/Tools/TortoiseSVN/bin:/e/MyPack/Tools/TortoiseGit/bin:/c/Program Files/Microsoft Windows Performance Toolkit/:/d/Program Files (x86)/QuickTime/QTSystem/:/e/MyPack/MinGW/bin:/e/MyPack/Compiler/Python27:/e/MyPack/GnuWin32/bin:/e/MyPack/3rdLib/GUI/Qt/Qt_lib_vc/bin:/e/MyPack/Cygwin/bin:/usr/bin' configure: error: Cannot find GMP version 4.1.3 or higher. GMP is the GNU Multi-Precision library: see http://www.swox.com/gmp/ for more information. When compiling the GMP library, do not forget to enable the C++ interface: add --enable-cxx to the configuration options. ./configure: line 366: sed: No such file or directory ./configure: line 321: sort: No such file or directory ./configure: line 318: sed: No such file or directory ./configure: line 336: sort: No such file or directory ./configure: line 360: cat: No such file or directory ./configure: line 367: rm: No such file or directory -- Best Regards, PcX

4 21

Two failing tests on Solaris
by Maciej Bliziński 11 Aug '11

11 Aug '11

Hello PPL developers, I'm a package maintainer at OpenCSW, a project providing binary packages for Solaris. I'm currently working on building PPL. I've compiled the dependencies and the PPL library itself. There are two failing tests that prevent me from releasing the updated binary. The library is built with gcc-4.3.3. maciej@unstable9s :~/src/opencsw/pkg/ppl/trunk > /opt/csw/gcc4/bin/gcc --version gcc (GCC) 4.3.3 maciej@unstable9s :~/src/opencsw/pkg/ppl/trunk > uname -a SunOS unstable9s 5.9 Generic_Virtual sun4u sparc SUNW,SPARC-Enterprise-T5220 Compilation flags: CFLAGS = -O0 -mcpu=v8 CXXFLAGS = -O0 -mcpu=v8 CPPFLAGS = -I/opt/csw/include FFLAGS = -O0 -mcpu=v8 FCFLAGS = -O0 -mcpu=v8 LDFLAGS = -L/opt/csw/gcc4/lib/. -mcpu=v8 -lgnugetopt -L/opt/csw/lib LD_OPTIONS = -R/opt/csw/gcc4/lib -R/opt/csw/lib/$ISALIST -R/opt/csw/lib ASFLAGS = OPTFLAGS = -O0 -mcpu=v8 When running the tests by hand: gmake[5]: Entering directory `/home/maciej/src/opencsw/pkg/ppl/trunk/work/solaris9-sparc/build-isa-sparcv8/ppl-0.11.2/tests/Partially_Reduced_Product' (...) FAIL: bounds1 (..._ FAIL: smashproduct1 When running the binary by hand, I see a segfault: maciej@unstable9s :~/src/opencsw/pkg/ppl/trunk > work/solaris9-sparc/build-isa-sparcv8/ppl-0.11.2/tests/Partially_Reduced_Product/bounds1 Bus Error (core dumped) maciej@unstable9s :~/src/opencsw/pkg/ppl/trunk > pstack ./core core './core' of 18057: /home/maciej/src/opencsw/pkg/ppl/trunk/work/solaris9-sparc/build-isa-s fed5e4d4 emutls_destroy (bb218, fed5e494, 0, bb618, 1, ffbff82c) + 40 febd6aa8 keys_destruct (0, 9f384, 5068c, feb8bb08, 5, 0) + 68 feb9cce8 _exithandle (511c4, 2, fb, 10034, ffffffff, fec3c000) + 70 fec207c0 exit (0, ffbff934, ffbff93c, b8fdc, 7d8, ffbffa54) + 24 000511c4 _start (0, ffbff934, 1, ff3dc608, ff3ee834, ff3ee000) + 64 For easier inspection, I've tarred up the whole build: http://buildfarm.opencsw.org/~maciej/ppl-2011-08-11.tar.gz Do you have an idea what might be the problem? Maciej

2 7

[GIT] ppl/ppl(master): Prepend to old content of shared library path var, instead of overwriting.
by Abramo Bagnara 11 Aug '11

11 Aug '11

Module: ppl/ppl Branch: master Commit: b74a88168b9467502abe2cf1ea3919291ebdc387 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b74a88168b94… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Thu Aug 11 12:49:13 2011 +0200 Prepend to old content of shared library path var, instead of overwriting. --- m4/ac_check_gmp.m4 | 8 ++++---- 1 files changed, 4 insertions(+), 4 deletions(-) diff --git a/m4/ac_check_gmp.m4 b/m4/ac_check_gmp.m4 index ffe9eef..42db027 100644 --- a/m4/ac_check_gmp.m4 +++ b/m4/ac_check_gmp.m4 @@ -61,7 +61,7 @@ AC_ARG_WITH(gmp-build, || test -n "$with_gmp_include" || test -n "$with_gmp_lib" then gmp_include_options="-I$gmp_build_dir -I$gmp_build_dir/tune" - gmp_library_paths="$gmp_build_dir:$gmp_build_dir/.libs:$gmp_build_dir/tune" + gmp_library_paths="$gmp_build_dir$PATH_SEPARATOR$gmp_build_dir/.libs:$gmp_build_dir/tune" gmp_library_options="-L$gmp_build_dir -L$gmp_build_dir/.libs" gmp_library_options="$gmp_library_options -L$gmp_build_dir/tune" else @@ -74,8 +74,8 @@ ac_save_CPPFLAGS="$CPPFLAGS" CPPFLAGS="$CPPFLAGS $gmp_include_options" ac_save_LIBS="$LIBS" LIBS="$LIBS $gmp_library_options" -eval ac_save_shared_library_path_env_var="\$$shared_library_path_env_var" -eval $shared_library_path_env_var=\"$gmp_library_paths\" +eval ac_save_shared_library_path="\$$shared_library_path_env_var" +eval $shared_library_path_env_var=\"$gmp_library_paths:$ac_save_shared_library_path\" export $shared_library_path_env_var AC_LANG_PUSH(C++) @@ -217,7 +217,7 @@ AC_DEFINE_UNQUOTED(PPL_GMP_SUPPORTS_EXCEPTIONS, $value, fi AC_LANG_POP(C++) -eval $shared_library_path_env_var=\"$ac_save_shared_library_path_env_var\" +eval $shared_library_path_env_var=\"$ac_save_shared_library_path\" LIBS="$ac_save_LIBS" CPPFLAGS="$ac_save_CPPFLAGS" ])

1 0

[GIT] ppl/ppl(master): Quoted more double quotes.
by Roberto Bagnara 10 Aug '11

10 Aug '11

Module: ppl/ppl Branch: master Commit: a948c306a9a705a2b170eb1888afe2778ed06154 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a948c306a9a7… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 10 20:42:12 2011 +0200 Quoted more double quotes. --- m4/ac_check_gmp.m4 | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/m4/ac_check_gmp.m4 b/m4/ac_check_gmp.m4 index e4bb602..ffe9eef 100644 --- a/m4/ac_check_gmp.m4 +++ b/m4/ac_check_gmp.m4 @@ -75,7 +75,7 @@ CPPFLAGS="$CPPFLAGS $gmp_include_options" ac_save_LIBS="$LIBS" LIBS="$LIBS $gmp_library_options" eval ac_save_shared_library_path_env_var="\$$shared_library_path_env_var" -eval $shared_library_path_env_var="$gmp_library_paths" +eval $shared_library_path_env_var=\"$gmp_library_paths\" export $shared_library_path_env_var AC_LANG_PUSH(C++)

1 0

[GIT] ppl/ppl(master): Quoted double quotes.
by Roberto Bagnara 10 Aug '11

10 Aug '11

Module: ppl/ppl Branch: master Commit: 633ccc979bf58a29cdc65af36816804c1cdddc57 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=633ccc979bf5… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 10 19:35:47 2011 +0200 Quoted double quotes. --- m4/ac_check_gmp.m4 | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/m4/ac_check_gmp.m4 b/m4/ac_check_gmp.m4 index 9d58d02..e4bb602 100644 --- a/m4/ac_check_gmp.m4 +++ b/m4/ac_check_gmp.m4 @@ -217,7 +217,7 @@ AC_DEFINE_UNQUOTED(PPL_GMP_SUPPORTS_EXCEPTIONS, $value, fi AC_LANG_POP(C++) -eval $shared_library_path_env_var="$ac_save_shared_library_path_env_var" +eval $shared_library_path_env_var=\"$ac_save_shared_library_path_env_var\" LIBS="$ac_save_LIBS" CPPFLAGS="$ac_save_CPPFLAGS" ])

1 0

Fwd: PPL and FPU rounding mode
by Roberto Bagnara 10 Aug '11

10 Aug '11

-------- Original Message -------- Subject: PPL and FPU rounding mode Date: Wed, 10 Aug 2011 16:12:32 +0200 From: Benjamin Hiller <hiller(a)zib.de> To: bagnara(a)cs.unipr.it Dear Prof. Bagnara, we are using your PPL in a research project and so far it perfectly suits our needs. Thank you for developing such a great piece of software and making it available for research. There is a question I could not find enough details for on the web. I found out that using the functions restore_pre_PPL_rounding() and set_rounding_for_PPL() a user can manually decide when the conservative rounding mode assumed by PPL is in effect. The documentation states that "After calling restore_pre_PPL_rounding() it is absolutely necessary to call set_rounding_for_PPL() before using any PPL abstractions based on floating point numbers." to obtain correct results. Does this mean that if I do not set the PPL-rounding mode, all the results computed by PPL will be bogus? Or does it mean that they may be less accurate/correct approximations that are no longer suitable for proving something? (I understand that PPL has been used for verification where this issue is very important.) In our project, we use PPL to compute polyhedrons that are approximations anyway and some loss of accuracy would not hurt much. It is safe under these circumstances to just disable the rounding mode used by PPL? Best regards, Benjamin Hiller -- Benjamin Hiller hiller(a)zib.de Abteilung Optimierung phone +49 30 84185-406 Konrad-Zuse-Zentrum für Informationstechnik Berlin (ZIB) Takustraße 7 14195 Berlin

1 1

[GIT] ppl/ppl(master): More missing quotes added.
by Roberto Bagnara 10 Aug '11

10 Aug '11

Module: ppl/ppl Branch: master Commit: a28af2b43f0747cfa701c1f5636a11f4f51b3f6a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a28af2b43f07… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 10 18:22:47 2011 +0200 More missing quotes added. --- m4/ac_check_gmp.m4 | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/m4/ac_check_gmp.m4 b/m4/ac_check_gmp.m4 index 76e54e4..9d58d02 100644 --- a/m4/ac_check_gmp.m4 +++ b/m4/ac_check_gmp.m4 @@ -217,7 +217,7 @@ AC_DEFINE_UNQUOTED(PPL_GMP_SUPPORTS_EXCEPTIONS, $value, fi AC_LANG_POP(C++) -eval $shared_library_path_env_var=$ac_save_shared_library_path_env_var +eval $shared_library_path_env_var="$ac_save_shared_library_path_env_var" LIBS="$ac_save_LIBS" CPPFLAGS="$ac_save_CPPFLAGS" ])

1 0

[GIT] ppl/ppl(master): Missing quotes added.
by Roberto Bagnara 10 Aug '11

10 Aug '11

Module: ppl/ppl Branch: master Commit: 7351f86ec396806840f67556a30c12b10c2ce6ff URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7351f86ec396… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 10 09:20:06 2011 +0200 Missing quotes added. --- m4/ac_check_gmp.m4 | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/m4/ac_check_gmp.m4 b/m4/ac_check_gmp.m4 index 35efd5c..76e54e4 100644 --- a/m4/ac_check_gmp.m4 +++ b/m4/ac_check_gmp.m4 @@ -75,7 +75,7 @@ CPPFLAGS="$CPPFLAGS $gmp_include_options" ac_save_LIBS="$LIBS" LIBS="$LIBS $gmp_library_options" eval ac_save_shared_library_path_env_var="\$$shared_library_path_env_var" -eval $shared_library_path_env_var=$gmp_library_paths +eval $shared_library_path_env_var="$gmp_library_paths" export $shared_library_path_env_var AC_LANG_PUSH(C++)

1 0