West Home

West Team --- SPPoC

SPPoC: Symbolic Parameterized Polyhedral Calculator

What is it all about?

Polyhedral computation tools

• PolyLib
• PIP
• Omega

Applications

All the field of the static analysis of "static control" programs.

Installing SPPoC

Requirements, download area

SPPoC is written in Objective Caml. You will need version 3.00 (or higher) of the Objective Caml compiler [download]. You will also need the companion program camlp4 [download].

As the PolyLib uses the GNU MP library to handle multi-precision arithmetic, you will need to download it as well [download].

You will also need the GNU versions of make and test and gcc v3.3 or higher.

Finally, you can download the source files of SPPoC (current version: 1.2.1 released 2003/11/19): [download (763KB)] (it includes the PolyLib v4.16, the omega library v1.1 and a modified version of PIP).

The development version is available at http://repo.or.cz/w/sppoc.git (thanks to Sven Verdoolaege for setting this up). The main differences from release 1.2.1 are the removal of the polylib and Omega from the tool (you should now use an standard install of those libraries), the adaptation to the new ocaml compiler versions (you need camlp5 to compile).

Optionally you can download and install the ledit line editor that improves the editing facilities of sppoc [download].

Compilation

• Extract the archive: tar xzf spocc.tgz.
• Configure the Makefiles: edit file Etc/Makefile.config to suit your installation.
• You may need to adjust some variables in Polylib/Makefile to compile the PolyLib.
• Compile SPPoC: make (if some problem occur, try make depend followed by make).
• You then have an interactive version of SPPoC: Bin/spocc. You can test this version with the examples from the Test and Calcom directories.
• You can then install SPPoC: make install.

User's Guide

• One way to use SPPoC is the sppoc interactive calculator. Actually it is an ocaml toplevel with the SPPoC module and all the necessary libraries preloaded. The quotations and the pretty-printers are also automatically started. The preloading mechanism installs a .ocamlinit file in the current directory. If such a file already exists, it is not replaced. See the ocaml documentation for more details on this mechanism.
  The sppoc command used alone starts the interactive calculator. If a file is given as an argument, the commands in this file are exectued as a script.
  As sppoc tries to use the ledit line editor if you have it, using sppoc by redirection of its input is not reliable. The right way to interactively execute a file is: start sppoc and type the command #use "file.ml";;.
• You can also use SPPoC as a library. To link an ocaml program with SSPoC, use a command line such as:

  ocaml -o yourprogram -I /path/to/libsppoc libsppoc.cma yourprogram.ml

  or

  ocaml -o yourprogram -pp camlp4sppoc -I /path/to/libsppoc libsppoc.cma yourprogram.ml

  if you want to use the quotations.

In all the cases you have to open the SPPoC module (via the open SPPoC;; statement) to be able to avoid prefixing all the sppoc commands by SPPoC.

TO DO list

• Upgrade to omega 1.2
• Smash the remaining bugs
• Test the native code compilation.
• Update the documentation
• For a future version: handle equalities in QUASTs' predicates

Main Publications

Abstract (in French) and slides of the presentation of SPPoC at the Workshop Compilation et Parallélisation Automatique in St Nabor, October 1999.

The LIFL Research Report 00-04 (in French) describing SPPoC and some applications: "SPPoC : fonctionnement et applications".

SPPoC : manipulation automatique de polyèdres pour la compilation (in French), Technique et Science Informatique, volume 20, n°8, pages 1019--1048, 2001

Copyright © 2000-2008 LIFL.

Oct 10 2008, 14:41.