vbpf / prevail / 24571609553

push

github

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%)

13445 of 15103 relevant lines covered (89.02%)

4467212.83 hits per line