From: Tim King Date: Wed, 15 Aug 2018 22:49:15 +0000 (-0700) Subject: Removing attribute cleanups. (#2300) X-Git-Tag: cvc5-1.0.0~4779 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bca6b323721b24805c375f682e05d5463c38a8d2;p=cvc5.git Removing attribute cleanups. (#2300) * Removing attribute cleanups. --- diff --git a/src/expr/attribute.h b/src/expr/attribute.h index aafe168ea..db6fb52a0 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -423,66 +423,23 @@ AttributeManager::setAttribute(NodeValue* nv, ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value); } -/** - * Search for the NodeValue in all attribute tables and remove it, - * calling the cleanup function if one is defined. - * - * This cannot use nv as anything other than a pointer! - */ +/** Search for the NodeValue in all attribute tables and remove it. */ template inline void AttributeManager::deleteFromTable(AttrHash& table, NodeValue* nv) { - for(uint64_t id = 0; id < attr::LastAttributeId::getId(); ++id) { - typedef AttributeTraits traits_t; - typedef AttrHash hash_t; - std::pair pr = std::make_pair(id, nv); - if(traits_t::getCleanup()[id] != NULL) { - typename hash_t::iterator i = table.find(pr); - if(i != table.end()) { - traits_t::getCleanup()[id]((*i).second); - table.erase(pr); - } - } else { - table.erase(pr); - } + // This cannot use nv as anything other than a pointer! + const uint64_t last = attr::LastAttributeId::getId(); + for (uint64_t id = 0; id < last; ++id) + { + table.erase(std::make_pair(id, nv)); } } -/** - * Remove all attributes from the table calling the cleanup function - * if one is defined. - */ +/** Remove all attributes from the table. */ template inline void AttributeManager::deleteAllFromTable(AttrHash& table) { Assert(!d_inGarbageCollection); d_inGarbageCollection = true; - - bool anyRequireClearing = false; - typedef AttributeTraits traits_t; - typedef AttrHash hash_t; - for(uint64_t id = 0; id < attr::LastAttributeId::getId(); ++id) { - if(traits_t::getCleanup()[id] != NULL) { - anyRequireClearing = true; - } - } - - if(anyRequireClearing) { - typename hash_t::iterator it = table.begin(); - typename hash_t::iterator it_end = table.end(); - - while (it != it_end){ - uint64_t id = (*it).first.first; - /* - Debug("attrgc") << "id " << id - << " node_value: " << ((*it).first.second) - << std::endl; - */ - if(traits_t::getCleanup()[id] != NULL) { - traits_t::getCleanup()[id]((*it).second); - } - ++it; - } - } table.clear(); d_inGarbageCollection = false; Assert(!d_inGarbageCollection); @@ -499,7 +456,6 @@ AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){ template void AttributeManager::deleteAttributesFromTable(AttrHash& table, const std::vector& ids){ d_inGarbageCollection = true; - typedef AttributeTraits traits_t; typedef AttrHash hash_t; typename hash_t::iterator it = table.begin(); @@ -516,9 +472,6 @@ void AttributeManager::deleteAttributesFromTable(AttrHash& table, const std:: if(std::binary_search(begin_ids, end_ids, id)){ tmp = it; ++it; - if(traits_t::getCleanup()[id] != NULL) { - traits_t::getCleanup()[id]((*tmp).second); - } table.erase(tmp); }else{ ++it; diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index ed1769740..e474c3dfb 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -332,45 +332,6 @@ public: }/* CVC4::expr::attr namespace */ -// ATTRIBUTE CLEANUP FUNCTIONS ================================================= - -namespace attr { - -/** Default cleanup for unmanaged Attribute<> */ -struct NullCleanupStrategy { -};/* struct NullCleanupStrategy */ - -/** - * Helper for Attribute<> class below to determine whether a cleanup - * is defined or not. - */ -template -struct getCleanupStrategy { - typedef T value_type; - typedef KindValueToTableValueMapping mapping; - static void fn(typename mapping::table_value_type t) { - C::cleanup(mapping::convertBack(t)); - } -};/* struct getCleanupStrategy<> */ - -/** - * Specialization for NullCleanupStrategy. - */ -template -struct getCleanupStrategy { - typedef T value_type; - typedef KindValueToTableValueMapping mapping; - static void (*const fn)(typename mapping::table_value_type); -};/* struct getCleanupStrategy */ - -// out-of-class initialization required (because it's a non-integral type) -template -void (*const getCleanupStrategy::fn) - (typename getCleanupStrategy:: - mapping::table_value_type) = NULL; - -}/* CVC4::expr::attr namespace */ - // ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ==================================== namespace attr { @@ -381,39 +342,21 @@ namespace attr { */ template struct LastAttributeId { - static uint64_t& getId() { - static uint64_t s_id = 0; - return s_id; + public: + static uint64_t getNextId() { + uint64_t* id = raw_id(); + const uint64_t next_id = *id; + ++(*id); + return next_id; } -}; - -}/* CVC4::expr::attr namespace */ - -// ATTRIBUTE TRAITS ============================================================ - -namespace attr { - -/** - * This is the last-attribute-assigner. IDs are not globally - * unique; rather, they are unique for each table_value_type. - */ -template -struct AttributeTraits { - typedef void (*cleanup_t)(T); - static std::vector& getCleanup() { - // Note: we do not destroy this vector on purpose. Instead, we rely on the - // OS to clean up our mess. The reason for that is that we need this vector - // to remain initialized at least as long as the ExprManager because - // ExprManager's destructor calls this method. The only way to guarantee - // this is to never destroy it. This is a common idiom [0]. In the past, we - // had an issue when `cleanup` wasn't a pointer and just an `std::vector` - // instead. CxxTest stores the test class in a static variable, which could - // lead to the ExprManager being destroyed after the destructor of the - // vector was called. - // - // [0] https://isocpp.org/wiki/faq/ctors#static-init-order-on-first-use - static std::vector* cleanup = new std::vector(); - return *cleanup; + static uint64_t getId() { + return *raw_id(); + } + private: + static uint64_t* raw_id() + { + static uint64_t s_id = 0; + return &s_id; } }; @@ -428,18 +371,12 @@ struct AttributeTraits { * * @param value_t the underlying value_type for the attribute kind * - * @param CleanupStrategy Clean-up routine for associated values when the - * Node goes away. Useful, e.g., for pointer-valued attributes when - * the values are "owned" by the table. - * * @param context_dep whether this attribute kind is * context-dependent */ -template -class Attribute { +template +class Attribute +{ /** * The unique ID associated to this attribute. Assigned statically, * at load time. @@ -475,33 +412,16 @@ public: static inline uint64_t registerAttribute() { typedef typename attr::KindValueToTableValueMapping:: table_value_type table_value_type; - typedef attr::AttributeTraits traits; - uint64_t id = attr::LastAttributeId::getId()++; - Assert(traits::getCleanup().size() == id);// sanity check - traits::getCleanup().push_back(attr::getCleanupStrategy::fn); - return id; + return attr::LastAttributeId::getNextId(); } };/* class Attribute<> */ -/** - * An "attribute type" structure for boolean flags (special). The - * full one is below; the existence of this one disallows for boolean - * flag attributes with a specialized cleanup function. - */ -/* -- doesn't work; other specialization is "more specific" ?? -template -class Attribute { - template struct ERROR_bool_attributes_cannot_have_cleanup_functions; - ERROR_bool_attributes_cannot_have_cleanup_functions blah; -}; -*/ - /** * An "attribute type" structure for boolean flags (special). */ template -class Attribute { +class Attribute +{ /** IDs for bool-valued attributes are actually bit assignments. */ static const uint64_t s_id; @@ -538,7 +458,7 @@ public: * return the id. */ static inline uint64_t registerAttribute() { - uint64_t id = attr::LastAttributeId::getId()++; + const uint64_t id = attr::LastAttributeId::getNextId(); AlwaysAssert( id <= 63, "Too many boolean node attributes registered " "during initialization !" ); @@ -549,25 +469,15 @@ public: // ATTRIBUTE IDENTIFIER ASSIGNMENT ============================================= /** Assign unique IDs to attributes at load time. */ -// Use of the comma-operator here forces instantiation (and -// initialization) of the AttributeTraits<> structure and its -// "cleanup" vector before registerAttribute() is called. This is -// important because otherwise the vector is initialized later, -// clearing the first-pushed cleanup function. -template -const uint64_t Attribute::s_id = - ( attr::AttributeTraits:: - table_value_type, - context_dep>::getCleanup().size(), - Attribute::registerAttribute() ); +template +const uint64_t Attribute::s_id = + Attribute::registerAttribute(); + /** Assign unique IDs to attributes at load time. */ template -const uint64_t Attribute::s_id = - Attribute:: - registerAttribute(); +const uint64_t Attribute::s_id = + Attribute::registerAttribute(); }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 8bbf905a9..7d1259fcc 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -128,10 +128,7 @@ class NodeManager { * contexts, like as a key in attribute tables), even though * normally it's an error to have a TNode to a node value with a * reference count of 0. Being "under deletion" also enables - * assertions that inc() is not called on it. (A poorly-behaving - * attribute cleanup function could otherwise create a "Node" that - * points to the node value that is in the process of being deleted, - * springing it back to life.) + * assertions that inc() is not called on it. */ expr::NodeValue* d_nodeUnderDeletion;