diff --git a/src/util/cow.h b/src/util/cow.h new file mode 100644 index 00000000000..1db6469bbca --- /dev/null +++ b/src/util/cow.h @@ -0,0 +1,254 @@ +/*******************************************************************\ + +Module: Copy on write class + +Author: Reuben Thomas, reuben.thomas@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_COW_H +#define CPROVER_UTIL_COW_H + +#include "invariant.h" +#include "small_shared_ptr.h" + +#include + +/// A utility class for writing types with copy-on-write behaviour (like irep). +/// This is a thin wrapper over a shared pointer, but instead of a single +/// getter for the pointer value, we supply a separate 'read' and 'write' +/// method. 'read' returns a reference to the owned object, while 'write' +/// will create a copy of the owned object if more than one copy_on_write +/// instance points to it. +template +class copy_on_writet final +{ +public: + // Note that this *is* the default constructor. An invariant of a + // copy-on-write object is that it is never null. + template + explicit copy_on_writet(Ts &&... ts) + : t_(make_small_shared_ptr(std::forward(ts)...)) + { + INVARIANT( + pointee_is_shareable(*t_), + "newly-constructed COW pointers must be shareable"); + } + + copy_on_writet(const copy_on_writet &rhs) + : t_( + pointee_is_shareable(*rhs.t_) ? rhs.t_ + : make_small_shared_ptr(*rhs.t_)) + { + INVARIANT( + pointee_is_shareable(*t_), + "newly-constructed COW pointers must be shareable"); + } + + copy_on_writet &operator=(const copy_on_writet &rhs) + { + auto copy(rhs); + swap(copy); + return *this; + } + + copy_on_writet(copy_on_writet &&rhs) + { + swap(rhs); + } + + copy_on_writet &operator=(copy_on_writet &&rhs) + { + swap(rhs); + return *this; + } + + void swap(copy_on_writet &rhs) + { + std::swap(t_, rhs.t_); + } + + const T &read() const + { + return *t_; + } + + T &write(bool mark_shareable) + { + if(pointee_use_count(*t_) != 1) + { + t_ = make_small_shared_ptr(*t_); + } + INVARIANT( + pointee_use_count(*t_) == 1, + "mutable references to a COW pointer must be unique"); + pointee_set_shareable(*t_, mark_shareable); + return *t_; + } + + // Ideally these would be non-members, but they depend on private member t_ + + template + bool operator==(const copy_on_writet &rhs) const + { + return t_ == rhs.t_; + } + + template + bool operator!=(const copy_on_writet &rhs) const + { + return t_ != rhs.t_; + } + + template + bool operator<(const copy_on_writet &rhs) const + { + return t_ < rhs.t_; + } + + template + bool operator>(const copy_on_writet &rhs) const + { + return t_ > rhs.t_; + } + + template + bool operator<=(const copy_on_writet &rhs) const + { + return t_ <= rhs.t_; + } + + template + bool operator>=(const copy_on_writet &rhs) const + { + return t_ >= rhs.t_; + } + +private: + small_shared_ptrt t_; +}; + +//////////////////////////////////////////////////////////////////////////////// + +/// A helper class to store use-counts of copy-on-write objects. +/// The suggested usage pattern is to have copy-on-write data types inherit +/// from this class, and then to access them through a copy_on_writet. +/// \tparam Num some numeric type, used to store a reference count +template +class copy_on_write_pointeet +{ +public: + copy_on_write_pointeet() = default; + + copy_on_write_pointeet(const copy_on_write_pointeet &) + { + } + + copy_on_write_pointeet &operator=(const copy_on_write_pointeet &) + { + return *this; + } + + copy_on_write_pointeet(copy_on_write_pointeet &&) + { + } + + copy_on_write_pointeet &operator=(copy_on_write_pointeet &&) + { + return *this; + } + + void increment_use_count() + { + INVARIANT( + is_shareable(), + "cannot increment the use count of a non-shareable reference"); + ++use_count_; + } + + void decrement_use_count() + { + INVARIANT( + is_shareable(), + "cannot decrement the use count of a non-shareable reference"); + --use_count_; + } + + Num use_count() const + { + return is_shareable() ? use_count_ : 1; + } + + void set_shareable(bool u) + { + use_count_ = u ? 1 : unshareable; + } + + bool is_shareable() const + { + return use_count_ != unshareable; + } + +protected: + ~copy_on_write_pointeet() = default; + +private: + /// A special sentry value which will be assigned to use_count_ if + /// a mutable reference to the held object has been created. We check for + /// this sentry value, and use it to decide whether the next copy + /// constructor/assignment call should invoke a deep or shallow copy. + /// Note that this is set to the max value that can be held by Num, but + /// this cannot be done inline. + static const Num unshareable; + Num use_count_ = 0; +}; + +template +const Num copy_on_write_pointeet::unshareable = + (std::numeric_limits::max)(); // suppress macro expansion on windows + +/// The following functions are required by copy_on_writet, and by default pass +/// through to the member functions of copy_on_write_pointeet by the same name. +/// We provide these as non-members just in case a future client wants to +/// implement a copy-on-write class, which is unable to inherit from +/// copy_on_write_pointeet for some reason. In this case, new overloads for +/// the functions below can be provided, with appropriate behavior for the new +/// type. + +template +inline void pointee_increment_use_count(copy_on_write_pointeet &p) +{ + p.increment_use_count(); +} + +template +inline void pointee_decrement_use_count(copy_on_write_pointeet &p) +{ + p.decrement_use_count(); +} + +template +inline Num pointee_use_count(const copy_on_write_pointeet &p) +{ + return p.use_count(); +} + +template +inline void pointee_set_use_count(copy_on_write_pointeet &p, T count) +{ + p.set_use_count(count); +} + +template +inline void pointee_set_shareable(copy_on_write_pointeet &p, bool u) +{ + p.set_shareable(u); +} + +template +inline bool pointee_is_shareable(const copy_on_write_pointeet &p) +{ + return p.is_shareable(); +} + +#endif diff --git a/src/util/irep.cpp b/src/util/irep.cpp index af2f3f18831..d46a06e216c 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -26,12 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif -irept nil_rep_storage; - -#ifdef SHARING -irept::dt irept::empty_d; -#endif - #ifdef SUB_IS_LIST static inline bool named_subt_order( const std::pair &a, @@ -55,157 +49,20 @@ static inline irept::named_subt::iterator named_subt_lower_bound( 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; } -#ifdef SHARING -void irept::detach() -{ - #ifdef IREP_DEBUG - std::cout << "DETACH1: " << data << '\n'; - #endif - - if(data==&empty_d) - { - data=new dt; - - #ifdef IREP_DEBUG - std::cout << "ALLOCATED " << data << '\n'; - #endif - } - else if(data->ref_count>1) - { - dt *old_data(data); - data=new dt(*old_data); - - #ifdef IREP_DEBUG - std::cout << "ALLOCATED " << data << '\n'; - #endif - - data->ref_count=1; - remove_ref(old_data); - } - - POSTCONDITION(data->ref_count==1); - - #ifdef IREP_DEBUG - std::cout << "DETACH2: " << data << '\n'; - #endif -} -#endif - -#ifdef SHARING -void irept::remove_ref(dt *old_data) -{ - if(old_data==&empty_d) - return; - - #if 0 - nonrecursive_destructor(old_data); - #else - - PRECONDITION(old_data->ref_count!=0); - - #ifdef IREP_DEBUG - std::cout << "R: " << old_data << " " << old_data->ref_count << '\n'; - #endif - - old_data->ref_count--; - if(old_data->ref_count==0) - { - #ifdef IREP_DEBUG - std::cout << "D: " << pretty() << '\n'; - std::cout << "DELETING " << old_data->data - << " " << old_data << '\n'; - 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 - -/// 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; - - INVARIANT(d->ref_count!=0, "All contents of the stack must be in use"); - 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 - void irept::move_to_named_sub(const irep_namet &name, irept &irep) { - #ifdef SHARING - detach(); - #endif add(name).swap(irep); irep.clear(); } 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 f0f42abda20..fbaf0ad5a94 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -19,9 +19,12 @@ Author: Daniel Kroening, kroening@kroening.com #define SHARING // #define HASH_CODE -#define USE_MOVE // #define SUB_IS_LIST +#ifdef SHARING +#include "cow.h" +#endif + #ifdef SUB_IS_LIST #include #else @@ -103,89 +106,13 @@ class irept bool is_nil() const { return id()==ID_nil; } bool is_not_nil() const { return id()!=ID_nil; } + irept() = default; + explicit irept(const irep_idt &_id) -#ifdef SHARING - :data(&empty_d) -#endif { 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 << '\n'; - #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() - { - remove_ref(data); - } - - #else - irept() - { - } - #endif - const irep_idt &id() const { return read().data; } @@ -193,7 +120,9 @@ class irept { return id2string(read().data); } void id(const irep_idt &_data) - { write().data=_data; } + { + write(true).data = _data; + } const irept &find(const irep_namet &name) const; irept &add(const irep_namet &name); @@ -242,11 +171,20 @@ class irept void make_nil() { *this=get_nil_irep(); } - subt &get_sub() { return write().sub; } // DANGEROUS + subt &get_sub() + { + return write(false).sub; + } const subt &get_sub() const { return read().sub; } - named_subt &get_named_sub() { return write().named_sub; } // DANGEROUS + named_subt &get_named_sub() + { + return write(false).named_sub; + } const named_subt &get_named_sub() const { return read().named_sub; } - named_subt &get_comments() { return write().comments; } // DANGEROUS + named_subt &get_comments() + { + return write(false).comments; + } const named_subt &get_comments() const { return read().comments; } std::size_t hash() const; @@ -260,106 +198,60 @@ class irept static bool is_comment(const irep_namet &name) { return !name.empty() && name[0]=='#'; } -public: +private: class dt +#ifdef SHARING + : public copy_on_write_pointeet +#endif { - private: - friend class irept; - - #ifdef SHARING - unsigned ref_count; - #endif - + public: + /// This irep_idt is the only place to store data in an irep, other than + /// the mere nesting structure 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(); - -public: - const dt &read() const - { - return *data; - } - - dt &write() - { - detach(); - #ifdef HASH_CODE - data->hash_code=0; - #endif - return *data; - } - - #else +#ifdef SHARING + copy_on_writet
data; +#else dt data; +#endif -public: - const dt &read() const + dt &write(bool mark_shareable) { +#ifdef SHARING + return data.write(mark_shareable); +#else return data; +#endif } - dt &write() +public: + const dt &read() const { - #ifdef HASH_CODE - data.hash_code=0; - #endif +#ifdef SHARING + return data.read(); +#else return data; +#endif } - #endif }; // NOLINTNEXTLINE(readability/identifiers) diff --git a/src/util/small_shared_ptr.h b/src/util/small_shared_ptr.h new file mode 100644 index 00000000000..4ae45fe37cc --- /dev/null +++ b/src/util/small_shared_ptr.h @@ -0,0 +1,250 @@ +/*******************************************************************\ + +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. +/// The idea is that the pointed-to object stores its reference-count +/// internally, which is more space-efficient than storing it in a separate +/// control block (which is what shared_ptr does). +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; + } + if(pointee_use_count(*t_) == 1) + { + delete t_; + return; + } + pointee_decrement_use_count(*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_; + } + + auto use_count() const -> decltype(pointee_use_count(std::declval())) + { + 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(); +} + +/// This function is similar to std::make_unique and std::make_shared, and +/// should be the preferred way of creating small_shared_ptrs. +/// The public constructors of small_shared_ptr are just provided to keep the +/// class design similar to that of unique_ptr and shared_ptr, but in +/// practice they should not be used directly. +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() < 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(); +} + +template +bool operator>=( + const small_shared_ptrt &lhs, + const small_shared_ptrt &rhs) +{ + return lhs.get() >= rhs.get(); +} + +//////////////////////////////////////////////////////////////////////////////// + +/// A helper class to store use-counts of objects held by small shared pointers. +/// The suggested usage pattern is to have such objects inherit +/// from this class, and then to access them through a small_shared_ptrt. +/// This approach provides us with shared_ptr-like semantics, but without the +/// space overhead required by shared_ptr. The idea is similar to +/// boost's intrusive_ptr. +/// \tparam Num some numeric type, used to store a reference count +template +class small_shared_pointeet +{ +public: + small_shared_pointeet() = default; + + // These can't be `= default` because we need the use_count_ to be unaffected + small_shared_pointeet(const small_shared_pointeet &rhs) + { + } + small_shared_pointeet &operator=(const small_shared_pointeet &rhs) + { + return *this; + } + small_shared_pointeet(small_shared_pointeet &&rhs) + { + } + small_shared_pointeet &operator=(small_shared_pointeet &&rhs) + { + return *this; + } + + void increment_use_count() + { + ++use_count_; + } + void decrement_use_count() + { + --use_count_; + } + Num use_count() const + { + return use_count_; + } + +protected: + // Enables public inheritance but disables polymorphic usage + ~small_shared_pointeet() = default; + +private: + Num use_count_ = 0; +}; + +/// The following functions are required by small_shared_ptrt, and by +/// default pass through to the member functions of small_shared_pointeet by the +/// same name. We provide these as non-members just in case a future client +/// wants to implement a shared object, which is unable to inherit from +/// small_shared_pointeet for some reason. In this case, new overloads for +/// the functions below can be provided, with appropriate behavior for the +/// new type. + +template +inline void pointee_increment_use_count(small_shared_pointeet &p) +{ + p.increment_use_count(); +} + +template +inline void pointee_decrement_use_count(small_shared_pointeet &p) +{ + p.decrement_use_count(); +} + +template +inline Num pointee_use_count(const small_shared_pointeet &p) +{ + return p.use_count(); +} + +#endif