mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-01 19:54:04 +00:00
Code Activity

Fix uses of gnu anonymous structs. (#10345)

Browse source 
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.
This commit is contained in:
davedets 2026-08-01 11:44:01 -07:00 • committed by GitHub
parent 90c401c5f2
commit b902c020ce
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 59 additions and 54 deletions
Download patch file Download diff file Expand all files Collapse all files

1
cmake/compiler_warnings.cmake
View file

@ -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")

6
src/ast/euf/euf_egraph.cpp
View file

@ -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();

6
src/ast/euf/euf_egraph.h
View file

@ -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<to_merge> m_to_merge;

46
src/ast/euf/euf_mam.cpp
View file

@ -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<const cont*>(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();
}

46
src/smt/mam.cpp
View file

@ -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<const cont*>(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();
}

4
src/smt/smt_conflict_resolution.cpp
View file

@ -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)) {

4
src/smt/smt_conflict_resolution.h
View file

@ -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);}
};