This workspace contains the usable libraries from .
- Get rust
- Use cargo in this directory to build, test, benchmark and create docs
- Get an IDE supporting rust analyzer (vscode, rustrover, clion, zed, nvim, etc. )
A basic toolchain is setup ayutomatically when running cargo by ./rust-toolchain.toml, however some useful tools to additionally install are...
Expands procedural macros and outputs highlighted expansion to the terminal.
cd emdb
cargo expand --test scratchNote for single file expansion (e.g. of a macro rules) we can also use rustc -Zunpretty=expanded <file>.rs
View intermediate results (mir, llvm, asm) generated by rustc. Allows easy scoping down to the level of individual functions.
# view the available objects in the dereferencing example
cargo asm -p emdb --example dereferencing
# for the 2nd object option
cargo asm -p emdb --example dereferencing --mir 1 # view the MIR code
cargo asm -p emdb --example dereferencing --mca 1 # view the llvm mca analysisGenerates flame graphs using perf, from tests and benchmarks.
CARGO_PROFILE_BENCH_DEBUG=true cargo flamegraph -p combi --bench tokenskani is a bit-precise model checker using CBMC, it can be used to verify memory
safety, panic safety (e.g. on asserts) and other behaviour (e.g. arithmetic
overflows).
cargo kanikani is used to verify the correctness of unsafe code in this project. While Kani
is sound (no false negatives - VERIFIED means proved no errors), verification
can take a long time, and it is not complete (has false positives - can fail to
verify correct code).
Furthermore coverage of proofs is important, kani only analyses proofs.
Profile guided optimisation addon for cargo.
All crates part of this project are contained in a single cargo workspace.
- Beware: The project relies on a fork of divan for benchmarks from outside this repo
cargo test
cargo benchFor test output from prints, and getting panic backtraces, a handy command is
RUST_BACKTRACE=1 cargo test -- --nocaptureCargo.lock is tracked by version control for reproducability (see this justification).
cargo doc # public docs
cargo doc --document-private-items # include private documentationIf using vscode, the live preview can be used to view documentation built in the target directory.
- For rare failure, see the ./emdb/tests/valid/fixme directory.
- Nondeterministic compile behaviour for ./emdb/tests/valid/complex/favourite_colours.rs