From aef1ae90a24a6e9cdc666a223f1874a6b59dc290 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 23 Mar 2018 19:20:07 +0000 Subject: [PATCH 1/2] irept: Use singly-linked lists with SUB_IS_LIST This reduces the memory footprint by up to 5 (GCC's STL) pointers for both named_sub. The cost is that computing the size of lists and add/remove require additional iterator increments. --- src/util/irep.cpp | 50 +++++++++++++++++++----- src/util/irep.h | 10 ++--- src/util/irep_hash_container.cpp | 10 ++++- src/util/lispirep.cpp | 8 +++- src/util/merge_irep.cpp | 65 ++++++++++++++++++++++++-------- unit/util/irep.cpp | 24 ++++++++---- 6 files changed, 127 insertions(+), 40 deletions(-) diff --git a/src/util/irep.cpp b/src/util/irep.cpp index b5fb653ae3f..01c77846025 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -152,9 +152,9 @@ void irept::nonrecursive_destructor(dt *old_data) if(d->ref_count==0) { - stack.reserve(stack.size()+ - d->named_sub.size()+ - d->sub.size()); + stack.reserve( + stack.size() + std::distance(d->named_sub.begin(), d->named_sub.end()) + + d->sub.size()); for(named_subt::iterator it=d->named_sub.begin(); @@ -263,7 +263,12 @@ void irept::remove(const irep_namet &name) named_subt::iterator it=named_subt_lower_bound(s, name); if(it!=s.end() && it->first==name) - s.erase(it); + { + named_subt::iterator before = s.before_begin(); + while(std::next(before) != it) + ++before; + s.erase_after(before); + } #else s.erase(name); #endif @@ -298,7 +303,12 @@ irept &irept::add(const irep_namet &name) if(it==s.end() || it->first!=name) - it=s.insert(it, std::make_pair(name, irept())); + { + named_subt::iterator before = s.before_begin(); + while(std::next(before) != it) + ++before; + it = s.emplace_after(before, name, irept()); + } return it->second; #else @@ -315,7 +325,12 @@ irept &irept::add(const irep_namet &name, const irept &irep) if(it==s.end() || it->first!=name) - it=s.insert(it, std::make_pair(name, irep)); + { + named_subt::iterator before = s.before_begin(); + while(std::next(before) != it) + ++before; + it = s.emplace_after(before, name, irep); + } else it->second=irep; @@ -407,13 +422,24 @@ bool irept::full_eq(const irept &other) const const irept::subt &i1_sub=get_sub(); const irept::subt &i2_sub=other.get_sub(); + + if(i1_sub.size() != i2_sub.size()) + return false; + const irept::named_subt &i1_named_sub=get_named_sub(); const irept::named_subt &i2_named_sub=other.get_named_sub(); +#ifdef SUB_IS_LIST if( - i1_sub.size() != i2_sub.size() || - i1_named_sub.size() != i2_named_sub.size()) + std::distance(i1_named_sub.begin(), i1_named_sub.end()) != + std::distance(i2_named_sub.begin(), i2_named_sub.end())) + { + return false; + } +#else + if(i1_named_sub.size() != i2_named_sub.size()) return false; +#endif for(std::size_t i=0; isecond.full_hash()); } - result = hash_finalize(result, named_sub.size() + sub.size()); +#ifdef SUB_IS_LIST + const std::size_t named_sub_size = + std::distance(named_sub.begin(), named_sub.end()); +#else + const std::size_t named_sub_size = named_sub.size(); +#endif + result = hash_finalize(result, named_sub_size + sub.size()); return result; } diff --git a/src/util/irep.h b/src/util/irep.h index 91c94b4cf6b..70e62be2c8d 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com // #define SUB_IS_LIST #ifdef SUB_IS_LIST -#include +#include #else #include #endif @@ -160,11 +160,11 @@ class irept // use std::forward_list or std::vector< unique_ptr > to save // memory and increase efficiency. - #ifdef SUB_IS_LIST - typedef std::list > named_subt; - #else +#ifdef SUB_IS_LIST + typedef std::forward_list> named_subt; +#else typedef std::map named_subt; - #endif +#endif bool is_nil() const { return id()==ID_nil; } bool is_not_nil() const { return id()!=ID_nil; } diff --git a/src/util/irep_hash_container.cpp b/src/util/irep_hash_container.cpp index bb88e0ae001..2d800ca1050 100644 --- a/src/util/irep_hash_container.cpp +++ b/src/util/irep_hash_container.cpp @@ -54,7 +54,13 @@ void irep_hash_container_baset::pack( { // we pack: the irep id, the sub size, the subs, the named-sub size, and // each of the named subs with their ids - packed.reserve(1 + 1 + sub.size() + 1 + named_sub.size() * 2); +#ifdef SUB_IS_LIST + const std::size_t named_sub_size = + std::distance(named_sub.begin(), named_sub.end()); +#else + const std::size_t named_sub_size = named_sub.size(); +#endif + packed.reserve(1 + 1 + sub.size() + 1 + named_sub_size * 2); packed.push_back(irep_id_hash()(irep.id())); @@ -62,7 +68,7 @@ void irep_hash_container_baset::pack( forall_irep(it, sub) packed.push_back(number(*it)); - packed.push_back(named_sub.size()); + packed.push_back(named_sub_size); for(const auto &sub_irep : named_sub) { packed.push_back(irep_id_hash()(sub_irep.first)); // id diff --git a/src/util/lispirep.cpp b/src/util/lispirep.cpp index 9ba1a3ceae7..8792acbfc40 100644 --- a/src/util/lispirep.cpp +++ b/src/util/lispirep.cpp @@ -46,7 +46,13 @@ void irep2lisp(const irept &src, lispexprt &dest) dest.value=""; dest.type=lispexprt::List; - dest.reserve(2 + 2 * src.get_sub().size() + 2 * src.get_named_sub().size()); +#ifdef SUB_IS_LIST + const std::size_t named_sub_size = + std::distance(src.get_named_sub().begin(), src.get_named_sub().end()); +#else + const std::size_t named_sub_size = src.get_named_sub().size(); +#endif + dest.reserve(2 + 2 * src.get_sub().size() + 2 * named_sub_size); lispexprt id; id.type=lispexprt::String; diff --git a/src/util/merge_irep.cpp b/src/util/merge_irep.cpp index 7937adb29cf..e8340f0031e 100644 --- a/src/util/merge_irep.cpp +++ b/src/util/merge_irep.cpp @@ -28,7 +28,13 @@ std::size_t to_be_merged_irept::hash() const result, static_cast(it->second).hash()); } - result=hash_finalize(result, named_sub.size()+sub.size()); +#ifdef SUB_IS_LIST + const std::size_t named_sub_size = + std::distance(named_sub.begin(), named_sub.end()); +#else + const std::size_t named_sub_size = named_sub.size(); +#endif + result = hash_finalize(result, named_sub_size + sub.size()); return result; } @@ -45,8 +51,17 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const if(sub.size()!=o_sub.size()) return false; +#ifdef SUB_IS_LIST + if( + std::distance(named_sub.begin(), named_sub.end()) != + std::distance(o_named_sub.begin(), o_named_sub.end())) + { + return false; + } +#else if(named_sub.size()!=o_named_sub.size()) return false; +#endif { irept::subt::const_iterator s_it=sub.begin(); @@ -95,13 +110,19 @@ const merged_irept &merged_irepst::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); +#ifdef SUB_IS_LIST + irept::named_subt::iterator before = dest_named_sub.before_begin(); +#endif forall_named_irep(it, src_named_sub) - #ifdef SUB_IS_LIST - dest_named_sub.push_back( - std::make_pair(it->first, merged(it->second))); // recursive call - #else + { +#ifdef SUB_IS_LIST + dest_named_sub.emplace_after( + before, it->first, merged(it->second)); // recursive call + ++before; +#else dest_named_sub[it->first]=merged(it->second); // recursive call - #endif +#endif + } std::pair result= to_be_merged_irep_store.insert(to_be_merged_irept(new_irep)); @@ -140,13 +161,19 @@ const irept &merge_irept::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); +#ifdef SUB_IS_LIST + irept::named_subt::iterator before = dest_named_sub.before_begin(); +#endif forall_named_irep(it, src_named_sub) - #ifdef SUB_IS_LIST - dest_named_sub.push_back( - std::make_pair(it->first, merged(it->second))); // recursive call - #else + { +#ifdef SUB_IS_LIST + dest_named_sub.emplace_after( + before, it->first, merged(it->second)); // recursive call + ++before; +#else dest_named_sub[it->first]=merged(it->second); // recursive call - #endif +#endif + } return *irep_store.insert(std::move(new_irep)).first; } @@ -177,13 +204,19 @@ const irept &merge_full_irept::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); +#ifdef SUB_IS_LIST + irept::named_subt::iterator before = dest_named_sub.before_begin(); +#endif forall_named_irep(it, src_named_sub) - #ifdef SUB_IS_LIST - dest_named_sub.push_back( - std::make_pair(it->first, merged(it->second))); // recursive call - #else + { +#ifdef SUB_IS_LIST + dest_named_sub.emplace_after( + before, it->first, merged(it->second)); // recursive call + ++before; +#else dest_named_sub[it->first]=merged(it->second); // recursive call - #endif +#endif + } return *irep_store.insert(std::move(new_irep)).first; } diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp index f22bbfd35e9..336e4140501 100644 --- a/unit/util/irep.cpp +++ b/unit/util/irep.cpp @@ -47,9 +47,9 @@ SCENARIO("irept_memory", "[core][utils][irept]") # endif # endif #else - const std::size_t named_size = sizeof(std::list); + const std::size_t named_size = sizeof(std::forward_list); # ifndef _GLIBCXX_DEBUG - REQUIRE(sizeof(std::list) == 3 * sizeof(void *)); + REQUIRE(sizeof(std::forward_list) == sizeof(void *)); # endif #endif @@ -140,12 +140,16 @@ SCENARIO("irept_memory", "[core][utils][irept]") irep.add("a_new_element", irep2); REQUIRE(!irept::is_comment("a_new_element")); REQUIRE(irep.find("a_new_element").id() == "second_irep"); - REQUIRE(irep.get_named_sub().size() == 1); + std::size_t named_sub_size = + std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end()); + REQUIRE(named_sub_size == 1); irep.add("#a_comment", irep2); REQUIRE(irept::is_comment("#a_comment")); REQUIRE(irep.find("#a_comment").id() == "second_irep"); - REQUIRE(irep.get_named_sub().size() == 2); + named_sub_size = + std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end()); + REQUIRE(named_sub_size == 2); REQUIRE(irept::number_of_non_comments(irep.get_named_sub()) == 1); irept bak(irep); @@ -160,17 +164,23 @@ SCENARIO("irept_memory", "[core][utils][irept]") irep.move_to_named_sub("another_entry", irep2); REQUIRE(irep.get_sub().size() == 1); - REQUIRE(irep.get_named_sub().size() == 2); + named_sub_size = + std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end()); + REQUIRE(named_sub_size == 2); irept irep3; irep.move_to_named_sub("#a_comment", irep3); REQUIRE(irep.find("#a_comment").id().empty()); REQUIRE(irep.get_sub().size() == 1); - REQUIRE(irep.get_named_sub().size() == 2); + named_sub_size = + std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end()); + REQUIRE(named_sub_size == 2); irept irep4; irep.move_to_named_sub("#another_comment", irep4); - REQUIRE(irep.get_named_sub().size() == 3); + named_sub_size = + std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end()); + REQUIRE(named_sub_size == 3); } THEN("Setting and getting works") From a4828df7939c245e0b2527a62f6150d251834788 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 20 Dec 2018 12:47:06 +0000 Subject: [PATCH 2/2] Rename SUB_IS_LIST define to NAMED_SUB_IS_FORWARD_LIST As suggested in code review. --- src/util/irep.cpp | 18 +++++++++--------- src/util/irep.h | 6 +++--- src/util/irep_hash_container.cpp | 2 +- src/util/lispirep.cpp | 2 +- src/util/merge_irep.cpp | 16 ++++++++-------- unit/util/irep.cpp | 2 +- 6 files changed, 23 insertions(+), 23 deletions(-) diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 01c77846025..e9778239ef6 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "string_hash.h" #include "irep_hash.h" -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST #include #endif @@ -31,7 +31,7 @@ irept nil_rep_storage; irept::dt irept::empty_d; #endif -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST static inline bool named_subt_order( const std::pair &a, const irep_namet &b) @@ -203,7 +203,7 @@ const irep_idt &irept::get(const irep_namet &name) const { const named_subt &s = get_named_sub(); -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST named_subt::const_iterator it=named_subt_lower_bound(s, name); if(it==s.end() || @@ -259,7 +259,7 @@ void irept::remove(const irep_namet &name) { named_subt &s = get_named_sub(); -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST named_subt::iterator it=named_subt_lower_bound(s, name); if(it!=s.end() && it->first==name) @@ -278,7 +278,7 @@ const irept &irept::find(const irep_namet &name) const { const named_subt &s = get_named_sub(); -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST named_subt::const_iterator it=named_subt_lower_bound(s, name); if(it==s.end() || @@ -298,7 +298,7 @@ irept &irept::add(const irep_namet &name) { named_subt &s = get_named_sub(); -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST named_subt::iterator it=named_subt_lower_bound(s, name); if(it==s.end() || @@ -320,7 +320,7 @@ irept &irept::add(const irep_namet &name, const irept &irep) { named_subt &s = get_named_sub(); -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST named_subt::iterator it=named_subt_lower_bound(s, name); if(it==s.end() || @@ -429,7 +429,7 @@ bool irept::full_eq(const irept &other) const const irept::named_subt &i1_named_sub=get_named_sub(); const irept::named_subt &i2_named_sub=other.get_named_sub(); -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST if( std::distance(i1_named_sub.begin(), i1_named_sub.end()) != std::distance(i2_named_sub.begin(), i2_named_sub.end())) @@ -693,7 +693,7 @@ std::size_t irept::full_hash() const result=hash_combine(result, it->second.full_hash()); } -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST const std::size_t named_sub_size = std::distance(named_sub.begin(), named_sub.end()); #else diff --git a/src/util/irep.h b/src/util/irep.h index 70e62be2c8d..6e96af7ba9f 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -20,9 +20,9 @@ Author: Daniel Kroening, kroening@kroening.com #define SHARING // #define HASH_CODE #define USE_MOVE -// #define SUB_IS_LIST +// #define NAMED_SUB_IS_FORWARD_LIST -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST #include #else #include @@ -160,7 +160,7 @@ class irept // use std::forward_list or std::vector< unique_ptr > to save // memory and increase efficiency. -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST typedef std::forward_list> named_subt; #else typedef std::map named_subt; diff --git a/src/util/irep_hash_container.cpp b/src/util/irep_hash_container.cpp index 2d800ca1050..7ef373be684 100644 --- a/src/util/irep_hash_container.cpp +++ b/src/util/irep_hash_container.cpp @@ -54,7 +54,7 @@ void irep_hash_container_baset::pack( { // we pack: the irep id, the sub size, the subs, the named-sub size, and // each of the named subs with their ids -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST const std::size_t named_sub_size = std::distance(named_sub.begin(), named_sub.end()); #else diff --git a/src/util/lispirep.cpp b/src/util/lispirep.cpp index 8792acbfc40..ec42c2dbf58 100644 --- a/src/util/lispirep.cpp +++ b/src/util/lispirep.cpp @@ -46,7 +46,7 @@ void irep2lisp(const irept &src, lispexprt &dest) dest.value=""; dest.type=lispexprt::List; -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST const std::size_t named_sub_size = std::distance(src.get_named_sub().begin(), src.get_named_sub().end()); #else diff --git a/src/util/merge_irep.cpp b/src/util/merge_irep.cpp index e8340f0031e..eeb0d45c733 100644 --- a/src/util/merge_irep.cpp +++ b/src/util/merge_irep.cpp @@ -28,7 +28,7 @@ std::size_t to_be_merged_irept::hash() const result, static_cast(it->second).hash()); } -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST const std::size_t named_sub_size = std::distance(named_sub.begin(), named_sub.end()); #else @@ -51,7 +51,7 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const if(sub.size()!=o_sub.size()) return false; -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST if( std::distance(named_sub.begin(), named_sub.end()) != std::distance(o_named_sub.begin(), o_named_sub.end())) @@ -110,12 +110,12 @@ const merged_irept &merged_irepst::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST irept::named_subt::iterator before = dest_named_sub.before_begin(); #endif forall_named_irep(it, src_named_sub) { -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST dest_named_sub.emplace_after( before, it->first, merged(it->second)); // recursive call ++before; @@ -161,12 +161,12 @@ const irept &merge_irept::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST irept::named_subt::iterator before = dest_named_sub.before_begin(); #endif forall_named_irep(it, src_named_sub) { -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST dest_named_sub.emplace_after( before, it->first, merged(it->second)); // recursive call ++before; @@ -204,12 +204,12 @@ const irept &merge_full_irept::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST irept::named_subt::iterator before = dest_named_sub.before_begin(); #endif forall_named_irep(it, src_named_sub) { -#ifdef SUB_IS_LIST +#ifdef NAMED_SUB_IS_FORWARD_LIST dest_named_sub.emplace_after( before, it->first, merged(it->second)); // recursive call ++before; diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp index 336e4140501..e5ac9c61b30 100644 --- a/unit/util/irep.cpp +++ b/unit/util/irep.cpp @@ -35,7 +35,7 @@ SCENARIO("irept_memory", "[core][utils][irept]") REQUIRE(sizeof(std::vector) == 3 * sizeof(void *)); #endif -#ifndef SUB_IS_LIST +#ifndef NAMED_SUB_IS_FORWARD_LIST const std::size_t named_size = sizeof(std::map); # ifndef _GLIBCXX_DEBUG # ifdef __APPLE__