PPLite 0.11 integration in Apron (C, Java and OCaml bindings)

COPYING

@@ -29,6 +29,10 @@ of the original package are not covered by the License described in this
 file. They are distributed under the GNU General Public License version 2,
 included in the COPYING file contained in those subdirectories.
 
+The files contained in the pplite subdirectory of the original package
+are not covered by the License described in this file. They are distributed
+under the GNU General Public License version 3, included in the COPYING
+file contained in those subdirectories.
 
 ----------------------------------------------------------------------
 

Makefile

@@ -26,6 +26,9 @@ c:
 ifneq ($(HAS_PPL),)
 	(cd ppl; $(MAKE))
 	(cd products; $(MAKE))
+endif
+ifneq ($(HAS_PPLITE),)
+	(cd pplite; $(MAKE))
 endif
 	(cd avoct; $(MAKE) MPQ D)
 ifneq ($(HAS_GLPK),)
@@ -47,6 +50,9 @@ ml:
 ifneq ($(HAS_PPL),)
 	(cd ppl; $(MAKE) ml)
 	(cd products; $(MAKE) ml)
+endif
+ifneq ($(HAS_PPLITE),)
+	(cd pplite; $(MAKE) ml)
 endif
 	(cd avoct; $(MAKE) mlMPQ mlD)
 ifneq ($(HAS_GLPK),)
@@ -61,6 +67,10 @@ apronppltop:
 	$(OCAMLMKTOP) -I $(MLGMPIDL_LIB) -I $(APRON_LIB) -verbose -o $@ \
 	bigarray.cma gmp.cma apron.cma boxMPQ.cma octMPQ.cma polkaMPQ.cma ppl.cma polkaGrid.cma t1pMPQ.cmxa avoMPQ.cma
 
+apronpplitetop:
+	$(OCAMLMKTOP) -I $(MLGMPIDL_LIB) -I $(APRON_LIB) -verbose -o $@ \
+	bigarray.cma gmp.cma apron.cma boxMPQ.cma octMPQ.cma polkaMPQ.cma pplite.cma t1pMPQ.cmxa avoMPQ.cma
+
 apronglpktop:
 	$(OCAMLMKTOP) -I $(MLGMPIDL_LIB) -I $(APRON_LIB) -verbose -o $@ \
 	bigarray.cma gmp.cma apron.cma boxMPQ.cma octMPQ.cma polkaMPQ.cma t1pMPQ.cma avoMPQ.cma fppMPQ.cma
@@ -105,6 +115,12 @@ OCAMLFIND_FILES += \
 	$(patsubst %,products/%, polkaGrid.idl polkaGrid.mli polkaGrid.cmi polkaGrid.cmx) \
 	$(patsubst %,products/%, $(subst xxx,polkaGrid, $(OCAMLFIND_PROTO)))
 endif
+ifneq ($(HAS_PPLITE),)
+OCAMLFIND_FILES += \
+	$(patsubst %,pplite/%, pplite.idl pplite.mli pplite.cmi pplite.cma pplite.cmx $(call OCAMLOPT_TARGETS, pplite) libap_pplite_caml.a libap_pplite_caml_debug.a dllap_pplite_caml.$(EXT_DLL)) \
+	$(patsubst %,products/%, polkaGrid.idl polkaGrid.mli polkaGrid.cmi polkaGrid.cmx) \
+	$(patsubst %,products/%, $(subst xxx,polkaGrid, $(OCAMLFIND_PROTO)))
+endif
 ifneq ($(HAS_GLPK),)
 OCAMLFIND_FILES += \
 	$(patsubst %,fppol/%, fpp.mli fpp.cmi fpp.cmx) \
@@ -123,6 +139,10 @@ ifneq ($(HAS_PPL),)
 OCAMLFIND_FILES += \
 	$(patsubst %,ppl/%, ppl.cmti ppl.cmt) \
 	$(patsubst %,products/%, polkaGrid.cmti polkaGrid.cmt)
