Fix EbpfDomain::to_set() returning top instead of bottom

[elazarg]

Summary

• EbpfDomain::to_set() returned StringInvariant::top() when the domain is bottom (unreachable), instead of StringInvariant::bottom().
• Updated 225 YAML test expectations across 15 test-data files that encoded the wrong answer (post: [] = top) to the correct post: ["_|_"] (bottom).

Fixes the last item in #1077

Test plan

• All YAML tests pass
• Full test suite passes

🤖 Generated with Claude Code

[coderabbitai]

📝 Walkthrough

Walkthrough

Modified EbpfDomain::to_set() to return bottom instead of top when stack is absent, with corresponding test case updates across 15 YAML test files to explicitly assert bottom (_|_) for failing scenarios instead of empty post-state expectations.

Changes

Cohort / File(s)	Summary
Domain behavior src/crab/ebpf_domain.cpp	Changed EbpfDomain::to_set() to return StringInvariant::bottom() when domain has no stack, replacing prior StringInvariant::top() return with associated comment removal.
Test expectations test-data/assign.yaml, test-data/atomic.yaml, test-data/call.yaml, test-data/callx.yaml, test-data/jump.yaml, test-data/loop.yaml, test-data/movsx.yaml, test-data/packet.yaml, test-data/pointer.yaml, test-data/sdivmod.yaml, test-data/stack.yaml, test-data/subtract.yaml, test-data/udivmod.yaml, test-data/uninit.yaml, test-data/unsigned.yaml	Updated post expectations from empty lists (post: []) to bottom sentinel (post: ["_|_"]) for test cases expecting invalid/unreachable outcomes, including null-access, bounds violations, type errors, division by zero, and uninitialized operand scenarios.

Possibly related PRs

• Fix bpf2bpf local function calls with stack usage #784: Modifies stack-related behavior in src/crab/ebpf_domain.cpp with related null-stack handling.
• Fix spurious widening precision loss in EbpfDomain (#1071) #1072: Addresses bottom/precision semantics in EbpfDomain handling within the same implementation.
• Fail hard when a non-Assume instruction turns an invariant into bottom #791: Related to how domain enters bottom state and when bottom is propagated during analysis.

Suggested labels

precision

Suggested reviewers

• Alan-Jowett

🚥 Pre-merge checks | ✅ 2 | ❌ 3

❌ Failed checks (2 warnings, 1 inconclusive)

Check name	Status	Explanation	Resolution
Out of Scope Changes check	⚠️ Warning	The PR contains a semantic bug fix unrelated to the AnalysisContext migration outlined in #1077, which does not appear to require changes to EbpfDomain::to_set() logic.	Either clarify the relationship to #1077 or reference the correct issue tracking this specific semantic bug fix.
Docstring Coverage	⚠️ Warning	Docstring coverage is 0.00% which is insufficient. The required threshold is 80.00%.	Write docstrings for the functions missing them to satisfy the coverage threshold.
Linked Issues check	❓ Inconclusive	The PR fixes a semantic bug in EbpfDomain::to_set() but issue #1077 focuses on making analysis dependencies explicit via AnalysisContext. The connection is unclear.	Clarify how this fix relates to the AnalysisContext refactoring goals in issue #1077 or link a different issue if this is a separate bug fix.

✅ Passed checks (2 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title accurately summarizes the main change: fixing EbpfDomain::to_set() to return bottom instead of top for unreachable states.
Description check	✅ Passed	The PR description directly addresses the changeset: it explains the bug fix in EbpfDomain::to_set() and documents the 225 YAML test updates that reflect the corrected semantics.

_{✏️ 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 fix-ebpf-domain-to-set-bottom

---

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]

Caution

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

⚠️ Outside diff range comments (1)

test-data/jump.yaml (1)

601-611: ⚠️ Potential issue | 🟠 Major

Missed update: post: [] still here despite unreachable message.

This test case (Lines 601-611) has messages: "0: Code becomes unreachable (assume r1 != r2)", which means the post-state is bottom — identical in shape to the neighbors that were flipped to post: ["_|_"]. Leaving post: [] here is inconsistent with the rest of the PR and, given the corrected EbpfDomain::to_set(), an empty post list now asserts the top invariant rather than bottom, so this case is no longer testing what its messages say it tests.

Side note: the test-case name assume map_fd1 != map_fd2 is also duplicated with Line 587. Worth disambiguating while you're here.

Proposed fix

-post: []
+post:
+  - "_|_"
 messages:
   - "0: Code becomes unreachable (assume r1 != r2)"

🤖 Prompt for AI Agents

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

In `@test-data/jump.yaml` around lines 601 - 611, The test-case named "assume
map_fd1 != map_fd2" has messages indicating the code becomes unreachable
(bottom) but still uses post: [] which now denotes top after the
EbpfDomain::to_set() change; update this test to set post: ["_|_"] (or otherwise
represent bottom) to match the unreachable message, and also rename the
duplicate test-case (the one at lines ~601) to a unique name to avoid collision
with the other "assume map_fd1 != map_fd2" entry; ensure you modify the
test-case's post field and its name consistently so the test asserts bottom as
intended.

🤖 Prompt for all review comments with AI agents

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

Outside diff comments:
In `@test-data/jump.yaml`:
- Around line 601-611: The test-case named "assume map_fd1 != map_fd2" has
messages indicating the code becomes unreachable (bottom) but still uses post:
[] which now denotes top after the EbpfDomain::to_set() change; update this test
to set post: ["_|_"] (or otherwise represent bottom) to match the unreachable
message, and also rename the duplicate test-case (the one at lines ~601) to a
unique name to avoid collision with the other "assume map_fd1 != map_fd2" entry;
ensure you modify the test-case's post field and its name consistently so the
test asserts bottom as intended.

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Repository UI

Review profile: ASSERTIVE

Plan: Pro

Run ID: f64b8003-ff47-4238-b3c0-fc65b552a2a5

📥 Commits

Reviewing files that changed from the base of the PR and between f5466bb and 3bd5e4f.

📒 Files selected for processing (16)

• src/crab/ebpf_domain.cpp
• test-data/assign.yaml
• test-data/atomic.yaml
• test-data/call.yaml
• test-data/callx.yaml
• test-data/jump.yaml
• test-data/loop.yaml
• test-data/movsx.yaml
• test-data/packet.yaml
• test-data/pointer.yaml
• test-data/sdivmod.yaml
• test-data/stack.yaml
• test-data/subtract.yaml
• test-data/udivmod.yaml
• test-data/uninit.yaml
• test-data/unsigned.yaml