skip bitwise_and when noop to preserve relations

[mikeagun]

Preserve relational constraints in bitwise_and when AND is a no-op

Problem

When clang compiles bounded loops using narrow integer types (uint8_t, uint16_t, uint32_t), it generates SHL 32 +
RSH 32 sequences (or AND with a mask like 0xFF) for truncation. The verifier's bitwise_and implementation calls
apply_unsigned → apply(AND) → set() → havoc(), which destroys all SplitDBM difference constraints on the variable —
including relational constraints like counter ≤ r.svalue established by calculate_constant_limits() during loop
widening.

Without those relational constraints, the loop counter widens to [0, +∞] and verification fails with "Loop counter
is too large", even when the loop is provably bounded.

Fix

Add a no-op check at the top of FiniteDomain::bitwise_and(Variable, Variable, const Number&) in finite_domain.cpp.
When all of the following hold, the AND is a mathematical identity and the function returns early, preserving
relational constraints:

1. Mask is 2^n - 1 — op2 > 0 && (op2 & (op2 + 1)) == 0 — ensuring value ≤ mask implies value & mask == value
2. Both svalue and uvalue intervals fit within [0, mask]
3. svalue and uvalue intervals are equal — no new information to establish; skipping won't lose any narrowing

The check is inside bitwise_and itself rather than at call sites, so all callers (immediate AND, 32-bit
zero-extension, etc.) benefit automatically.

Why sinterval == uinterval is required

Without this guard, cases like sext.yaml "small zext relational nop" would regress: when uvalue=[0,5] but svalue is
unconstrained, the AND must execute to establish svalue from uvalue. The equality check ensures we only skip when
both are already in agreement.

Tests added

bitop.yaml — unit tests for the no-op optimization:

• AND with 0xFF preserves relations when value fits — r1 ∈ [0, 100], AND 255 → relations to r2 preserved
• AND with 0xFFFF preserves relations when value fits — same pattern with 16-bit mask
• AND with 0xFF destroys relations when value may not fit — r1 ∈ [0, 300], AND 255 → relations broken, r1 clamped
  to [0, 255]

loop.yaml — end-to-end bounded loop verification (prior commit):

• 32-bit truncation (w2 = r2) with variable bound
• 8-bit AND truncation (r2 &= 255) with variable bound
• 16-bit AND truncation (r2 &= 0xffff) with variable bound

Summary by CodeRabbit

• Tests

  • Added multiple test cases for bitwise AND with constant masks and loop truncation, covering relation preservation, relation loss, sign/fit interactions, and edge-case bounds.

• Refactor

  • Improved bitwise AND behavior to preserve existing value relations when a mask guarantees no change, avoiding unnecessary downstream updates and ensuring consistent interval handling.

[coderabbitai]

Walkthrough

Adds a short-circuit in FiniteDomain::bitwise_and for RHS masks (2^n-1) that preserves relational constraints when LHS signed and unsigned intervals are identical and within the mask; otherwise performs the AND using 64-bit width. Adds test cases for AND with constants and loop truncation behaviors.

Changes

Cohort / File(s)	Summary
FiniteDomain bitwise AND change src/crab/finite_domain.cpp	Introduce an early-return when RHS is a mask (2^n-1) and LHS svalue/uvalue intervals are identical and within [0, mask], preserving relational constraints; if not, perform AND using 64-bit width so both svalue and uvalue update.
Bitwise tests test-data/bitop.yaml	Add five test blocks covering r1 &= constant scenarios: preservation when value fits (0xFF, 0xFFFF), relation destroyed when value may not fit, reconciliation when svalue/uvalue differ, and a simple 2 & 1 == 0 case.
Loop/truncation tests test-data/loop.yaml	Add four loop test blocks exercising 32-bit, 8-bit (& 0xFF), capped-by-mask, and 16-bit (& 0xFFFF) truncation behaviors with corresponding pre/postconditions for r0, r1, r2, and pc[1].

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~20 minutes

🚥 Pre-merge checks | ✅ 2 | ❌ 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 (2 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 optimization: skipping bitwise_and when it's a no-op to preserve relational constraints, which is the core fix addressing loop counter verification failures.

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

✨ Finishing touches

• 📝 Generate docstrings

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Post copyable unit tests in a comment

---

No actionable comments were generated in the recent review. 🎉

---

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

🤖 Fix all issues with AI agents

In `@src/crab/finite_domain.cpp`:
- Around line 951-964: The early-exit in FiniteDomain::bitwise_and is sound but
the comment should explicitly state the mathematical identity used for
auditability: when mask = 2^n − 1, every v in Interval[0, mask] satisfies v &
mask = v, and therefore if eval_interval(lhss) and eval_interval(lhsu) are both
⊆ [0, mask] and equal the AND is a no-op; update the comment above the guard
(near mask_interval, sinterval, uinterval) to spell out this assumption (mask
definition, v range, and the equality v & mask = v) and reference the reason why
sinterval == uinterval prevents skipping, keeping the code
(apply_unsigned(BitwiseBinOp::AND, ...)) unchanged.

In `@test-data/bitop.yaml`:
- Around line 79-117: Add a new YAML test-case that covers the edge where
r1.svalue != r1.uvalue but both signed and unsigned intervals fit inside the
mask so the AND optimization should proceed; e.g. add a test-case with pre:
["r1.type=number","r1.svalue=[0,100]","r1.uvalue=[0,200]","r2.type=number","r2.svalue=r1.svalue","r2.uvalue=r1.svalue"],
code: "r1 &= 255", and a post that asserts the relation is preserved (signed
bounds established from unsigned) such as r1.svalue=[0,100], r1.uvalue=r1.svalue
and r2.svalue/r2.uvalue tied to r1.svalue; use the existing test-case naming
style to place it alongside the other AND-with-mask cases.

In `@test-data/loop.yaml`:
- Around line 423-527: Add a negative test that mirrors the 8-bit AND case but
sets r1.svalue to a range that can exceed the mask (e.g., r1.svalue=[1,300]) so
the verifier must report a loop-counter-too-large/widened bound; specifically
copy the "while loop with 8-bit AND truncation, variable bound" test-case
(referencing symbols r0, r1, r2 and the instruction r2 &= 255) and change the
precondition to "r1.svalue=[1,300]" and update the expected post/messages to
assert the verifier emits the appropriate error or widened bound (messages not
empty / contains loop counter too large).

[coveralls]

Pull Request Test Coverage Report for Build 21921970224

Warning: This coverage report may be inaccurate.

This pull request's base commit is no longer the HEAD commit of its target branch. This means it includes changes from outside the original pull request, including, potentially, unrelated coverage changes.

• For more information on this, see Tracking coverage changes with pull request builds.
• To avoid this issue with future PRs, see these Recommended CI Configurations.
• For a quick fix, rebase this PR at GitHub. Your next report should be accurate.

Details

• 9 of 9 (100.0%) changed or added relevant lines in 1 file are covered.
• No unchanged relevant lines lost coverage.
• Overall coverage increased (+0.01%) to 86.793%

---

Totals
Change from base Build 21880446004:	0.01%
Covered Lines:	9378
Relevant Lines:	10805

---

💛 - Coveralls