Merge pull request #5539 from thomasspriggs/tas/arrays_optimisation

tautschnig · web-flow · commit 610761e625b5 · 2020-11-10T13:36:38.000+01:00
Performance optimisation - Use `unordered_map` in `numbering` instead of `map`
diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h
@@ -163,7 +163,7 @@ class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
 
   unsigned get_bit_nr(const exprt &);
 
-  typedef numbering<irep_idt> bitst;
+  typedef numberingt<irep_idt> bitst;
   bitst bits;
 
 protected:
diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h
@@ -120,7 +120,7 @@ class escape_analysist:public ait<escape_domaint>
   {
   }
 
-  numbering<irep_idt> bits;
+  numberingt<irep_idt> bits;
 
   void insert_cleanup(
     goto_functionst::goto_functiont &,
diff --git a/src/analyses/invariant_set.h b/src/analyses/invariant_set.h
@@ -55,7 +55,7 @@ class inv_object_storet
 protected:
   const namespacet &ns;
 
-  typedef hash_numbering<irep_idt, irep_id_hash> mapt;
+  typedef numberingt<irep_idt> mapt;
   mapt map;
 
   struct entryt
diff --git a/src/analyses/local_bitvector_analysis.h b/src/analyses/local_bitvector_analysis.h
@@ -183,7 +183,7 @@ class local_bitvector_analysist
 
   typedef std::stack<unsigned> work_queuet;
 
-  numbering<irep_idt> pointers;
+  numberingt<irep_idt> pointers;
 
   // pointers -> flagst
   // This is a vector, so it's fast.
diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h
@@ -60,7 +60,7 @@ class local_may_aliast
 
   typedef std::stack<local_cfgt::node_nrt> work_queuet;
 
-  mutable numbering<exprt> objects;
+  mutable numberingt<exprt, irep_hash> objects;
 
   typedef unsigned_union_find alias_sett;
 
diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp
@@ -82,7 +82,7 @@ void output_vcd(
 
   // we first collect all variables that are assigned
 
-  numbering<irep_idt> n;
+  numberingt<irep_idt> n;
 
   for(const auto &step : goto_trace.steps)
   {
diff --git a/src/pointer-analysis/object_numbering.h b/src/pointer-analysis/object_numbering.h
@@ -25,6 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr.h>
 #include <util/numbering.h>
 
-typedef hash_numbering<exprt, irep_hash> object_numberingt;
+typedef numberingt<exprt, irep_hash> object_numberingt;
 
 #endif // CPROVER_POINTER_ANALYSIS_OBJECT_NUMBERING_H
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
@@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 const value_set_fit::object_map_dt value_set_fit::object_map_dt::blank{};
 
 object_numberingt value_set_fit::object_numbering;
-hash_numbering<irep_idt, irep_id_hash> value_set_fit::function_numbering;
+numberingt<irep_idt> value_set_fit::function_numbering;
 
 static const char *alloc_adapter_prefix="alloc_adaptor::";
 
diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
@@ -39,7 +39,7 @@ class value_set_fit
   unsigned to_function, from_function;
   unsigned to_target_index, from_target_index;
   static object_numberingt object_numbering;
-  static hash_numbering<irep_idt, irep_id_hash> function_numbering;
+  static numberingt<irep_idt> function_numbering;
 
   void set_from(const irep_idt &function, unsigned inx)
   {
diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h
@@ -36,7 +36,7 @@ class value_set_fivrt
   unsigned to_function, from_function;
   unsigned to_target_index, from_target_index;
   static object_numberingt object_numbering;
-  static hash_numbering<irep_idt, irep_id_hash> function_numbering;
+  static numberingt<irep_idt> function_numbering;
 
   void set_from(const irep_idt &function, unsigned inx)
   {
diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h
@@ -37,7 +37,7 @@ class value_set_fivrnst
   unsigned to_function, from_function;
   unsigned to_target_index, from_target_index;
   static object_numberingt object_numbering;
-  static hash_numbering<irep_idt, irep_id_hash> function_numbering;
+  static numberingt<irep_idt> function_numbering;
 
   void set_from(const irep_idt &function, unsigned inx)
   {
diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h
@@ -68,7 +68,7 @@ class arrayst:public equalityt
   array_equalitiest array_equalities;
 
   // this is used to find the clusters of arrays being compared
-  union_find<exprt> arrays;
+  union_find<exprt, irep_hash> arrays;
 
   // this tracks the array indicies for each array
   typedef std::set<exprt> index_sett;
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
@@ -262,7 +262,7 @@ class boolbvt:public arrayst
   offset_mapt build_offset_map(const struct_typet &src);
 
   // strings
-  numbering<irep_idt> string_numbering;
+  numberingt<irep_idt> string_numbering;
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H
diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h
@@ -23,7 +23,7 @@ class pointer_logict
 {
 public:
   // this numbers the objects
-  hash_numbering<exprt, irep_hash> objects;
+  numberingt<exprt, irep_hash> objects;
 
   struct pointert
   {
diff --git a/src/util/irep_hash_container.h b/src/util/irep_hash_container.h
@@ -69,8 +69,7 @@ class irep_hash_container_baset
     std::size_t operator()(const packedt &p) const;
   };
 
-  typedef hash_numbering<packedt, vector_hasht> numberingt;
-  numberingt numbering;
+  numberingt<packedt, vector_hasht> numbering;
 
   void pack(const irept &irep, packedt &);
 
diff --git a/src/util/numbering.h b/src/util/numbering.h
@@ -9,25 +9,25 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_NUMBERING_H
 #define CPROVER_UTIL_NUMBERING_H
 
-#include <map>
 #include <unordered_map>
 #include <vector>
 
 #include "invariant.h"
 #include "optional.h"
 
-/// \tparam Map: a map from a key type to some numeric type
-template <typename Map>
-class template_numberingt final
+/// \tparam keyt: The type of keys which will be numbered.
+/// \tparam hasht: The type of hashing functor used to hash keys.
+template <typename keyt, typename hasht = std::hash<keyt>>
+class numberingt final
 {
 public:
-  using number_type = typename Map::mapped_type; // NOLINT
-  using key_type = typename Map::key_type;       // NOLINT
+  using number_type = std::size_t; // NOLINT
+  using key_type = keyt;           // NOLINT
 
 private:
   using data_typet = std::vector<key_type>; // NOLINT
   data_typet data_;
-  Map numbers_;
+  std::unordered_map<keyt, number_type, hasht> numbers_;
 
 public:
   using size_type = typename data_typet::size_type;           // NOLINT
@@ -109,11 +109,5 @@ class template_numberingt final
   }
 };
 
-template <typename Key>
-using numbering = template_numberingt<std::map<Key, std::size_t>>; // NOLINT
-
-template <typename Key, typename Hash>
-using hash_numbering = // NOLINT
-  template_numberingt<std::unordered_map<Key, std::size_t, Hash>>;
 
 #endif // CPROVER_UTIL_NUMBERING_H
diff --git a/src/util/union_find.h b/src/util/union_find.h
@@ -132,23 +132,25 @@ class unsigned_union_find
   size_type get_other(size_type a);
 };
 
-template <typename T>
+/// \tparam T: The type of values stored.
+/// \tparam hasht: The type of hash used for looking up the value numbering.
+template <typename T, typename hasht = std::hash<T>>
 // NOLINTNEXTLINE(readability/identifiers)
 class union_find final
 {
-  typedef numbering<T> numbering_typet;
+  using numbering_typet = numberingt<T, hasht>;
   numbering_typet numbers;
 
   // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename numbering_typet::number_type number_type;
+  using number_type = typename numbering_typet::number_type;
 
 public:
   // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename numbering_typet::size_type size_type;
+  using size_type = typename numbering_typet::size_type;
   // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename numbering_typet::iterator iterator;
+  using iterator = typename numbering_typet::iterator;
   // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename numbering_typet::const_iterator const_iterator;
+  using const_iterator = typename numbering_typet::const_iterator;
 
   // true == already in same set
   bool make_union(const T &a, const T &b)
@@ -160,8 +162,7 @@ class union_find final
   }
 
   // true == already in same set
-  bool make_union(typename numbering<T>::const_iterator it_a,
-                  typename numbering<T>::const_iterator it_b)
+  bool make_union(const_iterator it_a, const_iterator it_b)
   {
     size_type na=it_a-numbers.begin(), nb=it_b-numbers.begin();
     bool is_union=find_number(na)==find_number(nb);
@@ -183,13 +184,12 @@ class union_find final
   }
 
   // are 'a' and 'b' in the same set?
-  bool same_set(typename numbering<T>::const_iterator it_a,
-                typename numbering<T>::const_iterator it_b) const
+  bool same_set(const_iterator it_a, const_iterator it_b) const
   {
     return uuf.same_set(it_a-numbers.begin(), it_b-numbers.begin());
   }
 
-  const T &find(typename numbering<T>::const_iterator it) const
+  const T &find(const_iterator it) const
   {
     return numbers[find_number(it-numbers.begin())];
   }
@@ -199,7 +199,7 @@ class union_find final
     return numbers[find_number(number(a))];
   }
 
-  size_type find_number(typename numbering<T>::const_iterator it) const
+  size_type find_number(const_iterator it) const
   {
     return find_number(it-numbers.begin());
   }
@@ -228,7 +228,7 @@ class union_find final
       return uuf.is_root(na);
   }
 
-  bool is_root(typename numbering<T>::const_iterator it) const
+  bool is_root(const_iterator it) const
   {
     return uuf.is_root(it-numbers.begin());
   }
@@ -251,7 +251,7 @@ class union_find final
     uuf.clear();
   }
 
-  void isolate(typename numbering<T>::const_iterator it)
+  void isolate(const_iterator it)
   {
     uuf.isolate(it-numbers.begin());
   }
@@ -281,7 +281,7 @@ class union_find final
 
 protected:
   unsigned_union_find uuf;
-  typedef numbering<T> subt;
+  using subt = numbering_typet;
 };
 
 #endif // CPROVER_UTIL_UNION_FIND_H

Original file line number	Diff line number	Diff line change
`@@ -120,7 +120,7 @@ class escape_analysist:public ait<escape_domaint>`
`120`	`120`	`{`
`121`	`121`	`}`
`122`	`122`
`123`		`- numbering<irep_idt> bits;`
	`123`	`+ numberingt<irep_idt> bits;`
`124`	`124`
`125`	`125`	`void insert_cleanup(`
`126`	`126`	`goto_functionst::goto_functiont &,`
Original file line number	Diff line number	Diff line change
`@@ -82,7 +82,7 @@ void output_vcd(`
`82`	`82`
`83`	`83`	`// we first collect all variables that are assigned`
`84`	`84`
`85`		`- numbering<irep_idt> n;`
	`85`	`+ numberingt<irep_idt> n;`
`86`	`86`
`87`	`87`	`for(const auto &step : goto_trace.steps)`
`88`	`88`	`{`
Original file line number	Diff line number	Diff line change
`@@ -39,7 +39,7 @@ class value_set_fit`
`39`	`39`	`unsigned to_function, from_function;`
`40`	`40`	`unsigned to_target_index, from_target_index;`
`41`	`41`	`static object_numberingt object_numbering;`
`42`		`- static hash_numbering<irep_idt, irep_id_hash> function_numbering;`
	`42`	`+ static numberingt<irep_idt> function_numbering;`
`43`	`43`
`44`	`44`	`void set_from(const irep_idt &function, unsigned inx)`
`45`	`45`	`{`
Original file line number	Diff line number	Diff line change
`@@ -36,7 +36,7 @@ class value_set_fivrt`
`36`	`36`	`unsigned to_function, from_function;`
`37`	`37`	`unsigned to_target_index, from_target_index;`
`38`	`38`	`static object_numberingt object_numbering;`
`39`		`- static hash_numbering<irep_idt, irep_id_hash> function_numbering;`
	`39`	`+ static numberingt<irep_idt> function_numbering;`
`40`	`40`
`41`	`41`	`void set_from(const irep_idt &function, unsigned inx)`
`42`	`42`	`{`