+endif
+ifneq ($(HAS_PPLITE),)
+OCAMLFIND_FILES += \
+	$(patsubst %,pplite/%, pplite.cmti pplite.cmt)
 endif
 	$(patsubst %,avoct/%, avo.cmti avo.cmt)
 ifneq ($(HAS_GLPK),)
@@ -142,6 +162,9 @@ install: all
 ifneq ($(HAS_PPL),)
 	(cd ppl; $(MAKE) install)
 	(cd products; $(MAKE) install)
+endif
+ifneq ($(HAS_PPLITE),)
+	(cd pplite; $(MAKE) install)
 endif
 	(cd avoct; $(MAKE) install)
 ifneq ($(HAS_GLPK),)
@@ -155,6 +178,9 @@ ifeq ($(OCAMLFIND),)
 ifneq ($(HAS_PPL),)
 	if test -f apronppltop; then $(INSTALL) apronppltop $(APRON_BIN); fi
 endif
+ifneq ($(HAS_PPLITE),)
+	if test -f apronpplitetop; then $(INSTALL) apronpplitetop $(APRON_BIN); fi
+endif
 ifneq ($(HAS_GLPK),)
 		if test -f apronglpktop; then $(INSTALL) apronglpktop $(APRON_BIN); fi
 endif
@@ -176,10 +202,13 @@ endif
 
 ifneq ($(OCAMLFIND),)
 install: mlapronidl/META
-mlapronidl/META: mlapronidl/META.in mlapronidl/META.ppl.in
+mlapronidl/META: mlapronidl/META.in mlapronidl/META.ppl.in mlapronidl/META.pplite.in
 	$(SED) -e "s!@VERSION@!$(VERSION_STR)!g;" $< > $@;
   ifneq ($(HAS_PPL),)
 	cat mlapronidl/META.ppl.in >> $@;
+  endif
+  ifneq ($(HAS_PPLITE),)
+	cat mlapronidl/META.pplite.in >> $@;
   endif
 	$(SED) -e '/^[[:space:]]*archive(byte)/ { p; s ) ,plugin) ;}' -i.bak $@;
   ifneq ($(HAS_NATIVE_PLUGINS),)
@@ -199,14 +228,15 @@ clean:
 	(cd octagons; $(MAKE) clean)
 	(cd taylor1plus; $(MAKE) clean)
 	(cd ppl; $(MAKE) clean)
+	(cd pplite; $(MAKE) clean)
 	(cd products; $(MAKE) clean)
 	(cd avoct; $(MAKE) clean)
 	(cd fppol; $(MAKE) clean) 
 	(cd apronxx; $(MAKE) clean)
 	(cd examples; $(MAKE) clean)
 	(cd test; $(MAKE) clean)
 	(cd japron; $(MAKE) clean)
-	rm -fr online tmp apron*run aprontop apronppltop apronglpktop
+	rm -fr online tmp apron*run aprontop apronppltop apronpplitetop apronglpktop
 	rm -f mlapronidl/META
 
 distclean: clean
@@ -223,6 +253,7 @@ uninstall:
 	(cd taylor1plus; $(MAKE) uninstall)
 	(cd examples; $(MAKE) uninstall)
 	(cd ppl; $(MAKE) uninstall)
+	(cd pplite; $(MAKE) uninstall)
 	(cd products; $(MAKE) uninstall)
 	(cd avoct; $(MAKE) uninstall)
 	(cd fppol; $(MAKE) uninstall) 
@@ -249,7 +280,7 @@ endif
 
 PKG  = $(PKGNAME)-$(VERSION_STR)
 PKGFILES = Makefile README README.windows README.mac AUTHORS COPYING Makefile.config.model Changes configure vars.mk ocamlpack
-PKGDIRS  = apron num itv octagons box newpolka taylor1plus ppl products avoct fppol mlapronidl examples test apronxx japron
+PKGDIRS  = apron num itv octagons box newpolka taylor1plus ppl pplite products avoct fppol mlapronidl examples test apronxx japron
 
 dist:
 	$(MAKE) all

Makefile.config.model

@@ -21,6 +21,10 @@ HAS_OCAMLOPT = 1
 
 # HAS_PPL = 1
 
