Remove thread_local_options; pass options explicitly

[elazarg]

Summary

• Thread big_endian and total_stack_size through ArrayDomain methods (load, store, havoc, split_cell, split_number_var) instead of reading thread_local_options. Derive total_stack_size from ArrayDomain's own BitsetDomain::size()
• Add analyze(prog, options) and verify(prog, options) overloads; remove the no-options shims that read thread_local_options
• Pass print_line_info explicitly through all print functions (print_program, print_invariants, print_error, print_invariants_filtered, print_failure_slices)
• Remove thread_local_options variable, extern declaration, and all test harness assignments
• Replace test macro thread_local_options usage with local variables or default {}

Continues #1091. Together with that PR, this eliminates all semantic thread-local state from the verifier. The only remaining thread-locals are domain-internal caches (thread_local_array_map, SplitDBM::scratch_) that are per-analysis scratch space, not semantic inputs.

Closes #1077.

Test plan

• Full test suite passes with seed 2276513626
• Codex review clean (one finding about print_failure_slices not forwarding print_line_info — fixed)

🤖 Generated with Claude Code

[coderabbitai]

Warning

Rate limit exceeded

@elazarg has exceeded the limit for the number of commits that can be reviewed per hour. Please wait 49 minutes and 54 seconds before requesting another review.

Your organization is not enrolled in usage-based pricing. Contact your admin to enable usage-based pricing to continue reviews beyond the rate limit, or try again in 49 minutes and 54 seconds.

⌛ How to resolve this issue?

After the wait time has elapsed, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

We recommend that you space out your commits to avoid hitting the rate limit.

🚦 How do rate limits work?

CodeRabbit enforces hourly rate limits for each developer per organization.

Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout.

Please see our FAQ for further information.

ℹ️ Review info

⚙️ Run configuration

Configuration used: Repository UI

Review profile: ASSERTIVE

Plan: Pro

Run ID: 350e4e99-191c-4ba4-90ea-aee99ef08a55

📥 Commits

Reviewing files that changed from the base of the PR and between dd4197d and 02f532b.

📒 Files selected for processing (14)

• src/config.hpp
• src/fwd_analyzer.cpp
• src/ir/cfg_builder.cpp
• src/ir/program.hpp
• src/main.cpp
• src/printing.cpp
• src/result.hpp
• src/test/ebpf_yaml.cpp
• src/test/test_elf_loader.cpp
• src/test/test_marshal.cpp
• src/test/test_print.cpp
• src/test/test_verify.hpp
• src/test/test_verify_multithreading.cpp
• src/verifier.hpp

📝 Walkthrough

Walkthrough

Removes thread-local global state (thread_local_options) and threads explicit ebpf_verifier_options_t, big_endian, and print_line_info parameters through analysis, transformation, and printing functions to eliminate hidden semantic dependencies in core code paths.

Changes

Cohort / File(s)	Summary
Thread-local state removal src/config.hpp, src/fwd_analyzer.cpp, src/ir/cfg_builder.cpp, src/verifier.hpp	Removed extern thread_local ebpf_verifier_options_t thread_local_options declaration and eliminated convenience overloads of analyze() and verify() that relied on implicit thread-local state; callers must now pass options explicitly.
Array domain endianness threading src/crab/array_domain.hpp, src/crab/array_domain.cpp	Added total_stack_size() method to ArrayDomain and threaded bool big_endian parameter through load(), store(), havoc(), split_cell(), and split_number_var() signatures; removed overloads without this parameter and replaced thread_local_options.total_stack_size() reads with explicit total_stack_size() calls.
Bitset domain API src/crab/bitset_domain.hpp	Added size() const noexcept public method to BitsetDomain returning underlying byte count.
Transformer option threading src/crab/ebpf_transformer.cpp	Threaded context.options.big_endian into stack memory operations (load(), store(), havoc()) for endian-aware semantics during value manipulation.
Printing API refactoring src/ir/program.hpp, src/printing.cpp, src/result.hpp, src/main.cpp	Extended print_program(), print_invariants(), print_error(), print_invariants_filtered(), and print_failure_slices() signatures with bool print_line_info parameter; updated DetailedPrinter constructor and all call sites to accept and forward this parameter instead of reading thread_local_options.verbosity_opts.print_line_info.
Test cleanup src/test/ebpf_yaml.cpp, src/test/test_elf_loader.cpp, src/test/test_marshal.cpp, src/test/test_print.cpp, src/test/test_verify.hpp, src/test/test_verify_multithreading.cpp	Removed per-test thread_local_options = {} assignments; updated all unmarshal(), verify(), and analyze() calls to pass explicit ebpf_verifier_options_t{} or _prevail_opts arguments; threaded total_stack_size parameter through stack invariant construction helpers.

