verify-bpf

为ebpf-for-windows项目构建并验证eBPF程序。当要求将.c BPF源码编译为.o文件，或使用bpf2c验证.o ELF文件时，使用此技能。

npx skills add https://github.com/microsoft/ebpf-for-windows --skill 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

Flag	Purpose
`--bpf <file>`	Input ELF file containing BPF bytecode
`--sys <file>`	Generate Windows kernel driver C wrapper
`--dll <file>`	Generate Windows DLL C wrapper
`--raw <file>`	Generate C code without platform wrapper
`--verbose`	Show detailed verifier failure info (invariants)
`--type <str>`	Override eBPF program type string
`--hash <alg>`	Algorithm used to hash ELF file

Workflow

Step 1: Identify the Source

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

Source Location	Include Flags
`tests\sample\*.c`	`-Iinclude -Iexternal\bpftool -Itests\xdp -Itests\socket -Itests\sample\ext\inc -Itests\include`
`tests\sample\undocked\*.c`	Same as above, plus `-Itests\sample -Iundocked\tests\sample\ext\inc`
User-provided file	Start with the standard sample flags; add more `-I` paths as needed

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:

Re-run with --verbose if not already used, to get full invariant output.
Read external/ebpf-verifier/docs/llm-context.md — the authoritative PREVAIL diagnostic reference.
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