Skip to content

Conversation

@Alan-Jowett
Copy link
Contributor

@Alan-Jowett Alan-Jowett commented Jan 12, 2026

Resolves: #972

Problem

The constant_limits static variable in ebpf_domain.cpp was initialized at static initialization time, before thread_local_options and variable_registry were properly set up. In release builds, this caused static initialization order issues where EbpfDomain::calculate_constant_limits() would capture uninitialized or default state from these thread-local variables, leading to incorrect constraint limits being cached and reused throughout the program's lifetime.

Additionally, even with lazy initialization, the cached limits could become stale when threads are reused with different configurations (e.g., in test suites where thread_local_options is reassigned between test cases), as the cache was never invalidated during thread-local state cleanup.

Solution

  1. Lazy initialization: Replace static initialization with LazyAllocator<EbpfDomain, EbpfDomain::calculate_constant_limits> to defer computation until first use, ensuring thread_local_options and variable_registry are populated before calculate_constant_limits() captures their state.

  2. Cache invalidation: Add EbpfDomain::clear_thread_local_state() method that clears the constant_limits cache, and call it from ebpf_verifier_clear_thread_local_state() to prevent stale cached limits when threads are reused with different configurations.

  3. Soundness documentation: Expand comment to explicitly document reentrancy safety (no recursion possible since calculate_constant_limits doesn't call get_constant_limits() or widen(to_constants=true)) and soundness of intersection-based clamping (only shrinks domain, preserving over-approximation).

Changes

  • Changed constant_limits from static initialization to thread_local LazyAllocator
  • Added get_constant_limits() accessor function
  • Added EbpfDomain::clear_thread_local_state() to invalidate the cache
  • Updated widen() to use get_constant_limits() accessor
  • Added comprehensive comment documenting soundness and safety

Widening clamping behavior remains identical; this only fixes the initialization timing and cache lifetime issues.

Testing

Existing tests pass. The fix ensures correct behavior in release builds and when threads are reused across different verification contexts.

Summary by CodeRabbit

  • Chores
    • Optimized constant limits initialization through lazy-loading mechanism for improved performance and resource management.

✏️ Tip: You can customize this high-level summary in your review settings.

Summary by CodeRabbit

  • Refactor

    • Domain constants now initialize lazily to reduce startup cost and memory use.
    • Public control added to reset domain thread-local state for better lifecycle handling.
  • Bug Fixes

    • Verifier teardown now clears domain-specific thread-local state too, preventing stale state across runs.

✏️ Tip: You can customize this high-level summary in your review settings.

@coderabbitai
Copy link

coderabbitai bot commented Jan 12, 2026

Walkthrough

Introduce thread-local lazy initialization for EbpfDomain constant limits via a thread-local LazyAllocator and accessor; add EbpfDomain::clear_thread_local_state() and call it from verifier shutdown; tidy duplicate #include <ranges> and update includes.

Changes

Cohort / File(s) Summary
EbpfDomain implementation
src/crab/ebpf_domain.cpp
Add thread_local LazyAllocator and get_constant_limits() for lazy initialization; replace direct static constant usage in widen(... to_constants=true) with the lazy accessor; include crab_utils/lazy_allocator.hpp; preserve calculate_constant_limits() and add explanatory comments about TLS/non-reentrancy.
EbpfDomain header
src/crab/ebpf_domain.hpp
Add public static method static void clear_thread_local_state() (placed after calculate_constant_limits()).
Verifier shutdown / includes cleanup
src/fwd_analyzer.cpp
Remove duplicate #include <ranges> and add EbpfDomain::clear_thread_local_state() call to ebpf_verifier_clear_thread_local_state() to clear thread-local lazy state on shutdown.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~20 minutes

🚥 Pre-merge checks | ✅ 4 | ❌ 1
❌ Failed checks (1 warning)
Check name Status Explanation Resolution
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.
✅ Passed checks (4 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title accurately describes the main change: replacing static initialization with LazyAllocator for constant_limits to defer computation until first use.
Linked Issues check ✅ Passed All requirements from #972 are met: constant_limits uses LazyAllocator for lazy initialization, clear_thread_local_state() was added to invalidate cache, and integration into ebpf_verifier_clear_thread_local_state() ensures cache lifetime correctness.
Out of Scope Changes check ✅ Passed All changes are directly scoped to fixing the static initialization ordering issue: LazyAllocator integration, clear_thread_local_state() method, and duplicate #include removal are all necessary for the fix.

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

✨ Finishing touches
  • 📝 Generate docstrings

📜 Recent review details

Configuration used: Repository UI

Review profile: ASSERTIVE

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 3ef0772 and c73b885.

📒 Files selected for processing (3)
  • src/crab/ebpf_domain.cpp
  • src/crab/ebpf_domain.hpp
  • src/fwd_analyzer.cpp
🧰 Additional context used
📓 Path-based instructions (4)
src/**/*.{cpp,hpp,h}

📄 CodeRabbit inference engine (AGENTS.md)

src/**/*.{cpp,hpp,h}: Prove invariants when possible — encode the assumptions an analysis relies on (preconditions, lattice properties, monotonicity) directly in code comments, assertions, or type-level checks before trusting experiments.
Optimise for auditability — choose designs that are easy to step through and review by hand (even if marginally slower or more verbose) so future engineers can re-establish the soundness argument quickly.
Favour explicit error handling and early exits to surface problems instead of deferring to implicit behaviour.

Files:

  • src/crab/ebpf_domain.hpp
  • src/crab/ebpf_domain.cpp
  • src/fwd_analyzer.cpp
src/{asm_*,cfg,arith,crab,linux}/**/*.{cpp,hpp,h}

📄 CodeRabbit inference engine (AGENTS.md)

Narrate the reasoning — 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.

Files:

  • src/crab/ebpf_domain.hpp
  • src/crab/ebpf_domain.cpp
**/*.{hpp,h}

📄 CodeRabbit inference engine (AGENTS.md)

Use #pragma once for static includes in header files; follow existing patterns within each subdirectory.

Files:

  • src/crab/ebpf_domain.hpp
**/*.{cpp,c,hpp,h}

📄 CodeRabbit inference engine (AGENTS.md)

**/*.{cpp,c,hpp,h}: Ensure new C/C++ sources include the standard SPDX license header; validate with ./scripts/check-license.sh.
Run ./scripts/format-code --staged before committing to enforce clang-format standards; this mirrors the installed Git hook.

Files:

  • src/crab/ebpf_domain.hpp
  • src/crab/ebpf_domain.cpp
  • src/fwd_analyzer.cpp
🧠 Learnings (3)
📚 Learning: 2025-12-09T20:31:07.030Z
Learnt from: CR
Repo: vbpf/prevail PR: 0
File: AGENTS.md:0-0
Timestamp: 2025-12-09T20:31:07.030Z
Learning: Applies to src/**/*.{cpp,hpp,h} : Prove invariants when possible — encode the assumptions an analysis relies on (preconditions, lattice properties, monotonicity) directly in code comments, assertions, or type-level checks before trusting experiments.

Applied to files:

  • src/crab/ebpf_domain.cpp
📚 Learning: 2025-12-09T20:31:07.030Z
Learnt from: CR
Repo: vbpf/prevail PR: 0
File: AGENTS.md:0-0
Timestamp: 2025-12-09T20:31:07.030Z
Learning: Applies to src/{asm_*,cfg,arith,crab,linux}/**/*.{cpp,hpp,h} : Narrate the reasoning — 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.

Applied to files:

  • src/crab/ebpf_domain.cpp
  • src/fwd_analyzer.cpp
📚 Learning: 2025-12-09T20:31:07.030Z
Learnt from: CR
Repo: vbpf/prevail PR: 0
File: AGENTS.md:0-0
Timestamp: 2025-12-09T20:31:07.030Z
Learning: Core verifier is implemented in modern C++20 — see CMakeLists.txt for build configuration details.

Applied to files:

  • src/fwd_analyzer.cpp
🧬 Code graph analysis (1)
src/fwd_analyzer.cpp (1)
src/crab/ebpf_domain.cpp (2)
  • clear_thread_local_state (167-167)
  • clear_thread_local_state (167-167)
🪛 Clang (14.0.6)
src/crab/ebpf_domain.cpp

[warning] 163-163: variable 'constant_limits' is non-const and globally accessible, consider making it const

(cppcoreguidelines-avoid-non-const-global-variables)


[warning] 165-165: use a trailing return type for this function

(modernize-use-trailing-return-type)


[warning] 169-169: use a trailing return type for this function

(modernize-use-trailing-return-type)


[warning] 169-169: method 'widen' can be made static

(readability-convert-member-functions-to-static)

src/fwd_analyzer.cpp

[error] 3-3: 'ranges' file not found

(clang-diagnostic-error)

🪛 Cppcheck (2.19.0)
src/crab/ebpf_domain.cpp

[style] 164-164: The function 'urem' is never used.

(unusedFunction)


[style] 173-173: The function 'copy' is never used.

(unusedFunction)

src/fwd_analyzer.cpp

[information] 3-3: Include file

(missingIncludeSystem)


[information] 30-30: Include file

(missingIncludeSystem)

⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (10)
  • GitHub Check: build_ubuntu (Debug, library)
  • GitHub Check: build_windows (Debug, library)
  • GitHub Check: build_ubuntu (Debug, tests)
  • GitHub Check: build_windows (Release, library)
  • GitHub Check: build_windows (Release, tests)
  • GitHub Check: build_ubuntu (Release, tests)
  • GitHub Check: build_windows (Debug, tests)
  • GitHub Check: build_ubuntu (Debug)
  • GitHub Check: build_ubuntu (Release)
  • GitHub Check: Analyze (cpp)
🔇 Additional comments (6)
src/crab/ebpf_domain.hpp (1)

70-71: LGTM!

The clear_thread_local_state() declaration is appropriately placed alongside calculate_constant_limits() and follows the existing pattern for static cleanup methods.

src/crab/ebpf_domain.cpp (3)

17-17: LGTM!

Include added for LazyAllocator template.


157-167: Well-documented soundness and safety invariants.

The comment correctly narrates:

  1. Initialization timing: Deferred until thread-local state is ready
  2. Non-reentrancy: calculate_constant_limits() doesn't recurse into get_constant_limits() or widen(to_constants=true)
  3. Soundness of clamping: Intersection only shrinks domains, preserving over-approximation

Per coding guidelines, this satisfies the requirement to spell out invariants and the reasoning for soundness.


169-176: LGTM!

The accessor get_constant_limits() correctly replaces direct access to constant_limits. First invocation of widen(..., true) will trigger lazy initialization after thread-local state is set.

src/fwd_analyzer.cpp (2)

3-3: LGTM!

The <ranges> header is required for std::views::values at line 129. The static analysis warning about missing header is a false positive—the codebase targets C++20 where <ranges> is standard.


25-31: LGTM!

Adding EbpfDomain::clear_thread_local_state() to the cleanup sequence ensures the lazily-initialized constant_limits is invalidated when thread-local state is reset. This prevents stale cached values when threads are reused with different configurations (e.g., in test scenarios).


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

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

Copy link

@coderabbitai coderabbitai bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 1

🤖 Fix all issues with AI agents
In @src/crab/ebpf_domain.cpp:
- Around line 157-160: The LazyAllocator instance constant_limits caches results
from EbpfDomain::calculate_constant_limits which capture thread_local_options
and variable_registry; add a call to constant_limits.clear() inside
ebpf_verifier_clear_thread_local_state() (in the cleanup routine in
src/fwd_analyzer.cpp) so the LazyAllocator is invalidated when thread-local
state is reset, preventing stale cached limits across reused threads.
📜 Review details

Configuration used: Repository UI

Review profile: ASSERTIVE

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 1ff4ace and 07e1a06.

📒 Files selected for processing (1)
  • src/crab/ebpf_domain.cpp
🧰 Additional context used
📓 Path-based instructions (3)
src/**/*.{cpp,hpp,h}

📄 CodeRabbit inference engine (AGENTS.md)

src/**/*.{cpp,hpp,h}: Prove invariants when possible — encode the assumptions an analysis relies on (preconditions, lattice properties, monotonicity) directly in code comments, assertions, or type-level checks before trusting experiments.
Optimise for auditability — choose designs that are easy to step through and review by hand (even if marginally slower or more verbose) so future engineers can re-establish the soundness argument quickly.
Favour explicit error handling and early exits to surface problems instead of deferring to implicit behaviour.

Files:

  • src/crab/ebpf_domain.cpp
src/{asm_*,cfg,arith,crab,linux}/**/*.{cpp,hpp,h}

📄 CodeRabbit inference engine (AGENTS.md)

Narrate the reasoning — 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.

Files:

  • src/crab/ebpf_domain.cpp
**/*.{cpp,c,hpp,h}

📄 CodeRabbit inference engine (AGENTS.md)

**/*.{cpp,c,hpp,h}: Ensure new C/C++ sources include the standard SPDX license header; validate with ./scripts/check-license.sh.
Run ./scripts/format-code --staged before committing to enforce clang-format standards; this mirrors the installed Git hook.

Files:

  • src/crab/ebpf_domain.cpp
🧬 Code graph analysis (1)
src/crab/ebpf_domain.cpp (1)
src/crab/ebpf_domain.hpp (10)
  • other (59-59)
  • other (60-60)
  • other (61-61)
  • other (62-62)
  • other (63-63)
  • other (64-64)
  • other (65-65)
  • other (66-66)
  • other (67-67)
  • other (68-68)
🪛 Clang (14.0.6)
src/crab/ebpf_domain.cpp

[warning] 158-158: variable 'constant_limits' is non-const and globally accessible, consider making it const

(cppcoreguidelines-avoid-non-const-global-variables)


[warning] 160-160: use a trailing return type for this function

(modernize-use-trailing-return-type)


[warning] 162-162: use a trailing return type for this function

(modernize-use-trailing-return-type)


[warning] 162-162: method 'widen' can be made static

(readability-convert-member-functions-to-static)

🪛 Cppcheck (2.19.0)
src/crab/ebpf_domain.cpp

[style] 164-164: The function 'urem' is never used.

(unusedFunction)

⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (10)
  • GitHub Check: build_windows (Debug, library)
  • GitHub Check: build_ubuntu (Release, library)
  • GitHub Check: build_windows (Release, library)
  • GitHub Check: build_windows (Debug, tests)
  • GitHub Check: build_ubuntu (Release, tests)
  • GitHub Check: build_ubuntu (Debug, tests)
  • GitHub Check: build_windows (Release, tests)
  • GitHub Check: build_ubuntu (Release)
  • GitHub Check: build_ubuntu (Debug)
  • GitHub Check: Analyze (cpp)
🔇 Additional comments (2)
src/crab/ebpf_domain.cpp (2)

17-17: LGTM!

Required include for the LazyAllocator template.


162-169: LGTM!

Usage of get_constant_limits() correctly replaces the former static reference. The widening logic remains intact.

(The static-analysis hint that widen can be made static is a false positive—it accesses this->rcp and stack.)

Copy link

@coderabbitai coderabbitai bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 1

🤖 Fix all issues with AI agents
In @src/crab/ebpf_domain.cpp:
- Around line 157-160: Update the comment above the LazyAllocator instantiation
to explicitly document why clamping to constant limits via intersection is sound
and safe: state that LazyAllocator<EbpfDomain,
EbpfDomain::calculate_constant_limits> is used so thread_local_options is
populated first, note that LazyAllocator::get() has no reentrancy guard but
calculate_constant_limits does not call get_constant_limits() or
widen(to_constants=true) so recursion cannot occur, and explain that the
intersection operation only shrinks the domain (element-wise tightening of
constraints) and therefore preserves the over-approximation required for
soundness; reference LazyAllocator, EbpfDomain::calculate_constant_limits,
get_constant_limits, and widen(to_constants=true) in the comment.
📜 Review details

Configuration used: Repository UI

Review profile: ASSERTIVE

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 07e1a06 and 9f3f25f.

📒 Files selected for processing (1)
  • src/crab/ebpf_domain.cpp
🧰 Additional context used
📓 Path-based instructions (3)
src/**/*.{cpp,hpp,h}

📄 CodeRabbit inference engine (AGENTS.md)

src/**/*.{cpp,hpp,h}: Prove invariants when possible — encode the assumptions an analysis relies on (preconditions, lattice properties, monotonicity) directly in code comments, assertions, or type-level checks before trusting experiments.
Optimise for auditability — choose designs that are easy to step through and review by hand (even if marginally slower or more verbose) so future engineers can re-establish the soundness argument quickly.
Favour explicit error handling and early exits to surface problems instead of deferring to implicit behaviour.

Files:

  • src/crab/ebpf_domain.cpp
src/{asm_*,cfg,arith,crab,linux}/**/*.{cpp,hpp,h}

📄 CodeRabbit inference engine (AGENTS.md)

Narrate the reasoning — 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.

Files:

  • src/crab/ebpf_domain.cpp
**/*.{cpp,c,hpp,h}

📄 CodeRabbit inference engine (AGENTS.md)

**/*.{cpp,c,hpp,h}: Ensure new C/C++ sources include the standard SPDX license header; validate with ./scripts/check-license.sh.
Run ./scripts/format-code --staged before committing to enforce clang-format standards; this mirrors the installed Git hook.

Files:

  • src/crab/ebpf_domain.cpp
🧬 Code graph analysis (1)
src/crab/ebpf_domain.cpp (1)
src/crab/ebpf_domain.hpp (10)
  • other (59-59)
  • other (60-60)
  • other (61-61)
  • other (62-62)
  • other (63-63)
  • other (64-64)
  • other (65-65)
  • other (66-66)
  • other (67-67)
  • other (68-68)
🪛 Clang (14.0.6)
src/crab/ebpf_domain.cpp

[warning] 158-158: variable 'constant_limits' is non-const and globally accessible, consider making it const

(cppcoreguidelines-avoid-non-const-global-variables)


[warning] 160-160: use a trailing return type for this function

(modernize-use-trailing-return-type)


[warning] 162-162: use a trailing return type for this function

(modernize-use-trailing-return-type)


[warning] 162-162: method 'widen' can be made static

(readability-convert-member-functions-to-static)

🪛 Cppcheck (2.19.0)
src/crab/ebpf_domain.cpp

[style] 164-164: The function 'urem' is never used.

(unusedFunction)

⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (8)
  • GitHub Check: build_windows (Release, library)
  • GitHub Check: build_ubuntu (Release, library)
  • GitHub Check: build_ubuntu (Debug, library)
  • GitHub Check: build_ubuntu (Release, tests)
  • GitHub Check: build_ubuntu (Debug, tests)
  • GitHub Check: Analyze (cpp)
  • GitHub Check: build_ubuntu (Release)
  • GitHub Check: build_ubuntu (Debug)
🔇 Additional comments (2)
src/crab/ebpf_domain.cpp (2)

17-17: LGTM!

Include is correctly placed and necessary for the LazyAllocator template.


162-169: LGTM!

The widening implementation correctly uses get_constant_limits() to clamp the result when to_constants is true. The intersection operation preserves soundness by narrowing to the domain of representable constants.

@Alan-Jowett
Copy link
Contributor Author

✅ Review comment addressed. I've added:

  1. EbpfDomain::clear_thread_local_state() static method to clear the constant_limits LazyAllocator
  2. Called this method from ebpf_verifier_clear_thread_local_state() alongside the other cleanup operations

This ensures the cached constant limits are invalidated when thread-local state is reset, preventing stale cached values when threads are reused with different configurations.

@coveralls
Copy link

coveralls commented Jan 12, 2026

Pull Request Test Coverage Report for Build 20967734412

Details

  • 5 of 5 (100.0%) changed or added relevant lines in 2 files are covered.
  • No unchanged relevant lines lost coverage.
  • Overall coverage increased (+0.05%) to 86.664%

Totals Coverage Status
Change from base Build 20882100451: 0.05%
Covered Lines: 9033
Relevant Lines: 10423

💛 - Coveralls

@Alan-Jowett Alan-Jowett force-pushed the lazy-allocator-constant-limits branch from 173f260 to bdc575b Compare January 12, 2026 23:41
@elazarg
Copy link
Collaborator

elazarg commented Jan 13, 2026

@Alan-Jowett Could you just update the sign-off to use your signature instead of Copilot's?

@Alan-Jowett
Copy link
Contributor Author

Whoops. Will do.

@Alan-Jowett Alan-Jowett force-pushed the lazy-allocator-constant-limits branch from bdc575b to 3ef0772 Compare January 13, 2026 16:41
Signed-off-by: Alan Jowett <alanjo@microsoft.com>
@Alan-Jowett Alan-Jowett force-pushed the lazy-allocator-constant-limits branch from 3ef0772 to c73b885 Compare January 13, 2026 18:19
@elazarg elazarg merged commit 67479e2 into vbpf:main Jan 14, 2026
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Release build hang in bpf2c due to static init ordering of constant_limits

3 participants