SMT2: encode structs and multi-constructor ADTs as SMT-LIB datatypes#9072
Open
tautschnig wants to merge 1 commit into
Open
SMT2: encode structs and multi-constructor ADTs as SMT-LIB datatypes#9072tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
tautschnig
requested review from
TGWDB,
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
This PR extends the SMT2 backend to encode CBMC structs and multi-constructor ADTs as SMT-LIB datatypes, including parsing/printing constructors, member access, and with updates.
Changes:
- Add multi-constructor ADT handling in struct parsing (
parse_struct) and printing (convert_struct). - Encode
memberaccess andwithupdates for ADT-backed datatypes using(_ is ...)discriminator checks. - Extend symbol discovery to traverse additional type metadata (
ID_C_index_type) and reuse datatype names by struct tag.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #9072 +/- ##
===========================================
+ Coverage 80.68% 80.70% +0.01%
===========================================
Files 1714 1714
Lines 189522 189797 +275
Branches 73 73
===========================================
+ Hits 152925 153175 +250
- Misses 36597 36622 +25 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
strata/smt2-adt-struct-datatypes
branch
2 times, most recently
from
7cb0c09 to
9d2fb95
Compare
Declare/parse struct and #adt_constructors (algebraic data) types as SMT-LIB datatypes keyed by tag/#index_type, and handle their construction, member access, and 'with' updates (parse_struct, convert_struct, convert_member, convert_with, find_symbols_rec). The constructor tag is always emitted in its own sort (a bit-vector literal via from_integer), both in the convert_struct ite-chain and in $tag member access, so the comparisons are well-sorted. A convert_adt_constructor helper centralises the constructor-application emission. Because the front end gives no guarantees, the paths that cannot be encoded soundly are guarded by invariants that fail loudly rather than emit wrong-but-well-formed SMT: 'with' on $tag (which would change the constructor) is rejected; constructors sharing a field name (which would declare a selector twice) are rejected; and a member access on a multi-constructor ADT must name a field with a declared selector. Same-tag struct datatype reuse now compares component SMT sorts (array sizes are irrelevant, element types and bit-widths are not), falling back to a fresh datatype when they differ, so differently-typed same-tagged structs are not conflated. Add unit tests covering the multi-constructor ADT declaration, construction (constant and non-constant tag), member and 'with' access, the rejection invariants, and the same-tag reuse (merge vs. reject). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
strata/smt2-adt-struct-datatypes
branch
from
9d2fb95 to
80356e0
Compare
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.
Declare/parse struct and #adt_constructors (algebraic data) types as SMT-LIB datatypes keyed by tag/#index_type, and handle their construction, member access, and 'with' updates (parse_struct, convert_struct, convert_member, convert_with, find_symbols_rec).