Possibly related PRs

• vbpf/prevail#1070: Removes thread-local option access in array-domain stack-size handling and replaces it with explicit total_stack_size() parameter threading.
• vbpf/prevail#946: Adds explicit ebpf_verifier_options_t propagation and gates print_line_info through options rather than thread-local state.
• vbpf/prevail#1091: Refactors away thread-local globals across the same code paths (fwd_analyzer, printing, transformer, main.cpp).

Suggested labels

codex, feature

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 28.57% which is insufficient. The required threshold is 80.00%.	Write docstrings for the functions missing them to satisfy the coverage threshold.

✅ Passed checks (4 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title clearly summarizes the main change: removing thread_local_options and passing options explicitly throughout the codebase.
Description check	✅ Passed	The description is comprehensive and directly related to the changeset, detailing how thread_local_options is removed and how options are threaded through functions.
Linked Issues check	✅ Passed	The PR fully addresses the linked issue #1077 by removing thread_local_options from ArrayDomain methods, adding explicit analyze/verify overloads, and threading print_line_info through all print functions.
Out of Scope Changes check	✅ Passed	All changes are directly aligned with the stated objectives of removing thread_local_options and making options explicit; no unrelated modifications detected.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch remove-thread-local-options

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[coderabbitai]

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@src/test/ebpf_yaml.cpp`:
- Around line 526-541: The comparison between memory_bytes.size() (size_t) and
options.total_stack_size() (int) is a signed/unsigned mismatch; change the guard
to first validate options.total_stack_size() is non-negative, then use a size_t
cast for comparisons and for stack_contents_invariant calls (e.g., use
static_cast<size_t>(options.total_stack_size()) when comparing
memory_bytes.size() and when calling stack_contents_invariant), and if
total_stack_size() is negative return an error early; refer to
memory_bytes.size(), options.total_stack_size(), stack_contents_invariant(), and
pre_invariant to locate the changes.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Repository UI

Review profile: ASSERTIVE

Plan: Pro

Run ID: e130a5af-07bc-4572-bb63-32cfc40c1d95

📥 Commits

Reviewing files that changed from the base of the PR and between 4465b3f and dd4197d.

📒 Files selected for processing (18)

• src/config.hpp
• src/crab/array_domain.cpp
• src/crab/array_domain.hpp
• src/crab/bitset_domain.hpp
• src/crab/ebpf_transformer.cpp
• src/fwd_analyzer.cpp
• src/ir/cfg_builder.cpp
• src/ir/program.hpp
• src/main.cpp
• src/printing.cpp
• src/result.hpp
• src/test/ebpf_yaml.cpp
• src/test/test_elf_loader.cpp
• src/test/test_marshal.cpp
• src/test/test_print.cpp
• src/test/test_verify.hpp
• src/test/test_verify_multithreading.cpp
• src/verifier.hpp

💤 Files with no reviewable changes (5)

• src/config.hpp
• src/ir/cfg_builder.cpp
• src/verifier.hpp
• src/fwd_analyzer.cpp
• src/test/test_elf_loader.cpp