- PPL-devel - BUGSENG Mailman

Configure errors on Solaris 10
by Marc Girod 10 Mar '13

10 Mar '13

Hello, I get two warnings and on error while configuring ppl-1.0 for Solaris 10, with gcc 3.4.3 My command: ppl-1.0> ./configure --prefix=/vobs/cello/cade_A_tools_utils/ppl --with-gmp=/vobs/cello/cade_A_tools_utils/gmp CFLAGS='-O2 -pedantic -m64 -mptr64 -mcpu=ultrasparc' CC='/usr/sfw/bin/gcc -std=gnu99' The warnings: configure: WARNING: ieeefp.h: present but cannot be compiled configure: WARNING: ieeefp.h: check for missing prerequisite headers? configure: WARNING: ieeefp.h: see the Autoconf documentation configure: WARNING: ieeefp.h: section "Present But Cannot Be Compiled" configure: WARNING: ieeefp.h: proceeding with the compiler's result configure: WARNING: ## ------------------------------------ ## configure: WARNING: ## Report this to ppl-devel(a)cs.unipr.it ## configure: WARNING: ## ------------------------------------ ## configure: WARNING: getopt.h: present but cannot be compiled configure: WARNING: getopt.h: check for missing prerequisite headers? configure: WARNING: getopt.h: see the Autoconf documentation configure: WARNING: getopt.h: section "Present But Cannot Be Compiled" configure: WARNING: getopt.h: proceeding with the compiler's result configure: WARNING: ## ------------------------------------ ## configure: WARNING: ## Report this to ppl-devel(a)cs.unipr.it ## configure: WARNING: ## ------------------------------------ ## The error: checking for the GMP library version 4.1.3 or above... no configure: error: Cannot find GMP version 4.1.3 or higher. I assume the two headers are the ones in /usr/include, and part of: ppl-1.0> pkginfo -l SUNWhea PKGINST: SUNWhea NAME: SunOS Header Files CATEGORY: system ARCH: sparc VERSION: 11.10.0,REV=2005.01.21.15.53 BASEDIR: / VENDOR: Oracle Corporation DESC: SunOS C/C++ header files for general development of software PSTAMP: on10-patch20120806013413 INSTDATE: Aug 25 2012 11:34 HOTLINE: Please contact your local service provider STATUS: completely installed FILES: 1623 installed pathnames 43 shared pathnames 128 directories 22681 blocks used (approx) GMP I just installed and it is 5.1.1 gmp-5.1.1> ll /vobs/cello/cade_A_tools_utils/gmp/lib total 3102 drwxrwxr-x 2 emagiro ossdes 154 Mar 4 19:02 . drwxrwxr-x 5 emagiro ossdes 75 Mar 4 19:02 .. -r--r--r-- 1 emagiro ossdes 1040202 Mar 4 18:49 libgmp.a -r-xr-xr-x 1 emagiro ossdes 938 Mar 4 18:49 libgmp.la lr-xr-xr-x 1 emagiro ossdes 16 Mar 4 19:02 libgmp.so -> libgmp.so.10.1.1 lr-xr-xr-x 1 emagiro ossdes 16 Mar 4 19:02 libgmp.so.10 -> libgmp.so.10.1.1 -r-xr-xr-x 1 emagiro ossdes 544608 Mar 4 18:49 libgmp.so.10.1.1 I attache my config.log Thanks, Marc

2 3

[GIT] ppl/ppl(master): Fixed constructor from a different partially reduced product element.
by Enea Zaffanella 03 Mar '13

03 Mar '13

