vbpf / prevail / 24963666837

push

github

Split runtime semantics from presentation/orchestration (#1101)

Closes #1085. Introduces `RuntimeConfig` — the subset of verifier options that affects which programs are accepted — and reshapes `VerifierOptions` so a signature reveals whether a knob can change verification outcome.

- New `RuntimeConfig` groups the analysis-semantic fields: `strict`, `allow_division_by_zero`, `setup_constraints`, `big_endian`, `check_for_termination`, `subprogram_stack_size`, `max_call_stack_frames`, `max_packet_size`. `validate()` and `total_stack_size()` live here.
- `VerifierOptions` composes `RuntimeConfig` and `VerbosityOptions`; `mock_map_fds` and `must_have_exit` stay as top-level fields. The single-field `prepare_cfg_options` wrapper is gone.
- `check_for_termination` moved out of CFG-prep options into `RuntimeConfig` — it instruments loop heads and gates the post-analysis termination check, so it changes verification outcome.
- Functions that only consume runtime semantics (`get_assertions`, `AssertExtractor`, the abstract domain/checker/transformer) take `RuntimeConfig` directly. `AnalysisContext::runtime()` exposes the runtime subset.
- Legacy `_t`-suffixed structs renamed to PascalCase to match the rest of the codebase: `ebpf_verifier_options_t` → `VerifierOptions`, `verbosity_options_t` → `VerbosityOptions`, `ebpf_verifier_stats_t` → `VerifierStats`.
- Adds `src/test/test_runtime_config.cpp` covering `validate()` bounds and `total_stack_size()`.
- Includes incidental clang-tidy-style cleanups in unrelated files picked up by the formatter run.
---------

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

198 of 203 new or added lines in 29 files covered. (97.54%)

13772 of 15426 relevant lines covered (89.28%)

4377862.11 hits per line