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.
Comment on lines
+3591
to
+3606
| for(std::size_t ci = 0; ci < ctors.size(); ++ci) | ||
| { | ||
| if(ci + 1 < ctors.size()) | ||
| { out << "(ite (= "; convert_expr(tag_op); out << " " << ci << ") "; } | ||
| const auto &ctor_fields = ctors[ci].find(irep_idt("fields")).get_sub(); | ||
| if(ctor_fields.empty()) | ||
| out << ctors[ci].find(ID_name).id(); | ||
| else | ||
| { | ||
| out << "(" << ctors[ci].find(ID_name).id(); | ||
| for(const auto &field : ctor_fields) | ||
| for(std::size_t j = 0; j < components.size(); ++j) | ||
| if(components[j].get_name() == field.id()) | ||
| { out << " "; convert_expr(expr.operands()[j]); } | ||
| out << ")"; | ||
| } |
Comment on lines
+4971
to
+4978
| const auto &ctors = adt_ctors_cm.get_sub(); | ||
| for(std::size_t i = 0; i < ctors.size(); ++i) | ||
| { | ||
| if(i + 1 < ctors.size()) | ||
| { out << "(ite ((_ is " << ctors[i].find(ID_name).id() << ") "; convert_expr(struct_op); out << ") " << i << " "; } | ||
| else out << i; | ||
| } | ||
| for(std::size_t i = 0; i + 1 < ctors.size(); ++i) out << ")"; |
Comment on lines
+4717
to
+4739
| const auto &adt_ctors_cw = struct_type.find(irep_idt("#adt_constructors")); | ||
| if(adt_ctors_cw.is_not_nil() && adt_ctors_cw.get_sub().size() > 1) | ||
| { | ||
| const auto &ctors = adt_ctors_cw.get_sub(); | ||
| for(std::size_t ci = 0; ci < ctors.size(); ++ci) | ||
| { | ||
| const auto &cn = ctors[ci].find(ID_name).id(); | ||
| const auto &flds = ctors[ci].find(irep_idt("fields")).get_sub(); | ||
| if(ci + 1 < ctors.size()) | ||
| { out << "(ite ((_ is " << cn << ") "; convert_expr(expr.old()); out << ") "; } | ||
| if(flds.empty()) | ||
| out << cn; | ||
| else | ||
| { | ||
| out << "(" << cn; | ||
| for(const auto &fld : flds) | ||
| { out << " "; if(fld.id() == component_name) convert_expr(value); else { out << "(" << smt_typename << "." << fld.id() << " "; convert_expr(expr.old()); out << ")"; } } | ||
| out << ")"; | ||
| } | ||
| if(ci + 1 < ctors.size()) out << " "; | ||
| } | ||
| for(std::size_t ci = 0; ci + 1 < ctors.size(); ++ci) out << ")"; | ||
| } |
Comment on lines
+6354
to
+6376
| // Reuse existing datatype for structs with the same tag name | ||
| // (variants may differ in non-semantic annotations like array sizes). | ||
| const irep_idt &tag = to_struct_type(type).get_tag(); | ||
| std::string smt_typename; | ||
| if(!tag.empty()) | ||
| { | ||
| for(const auto &entry : datatype_map) | ||
| { | ||
| if( | ||
| entry.first.id() == ID_struct && | ||
| to_struct_type(entry.first).get_tag() == tag) | ||
| { | ||
| smt_typename = entry.second; | ||
| break; | ||
| } | ||
| } | ||
| } | ||
| if(smt_typename.empty()) | ||
| { | ||
| smt_typename = | ||
| "struct." + std::to_string(datatype_map.size()); | ||
| need_decl = true; | ||
| } |
Comment on lines
+6317
to
+6320
| const typet &idx_type = | ||
| static_cast<const typet &>(type.find(ID_C_index_type)); | ||
| if(idx_type.is_not_nil()) | ||
| find_symbols_rec(idx_type, recstack); |
| if(adt_ctors.is_nil() || adt_ctors.get_sub().size() <= 1) | ||
| { | ||
| // Let's also declare convenience functions to update individual | ||
| // members of the struct whil we're at it. The functions are |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #9072 +/- ##
===========================================
- Coverage 80.68% 80.64% -0.05%
===========================================
Files 1714 1714
Lines 189501 189640 +139
Branches 73 73
===========================================
+ Hits 152902 152930 +28
- Misses 36599 36710 +111 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
strata/smt2-adt-struct-datatypes
branch
from
b06f999 to
7cb0c09
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). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
strata/smt2-adt-struct-datatypes
branch
from
7cb0c09 to
9d2fb95
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).