I'm working on verifying some Rust code using SAW. SAW requires that you compile to LLVM bitcode, which you can then import and verify. I know you can generate bitcode using the --emit=llvm-bc
flag to rustc, and this works great for projects without dependencies.
The issue comes when trying to compile a project which makes use of external crates. Here's an example Cargo.toml file:
[package]
name = "foobar"
version = "0.1.0"
edition = "2018"
[dependencies]
pythagoras = "0.1.1"
And here's a basic src/lib.rs
we might want to compile & verify:
pub use pythagoras;
#[no_mangle]
pub extern "C" fn calc_hypot(a: u32, b: u32) -> f64 {
pythagoras::theorem(a, b)
}
We can compile this to bitcode like this: RUSTFLAGS="--emit=llvm-bc" cargo build --release
. The issue is that the bitcode for the current module and its dependencies are generated separately (in target/release/deps/foobar-something.bc
and target/release/deps/pythagoras-somethingelse.bc
). They're only combined when the actual compiled library is generated.
Is there any way to generate a single bitcode file containing both the current module & all its dependencies, so this file can be imported, and won't refer to any external names? I realise this is a pretty niche case, so hacky solutions (e.g: Compiling to a C static lib, then converting that back to LLVM bitcode somehow) are also completely reasonable.