Chapter 2. Installation and Usage Guide
Platform Support
- Linux
- macOS (both x86_64 and aarch64 version)
Preparation
The latest RAPx is developped based on Rust version nightly-2024-02-01. You can install this version using the following command.
rustup toolchain install nightly-2025-02-01 --profile minimal --component rustc-dev,rust-src,llvm-tools-preview
If you have multiple Rust versions, please ensure the default version is set to nightly-2025-02-01.
rustup show
Install
Download the project
git clone https://github.com/Artisan-Lab/RAPx.git
Build and install RAPx
./install.sh
You can combine the previous two steps into a single command:
cargo +nightly-2025-02-01 install rapx --git https://github.com/Artisan-Lab/RAPx.git
For macOS users, you may encounter compilation errors related to Z3 headers and libraries. There are two solutions:
The first one is to manually export the headers and libraries as follows:
export C_INCLUDE_PATH=/opt/homebrew/Cellar/z3/VERSION/include:$C_INCLUDE_PATH
ln -s /opt/homebrew/Cellar/z3/VERSION/lib/libz3.dylib /usr/local/lib/libz3.dylib
Alternatively, you can modify the Cargo.toml file to change the dependency of Z3 to use static linkage. However, this may significantly slow down the installation process, so we do not recommend enabling this option by default.
[dependencies]
z3 = {version="0.12.1", features = ["static-link-z3"]}
After this step, you should be able to see the RAPx plugin for cargo.
cargo --list
Execute the following command to run RAPx and print the help message:
cargo rapx -help
Usage:
cargo rapx [rapx options] -- [cargo check options]
RAPx Options:
Application:
-F or -uaf use-after-free/double free detection.
-M or -mleak memory leakage detection.
-O or -opt automatically detect code optimization chances.
-I or -infer (under development) infer the safety properties required by unsafe APIs.
-V or -verify (under development) verify if the safety requirements of unsafe API are satisfied.
Analysis:
-alias perform alias analysis (meet-over-paths)
-adg generate API dependency graphs
-callgraph generate callgraphs
-dataflow (not supported yet) generate dataflow graphs
-heap analyze if the type holds a piece of memory on heap
-audit (under development) generate unsafe code audit units
...
Uninstall
cargo uninstall rapx