Pass explicit AnalysisContext; treat VariableRegistry as a global service

[elazarg]

Summary

Reshapes the verifier's analysis API to thread per-analysis state explicitly via a new AnalysisContext struct (program_info, options, platform), and corrects the modeling of VariableRegistry as a global name-interning service rather than per-analysis state.

The branch grew through several refactor steps that, taken together, replace the implicit thread-local environment with explicit parameters wherever the data is genuinely per-analysis, and clarify the responsibilities of the registry where it isn't.

Why

Before this branch, the analyzer reached for thread_local_options, thread_local_program_info, and variable_registry from arbitrary depths in the call graph. That made:

• the dependencies of EbpfDomain, EbpfChecker, EbpfTransformer opaque;
• testing harder (every test sets up the thread-locals);
• the registry's role unclear (used both as an interner and, incorrectly, as a per-analysis state oracle).

Two semantic bugs surfaced from that confusion:

• EbpfDomain::get_loop_count_upper_bound() queried variable_registry.get_loop_counters(), which after the registry-as-global reframing accumulated counters across analyses. Stale counters evaluated to top in current state, sending max_loop_count silently to INT_MAX.
• EbpfDomain::from_constraints could leave state bottom while stack stayed materialized — to_set() then printed stack content instead of _|_.

Both are fixed.

What changed

• AnalysisContext carries the three things that vary per analysis. VariableRegistry deliberately isn't a member: it's a global interning service (no clearing, no LazyAllocator wrapper, never threaded as state).
• Domain construction is context-aware: top(context) / top(size_t), setup_entry(bool, context), both from_constraints overloads, calculate_constant_limits(context, loop_counters), widen(other, to_constants, context, loop_counters). Sized BitsetDomain(size_t) / ArrayDomain(size_t) ctors; default ctors removed.
• EbpfDomain::stack becomes std::optional<ArrayDomain> with the invariant state.is_bottom() ⇔ !stack.has_value(). Bottom default-construction needs no thread-local read. BitsetDomain and ArrayDomain lose their fake is_bottom/set_to_bottom (the bottom concept now lives only at EbpfDomain).
• State-mutating methods on EbpfDomain (add_value_constraint, assume_eq_types, restrict_type) maintain the invariant via a single normalize_after_state_mutation helper.
• Loop counters are sourced from the analyzer's Wto (per-program loop heads), not from the registry.
• Type variables are sourced from TypeDomain::variables() / variables_with_type(type) (per-state tracked vars), not from variable_registry.get_type_variables() (which is removed).
• VariableRegistry is now: non-copyable, all methods const over a mutable interning cache, make renamed to intern. RegPack and reg_pack moved here from type_to_num.hpp.
• Other thread-local reads in adjacent code (extract_instruction_deps, RelevantState, get_assertions, Unmarshaller, cfg_builder, result.cpp) take their inputs explicitly.

Known leftover

EbpfDomain::to_set() still serializes a bottom domain as top, with a BUG: comment, to satisfy YAML test expectations encoded in post: []. Real fix is to return bottom and update the YAML expectations — left as a follow-up.

Test plan

• Full test suite passes: 1296 / 236 expected-fail / 1 skipped.
• Loop-counter-bound bug verified by inspection (no test pinned the value before).
• Independent code review pass; one invariant hole found and fixed before opening this PR.

🤖 Generated with Claude Code

[coderabbitai]

📝 Walkthrough

Walkthrough

Adds prevail::AnalysisContext and threads it through analysis, checker, transformer, and domain APIs; replaces many thread-local/global accesses with context or registry instance methods; converts stack/bitset domains to size-constructed, non-bottom-intrinsic types and represents stack bottom via std::optional; updates related signatures and tests.

Changes

