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.

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

Current version (see below for older ones)

2024-04-11: PPLite 0.12 can be downloaded.

Support

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

Goals (and non-goals)

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.

• Both closed and NNC rational convex polyhedra are supported.
• Performance and portability are deemed important, but not the main concern (ease of implementation and readability are given priority).
• The library is written in C++ (currently, c++17).
• The library is meant to be lightweight from the point of view of the developers: the goal is to reduce maintenance costs. This implies, among other things:
  • backward compatibility is a non-goal;
  • documentation is kept minimal (if not omitted altogether);
  • there is no plan to provide foreign language interfaces (but the library can be accessed through Apron, using the C, Java or OCaml bindings);
  • the library typically provides narrow contracts: preconditions on operators are not checked at runtime, so that user errors will lead to undefined behavior (rather than exceptions);
  • encapsulation is not fully enforced: a knowledgeable user can directly change the contents of inner data structures, e.g., to experiment with alternative implementations of domain operators.

Compilation/installation instructions

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.

Main developers

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

Contributors and past members of development team

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.

Available downloads

• 2024-04-11: PPLite 0.12 can be downloaded.
  The library no longer depends on the C++ interface of GMP (this change mainly affects classes `pplite::Integer` and `pplite::Rational`). The support for conditional thread safety is now enabled by default.
• 2023-06-10: PPLite 0.11 can be downloaded.
  While the library is based on the c++17 standard, its header files are now c++11 standard compliant (hence can be used more easily in other projects, e.g., the Apron library wrapper). Added new method Index_Set get_unconstrained() const; to polyhedra domains, returning the set of unconstrained space dimensions.
• 2023-05-29: PPLite 0.10.2 can be downloaded. (No longer maintained: switch to the most recent one.)
  Fixed a bug in the polyhedra simplification procedure. The bug could be triggered when using NNC polyhedra and converting from generator to constraints.
• 2023-03-07: PPLite 0.10.1 can be downloaded. (No longer maintained: switch to the most recent one.)
  Added support for the integral split operator.
• 2023-01-26: PPLite 0.10 can be downloaded. (No longer maintained: switch to the most recent one.)
  Main change: the Apron wrapper is no longer part of the library; it will be integrated into Apron itself.
• 2023-01-02: PPLite 0.9 can be downloaded. (No longer maintained: switch to the most recent one.)
  The finite powerset domain is now a class template: pre-generated instances, also available via Apron interface, include finite sets of boxed polyhedra (P_Set) and finite sets of Cartesian factored boxed polyhedra (FP_Set).
• 2022-11-02: PPLite 0.8 can be downloaded. (No longer maintained: switch to the most recent one.)
  This new version adds a prototype implementation of the finite powerset of Poly elements (PSet). It also provide an efficiency improved version of the F_Poly domain and a couple of bug fixes in the Apron wrapper.
• 2022-08-26: PPLite 0.7.1 can be downloaded. (No longer maintained: don't use it, switch to the most recent one.)
  Note: this version fixes a silly build error; no functionality changes wrt 0.7.
• 2020-11-24: PPLite 0.7 can be downloaded. (No longer maintained: don't use it, switch to the most recent one.)
  New configuration option --enable-apron allows for compiling the wrapper for (the C language bindings of) the Apron interface. This version also adds a C++ polymorphic interface allowing to experiment with several variants of the domain of convex polyhedra: Poly, U_Poly, F_Poly, UF_Poly and their XXX_Stats versions, computing timing information for abstract operators.
• 2020-04-23: PPLite 0.6 can be downloaded. (No longer maintained: don't use it, switch to the most recent one.)
  Added pplite::F_Poly, adding support for factored polyhedra (experimental feature, not optimized).
• 2019-10-15: PPLite 0.5.1 can be downloaded. (No longer maintained: don't use it, switch to the most recent one.)
  This version fixes a bug affecting Poly::parallel_affine_image() in version 0.5 (the bug was affecting computations of affine images when the denominators of the expressions where different from 1).
• 2019-07-12: PPLite 0.5 can be downloaded (No longer maintained: don't use it, switch to the most recent one.)
  Added helper class BBox to encode the (topologically closed, possibly infinite) bounding box of a polyhedron; this is used in new methods Poly::boxed_contains() and Poly::boxed_is_disjoint_from() so as to speed up computation (in particular, in client code computing over sets of polyhedra, as found in tools such as PHAVerLite).
• 2019-03-08: PPLite 0.4.1 can be downloaded (No longer maintained: don't use it, switch to the most recent one.)
  (Note: version 0.4.1 fixes a bug affecting Poly::hash() in version 0.4, which was released on 2019-03-03.) Added new method Poly::hash(), which can be used to quickly decide that two polyhedra are different. Added new method Poly::con_hull_assign(), computing the constraint hull of two polyhedra (note: the result depends on the specific constraint representation computed by the library). Improved the efficiency of the parallel affine image method. Corrected a few, corner case bugs (affected functionalities were: computation of the bhrz03 widening; the removal of space dimensions; the addition of generating lines).
• 2018-10-09: PPLite 0.3 can be downloaded. (No longer maintained: don't use it, switch to the most recent one.)
  Added wrappers on the polyhedra domain: Poly_Stats collects time statistics on abstract operator calls; U_Poly improves the handling of unconstrained space dimensions. Corrected a few bugs: intersection of 0-dim polyhedra; printing of universe polyhedra; minimization of an affine function; a couple of other bugs in code used only in debugging mode.
• 2018-07-10: PPLite 0.2 can be downloaded. (No longer maintained: don't use it, switch to the most recent one.)
  Added support for (conditional) thread safety: it is now possible to develop multithreaded applications using PPLite. Implemented a few other operators on the polyhedra domain, including the more precise bhrz03 widening.
• 2018-05-08: PPLite 0.1 can be downloaded. (No longer maintained: don't use it, switch to the most recent one.)
  Initial release.