See Installation for how to install cclyzer++.

Configuring the Analysis

The analysis is configured via command-line arguments passed to the fact generator, primarily --context-sensitivity and --signatures. For example,

factgen-exe --out-dir <fact-dir> --signatures sigs.json --context-sensitivity 1-callsite prog.bc

where prog.bc is an LLVM bitcode module. The valid settings for context sensitivity are:

  • insensitive

  • 1-callsite

  • 2-callsite

  • 3-callsite

  • 4-callsite

  • 5-callsite

  • 6-callsite

  • 7-callsite

  • 8-callsite

  • 9-callsite

  • 1-caller

  • 2-caller

  • 3-caller

  • 4-caller

  • 5-caller

  • 6-caller

  • 7-caller

  • 8-caller

  • 9-caller

  • 1-file

  • 2-file

  • 3-file

  • 4-file

  • 5-file

  • 6-file

  • 7-file

  • 8-file

  • 9-file

Run factgen-exe --help to see the full list of options. See the architecture documentation for more information on the role of the fact generator.

Running the Analysis

Soufflé ships with an interpreter and a synthesizer, which outputs C++ code that can be compiled by Clang. Accordingly, there are three ways to run the analysis:

  • Directly via the Soufflé interpreter

  • By synthesizing the Datalog to C++ and then either

    • compiling the C++ via Clang to a standalone executable

    • compiling the C++ via Clang to a shared library that gets loaded by LLVM’s opt and used by the C++ interface

The Debian package and dist Docker image only ship with the latter option.

With Opt

The LLVM pass is used via opt. If you installed via the Debian package or are running in the dist container, try:

opt --disable-output --load=/usr/lib/ --load=/usr/lib/ -cclyzer --context-sensitivity=1-callsite --datalog-analysis=subset prog.bc

To see more options, run

opt --load=/usr/lib/ --load=/usr/lib/ --help

though be warned - this includes all opt flags, and most of them are irrelevant to running the analysis.

(If you built from source, the .so files will be in build/.)

With Soufflé

If you’re not running in the dist Docker image and have the cclyzer++ source available, you can run the analysis from the Soufflé interpreter. For example, here’s how to run the subset analysis:

souffle --fact-dir <fact-dir> --output-dir <output-dir> datalog/subset.project

where fact-dir was the directory passed to the --out-dir option of the fact generator. Pass -j <n> to parallelize the analysis across n threads. See the Soufflé documentation for more details.

To synthesize and compile the analysis, run

souffle --generate=subset.cpp datalog/subset.project subset.cpp
subset --facts <fact-dir> --output <output-dir> -j <n>