From b902c020ced4fa23958d5c37f73afbc30c5cd181 Mon Sep 17 00:00:00 2001 From: davedets Date: Sat, 1 Aug 2026 11:44:01 -0700 Subject: [PATCH] Fix uses of gnu anonymous structs. (#10345) This is another PR towards the goal of getting Z3 to compile cleanly when included via FetchContents into clang-tidy, which uses a pretty strict set of warnings. (1 more flag after this!) This one adds the flag -Wgnu-anonymous-struct. Z3 uses this anonymous struct idiom, usually when using a struct as one of the members of a union, as in: ``` union { justification * m_js; unsigned m_lidx; struct { enode * m_lhs; enode * m_rhs; }; }; ``` This is not, strictly speaking, legal C++ (at least according to Google's AI summary -- and the existence of this flag in Clang implies that it is a GNU extension). You need to give the struct a member name in the outer union to prevent the warning. I'm of two minds on this. On the one hand it's not hurting anything, and all the major compilers seem to support the idiom. On the other hand, well, why do we have standards if we're going to ignore them in favor of de-facto standards? I submit this PR to show the size of the changes necessary to eliminate the use of the extension. Personally, I'd do it, but I would gladly withdraw the PR in favor of one that just silences the warning, if that was the reviewer's preference. --- cmake/compiler_warnings.cmake | 1 + src/ast/euf/euf_egraph.cpp | 6 ++-- src/ast/euf/euf_egraph.h | 6 ++-- src/ast/euf/euf_mam.cpp | 46 +++++++++++++++-------------- src/smt/mam.cpp | 46 +++++++++++++++-------------- src/smt/smt_conflict_resolution.cpp | 4 +-- src/smt/smt_conflict_resolution.h | 4 +-- 7 files changed, 59 insertions(+), 54 deletions(-) diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index 3b9ae912ef..2e20545475 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -30,6 +30,7 @@ set(CLANG_ONLY_WARNINGS "-Wignored-qualifiers" "-Wnoctad-maybe-unsupported" "-Wdeprecated-copy-with-user-provided-copy" + "-Wgnu-anonymous-struct" ) set(MSVC_WARNINGS "/W3") diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 7240d60e86..46fa054250 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -452,8 +452,8 @@ namespace euf { undo_add_th_var(p.r1, p.r2_num_parents); break; case update_record::tag_t::is_replace_th_var: - SASSERT(p.r1->get_th_var(p.m_th_id) != null_theory_var); - p.r1->replace_th_var(p.m_old_th_var, p.m_th_id); + SASSERT(p.r1->get_th_var(p.m_th.m_th_id) != null_theory_var); + p.r1->replace_th_var(p.m_th.m_old_th_var, p.m_th.m_th_id); break; case update_record::tag_t::is_new_th_eq: m_new_th_eqs.pop_back(); @@ -490,7 +490,7 @@ namespace euf { } break; case update_record::tag_t::is_plugin_undo: - m_plugins[p.m_th_id]->undo(); + m_plugins[p.m_th.m_th_id]->undo(); break; default: UNREACHABLE(); diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 6abcd38e1c..bae18e043d 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -137,7 +137,7 @@ namespace euf { struct { unsigned m_th_id : 8; unsigned m_old_th_var : 24; - }; + } m_th; unsigned qhead; bool m_inconsistent; signed char m_lbl_hash; @@ -154,7 +154,7 @@ namespace euf { update_record(enode* n, unsigned id, add_th_var) : tag(tag_t::is_add_th_var), r1(n), n1(nullptr), r2_num_parents(id) {} update_record(enode* n, theory_id id, theory_var v, replace_th_var) : - tag(tag_t::is_replace_th_var), r1(n), n1(nullptr), m_th_id(id), m_old_th_var(v) {} + tag(tag_t::is_replace_th_var), r1(n), n1(nullptr), m_th(id, v) {} update_record(new_th_eq) : tag(tag_t::is_new_th_eq), r1(nullptr), n1(nullptr), r2_num_parents(0) {} update_record(unsigned qh, new_th_eq_qhead): @@ -174,7 +174,7 @@ namespace euf { update_record(enode* n, set_relevant) : tag(tag_t::is_set_relevant), r1(n), n1(nullptr), r2_num_parents(UINT_MAX) {} update_record(unsigned th_id, plugin_undo) : - tag(tag_t::is_plugin_undo), r1(nullptr), n1(nullptr), m_th_id(th_id) {} + tag(tag_t::is_plugin_undo), r1(nullptr), n1(nullptr), m_th(th_id) {} }; ast_manager& m; svector m_to_merge; diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp index 8148fe7d9d..4ce83cfeb9 100644 --- a/src/ast/euf/euf_mam.cpp +++ b/src/ast/euf/euf_mam.cpp @@ -1874,7 +1874,7 @@ namespace euf { enode_vector * m_to_recycle; enode * const * m_it; enode * const * m_end; - }; + } m_rest; }; }; @@ -2212,32 +2212,33 @@ namespace euf { backtrack_point & bp = m_backtrack_stack[m_top]; bp.m_instr = c; bp.m_old_max_generation = m_max_generation; + auto& bp_rest = bp.m_rest; if (best_v == nullptr) { TRACE(mam_bug, tout << "m_top: " << m_top << ", m_backtrack_stack.size(): " << m_backtrack_stack.size() << "\n"; tout << *c << "\n";); - bp.m_to_recycle = nullptr; - bp.m_it = ctx.get_egraph().enodes_of(lbl).begin(); - bp.m_end = ctx.get_egraph().enodes_of(lbl).end(); + bp_rest.m_to_recycle = nullptr; + bp_rest.m_it = ctx.get_egraph().enodes_of(lbl).begin(); + bp_rest.m_end = ctx.get_egraph().enodes_of(lbl).end(); } else { SASSERT(!best_v->empty()); - bp.m_to_recycle = best_v; - bp.m_it = best_v->begin(); - bp.m_end = best_v->end(); + bp_rest.m_to_recycle = best_v; + bp_rest.m_it = best_v->begin(); + bp_rest.m_end = best_v->end(); } // find application with the right number of arguments - for (; bp.m_it != bp.m_end; ++bp.m_it) { - enode * curr = *bp.m_it; + for (; bp_rest.m_it != bp_rest.m_end; ++bp_rest.m_it) { + enode * curr = *bp_rest.m_it; if (curr->num_args() == expected_num_args && ctx.is_relevant(curr)) break; } - if (bp.m_it == bp.m_end) { - recycle_enode_vector(bp.m_to_recycle); + if (bp_rest.m_it == bp_rest.m_end) { + recycle_enode_vector(bp_rest.m_to_recycle); return nullptr; } m_top++; - update_max_generation(*(bp.m_it), nullptr); - return *(bp.m_it); + update_max_generation(*(bp_rest.m_it), nullptr); + return *(bp_rest.m_it); } void interpreter::display_reg(std::ostream & out, unsigned reg) { @@ -2812,8 +2813,8 @@ namespace euf { // Cleanup before exiting while (m_top != 0) { backtrack_point & bp = m_backtrack_stack[m_top - 1]; - if (bp.m_instr->m_opcode == CONTINUE && bp.m_to_recycle) - recycle_enode_vector(bp.m_to_recycle); + if (bp.m_instr->m_opcode == CONTINUE && bp.m_rest.m_to_recycle) + recycle_enode_vector(bp.m_rest.m_to_recycle); m_top--; } #ifdef _PROFILE_MAM @@ -2910,10 +2911,11 @@ namespace euf { m_pc = bp.m_instr->m_next; goto main_loop; - case CONTINUE: - ++bp.m_it; - for (; bp.m_it != bp.m_end; ++bp.m_it) { - m_app = *bp.m_it; + case CONTINUE: { + auto &bp_rest = bp.m_rest; + ++bp_rest.m_it; + for (; bp_rest.m_it != bp_rest.m_end; ++bp_rest.m_it) { + m_app = *bp_rest.m_it; const cont * c = static_cast(bp.m_instr); // bp.m_it may reference an enode in [begin_enodes_of(lbl), end_enodes_of(lbl)) // This enodes are not necessarily relevant. @@ -2939,11 +2941,11 @@ namespace euf { } } // continue failed - if (bp.m_to_recycle) - recycle_enode_vector(bp.m_to_recycle); + if (bp_rest.m_to_recycle) + recycle_enode_vector(bp_rest.m_to_recycle); m_top--; goto backtrack; - + } default: UNREACHABLE(); } diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 485228f059..61a94361eb 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1833,7 +1833,7 @@ namespace { enode_vector * m_to_recycle; enode * const * m_it; enode * const * m_end; - }; + } m_rest; }; }; @@ -2194,35 +2194,36 @@ namespace { bp.m_instr = c; bp.m_old_max_generation = m_max_generation; bp.m_old_used_enodes_size = m_used_enodes.size(); + auto& bp_rest = bp.m_rest; if (best_v == nullptr) { TRACE(mam_bug, tout << "m_top: " << m_top << ", m_backtrack_stack.size(): " << m_backtrack_stack.size() << "\n"; tout << *c << "\n";); - bp.m_to_recycle = nullptr; - bp.m_it = m_context.begin_enodes_of(lbl); - bp.m_end = m_context.end_enodes_of(lbl); + bp_rest.m_to_recycle = nullptr; + bp_rest.m_it = m_context.begin_enodes_of(lbl); + bp_rest.m_end = m_context.end_enodes_of(lbl); } else { SASSERT(!best_v->empty()); - bp.m_to_recycle = best_v; - bp.m_it = best_v->begin(); - bp.m_end = best_v->end(); + bp_rest.m_to_recycle = best_v; + bp_rest.m_it = best_v->begin(); + bp_rest.m_end = best_v->end(); } // find application with the right number of arguments - for (; bp.m_it != bp.m_end; ++bp.m_it) { - enode * curr = *bp.m_it; + for (; bp_rest.m_it != bp_rest.m_end; ++bp_rest.m_it) { + enode * curr = *bp_rest.m_it; if (curr->get_num_args() == expected_num_args && m_context.is_relevant(curr)) break; } - if (bp.m_it == bp.m_end) { + if (bp_rest.m_it == bp_rest.m_end) { if (best_v) { - bp.m_to_recycle = nullptr; + bp_rest.m_to_recycle = nullptr; recycle_enode_vector(best_v); } return nullptr; } m_top++; - update_max_generation(*(bp.m_it), nullptr); - return *(bp.m_it); + update_max_generation(*(bp_rest.m_it), nullptr); + return *(bp_rest.m_it); } #ifdef _TRACE @@ -2723,8 +2724,8 @@ namespace { // Cleanup before exiting while (m_top != 0) { backtrack_point & bp = m_backtrack_stack[m_top - 1]; - if (bp.m_instr->m_opcode == CONTINUE && bp.m_to_recycle) - recycle_enode_vector(bp.m_to_recycle); + if (bp.m_instr->m_opcode == CONTINUE && bp.m_rest.m_to_recycle) + recycle_enode_vector(bp.m_rest.m_to_recycle); m_top--; } #ifdef _PROFILE_MAM @@ -2811,10 +2812,11 @@ namespace { m_pc = m_b->m_next; goto main_loop; - case CONTINUE: - ++bp.m_it; - for (; bp.m_it != bp.m_end; ++bp.m_it) { - m_app = *bp.m_it; + case CONTINUE: { + auto &bp_rest = bp.m_rest; + ++bp_rest.m_it; + for (; bp_rest.m_it != bp_rest.m_end; ++bp_rest.m_it) { + m_app = *bp_rest.m_it; const cont * c = static_cast(bp.m_instr); // bp.m_it may reference an enode in [begin_enodes_of(lbl), end_enodes_of(lbl)) // This enodes are not necessarily relevant. @@ -2840,11 +2842,11 @@ namespace { } } // continue failed - if (bp.m_to_recycle) - recycle_enode_vector(bp.m_to_recycle); + if (bp_rest.m_to_recycle) + recycle_enode_vector(bp_rest.m_to_recycle); m_top--; goto backtrack; - + } default: UNREACHABLE(); } diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index c1bed6fdb8..fae8ee9720 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -1281,8 +1281,8 @@ namespace smt { switch (elem.m_kind) { case tp_elem::EQUALITY: { - enode * lhs = elem.m_lhs; - enode * rhs = elem.m_rhs; + enode * lhs = elem.m_pair.m_lhs; + enode * rhs = elem.m_pair.m_rhs; if (m_eq2proof.contains(lhs, rhs)) m_todo_pr.pop_back(); else if (visit_eq_justications(lhs, rhs)) { diff --git a/src/smt/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h index 54e91ba941..1a10873d79 100644 --- a/src/smt/smt_conflict_resolution.h +++ b/src/smt/smt_conflict_resolution.h @@ -91,10 +91,10 @@ namespace smt { struct { enode * m_lhs; enode * m_rhs; - }; + } m_pair; }; tp_elem(literal l):m_kind(LITERAL), m_lidx(l.index()) {} - tp_elem(enode * lhs, enode * rhs):m_kind(EQUALITY), m_lhs(lhs), m_rhs(rhs) {} + tp_elem(enode * lhs, enode * rhs):m_kind(EQUALITY), m_pair(lhs, rhs) {} tp_elem(justification * js):m_kind(JUSTIFICATION), m_js(js) { SASSERT(js);} };