From 8affad0554867aa995092f189822aef59c5ae99a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <michael.tautschnig@qmul.ac.uk>
Date: Mon, 26 Dec 2016 12:30:50 +0000
Subject: [PATCH] Enable HASH_CODE by default to avoid repeated hash
 computation

On some SV-COMP benchmark categories, hashing accounts for >20% of CPU
time (with profiling enabled) - top five:

* ReachSafety-BitVectors: 29.29% (470.54 seconds, which reduces to 4.39
  seconds; for benchmarks not timing out we save 170 seconds (25%) in
  non-profiling mode)
* Systems_BusyBox_NoOverflows: 27.98% (284.15 seconds, which reduces to
  1.74 seconds; for the 1 benchmark not timing out we save 23 seconds
  (6%) in non-profiling mode)
* Systems_BusyBox_MemSafety: 24.24% (194.74 seconds, which reduces to
  0.93 seconds; no measurable difference on the 2 benchmarks not
  failing/timing out)
* NoOverflows-Other: 18.84% (1127.61 seconds, which reduces to
  23.57 seconds; for benchmarks not timing out we save 5 seconds (7%) in
  non-profiling mode)
* ReachSafety-ControlFlow: 17.75% (1194.04 seconds, which reduces to
  29.17 seconds; for benchmarks not timing out we save 200 seconds (25%)
  in non-profiling mode)

For ReachSafety-ECA it's only 4.7%, which still amounts to 3006.7
seconds. With this change this reduces to 323.07 seconds. On
ReachSafety-ECA, this enables 3055.35 symex_step calls per second over
2752.28 calls per second without this change.
---
 src/solvers/smt2/letify.h    |  2 +-
 src/solvers/smt2/smt2_conv.h |  4 ++--
 src/util/irep.cpp            |  4 ++--
 src/util/irep.h              | 14 ++++++++------
 unit/util/irep.cpp           |  2 +-
 5 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/src/solvers/smt2/letify.h b/src/solvers/smt2/letify.h
index 71085432b2d..6a5239a2e9d 100644
--- a/src/solvers/smt2/letify.h
+++ b/src/solvers/smt2/letify.h
@@ -33,7 +33,7 @@ class letifyt
     symbol_exprt let_symbol;
   };
 
-#ifdef HASH_CODE
+#if HASH_CODE
   using seen_expressionst = std::unordered_map<exprt, let_count_idt, irep_hash>;
 #else
   using seen_expressionst = irep_hash_mapt<exprt, let_count_idt>;
diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h
index b66883496bc..47c17f395fe 100644
--- a/src/solvers/smt2/smt2_conv.h
+++ b/src/solvers/smt2/smt2_conv.h
@@ -16,8 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/byte_operators.h>
 
-#ifndef HASH_CODE
-#include <util/irep_hash_container.h>
+#if !HASH_CODE
+#  include <util/irep_hash_container.h>
 #endif
 
 #include <solvers/prop/prop_conv.h>
diff --git a/src/util/irep.cpp b/src/util/irep.cpp
index 543c7b662ff..8f4074e89bf 100644
--- a/src/util/irep.cpp
+++ b/src/util/irep.cpp
@@ -519,7 +519,7 @@ std::size_t irept::number_of_non_comments(const named_subt &named_sub)
 
 std::size_t irept::hash() const
 {
-  #ifdef HASH_CODE
+#if HASH_CODE
   if(read().hash_code!=0)
     return read().hash_code;
   #endif
@@ -543,7 +543,7 @@ std::size_t irept::hash() const
 
   result = hash_finalize(result, sub.size() + number_of_named_ireps);
 
-#ifdef HASH_CODE
+#if HASH_CODE
   read().hash_code=result;
 #endif
 #ifdef IREP_HASH_STATS
diff --git a/src/util/irep.h b/src/util/irep.h
index 3cb27175392..ee955d1048b 100644
--- a/src/util/irep.h
+++ b/src/util/irep.h
@@ -17,7 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "irep_ids.h"
 
 #define SHARING
-// #define HASH_CODE
+#ifndef HASH_CODE
+#  define HASH_CODE 1
+#endif
 // #define NAMED_SUB_IS_FORWARD_LIST
 
 #ifdef NAMED_SUB_IS_FORWARD_LIST
@@ -138,7 +140,7 @@ class tree_nodet : public ref_count_ift<sharing>
   named_subt named_sub;
   subt sub;
 
-#ifdef HASH_CODE
+#if HASH_CODE
   mutable std::size_t hash_code = 0;
 #endif
 
@@ -147,7 +149,7 @@ class tree_nodet : public ref_count_ift<sharing>
     data.clear();
     sub.clear();
     named_sub.clear();
-#ifdef HASH_CODE
+#if HASH_CODE
     hash_code = 0;
 #endif
   }
@@ -157,7 +159,7 @@ class tree_nodet : public ref_count_ift<sharing>
     d.data.swap(data);
     d.sub.swap(sub);
     d.named_sub.swap(named_sub);
-#ifdef HASH_CODE
+#if HASH_CODE
     std::swap(d.hash_code, hash_code);
 #endif
   }
@@ -278,7 +280,7 @@ class sharing_treet
   dt &write()
   {
     detach();
-#ifdef HASH_CODE
+#if HASH_CODE
     data->hash_code = 0;
 #endif
     return *data;
@@ -319,7 +321,7 @@ class non_sharing_treet
 
   dt &write()
   {
-#ifdef HASH_CODE
+#if HASH_CODE
     data.hash_code = 0;
 #endif
     return data;
diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp
index f0d45369432..d9da47bb18b 100644
--- a/unit/util/irep.cpp
+++ b/unit/util/irep.cpp
@@ -53,7 +53,7 @@ SCENARIO("irept_memory", "[core][utils][irept]")
 #  endif
 #endif
 
-#ifdef HASH_CODE
+#if HASH_CODE
       const std::size_t hash_code_size = sizeof(std::size_t);
 #else
       const std::size_t hash_code_size = 0;