Overview
Notable Features
Subset and Unification Analyses
There are two widely-used paradigms in constructing pointer analyses: subset-based and unification-based. Unification-based analyses are generally highly scalable, but less precise than comparable subset-based analyses. cclyzer++ provides both.
See the implementation documentation for information about the unification-based analysis.
Configurable Context Sensitivity and Heap Cloning
Context-sensitive pointer analyses are often more precise than context-insensitive ones, but their performance is less predictable. cclyzer++ provides a variety of context sensitivity strategies and depths, including k-callsite. The choice of context sensitivity can be configured at runtime.
cclyzer++ also performs heap cloning, matching whichever strategy is chosen for context-sensitivity.
Modeling Library Functions
cclyzer++ supports modeling external functions with signatures which summarize their effect on memory. Signatures can be used to model functions from libc or other external libraries. Such models are crucial for soundness. See Signatures for details on how to create signatures.
Language Support
cclyzer++ has primarily been tested on LLVM code produced by Clang 10 through 14 when compiling from C and C++ for x86_64. Your mileage may vary with other languages, compilers, and targets.
Bibliography
The following papers significantly influenced the development of cclyzer++.
Bravenboer, M. and Smaragdakis, Y., 2009, October. Strictly declarative specification of sophisticated points-to analyses. In Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications (pp. 243-262).
Balatsouras, G. and Smaragdakis, Y., 2016, September. Structure-sensitive points-to analysis for C and C++. In International Static Analysis Symposium (pp. 84-104). Springer, Berlin, Heidelberg.
The pointer analysis tutorial of Smaragdakis and Balatsouras was also quite helpful.
Comparison to cclyzer
As mentioned above, cclyzer++ is based on cclyzer. The major differences are that cclyzer++
supports LLVM 10 through 14, with limited support for LLVM 15.
is implemented in Soufflé rather than LogicBlox
has a C++ interface, rather than a Python one
has runtime-configurable context-sensitivity and heap-cloning
features a unification-based analysis
allows modeling external functions with signatures
drops certain uninformative contexts (see
drop.dl)
On the less impactful side, cclyzer++ also
includes assertions about correctness
improves on the heuristic that controls array suballocations (see
allocations-subobjects.dl)tracks suballocation sizes and offsets (see
allocations-subobjects.dl)soundly handles
argvhas additional documentation (both code-level comments and higher-level documents such as this one)
Many thanks to the authors of cclyzer for their contributions! The cclyzer
license is included with the source distribution of cclyzer++ as
LICENSE-cclyzer.txt.
Project Status
cclyzer++ is actively developed and maintained by Galois, Inc. Points of contact are: Langston Barrett (email: langston at galois dot com) Scott Moore (email: scott at galois dot com).
Versioning
Since v0.4.0, cclyzer++ has attempted to follow semantic versioning 2.0.0.
LLVM Library Version
cclyzer++ currently builds against LLVM 14 by default and can be built with previous versions 13 through 10. cclyzer++ can be built with LLVM 15, but the analysis does not yet support opaque pointers.
