From bbeea251ec8eb40e4f271a6e66185dfbced8af63 Mon Sep 17 00:00:00 2001 From: reuk Date: Mon, 20 Mar 2017 22:52:22 +0000 Subject: [PATCH 1/2] Use shared_ptr in irept --- src/util/irep.cpp | 192 ++----------------------------- src/util/irep.h | 254 +++++++++++++----------------------------- src/util/merge_irep.h | 9 +- 3 files changed, 88 insertions(+), 367 deletions(-) diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 886f8ce9d7b..07c16006778 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -6,26 +6,20 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include -#include - -#include "string2int.h" #include "irep.h" -#include "string_hash.h" #include "irep_hash.h" +#include "string2int.h" +#include "string_hash.h" + +#include +#include #ifdef SUB_IS_LIST #include #endif -#ifdef IREP_DEBUG -#include -#endif - -irept nil_rep_storage; - #ifdef SHARING -irept::dt irept::empty_d; +std::shared_ptr irept::empty=std::make_shared
(); #endif /*******************************************************************\ @@ -75,6 +69,7 @@ Function: get_nil_irep const irept &get_nil_irep() { + static irept nil_rep_storage; if(nil_rep_storage.id().empty()) // initialized? nil_rep_storage.id(ID_nil); return nil_rep_storage; @@ -82,173 +77,6 @@ const irept &get_nil_irep() /*******************************************************************\ -Function: irept::detach - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -#ifdef SHARING -void irept::detach() -{ - #ifdef IREP_DEBUG - std::cout << "DETACH1: " << data << std::endl; - #endif - - if(data==&empty_d) - { - data=new dt; - - #ifdef IREP_DEBUG - std::cout << "ALLOCATED " << data << std::endl; - #endif - } - else if(data->ref_count>1) - { - dt *old_data(data); - data=new dt(*old_data); - - #ifdef IREP_DEBUG - std::cout << "ALLOCATED " << data << std::endl; - #endif - - data->ref_count=1; - remove_ref(old_data); - } - - assert(data->ref_count==1); - - #ifdef IREP_DEBUG - std::cout << "DETACH2: " << data << std::endl; - #endif -} -#endif - -/*******************************************************************\ - -Function: irept::remove_ref - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -#ifdef SHARING -void irept::remove_ref(dt *old_data) -{ - if(old_data==&empty_d) - return; - - #if 0 - nonrecursive_destructor(old_data); - #else - - assert(old_data->ref_count!=0); - - #ifdef IREP_DEBUG - std::cout << "R: " << old_data << " " << old_data->ref_count << std::endl; - #endif - - old_data->ref_count--; - if(old_data->ref_count==0) - { - #ifdef IREP_DEBUG - std::cout << "D: " << pretty() << std::endl; - std::cout << "DELETING " << old_data->data - << " " << old_data << std::endl; - old_data->clear(); - std::cout << "DEALLOCATING " << old_data << "\n"; - #endif - - // may cause recursive call - delete old_data; - - #ifdef IREP_DEBUG - std::cout << "DONE\n"; - #endif - } - #endif -} -#endif - -/*******************************************************************\ - -Function: irept::nonrecursive_destructor - - Inputs: - - Outputs: - - Purpose: Does the same as remove_ref, but - using an explicit stack instead of recursion. - -\*******************************************************************/ - -#ifdef SHARING -void irept::nonrecursive_destructor(dt *old_data) -{ - std::vector
stack(1, old_data); - - while(!stack.empty()) - { - dt *d=stack.back(); - stack.erase(--stack.end()); - if(d==&empty_d) - continue; - - assert(d->ref_count!=0); - d->ref_count--; - - if(d->ref_count==0) - { - stack.reserve(stack.size()+ - d->named_sub.size()+ - d->comments.size()+ - d->sub.size()); - - for(named_subt::iterator - it=d->named_sub.begin(); - it!=d->named_sub.end(); - it++) - { - stack.push_back(it->second.data); - it->second.data=&empty_d; - } - - for(named_subt::iterator - it=d->comments.begin(); - it!=d->comments.end(); - it++) - { - stack.push_back(it->second.data); - it->second.data=&empty_d; - } - - for(subt::iterator - it=d->sub.begin(); - it!=d->sub.end(); - it++) - { - stack.push_back(it->data); - it->data=&empty_d; - } - - // now delete, won't do recursion - delete d; - } - } -} -#endif - -/*******************************************************************\ - Function: irept::move_to_named_sub Inputs: @@ -261,9 +89,6 @@ Function: irept::move_to_named_sub void irept::move_to_named_sub(const irep_namet &name, irept &irep) { - #ifdef SHARING - detach(); - #endif add(name).swap(irep); irep.clear(); } @@ -282,9 +107,6 @@ Function: irept::move_to_sub void irept::move_to_sub(irept &irep) { - #ifdef SHARING - detach(); - #endif get_sub().push_back(get_nil_irep()); get_sub().back().swap(irep); } diff --git a/src/util/irep.h b/src/util/irep.h index af0b68ac26e..28ba21faa32 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -9,29 +9,33 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_IREP_H #define CPROVER_UTIL_IREP_H -#include -#include -#include -#include - #define USE_DSTRING #define SHARING // #define HASH_CODE -#define USE_MOVE // #define SUB_IS_LIST +#include "irep_ids.h" + +#ifdef USE_DSTRING +#include "dstring.h" +#endif + +#include +#include +#include +#include +#include + #ifdef SUB_IS_LIST #include #else #include #endif -#ifdef USE_DSTRING -#include "dstring.h" +#ifdef IREP_DEBUG +#include #endif -#include "irep_ids.h" - #ifdef USE_DSTRING typedef dstringt irep_idt; typedef dstringt irep_namet; @@ -79,10 +83,6 @@ inline const std::string &name2string(const irep_namet &n) for(irept::named_subt::iterator it=(irep).begin(); \ it!=(irep).end(); ++it) -#ifdef IREP_DEBUG -#include -#endif - class irept; const irept &get_nil_irep(); @@ -97,104 +97,24 @@ class irept // named_subt has to provide stable references; with C++11 we could // use std::forward_list or std::vector< unique_ptr > to save // memory and increase efficiency. - #ifdef SUB_IS_LIST - typedef std::list > named_subt; + typedef std::list> named_subt; #else typedef std::map named_subt; #endif - bool is_nil() const { return id()==ID_nil; } - bool is_not_nil() const { return id()!=ID_nil; } - - explicit irept(const irep_idt &_id):data(&empty_d) - { - id(_id); - } - - #ifdef SHARING - // constructor for blank irep - irept():data(&empty_d) - { - } - - // copy constructor - irept(const irept &irep):data(irep.data) - { - if(data!=&empty_d) - { - assert(data->ref_count!=0); - data->ref_count++; - #ifdef IREP_DEBUG - std::cout << "COPY " << data << " " << data->ref_count << std::endl; - #endif - } - } - - #ifdef USE_MOVE - // Copy from rvalue reference. - // Note that this does avoid a branch compared to the - // standard copy constructor above. - irept(irept &&irep):data(irep.data) - { - #ifdef IREP_DEBUG - std::cout << "COPY MOVE\n"; - #endif - irep.data=&empty_d; - } - #endif - - irept &operator=(const irept &irep) - { - #ifdef IREP_DEBUG - std::cout << "ASSIGN\n"; - #endif - - // Ordering is very important here! - // Consider self-assignment, which may destroy 'irep' - dt *irep_data=irep.data; - if(irep_data!=&empty_d) - irep_data->ref_count++; - - remove_ref(data); // this may kill 'irep' - data=irep_data; - - return *this; - } - - #ifdef USE_MOVE - // Note that the move assignment operator does avoid - // three branches compared to standard operator above. - irept &operator=(irept &&irep) - { - #ifdef IREP_DEBUG - std::cout << "ASSIGN MOVE\n"; - #endif - // we simply swap two pointers - std::swap(data, irep.data); - return *this; - } - #endif + irept()=default; - ~irept() - { - remove_ref(data); - } + explicit irept(const irep_idt &_id) { id(_id); } - #else - irept() - { - } - #endif + bool is_nil() const { return id()==ID_nil; } + bool is_not_nil() const { return id()!=ID_nil; } - const irep_idt &id() const - { return read().data; } + const irep_idt &id() const { return read().data; } - const std::string &id_string() const - { return id2string(read().data); } + const std::string &id_string() const { return id2string(read().data); } - void id(const irep_idt &_data) - { write().data=_data; } + void id(const irep_idt &_data) { write().data=_data; } const irept &find(const irep_namet &name) const; irept &add(const irep_namet &name); @@ -213,9 +133,10 @@ class irept long long get_long_long(const irep_namet &name) const; void set(const irep_namet &name, const irep_idt &value) - { add(name).id(value); } - void set(const irep_namet &name, const irept &irep) - { add(name, irep); } + { + add(name).id(value); + } + void set(const irep_namet &name, const irept &irep) { add(name, irep); } void set(const irep_namet &name, const long long value); void remove(const irep_namet &name); @@ -224,14 +145,12 @@ class irept bool operator==(const irept &other) const; - bool operator!=(const irept &other) const - { - return !(*this==other); - } + bool operator!=(const irept &other) const { return !operator==(other); } - void swap(irept &irep) + void swap(irept &irep) noexcept { - std::swap(irep.data, data); + using std::swap; + swap(data, irep.data); } bool operator<(const irept &other) const; @@ -257,28 +176,17 @@ class irept std::string pretty(unsigned indent=0, unsigned max_indent=0) const; -protected: - static bool is_comment(const irep_namet &name) - { return !name.empty() && name[0]=='#'; } - -public: +private: class dt { - private: - friend class irept; - - #ifdef SHARING - unsigned ref_count; - #endif - + public: irep_idt data; - named_subt named_sub; named_subt comments; subt sub; #ifdef HASH_CODE - mutable std::size_t hash_code; + mutable std::size_t hash_code=0; #endif void clear() @@ -295,75 +203,63 @@ class irept hash_code=0; #endif } + }; - void swap(dt &d) - { - d.data.swap(data); - d.sub.swap(sub); - d.named_sub.swap(named_sub); - d.comments.swap(comments); - #ifdef HASH_CODE - std::swap(d.hash_code, hash_code); - #endif - } +public: + // TODO This is only public so that we can use the data pointer as a hash. + // This is poor encapsulation, which might be fixed by making this method + // private and providing a dedicated `ptr_hash` method which returns a + // `std::size_t`. + const dt &read() const { return *ptr(); } +private: + dt &write() + { #ifdef SHARING - dt():ref_count(1) - #ifdef HASH_CODE - , hash_code(0) - #endif - { - } - #else - dt() - #ifdef HASH_CODE - :hash_code(0) - #endif - { - } + #ifdef IREP_DEBUG + std::cout << "DETACH1: " << data << '\n'; #endif - }; - -protected: - #ifdef SHARING - dt *data; - static dt empty_d; - static void remove_ref(dt *old_data); - static void nonrecursive_destructor(dt *old_data); - void detach(); + if(!data.unique()) + { + data=std::make_shared
(*data); + } -public: - const dt &read() const - { - return *data; - } + #ifdef IREP_DEBUG + std::cout << "ALLOCATED " << data << '\n'; + #endif - dt &write() - { - detach(); + #ifdef IREP_DEBUG + std::cout << "DETACH2: " << data << '\n'; + #endif + #endif #ifdef HASH_CODE - data->hash_code=0; + ptr()->hash_code=0; #endif - return *data; + return *ptr(); } - #else - dt data; + #ifdef SHARING + static std::shared_ptr
empty; + #endif -public: - const dt &read() const + static bool is_comment(const irep_namet &name) { - return data; + return !name.empty() && name[0]=='#'; } - dt &write() - { - #ifdef HASH_CODE - data.hash_code=0; - #endif - return data; - } + #ifdef SHARING + std::shared_ptr
data=empty; + #else + dt data; + #endif + + #ifdef SHARING + dt *ptr() { return data.get(); } + const dt *ptr() const { return data.get(); } + #else + dt *ptr() { return &data; } + const dt *ptr() const { return &data; } #endif }; diff --git a/src/util/merge_irep.h b/src/util/merge_irep.h index c656cfccca0..e4968f631b9 100644 --- a/src/util/merge_irep.h +++ b/src/util/merge_irep.h @@ -20,16 +20,19 @@ class merged_irept:public irept { // We assume that both are in the same container, // which isn't checked. - return data==other.data; + return &read()==&other.read(); } bool operator<(const merged_irept &other) const { // again, assumes that both are in the same container - return ((std::size_t)data)<((std::size_t)other.data); + return &read()<&other.read(); } - std::size_t hash() const { return (std::size_t)data; } + std::size_t hash() const + { + return reinterpret_cast(&read()); + } // copy constructor: will only copy from other merged_irepts merged_irept(const merged_irept &_src):irept(_src) From 3affd8b5b18f7707925f3e5a0ecdffc284800a69 Mon Sep 17 00:00:00 2001 From: reuk Date: Thu, 23 Mar 2017 13:48:27 +0000 Subject: [PATCH 2/2] Remove `noexcept`, fixing Windows build --- src/util/irep.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/irep.h b/src/util/irep.h index 28ba21faa32..945b7341564 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -147,7 +147,7 @@ class irept bool operator!=(const irept &other) const { return !operator==(other); } - void swap(irept &irep) noexcept + void swap(irept &irep) { using std::swap; swap(data, irep.data);