This is a Rust port of the original C++ implementation.
The version discussed in the PLDI paper is available here.
prevail tests/upstream/ebpf-samples/cilium/bpf_lxc.o 2/1The output is three comma-separated values:
- 1 or 0, for "pass" and "fail" respectively
- The runtime of the fixpoint algorithm (in seconds)
- The peak memory consumption, in kb, as reflected by the resident-set size (rss)
Additional flags: --asm <file> (disassembly), --dot <file> (CFG dot graph), -v (verbose invariants), -f (print first failure).
- Functional parity with upstream. The Rust verifier should accept and reject the same programs as the upstream C++ verifier, and pass the same (or a superset of) test cases. Added features must be first accepted to upstream.
- Idiomatic Rust. use idiomatic Rust while preserving correctness.
The repository uses two distinct test concepts:
- Conformance: ISA semantics checks using the
bpf_conformancecorpus. Run withcargo test --test conformance_tests. - Upstream parity: behavioral equivalence checks against the upstream C++
Prevail verifier on shared fixtures/baselines.
Run with
cargo xtask parity compare.
The tests/upstream submodule pins the upstream C++ commit used as
the sync anchor. See docs/upstream-sync.md for the
full sync workflow.
Quick check for new upstream changes:
cargo xtask upstream-diffThese are intentional design/architecture differences that are useful to keep in mind when bumping upstream:
- Thread-local globals replaced by explicit context passing.
Rust uses
DomainContext(thread-safe and explicit) instead of C++thread_local_*globals. - BTF is ported and used natively in Rust.
Rust has its own
src/btf/implementation used by ELF loading and CO-RE relocation handling; it is not a direct runtime link to upstreamlibbtf. - Canonical fixtures come from upstream submodule.
YAML tests and schema are read from
tests/upstream/test-data/andtests/upstream/test-schema.yaml, not duplicated in this repo. - Test/CI infrastructure is Rust-repo specific. Differential scripts and CI orchestration differ from upstream CMake/Catch2, while preserving parity goals.
- Array offset map data structure differs.
Rust currently uses
BTreeMapwhere upstream uses a radix/patricia tree. This is mostly a performance/design divergence and can affect bump effort.
If an upstream change touches one of these areas, a bump is likely to require manual adaptation rather than mechanical porting.
- Rust (version pinned in
rust-toolchain.toml)
cargo build --releaseTo work from the local checkout:
cargo install --path .To install the released crate with the prevail binary already wired up:
cargo install prevailBoth commands drop a prevail executable into your Cargo bin directory thanks to the default prevail binary entry in Cargo.toml.
cargo testFor final testing, before a push, prefer:
cargo xtask testThis runs the default non-parity suite (all-no-parity) through the local certification/cache workflow used by hooks.
By default it amends HEAD to attach certification metadata (--no-amend to opt out).
Use plain cargo test any time you want a direct, always-run test invocation.
all-no-parity is kept as a compatibility alias and runs the same suite:
cargo xtask test all-no-parityFor full coverage including parity compare:
cargo xtask test allSee CONTRIBUTING.md for development workflows.
cargo xtask gen-corpus
cargo fuzz run fuzz_assembler fuzz/corpus/fuzz_assemblerSeed corpora are generated under fuzz/corpus/ from upstream conformance and
ELF sample fixtures.
See LICENSE.txt.