Module: ppl/ppl Branch: master Commit: eaac930eb9a08b129381fc9cf96d6cfa45f57d6a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eaac930eb9a0… Author: Enea Zaffanella <enea.zaffanella(a)bugseng.com> Date: Sun Mar 3 16:03:15 2013 +0100 Fixed constructor from a different partially reduced product element. --- src/Partially_Reduced_Product_inlines.hh | 5 +---- 1 files changed, 1 insertions(+), 4 deletions(-) diff --git a/src/Partially_Reduced_Product_inlines.hh b/src/Partially_Reduced_Product_inlines.hh index 591fbba..378b5a7 100644 --- a/src/Partially_Reduced_Product_inlines.hh +++ b/src/Partially_Reduced_Product_inlines.hh @@ -156,14 +156,11 @@ inline Partially_Reduced_Product<D1, D2, R> ::Partially_Reduced_Product(const Partially_Reduced_Product<E1, E2, S>& y, Complexity_Class complexity) - : d1(y.space_dimension()), d2(y.space_dimension()) { + : d1(y.space_dimension()), d2(y.space_dimension()), reduced(false) { Partially_Reduced_Product<D1, D2, R> pg1(y.domain1(), complexity); Partially_Reduced_Product<D1, D2, R> pg2(y.domain2(), complexity); pg1.intersection_assign(pg2); m_swap(pg1); - /* Even if y is reduced, the built product may not be reduced as - the reduction method may have changed (i.e., S != R). */ - clear_reduced_flag(); } template <typename D1, typename D2, typename R>

1 0

[GIT] ppl/ppl(master): Fix indentation.
by Enea Zaffanella 03 Mar '13

03 Mar '13

Module: ppl/ppl Branch: master Commit: 87f09547a592229bfbd7722103f8e64ef074fb92 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=87f09547a592… Author: Enea Zaffanella <enea.zaffanella(a)bugseng.com> Date: Sun Mar 3 15:43:46 2013 +0100 Fix indentation. --- src/Bit_Matrix.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Bit_Matrix.cc b/src/Bit_Matrix.cc index 4b4235f..85eedf0 100644 --- a/src/Bit_Matrix.cc +++ b/src/Bit_Matrix.cc @@ -124,7 +124,7 @@ PPL::Bit_Matrix::transpose_assign(const Bit_Matrix& y) { void PPL::Bit_Matrix::resize(dimension_type new_n_rows, - dimension_type new_n_columns) { + dimension_type new_n_columns) { PPL_ASSERT(OK()); const dimension_type old_num_rows = num_rows(); if (new_n_columns < row_size) {

1 0

[GIT] ppl/ppl(master): Activate a couple of tests that were ignored.
by Enea Zaffanella 03 Mar '13

03 Mar '13

Module: ppl/ppl Branch: master Commit: 464f7b65bde5166d2ac665289389f2b0c92a1c54 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=464f7b65bde5… Author: Enea Zaffanella <enea.zaffanella(a)bugseng.com> Date: Sun Mar 3 15:42:56 2013 +0100 Activate a couple of tests that were ignored. --- tests/Box/refinewithcongruences1.cc | 14 +++++++------- 1 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/Box/refinewithcongruences1.cc b/tests/Box/refinewithcongruences1.cc index e94e270..3f4a8d0 100644 --- a/tests/Box/refinewithcongruences1.cc +++ b/tests/Box/refinewithcongruences1.cc @@ -122,7 +122,8 @@ test05() { cgs.insert(B %= 0); cgs.insert(C %= 7); - TBox box(cgs); + TBox box(3); + box.refine_with_congruences(cgs); TBox box1(box.congruences()); @@ -147,16 +148,13 @@ test06() { Congruence_System cgs; cgs.insert((A %= 7) / 0); cgs.insert((B %= 3) / 0); - // This inconsistent equality is ignored when congruences - // are added to the box. cgs.insert((A + B %= 0) / 0); cgs.insert(C %= 7); - TBox box(cgs); + TBox box(3); + box.refine_with_congruences(cgs); - Rational_Box known_result(3); - known_result.add_constraint(A == 7); - known_result.add_constraint(B == 3); + Rational_Box known_result(3, EMPTY); bool ok = check_result(box, known_result); @@ -376,6 +374,8 @@ BEGIN_MAIN DO_TEST(test02); DO_TEST(test03); DO_TEST(test04); + DO_TEST(test05); + DO_TEST(test06); DO_TEST(test07); DO_TEST(test08); DO_TEST(test09);

1 0

[GIT] ppl/ppl(master): Complete application of systematic file header renaming.
by Enea Zaffanella 27 Feb '13

27 Feb '13

Module: ppl/ppl Branch: master Commit: ad11ba0a2159d9e4ee938dc12fcb12994d3471f7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ad11ba0a2159… Author: Enea Zaffanella <enea.zaffanella(a)bugseng.com> Date: Wed Feb 27 15:28:02 2013 +0100 Complete application of systematic file header renaming. --- README | 658 +++++++++++++++--------------- STANDARDS | 16 +- doc/devref.doxyconf-html.in | 8 +- doc/devref.doxyconf-latex.in | 8 +- src/Any_Pointset_defs.hh | 2 +- tests/Concrete_Expression/C_Expr_defs.hh | 2 +- 6 files changed, 347 insertions(+), 347 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=ad11ba0a…

1 0

On the performance and expressiveness of the PPL java bindings
by Gianluca Amato 27 Feb '13

27 Feb '13

Hi all, I am using the PPL library from Java (hmm.. Scala, actually) to make experiments on abstract interpretation based static analysis. I would like to share some considerations about a couple of aspects of the Java bindings which I believe could be improved. First aspect is performance. Obviously, using native libraries in the JVM always incurs a certain amount of performance penalty. I tried to develop a native implementation of Double_Box, and it is much faster than using the Double_Box fron PPL (the native implementation is not safe since I cannot control rounding mode within Java, but I do not think this impacts performance a lot). Obviously for more complex domains the overhead of calling native methods is proportionally lower. My question is: is it possible to improve performance of the Java bindings? I am not an expert in JNI, but from a fast scan of the code, it seems the Java code passes to the native methods an object. The native code calls some accessor function to get the ptr field (which is the pointer to the native PPL object). It should be possible to rewrite the native functions so that they receive directly the pointer, and therefore do not need to call the accessor methods. From what I have heard, calling accessor methods is slow. Has this approach been pursued and abandoned or not? Do you think it could produce a noticeable improvement in performance? The other point regards expressiveness. Java classes in PPL form a flat hierarchy. This makes difficult to write generic code, parametric w.r.t. the abstract domain. In C++ there is a flat hierarchy, too, but there templates may be used to write generic code effectively. In Java, the only choices to write generic code are either to use reflection (which is quite costly) or to write thin wrappers over the PPL classes, and put wrappers in a hierarchy, (which is tedious). Who works in Scala may use macros, but in any case, writing generic code is cumbersome, and the model of a flat hierarchy is against standard Java best-practices. Would it be possible to define an interface which declares all the methods in common between the PPL domains? The domains could implement this interface. This would allow to write generic code by just exploiting the subclass relationship. Sorry for the long mail. I am very interested to know the opinion of the PPL developer and users on this points. Cheers, --gianluca

2 1

Configure error when building on Core 2 Duo CPU
by Frank Murphy 27 Feb '13

27 Feb '13

Hi, I had a problem trying to build PPL with Homebrew on Mac OS X with a Core 2 Duo CPU. I filed a bug with Homebrew here (along with all the output from configure): https://github.com/mxcl/homebrew/issues/17917 The problem is that the `uname -m` command on this CPU returns the string "i386", but the cc compiler from Xcode 4.6 on Mac OS X doesn't accept the argument "-march=i386". Configure tries to do this: configure:6759: cc -c -g -O3 -fomit-frame-pointer -march=i386 conftest.c >&5 error: unknown target CPU 'i386' configure:6759: $? = 1 The result is confusing because configure ends up complaining about not finding the GMP library version 4.1.3 or above. I was able to work around this problem for me by adding "--enable-arch=core2" to the ./configure line, but that's not an ideal solution. Thanks for looking at this, Frank

2 2

Re: [PPL-devel] C++ preprocessor problem when installing ppl
by Roberto Bagnara 16 Feb '13

16 Feb '13

Hello Zhoulai. On 02/15/13 11:24, Zhoulai wrote: > I don't think so. > > bash-3.2$ c++ -v > Using built-in specs. > Target: i686-apple-darwin10 > Configured with: /var/tmp/gcc/gcc-5666.3~6/src/configure --disable-checking --enable-werror --prefix=/usr --mandir=/share/man --enable-languages=c,objc,c++,obj-c++ --program-transform-name=/^[cg][^.-]*$/s/$/-4.2/ --with-slibdir=/usr/lib --build=i686-apple-darwin10 --program-prefix=i686-apple-darwin10- --host=x86_64-apple-darwin10 --target=i686-apple-darwin10 --with-gxx-include-dir=/include/c++/4.2.1 > Thread model: posix > gcc version 4.2.1 (Apple Inc. build 5666) (dot 3) It looks like the experiment you show above has been done with a different PATH from the one that was in effect when you generated the config.log you sent. Look at lines 187 and following: configure:5154: checking for g++ configure:5184: result: no configure:5154: checking for c++ configure:5184: result: no Kind regards, Roberto > On Fri, Feb 15, 2013 at 11:16 AM, Roberto Bagnara <bagnara(a)cs.unipr.it <mailto:bagnara@cs.unipr.it>> wrote: > > On 02/15/13 10:25, Zhoulai wrote: > > Thank you for your help. Could you pls take a look at the zipped config.log pls? Thanks a lot. > > It appears you don't have a C++ compiler installed. > Is that possible? > > > > Do you know how to solve this problem? A quick answer would be most appreciated. The installation of PPL is necessary for my artifacts submission for a conference whose deadline is the 17th. > > > > Can you please send the entire config.log file > > (possibly compressed)? > > > > > p.s > > > the confiig.log has a strange line > > > " configure: 4332: gcc --version >& 5" > > > which is strange because ppl documents say that it suffices to have a gcc later than 4.0.2 > > > > ">&" is a redirection, not a comparison. > > Kind regards, > > > > Roberto > > > -- > Prof. Roberto Bagnara > > Applied Formal Methods Laboratory - University of Parma, Italy > mailto:bagnara@cs.unipr.it <mailto:bagnara@cs.unipr.it> > BUGSENG srl - http://bugseng.com > mailto:roberto.bagnara@bugseng.com <mailto:roberto.bagnara@bugseng.com> > > -- Prof. Roberto Bagnara Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com

2 1

C++ preprocessor problem when installing ppl
by Zhoulai 15 Feb '13

15 Feb '13

Hello, I am trying to install ppl in my ubuntu 12.04. But "./configure" gives me an error, * c++ preprocessor "lib/cpp" fails sanity check* I don't know what to do with it. I have my gcc version 4.7.2, which should be Ok to compile PPL, right? The ubuntu is run on the virtual machine. Do you know how to solve this problem? A quick answer would be most appreciated. The installation of PPL is necessary for my artifacts submission for a conference whose deadline is the 17th. Thank you for your help. Zhoulai (Zell) p.s the confiig.log has a strange line " configure: 4332: gcc --version >& 5" which is strange because ppl documents say that it suffices to have a gcc later than 4.0.2

2 3

Re: [PPL-devel] ppl-1.0 tests fail to build on s390/s390x
by Roberto Bagnara 06 Feb '13

06 Feb '13

Hi Matthias. I just hit the wrong button on the administrative interface of the ppl-devel mailing list. So the message has gone forever before I could read it. Please resend it to the list and accept my apologies. Kind regards, Roberto P.S. This is the failure, right? https://buildd.debian.org/fetch.cgi?pkg=ppl&arch=s390x&ver=1.0-1&stamp=1359… -- Prof. Roberto Bagnara Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com

2 5