Byte-operator lowering: add support pointer types in adjust_width#8892
Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
Open
Byte-operator lowering: add support pointer types in adjust_width#8892tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
The adjust_width function in lower_byte_operators.cpp did not handle the ID_pointer type. When CBMC processes byte extraction operations on data involving pointers, it may need to create bitvector types from the pointer type. Since pointers were not supported, the function would hit the PRECONDITION(false) fallthrough case. Add support for ID_pointer type by returning bv_typet, consistent with how pointers are treated elsewhere in the byte-operator lowering code (e.g., in unpack_rec). Add a unit test that directly verifies adjust_width handles pointer types, plus additional unit tests for byte extraction involving pointer types and arrays of pointers. Fixes: diffblue#8475 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-8475-adjust-width
branch
from
2bb57a7 to
9c2f8cd
Compare
There was a problem hiding this comment.
Pull request overview
This PR fixes a crash in the byte-operator lowering logic by teaching adjust_width how to handle pointer-typed bitvectors, which can arise when lowering byte_extract/byte_update involving pointers (including arrays of pointers).
Changes:
- Extend
adjust_widthto acceptID_pointerand return a resized bitvector type instead of failing a precondition. - Add unit/regression tests covering
adjust_widthon pointers andlower_byte_extracton pointer and array-of-pointer result types.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
src/util/lower_byte_operators.cpp |
Allows pointer-typed widths to be adjusted without triggering a PRECONDITION(false) during lowering. |
unit/util/lower_byte_operators.cpp |
Adds regression coverage for pointer handling in adjust_width and for lowering byte_extract producing pointer/array-of-pointer types. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8892 +/- ##
========================================
Coverage 80.41% 80.42%
========================================
Files 1703 1703
Lines 188398 188443 +45
Branches 73 73
========================================
+ Hits 151502 151549 +47
+ Misses 36896 36894 -2 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add support for ID_pointer type in adjust_width function to handle byte extraction from pointer arrays correctly.
Fixes: #8475