From 4f9f046557b4de30c8f2ff654ea6e172e9cd912d Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 7 Jul 2017 15:21:12 -0700 Subject: [PATCH] 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. 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. --- src/util/statistics_registry.h | 39 ++++++++++++++++++++++++---------- 1 file changed, 28 insertions(+), 11 deletions(-) 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(fd, getData()); + safe_print(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 */ @@ -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 */ @@ -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(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(fd, data); } SExpr getValue() const; -- 2.30.2