Usage
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/libSoufflePA.so --load=/usr/lib/libPAPass.so -cclyzer --context-sensitivity=1-callsite --datalog-analysis=subset prog.bc
To see more options, run
opt --load=/usr/lib/libSoufflePA.so --load=/usr/lib/libPAPass.so --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
souffle-compile.py subset.cpp
subset --facts <fact-dir> --output <output-dir> -j <n>