Usage

For a list of arguments accepted by PAGAI, run pagai -h.

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).

With a C input

If you want to use PAGAI with a C input, you first need to setup a pagai.conf file in the same directory as the PAGAI executable. This conf file contains only one variable so far, named ResourceDir. This variable should be set to the path of your LLVM/Clang installation. In particular, make sure you set ResourceDir so that the path $(ResourceDir)/lib/clang/3.4/include/ exists and contains e.g. float.h.

The pagai.conf file should have the form:

"ResourceDir <dir>"

Example:

~$ cat pagai.conf
ResourceDir /Users/julien/work/pagai/external/llvm

With a LLVM .bc input

The pagai.conf file is only used for compiling C/C++ code into LLVM bitcode. If you directly give to PAGAI a bitcode file, it will process it. Note that you will need to compile into bitcode with clang and the -g and -emit-llvm arguments.

Example

How to analyze 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.