Cohort / File(s)	Summary
Context/Infrastructure src/analysis_context.hpp, src/verifier.hpp	Introduce prevail::AnalysisContext, thread_local_analysis_context() helper, and new analyze overloads accepting an AnalysisContext.
Core EbpfDomain API src/crab/ebpf_domain.hpp, src/crab/ebpf_domain.cpp	Make stack an std::optional<ArrayDomain>, add context-aware APIs (top/widen/calculate_constant_limits/setup_entry/from_constraints/initialize_packet/get_map_*), normalize bottom/stack invariant, change ptr_max signature, remove thread-local constant machinery.
Checker & Transformer src/crab/ebpf_checker.cpp, src/crab/ebpf_transformer.cpp	Inject const AnalysisContext& into EbpfChecker/EbpfTransformer; add context parameters to ebpf_domain_check/ebpf_domain_transform and replace thread-local program/options/platform usage.
Array / Bitset Domains src/crab/array_domain.hpp, src/crab/array_domain.cpp, src/crab/bitset_domain.hpp, src/crab/bitset_domain.cpp	Require explicit size constructors, remove intrinsic bottom APIs (set_to_bottom/is_bottom), adjust to_set semantics and document bottom represented externally.
Variable Registry & RegPack src/crab/var_registry.hpp, src/crab/var_registry.cpp	Switch make→intern, mark many accessors const, add RegPack and reg_pack(int) const, replace thread_local LazyAllocator with thread_local VariableRegistry.
Registry Call-site Adjustments src/crab/finite_domain.cpp, src/crab/type_domain.cpp, src/crab/type_domain.hpp, src/crab/type_to_num.cpp, src/crab/type_to_num.hpp, src/crab/zone_domain.cpp	Replace variable_registry->... with variable_registry...., add TypeDomain::variables() and variables_with_type(), adapt type-to-num iteration and reg_pack delegation to registry instance.
Forward Analyzer / Analysis Entrypoints src/fwd_analyzer.cpp, src/result.cpp, src/result.hpp	Interleaved forward iterator and analyze overloads accept/store AnalysisContext; compute per-analysis loop-counters; propagate context into widen/extrapolate/check/transform calls; add total_stack_size plumbing to extract_instruction_deps/RelevantState.
IR, CFG, Assertions, Unmarshal src/ir/assertions.cpp, src/ir/program.hpp, src/ir/cfg_builder.cpp, src/ir/parse.cpp, src/ir/unmarshal.cpp	get_assertions now takes options; CFG and pseudo resolution use ProgramInfo and limits from options; parse/unmarshal and Unmarshaller use instance-registry/options instead of thread-locals.
Printing & Reporting src/printing.cpp	Printing updated to use member-access registry APIs; join relevance copies total_stack_size for correct relevance unions.
Tests src/test/test_elf_loader.cpp, src/test/test_failure_slice.cpp, src/test/test_marshal.cpp	Update tests to pass explicit stack-size and options/context where required; minor formatting simplification in one test.
Misc: small API/site changes src/crab/array_domain.cpp, src/crab/bitset_domain.cpp, various crab sources	Remove/adjust bottom-handling methods; replace pointer-style registry access with direct instance access across numerous files.

Possibly related issues

• Make analysis dependencies explicit with an AnalysisContext #1077: Implements an AnalysisContext and propagates it through analyzer/checker/transformer/domain APIs, matching this PR’s objective.

Possibly related PRs

