mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

Introduce (and use) a macro for the "trailing array" idiom, so we can disable warnings for this when they're in force.

Browse source
This commit is contained in:
David Detlefs 2026-06-08 11:25:43 -07:00
parent 7e3aad4e17
commit fe2b6fac24
29 changed files with 93 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

1
cmake/compiler_warnings.cmake
View file

@ -12,6 +12,7 @@ set(GCC_ONLY_WARNINGS "")
set(CLANG_ONLY_WARNINGS
"-Wno-c++98-compat"
"-Wno-c++98-compat-pedantic"
"-Wzero-length-array"
)
set(MSVC_WARNINGS "/W3")

7
src/ast/ast.h
View file

@ -20,6 +20,7 @@ Revision History:
#include "util/vector.h"
#include "util/trailing_array.h"
#include "util/hashtable.h"
#include "util/buffer.h"
#include "util/zstring.h"
@ -642,7 +643,7 @@ class func_decl : public decl {
unsigned m_arity;
sort * m_range;
sort * m_domain[0];
TRAILING_ARRAY(sort *, m_domain);
static unsigned get_obj_size(unsigned arity) { return sizeof(func_decl) + arity * sizeof(sort *); }
@ -725,7 +726,7 @@ class app : public expr {
func_decl * m_decl;
unsigned m_num_args;
app_flags m_flags;
expr * m_args[0];
TRAILING_ARRAY(expr *, m_args);
static unsigned get_obj_size(unsigned num_args) {
return sizeof(app) + num_args * sizeof(expr *);
@ -872,7 +873,7 @@ class quantifier : public expr {
symbol m_skid;
unsigned m_num_patterns;
unsigned m_num_no_patterns;
char m_patterns_decls[0];
TRAILING_ARRAY(char, m_patterns_decls);
static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) {
return (unsigned)(sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*));

3
src/ast/euf/euf_enode.h
View file

@ -16,6 +16,7 @@ Author:
--*/
#include "util/vector.h"
#include "util/trailing_array.h"
#include "util/id_var_list.h"
#include "util/lbool.h"
#include "util/approx_set.h"
@ -66,7 +67,7 @@ namespace euf {
signed char m_lbl_hash = -1; // It is different from -1, if enode is used in a pattern
approx_set m_lbls;
approx_set m_plbls;
enode* m_args[0];
TRAILING_ARRAY(enode*, m_args);
friend class enode_args;
friend class enode_parents;

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

@ -20,6 +20,7 @@ Revision History:
--*/
#include <algorithm>
#include "util/trailing_array.h"
#include "util/pool.h"
#include "util/trail.h"
@ -231,7 +232,7 @@ namespace euf {
The size of the array is m_num_args.
*/
enode * m_joints[0];
TRAILING_ARRAY(enode *, m_joints);
};
struct bind : public instruction {
@ -247,21 +248,21 @@ namespace euf {
approx_set m_lbl_set;
unsigned short m_num_args;
unsigned m_oreg;
unsigned m_iregs[0];
TRAILING_ARRAY(unsigned, m_iregs);
};
struct yield : public instruction {
quantifier * m_qa;
app * m_pat;
unsigned short m_num_bindings;
unsigned m_bindings[0];
TRAILING_ARRAY(unsigned, m_bindings);
};
struct is_cgr : public instruction {
unsigned m_ireg;
func_decl * m_label;
unsigned short m_num_args;
unsigned m_iregs[0];
TRAILING_ARRAY(unsigned, m_iregs);
};
void display_num_args(std::ostream & out, unsigned num_args) {

3
src/ast/rewriter/cached_var_subst.h
View file

@ -19,13 +19,14 @@ Revision History:
#pragma once
#include "ast/rewriter/var_subst.h"
#include "util/trailing_array.h"
#include "util/map.h"
class cached_var_subst {
struct key {
quantifier * m_qa;
unsigned m_num_bindings;
expr * m_bindings[0];
TRAILING_ARRAY(expr *, m_bindings);
};
struct key_hash_proc {
unsigned operator()(key * k) const {

3
src/ast/simplifiers/euf_completion.h
View file

@ -21,6 +21,7 @@ Author:
#pragma once
#include "util/scoped_vector.h"
#include "util/trailing_array.h"
#include "util/dlist.h"
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/euf/euf_egraph.h"
@ -53,7 +54,7 @@ namespace euf {
unsigned m_max_generation;
unsigned m_min_top_generation;
unsigned m_max_top_generation;
euf::enode* m_nodes[0];
TRAILING_ARRAY(euf::enode*, m_nodes);
binding(quantifier* q, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top) :
m_q(q),

3
src/math/polynomial/polynomial.cpp
View file

@ -17,6 +17,7 @@ Notes:
--*/
#include "math/polynomial/polynomial.h"
#include "util/trailing_array.h"
#include "util/vector.h"
#include "util/chashtable.h"
#include "util/small_object_allocator.h"
@ -160,7 +161,7 @@ namespace polynomial {
unsigned m_total_degree; //!< total degree of the monomial
unsigned m_size; //!< number of powers
unsigned m_hash;
power m_powers[0];
TRAILING_ARRAY(power, m_powers);
friend class tmp_monomial;
void sort() {

3
src/math/polynomial/rpolynomial.cpp
View file

@ -17,6 +17,7 @@ Notes:
--*/
#include "math/polynomial/rpolynomial.h"
#include "util/trailing_array.h"
#include "util/tptr.h"
#include "util/buffer.h"
@ -39,7 +40,7 @@ namespace rpolynomial {
unsigned m_ref_count;
var m_var;
unsigned m_size;
poly_or_num * m_args[0];
TRAILING_ARRAY(poly_or_num *, m_args);
public:
unsigned ref_count() const { return m_ref_count; }

5
src/math/subpaving/subpaving_t.h
View file

@ -19,6 +19,7 @@ Revision History:
#pragma once
#include<ostream>
#include "util/trailing_array.h"
#include "util/tptr.h"
#include "util/small_object_allocator.h"
#include "util/chashtable.h"
@ -94,7 +95,7 @@ public:
unsigned m_lemma:1; //!< True if it is a learned clause.
unsigned m_watched:1; //!< True if it we are watching this clause. All non-lemmas are watched.
unsigned m_num_jst:30; //!< Number of times it is used to justify some bound.
ineq * m_atoms[0];
TRAILING_ARRAY(ineq *, m_atoms);
static unsigned get_obj_size(unsigned sz) { return sizeof(clause) + sz*sizeof(ineq*); }
public:
clause():constraint(constraint::CLAUSE) {}
@ -322,7 +323,7 @@ public:
class monomial : public definition {
friend class context_t;
unsigned m_size;
power m_powers[0];
TRAILING_ARRAY(power, m_powers);
monomial(unsigned sz, power const * pws);
static unsigned get_obj_size(unsigned sz) { return sizeof(monomial) + sz*sizeof(power); }
public:

3
src/muz/base/dl_rule.h
View file

@ -20,6 +20,7 @@ Revision History:
#pragma once
#include "ast/ast.h"
#include "util/trailing_array.h"
#include "muz/base/dl_costs.h"
#include "muz/base/dl_util.h"
#include "ast/used_vars.h"
@ -308,7 +309,7 @@ namespace datalog {
The negated flag is never set for interpreted tails.
*/
app * m_tail[0];
TRAILING_ARRAY(app *, m_tail);
static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); }

3
src/nlsat/nlsat_clause.h
View file

@ -19,6 +19,7 @@ Revision History:
#pragma once
#include "nlsat/nlsat_types.h"
#include "util/trailing_array.h"
#include "util/vector.h"
namespace nlsat {
@ -34,7 +35,7 @@ namespace nlsat {
unsigned m_marked:1;
unsigned m_var_hash;
assumption_set m_assumptions;
literal m_lits[0];
TRAILING_ARRAY(literal, m_lits);
static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); }
size_t get_size() const { return get_obj_size(m_capacity); }
clause(unsigned id, unsigned sz, literal const * lits, bool learned, assumption_set as);

3
src/nlsat/nlsat_interval_set.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include "nlsat/nlsat_interval_set.h"
#include "util/trailing_array.h"
#include "math/polynomial/algebraic_numbers.h"
#include "util/buffer.h"
@ -39,7 +40,7 @@ namespace nlsat {
unsigned m_num_intervals;
unsigned m_ref_count:31;
unsigned m_full:1;
interval m_intervals[0];
TRAILING_ARRAY(interval, m_intervals);
};
void display(std::ostream & out, anum_manager & am, interval const & curr) {

3
src/nlsat/nlsat_justification.h
View file

@ -20,6 +20,7 @@ Revision History:
#pragma once
#include "nlsat/nlsat_types.h"
#include "util/trailing_array.h"
#include "util/tptr.h"
namespace nlsat {
@ -38,7 +39,7 @@ namespace nlsat {
class lazy_justification {
unsigned m_num_literals;
unsigned m_num_clauses;
char m_data[0];
TRAILING_ARRAY(char, m_data);
nlsat::clause* const* clauses() const { return (nlsat::clause *const*)(m_data); }
public:
static unsigned get_obj_size(unsigned nl, unsigned nc) { return sizeof(lazy_justification) + sizeof(literal)*nl + sizeof(nlsat::clause*)*nc; }

3
src/nlsat/nlsat_types.h
View file

@ -19,6 +19,7 @@ Revision History:
#pragma once
#include "math/polynomial/polynomial.h"
#include "util/trailing_array.h"
#include "util/buffer.h"
#include "sat/sat_types.h"
#include "util/z3_exception.h"
@ -99,7 +100,7 @@ namespace nlsat {
class ineq_atom : public atom {
friend class solver;
unsigned m_size;
poly * m_ps[0];
TRAILING_ARRAY(poly *, m_ps);
ineq_atom(kind k, unsigned sz, poly * const * ps, bool const * is_even, var max_var);
static unsigned get_obj_size(unsigned sz) { return sizeof(ineq_atom) + sizeof(poly*)*sz; }
public:

3
src/sat/sat_clause.h
View file

@ -19,6 +19,7 @@ Revision History:
#pragma once
#include "util/small_object_allocator.h"
#include "util/trailing_array.h"
#include "util/id_gen.h"
#include "util/map.h"
#include "sat/sat_types.h"
@ -53,7 +54,7 @@ namespace sat {
unsigned m_inact_rounds:8;
unsigned m_glue:8;
unsigned m_psm:8; // transient field used during gc
literal m_lits[0];
TRAILING_ARRAY(literal, m_lits);
static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); }
size_t get_size() const { return get_obj_size(m_capacity); }

3
src/sat/sat_lookahead.h
View file

@ -21,6 +21,7 @@ Notes:
#include "util/small_object_allocator.h"
#include "util/trailing_array.h"
#include "sat/sat_elim_eqs.h"
namespace pb {
@ -147,7 +148,7 @@ namespace sat {
unsigned m_size; // number of non-false literals
size_t m_obj_size; // object size (counting all literals)
literal m_head; // head literal
literal m_literals[0]; // list of literals, put any true literal in head.
TRAILING_ARRAY(literal, m_literals); // list of literals, put any true literal in head.
size_t num_lits() const {
return (m_obj_size - sizeof(nary)) / sizeof(literal);
}

3
src/sat/smt/ba_xor.h
View file

@ -18,13 +18,14 @@ Author:
#pragma once
#include "sat/sat_types.h"
#include "util/trailing_array.h"
#include "sat/smt/ba_constraint.h"
namespace ba {
class xr : public constraint {
literal m_lits[0];
TRAILING_ARRAY(literal, m_lits);
public:
static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(xr) + num_lits * sizeof(literal)); }
xr(unsigned id, literal_vector const& lits);

3
src/sat/smt/pb_card.h
View file

@ -18,13 +18,14 @@ Author:
#pragma once
#include "sat/sat_types.h"
#include "util/trailing_array.h"
#include "sat/smt/pb_constraint.h"
namespace pb {
class card : public constraint {
literal m_lits[0];
TRAILING_ARRAY(literal, m_lits);
public:
static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(card) + num_lits * sizeof(literal)); }
card(unsigned id, literal lit, literal_vector const& lits, unsigned k);

3
src/sat/smt/pb_pb.h
View file

@ -18,6 +18,7 @@ Author:
#pragma once
#include "sat/sat_types.h"
#include "util/trailing_array.h"
#include "sat/smt/pb_card.h"
@ -27,7 +28,7 @@ namespace pb {
unsigned m_slack;
unsigned m_num_watch;
unsigned m_max_sum;
wliteral m_wlits[0];
TRAILING_ARRAY(wliteral, m_wlits);
public:
static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(pbc) + num_lits * sizeof(wliteral)); }
pbc(unsigned id, literal lit, svector<wliteral> const& wlits, unsigned k);

3
src/sat/smt/q_clause.h
View file

@ -17,6 +17,7 @@ Author:
#pragma once
#include "util/dlist.h"
#include "util/trailing_array.h"
#include "ast/ast.h"
#include "ast/quantifier_stat.h"
#include "ast/euf/euf_enode.h"
@ -66,7 +67,7 @@ namespace q {
unsigned m_max_generation;
unsigned m_min_top_generation;
unsigned m_max_top_generation;
euf::enode* m_nodes[0];
TRAILING_ARRAY(euf::enode*, m_nodes);
binding(clause& c, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top):
c(&c),

3
src/sat/smt/q_solver.h
View file

@ -17,6 +17,7 @@ Author:
#pragma once
#include "util/obj_hashtable.h"
#include "util/trailing_array.h"
#include "ast/ast_trail.h"
#include "ast/rewriter/der.h"
#include "sat/smt/sat_th.h"
@ -35,7 +36,7 @@ namespace q {
unsigned m_num_bindings;
unsigned m_num_literals;
sat::literal* m_literals;
expr* m_bindings[0];
TRAILING_ARRAY(expr*, m_bindings);
q_proof_hint(symbol const& method, unsigned g, unsigned b, unsigned l) {
m_method = method;

3
src/sat/smt/sat_smt.h
View file

@ -16,6 +16,7 @@ Author:
--*/
#pragma once
#include "ast/ast.h"
#include "util/trailing_array.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "sat/sat_solver.h"
@ -31,7 +32,7 @@ namespace sat {
class constraint_base {
extension* m_ex = nullptr;
unsigned m_mem[0];
TRAILING_ARRAY(unsigned, m_mem);
static size_t ext_size() {
return sizeof(((constraint_base*)nullptr)->m_ex);
}

9
src/smt/mam.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include <algorithm>
#include "util/trailing_array.h"
#include "util/pool.h"
#include "util/trail.h"
@ -207,7 +208,7 @@ namespace {
The size of the array is m_num_args.
*/
enode * m_joints[0];
TRAILING_ARRAY(enode *, m_joints);
};
struct bind : public instruction {
@ -223,21 +224,21 @@ namespace {
approx_set m_lbl_set;
unsigned short m_num_args;
unsigned m_oreg;
unsigned m_iregs[0];
TRAILING_ARRAY(unsigned, m_iregs);
};
struct yield : public instruction {
quantifier * m_qa;
app * m_pat;
unsigned short m_num_bindings;
unsigned m_bindings[0];
TRAILING_ARRAY(unsigned, m_bindings);
};
struct is_cgr : public instruction {
unsigned m_ireg;
func_decl * m_label;
unsigned short m_num_args;
unsigned m_iregs[0];
TRAILING_ARRAY(unsigned, m_iregs);
};
void display_num_args(std::ostream & out, unsigned num_args) {

3
src/smt/smt_clause.h
View file

@ -19,6 +19,7 @@ Revision History:
#pragma once
#include "ast/ast.h"
#include "util/trailing_array.h"
#include "smt/smt_literal.h"
#include "util/tptr.h"
#include "util/obj_hashtable.h"
@ -62,7 +63,7 @@ namespace smt {
unsigned m_has_del_eh:1; //!< true if must notify event handler when deleted.
unsigned m_has_justification:1; //!< true if the clause has a justification attached to it.
unsigned m_deleted:1; //!< true if the clause is marked for deletion by was not deleted yet because it is referenced by some data-structure (e.g., m_lemmas)
literal m_lits[0];
TRAILING_ARRAY(literal, m_lits);
static unsigned get_obj_size(unsigned num_lits, clause_kind k, bool has_atoms, bool has_del_eh, bool has_justification) {
unsigned r = sizeof(clause) + sizeof(literal) * num_lits;

3
src/smt/smt_enode.h
View file

@ -19,6 +19,7 @@ Revision History:
#pragma once
#include "util/id_var_list.h"
#include "util/trailing_array.h"
#include "util/approx_set.h"
#include "ast/ast.h"
#include "ast/ast_pp.h"
@ -101,7 +102,7 @@ namespace smt {
trans_justification m_trans; //!< A justification for the enode being equal to its root.
approx_set m_lbls;
approx_set m_plbls;
enode * m_args[0]; //!< Cached args
TRAILING_ARRAY(enode *, m_args); //!< Cached args
friend class context;
friend class conflict_resolution;

3
src/smt/smt_quantifier_instances.h
View file

@ -1,3 +1,4 @@
#include "util/trailing_array.h"
/*++
Copyright (c) 2006 Microsoft Corporation
@ -25,7 +26,7 @@ namespace smt {
class quantifier_instance {
quantifier * m_quantifier;
double m_cost;
enode * m_enodes[0];
TRAILING_ARRAY(enode *, m_enodes);
quantifier_instance(quantifier * q, enode * const * enodes);
friend class quantifier_instances;
public:

3
src/util/mpz.h
View file

@ -19,6 +19,7 @@ Revision History:
#pragma once
#include<string>
#include "util/trailing_array.h"
#include "util/mutex.h"
#include "util/util.h"
#include "util/small_object_allocator.h"
@ -57,7 +58,7 @@ typedef unsigned int digit_t;
class mpz_cell {
unsigned m_size;
unsigned m_capacity;
digit_t m_digits[0];
TRAILING_ARRAY(digit_t, m_digits);
friend class mpz_manager<true>;
friend class mpz_manager<false>;
friend class mpz_stack;

3
src/util/sexpr.cpp
View file

@ -17,6 +17,7 @@ Notes:
--*/
#include "util/sexpr.h"
#include "util/trailing_array.h"
#include "util/vector.h"
#include "util/buffer.h"
@ -27,7 +28,7 @@ Notes:
struct sexpr_composite : public sexpr {
unsigned m_num_children;
sexpr * m_children[0];
TRAILING_ARRAY(sexpr *, m_children);
sexpr_composite(unsigned num_children, sexpr * const * children, unsigned line, unsigned pos):
sexpr(kind_t::COMPOSITE, line, pos),
m_num_children(num_children) {

29
src/util/trailing_array.h Normal file
View file

@ -0,0 +1,29 @@
#pragma once
// Copyright (c) Microsoft Corporation. All Rights Reserved.
// Many classes in Z3 use the "trailing array" idiom: the last field
// of the class C is a zero-length array of some type T, and the allocation
// of an instance adds extra space for some number of T's (usually the
// number is held in some other field of C).
// Zero-length arrays are non-standard, and provoke a warning in Clang
// when -Wzero-length-array is specified. This file introduces a macro
// for this idiom, which, for compilers that give a warning, disables
// the warning around the declaration. So far that's only Clang,
// but more could be added.
#define STR_PRAGMA_FOR_TRAILING_ARRAY(x) _Pragma(#x)
#ifdef __clang__
#define TRAILING_ARRAY(type, field) \
STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic push) \
STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic ignored "-Wzero-length-array") \
type field[0]; \
STR_PRAGMA_FOR_TRAILING_ARRAY(clang diagnostic pop)
#else
#define TRAILING_ARRAY(type, field) type field[0];
#endif