Narrow comparisons per type and never by a pointer's address

[elazarg]

Fixes #1247. Alternative to #1248 (same checker rule; covers the cases below that #1248 leaves open).

Issues

1. Pointer vs. nonzero scalar register (Prevent pointer addresses from narrowing mixed pointer/scalar comparisons #1247). Comparable ignores or_r2_is_number, so the checker accepts a comparison between a pointer and any number. Before Fix assertion crash in Assume when operands have different types #1037 this hit an assert in Assume; since Fix assertion crash in Assume when operands have different types #1037 it narrows the pointer's svalue/uvalue against the scalar, pruning branches from the modeled address range ([1, ptr_max]), which is not where real pointers live.
2. Unsplit narrowing of a {number, pointer} register. svalue is a number-only kind, so after a join the number side's value (e.g. svalue = 0) remains in the shared state. Applying r7 != 0 to that state without splitting by type kills the pointer path too. On HEAD, r7 = {0, packet} followed by if r7 == 0 hides an out-of-bounds packet read at r7 + 60000. Affects the immediate path and the mixed-type register path.
3. Pointer narrowing that depends on where regions lie. Reachable by privileged programs (no comparison assertions) and other unchecked Assumes: pointer vs. nonzero immediate; signed or 32-bit comparisons of pointers (with zero or with each other); !=/ordering of map-value pointers with equal offsets (different regions); pointers of different types (sent to bottom).
4. Register zero looser than immediate zero. A signed or 32-bit comparison of a pointer with a zero register was accepted; with an immediate zero it is rejected.

Fix

• Checker (Comparable): when the types may differ, a comparison requires the scalar to be exactly zero ([0, 1] is rejected). Subtraction is unchanged.

• Assertions: a signed or 32-bit register comparison requires both operands to be numbers, via the new admits_pointer_operands(Condition), which the immediate-zero case now also uses.

• Transformer (Assume): split both operands by type and narrow only what is independent of region placement:

  operands	narrowing
  number, number	as before
  same pointer type, 64-bit unsigned/equality	offsets: singleton regions any op; map fds ==/!=; other regions == only
  pointer, exact zero (register or immediate), 64-bit unsigned/equality	null check on uvalue
  anything else	none (both branches feasible)

  Soundness no longer depends on the checker, so privileged programs are covered.

issue	#1248	this PR
1	fixed	fixed
2	open (OOB read accepted via immediate and exact-zero register)	fixed
3	open	fixed
4	open	fixed

Behavior changes

• correlated_branch.o (xdp) passed only through issue 2: the packet path was pruned, so its bounds check never ran. Now that path is analysed, and the read fails because the join loses packet_size >= 14, which holds only on the packet path. Marked expected_failure (VerifierTypeTracking).
• jump.yaml "assume reg-vs-reg with different types (ctx == number)": the expected post-state now reads r2.svalue=0 instead of r2.svalue=r1.svalue. Given the pre-state, these mean the same.

Not addressed

• Pointer uvalue still models the address, capped at ptr_max. It now affects verdicts only through null checks, which use its lower bound. A null type, with no uvalue tracking for pointers, is the intended long-term design.
• A separate null-pointer soundness issue found during this audit is tracked separately.

Tests

• src/test/test_assume.cpp: applies implicit (unchecked) Assumes directly; 27 checks. HEAD fails 11; Reject nonzero scalar comparisons with pointers #1248 fails 9.
• jump.yaml: the Prevent pointer addresses from narrowing mixed pointer/scalar comparisons #1247 case; a possibly-pointer register vs. nonzero scalar; a [0, 1] scalar; exact-zero ==/!=/>; signed and 32-bit vs. zero register (rejected); packet-or-zero null check with an out-of-bounds read (rejected). Each rejection test fails on HEAD.
• Full suite: 651 cases, 650 passed, 1 skipped.

🤖 Generated with Claude Code

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-15T06:38:36.309276Z	6e1dbeb	PR opened

ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

• Configuration used: Repository UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: 0067211f-c764-4d4e-820c-96d7fa62ada6

📥 Commits

Reviewing files that changed from the base of the PR and between cefe6a7 and 6e1dbeb.

📒 Files selected for processing: 8

• CMakeLists.txt
• src/crab/ebpf_checker.cpp
• src/crab/ebpf_transformer.cpp
• src/ir/assertions.cpp
• src/ir/syntax.hpp
• src/test/test_assume.cpp
• test-data/elf_inventory.json
• test-data/jump.yaml

Included review availability: This review used your included allowance. Your plan provides up to 2 included reviews per hour; 1 remain after this review.

📝 Walkthrough

Pointer comparison validation and assumptions now distinguish numeric operands, exact-zero comparisons, and compatible pointer types. The changes add unit and jump-test coverage for these cases, including pointer comparisons across regions and types.

Changes: Pointer Comparison Assumptions

Layer / File(s)	Summary
Define comparison operand rules src/ir/syntax.hpp, src/ir/assertions.cpp, src/crab/ebpf_checker.cpp	admits_pointer_operands rejects signed comparisons and admits other comparisons only for 64-bit conditions. Assertion extraction uses this rule to constrain operands. The checker requires exact zero for mixed-type comparisons.
Apply comparison assumptions src/crab/ebpf_transformer.cpp	Assume applies numeric constraints to numeric pairs, offset constraints when pointer offsets decide the comparison, and null-check constraints for exact-zero comparisons. Incompatible nonnumeric comparisons add no constraints.
Validate pointer comparison behavior src/test/test_assume.cpp, test-data/jump.yaml, test-data/elf_inventory.json, CMakeLists.txt	Unit and jump tests cover pointer comparisons with nonzero values, exact zero, signed and 32-bit conditions, and different pointer regions or types. The test inventory records an expected verifier failure for a packet-bounds case, and CMake includes the new unit-test source.

Priority: ➖ Normal

Change: Bug fix · Severity of issue fixed: Medium

Merge Risk: ⚪ Minimal · up to 6e1db

The change tightens mixed pointer and scalar comparison handling and adds regression coverage. No concrete merge-blocking risk was identified from the supplied evidence.

Pre-merge checks: 6 · 1

Failed checks: 1 warning

Check name	Status	Explanation	Resolution
Docstring Coverage		Docstring coverage is 33.33% which is insufficient. The required threshold is 80.00%. Docstring coverage is scoped to functions touched by this diff. Analyzed 15 functions across 5 files. (3 skipped: …	Write docstrings for the functions missing them to satisfy the coverage threshold.

Passed checks: 6 passed

Check name	Status	Explanation
Title check		The title clearly summarizes the primary change: type-aware comparison narrowing that does not depend on pointer addresses.
Description check		The description is detailed and directly explains the mixed pointer/scalar comparison fixes, implementation changes, behavior changes, and tests.
Linked Issues check		The changes address the linked issue objectives by rejecting nonzero scalar comparisons, preserving exact-zero handling, rejecting possibly-zero scalar ranges, and adding regression tests.
Out of Scope Changes check		The modified implementation, tests, and expected-failure updates support the stated comparison-narrowing objectives. No unrelated changes are evident.
Linked Issues check		Issue [#1247] requires rejection of pointer comparisons with nonzero scalars, rejection of scalar ranges that may be zero, and preservation of exact-zero register checks. `EbpfChecker::operator()(cons…
Out of Scope Changes check		The changes remain connected to [#1247]. The Assume updates prevent pointer-address narrowing for unchecked comparisons and for pointer types or regions that the checker cannot safely compare. The a…

Full details: Docstring Coverage

Explanation

Docstring coverage is 33.33% which is insufficient. The required threshold is 80.00%. Docstring coverage is scoped to functions touched by this diff. Analyzed 15 functions across 5 files. (3 skipped: 3 unsupported.)

• Fix all pre-merge checks with AI

✨ Finishing Touches: 💡 1

📝 Generate docstrings: 💡

• Commit to this branch
• Create a new PR

🧪 Generate unit tests (beta)

• Commit to this branch
• Create a new PR

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

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.}

[elazarg]

@mikeagun I think this is a better route than #1248. Does it solve your issue?

[mikeagun]

@mikeagun I think this is a better route than #1248. Does it solve your issue?

Thanks! Yes, this covers the safety issue and I agree this is a better route. I'll close #1248