vbpf / prevail / 24571609553
86%

DEFAULT BRANCH: main
Ran
Jobs 2
Files 107
Run time 1min
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst
coverage: 89.022% (-0.09%) from 89.111%
24571609553

push

github

web-flow 
Pass explicit AnalysisContext; treat VariableRegistry as a global service (#1088)

* Introduce AnalysisContext to thread explicit verification state

Wrap the thread-local analysis inputs (ProgramInfo, options, platform,
VariableRegistry) in a single AnalysisContext aggregate, and plumb it
explicitly through analyze, ebpf_domain_check, ebpf_domain_transform,
and ebpf_domain_initialize_loop_counter. Backward-compatible overloads
continue to synthesize the context from thread-locals.

This is a migration step: EbpfDomain internals and a few helpers in
ebpf_domain.cpp still reach the thread-locals, so analyze asserts that
the caller-supplied VariableRegistry matches variable_registry.get().

* Unify ptr_max on an explicit max_packet_size argument, fold transformer helpers into instance methods

- ptr_max() in ebpf_domain.hpp now takes max_packet_size directly and
  no longer reads thread_local_options. The only remaining callers
  pass thread_local_options.max_packet_size (in ebpf_domain.cpp) or
  context.options.max_packet_size (in ebpf_transformer.cpp). The
  duplicate static ptr_max(context) in ebpf_transformer.cpp is gone.
- max_packet_size() helper removed; its sole caller inlines
  thread_local_options.max_packet_size, making the dependency visible.
- do_load_stack, do_store_stack, recompute_stack_numeric_size were
  static helpers taking an AnalysisContext and ArrayDomain. Since
  EbpfTransformer already holds both as members and is always
  constructed per-instruction, convert them to non-static methods
  that use this->stack and this->context.

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

* Thread AnalysisContext into EbpfDomain::setup_entry, from_constraints, initialize_packet

These entry-point domain methods previously read thread_local_options,
variable_registry, and thread_local_program_info directly. They now
receive them explicitly via AnalysisContext.

- setup_en... (continued)

378 of 415 new or added lines in 25 files covered. (91.08%)

16 existing lines in 8 files now uncovered.

13445 of 15103 relevant lines covered (89.02%)

4467212.83 hits per line

Uncovered Changes

Lines Coverage ∆ File
10
80.65
 -0.2% src/crab/ebpf_domain.cpp
7
76.52
 0.38% src/result.cpp
6
91.96
 0.03% src/crab/ebpf_transformer.cpp
5
89.11
 -0.7% src/crab/ebpf_checker.cpp
3
86.52
 0.0% src/ir/parse.cpp
2
90.24
 -0.23% src/crab/type_domain.cpp
2
85.53
 -5.65% src/crab/var_registry.cpp
2
57.63
 -0.04% src/printing.cpp

Coverage Regressions

Lines Coverage ∆ File
6
91.55
 -1.18% src/crab/zone_domain.cpp
4
85.53
 -5.65% src/crab/var_registry.cpp
1
88.41
 0.23% src/crab/array_domain.cpp
1
91.94
 -0.37% src/crab/bitset_domain.hpp
1
89.11
 -0.7% src/crab/ebpf_checker.cpp
1
90.24
 -0.23% src/crab/type_domain.cpp
1
88.46
 0.26% src/crab/type_to_num.cpp
1
78.95
 -5.26% src/string_constraints.hpp
Jobs
ID Job ID Ran Files Coverage
1 run-Release - 24571609553.1 107
88.22
 GitHub Action Run
2 run-Debug - 24571609553.2 107
87.28
 GitHub Action Run
Source Files on build 24571609553