Add and fix a few general compiler warnings. (#5628)

* rewriter: fix unused variable warnings

* cmake: make missing non-virtual dtors error

* treewide: add missing virtual destructors

* cmake: add a few more checks

* api: add missing virtual destructor to user_propagator_base

* examples: compile cpp example with compiler warnings

* model: fix unused variable warnings

* rewriter: fix logical-op-parentheses warnings

* sat: fix unused variable warnings

* smt: fix unused variable warnings

cmake/compiler_warnings.cmake

@@ -39,6 +39,27 @@ set(CLANG_WARNINGS_AS_ERRORS
   "-Werror=delete-non-virtual-dtor"
   # https://clang.llvm.org/docs/DiagnosticsReference.html#woverloaded-virtual
   "-Werror=overloaded-virtual"
+  # warn the user if a class with virtual functions has a
+  # non-virtual destructor. This helps catch hard to
+  # track down memory errors
+  "-Werror=non-virtual-dtor"
+  # warn if a null dereference is detected
+  "-Werror=null-dereference"
+  # warn for potential performance problem casts
+  # "-Werror=cast-align"
+  # warn if float is implicit promoted to double
+  # "-Werror=double-promotion"
+  "-Werror=no-unreachable-code-return"
+  # warn the user if a variable declaration shadows one from a parent context
+  # "-Werror=shadow"
+  # warn for c-style casts
+  # "-Werror=old-style-cast"
+  # warn on sign conversions
+  # "-Werror=sign-conversion"
+  # warn on type conversions that may lose data
+  # "-Werror=conversion"
+  # warn on anything being unused
+  # "-Werror=unused"
 )
 
 ################################################################################

examples/c++/CMakeLists.txt

@@ -28,6 +28,8 @@ add_executable(cpp_example example.cpp)
 target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
 target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES})
 
