From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 7 Jul 2017 22:21:12 +0000 (-0700)
Subject: Avoid invoking copy constructor when safe printing (#184)
X-Git-Tag: cvc5-1.0.0~5735^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f9f046557b4de30c8f2ff654ea6e172e9cd912d;p=cvc5.git

Avoid invoking copy constructor when safe printing (#184)

When CVC4 gets interrupted, we use async-signal safe printing functions
to print statistics. Unfortunately, the code for that was invoking copy
constructors, which is problematic due to memory allocation; for example
with statistics such as ReferenceStat<std::string>. This commit adds a
getDataRef() method for statistics that returns a const reference to the
object being printed such that the copy constructor is not called. Note:
modifying getData() was unfortunately not an option because in the case
of TimerStat, we can't return a reference to an object on the stack. We
could remove the const modifier on getData() and use d_data to store the
information but then we would have to remove it on
safeFlushInformation() and potentially other methods as well, which
seems like a worse solution.
---

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index d77dceea7..30f330cd7 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -225,6 +225,9 @@ public:
   /** Get the value of the statistic. */
   virtual T getData() const = 0;
 
+  /** Get a reference to the data value of the statistic. */
+  virtual const T& getDataRef() const = 0;
+
   /** Flush the value of the statistic to the given output stream. */
   void flushInformation(std::ostream& out) const {
     if(__CVC4_USE_STATISTICS) {
@@ -234,7 +237,7 @@ public:
 
   virtual void safeFlushInformation(int fd) const {
     if (__CVC4_USE_STATISTICS) {
-      safe_print<T>(fd, getData());
+      safe_print<T>(fd, getDataRef());
     }
   }
 
@@ -320,9 +323,10 @@ public:
   }
 
   /** Get the value of the referenced data cell. */
-  T getData() const {
-    return *d_data;
-  }
+  virtual T getData() const { return *d_data; }
+
+  /** Get a reference to the value of the referenced data cell. */
+  virtual const T& getDataRef() const { return *d_data; }
 
 };/* class ReferenceStat<T> */
 
@@ -361,9 +365,10 @@ public:
   }
 
   /** Get the underlying data value. */
-  T getData() const {
-    return d_data;
-  }
+  virtual T getData() const { return d_data; }
+
+  /** Get a reference to the underlying data value. */
+  virtual const T& getDataRef() const { return d_data; }
 
 };/* class BackedStat<T> */
 
@@ -402,8 +407,16 @@ public:
   }
 
   /** Get the data of the underlying (wrapped) statistic. */
-  T getData() const {
-    return d_stat.getData();
+  virtual T getData() const { return d_stat.getData(); }
+
+  /** Get a reference to the data of the underlying (wrapped) statistic. */
+  virtual const T& getDataRef() const { return d_stat.getDataRef(); }
+
+  virtual void safeFlushInformation(int fd) const {
+    // ReadOnlyDataStat uses getDataRef() to get the information to print,
+    // which might not be appropriate for all wrapped statistics. Delegate the
+    // printing to the wrapped statistic instead.
+    d_stat.safeFlushInformation(fd);
   }
 
   SExpr getValue() const {
@@ -728,10 +741,14 @@ public:
   /** If the timer is currently running */
   bool running() const;
 
-  timespec getData() const;
+  virtual timespec getData() const;
 
   virtual void safeFlushInformation(int fd) const {
-    safe_print<timespec>(fd, d_data);
+    // Overwrite the implementation in the superclass because we cannot use
+    // getDataRef(): it might return stale data if the timer is currently
+    // running.
+    ::timespec data = getData();
+    safe_print<timespec>(fd, data);
   }
 
   SExpr getValue() const;