PAGAI static analyser

The PAGAI tool

PAGAI stands for "Path Analysis for invariant Generation by Abstract Interpretation".

Contributors

Julien Henry, David Monniaux, Matthieu Moy

Contact: <First Name> DOT <Last Name> AT imag.fr

Related papers

Download

Get Binary

A self-contained binary is available for Linux and MacOS:

Install from source

The code is freely available. You can clone the latest version of the code on the git repository :

git clone http://forge.imag.fr/anonscm/git/pagai/pagai.git

After cloning the repository, run autoinstall.sh to install all PAGAI dependencies and then PAGAI itself. Installation may take a while, since there are several external dependencies to compile (LLVM, Cudd, Apron, ...). Please report if the installation fails.

If you wish to use z3, CVC4, mathsat or smtinterpol as SMT-solvers, make sure their binaries are in your $PATH before running PAGAI.

You should also install Clang to be able to generate LLVM bitcode from C programs.

Usage

PAGAI takes as input LLVM bitcode. Bitcode can be obtained from C programs using Clang. To compile a C file into LLVM bitcode, you can run the script located in the scripts directory of the Git repository

./scripts/compile_llvm.sh -h

In order to have a nicer PAGAI output, you have to compile your C code with debug infos (option "-g").

Example

How to analyse the following C program :
~$ more gopan.c
#include "../pagai_assert.h"
int main() {
	int x = 0;
	int y = 0;
	while (1) {
		if (x <= 50)  {
			y++;
		} else y--;
		if (y < 0) break;
		x++;
	}
	assert(x+y<=101);
	assert(x <= 102);
}

First, we have to compile this program into LLVM bitcode. We can either use our script, or call clang directly :

~$ clang -emit-llvm -g -c gopan.c -o gopan.bc
or
~$ compile_llvm.sh -g -i gopan.c -o gopan.bc

We can now run PAGAI on the resulting bitcode file. It outputs the C source code with annotations. safe means that the numerical operation cannot overflow, and assert OK means that the assert statement is proved correct.

~$ pagai -i gopan.bc
#include "../pagai_assert.h"
int main() {
	int x = 0;
	int y = 0;

	/* reachable */
	while (1) {
		/* invariant:
		102-x-y >= 0
		y >= 0
		x-y >= 0
		*/
		if (x <= 50)  {
			// safe
			y++;
		} else // safe
		       y--;
	

		if (y < 0) break;
		// safe
		x++;
	}
 	
	// safe
	/* assert OK */
	assert(x+y<=101);
	/* assert OK */
	assert(x <= 102);
/* reachable */
}

Pagai can also output an annotated LLVM bitcode file with the invariants stored as LLVM metadata, so that they can be used by external tools.

See pagai --help for a full list of options.