From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Fri, 23 Apr 2021 13:46:52 +0000 (+0200)
Subject: Make sure a ReferenceStat is set to values of the correct type (#6430)
X-Git-Tag: cvc5-1.0.0~1843
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f8af16037ecb1b9a3c322fc4ea2821497f8a2225;p=cvc5.git

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.
---

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<T>;
   /** Reset the reference to point to `t`. */
-  void set(const T& t)
+  template <typename TT>
+  void set(const TT& t)
   {
+    static_assert(std::is_same_v<T, TT>, "Incorrect type for ReferenceStat");
     if constexpr (Configuration::isStatisticsBuild())
     {
       d_data->d_value = &t;