summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2017-07-07 15:21:12 -0700
committerGitHub <noreply@github.com>2017-07-07 15:21:12 -0700
commit4f9f046557b4de30c8f2ff654ea6e172e9cd912d (patch)
treeae08cd8d86cdfc86a8f8b67e596e74377685ccb7 /src
parent4fa50d388112bf30f9ebe219898cdc4dea76fd18 (diff)
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.
Diffstat (limited to 'src')
-rw-r--r--src/util/statistics_registry.h39
1 files 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<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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback