Building this project will first require installations of Rust, cbindgen and LLVM 14
To start, install rustc and rustup from the rust web site
Next step is to set the rust version to one that used LLVM 14. It was first added in version 1.60 and last used in version 1.64.0. To do this for a version such as 1.64.0, use the following command:
rustup install <version>
rustup default <version>
To check that the update worked, run the following command to view the rustc version being used along with the version of LLVM being used:
rustc --version --verbose
The rust library contained in this project contains a rust-toolchain.toml
to set the version to that needed for compatability with LLVM 14 and the required rust compiler flags. If building the project with additional crates, ensure to add a rust-toolchain.toml
file in the crate directory setting the default toolchain channel to nightly-2022-08-01
.
Using cargo, install cbindgen and add it to your path:
cargo install --force cbindgen
export PATH=$PATH:~/.cargo/bin
First ensure that clang and lld are installed and based on LLVM version 14
sudo apt install clang-14 lld-14
To check installation, run
clang-14 --version
ld.lld-14 --version
As a prerequisite, follow this guide to build SeaHorn locally.
Create a build directory
mkdir build
cd build
Configure with cmake
cmake \
-DCMAKE_C_COMPILER=clang-14 \
-DCMAKE_CXX_COMPILER=clang++-14 \
-DSEAHORN_ROOT=<SEAHORN_ROOT> \
../ -GNinja
Where SEAHORN_ROOT
is the directory containing your local seahorn build.
Alternatively, the project can be configured using cmake presets. To do this, simply run the following command:
cmake --preset <PRESET_NAME>
Where PRESET_NAME
is the preset you would like to use. The presets that are currently available are: default-jammy
. These presets assume that seahorn
is in your home directory.
This will also allow the project to be configured and compiled within VS Code using the CMake Tools extension.
If you would like to use different compilation settings or if you have seahorn
in any other directory, you will need to make your own CMakeUserPresets.json
file with your own presets.
Compile
ninja
or
cmake --build .
In order to use the project on Windows, a Docker container is used to run the project. To set this up, do the following:
Install and setup the Windows Subsystem for Linux (WSL)
Install Docker Desktop for Windows
Install the Dev - Containers extension for VS Code
From a command prompt, enter WSL using:
wsl
Configure git inside of WSL
git config --global user.name "Your Name"
git config --global user.email "Your Email"
Setup an SSH key for GitHub by following this guide
Clone the project into your home directory
cd ~
git clone git@github.com:thomashart17/c-rust.git
Build the Docker container
From the root of the project, run:
docker pull seahorn/seahorn-llvm14:nightly
docker build -t c-rust -f docker/c-rust.Dockerfile .
Run the Docker container
docker run -it c-rust
After completing this step, you will be able to stop and start the docker container from the Docker Desktop application. Running this again will create a new container that will not contain any of the changes made in the previous container.
Open the project in VS Code
Once the container is running, open VS Code and select the Dev Containers: Attach to Running Container...
command from the command palette. Select the container that was just created and wait for the project to open.
To avoid increased runtime for jobs using print macros, custom print macros can overwrite the standard print macros and remove their functionality. These macros are defined in sea
and can be imported as follows:
use sea::print;
use sea::println;
use sea::eprint;
use sea::eprintln;
Use CBindGen to generate C header files for Rust library. First install CBindGen
cargo install -force cbindgen
export PATH=$PATH:~/.cargo/bin
Next create a cbindgen.toml file in the crate's directory. For the test lib in this project,
cd /project-path/src/test-lib
echo -e "language = \"C\"\n\ninclude_guard = \"TEST_LIB_H_\"" > cbindgen.toml
Once configured, inside the same directory, run the cbindgen command
cbindgen --config cbindgen.toml --output ./inc/lib.h
This will generate a header file lib.h
inside the crate's folder inside of a new inc
folder.
Link Time Optimization was based off the resource available here.
Before running LTO between rust and C, clang and lld must be installed as described in Installing LLVM 14 Tools Now to build the lto files
When building for LTO, certain flags are set for the rust compiler rustc
, the LLVM C frontend and the LLVM linker.
The flags needed for LTO with the rustc compiler are set in the Cargo.toml
file and will be implemented by the cargo tool automatically. They are described here.
crate-type = static-lib
- Will generate a static system library as the output of crate compilation.opt-level = 2
- Sets optimizer level 2Clinker-plugin-lto
- Defers LTO optimization to the final linking stage. Passed as a profile RUSTFLAG
.Zemit-thin-lto=no
- Experimental flag to running thin LTO pass when using the LTO linker plugin. Passed as a profile RUSTFLAG
.The flags needed for LTO with the clang compiler are passed as compiler arguments. They are described here.
flto
- Defers LTO optimization to the final linking stageO2
- Sets optimizer level 2The flags needed for LTO with the lld linker are passed as arguments. They are described here
flto
- Enables LTOfuse-ld=lld-14
- Enables using the LLVM linker LLD of version 14Wl,--plugin-opt=-lto-embed-bitcode=post-merge-pre-opt
- Embeds the post merge, pre optimized bitcode to the resultant binary fileO2
- Set optimizer level 2Once the binary is generated, it is necessary to extract the bitcode from the file. This is done using the llvm-objcopy-14
and llvm-dis-14
tool
objcopy a.out --dump-section .llvmbc=llvm.bc
llvm-dis-14 llvm.bc