diff --git a/src/util/cow.h b/src/util/cow.h new file mode 100644 index 00000000000..2d4261d4d0e --- /dev/null +++ b/src/util/cow.h @@ -0,0 +1,86 @@ +#pragma once + +template class cow final { +public: + cow() = default; + + template + explicit cow(Ts &&... ts) : t_(new T(std::forward(ts)...)) { + t_->increment_use_count(); + } + + cow(const cow &rhs) { + if (!rhs.t_->is_unshareable()) { + t_ = rhs.t_; + t_->increment_use_count(); + } else { + t_ = new T(*t_); + } + } + + cow &operator=(const cow &rhs) { + auto copy(rhs); + swap(copy); + return *this; + } + + cow(cow &&rhs) { swap(rhs); } + + cow &operator=(cow &&rhs) { + swap(rhs); + return *this; + } + + ~cow() { + if (t_->is_unshareable()) { + delete t_; + } else { + t_->decrement_use_count(); + if (t_->get_use_count() == 0) { + delete t_; + } + } + } + + void swap(cow &rhs) { + using std::swap; + swap(t_, rhs.t_); + } + + const T &operator*() const { return *t_; } + + T &write(bool mark_unshareable) { + if (!t_->is_unshareable() && t_->get_use_count() != 1) { + + } else { + + } + } + +private: + T *t_ = nullptr; +}; + +class cow_base { +public: + cow_base() = default; + cow_base(const cow_base &) {} + cow_base &operator=(const cow_base &) {} + cow_base(cow_base &&) {} + cow_base &operator=(cow_base &&) {} + + void increment_use_count() { use_count_ += 1; } + void decrement_use_count() { use_count_ -= 1; } + std::size_t get_use_count() const { return use_count_; } + + void set_unshareable(bool u) { use_count_ = u ? unshareable : 1; } + bool is_unshareable() { return use_count_ == unshareable; } + +protected: + ~cow_base() = default; + +private: + static const std::size_t unshareable = + std::numeric_limits::max(); + std::size_t use_count_ = 0; +}; diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 886f8ce9d7b..d3028cbee77 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -22,12 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif -irept nil_rep_storage; - -#ifdef SHARING -irept::dt irept::empty_d; -#endif - /*******************************************************************\ Function: named_subt_lower_bound @@ -75,177 +69,13 @@ 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; -} - -/*******************************************************************\ - -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; - } + nil_rep_storage.id(ID_nil); } + return nil_rep_storage; } -#endif /*******************************************************************\ @@ -261,9 +91,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 +109,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 938462868b6..c7cfc8c4255 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -18,9 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com #define SHARING // #define HASH_CODE -#define USE_MOVE // #define SUB_IS_LIST +#ifdef SHARING +#include "small_shared_ptr.h" +#endif + #ifdef SUB_IS_LIST #include #else @@ -102,85 +105,12 @@ class irept 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()=default; - 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() - { - remove_ref(data); - } - - #else - irept() + explicit irept(const irep_idt &_id) { + id(_id); } - #endif const irep_idt &id() const { return read().data; } @@ -256,106 +186,68 @@ class irept static bool is_comment(const irep_namet &name) { return !name.empty() && name[0]=='#'; } -public: +private: class dt + #ifdef SHARING + :public small_pointeet + #endif { - 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() { data.clear(); - sub.clear(); named_sub.clear(); comments.clear(); + sub.clear(); #ifdef HASH_CODE 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 - } - - #ifdef SHARING - dt():ref_count(1) - #ifdef HASH_CODE - , hash_code(0) - #endif - { - } - #else - dt() - #ifdef HASH_CODE - :hash_code(0) - #endif - { - } - #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(); +#ifdef SHARING + small_shared_ptrt
data=make_small_shared_ptr
(); +#else + dt data; +#endif public: const dt &read() const { + #ifdef SHARING + assert(data); return *data; + #else + return data; + #endif } +private: dt &write() { - detach(); + #ifdef SHARING + assert(data); + if(data.use_count()!=1) + { + data=make_small_shared_ptr
(*data); + } #ifdef HASH_CODE data->hash_code=0; #endif return *data; - } - - #else - dt data; - -public: - const dt &read() const - { + #else return data; - } - - dt &write() - { - #ifdef HASH_CODE - data.hash_code=0; #endif - return data; } - #endif }; // NOLINTNEXTLINE(readability/identifiers) diff --git a/src/util/merge_irep.h b/src/util/merge_irep.h index c656cfccca0..5daddbcd544 100644 --- a/src/util/merge_irep.h +++ b/src/util/merge_irep.h @@ -20,16 +20,16 @@ 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) diff --git a/src/util/small_shared_ptr.h b/src/util/small_shared_ptr.h new file mode 100644 index 00000000000..e03942a063e --- /dev/null +++ b/src/util/small_shared_ptr.h @@ -0,0 +1,208 @@ +/*******************************************************************\ + +Module: Small intrusive shared pointers + +Author: Reuben Thomas, reuben.thomas@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_SMALL_SHARED_PTR_H +#define CPROVER_UTIL_SMALL_SHARED_PTR_H + +#include // ostream +#include // swap + +// TODO We should liberally scatter `constexpr`s and `noexcept`s on platforms +// that support them. + +// This class is really similar to boost's intrusive_pointer, but can be a bit +// simpler seeing as we're only using it one place... + +template +class small_shared_ptrt final +{ +public: + small_shared_ptrt()=default; + + explicit small_shared_ptrt(T *t):t_(t) + { + if(t_) + { + pointee_increment_use_count(*t_); + } + } + + small_shared_ptrt(const small_shared_ptrt &rhs):t_(rhs.t_) + { + if(t_) + { + pointee_increment_use_count(*t_); + } + } + + small_shared_ptrt &operator=(const small_shared_ptrt &rhs) + { + auto copy(rhs); + swap(copy); + return *this; + } + + small_shared_ptrt(small_shared_ptrt &&rhs) + { + swap(rhs); + } + + small_shared_ptrt &operator=(small_shared_ptrt &&rhs) + { + swap(rhs); + return *this; + } + + ~small_shared_ptrt() + { + if(!t_) + { + return; + } + pointee_decrement_use_count(*t_); + if(pointee_use_count(*t_)==0) + { + delete t_; + } + } + + void swap(small_shared_ptrt &rhs) + { + std::swap(t_, rhs.t_); + } + + T *get() const + { + return t_; + } + + T &operator*() const + { + return *t_; + } + + T *operator->() const + { + return t_; + } + + unsigned use_count() const + { + return t_?pointee_use_count(*t_):0; + } + + explicit operator bool() const + { + return t_!=nullptr; + } + +private: + T *t_=nullptr; +}; + +template +std::ostream &operator<<(std::ostream &os, const small_shared_ptrt &ptr) +{ + return os << ptr.get(); +} + +template +small_shared_ptrt make_small_shared_ptr(Ts &&... ts) +{ + return small_shared_ptrt(new T(std::forward(ts)...)); +} + +template +bool operator==( + const small_shared_ptrt &lhs, + const small_shared_ptrt &rhs) +{ + return lhs.get()==rhs.get(); +} + +template +bool operator!=( + const small_shared_ptrt &lhs, + const small_shared_ptrt &rhs) +{ + return lhs.get()!=rhs.get(); +} + +template +bool operator<( + const small_shared_ptrt &lhs, + const small_shared_ptrt &rhs) +{ + return lhs.get() +bool operator>( + const small_shared_ptrt &lhs, + const small_shared_ptrt &rhs) +{ + return lhs.get()>rhs.get(); +} + +template +bool operator<=( + const small_shared_ptrt &lhs, + const small_shared_ptrt &rhs) +{ + return lhs.get()<=rhs.get(); +} + +template +bool operator>=( + const small_shared_ptrt &lhs, + const small_shared_ptrt &rhs) +{ + return lhs.get()>=rhs.get(); +} + +//////////////////////////////////////////////////////////////////////////////// + +class small_pointeet +{ +public: + small_pointeet()=default; + + // These can't be `= default` because we need the use_count_ to be unaffected + small_pointeet(const small_pointeet &rhs) {} + small_pointeet &operator=(const small_pointeet &rhs) { return *this; } + small_pointeet(small_pointeet &&rhs) {} + small_pointeet &operator=(small_pointeet &&rhs) { return *this; } + + void increment_use_count() { use_count_+=1; } + void decrement_use_count() { use_count_-=1; } + unsigned use_count() const { return use_count_; } + +protected: + // Enables public inheritance but disables polymorphic usage + ~small_pointeet()=default; + +private: + unsigned use_count_=0; +}; + +inline void pointee_increment_use_count(small_pointeet &p) +{ + p.increment_use_count(); +} + +inline void pointee_decrement_use_count(small_pointeet &p) +{ + p.decrement_use_count(); +} + +inline unsigned pointee_use_count(const small_pointeet &p) +{ + return p.use_count(); +} + +#endif