Translation validation for the LLVM BPF backend, built on Alive2's arm-tv branch (the arm-tv / riscv-tv lineage).

Given an LLVM IR function, bpf-tv runs the real BPF backend to produce assembly, lifts that assembly back to LLVM IR with a hand-written BPF lifter (bpf2llvm), and asks Alive2 whether the round trip is a refinement — i.e. whether the backend miscompiled. The kernel verifier checks safety; this checks correctness, the pipeline stage nothing else covers.

See DESIGN.md for architecture, scope, and staging.

src/                       BPF lifter (bpf2llvm) + driver (bpf-tv)
third_party/alive2         pinned submodule: official AliveToolkit/alive2
third_party/alive2-arm-tv  pinned submodule: regehr/alive2 @ arm-tv branch
                           (reference only — never built)
third_party/llvm-project   pinned submodule: llvm/llvm-project
scripts/build-deps.sh      builds LLVM + alive2, out-of-tree under build*/
.devcontainer/             reproducible Ubuntu build environment

Everything is pinned: dependencies are submodules at exact commits chosen to be API-compatible (official alive2 at the arm-tv branch's merge-base, LLVM at a main commit of the same vintage), and the canonical build environment is the devcontainer. Pushes to main that touch .devcontainer/ publish the image to GHCR (ghcr.io/qobilidop/bpf-tv-devcontainer) for local dev and CI reuse.

The canonical environment is the devcontainer (Ubuntu 24.04; open the repo in VS Code → "Reopen in Container", or use the devcontainer CLI). Inside it:

git submodule update --init --depth 1   # pinned SHAs; shallow is fine
./scripts/build-deps.sh                 # builds LLVM, then alive2 (long)
cmake -S . -B "$BUILD_ROOT/bpf-tv" -G Ninja
ninja -C "$BUILD_ROOT/bpf-tv"

BUILD_ROOT defaults to build/; the devcontainer sets it to build-linux/ so a native macOS build tree can coexist. A native (non-container) build works too with brew install cmake ninja re2c z3 — but note the devcontainer's pinned source-built Z3 is the configuration of record (brew's Z3 rolls forward untested).

An LLVM source build is required (RTTI, EH, assertions; targets AArch64;RISCV;BPF) because the lifters use build-tree tablegen headers.

build/bpf-tv foo.ll                  # validate first function
build/bpf-tv --fn=my_func foo.ll     # validate a specific function
build/bpf-tv --asm-only foo.ll       # just show the backend's asm