Using cache to speed up generation of GraphML file

Expression-to-string conversion is costly.

Author: marek-trtik

src/goto-programs/graphml_witness.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/ssa_expr.h>
+#include <util/string_container.h>
 
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
@@ -65,6 +66,15 @@ std::string graphml_witnesst::convert_assign_rec(
   const irep_idt &identifier,
   const code_assignt &assign)
 {
+#ifdef USE_DSTRING
+  const auto cit = cache.find({identifier.get_no(), &assign.read()});
+#else
+  const auto cit =
+    cache.find({get_string_container()[id2string(identifier)], &assign.read()});
+#endif
+  if(cit != cache.end())
+    return cit->second;
+
   std::string result;
 
   if(assign.rhs().id() == ID_array_list)
@@ -197,6 +207,12 @@ std::string graphml_witnesst::convert_assign_rec(
     result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";";
   }
 
+#ifdef USE_DSTRING
+  cache.insert({{identifier.get_no(), &assign.read()}, result});
+#else
+  cache.insert(
+    {{get_string_container()[id2string(identifier)], &assign.read()}, result});
+#endif
   return result;
 }
 

src/goto-programs/graphml_witness.h

@@ -42,6 +42,30 @@ class graphml_witnesst
   std::string convert_assign_rec(
     const irep_idt &identifier,
     const code_assignt &assign);
+
+  template <typename T>
+  static void hash_combine(std::size_t &seed, const T &v)
+  {
+    std::hash<T> hasher;
+    seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
+  }
+
+  template <typename S, typename T>
+  struct pair_hash // NOLINT(readability/identifiers)
+  {
+    std::size_t operator()(const std::pair<S, T> &v) const
+    {
+      std::size_t seed = 0;
+      hash_combine(seed, v.first);
+      hash_combine(seed, v.second);
+      return seed;
+    }
+  };
+  std::unordered_map<
+    std::pair<unsigned int, const irept::dt *>,
+    std::string,
+    pair_hash<unsigned int, const irept::dt *>>
+    cache;
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H