Human-friendly CLI output for bin/prevail (#1042)

* Replace CSV output with human-friendly PASS/FAIL CLI output

The default output was `{0|1},{seconds},{memory_kb}` — a CSV row for
benchmarking scripts that is unfriendly for humans. Benchmarking is
better done externally (time, /usr/bin/time -v).

New output: `PASS: section/function` or `FAIL: section/function` with
the first error and a hint line pointing to --failure-slice / -v.
Add -q/--quiet (exit code only) and --cfg (replaces --domain cfg).

Remove dead code: --domain option (linux, stats, zoneCrab selectors),
linux_verifier, memsize helpers, collect_stats/stats_headers, fnv1a64,
@headers special filename, bin/check alias, and stale benchmark scripts.

Move src/main/check.cpp → src/main.cpp (simplified, rewritten).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

* Graduate loop3.o from skip to expected failure

The >4x performance improvement means loop3.o no longer hangs.
It now completes quickly but is rejected due to type precision
loss through the loop join (VerifierTypeTracking).

* Remove redundant install exclude, fix doc path

- Remove `PATTERN "main.cpp" EXCLUDE` from install — the glob only
  matches *.hpp/*.h so main.cpp would never be included anyway.
- Fix `./prevail` → `./bin/prevail` in docs/architecture.md for
  consistency with the actual binary location.

---------

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Author: elazarg

AGENTS.md

@@ -10,7 +10,7 @@
 ## Quick project facts
 - **Language & standards:** Core verifier is implemented in modern C++20 (see `CMakeLists.txt`).
 - **Primary deliverables:**
-  - `check`: command-line verifier for eBPF object files.
+  - `prevail`: command-line verifier for eBPF object files.
   - `tests`: Catch2-based regression suite.
   - `run_yaml`: YAML test case runner.
 - **Third-party code:** resides under `external/` and is treated as vendored dependencies. Do not edit these unless explicitly asked.
@@ -39,7 +39,7 @@
    ```
 4. **Spot-check the verifier** against bundled samples:
    ```bash
-   ./prevail ebpf-samples/cilium/bpf_lxc.o 2/1
+   ./bin/prevail ebpf-samples/cilium/bpf_lxc.o 2/1
    ```
 5. **Capture reasoning.** When a change introduces or relies on a new invariant, add a targeted regression test and document the invariant in code comments or `docs/` notes so future auditors can reconstruct the argument.
 

CHANGELOG.md

@@ -3,7 +3,7 @@
 ## v0.2.0 (2026-02-22)
 
 Major expansion of type system, platform modeling, and safety guarantees.
-27 commits since v0.1.3.
+34 commits since v0.1.3.
 
 ### Type system
 
@@ -36,22 +36,32 @@ Major expansion of type system, platform modeling, and safety guarantees.
   domain (#960).
 - Propagate alloc_mem_size through helpers and decompose kfunc flags.
 
+### Performance
+
+- >4× faster verification on large programs through splitdbm graph
+  internals modernization and zone domain optimizations (#1017).
+
 ### Diagnostics
 
 - Add failure slicing: `--failure-slice` prints a minimal causal trace
   from the first verification error back to its root cause.
+- Human-friendly CLI output: `PASS: section/function` / `FAIL: section/function`
+  with first error and hint line, replacing the old CSV format.
+- Add `-q`/`--quiet` flag (exit code only, no stdout).
 
 ### Infrastructure
 
 - Overhaul ELF loader and bump ebpf-samples (#1026).
 - Handle invalid BTF map metadata gracefully (#1034).
-- Modernize splitdbm graph internals (#1017).
 - Add MSVC debug assert handler (#1018).
 - Simplify test framework: drop per-test diagnostic strings, reclassify
   genuinely-unsafe programs as rejections, document VerifyIssueKind enum
   centrally.
-- Rename main executable from `bin/check` to `bin/prevail`; `bin/check` is
-  kept as a backwards-compatible copy during the transition.
+- Rename main executable from `bin/check` to `bin/prevail`.
+- Remove dead code: `--domain` option (`linux`, `stats` paths),
+  `linux_verifier`, `memsize` helpers, `collect_stats`, stale benchmark
+  scripts.
+- Move CLI entry point from `src/main/check.cpp` to `src/main.cpp`.
 - Bump external/libbtf, external/bpf_conformance, actions/checkout.
 
 ## v0.1.3

CMakeLists.txt

@@ -99,7 +99,7 @@ include(cmake/SetupBoostHeaders.cmake)
 string(REGEX REPLACE "([][+.*()^$?|\\\\])" "\\\\\\1" prevail_source_dir_escaped "${prevail_source_dir}")
 
 file(GLOB_RECURSE prevail_LIB_SRC CONFIGURE_DEPENDS "${prevail_source_dir}/src/*.cpp")
-list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/main/.*")
+list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/main\\.cpp$")
 list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/test/.*")
 
 add_library(prevail ${prevail_LIB_SRC})
@@ -178,8 +178,8 @@ set_target_properties(prevail PROPERTIES
 
 set(prevail_binary_dir "${prevail_source_dir}/bin" CACHE INTERNAL "")
 
-# Main executable: bin/prevail (with bin/check alias for backwards compatibility)
-add_executable(prevail-cli "${prevail_source_dir}/src/main/check.cpp" "${prevail_source_dir}/src/main/linux_verifier.cpp")
+# Main executable: bin/prevail
+add_executable(prevail-cli "${prevail_source_dir}/src/main.cpp")
 set_target_properties(prevail-cli PROPERTIES OUTPUT_NAME "prevail")
 target_link_libraries(prevail-cli PRIVATE prevail ${CMAKE_DL_LIBS})
 if (CMAKE_CONFIGURATION_TYPES)
@@ -192,13 +192,6 @@ else ()
   set_target_properties(prevail-cli PROPERTIES
     RUNTIME_OUTPUT_DIRECTORY "${prevail_binary_dir}")
 endif ()
-# Transitional alias: bin/check -> bin/prevail
-add_custom_command(TARGET prevail-cli POST_BUILD
-  COMMAND ${CMAKE_COMMAND} -E copy_if_different
-    "$<TARGET_FILE:prevail-cli>"
-    "$<TARGET_FILE_DIR:prevail-cli>/check$<TARGET_FILE_SUFFIX:prevail-cli>"
-  COMMENT "Creating backwards-compatible bin/check alias"
-)
 
 # Tests
 if (prevail_ENABLE_TESTS)
@@ -256,7 +249,6 @@ install(TARGETS prevail libbtf GSL
 install(DIRECTORY "${prevail_source_dir}/src/"
   DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/prevail"
   FILES_MATCHING PATTERN "*.hpp" PATTERN "*.h"
-  PATTERN "main/*" EXCLUDE
   PATTERN "test/*" EXCLUDE
 )
 

README.md

@@ -88,9 +88,6 @@ cmake --build build
 ```bash
 docker build -t prevail .
 docker run -it prevail ebpf-samples/cilium/bpf_lxc.o 2/1
-1,0.009812,4132
-# To run the Linux verifier you'll need a privileged container:
-docker run --privileged -it prevail ebpf-samples/linux/cpustat_kern.o --domain=linux
 ```
 
 </details>
@@ -99,18 +96,12 @@ docker run --privileged -it prevail ebpf-samples/linux/cpustat_kern.o --domain=l
 
 ```
 $ bin/prevail ebpf-samples/cilium/bpf_lxc.o 2/1
-1,0.014153,6080
+PASS: 2/1
 ```
 
-The output is three comma-separated values:
-
-* 1 or 0, for "pass" and "fail" respectively
-* The runtime of the fixpoint algorithm (in seconds)
-* The peak memory consumption, in kb, as reflected by the resident-set size (rss)
-
 <details><summary>Usage</summary>
 
-```
+```text
 PREVAIL is a new eBPF verifier based on abstract interpretation.
 
 
@@ -127,8 +118,8 @@ OPTIONS:
           --section SECTION   Section to analyze
           --function FUNCTION Function to analyze
   -l                          List programs
-          --domain DOMAIN:{stats,linux,zoneCrab,cfg} [zoneCrab]
-                              Abstract domain
+  -q,     --quiet             No stdout output, exit code only
+          --cfg               Print control-flow graph and exit
 
 Features:
           --termination, --no-verify-termination{false}
@@ -144,14 +135,16 @@ Features:
 Verbosity:
           --simplify, --no-simplify{false}
                               Simplify the display of the CFG by merging chains of instructions
-                              into a single basic block. Default: enabled
+                              into a single basic block. Default: enabled (disabled with
+                              --failure-slice)
           --line-info         Print line information
           --print-btf-types   Print BTF types
-          --failure-slice     Print minimal failure diagnostic (causal trace)
-          --failure-slice-depth N
-                              Maximum backward traversal steps (default: 200)
   -v                          Print invariants and first failure
   -f                          Print first failure
+          --failure-slice     Print minimal failure slices showing only instructions that
+                              contributed to errors
+          --failure-slice-depth UINT
+                              Maximum backward steps for failure slicing (default: 200)
 
 CFG output:
           --asm FILE          Print disassembly to FILE
@@ -164,16 +157,8 @@ The cfg can be viewed using `dot` and the standard PDF viewer:
 
 ```
 sudo apt install graphviz
-bin/prevail ebpf-samples/cilium/bpf_lxc.o 2/1 --dot cfg.dot --domain=stats
+bin/prevail ebpf-samples/cilium/bpf_lxc.o 2/1 --dot cfg.dot
 dot -Tpdf cfg.dot > cfg.pdf
 ```
 
 </details>
-
-## Testing the Linux verifier
-
-To run the Linux verifier, you must use `sudo`:
-
-```
-sudo bin/prevail ebpf-samples/linux/cpustat_kern.o tracepoint/power/cpu_idle --domain=linux
-```

docs/README.md

@@ -93,7 +93,7 @@ Prevail verifies that eBPF programs:
 
 ```text
 src/
-├── main/           # Entry points (check.cpp - CLI verifier)
+├── main.cpp        # CLI entry point
 ├── ir/             # Intermediate representation
 │   ├── syntax.hpp  # Instruction definitions
 │   └── cfg_builder.cpp

docs/architecture.md

@@ -169,16 +169,19 @@ Separating assertions from semantics enables:
 
 ## Entry Points
 
-### CLI Tool: `check`
+### CLI Tool
 
-**File**: `src/main/check.cpp`
+**File**: `src/main.cpp`
 
 ```bash
-./prevail <elf-file> <section>/<function> [options]
+./bin/prevail <elf-file> <section>/<function> [options]
 ```
 
 Options:
-- `--domain`: Choose abstract domain (e.g., `zoneCrab`)
+- `-q`/`--quiet`: No stdout output, exit code only
+- `--cfg`: Print control-flow graph and exit
+- `--failure-slice`: Print causal trace for failures
+- `-v`: Print invariants and first failure
 - `--no-simplify`: Don't merge basic blocks
 - `--strict`: Require explicit map bounds
 

docs/building.md

@@ -119,7 +119,6 @@ After building, you'll find these executables in `bin/`:
 | Executable | Description |
 |------------|-------------|
 | `prevail` | Main verifier CLI tool |
-| `check` | Backwards-compatible alias for `prevail` |
 | `tests` | Catch2 test runner |
 | `run_yaml` | YAML test case runner |
 

docs/failure-slicing.md

@@ -472,4 +472,4 @@ verification failures. When using failure slices with an LLM:
 | `src/fwd_analyzer.cpp` | Hooks to populate deps during forward analysis |
 | `src/ir/parse.cpp` | Invariant filter integration in `operator<<(StringInvariant)` |
 | `src/config.hpp` | `collect_instruction_deps` flag |
-| `src/main/check.cpp` | `--failure-slice` and `--failure-slice-depth` CLI flags |
+| `src/main.cpp` | `--failure-slice` and `--failure-slice-depth` CLI flags |

scripts/.check-license.ignore

@@ -47,8 +47,6 @@ external/catch.hpp
 # Files using BSD-3-Clause
 external/CLI11/CLI11.hpp
 
-# Files using CC-BY-SA-2.5 license
-src/main/memsize_linux.hpp
 
 # Files with custom licenses embedded
 src/crab_utils/heap.hpp