• Fix spurious widening precision loss in EbpfDomain (#1071) #1072: Modifies EbpfDomain::widen and constant-limit handling; strongly intersects with this PR’s widen/constant-limit/context changes.
• Refactor variables+numbers #886: Refactors VariableRegistry and related APIs; directly related to reg_pack/intern/const changes in this PR.
• Make stack size and call depth runtime parameters #1070: Migrates stack-size/config to runtime options and updates Bitset/Array domain constructors; overlaps with this PR’s stack/bitset/domain refactors.

Suggested labels

feature

Suggested reviewers

• dthaler

🚥 Pre-merge checks | ✅ 2 | ❌ 1

❌ Failed checks (1 warning)

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

✅ Passed checks (2 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title clearly summarizes the main architectural change: threading AnalysisContext explicitly and reclassifying VariableRegistry as a global service.
Description check	✅ Passed	The description thoroughly explains the rationale, semantic bugs fixed, key API changes, and implementation details, directly relating to the changeset.

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

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch verification-context

---

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: 9

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (5)

src/crab/type_to_num.cpp (1)

114-128: 🧹 Nitpick | 🔵 Trivial

Iterating types.variables() instead of every registered type var is a precision improvement — worth noting soundness explicitly.

The previous implementation walked all registry-wide type variables; the new one only walks variables tracked in this. For an untracked variable, the abstract type is top (any type is possible), so none of its kinds are "nonexistent" and no havoc of tmp.values is warranted — meaning this change makes operator<= strictly stricter (less likely to return true spuriously), which is sound.

As per coding guidelines: "Any change that affects analysis results should spell out the argument for soundness: what inputs are assumed, what invariants are maintained, and how the change preserves them." Consider adding a one-liner comment on line 116 capturing that reasoning so auditors don't have to re-derive it.

🤖 Prompt for AI Agents

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

In `@src/crab/type_to_num.cpp` around lines 114 - 128, Add a one-line comment
inside TypeToNumDomain::get_nonexistent_kind_variables (near the loop over
types.variables()) explaining that we intentionally iterate only the variables
tracked in this->types (not all registry-wide type vars) because untracked
variables are treated as top (all types possible) so no kinds are "nonexistent"
for them; mention that this preserves soundness for operator<= and prevents
spurious inclusion in tmp.values, and reference type_to_kinds and
variable_registry.kind_var for context.

src/result.hpp (1)

66-74: ⚠️ Potential issue | 🟡 Minor

total_stack_size = 0 default is a silent-wrong-answer hazard.

RelevantState is passed around by value and constructed in several places (e.g., join_relevance on printing.cpp:815, where only the primary label's field is copied into the merged state). A zero default means any code path that forgets to seed it will quietly translate relative offsets against a stack size of 0 rather than failing loudly.

Either drop the default and force callers to supply it, or make translation assert total_stack_size > 0 before using it. A short comment here stating "must match options.total_stack_size() of the owning analysis" would also help.

🤖 Prompt for AI Agents

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

In `@src/result.hpp` around lines 66 - 74, RelevantState's total_stack_size must
not default to 0 because callers sometimes copy/construct it without seeding and
that silently produces wrong translations; remove the "= 0" default, add an
explicit constructor (e.g., RelevantState(int total_stack_size)) that
initializes total_stack_size and keeps registers/stack_offsets
default-initialized, update all call sites that create RelevantState (including
the merge in join_relevance) to pass the correct options.total_stack_size(), and
add a short comment on the field that it must match options.total_stack_size()
of the owning analysis.

src/crab/var_registry.cpp (1)

232-240: 🧹 Nitpick | 🔵 Trivial

get_loop_counters() does a redundant O(n) lookup per counter and matches too loose a prefix.

Each matching name is re-interned via intern(name), which scans the entire names vector again — so this is O(n²) in the number of interned names, even though we already know the index while iterating. Also, loop_counter(label) produces "pc[" + label + "]", but the filter uses bare "pc", which would falsely match any future name starting with pc (e.g. pc_whatever).

♻️ Proposed refactor

 std::vector<Variable> VariableRegistry::get_loop_counters() const {
     std::vector<Variable> res;
-    for (const std::string& name : names) {
-        if (name.starts_with("pc")) {
-            res.push_back(intern(name));
-        }
+    for (size_t i = 0; i < names.size(); ++i) {
+        if (names[i].starts_with("pc[")) {
+            res.push_back(Variable(i));
+        }
     }
     return res;
 }

🤖 Prompt for AI Agents

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

In `@src/crab/var_registry.cpp` around lines 232 - 240, The get_loop_counters()
implementation currently re-interns each matching name causing O(n²) work and
uses too-broad prefix "pc"; change VariableRegistry::get_loop_counters to
iterate with an index over names, match the exact "pc[" prefix (since
loop_counter(label) formats as "pc[" + label + "]"), and construct Variables
directly from the known index/slot rather than calling intern(name) again so you
avoid the extra scan.

src/crab/ebpf_domain.cpp (2)

289-308: ⚠️ Potential issue | 🟠 Major

Wrong field compared in get_map_inner_map_fd — map->type vs. accumulated inner_map_fd.

After seeding inner_map_fd = map->inner_map_fd, subsequent iterations compare map->type != *inner_map_fd instead of map->inner_map_fd != *inner_map_fd. That means the consistency check across the fd range is effectively checking the wrong descriptor field: two maps whose inner_map_fd values differ will pass this guard as long as their types happen to match the first seen inner_map_fd (and vice versa). The function can then return a spurious "agreed" inner_map_fd, which is a soundness hazard for any caller keying off it.

Likely pre-existing, but worth fixing in this PR since the signature is being reworked here anyway.

🐛 Proposed fix

         if (!inner_map_fd.has_value()) {
             inner_map_fd = map->inner_map_fd;
-        } else if (map->type != *inner_map_fd) {
+        } else if (map->inner_map_fd != *inner_map_fd) {
             return {};
         }

As per coding guidelines: "Any change that affects analysis results should spell out the argument for soundness: what inputs are assumed, what invariants are maintained, and how the change preserves them."

🤖 Prompt for AI Agents

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

In `@src/crab/ebpf_domain.cpp` around lines 289 - 308, The function
get_map_inner_map_fd seeds inner_map_fd from map->inner_map_fd but then
erroneously compares map->type to *inner_map_fd; change the consistency check so
each subsequent iteration compares map->inner_map_fd to *inner_map_fd (not
map->type) and return {} on mismatch. Locate the loop in get_map_inner_map_fd,
keep the initial seeding of inner_map_fd from map->inner_map_fd, and replace the
map->type != *inner_map_fd condition with map->inner_map_fd != *inner_map_fd to
ensure the returned inner_map_fd is consistent across the full fd range obtained
via get_map_fd_range and platform.get_map_descriptor.

---

267-286: ⚠️ Potential issue | 🟡 Minor

Dead null check on a reference-returning accessor.

platform.get_map_descriptor(map_fd) returns a reference, so &platform.get_map_descriptor(...) is never null and the if (map == nullptr) return {}; guard is unreachable. Same pattern at lines 297, 319, 337, 355. Pre-existing, but now that platform is passed explicitly the contract is clearer — either drop the dead branch, or switch to a nullable API if invalid fds should produce {} instead of relying on whatever get_map_descriptor does internally for unknown fds.

🤖 Prompt for AI Agents

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

In `@src/crab/ebpf_domain.cpp` around lines 267 - 286,
platform.get_map_descriptor(...) returns a reference so taking its address and
checking for nullptr is dead code; change the local variable to a reference
(EbpfMapDescriptor& map = platform.get_map_descriptor(map_fd)) and remove the
unreachable if (map == nullptr) return {} check in EbpfDomain::get_map_type, and
apply the same fix to the other similar sites where you use
&platform.get_map_descriptor(...) (the checks at the other occurrences should be
removed or replaced by reference usage). If the intended semantics are to handle
invalid fds, instead change/get_map_descriptor to return a nullable type
(pointer or std::optional) and update callers accordingly — pick one approach
and make it consistent across all occurrences.

🤖 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/analysis_context.hpp`:
- Around line 20-24: AnalysisContext contains non-owning const references
(program_info, options, platform) and can silently dangle if the referents are
shorter-lived; add a one-line doc comment immediately above struct
AnalysisContext clarifying the lifetime contract (e.g., that an AnalysisContext
is non-owning and must not outlive the ProgramInfo/options/platform used to
construct it and must not be cached beyond the creating analysis call), and
optionally add a brief TODO or assertion location comment where AnalysisContext
instances are created to remind callers to enforce that precondition; reference
the struct AnalysisContext and its members program_info, options, platform in
the comment.
- Around line 5-10: Remove the unused include of "crab/var_registry.hpp" from
the top of analysis_context.hpp: delete the `#include` "crab/var_registry.hpp"
line so AnalysisContext and its doc comment about variable_registry remain but
the registry header is not pulled in transitively; verify no symbols from
var_registry are referenced in the file (if any are, replace with a forward
declaration or adjust references) and run a rebuild to ensure no missing
dependencies.

In `@src/crab/ebpf_checker.cpp`:
- Around line 221-225: The checks in ebpf_checker.cpp use
context.program_info.callback_target_labels and callback_targets_with_exit but
Program::from_sequence() currently builds those sets on
thread_local_program_info, so the AnalysisContext's ProgramInfo stays empty and
valid callbacks are rejected; move the derived metadata population into the
ProgramInfo instance that AnalysisContext carries (or into Program) so that
context.program_info.callback_target_labels and
context.program_info.callback_targets_with_exit are populated before
ebpf_checker.cpp's checks run, ensuring the checks see the same sets regardless
of explicit-context vs thread-local paths (update Program::from_sequence() or
the code that constructs ProgramInfo to fill these fields, and remove reliance
on thread_local_program_info).

In `@src/crab/ebpf_domain.cpp`:
- Around line 22-31: EbpfDomain::to_set currently returns StringInvariant::top()
when stack is null to satisfy existing YAML tests, but it should return
StringInvariant::bottom(); change the return in EbpfDomain::to_set from
StringInvariant::top() to StringInvariant::bottom() and update any dependent
logic as needed, and create a tracking artifact (issue or PR stub) referencing
this change and the required YAML test updates so the test expectations (post:
[]) are amended in the same change; use the symbols EbpfDomain::to_set,
StringInvariant::bottom(), StringInvariant::top() in the tracking description.

In `@src/crab/ebpf_domain.hpp`:
- Around line 128-133: The comment claims all mutators maintain the
`state.is_bottom() <=> !stack` invariant via normalize_after_state_mutation, but
havoc(Variable) (implemented as state.values.havoc(var)) does not call
normalize_after_state_mutation; either defensively invoke
normalize_after_state_mutation() at the end of havoc(Variable) in
ebpf_domain.cpp to preserve the documented invariant (call
normalize_after_state_mutation() after state.values.havoc(var)), or update the
comment in ebpf_domain.hpp to exclude havoc from that group and add a short
rationale referencing havoc/ state.values.havoc explaining why it cannot drive
the numeric domain to bottom so the invariant still holds.

In `@src/crab/ebpf_transformer.cpp`:
- Around line 32-36: The constructor for EbpfTransformer currently
unconditionally dereferences _dom.stack (stack(*_dom.stack)) which can occur
when entry_inv is bottom; fix by guarding creation: before constructing
EbpfTransformer in ebpf_domain_transform (and the other site referenced around
1493-1495), check that _dom.stack has a value (e.g., if (!_dom.stack)
return/skip/handle bottom) or ensure entry_inv is satisfiable; alternatively
change EbpfTransformer to not dereference in its initializer (store a
pointer/optional reference to _dom.stack and only .value() after entry_inv is
confirmed non-bottom inside EbpfTransformer::run()). Ensure you update all
construction sites (including the ones noted) accordingly.

In `@src/crab/type_to_num.cpp`:
- Around line 209-218: The function
TypeToNumDomain::havoc_all_locations_having_type currently assumes
TypeDomain::variables_with_type returns empty when bottom; make that
precondition explicit by checking the domain bottom state at the start of
havoc_all_locations_having_type — e.g., add an assert(!is_bottom()) (or an
explicit if (is_bottom()) return;) and a short comment referencing the reliance
on variables_with_type's contract so the function fails fast if bottom-handling
changes in the future. Ensure the check uses TypeToNumDomain::is_bottom() to
locate the contract enforcement.

In `@src/result.cpp`:
- Around line 114-116: The AnalysisResult code currently rebuilds
AnalysisContext from thread_local_analysis_context() (see the calls near
EbpfDomain::from_constraints in result.cpp and the similar sites at 130-134 and
386-387), which causes results to depend on ambient TLS; change the
implementation to stop reading TLS: either fetch the AnalysisContext stored on
the AnalysisResult instance (add or use an existing member) or require an
explicit AnalysisContext parameter to the function that creates the EbpfDomain,
and pass that context into EbpfDomain::from_constraints instead of calling
thread_local_analysis_context(); update all similar call sites (the three
locations noted) to use the stored/explicit context.

In `@src/test/test_elf_loader.cpp`:
- Line 562: The SECTION call is on a single line while other SECTION blocks use
multi-line formatting; change SECTION("0x80000000 exceeds int32 — bails out
without mutation") { check_bailout_preserves_program(0x80000000ULL); } to the
same multi-line style used elsewhere (open SECTION on its own line, put the
check_bailout_preserves_program(0x80000000ULL); call on the next line, then
close the SECTION block on its own line) so the SECTION and the call to
check_bailout_preserves_program remain consistently formatted with surrounding
tests.

---

Outside diff comments:
In `@src/crab/ebpf_domain.cpp`:
- Around line 289-308: The function get_map_inner_map_fd seeds inner_map_fd from
map->inner_map_fd but then erroneously compares map->type to *inner_map_fd;
change the consistency check so each subsequent iteration compares
map->inner_map_fd to *inner_map_fd (not map->type) and return {} on mismatch.
Locate the loop in get_map_inner_map_fd, keep the initial seeding of
inner_map_fd from map->inner_map_fd, and replace the map->type != *inner_map_fd
condition with map->inner_map_fd != *inner_map_fd to ensure the returned
inner_map_fd is consistent across the full fd range obtained via
get_map_fd_range and platform.get_map_descriptor.
- Around line 267-286: platform.get_map_descriptor(...) returns a reference so
taking its address and checking for nullptr is dead code; change the local
variable to a reference (EbpfMapDescriptor& map =
platform.get_map_descriptor(map_fd)) and remove the unreachable if (map ==
nullptr) return {} check in EbpfDomain::get_map_type, and apply the same fix to
the other similar sites where you use &platform.get_map_descriptor(...) (the
checks at the other occurrences should be removed or replaced by reference
usage). If the intended semantics are to handle invalid fds, instead
change/get_map_descriptor to return a nullable type (pointer or std::optional)
and update callers accordingly — pick one approach and make it consistent across
all occurrences.

In `@src/crab/type_to_num.cpp`:
- Around line 114-128: Add a one-line comment inside
TypeToNumDomain::get_nonexistent_kind_variables (near the loop over
types.variables()) explaining that we intentionally iterate only the variables
tracked in this->types (not all registry-wide type vars) because untracked
variables are treated as top (all types possible) so no kinds are "nonexistent"
for them; mention that this preserves soundness for operator<= and prevents
spurious inclusion in tmp.values, and reference type_to_kinds and
variable_registry.kind_var for context.

In `@src/crab/var_registry.cpp`:
- Around line 232-240: The get_loop_counters() implementation currently
re-interns each matching name causing O(n²) work and uses too-broad prefix "pc";
change VariableRegistry::get_loop_counters to iterate with an index over names,
match the exact "pc[" prefix (since loop_counter(label) formats as "pc[" + label
+ "]"), and construct Variables directly from the known index/slot rather than
calling intern(name) again so you avoid the extra scan.

In `@src/result.hpp`:
- Around line 66-74: RelevantState's total_stack_size must not default to 0
because callers sometimes copy/construct it without seeding and that silently
produces wrong translations; remove the "= 0" default, add an explicit
constructor (e.g., RelevantState(int total_stack_size)) that initializes
total_stack_size and keeps registers/stack_offsets default-initialized, update
all call sites that create RelevantState (including the merge in join_relevance)
to pass the correct options.total_stack_size(), and add a short comment on the
field that it must match options.total_stack_size() of the owning analysis.

🪄 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: 3c0686dc-13ed-4737-ab14-d4fdffae0d13

📥 Commits

Reviewing files that changed from the base of the PR and between ac03ef6 and 6141700.

📒 Files selected for processing (30)

• src/analysis_context.hpp
• src/crab/array_domain.cpp
• src/crab/array_domain.hpp
• src/crab/bitset_domain.cpp
• src/crab/bitset_domain.hpp
• src/crab/ebpf_checker.cpp
• src/crab/ebpf_domain.cpp
• src/crab/ebpf_domain.hpp
• src/crab/ebpf_transformer.cpp
• src/crab/finite_domain.cpp
• src/crab/type_domain.cpp
• src/crab/type_domain.hpp
• src/crab/type_to_num.cpp
• src/crab/type_to_num.hpp
• src/crab/var_registry.cpp
• src/crab/var_registry.hpp
• src/crab/zone_domain.cpp
• src/fwd_analyzer.cpp
• src/ir/assertions.cpp
• src/ir/cfg_builder.cpp
• src/ir/parse.cpp
• src/ir/program.hpp
• src/ir/unmarshal.cpp
• src/printing.cpp
• src/result.cpp
• src/result.hpp
• src/test/test_elf_loader.cpp
• src/test/test_failure_slice.cpp
• src/test/test_marshal.cpp
• src/verifier.hpp

💤 Files with no reviewable changes (1)

• src/crab/bitset_domain.cpp

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 6141700718

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[coderabbitai]

Actionable comments posted: 2

🤖 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/crab/ebpf_domain.hpp`:
- Around line 100-102: Remove the implicit default for total_stack_size on
EbpfDomain::from_constraints so callers must supply it explicitly: update the
declaration and corresponding definition of EbpfDomain::from_constraints to
remove the default argument (the parameter remains size_t total_stack_size), and
update all call sites (including tests) to pass an explicit value (use
ebpf_verifier_options_t{}.total_stack_size() in tests where the default behavior
is intended). Ensure any overloads or wrappers around from_constraints are
adjusted likewise to avoid implicit defaults.

In `@src/crab/type_to_num.cpp`:
- Around line 135-144: The current code builds type_vars as a std::set which
gives deterministic ordering but incurs O(log n) inserts; change type_vars to a
std::unordered_set<Variable> when collecting from types.variables() and
right.types.variables() to get amortized O(1) inserts (then iterate that
unordered_set when computing per-variable work for join_selective); if
deterministic iteration is actually required downstream (e.g. some future
non-commutative use of values.set(...)), sort the collected elements into a
vector after deduplication before iterating; ensure Variable is hashable
(add/enable a std::hash<Variable> specialization) or fall back to std::set if
hashing isn’t available.

🪄 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: 9bd0b51c-6d06-4fab-a581-a68f1d46cdb1

📥 Commits

Reviewing files that changed from the base of the PR and between 6141700 and 6c4d449.

📒 Files selected for processing (4)

• src/analysis_context.hpp
• src/crab/ebpf_domain.hpp
• src/crab/ebpf_transformer.cpp
• src/crab/type_to_num.cpp

[coderabbitai]

Actionable comments posted: 1

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)

src/result.cpp (1)

430-610: ⚠️ Potential issue | 🔴 Critical

Thread seed_relevance.total_stack_size through every RelevantState insertion into maps—stack constraint filtering is silently broken.

seed_relevance.total_stack_size arrives via parameter but never propagates into visited[current_label], slice_labels[current_label], or join_expansion entries. Every insertion uses default-constructed RelevantState with total_stack_size = 0.

is_relevant_constraint computes absolute stack offsets as total_stack_size + rel_offset (line ~69 in result.cpp). With zeroed total_stack_size, all stack range checks fail silently—constraints involving s[...] get compared against wrong absolute ranges.

Apply the fix at these locations:

• Line 432: existing.total_stack_size = seed_relevance.total_stack_size; after visited[current_label]
• Line 546–549: existing.total_stack_size = seed_relevance.total_stack_size; after slice_labels[current_label]
• Line 555–557: existing.total_stack_size = seed_relevance.total_stack_size; after slice_labels[current_label]
• Lines 594–603: Set total_stack_size when populating join_expansion

🤖 Prompt for AI Agents

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

In `@src/result.cpp` around lines 430 - 610, The RelevantState.total_stack_size
from seed_relevance is not being propagated when inserting into maps, breaking
stack-offset checks; update every place a RelevantState is
default-constructed/merged so its total_stack_size is set to
seed_relevance.total_stack_size: after creating/merging visited[current_label]
set existing.total_stack_size = seed_relevance.total_stack_size; after merging
into slice_labels[current_label] (both in the instruction_contributes branch and
the no-deps branch) set that existing.total_stack_size =
seed_relevance.total_stack_size; and when inserting entries into join_expansion
(both for the join label and for predecessor entries) initialize their
.total_stack_size from seed_relevance.total_stack_size (or from the visited
entry used when copying relevance). Ensure each inserted/merged RelevantState
preserves or copies total_stack_size rather than leaving it zero.

🤖 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/result.hpp`:
- Around line 66-70: The field RelevantState::total_stack_size currently
defaults to 0 which silently mis-translates relative stack offsets; update
RelevantState so total_stack_size has no default (or use an explicit sentinel
like -1) and ensure callers like compute_slice_from_label initialize it from the
seed, then add an assertion at the top of RelevantState::is_relevant_constraint
(assert(total_stack_size >= 0)) before computing abs = total_stack_size +
rel_offset to fail loudly on uninitialized state.

---

Outside diff comments:
In `@src/result.cpp`:
- Around line 430-610: The RelevantState.total_stack_size from seed_relevance is
not being propagated when inserting into maps, breaking stack-offset checks;
update every place a RelevantState is default-constructed/merged so its
total_stack_size is set to seed_relevance.total_stack_size: after
creating/merging visited[current_label] set existing.total_stack_size =
seed_relevance.total_stack_size; after merging into slice_labels[current_label]
(both in the instruction_contributes branch and the no-deps branch) set that
existing.total_stack_size = seed_relevance.total_stack_size; and when inserting
entries into join_expansion (both for the join label and for predecessor
entries) initialize their .total_stack_size from seed_relevance.total_stack_size
(or from the visited entry used when copying relevance). Ensure each
inserted/merged RelevantState preserves or copies total_stack_size rather than
leaving it zero.

🪄 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: 18d38e41-a514-4886-ad2f-17bef043abdf

📥 Commits

Reviewing files that changed from the base of the PR and between 6c4d449 and 9153fed.

📒 Files selected for processing (2)

• src/result.cpp
• src/result.hpp