- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Mentioned the improvement in the polyhedra conversion algorithm.
by Enea Zaffanella 10 Feb '16

10 Feb '16

Module: ppl/ppl Branch: master Commit: e1d8ae6dff428bd849b8fe3b0adc7d40e9e0891f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e1d8ae6dff42… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Feb 10 09:49:57 2016 +0100 Mentioned the improvement in the polyhedra conversion algorithm. --- NEWS | 5 ++++- 1 files changed, 4 insertions(+), 1 deletions(-) diff --git a/NEWS b/NEWS index bee0c90..49ff56f 100644 --- a/NEWS +++ b/NEWS @@ -15,8 +15,11 @@ NEWS for version 1.2 (released date to be decided) New and Changed Features ======================== -o TO BE WRITTEN +o Improved the efficiency of the conversion procedure for polyhedra + by adding a quick adjacency check. +o In the Java language interface, throw an exception when trying + to build a disequality Constraint. Bugfixes

1 0

[GIT] ppl/ppl(master): Be more consistent in the usage of PPL_DIRTY_TEMP macros.
by Enea Zaffanella 10 Feb '16

10 Feb '16

Module: ppl/ppl Branch: master Commit: 6b995ed0383990716171272238c550a02889fc13 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6b995ed03839… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Feb 10 09:47:40 2016 +0100 Be more consistent in the usage of PPL_DIRTY_TEMP macros. Got rid of a couple of FIXME's. --- src/BD_Shape_templates.hh | 8 ++-- src/Box_defs.hh | 3 +- src/Box_templates.hh | 70 +++++++++++++++++++------------------- src/Octagonal_Shape_templates.hh | 8 ++-- src/Polyhedron_nonpublic.cc | 11 +----- src/Polyhedron_public.cc | 11 +----- src/Polyhedron_templates.hh | 4 +- 7 files changed, 51 insertions(+), 64 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=6b995ed0…

1 0

[GIT] ppl/ppl(devel): Merge branch 'master' into devel.
by Roberto Bagnara 10 Feb '16

10 Feb '16

Module: ppl/ppl Branch: devel Commit: 73e389a07b894ba9404083af4c63060b23b40cb6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=73e389a07b89… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Wed Feb 10 21:10:26 2016 +0100 Merge branch 'master' into devel. ---

1 0

[GIT] ppl/ppl(devel): Avoid overriding LD_LIBRARY_PATH; use libtool instead .
by Roberto Bagnara 10 Feb '16

10 Feb '16

