From 3d64070de5ae048487c49f25ca273b974f12cf1c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 17 Feb 2018 13:38:30 +0000 Subject: [PATCH 1/4] Partially revert "Use small intrusive pointer in irep" This partially reverts commit b741d4b1251f522df6955cf89fe90713702a30e9. While safer to use, these changes prevented sharing on irept's where non-const references had been taken to any irept stored in their sub/named_sub collections. The newly introduced cow.h and small_shared_ptr.h are kept in place, but all modifications to irept are reverted. --- src/util/fresh_symbol.cpp | 1 + src/util/irep.cpp | 145 ++++++++++++++++++++++++++- src/util/irep.h | 199 +++++++++++++++++++++++++++++--------- 3 files changed, 300 insertions(+), 45 deletions(-) diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp index c77c7e33e47..8a71b888e9a 100644 --- a/src/util/fresh_symbol.cpp +++ b/src/util/fresh_symbol.cpp @@ -11,6 +11,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "fresh_symbol.h" +#include "invariant.h" #include "namespace.h" #include "rename.h" #include "symbol.h" diff --git a/src/util/irep.cpp b/src/util/irep.cpp index d46a06e216c..af2f3f18831 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -26,6 +26,12 @@ 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, @@ -49,20 +55,157 @@ 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 2365989bfaa..209b5008b94 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -10,19 +10,17 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_IREP_H #define CPROVER_UTIL_IREP_H -#include +#include #include +#include #include "irep_ids.h" #define SHARING // #define HASH_CODE +#define USE_MOVE // #define SUB_IS_LIST -#ifdef SHARING -#include "cow.h" -#endif - #ifdef SUB_IS_LIST #include #else @@ -104,13 +102,89 @@ 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; } @@ -118,9 +192,7 @@ class irept { return id2string(read().data); } void id(const irep_idt &_data) - { - write(true).data = _data; - } + { write().data=_data; } const irept &find(const irep_namet &name) const; irept &add(const irep_namet &name); @@ -169,20 +241,11 @@ class irept void make_nil() { *this=get_nil_irep(); } - subt &get_sub() - { - return write(false).sub; - } + subt &get_sub() { return write().sub; } // DANGEROUS const subt &get_sub() const { return read().sub; } - named_subt &get_named_sub() - { - return write(false).named_sub; - } + named_subt &get_named_sub() { return write().named_sub; } // DANGEROUS const named_subt &get_named_sub() const { return read().named_sub; } - named_subt &get_comments() - { - return write(false).comments; - } + named_subt &get_comments() { return write().comments; } // DANGEROUS const named_subt &get_comments() const { return read().comments; } std::size_t hash() const; @@ -196,60 +259,108 @@ class irept static bool is_comment(const irep_namet &name) { return !name.empty() && name[0]=='#'; } -private: +public: class dt -#ifdef SHARING - : public copy_on_write_pointeet -#endif { - public: + private: + friend class irept; + + #ifdef SHARING + unsigned ref_count; + #endif + /// 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 = 0; + mutable std::size_t hash_code; #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 }; -#ifdef SHARING - copy_on_writet
data; -#else - dt data; -#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(); - dt &write(bool mark_shareable) +public: + const dt &read() const { -#ifdef SHARING - return data.write(mark_shareable); -#else - return data; -#endif + return *data; + } + + dt &write() + { + detach(); + #ifdef HASH_CODE + data->hash_code=0; + #endif + return *data; } + #else + dt data; + public: const dt &read() const { -#ifdef SHARING - return data.read(); -#else return data; -#endif } + + dt &write() + { + #ifdef HASH_CODE + data.hash_code=0; + #endif + return data; + } + #endif }; // NOLINTNEXTLINE(readability/identifiers) From d58fd18159e978f01774d0842e6434cf34137489 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 17 Feb 2018 13:42:47 +0000 Subject: [PATCH 2/4] Silence the linter on assert in irep.h Using invariant.h would drag in a number of additional headers into almost every file thus it seems preferable to maintain the assert here. --- src/util/irep.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/irep.h b/src/util/irep.h index 209b5008b94..1d0607be640 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -121,6 +121,7 @@ class irept { if(data!=&empty_d) { + // NOLINTNEXTLINE(build/deprecated) assert(data->ref_count!=0); data->ref_count++; #ifdef IREP_DEBUG From abdb0443f2cc15d69232eca3c170f5cd9bbe6d30 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Fri, 16 Feb 2018 13:43:33 +0000 Subject: [PATCH 3/4] Unit test to check that irept implements sharing Separately test irept and exprt, where the latter are expected to have the very same behaviour. --- unit/util/irep_sharing.cpp | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/unit/util/irep_sharing.cpp b/unit/util/irep_sharing.cpp index 86b3880bef3..3d79cd5590a 100644 --- a/unit/util/irep_sharing.cpp +++ b/unit/util/irep_sharing.cpp @@ -93,6 +93,16 @@ SCENARIO("irept_sharing", "[core][utils][irept]") REQUIRE(&irep.read() != &test_irep.read()); REQUIRE(irep.id() != test_irep.id()); } + // the following would be desirable for irept to be safe, but we know it + // presently does not hold; see #1855 for a proposed solution + // THEN("Holding a reference to an operand should prevent sharing") + // { + // irept &operand = test_irep.get_sub()[0]; + // irept irep = test_irep; + // REQUIRE(&irep.read() != &test_irep.read()); + // operand = irept(ID_0); + // REQUIRE(irep.get_sub()[0].id() != test_irep.get_sub()[0].id()); + // } THEN("Changing an id should not prevent sharing") { test_irep.id(ID_0); @@ -190,6 +200,16 @@ SCENARIO("exprt_sharing", "[core][utils][exprt]") REQUIRE(&expr.read() != &test_expr.read()); REQUIRE(expr.id() != test_expr.id()); } + // the following would be desirable for irept to be safe, but we know it + // presently does not hold; see #1855 for a proposed solution + // THEN("Holding a reference to an operand should prevent sharing") + // { + // exprt &operand = test_expr.op0(); + // exprt expr = test_expr; + // REQUIRE(&expr.read() != &test_expr.read()); + // operand = exprt(ID_0); + // REQUIRE(expr.op0().id() != test_expr.op0().id()); + // } THEN("Changing an id should not prevent sharing") { test_expr.id(ID_0); From cbce4bc11741b4310a16b2ef3547ea6885da591a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 22 Mar 2018 18:45:32 +0000 Subject: [PATCH 4/4] Unit test of irept's public API --- unit/util/irep.cpp | 53 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp index c33ec3c181c..d532bccc12b 100644 --- a/unit/util/irep.cpp +++ b/unit/util/irep.cpp @@ -14,6 +14,57 @@ SCENARIO("irept_memory", "[core][utils][irept]") REQUIRE(sizeof(irept) == sizeof(void *)); } + THEN("The storage size of an irept is fixed") + { +#ifdef SHARING + const std::size_t ref_count_size = sizeof(unsigned); +#else + const std::size_t ref_count_size = 0; +#endif + +#ifndef USE_STRING + const std::size_t data_size = sizeof(dstringt); + REQUIRE(sizeof(dstringt) == sizeof(unsigned)); +#else + const std::size_t data_size = sizeof(std::string); + REQUIRE(sizeof(std::string) == sizeof(void *)); +#endif + + const std::size_t sub_size = sizeof(std::vector); +#ifndef _GLIBCXX_DEBUG + REQUIRE(sizeof(std::vector) == 3 * sizeof(void *)); +#endif + +#ifndef SUB_IS_LIST + const std::size_t named_size = sizeof(std::map); +# ifndef _GLIBCXX_DEBUG +# ifdef __APPLE__ + REQUIRE(sizeof(std::map) == 3 * sizeof(void *)); +# elif defined(_WIN32) + REQUIRE(sizeof(std::map) == 2 * sizeof(void *)); +# else + REQUIRE(sizeof(std::map) == 6 * sizeof(void *)); +# endif +# endif +#else + const std::size_t named_size = sizeof(std::list); +# ifndef _GLIBCXX_DEBUG + REQUIRE(sizeof(std::list) == 3 * sizeof(void *)); +# endif +#endif + +#ifdef HASH_CODE + const std::size_t hash_code_size = sizeof(std::size_t); +#else + const std::size_t hash_code_size = 0; +#endif + + REQUIRE( + sizeof(irept::dt) == + ref_count_size + data_size + sub_size + 2 * named_size + + hash_code_size); + } + THEN("get_nil_irep yields ID_nil") { REQUIRE(get_nil_irep().id() == ID_nil); @@ -88,7 +139,7 @@ SCENARIO("irept_memory", "[core][utils][irept]") REQUIRE(irep.find("a_new_element").id() == "some_id"); irept irep2("second_irep"); - irep.add("a_new_element", irep2); + irept &e2 = irep.add("a_new_element", irep2); REQUIRE(irep.find("a_new_element").id() == "second_irep"); REQUIRE(irep.get_named_sub().size() == 1);