build-prevail: Скилл для проверки и тестирования eBPF

--- name: build-prevail description: > Build and test the PREVAIL verifier (external/ebpf-verifier) standalone. Use this skill when asked to build, test, or iterate on the PREVAIL verifier, run YAML verification tests, or work with the verifier's cmake build system. --- # Build and Test PREVAIL Verifier Build and test the PREVAIL eBPF verifier (`external/ebpf-verifier`) independently from the main eBPF for Windows solution. ## When to Use - Working on verifier changes in `external/ebpf-verifier/` - Running or debugging YAML verification tests - Building `run_yaml.exe` or `tests.exe` for the verifier - Iterating on verifier fixes with faster feedback than full MSBuild ## Prerequisites The verifier's cmake build directory must exist. If `external/ebpf-verifier/build/` is missing, run from the solution root: ```powershell .scriptsinitialize_ebpf_repo.ps1 ``` This generates cmake projects for the verifier (and other submodules). You only need to do this once, or after resetting submodules. ## Building Standalone ```powershell cd externalebpf-verifier # Build the YAML test runner (most common during development) cmake --build build --config Release --target run_yaml # Build the full Catch2 test binary cmake --build build --config Release --target tests # Clean build (rebuild everything from scratch) cmake --build build --config Release --clean-first ``` ### Enabling Standalone Tests When built as a submodule, `prevail_ENABLE_TESTS` defaults to OFF. To enable standalone tests: ```powershell cmake -B build -Dprevail_ENABLE_TESTS=ON cmake --build build --config Release ``` **Note:** The `initialize_ebpf_repo.ps1` script does NOT enable tests. You need to reconfigure with `-Dprevail_ENABLE_TESTS=ON` if you want to build `tests.exe` standalone. ## Running YAML Tests YAML test files are in `external/ebpf-verifier/test-data/*.yaml`. Each file is a test suite with individual tests separated by `---`. ```powershell cd externalebpf-verifier # Run all tests in a suite .binrun_yaml.exe test-dataloop.yaml # Run tests matching a substring .binrun_yaml.exe test-dataloop.yaml "while loop with" # Run a specific test by exact name .binrun_yaml.exe test-databitop.yaml "AND with 0xFF preserves relations when value fits" ``` ### Exit codes - `0` — all tests passed - `1` — one or more tests failed ### Discovering postconditions for new tests When writing new YAML tests, use placeholder postconditions and run the test to discover actual values: ```yaml post: - placeholder messages: - placeholder ``` The failure output shows "Unexpected properties" (actual values) and "Unseen properties" (your placeholders). Copy the actual values into your test. ### Available test suites | Suite | Description | |-------|-------------| | `loop.yaml` | Bounded loop verification (termination checking) | | `bitop.yaml` | Bitwise operations (AND, OR, XOR) | | `movsx.yaml` | Sign extension (MOVSX) operations | | `sext.yaml` | Sign/zero extension relational tests | | `jump.yaml` | Conditional jumps and branching | | `packet.yaml` | Packet access safety | | `pointer.yaml` | Pointer arithmetic and safety | | `stack.yaml` | Stack access verification | | `call.yaml` | Helper function calls | | `calllocal.yaml` | Local (subprogram) calls | | `assign.yaml` | Register assignment | | `add.yaml` / `subtract.yaml` | Arithmetic operations | | `muldiv.yaml` / `sdivmod.yaml` / `udivmod.yaml` | Multiplication, division, modulo | | `shift.yaml` | Shift operations | | `atomic.yaml` | Atomic operations | | `full64.yaml` | 64-bit comparison operations | | `unsigned.yaml` | Unsigned comparison operations | | `unop.yaml` | Unary operations (neg, swap) | | `observe.yaml` | Observation/assertion tests | | `uninit.yaml` | Uninitialized variable detection | | `map.yaml` | Map operations | | `parse.yaml` | YAML parsing tests | | `callx.yaml` | Indirect calls | ## Running the Full Catch2 Test Binary ```powershell cd externalebpf-verifier # Run all tests .bintests.exe # Run with compact reporter .bintests.exe --reporter compact # Abort on first failure .bintests.exe --abort --reporter compact # Run specific test sections .bintests.exe "YAML suite: test-data/loop.yaml" ``` The `tests.exe` binary includes YAML tests, ELF verification tests, conformance tests, and unit tests. ## YAML Test Format ```yaml --- test-case: descriptive test name options: ["termination"] # optional; enables loop termination checking pre: ["r1.type=number", "r1.svalue=[0, 100]", "r1.uvalue=r1.svalue"] code: <start>: | r0 = 0 <loop>: | r0 += 1 if r1 > r0 goto <loop> <out>: | exit post: - r0.type=number - r0.svalue=[1, 100] messages: [] # expected verifier messages; omit for no messages ``` ### Key conventions - `r` prefix for 64-bit registers, `w` prefix for 32-bit - `w2 = r2` generates a 32-bit self-MOV (SHL 32 + RSH 32 truncation pattern) - `r2 &= 255` generates 64-bit AND with immediate - `svalue` = signed value, `uvalue` = unsigned value - `r2.svalue=r1.svalue` means relational constraint (r2 tracks r1) - `r1.svalue=[0, 100]` means interval [0, 100] - `pc[N]` refers to the loop counter at instruction N - `post:` must list ALL expected properties — unlisted ones cause "Unexpected properties" failure - `messages:` field is optional (defaults to empty) ## Building via MSBuild (within the main solution) When you need to build the verifier as part of the main solution (e.g., to build bpf2c which depends on it): ```powershell # From solution root msbuild ebpf-for-windows.sln /m /p:Configuration=Debug /p:Platform=x64 /t:"toolsbpf2c" /v:q /nologo ``` The MSBuild target for the verifier library is `libsuserprevail` (for Debug/Release configs). The `ubpf_fuzzerebpfverifier` target is a separate copy used only in `FuzzerDebug` configuration. ## Submodule Notes - The verifier lives at `external/ebpf-verifier/` as a git submodule - `git stash` in the parent repo does NOT affect the submodule working tree — stash separately in the submodule if needed - To reset to the committed pointer: `git submodule update --init --recursive` (from the parent repo root) - After resetting submodules, re-run `.scriptsinitialize_ebpf_repo.ps1` to regenerate cmake projects