util: expose is_zero_width via util/pointer_offset_size#9016
Open
tautschnig wants to merge 1 commit into
Open
Conversation
tautschnig
requested review from
TGWDB,
kroening,
martin-cs and
peterschrammel
as code owners
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9016 +/- ##
========================================
Coverage 80.59% 80.60%
========================================
Files 1711 1711
Lines 189454 189491 +37
Branches 73 73
========================================
+ Hits 152697 152736 +39
+ Misses 36757 36755 -2 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
is_zero_width(const typet &, const namespacet &) was a file-static
helper in src/solvers/smt2/smt2_conv.cpp. The predicate is generic
('does this type have effective width of zero bits?') and not
specific to the non-incremental SMT2 backend; the incremental SMT2
backend will need exactly the same predicate to detect empty-typed
expressions correctly without re-treading the same struct/union/
struct-tag/union-tag/array recursion. Move the function to
src/util/pointer_offset_size.{h,cpp} alongside its semantic
neighbours pointer_offset_size and pointer_offset_bits, drop the
'static' qualifier on the original definition, and remove the
duplicate body from smt2_conv.cpp.
smt2_conv.cpp continues to call is_zero_width through the shared
header (which it already includes); other back-ends and util-level
call sites can now do the same.
Behaviour change: the predicate now also unwraps ID_c_enum_tag via
ns.follow_tag() and recurses into the underlying integer type of
ID_c_enum (via c_enum_typet::subtype()). The previous code unwrapped
ID_struct_tag and ID_union_tag but fell through to 'return false'
for ID_c_enum_tag — which gave the correct answer for every C enum
that exists in practice (whose underlying integer type has non-zero
width) but was an unprincipled coincidence rather than the predicate
behaving symmetrically across all tag kinds. The new arms make the
symmetry explicit: a hypothetical zero-width c_enum (e.g. one whose
underlying type is empty_typet) now correctly reports as zero-width,
matching the existing struct/union behaviour.
A focused unit test in unit/util/pointer_offset_size.cpp pins down
the contract: empty_typet, signed/zero-width bitvectors, struct with
all-empty / mixed components, array of empty type with constant and
symbolic size (the deliberately non-obvious branch), struct_tag_typet
resolving to an empty struct, and the new c_enum / c_enum_tag arms
including both the regular signed-int-underlying case and the
zero-width-underlying edge case.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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.
is_zero_width(const typet &, const namespacet &) was a file-static helper in src/solvers/smt2/smt2_conv.cpp. The predicate is generic ('does this type have effective width of zero bits?') and not specific to the non-incremental SMT2 backend; the incremental SMT2 backend will need exactly the same predicate to detect empty-typed expressions correctly without re-treading the same struct/union/ struct-tag/union-tag/array recursion. Move the function to src/util/pointer_offset_size.{h,cpp} alongside its semantic neighbours pointer_offset_size and pointer_offset_bits, drop the 'static' qualifier on the original definition, and remove the duplicate body from smt2_conv.cpp.
No functional change. smt2_conv.cpp continues to call is_zero_width through the shared header (which it already includes); other back-ends and util-level call sites can now do the same.