From 6610eef6ae4fc85ae78f74eaafc29ccbb389eece Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 28 Oct 2020 14:39:52 +0000 Subject: [PATCH 1/7] Reuse existing type definitions in `union_find` Removing the duplicated types will enable changing the type of numbering which backs union find, with fewer lines of code changed. --- src/util/union_find.h | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/util/union_find.h b/src/util/union_find.h index b71422bad58..5859db02a81 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -160,8 +160,7 @@ class union_find final } // true == already in same set - bool make_union(typename numbering::const_iterator it_a, - typename numbering::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 +182,12 @@ class union_find final } // are 'a' and 'b' in the same set? - bool same_set(typename numbering::const_iterator it_a, - typename numbering::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::const_iterator it) const + const T &find(const_iterator it) const { return numbers[find_number(it-numbers.begin())]; } @@ -199,7 +197,7 @@ class union_find final return numbers[find_number(number(a))]; } - size_type find_number(typename numbering::const_iterator it) const + size_type find_number(const_iterator it) const { return find_number(it-numbers.begin()); } @@ -228,7 +226,7 @@ class union_find final return uuf.is_root(na); } - bool is_root(typename numbering::const_iterator it) const + bool is_root(const_iterator it) const { return uuf.is_root(it-numbers.begin()); } @@ -251,7 +249,7 @@ class union_find final uuf.clear(); } - void isolate(typename numbering::const_iterator it) + void isolate(const_iterator it) { uuf.isolate(it-numbers.begin()); } @@ -281,7 +279,7 @@ class union_find final protected: unsigned_union_find uuf; - typedef numbering subt; + typedef numbering_typet subt; }; #endif // CPROVER_UTIL_UNION_FIND_H From 3d99edf23a39210f99e41c75e0484c57fe7bf5ee Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 28 Oct 2020 15:44:48 +0000 Subject: [PATCH 2/7] Use `using` instead of `typedef` in `union_find` Because this matches the current coding standard and because it improves readability. --- src/util/union_find.h | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/util/union_find.h b/src/util/union_find.h index 5859db02a81..239793654d7 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -136,19 +136,19 @@ template // NOLINTNEXTLINE(readability/identifiers) class union_find final { - typedef numbering numbering_typet; + using numbering_typet = numbering; 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) @@ -279,7 +279,7 @@ class union_find final protected: unsigned_union_find uuf; - typedef numbering_typet subt; + using subt = numbering_typet; }; #endif // CPROVER_UTIL_UNION_FIND_H From e1acd5638c1d46bc2a652b6bd551540b1b566f26 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 28 Oct 2020 17:41:29 +0000 Subject: [PATCH 3/7] Define new `numberingt` This commit defines a new `numberingt`, which is equivalent to the existing `hash_numbering` type. This new name and its template parameters match the cbmc coding standards by ending the type names with a letter 't'. It also supports using `std::hash` by default, which will saves passing a hash function in the case where there is a standard hash function defined for a given type of `keyt`. The intention is to add this new type in this commit, swap over the existing usages of numbering in the subsequent commits and then finally remove the old variations of numbering. This will improve performance in one instance and will improve maintainability in others. Maintainability will be improved with a single version, because there won't be multiple versions to maintain and it will take away the possibility of accidentally choosing a variation which uses `irept` as the key in the backing `std::map`. --- src/util/numbering.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/util/numbering.h b/src/util/numbering.h index b658bc299c3..b1a254bcd90 100644 --- a/src/util/numbering.h +++ b/src/util/numbering.h @@ -116,4 +116,10 @@ template using hash_numbering = // NOLINT template_numberingt>; +/// \tparam keyt: The type of keys which will be numbered. +/// \tparam hasht: The type of hashing functor used to hash keys. +template > +using numberingt = + template_numberingt>; + #endif // CPROVER_UTIL_NUMBERING_H From b9f8fdda87467fd313368b8d8176830426afa59b Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 28 Oct 2020 12:12:44 +0000 Subject: [PATCH 4/7] Make `union_find` use hashes for numbering This avoids slow lookups into `std::map` caused by long running `irept::operator<` calls. The type of hash to use is included as a template parameter in order to make the data structure used to implement `union_find` more explicit. Run time on example exercising arrays code before this commit - real 2m39.018s user 2m37.394s sys 0m1.608s Run time on example exercising arrays code after this commit - real 0m30.897s user 0m29.476s sys 0m1.404s --- src/solvers/flattening/arrays.h | 2 +- src/util/union_find.h | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index b556c76b1d2..9a74d66dd65 100644 --- 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 arrays; + union_find arrays; // this tracks the array indicies for each array typedef std::set index_sett; diff --git a/src/util/union_find.h b/src/util/union_find.h index 239793654d7..81bac4b2740 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -132,11 +132,13 @@ class unsigned_union_find size_type get_other(size_type a); }; -template +/// \tparam T: The type of values stored. +/// \tparam hasht: The type of hash used for looking up the value numbering. +template > // NOLINTNEXTLINE(readability/identifiers) class union_find final { - using numbering_typet = numbering; + using numbering_typet = numberingt; numbering_typet numbers; // NOLINTNEXTLINE(readability/identifiers) From 30957a4b696b803c6665ac82d95ccaf9c6464713 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 28 Oct 2020 17:55:15 +0000 Subject: [PATCH 5/7] Use `numberingt` in place of `hash_numberingt` Because the naming follows our coding standards and it reduces the number of numbering variations to maintain. --- src/analyses/invariant_set.h | 2 +- src/pointer-analysis/object_numbering.h | 2 +- src/pointer-analysis/value_set_fi.cpp | 2 +- src/pointer-analysis/value_set_fi.h | 2 +- src/pointer-analysis/value_set_fivr.h | 2 +- src/pointer-analysis/value_set_fivrns.h | 2 +- src/solvers/flattening/pointer_logic.h | 2 +- src/util/irep_hash_container.h | 3 +-- src/util/numbering.h | 4 ---- 9 files changed, 8 insertions(+), 13 deletions(-) diff --git a/src/analyses/invariant_set.h b/src/analyses/invariant_set.h index d26df7fe7d4..cd70ba9af9a 100644 --- 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 mapt; + typedef numbering mapt; mapt map; struct entryt diff --git a/src/pointer-analysis/object_numbering.h b/src/pointer-analysis/object_numbering.h index 4e51a68f8fc..0e0250d4856 100644 --- 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 #include -typedef hash_numbering object_numberingt; +typedef numberingt 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 index ce518c36442..eafb928a06a 100644 --- 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 value_set_fit::function_numbering; +numberingt 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 index d96f4c0a80a..795d13d666f 100644 --- 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 function_numbering; + static numberingt 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 index adb95534526..f37202df954 100644 --- 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 function_numbering; + static numberingt 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 index d89196e68a9..b9c628d9a6f 100644 --- 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 function_numbering; + static numberingt function_numbering; void set_from(const irep_idt &function, unsigned inx) { diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h index 5e9636ce08f..8736c4ae28c 100644 --- 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 objects; + numberingt objects; struct pointert { diff --git a/src/util/irep_hash_container.h b/src/util/irep_hash_container.h index 58c64525d7f..3ece8bf4587 100644 --- 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 numberingt; - numberingt numbering; + numberingt numbering; void pack(const irept &irep, packedt &); diff --git a/src/util/numbering.h b/src/util/numbering.h index b1a254bcd90..f931d2cc47b 100644 --- a/src/util/numbering.h +++ b/src/util/numbering.h @@ -112,10 +112,6 @@ class template_numberingt final template using numbering = template_numberingt>; // NOLINT -template -using hash_numbering = // NOLINT - template_numberingt>; - /// \tparam keyt: The type of keys which will be numbered. /// \tparam hasht: The type of hashing functor used to hash keys. template > From d3f5cda48baaf2b9bd710041627d4773b99de8ec Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 28 Oct 2020 17:59:29 +0000 Subject: [PATCH 6/7] Use `numberingt` in place of `numbering` Because the naming follows our coding standards and it reduces the number of numbering variations to maintain. This does change the type of backing container used in these places, however the performance should be at least equivalent. --- src/analyses/custom_bitvector_analysis.h | 2 +- src/analyses/escape_analysis.h | 2 +- src/analyses/invariant_set.h | 2 +- src/analyses/local_bitvector_analysis.h | 2 +- src/analyses/local_may_alias.h | 2 +- src/goto-programs/vcd_goto_trace.cpp | 2 +- src/solvers/flattening/boolbv.h | 2 +- src/util/numbering.h | 4 ---- 8 files changed, 7 insertions(+), 11 deletions(-) diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index 511c3093833..1585b28159c 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -163,7 +163,7 @@ class custom_bitvector_analysist:public ait unsigned get_bit_nr(const exprt &); - typedef numbering bitst; + typedef numberingt bitst; bitst bits; protected: diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h index 7107fa310f5..fe7ab348cfc 100644 --- a/src/analyses/escape_analysis.h +++ b/src/analyses/escape_analysis.h @@ -120,7 +120,7 @@ class escape_analysist:public ait { } - numbering bits; + numberingt bits; void insert_cleanup( goto_functionst::goto_functiont &, diff --git a/src/analyses/invariant_set.h b/src/analyses/invariant_set.h index cd70ba9af9a..421bd153052 100644 --- 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 numbering mapt; + typedef numberingt mapt; mapt map; struct entryt diff --git a/src/analyses/local_bitvector_analysis.h b/src/analyses/local_bitvector_analysis.h index e675ef5d876..3151a14e9eb 100644 --- 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 work_queuet; - numbering pointers; + numberingt 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 index 307513a64eb..a07aaa8e586 100644 --- 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 work_queuet; - mutable numbering objects; + mutable numberingt 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 index f14749c2433..d06308abd23 100644 --- 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 n; + numberingt n; for(const auto &step : goto_trace.steps) { diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 28f4245a270..ad2ebf26b2f 100644 --- 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 string_numbering; + numberingt string_numbering; }; #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H diff --git a/src/util/numbering.h b/src/util/numbering.h index f931d2cc47b..dbee18952a8 100644 --- a/src/util/numbering.h +++ b/src/util/numbering.h @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_NUMBERING_H #define CPROVER_UTIL_NUMBERING_H -#include #include #include @@ -109,9 +108,6 @@ class template_numberingt final } }; -template -using numbering = template_numberingt>; // NOLINT - /// \tparam keyt: The type of keys which will be numbered. /// \tparam hasht: The type of hashing functor used to hash keys. template > From 2bf69bfa1d7d6f5722631090b32e2ebcc30ef46f Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 28 Oct 2020 18:07:15 +0000 Subject: [PATCH 7/7] Define `numberingt` as the implementation There is no need for separate a separe type alias and implementaion if numbering is always done using the same kind of map. Therefore we can use a single name instead of two, which means less to maintain. --- src/util/numbering.h | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/src/util/numbering.h b/src/util/numbering.h index dbee18952a8..ea9fc6e94eb 100644 --- a/src/util/numbering.h +++ b/src/util/numbering.h @@ -15,18 +15,19 @@ Author: Daniel Kroening, kroening@kroening.com #include "invariant.h" #include "optional.h" -/// \tparam Map: a map from a key type to some numeric type -template -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 > +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; // NOLINT data_typet data_; - Map numbers_; + std::unordered_map numbers_; public: using size_type = typename data_typet::size_type; // NOLINT @@ -108,10 +109,5 @@ 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 > -using numberingt = - template_numberingt>; #endif // CPROVER_UTIL_NUMBERING_H