Module: ppl/ppl Branch: devel Commit: 11f5d7fc82d6f92d135506f02e0ddc5536cbabb0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=11f5d7fc82d6… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Fri Feb 5 17:11:25 2016 +0100 Avoid overriding LD_LIBRARY_PATH; use libtool instead. --- configure.ac | 17 +++++++++++------ m4/Makefile.am | 1 + m4/ac_check_gmp.m4 | 4 ---- m4/ac_use_libtool.m4 | 27 +++++++++++++++++++++++++++ 4 files changed, 39 insertions(+), 10 deletions(-) diff --git a/configure.ac b/configure.ac index 23f227b..576f378 100644 --- a/configure.ac +++ b/configure.ac @@ -851,6 +851,17 @@ AC_CHECK_TYPES([int_fast16_t,int_fast32_t,int_fast64_t,uint_fast16_t,uint_fast32 AC_TYPE_UINTPTR_T +# Libtool. +LT_PREREQ([1.5.24]) +LT_INIT([dlopen,win32-dll]) +AM_CONDITIONAL(ENABLE_SHARED, test x"$enable_shared" = xyes) +AM_CONDITIONAL(ENABLE_STATIC, test x"$enable_static" = xyes) + + +# Make sure libtool is used for linking. +AC_USE_LIBTOOL + + # Checks on the GMP library. AC_CHECK_GMP @@ -1490,12 +1501,6 @@ quick) esac AM_CONDITIONAL(THOROUGH_MAKE_CHECK, test x"$enableval" = xthorough) -# Libtool. -LT_PREREQ([1.5.24]) -LT_INIT([dlopen,win32-dll]) -AM_CONDITIONAL(ENABLE_SHARED, test x"$enable_shared" = xyes) -AM_CONDITIONAL(ENABLE_STATIC, test x"$enable_static" = xyes) - # Checks for md5sum. AC_CHECK_PROG(MD5SUM, md5sum, md5sum) AM_CONDITIONAL(HAVE_MD5SUM, test x$MD5SUM = xmd5sum) diff --git a/m4/Makefile.am b/m4/Makefile.am index 2c955b0..ac17ea7 100644 --- a/m4/Makefile.am +++ b/m4/Makefile.am @@ -50,6 +50,7 @@ ac_prog_java.m4 \ ac_prog_javac.m4 \ ac_prog_javah.m4 \ ac_text_md5sum.m4 \ +ac_use_libtool.m4 \ libtool.m4 \ ltoptions.m4 \ ltsugar.m4 \ diff --git a/m4/ac_check_gmp.m4 b/m4/ac_check_gmp.m4 index 7e5e005..a424532 100644 --- a/m4/ac_check_gmp.m4 +++ b/m4/ac_check_gmp.m4 @@ -81,9 +81,6 @@ ac_save_CPPFLAGS="$CPPFLAGS" CPPFLAGS="$CPPFLAGS $gmp_include_options" ac_save_LIBS="$LIBS" LIBS="$LIBS $gmp_library_options" -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++) @@ -224,7 +221,6 @@ AC_DEFINE_UNQUOTED(PPL_GMP_SUPPORTS_EXCEPTIONS, $value, fi AC_LANG_POP(C++) -eval $shared_library_path_env_var=\"$ac_save_shared_library_path\" LIBS="$ac_save_LIBS" CPPFLAGS="$ac_save_CPPFLAGS" diff --git a/m4/ac_use_libtool.m4 b/m4/ac_use_libtool.m4 new file mode 100644 index 0000000..bc13e24 --- /dev/null +++ b/m4/ac_use_libtool.m4 @@ -0,0 +1,27 @@ +# Public macros for the TeX Live (TL) tree. +# Copyright (C) 1995-2009 Karl Berry <tex-live(a)tug.org> +# Copyright (C) 2009-2012 Peter Breitenlohner <tex-live(a)tug.org> +# +# This file is free software; the copyright holders +# give unlimited permission to copy and/or distribute it, +# with or without modifications, as long as this notice is preserved. + + +# Use libtool for linking. This allows testing properties of libraries +# that can be either (1) uninstalled libtool libraries already built +# when this configure runs, or (2) installed libraries -- libtool or not. + +AC_DEFUN([AC_USE_LIBTOOL], +[## $0: Generate a libtool script for use in configure tests +AC_PROVIDE_IFELSE([LT_INIT], , + [m4_fatal([$0: requires libtool])])[]dnl +LT_OUTPUT +m4_append([AC_LANG(C)], +[ac_link="./libtool --mode=link --tag=CC $ac_link" +])[]dnl +AC_PROVIDE_IFELSE([AC_PROG_CXX], +[m4_append([AC_LANG(C++)], +[ac_link="./libtool --mode=link --tag=CXX $ac_link" +])])[]dnl +AC_LANG(_AC_LANG)[]dnl +]) # AC_USE_LIBTOOL

1 0

[GIT] ppl/ppl(devel): Mentioned the improvement in the polyhedra conversion algorithm.
by Enea Zaffanella 10 Feb '16

10 Feb '16

Module: ppl/ppl Branch: devel Commit: e1d8ae6dff428bd849b8fe3b0adc7d40e9e0891f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e1d8ae6dff42… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Feb 10 09:49:57 2016 +0100 Mentioned the improvement in the polyhedra conversion algorithm. --- NEWS | 5 ++++- 1 files changed, 4 insertions(+), 1 deletions(-) diff --git a/NEWS b/NEWS index bee0c90..49ff56f 100644 --- a/NEWS +++ b/NEWS @@ -15,8 +15,11 @@ NEWS for version 1.2 (released date to be decided) New and Changed Features ======================== -o TO BE WRITTEN +o Improved the efficiency of the conversion procedure for polyhedra + by adding a quick adjacency check. +o In the Java language interface, throw an exception when trying + to build a disequality Constraint. Bugfixes

1 0

[GIT] ppl/ppl(devel): Be more consistent in the usage of PPL_DIRTY_TEMP macros.
by Enea Zaffanella 10 Feb '16

10 Feb '16

Module: ppl/ppl Branch: devel Commit: 6b995ed0383990716171272238c550a02889fc13 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6b995ed03839… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Feb 10 09:47:40 2016 +0100 Be more consistent in the usage of PPL_DIRTY_TEMP macros. Got rid of a couple of FIXME's. --- src/BD_Shape_templates.hh | 8 ++-- src/Box_defs.hh | 3 +- src/Box_templates.hh | 70 +++++++++++++++++++------------------- src/Octagonal_Shape_templates.hh | 8 ++-- src/Polyhedron_nonpublic.cc | 11 +----- src/Polyhedron_public.cc | 11 +----- src/Polyhedron_templates.hh | 4 +- 7 files changed, 51 insertions(+), 64 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=6b995ed0…

1 0

[GIT] ppl/ppl(master): Avoid overriding LD_LIBRARY_PATH; use libtool instead.
by Roberto Bagnara 05 Feb '16

05 Feb '16

Module: ppl/ppl Branch: master Commit: 11f5d7fc82d6f92d135506f02e0ddc5536cbabb0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=11f5d7fc82d6… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Fri Feb 5 17:11:25 2016 +0100 Avoid overriding LD_LIBRARY_PATH; use libtool instead. --- configure.ac | 17 +++++++++++------ m4/Makefile.am | 1 + m4/ac_check_gmp.m4 | 4 ---- m4/ac_use_libtool.m4 | 27 +++++++++++++++++++++++++++ 4 files changed, 39 insertions(+), 10 deletions(-) diff --git a/configure.ac b/configure.ac index 23f227b..576f378 100644 --- a/configure.ac +++ b/configure.ac @@ -851,6 +851,17 @@ AC_CHECK_TYPES([int_fast16_t,int_fast32_t,int_fast64_t,uint_fast16_t,uint_fast32 AC_TYPE_UINTPTR_T +# Libtool. +LT_PREREQ([1.5.24]) +LT_INIT([dlopen,win32-dll]) +AM_CONDITIONAL(ENABLE_SHARED, test x"$enable_shared" = xyes) +AM_CONDITIONAL(ENABLE_STATIC, test x"$enable_static" = xyes) + + +# Make sure libtool is used for linking. +AC_USE_LIBTOOL + + # Checks on the GMP library. AC_CHECK_GMP @@ -1490,12 +1501,6 @@ quick) esac AM_CONDITIONAL(THOROUGH_MAKE_CHECK, test x"$enableval" = xthorough) -# Libtool. -LT_PREREQ([1.5.24]) -LT_INIT([dlopen,win32-dll]) -AM_CONDITIONAL(ENABLE_SHARED, test x"$enable_shared" = xyes) -AM_CONDITIONAL(ENABLE_STATIC, test x"$enable_static" = xyes) - # Checks for md5sum. AC_CHECK_PROG(MD5SUM, md5sum, md5sum) AM_CONDITIONAL(HAVE_MD5SUM, test x$MD5SUM = xmd5sum) diff --git a/m4/Makefile.am b/m4/Makefile.am index 2c955b0..ac17ea7 100644 --- a/m4/Makefile.am +++ b/m4/Makefile.am @@ -50,6 +50,7 @@ ac_prog_java.m4 \ ac_prog_javac.m4 \ ac_prog_javah.m4 \ ac_text_md5sum.m4 \ +ac_use_libtool.m4 \ libtool.m4 \ ltoptions.m4 \ ltsugar.m4 \ diff --git a/m4/ac_check_gmp.m4 b/m4/ac_check_gmp.m4 index 7e5e005..a424532 100644 --- a/m4/ac_check_gmp.m4 +++ b/m4/ac_check_gmp.m4 @@ -81,9 +81,6 @@ ac_save_CPPFLAGS="$CPPFLAGS" CPPFLAGS="$CPPFLAGS $gmp_include_options" ac_save_LIBS="$LIBS" LIBS="$LIBS $gmp_library_options" -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++) @@ -224,7 +221,6 @@ AC_DEFINE_UNQUOTED(PPL_GMP_SUPPORTS_EXCEPTIONS, $value, fi AC_LANG_POP(C++) -eval $shared_library_path_env_var=\"$ac_save_shared_library_path\" LIBS="$ac_save_LIBS" CPPFLAGS="$ac_save_CPPFLAGS" diff --git a/m4/ac_use_libtool.m4 b/m4/ac_use_libtool.m4 new file mode 100644 index 0000000..bc13e24 --- /dev/null +++ b/m4/ac_use_libtool.m4 @@ -0,0 +1,27 @@ +# Public macros for the TeX Live (TL) tree. +# Copyright (C) 1995-2009 Karl Berry <tex-live(a)tug.org> +# Copyright (C) 2009-2012 Peter Breitenlohner <tex-live(a)tug.org> +# +# This file is free software; the copyright holders +# give unlimited permission to copy and/or distribute it, +# with or without modifications, as long as this notice is preserved. + + +# Use libtool for linking. This allows testing properties of libraries +# that can be either (1) uninstalled libtool libraries already built +# when this configure runs, or (2) installed libraries -- libtool or not. + +AC_DEFUN([AC_USE_LIBTOOL], +[## $0: Generate a libtool script for use in configure tests +AC_PROVIDE_IFELSE([LT_INIT], , + [m4_fatal([$0: requires libtool])])[]dnl +LT_OUTPUT +m4_append([AC_LANG(C)], +[ac_link="./libtool --mode=link --tag=CC $ac_link" +])[]dnl +AC_PROVIDE_IFELSE([AC_PROG_CXX], +[m4_append([AC_LANG(C++)], +[ac_link="./libtool --mode=link --tag=CXX $ac_link" +])])[]dnl +AC_LANG(_AC_LANG)[]dnl +]) # AC_USE_LIBTOOL

1 0

Implementation of convex hull for C_Polyhedron using only constraints
by Tushar Sharma 30 Jan '16

30 Jan '16

Hi all, I am using C_Polyhedron to perform abstract interpretation. The polyhedrons I am dealing with take a lot of time to perform convex hull. The convex hull spends a lot of time in add_and_minimize operation. I was wondering if there is an alternate implementation in PPL 1.1 (or some other unstable version), that performs hull operation using CLP so that I can compare the two implementations. Thanks, Tushar Sharma Graduate Student Computer Sciences University of Wisconsin-Madison

2 1

Octagon Closure on Half Matrix Form
by Markus Kusano 26 Jan '16

26 Jan '16

Hello, After reading a few of the papers on the PPL improvments to the Octagon domain, I have a question on reasoning about the equivalence between the half-matrix and full-matrix strong closure algorithms. Looking at the function `strong_closure_assign()` in `Octagonal_Shape_templates.hh` my understanding is that it computes the strong closure on the triangular (half) matrix twice. So, for each of the k = 0..n steps it visits each cell in the half-matrix twice which is the same as, in the full matrix, visiting each cell and its coherent-cell. Is my understanding correct? I am trying to reason about parallelizing some of the Octagon algorithms. Thanks a bunch, Markus

2 2

[GIT] ppl/ppl(master): New commits
by Roberto Bagnara 21 Jan '16

21 Jan '16

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5525b05b000c… Merge: cc65f4c19ad8d6e8005e76605c4dd8f62679c0eb 1a50eab30f191ed0fd9963d4e90a2753d715a6be Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Jan 3 15:08:56 2016 +0100 Merge branch 'master' into devel. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cc65f4c19ad8… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 26 12:31:01 2015 +0100 Avoid a memory leak due to the global list of dirty temporaries. The memory leak was not causing a real problem, in that the list of dirty temporaries is meant to survive up to the end of the process. However, it could cause a problem if/when the library is extended to become multi-thread safe, since in such a scenario it is meaningful to have a list of dirty temporaries for each thread (to be released on thread exit). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=34499fe65376… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 26 12:18:30 2015 +0100 Avoid a couple of memory leaks in the C interface tests. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=44ae5b13d058… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 26 11:54:30 2015 +0100 Get rid of temporary print previously added for debugging purposes. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=55f9787ca9c5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Nov 23 13:05:31 2015 +0100 Implemented the quick adjacency check in the conversion procedure. The test allows for significant performce improvements on certain classes of polyhedra (e.g., hypercubes) in that it saves many saturation subset checks. Added preprocessing flags to allow for enabling/disabling the new check (as well as the old quick non-adjacency check). Added new testcase tests/Polyhedron/hypercubes.cc that can be used for a performance comparison. The efficiency benefits can also be appreciated when running the ppl_lcdd demo testsuite. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f45c2558c69e… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 16:42:50 2015 +0100 In Java, throw an exception when trying to build a disequality. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=673343a9e22e… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 12:44:41 2015 +0100 Mention fixed bug. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e7cc92527494… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 12:36:02 2015 +0100 Provide a common, correct implementation for the methods Pointset_Powerset<PSET>::relation_with() working on Constraint and Congruence objects. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bbf24268be1c… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 12:34:48 2015 +0100 Corrected expected result for test02(). The test shows a bug in current implementation of method Pointset_Powerset<PSET>::relation_with(const Congruence& c) const URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=93b1fe4d63f7… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 12:08:43 2015 +0100 Fixed bug in Pointset_Powerset::relation_with(const Constraint&) const. The bug was causing wrong results for relations strictly_intersects() and saturates() on some inputs. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fd92d113b4b3… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Nov 19 11:57:02 2015 +0100 Corrected expected result for test06(). Added a new testcase as test11(). The two tests show a bug in current implementation of method Pointset_Powerset<PSET>::relation_with(const Constraint& c) const

1 0