verify-bpf

Build & Verify eBPF Programs (ebpf-for-windows)

Compile eBPF C source to ELF bytecode with clang, then verify (and optionally generate native code) with bpf2c. On verification failure, diagnose using the PREVAIL reference.

When to Use

• User asks to compile/build a .c eBPF program to .o
• User asks to verify a .o ELF file or check if it passes the verifier
• User asks to debug or fix a verification failure from bpf2c output
• User mentions bpf2c, clang+bpf, or PREVAIL verification in the ebpf-for-windows context

Prerequisites

• clang.exe — find the first existing path (highest priority first): packages\llvm.tools\clang.exe, "$env:ProgramFiles\LLVM\bin\clang.exe", "$(& "${env:ProgramFiles(x86)}\Microsoft Visual Studio\Installer\vswhere.exe" -latest -property installationPath)\VC\Tools\Llvm\bin\clang.exe"
• bpf2c.exe — if x64\Debug\bpf2c.exe is missing, build it: msbuild ebpf-for-windows.sln /m /p:Configuration=Debug /p:Platform=x64 /t:tools\bpf2c

Quick Reference

1. Compile: C → ELF (.o)

Run from the solution root directory (use the clang path found above):

# Standard sample programs
& '<clang-path>' -g -target bpf -O2 -Werror `
  -Iinclude -Iexternal\bpftool `
  -Itests\xdp -Itests\socket `
  -Itests\sample\ext\inc -Itests\include `
  -c <SOURCE>.c -o <OUTPUT>.o

For undocked programs (tests\sample\undocked\*.c), also add:

• -Itests\sample
• -Iundocked\tests\sample\ext\inc

2. Verify: ELF (.o) → native C (via bpf2c)

.\x64\Debug\bpf2c.exe --bpf <FILE>.o --sys <OUTPUT_DIR>\<name>_driver.c

Add --verbose to get detailed verifier output (pre/post invariants at each instruction) on failure.

bpf2c Options

Workflow

Step 1: Identify the Source

Determine the .c source file and where the .o should go. Common patterns:

Step 2: Compile with Clang

Run clang. If it fails, fix compiler errors in the C source (standard C/clang diagnostics).

Step 3: Verify with bpf2c

Run bpf2c with --sys (or --dll/--raw). Two outcomes:

• Success → bpf2c generates the output C file. Verification passed.
• Failure → bpf2c prints verifier errors. Proceed to diagnosis.

Step 4: Diagnose Failures

On verification failure:

1. Re-run with --verbose if not already used, to get full invariant output.
2. Read external/ebpf-verifier/docs/llm-context.md — the authoritative PREVAIL diagnostic reference.
3. Follow the diagnosis protocol in that document (identify error → check pre-invariant → trace root cause → recommend fix).

Example: Full Pipeline

# Compile (undocked program — needs full include paths)
& '<clang-path>' -g -target bpf -O2 -Werror `
  -Iinclude -Iexternal\bpftool `
  -Itests\xdp -Itests\socket -Itests\sample\ext\inc -Itests\include `
  -Itests\sample -Iundocked\tests\sample\ext\inc `
  -c tests\sample\undocked\perf_event_burst.c `
  -o x64\Debug\perf_event_burst.o

# Verify + generate driver
.\x64\Debug\bpf2c.exe --bpf x64\Debug\perf_event_burst.o `
  --sys .\x64\Debug\perf_event_burst_km\perf_event_burst_driver.c

# If verification fails, re-run with --verbose for diagnosis
.\x64\Debug\bpf2c.exe --bpf x64\Debug\perf_event_burst.o `
  --sys .\x64\Debug\perf_event_burst_km\perf_event_burst_driver.c `
  --verbose