Use sharing_map instead of unordered_map for cache

Author: TGWDB

src/goto-symex/goto_state.cpp

@@ -12,27 +12,6 @@ Author: Romain Brenguier, [email protected]
 
 #include <util/format_expr.h>
 
-optionalt<symbol_exprt>
-dereference_cachet::lookup(const exprt &dereference) const
-{
-  auto it = cache.find(dereference);
-  if(it == cache.end())
-  {
-    return nullopt;
-  }
-  else
-  {
-    return {it->second};
-  }
-}
-
-void dereference_cachet::insert(
-  exprt new_cached_expr,
-  symbol_exprt new_cache_symbol)
-{
-  cache.emplace(std::move(new_cached_expr), std::move(new_cache_symbol));
-}
-
 /// Print the constant propagation map in a human-friendly format.
 /// This is primarily for use from the debugger; please don't delete me just
 /// because there aren't any current callers.

src/goto-symex/goto_state.h

@@ -24,19 +24,6 @@ Author: Romain Brenguier, [email protected]
 // by the parent class.
 class goto_symex_statet;
 
-/// This is used for eliminating repeated complicated dereferences.
-/// This is pretty much just a simple wrapper around a map.
-/// \see goto_symext::dereference_rec
-struct dereference_cachet
-{
-private:
-  std::unordered_map<exprt, symbol_exprt, irep_hash> cache;
-
-public:
-  optionalt<symbol_exprt> lookup(const exprt &pointer) const;
-  void insert(exprt new_cached_pointer_expr, symbol_exprt new_cache_symbol);
-};
-
 /// Container for data that varies per program point, e.g. the constant
 /// propagator state, when state needs to branch. This is copied out of
 /// goto_symex_statet at a control-flow fork and then back into it at a
@@ -51,7 +38,9 @@ class goto_statet
   symex_level2t level2;
 
 public:
-  dereference_cachet dereference_cache;
+  /// This is used for eliminating repeated complicated dereferences.
+  /// \see goto_symext::dereference_rec
+  sharing_mapt<exprt, symbol_exprt, false, irep_hash> dereference_cache;
 
   const symex_level2t &get_level2() const
   {

src/goto-symex/symex_dereference.cpp

@@ -211,7 +211,7 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
     return cache_key;
   }();
 
-  if(auto cached = state.dereference_cache.lookup(cache_key))
+  if(auto cached = state.dereference_cache.find(cache_key))
   {
     return *cached;
   }