From f8af16037ecb1b9a3c322fc4ea2821497f8a2225 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 23 Apr 2021 15:46:52 +0200 Subject: [PATCH] Make sure a ReferenceStat is set to values of the correct type (#6430) This PR fixes a very subtle issue with setting the values a ReferenceStat refers to. ReferenceStat::set() would take a variable by const& and then store the pointer to it. When giving it a different, but implicitly convertible, type, the pointer would assume the wrong type and consequently read incorrect values from it. This PR makes set() a template function that explicitly checks that the given type is the correct one. As we can only export int64_t to the API, this forces users of ReferenceStat to use int64_t stats. --- src/prop/bvminisat/core/Solver.cc | 4 ++-- src/prop/bvminisat/core/Solver.h | 4 ++-- src/prop/bvminisat/simp/SimpSolver.h | 2 +- src/prop/minisat/core/Solver.cc | 6 ++---- src/prop/minisat/core/Solver.h | 4 ++-- src/util/statistics_stats.h | 4 +++- 6 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index e517b8f74..e7d9086bc 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -1412,9 +1412,9 @@ bool Solver::withinBudget(Resource r) const d_notify->safePoint(r); return !asynch_interrupt && - (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) && + (conflict_budget < 0 || conflicts < conflict_budget) && (propagation_budget < 0 || - propagations < (uint64_t)propagation_budget); + propagations < propagation_budget); } } // namespace BVMinisat diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index d2423a71a..7c08c3bcf 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -235,8 +235,8 @@ public: // Statistics: (read-only member variable) // - uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts; - uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, + int64_t solves, starts, decisions, rnd_decisions, propagations, conflicts; + int64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; // Bitvector Propagations diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index b103243d3..ec6ed375a 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -114,7 +114,7 @@ class SimpSolver : public Solver { // int merges; int asymm_lits; - int eliminated_vars; + int64_t eliminated_vars; // cvc5::TimerStat total_eliminate_time; protected: diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index ea30c12e9..40274489b 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -2383,10 +2383,8 @@ inline bool Solver::withinBudget(Resource r) const d_proxy->spendResource(r); bool within_budget = - !asynch_interrupt - && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) - && (propagation_budget < 0 - || propagations < (uint64_t)propagation_budget); + !asynch_interrupt && (conflict_budget < 0 || conflicts < conflict_budget) + && (propagation_budget < 0 || propagations < propagation_budget); return within_budget; } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index f85dc0d24..cd3f38c9e 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -351,9 +351,9 @@ public: // Statistics: (read-only member variable) // - uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts, + int64_t solves, starts, decisions, rnd_decisions, propagations, conflicts, resources_consumed; - uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, + int64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; protected: diff --git a/src/util/statistics_stats.h b/src/util/statistics_stats.h index 93d7e3e2a..4821dda60 100644 --- a/src/util/statistics_stats.h +++ b/src/util/statistics_stats.h @@ -122,8 +122,10 @@ class ReferenceStat /** Value stored for this statistic */ using stat_type = StatisticReferenceValue; /** Reset the reference to point to `t`. */ - void set(const T& t) + template + void set(const TT& t) { + static_assert(std::is_same_v, "Incorrect type for ReferenceStat"); if constexpr (Configuration::isStatisticsBuild()) { d_data->d_value = &t; -- 2.30.2