Fix extractbits invariant for non-byte-aligned bitfields

[tautschnig]

When unpacking a non-byte-aligned bitfield (e.g., 28 bits) into bytes, the unpack_rec function in lower_byte_operators.cpp created byte-sized extractbits operations that could exceed the source bitvector width. For a 28-bit source, the last byte extraction at offset 24 would try to read bits 24-31, but only bits 0-27 exist. The simplifier then merged these adjacent extractbits into a single extractbits(src, 0, bv[32]) from a 28-bit source, violating the DATA_INVARIANT in convert_extractbits.

Fix by zero-extending the source to the next byte boundary before creating byte-sized extractbits, so all extractions stay within bounds. Restore the original DATA_INVARIANT that correctly detects malformed extractbits expressions.

The regression test was minimised from CSmith seed 1736798452 using creduce.

Fixes: #8581

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

Fixes a crash/invariant violation in the byte-lowering pipeline when unpacking non-byte-aligned bitfields by ensuring generated extractbits operations never exceed the source bitvector width.

Changes:

• Zero-extend non-byte-aligned bitvector sources in unpack_rec up to the next byte boundary before emitting byte-sized extractbits.
• Add a regression test reproducing issue #8581 (CSmith seed minimised via creduce).

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
src/util/lower_byte_operators.cpp	Pads non-byte-aligned sources via zero-extension so bytewise extractbits stay in-bounds.
regression/cbmc/extractbits-bitfield-typecast/test.desc	Adds a regression harness expecting a clean CBMC run (no crash) for the reduced reproducer.
regression/cbmc/extractbits-bitfield-typecast/main.c	Minimal C reproducer exercising the problematic unpacking path for a non-byte-aligned bitfield.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.01%. Comparing base (7a4df92) to head (439aeed).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8860   +/-   ##
========================================
  Coverage    80.01%   80.01%           
========================================
  Files         1703     1703           
  Lines       188396   188406   +10     
  Branches        73       73           
========================================
+ Hits        150738   150758   +20     
+ Misses       37658    37648   -10     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.