reduce heap allocations and deallocations in proof_trace_callback_writer (#1198)

Avoid setup and tear-down costs for current_call_event_ and
current_rewrite_event_ by providing members to replace and reuse rather
than using optional::reset() and emplace().

Author: stevenmeker

include/runtime/proof_trace_writer.h

@@ -249,17 +249,16 @@ class proof_trace_callback_writer : public proof_trace_writer {
     char const *location;
     std::vector<kore_term_construction> arguments;
     std::optional<kore_term_construction> result;
-
-    call_event_construction(
-        char const *hook_name, char const *symbol_name, char const *location)
-        : hook_name(hook_name)
-        , symbol_name(symbol_name)
-        , location(location) { }
-
-    call_event_construction(char const *symbol_name, char const *location)
-        : hook_name(nullptr)
-        , symbol_name(symbol_name)
-        , location(location) { }
+    //
+    //	To avoid a heap allocation and deallocation for arguments on each event we reuse it.
+    //
+    void reinitialize(char const *h_name, char const *s_name, char const *loc) {
+      hook_name = h_name;
+      symbol_name = s_name;
+      location = loc;
+      arguments.clear();
+      result.reset();
+    }
   };
 
   struct rewrite_event_construction {
@@ -270,20 +269,23 @@ class proof_trace_callback_writer : public proof_trace_writer {
     uint64_t arity;
     size_t pos;
     subst_t substitution;
-
-    rewrite_event_construction(uint64_t ordinal, uint64_t arity)
-        : ordinal(ordinal)
-        , arity(arity)
-        , pos(0) {
+    //
+    //	To avoid a heap allocation and deallocation for substitution on each event we reuse it.
+    //
+    void reinitialize(uint64_t ord, uint64_t arty) {
+      ordinal = ord;
+      arity = arty;
+      pos = 0;
       substitution.resize(arity);
     }
   };
 
 private:
-  std::optional<call_event_construction> current_call_event_;
-
-  std::optional<rewrite_event_construction> current_rewrite_event_{
-      std::nullopt};
+  //
+  //	These structs get reused.
+  //
+  call_event_construction current_call_event_;
+  rewrite_event_construction current_rewrite_event_;
 
   bool rewrite_callback_pending_;
 
@@ -315,25 +317,23 @@ class proof_trace_callback_writer : public proof_trace_writer {
   void hook_event_pre(
       char const *name, char const *pattern,
       char const *location_stack) override {
-    current_call_event_.reset();
-    current_call_event_.emplace(name, pattern, location_stack);
+    current_call_event_.reinitialize(name, pattern, location_stack);
   }
 
   void hook_event_post(
       void *hook_result, uint64_t block_header, uint64_t bits) override {
-    current_call_event_->result.emplace(hook_result, block_header, bits);
-    hook_event_callback(current_call_event_.value());
+    current_call_event_.result.emplace(hook_result, block_header, bits);
+    hook_event_callback(current_call_event_);
   }
 
   void argument(void *arg, uint64_t block_header, uint64_t bits) override {
-    current_call_event_->arguments.emplace_back(arg, block_header, bits);
+    current_call_event_.arguments.emplace_back(arg, block_header, bits);
   }
 
   void rewrite_event_pre(uint64_t ordinal, uint64_t arity) override {
-    current_rewrite_event_.reset();
-    current_rewrite_event_.emplace(ordinal, arity);
+    current_rewrite_event_.reinitialize(ordinal, arity);
     if (arity == 0) {
-      rewrite_event_callback(current_rewrite_event_.value());
+      rewrite_event_callback(current_rewrite_event_);
     } else {
       rewrite_callback_pending_ = true;
     }
@@ -342,18 +342,18 @@ class proof_trace_callback_writer : public proof_trace_writer {
   void variable(
       char const *name, void *var, uint64_t block_header,
       uint64_t bits) override {
-    auto &p = current_rewrite_event_->substitution[current_rewrite_event_->pos];
+    auto &p = current_rewrite_event_.substitution[current_rewrite_event_.pos];
     p.first = name;
     p.second.subject = var;
     p.second.block_header = block_header;
     p.second.bits = bits;
-    size_t new_pos = ++current_rewrite_event_->pos;
-    if (new_pos == current_rewrite_event_->arity) {
+    size_t new_pos = ++current_rewrite_event_.pos;
+    if (new_pos == current_rewrite_event_.arity) {
       if (rewrite_callback_pending_) {
-        rewrite_event_callback(current_rewrite_event_.value());
+        rewrite_event_callback(current_rewrite_event_);
         rewrite_callback_pending_ = false;
       } else {
-        side_condition_event_callback(current_rewrite_event_.value());
+        side_condition_event_callback(current_rewrite_event_);
       }
     }
   }
@@ -366,19 +366,17 @@ class proof_trace_callback_writer : public proof_trace_writer {
 
   void
   function_event_pre(char const *name, char const *location_stack) override {
-    current_call_event_.reset();
-    current_call_event_.emplace(name, location_stack);
+    current_call_event_.reinitialize(nullptr, name, location_stack);
   }
 
   void function_event_post() override {
-    function_event_callback(current_call_event_.value());
+    function_event_callback(current_call_event_);
   }
 
   void side_condition_event_pre(uint64_t ordinal, uint64_t arity) override {
-    current_rewrite_event_.reset();
-    current_rewrite_event_.emplace(ordinal, arity);
+    current_rewrite_event_.reinitialize(ordinal, arity);
     if (arity == 0) {
-      side_condition_event_callback(current_rewrite_event_.value());
+      side_condition_event_callback(current_rewrite_event_);
     }
   }