+# If defined to non-empty value, enable domains from the PPLite library
+
+# HAS_PPLITE = 1
+
 # If defined to non-empty value, compiles the fppol domain
 # (The fppol domain requires GLPK)
 
@@ -68,6 +72,14 @@ MPFR_PREFIX = /usr
 #
 PPL_PREFIX = /usr
 
+# Where to find FLINT ($(FLINT_PREFIX)/include, ($FLINT_PREFIX)/lib
+# (only required by PPLite)
+FLINT_PREFIX = /usr
+
+# Where to find PPLITE ($(PPLITE_PREFIX)/include, $(PPLITE_PREFIX)/lib
+#
+PPLITE_PREFIX = /usr
+
 # Where to find GLPK ($(GLPK_PREFIX)/include, $(GLPK_PREFIX)/lib
 #
 GLPK_PREFIX = /usr
@@ -159,6 +171,12 @@ CXXFLAGS_DEBUG = \
 -Wno-unused -Wno-unused-parameter -Wno-unused-function \
 -fPIC -g -O0 -UNDEBUG
 
+# The PPLite wrapper requires using the C++11 language standard
+# (note: building PPLite from sources requires the C++17 language standard)
+PPLITE_CXXFLAGS = -std=c++11 $CXXFLAGS
+PPLITE_CXXFLAGS_DEBUG = -std=c++11 $CXXFLAGS_DEBUG
+
+
 AR = ar
 RANLIB = ranlib
 SED = sed

README.md

@@ -21,7 +21,7 @@ Apron includes the following numeric domains:
 * octagons
 * zonotopes (taylor1plus)
 
-Additional domains are made available through the optional PPL third-party library:
+Additional domains are made available through the optional PPL and PPLite third-party libraries:
 * alternate polyhedra implementation
 * grids
 * reduced products of polyhedra and grids
@@ -50,6 +50,14 @@ Compiling the built-in domains with the C interface requires:
 
 Compiling the PPL-based domains requires the [Parma Polyhedra Library](http://bugseng.com/products/ppl) (tested with version 1.2) and gcc (no clang).
 
+Compiling the PPLite-based domains requires the
+[PPLite library](https://github.com/ezaffanella/PPLite),
+which also depends on Flint.
+Note that building the PPLite library from sources requires using a
+C++ compiler (g++ or clang++) that supports the c++17 language standard;
+however, starting from PPLite version 0.11, the Apron wrapper for PPLite
+can be compiled using a C++ compiler supporting the c++11 language standard.
+
 
 ### Additional language support
 
@@ -91,6 +99,7 @@ In case some components fail to compile, it is possible to disable them through
 * `-no-java` to disable the Java API (there are known problems where the compilation fails to find `jni.h` )
 * `-no-ocaml` to disable the OCaml API
 * `-no-ppl` to disable the PPL domains
+* `-no-pplite` to disable the PPLite domains
 
 See `./configure -help` for more options.
 

apron/Makefile

@@ -71,7 +71,7 @@ dist: $(H_FILES) $(C_FILES) $(CH_FILES_AUX) apron.texi Makefile COPYING README a
 	(cd ..; tar zcvf apron.tgz $(^:%=apron/%))
 
 clean:
-	/bin/rm -f *.aux *.bbl *.blg *.dvi *.log *.toc *.ps *.pdf apron.cps apron.fns apron.info apron.fn apron.ky apron.pg apron.cp apron.tp apron.vr apron.kys apron.pgs apron.tps apron.vrs newpolka.texi box.texi ap_ppl.texi ap_pkgrid.texi apron.info* depend ap_version.h
+	/bin/rm -f *.aux *.bbl *.blg *.dvi *.log *.toc *.ps *.pdf apron.cps apron.fns apron.info apron.fn apron.ky apron.pg apron.cp apron.tp apron.vr apron.kys apron.pgs apron.tps apron.vrs newpolka.texi box.texi ap_ppl.texi ap_pplite.texi ap_pkgrid.texi apron.info* depend ap_version.h
 	/bin/rm -f *.o *.a *.cmi *.cmo *.cmx *.cmx[as] *.cma *.$(EXT_DLL)
 	/bin/rm -fr html
 	/bin/rm -f apron.pdf rationale.pdf
@@ -101,19 +101,21 @@ ap_pkgrid.texi: ../products/ap_pkgrid.texi
 	ln -sf $< $@
 ap_ppl.texi: ../ppl/ap_ppl.texi
 	ln -sf $< $@
+ap_pplite.texi: ../pplite/ap_pplite.texi
+	ln -sf $< $@
 newpolka.texi: ../newpolka/newpolka.texi
 	ln -sf $< $@
 box.texi: ../box/box.texi
 	ln -sf $< $@
 
-apron.pdf: apron.texi rationale.texi ../products/ap_pkgrid.texi ../ppl/ap_ppl.texi ../newpolka/newpolka.texi ../box/box.texi 
+apron.pdf: apron.texi rationale.texi ../products/ap_pkgrid.texi ../ppl/ap_ppl.texi ../pplite/ap_pplite.texi ../newpolka/newpolka.texi ../box/box.texi 
 	$(TEXI2ANY) --pdf -o $@ $<
 
-apron.info: apron.texi rationale.texi ap_pkgrid.texi ap_ppl.texi newpolka.texi box.texi
+apron.info: apron.texi rationale.texi ap_pkgrid.texi ap_ppl.texi ap_pplite.texi newpolka.texi box.texi
 	$(MAKEINFO) -o $@ $<
 
 
-html: apron.texi rationale.texi ap_pkgrid.texi ap_ppl.texi newpolka.texi box.texi 
+html: apron.texi rationale.texi ap_pkgrid.texi ap_ppl.texi ap_pplite.texi newpolka.texi box.texi 
 	$(TEXI2ANY) -o html --html --split=section --no-number-sections $<
 	cp -f ../octagons/oct_doc.html html
 	cp -f ../examples/*.c ../examples/*.ml html

apron/apron.texi

@@ -277,6 +277,22 @@ need to use @samp{g++} instead of @samp{gcc} for linking. You also
 need the C++ layer on top of GMP (@file{libgmpxx.a}). The
 @file{libap_ppl.a} library contains the layer on top of PPL which
 implements the APRON interface.
+
+@item
+If a C file @file{test.c} uses the PPLite library via APRON,
+the compilation command should look like @samp{g++ -I$ITV/include
+-I$MPFR/include -I$GMP/include -I$APRON/include -I$PPLITE/include
+-I$FLINT/include -L$ITV/lib -L$MPFR/lib -L$GMP/lib -L$APRON/lib
+-L$PPLITE/lib -L$FLINT/lib -o test test.c
+-lap_pplite -lpplite -lflint -lgmpxx -lapron -lmpfr -lgmp},
+assuming that PPLite resides in $PPLITE and PPLite APRON interface in
+@file{$APRON/include} and @file{$APRON/lib} directories.
+
+Notice that the PPLite library (@file{libpplite.a}) is a C++ library,
+you need to use @samp{g++} instead of @samp{gcc} for linking.
+You also need the C++ layer on top of GMP (@file{libgmpxx.a}).
+The @file{libap_pplite.a} library contains the layer on top of PPLite
+which implements the APRON interface.
 @end enumerate
 You should look at the specific documentation of the libraries for
 more details.
@@ -615,6 +631,7 @@ Managers are allocated by the underlying libraries/abstract domains, but are fre
 * NewPolka::
 * PPL::
 * pkgrid::
+* PPLite::
 @end menu
 
 @c ===================================================================
@@ -874,6 +891,13 @@ raised one.
 
 @include ap_pkgrid.texi
 
+@c ===================================================================
+@node PPLite, Managers and Abstract Domains
+@section PPLite (@file{ap_pplite.h}): convex polyhedra abstract domains
+@c ===================================================================
+
+@include ap_pplite.texi
+
 @c *******************************************************************
 @node Scalars & Intervals & Coefficients, Level 1 of the interface, Managers and Abstract Domains, Top
 @chapter Scalars & Intervals & coefficients