IntroductionCiaoPP is the abstract interpretation-based preprocessor of the Ciao multi-paradigm program development environment. CiaoPP can perform a number of program debugging, analysis, and source-to-source transformation tasks on (Ciao) Prolog programs. These tasks include:
- Inference of properties of the predicates and literals of the program, including types, modes and other variable instantiation properties, non-failure, determinacy, bounds on computational cost, bounds on sizes of terms in the program, etc.
- Certain kinds of static debugging and verification, finding errors before running the program. This includes checking how programs call system library predicates and also checking the assertions present in the program or in other modules used by the program. Such assertions represent essentially partial specifications of the program.
- Several kinds of source to source program transformations such as program specialization, slicing, partial evaluation of a program, program parallelization (taking granularity control into account), inclusion of run-time tests for assertions which cannot be checked completely at compile-time, etc.
- The abstract model of the program inferred by the analyzers is used in the system to certify that an untrusted mobile code is safe w.r.t. the given policy (i.e., an abstraction-carrying code approach to mobile code safety).
The information generated by analysis, the assertions in the system specifications are all written in the same assertion language, which is in turn also used by the Ciao system documentation generator, lpdoc.
CiaoPP is distributed under the GNU general public license.
How to use this manual
This is a reference manual. You can use it to look up in it descriptions for the commands, flags, and options that can be used with CiaoPP. The Predicate/Method Definition Index may help you in locating commands. The Regular Type Definition Index may help in locating the definitions of the types associated to the arguments of commands. The Concept Definition Index may help in locating the part of the manual where a particular feature of CiaoPP is described. The Global Index includes all of the above plus references to pages where the command, type, or concept is used (not necessarily defined).
This chapter gives a brief overview of CiaoPP and its capabilities. It assumes some familiarity with the techniques that implement such functionalities. However, references are included to technical papers that explain in detail such techniques. An overview of the functionalities available is given in [BLGPH06] in the form of a tutorial on CiaoPP.
We are in the process of merging all CiaoPP functionality into the 1.2 version. In the meantime, the current distribution is marked as alpha and you may find that some functionality documented in this manual is not available or not working properly. Please bear with us in the meantime. Sorry for any inconvenience.
Currently there are two Ciao distributions, one which includes CiaoPP, and another one which does not. For installing the Ciao distributions which include CiaoPP, it is sufficient to follow the instructions enclosed in the Ciao distribution itself. This describes the installation procedure for the Ciao Development Environment, including libraries and manuals, from a source distribution. This applies primarily to Unix-type systems (Linux, Mac OS X, Solaris, SunOS, etc.), and with some limitations to Windows (using the Cygnus Win32 development libraries).
It is recommended that you read the INSTALLATION file that comes with each component of CiaoDE. However, in many cases it suffices to follow this summary:
Software Requirements (ciaode)
For users of Linux distributions, you should install some software packages required by Ciao that do not come installed by default. Using the corresponding automatic software management tool, those are:
Debian/Ubuntu: sudo apt-get install emacs build-essential \ texi2html texlive texinfo imagemagick Fedora: su yum install gcc kernel-headers kernel-devel emacs texi2html \ texinfo ImageMagick
Some advanced libraries and components, like the cost analysis, require an additional set of software packages:
Debian/Ubuntu: sudo apt-get install libgsl0-dev libgsl0ldbl ant ant-optional \ sun-java6-jdk g++ sudo update-java-alternatives --set java-6-sun
su yum install gsl gsl-devel ant gnu-g++
Debian/Ubuntu users for 64-bit systems would also need libraries for 32-bit compatibility:
sudo apt-get install gcc-multilib libc6-i386 \ libc6-dev-i386 ia32-libs # Optionally, for the Parma Polyhedra Library sudo apt-get install g++-multilib
To install Java JDK on Fedora, please visit Sun Java website (http://java.sun.com/javase/downloads/index.jsp) and follow the installation instructions there.
If you are a Ciao developer, it is highly recommended to install Subversion to access the latest source code in our repositories:
Debian/Ubuntu: sudo apt-get install subversion Fedora: su yum install subversion
Users of other Linux variants or operating systems should use similar tools to add the required software packages. In Windows, doing a full installation of CygWin ensures that you have all the required packages.
Note that the GNU implementation of the make Un*x command is (still) internally used during the installation process. It is available in many systems (including all Linux systems and Mac OS X) simply as make. If any of the installation steps stop right away with make error messages, you probably need to install gmake.
Obtaining the Sources (ciaode)
- If you have obtained your copy of Ciao from a compressed source package, uncompress and unpackage it (using gunzip or bzip2 and tar -xpf). This will put everything in a new directory whose name reflects the Ciao version.
- Other method to get the sources is from the subversion repository (available for ciao developers).
Quick Installation from Source (ciaode)
The main command to build and install CiaoDE, located at the root of the source tree, is called ciaosetup. It provides useful commands to do quick installations from the sources with just one line:
- System-wide installation (e.g. as administrator or root user):
- User-local installation (that will be accessible just for your user)
If you need a more advanced control of configuration read the following section.
Custom Installations (ciaode)
Advanced uses of CiaoDE would require the customization of the default build and installation options. In that case, the installation process usually follows the following steps:
- From the directory where the sources are stored, run:
It will perform a default configuration, where the system will be configured to be installed as the system administrator (root) in a standard directory available for all users in the machine (e.g., /usr/local).
The additional options --instype=local will prepare CiaoDE to run from the sources directly, and configured in the user's home directory (recommended for CiaoDE developers).
In case you want to install elsewhere, or change any of the installation options, you can use a customized configuration procedure. The configure command accepts several options. You can see a brief description of them with:
./ciaosetup configure --help
Use the --menu option to select configuration options interactively. You must follow the instructions that appear on it. When asked for the configuration level, if you are happy with the default options, select the first option and no questions will be made. If you need a higher level of customization, select the last option.
- Once the configuration process has finished, run:
This will build executables and compile libraries.
- If you have obtained the CiaoDE source from the SVN repository, you need to generate the documentation. This can be done using:
- After the compilation completes successfully, run:
This will install everything in the specified directories.
If you want to see the other available commands, run ./ciaosetup help.
A CiaoPP session consists in the preprocessing of a file. The session is governed by a menu, where you can choose the kind of preprocessing you want to be done to your file among several analyses and program transformations available. Clicking on the icon in the buffer containing the file to be preprocessed displays the menu, which will look (depending on the options available in the current CiaoPP version) something like the “Preprocessor Option Browser” shown in the following figure:
Except for the first and last lines, which refer to loading or saving a menu configuration (a predetermined set of selected values for the different menu options), each line corresponds to an option you can select, each having several possible values. You can select either analysis (analyze) or assertion checking (check_assertions) or certificate checking (check_certificate) or program optimization (optimize), and you can later combine the four kinds of preprocessing. The relevant options for the action group selected are then shown, together with the relevant flags. A description of the values for each option will be given as it is used in the corresponding section of this manual.
CiaoPP can help you to analyze your program, in order to infer properties of the predicates and literals in your program (which might be useful in the subsequent steps during the same session). You can use Cost Analysis to infer both lower and upper bounds on the computational time cost and sizes of terms of procedures in a program. Mode Analyses obtain at compile-time accurate variable groundness and sharing information and other variable instantiation properties. Type Analysis infers regular types. Regular types are explained in detail in Declaring regular types. Non-failure and Determinacy Analyses detect procedures and goals that can be guaranteed to not fail and/or to be deterministic.
CiaoPP also can help to optimize your program (by means of source-to-source program transformations), using program specialization, partial evaluation, program parallelization and granularity control, and other program transformations. Specialization can help to simplify your program w.r.t. the analysis information (eliminating dead code, predicates that are guaranteed to either succeed or fail, etc.), specialize it and then simplify it, or just specialize it, i.e., to unfold all versions of the predicates in your program. CiaoPP can also perform automatic parallelization of your source program during precompilation using several annotation algorithms, and granularity control on parallel programs, transforming the program in order to perform run--time granularity control, i.e., deciding parallel or sequential execution of goals depending on the estimated amount of work under them (estimated by cost analysis).
CiaoPP also helps in debugging your programs. It makes possible to perform static debugging, i.e., finding errors at compile-time, before running the program, and also dynamic debugging, in the sense of including run-time tests that will perform the checking for errors at run-time. Static debugging is performed by assertion checking. This includes checking the ways in which programs call the system library predicates and also checking the assertions present in the program or in other modules used by the program. Such assertions essentially represent partial specifications of the program. For dynamic checking, CiaoPP will include run-time tests for the parts of assertions which cannot be checked completely at compile-time.
Using assertions for preprocessing programs, gives an overview on the use of the assertion language in CiaoPP. In that chapter and the following ones, several existing properties that can be used in assertions are described. Programmers can also define their own properties (see the abovementioned chapters).
There are three main levels of interaction with CiaoPP. There is a graphical menu interface, based on the emacs editor, that allows the selection of configuration options and the use of the different features of CiaoPP. If emacs is not available, this menu interface can be used as a text-based menu interface. There are several supplementary predicates for assisting the user and providing a kind of scripting language (based on the Ciao language). This interface is described in The CiaoPP user menu interface.
The second level of interaction with CiaoPP is the low-level interface, detailed in The CiaoPP low-level programming interface. This interface is intended for advanced developers, and contains the primitives used by the abovementioned menu-based interface for implementing the main features of the system.
And finally, the command-line interface allows the use of CiaoPP without direct interaction of the user. With this feature, the CiaoPP system can be integrated into other systems (as for example interactive web sites) by means of batch commands. It is described in The CiaoPP command-line interface.