Fix #1099: tighten ValidMapKeyValue packet bound; inline bounds checks

[elazarg]

Summary

Fixes #1099 and reshapes the bounds-check helpers around it into two primitives that each per-region case composes directly.

The bug

ValidMapKeyValue's T_PACKET branch checked the upper bound against the loose max_packet_size constant, while ValidAccess's T_PACKET dereference path used the runtime variable_registry.packet_size() for a tighter check. Helper map key/value pointers are real reads/writes through the pointer (the helper copies key_size / value_size bytes), so they need the same runtime ceiling as direct dereferences. Using max_packet_size was unsoundly loose: a program could pass verification while accessing past the actual runtime packet_size.

The fix at the call site now reads as one line:

require_upper_bound(ub, variable_registry.packet_size(), "Upper bound must be at most packet_size");

The refactor

Replaced the previous region_bounds / RegionBounds / require_region_bounds apparatus (and a brief detour through templated overloads and a static/dynamic taxonomy) with two trivial member primitives on EbpfChecker:

void require_lower_bound(const LinearExpression& access_lb,
                         const LinearExpression& floor,   const std::string& msg) const;
void require_upper_bound(const LinearExpression& access_ub,
                         const LinearExpression& ceiling, const std::string& msg) const;

Each per-type case (T_STACK, T_CTX, T_PACKET, T_SHARED, T_ALLOC_MEM) in EbpfChecker::operator()(const ValidAccess&) and operator()(const ValidMapKeyValue&) now spells out its floor and ceiling directly at the line where the access is checked, rather than routing through a per-region helper whose contract had to be carried in comments.

ValidAccess's outer loop also folds its inner is_region_access_type switch into the per-type switch — every bounds check is now in a case with a compile-time-constant region type. The runtime primary_kind_variable_for_type lookup is no longer needed at the call sites (each case names the offset variable directly).

The region_bounds free function and RegionBounds struct are removed; region_semantics.{hpp,cpp} shrinks to just is_region_access_type and primary_kind_variable_for_type (still used elsewhere).

Why this shape

The bug class behind #1099 was that the per-region helper had two T_PACKET ceilings (loose max_packet_size for pointer-comparison checks, runtime packet_size for dereferences) and the choice was hidden behind a std::optional<Variable> argument. "I forgot to pass it" looked identical to "I deliberately chose not to" — which is exactly how the asymmetry between ValidMapKeyValue and ValidAccess stayed invisible.

After the refactor the choice is the literal ceiling expression on the require_upper_bound line. The diff that fixes a #1099-class bug is the diff readers see at the call site.

Soundness

• packet_size <= max_packet_size is an invariant of the abstract domain, so tightening the T_PACKET ceiling at this site can only reject programs that the previous version also could have caught at the analogous ValidAccess site — no previously-verified program becomes rejected for a reason that wasn't already there.
• Pointer-comparison checks (width == 0) in ValidAccess::T_PACKET continue to use max_packet_size, preserving the legitimate end = ptr + N; if (end <= data_end) pattern.
• All other per-region bounds (T_STACK, T_CTX, T_SHARED, T_ALLOC_MEM) preserve their floor/ceiling expressions exactly as in the previous code.

Test plan

• cmake --build build --parallel — clean build
• ./bin/tests — 1314 passed, 1 skipped, 236 failed-as-expected (unchanged from main)

References

• Closes ValidMapKeyValue uses generic max_packet_size for T_PACKET bounds; ValidAccess uses runtime packet_size() #1099
• Origin discussion: PR Make Call composition explicit; centralize region semantics (refs #1086) #1097 (thread)

[coderabbitai]

📝 Walkthrough

Walkthrough

Replaces a single region_bounds API with three specialized region-bound helpers in src/crab/ebpf_checker.cpp, and removes the former region_bounds implementation and its declarations from src/crab/region_semantics.cpp / .hpp. Call sites in validity checks are updated to use the new helpers and simplified plumbing.

Changes

Cohort / File(s)	Summary
eBPF checker — region-bound helpers src/crab/ebpf_checker.cpp	Removed unified require_region_bounds; added three specialized helpers that split static vs dynamic region checks, handle T_STACK/T_CTX/T_PACKET ceilings (using either AnalysisContext, TypeEncoding::max_packet_size, or runtime packet_size), and constrain access_ub for T_SHARED/T_ALLOC_MEM. Updated ValidMapKeyValue and ValidAccess call sites to use new helpers and removed prior generic region-type / optional-packet-size plumbing.
Region semantics — implementation removed src/crab/region_semantics.cpp	Deleted region_bounds implementation and supporting includes; left only primary_kind_variable_for_type(...). Error-handling and RegionBounds computation removed.
Region semantics — API/header cleanup src/crab/region_semantics.hpp	Removed RegionBounds type and region_bounds(...) declaration, deleted related includes and docs referencing bounds API; retained is_region_access_type(...) and primary_kind_variable_for_type(...).

Possibly related PRs

• Make max packet size a runtime parameter #1073: Introduced runtime-configurable max_packet_size() uses and refactored packet-size ceiling handling — closely related to packet-bounds ceiling changes.
• Move checker and transformer to different cpp files #788: Prior changes to eBPF checker and memory-access/region-bounds logic; touches similar areas refactored here.

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 11.11% 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
Linked Issues check	✅ Passed	Code changes implement the objective from #1099: refactoring region_bounds into specialized helpers and updating ValidMapKeyValue to use runtime packet_size instead of generic max_packet_size ceiling.
Out of Scope Changes check	✅ Passed	All changes are scoped to the stated objective: removing unified region_bounds function and introducing specialized static/dynamic bounds helpers with explicit packet_size handling.
Title check	✅ Passed	The title directly addresses the main change: fixing issue #1099 by tightening ValidMapKeyValue packet bounds and inlining bounds checks as described in the PR objectives.
Description check	✅ Passed	The description thoroughly explains the bug, the refactor, and why the changes were made, all directly related to the changeset modifications across the three files.

_{✏️ 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/issue-1099-validmapkeyvalue-packet-size

---

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/crab/ebpf_checker.cpp`:
- Around line 75-83: The T_PACKET branch of
check_access_to_static_region(TypeEncoding, ...) is only sound for comparison
checks but this precondition is only in the comment; enforce it by either
asserting that callers pass a comparison-shaped access when
TypeEncoding==T_PACKET (e.g. assert is_comparison_check in the caller or at the
top of check_access_to_static_region) or, preferably, split the "loose packet"
semantics into a dedicated helper (e.g. check_access_to_loose_packet_region or
similar) and keep check_access_to_static_region's TypeEncoding overload to
reject unexpected T_PACKET values (throw_fail/default case) so stray T_PACKET
arguments are caught structurally; update callers such as the ValidAccess
T_PACKET arm to call the new helper explicitly and add a brief comment
documenting the new helper's narrower contract.

🪄 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: 4667111b-e5fd-499a-bf57-59e176aca057

📥 Commits

Reviewing files that changed from the base of the PR and between 9623d46 and 137f30b.

📒 Files selected for processing (3)

• src/crab/ebpf_checker.cpp
• src/crab/region_semantics.cpp
• src/crab/region_semantics.hpp

💤 Files with no reviewable changes (1)

• src/crab/region_semantics.cpp