+target_compile_options(cpp_example PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+
 if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
   # On Windows we need to copy the Z3 libraries
   # into the same directory as the executable

src/api/c++/z3++.h

@@ -3940,6 +3940,8 @@ namespace z3 {
         virtual void push() = 0;
         virtual void pop(unsigned num_scopes) = 0;
 
+        virtual ~user_propagator_base() = default;
+
         /**
            \brief user_propagators created using \c fresh() are created during 
            search and their lifetimes are restricted to search time. They should

src/ast/ast.h

@@ -1399,6 +1399,7 @@ inline bool has_labels(expr const * n) {
 class some_value_proc {
 public:
     virtual expr * operator()(sort * s) = 0;
+    virtual ~some_value_proc() = default;
 };
 
 // -----------------------------------

src/ast/ast_smt_pp.h

@@ -46,6 +46,7 @@ public:
     public:
         virtual bool operator()(func_decl* d) const { return false; }
         virtual bool operator()(sort* s) const { return false; }
+        virtual ~is_declared() = default;
     };
 private:
     ast_manager& m_manager;

src/ast/fpa/fpa2bv_converter.h

@@ -61,7 +61,7 @@ protected:
 public:
 
     fpa2bv_converter(ast_manager & m);
-    ~fpa2bv_converter();
+    virtual ~fpa2bv_converter();
 
     fpa_util & fu() { return m_util; }
     bv_util & bu() { return m_bv_util; }

src/ast/is_variable_test.h

@@ -23,6 +23,7 @@ Revision History:
 
 class is_variable_proc {
 public:
+    virtual ~is_variable_proc() = default;
     virtual bool operator()(const expr* e) const = 0;
 };
 

src/ast/normal_forms/name_exprs.h

@@ -23,6 +23,7 @@ Notes:
 
 class expr_predicate {
 public:
+    virtual ~expr_predicate() = default;
     virtual bool operator()(expr * t) = 0;
 };
 

src/ast/num_occurs.h

@@ -37,6 +37,8 @@ public:
         m_ignore_quantifiers(ignore_quantifiers) {
     }
 
+    virtual ~num_occurs() = default;
+
     void validate();
     virtual void reset() { m_num_occurs.reset(); }
     

src/ast/recfun_decl_plugin.h

@@ -93,6 +93,7 @@ namespace recfun {
     // closure for computing whether a `rhs` expression is immediate
     struct is_immediate_pred {
         virtual bool operator()(expr * rhs) = 0;
+        virtual ~is_immediate_pred() = default;
     };
 
     class def {

src/ast/rewriter/push_app_ite.h

@@ -33,6 +33,7 @@ struct push_app_ite_cfg : public default_rewriter_cfg {
     virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args);
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);
     push_app_ite_cfg(ast_manager& m): m(m), m_conservative(true) {}
+    virtual ~push_app_ite_cfg() = default;
     void set_conservative(bool c) { m_conservative = c; }
     bool rewrite_patterns() const { return false; }
 };

src/ast/rewriter/seq_eq_solver.h

@@ -39,6 +39,7 @@ namespace seq {
 
     class eq_solver_context {
     public:
+        virtual ~eq_solver_context() = default;
         virtual void  add_consequence(bool uses_dep, expr_ref_vector const& clause) = 0;
         virtual void  add_solution(expr* var, expr* term) = 0;
         virtual expr* expr2rep(expr* e) = 0;

src/ast/rewriter/seq_rewriter.cpp

@@ -3046,7 +3046,6 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
     auto nothing = [&]() { return expr_ref(re().mk_empty(r->get_sort()), m()); };
     auto epsilon = [&]() { return expr_ref(re().mk_epsilon(seq_sort), m()); };
     auto dotstar = [&]() { return expr_ref(re().mk_full_seq(r->get_sort()), m()); };
-    auto dotplus = [&]() { return expr_ref(re().mk_plus(re().mk_full_char(r->get_sort())), m()); };
     unsigned lo = 0, hi = 0;
     if (re().is_empty(r) || re().is_epsilon(r))
         // D(e,[]) = D(e,()) = []
@@ -3182,7 +3181,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
     else if (re().is_loop(r, r1, lo))
         result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, lo - 1));
     else if (re().is_loop(r, r1, lo, hi)) {
-        if (lo == 0 && hi == 0 || hi < lo)
+        if ((lo == 0 && hi == 0) || hi < lo)
             result = nothing();
         else
             result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, (lo == 0 ? 0 : lo - 1), hi - 1));
@@ -3260,7 +3259,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) {
 }
 
 expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* d) {
-    sort* seq_sort = nullptr, * ele_sort = nullptr;
+    sort* seq_sort = nullptr;
     VERIFY(m_util.is_re(d, seq_sort));
     auto nothing = [&]() { return expr_ref(re().mk_empty(d->get_sort()), m()); };
     auto epsilon = [&]() { return expr_ref(re().mk_epsilon(seq_sort), m()); };
@@ -3404,7 +3403,7 @@ expr_ref  seq_rewriter::simplify_path(expr* path) {
             result = simplify_path(t);
         else if (m().is_true(t))
             result = simplify_path(h);
-        else if (m().is_eq(h, lhs, rhs) || m().is_not(h, h1) && m().is_eq(h1, lhs, rhs))
+        else if (m().is_eq(h, lhs, rhs) || (m().is_not(h, h1) && m().is_eq(h1, lhs, rhs)))
             elim_condition(lhs, result);
     }
     return result;

src/math/hilbert/heap_trie.h

@@ -270,6 +270,7 @@ public:
     class check_value {
     public:
         virtual bool operator()(Value const& v) = 0;
+        virtual ~check_value() = default;
     };
 
     bool find_le(Key const* keys, check_value& check) {

src/math/lp/column_namer.h

@@ -23,6 +23,7 @@ Revision History:
 namespace lp {
 class column_namer {
 public:
+    virtual ~column_namer() = default;
     virtual std::string get_variable_name(unsigned j) const = 0;
     template <typename T>
     std::ostream & print_row(const row_strip<T> & row, std::ostream & out) const {

src/math/lp/factorization.h

@@ -120,6 +120,8 @@ struct factorization_factory {
         m_vars(vars), m_monic(m) {
     }
 
+    virtual ~factorization_factory() = default;
+
     bool_vector get_mask() const {
         // we keep the last element always in the first factor to avoid
         // repeating a pair twice, that is why m_mask is shorter by one then m_vars

src/math/lp/lp_settings.h

@@ -99,6 +99,7 @@ template <typename X> bool is_epsilon_small(const X & v, const double& eps);
 
 class lp_resource_limit {
 public:
+    virtual ~lp_resource_limit() = default;
     virtual bool get_cancel_flag() = 0;
 };
 

src/math/polynomial/polynomial.h

@@ -71,6 +71,7 @@ namespace polynomial {
     template<typename ValManager, typename Value = typename ValManager::numeral>
     class var2value {
     public:
+        virtual ~var2value() = default;
         virtual ValManager & m() const = 0;
         virtual bool contains(var x) const = 0;
         virtual Value const & operator()(var x) const = 0;
@@ -100,6 +101,7 @@ namespace polynomial {
 
     struct display_var_proc {
         virtual std::ostream& operator()(std::ostream & out, var x) const { return out << "x" << x; }
+        virtual ~display_var_proc() = default;
     };
 
     class polynomial;
@@ -228,6 +230,7 @@ namespace polynomial {
             del_eh * m_next;
         public:
             del_eh():m_next(nullptr) {}
+            virtual ~del_eh() = default;
             virtual void operator()(polynomial * p) = 0;
         };
 

src/math/polynomial/upolynomial_factorization_int.h

@@ -175,6 +175,8 @@ namespace upolynomial {
             m_current_size = 0;
         }
 
+        virtual ~factorization_combination_iterator_base() = default;
+
         /**
            \brief Returns the factors we are enumerating through.
         */

src/math/realclosure/realclosure.h

@@ -37,6 +37,7 @@ namespace realclosure {
 
     class mk_interval {
     public:
+        virtual ~mk_interval() = default;
         virtual void operator()(unsigned k, mpqi_manager & im, mpqi_manager::interval & r) = 0;
     };
 

src/math/subpaving/subpaving_types.h

@@ -42,6 +42,7 @@ public:
 };
 
 struct display_var_proc {
+    virtual ~display_var_proc() = default;
     virtual void operator()(std::ostream & out, var x) const { out << "x" << x; }
 };
 

src/model/model_evaluator.cpp

@@ -162,7 +162,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
         result_pr = nullptr;
         family_id fid = f->get_family_id();
         bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
-        func_decl* g = nullptr;
         br_status st = BR_FAILED;
 #if 0
         struct pp {

src/muz/base/dl_engine_base.h

@@ -122,6 +122,7 @@ namespace datalog {
 
     class register_engine_base {
     public:
+        virtual ~register_engine_base() = default;
         virtual engine_base* mk_engine(DL_ENGINE engine_type) = 0;
         virtual void set_context(context* ctx) = 0;
     };

src/nlsat/nlsat_solver.h

@@ -32,6 +32,7 @@ namespace nlsat {
 
     class display_assumption_proc {
     public:
+        virtual ~display_assumption_proc() = default;
         virtual std::ostream& operator()(std::ostream& out, assumption a) const = 0;
     };
 

src/opt/opt_context.h

@@ -45,6 +45,7 @@ namespace opt {
 
     class maxsat_context {
     public:        
+        virtual ~maxsat_context() = default;
         virtual generic_model_converter& fm() = 0;   // converter that removes fresh names introduced by simplification.
         virtual bool sat_enabled() const = 0;       // is using th SAT solver core enabled?
         virtual solver& get_solver() = 0;           // retrieve solver object (SAT or SMT solver)

src/opt/opt_pareto.h

@@ -26,6 +26,7 @@ namespace opt {
    
     class pareto_callback {
     public:
+        virtual ~pareto_callback() = default;
         virtual unsigned num_objectives() = 0;
         virtual expr_ref mk_gt(unsigned i, model_ref& model) = 0;
         virtual expr_ref mk_ge(unsigned i, model_ref& model) = 0;

src/qe/nlarith_util.cpp

@@ -989,6 +989,7 @@ namespace nlarith {
             imp& m_imp;
         public:
             isubst(imp& i) : m_imp(i) {}
+            virtual ~isubst() = default;
             virtual void mk_lt(poly const& p, app_ref& r) = 0;
             virtual void mk_eq(poly const& p, app_ref& r) = 0;
             virtual void mk_le(poly const& p, app_ref& r) { 

src/qe/qe.h

@@ -34,6 +34,7 @@ namespace qe {
 
     class i_nnf_atom {
     public:
+        virtual ~i_nnf_atom() = default;
         virtual void operator()(expr* e, bool pol, expr_ref& result) = 0;
     };
 

src/sat/sat_extension.h

@@ -40,6 +40,7 @@ namespace sat {
     class literal_occs_fun {
     public:
         virtual double operator()(literal l) = 0;        
+        virtual ~literal_occs_fun() = default;
     };
 
 

src/sat/sat_solver.cpp

@@ -1893,7 +1893,6 @@ namespace sat {
     void solver::init_ext_assumptions() {
         if (m_ext && m_ext->tracking_assumptions()) {
             m_ext_assumption_set.reset();
-            unsigned trail_size = m_trail.size();
             if (!inconsistent())
                 m_ext->add_assumptions(m_ext_assumption_set);
         }

src/sat/smt/array_model.cpp

@@ -119,7 +119,7 @@ namespace array {
 
     bool solver::must_have_different_model_values(theory_var v1, theory_var v2) {
         euf::enode* else1 = nullptr, * else2 = nullptr;
-        euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2);
+        euf::enode* n1 = var2enode(v1);
         expr* e1 = n1->get_expr();
         if (!a.is_array(e1))
             return true;

src/sat/smt/pb_constraint.h

@@ -52,6 +52,9 @@ namespace pb {
         constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz, unsigned k): 
             m_tag(t), m_lit(l), m_size(sz), m_obj_size(osz), m_id(id), m_k(k) {
         }
+
+        virtual ~constraint() = default;
+
         sat::ext_constraint_idx cindex() const { return sat::constraint_base::mem2base(this); }
         void deallocate(small_object_allocator& a) { a.deallocate(obj_size(), sat::constraint_base::mem2base_ptr(this)); }
         unsigned id() const { return m_id; }

src/sat/smt/pb_solver_interface.h

@@ -35,6 +35,7 @@ namespace pb {
 
     class solver_interface {
     public:
+        virtual ~solver_interface() = default;
         virtual lbool value(bool_var v) const = 0;
         virtual lbool value(literal lit) const = 0;
         virtual bool is_false(literal lit) const = 0;

src/smt/mam.cpp

@@ -2091,7 +2091,6 @@ namespace {
         enode * n = m_registers[j2->m_reg]->get_root();
         if (n->get_num_parents() == 0)
             return nullptr;
-        unsigned num_args = n->get_num_args();
         enode_vector * v  = mk_enode_vector();
         enode_vector::const_iterator it1  = n->begin_parents();
         enode_vector::const_iterator end1 = n->end_parents();

src/smt/smt_model_finder.cpp

@@ -50,6 +50,7 @@ namespace smt {
 
         class evaluator {
         public:
+            virtual ~evaluator() = default;
             virtual expr* eval(expr* n, bool model_completion) = 0;
         };
 

src/smt/theory_opt.h

@@ -29,6 +29,7 @@ namespace smt {
     class theory_opt {
     public:
         typedef inf_eps_rational<inf_rational> inf_eps;
+        virtual ~theory_opt() = default;
         virtual inf_eps value(theory_var) = 0;
         virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) = 0; 
         virtual theory_var add_objective(app* term) = 0;

src/solver/assertions/asserted_formulas.h

@@ -71,6 +71,7 @@ class asserted_formulas {
         char const*            m_id;
     public:
         simplify_fmls(asserted_formulas& af, char const* id): af(af), m(af.m), m_id(id) {}
+        virtual ~simplify_fmls() = default;
         char const* id() const { return m_id; }
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) = 0;
         virtual bool should_apply() const { return true;}

src/solver/solver.h

@@ -241,6 +241,7 @@ public:
 
     class propagate_callback {
     public:
+         virtual ~propagate_callback() = default;
         virtual void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) = 0;
     };
     class context_obj {

src/tactic/fd_solver/smtfd_solver.cpp

@@ -509,6 +509,8 @@ namespace smtfd {
             m_context.add_plugin(this);
         }
 
+        virtual ~theory_plugin() = default;
+
         table& ast2table(ast* f, sort* s) {
             unsigned idx = 0;
             if (!m_ast2table.find(f, s, idx)) {