Awesome

PPLite: convex polyhedra library for Abstract Interpretation

PPLite is an open-source C++ library implementing the abstract domain of convex polyhedra, to be used in tools for static analysis and verification.

<strong>Note:</strong> this public repository also collects previous (non-versioned) releases of the library.

2024-04-11: <a href="releases/pplite-0.12.tar.gz">PPLite 0.12 can be downloaded</a>.

If you need help for using PPLite or have some feature requests, send an email to enea.zaffanella@unipr.it

While being derived from the PPL (Parma Polyhedra Library), PPLite has a very different goal: to provide researchers and students with a lighter framework for experimenting with new ideas and algorithms in the context of polyhedral computations. In particular, PPLite is not aimed at implementing the full range of abstract domains and operators made available by the PPL. The main characteristics of PPLite are the following.

Library development is based on Linux (Ubuntu). The build system uses GNU autotools; the main external dependency is the FLINT library, for arbitrary precision integer and rationals; the library is written in C++ and requires a reasonably recent C++ compiler (tested using g++ and clang++).

Installation of main requirements:

sudo apt-get install make autoconf automake libtool
sudo apt-get install libgmp-dev libmpfr-dev libflint-dev

Out-of-tree builds are strongly recommended: in the following we assume using a source directory named MySources and a build directory named MyBuild; the commands shown should be adapted accordingly.

After cloning the library sources from git, resulting in directory MySources/PPLite, the following command will generate the configuration script (note: this preliminary step is not needed if the sources are extracted from a .tar.gz distribution):

cd MySources/PPLite
autoreconf --install

We then move to the build directory and configure it:

cd MyBuild
../MySources/PPLite/configure

This will use the default configuration options (which can be overridden, see configure --help), meaning that:

• the installation prefix is /usr/local
• the build is for release: optimizations are turned on and assertions are turned off
• dependencies will be searched for in "standard" places

Use option --prefix=INSTALLDIR to change the installation directory. Use option --enable-assertions (and maybe also option --enable-optimization=zero) for a debug build. If you have FLINT installed in a non-standard place the configure script will complain: in that case you can use option --with-flint=DIR or, if needed, the two options --with-flint-include=INCDIR and --with-flint-lib=LIBDIR to specify the location of the header files and the library; similar options are available for MPFR and GMP libraries.

After configuration, the following commands will build the library, run its tests and install it:

cd MyBuild
make -j8
make check -j8
sudo make install

Option -j<N> enables parallel builds using at most N workers; consider removing the sudo prefix from the installation command if it is not really needed. Note that the (static and dynamic) library files will be installed in <prefix>/lib, while the header files will be installed in their own subdirectory <prefix>/include/pplite.

The initial development team was composed by Anna Becchi and Enea Zaffanella. Currently the library is maintained by Enea Zaffanella.

Students collaborate to the development of the library (in a broad sense, which is sometimes different from writing source code), under supervision of Enea Zaffanella, during their internship and/or the activities related to the final exam of the Bachelor and/or Master Degree in Computer Science.

For the list of collaborators, see file CREDITS.