From d813626606c5eca8179eec492090b85dbd818867 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 4 Jun 2013 09:10:55 -0400 Subject: [PATCH] Fix clang static initialization order issue; fixes bug 512. --- src/expr/attribute.h | 16 ++-- src/expr/attribute_internals.h | 28 +++--- src/theory/type_enumerator.h | 3 + test/regress/regress0/Makefile.am | 1 + test/regress/regress0/bug512.smt2 | 147 ++++++++++++++++++++++++++++++ test/unit/expr/attribute_white.h | 12 +-- 6 files changed, 178 insertions(+), 29 deletions(-) create mode 100644 test/regress/regress0/bug512.smt2 diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 70f04be85..969843ddd 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -522,14 +522,14 @@ AttributeManager::setAttribute(NodeValue* nv, template inline void AttributeManager::deleteFromTable(AttrHash& table, NodeValue* nv) { - for(uint64_t id = 0; id < attr::LastAttributeId::s_id; ++id) { + 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::cleanup[id] != NULL) { + if(traits_t::getCleanup()[id] != NULL) { typename hash_t::iterator i = table.find(pr); if(i != table.end()) { - traits_t::cleanup[id]((*i).second); + traits_t::getCleanup()[id]((*i).second); table.erase(pr); } } else { @@ -544,7 +544,7 @@ inline void AttributeManager::deleteFromTable(AttrHash& table, template inline void AttributeManager::deleteFromTable(CDAttrHash& table, NodeValue* nv) { - for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { + for(unsigned id = 0; id < attr::LastAttributeId::getId(); ++id) { table.obliterate(std::make_pair(id, nv)); } } @@ -558,8 +558,8 @@ inline void AttributeManager::deleteAllFromTable(AttrHash& table) { bool anyRequireClearing = false; typedef AttributeTraits traits_t; typedef AttrHash hash_t; - for(uint64_t id = 0; id < attr::LastAttributeId::s_id; ++id) { - if(traits_t::cleanup[id] != NULL) { + for(uint64_t id = 0; id < attr::LastAttributeId::getId(); ++id) { + if(traits_t::getCleanup()[id] != NULL) { anyRequireClearing = true; } } @@ -575,8 +575,8 @@ inline void AttributeManager::deleteAllFromTable(AttrHash& table) { << " node_value: " << ((*it).first.second) << std::endl; */ - if(traits_t::cleanup[id] != NULL) { - traits_t::cleanup[id]((*it).second); + if(traits_t::getCleanup()[id] != NULL) { + traits_t::getCleanup()[id]((*it).second); } ++it; } diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 4893075c3..a0086440b 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -679,13 +679,12 @@ namespace attr { */ template struct LastAttributeId { - static uint64_t s_id; + static uint64_t& getId() { + static uint64_t s_id = 0; + return s_id; + } }; -/** Initially zero. */ -template -uint64_t LastAttributeId::s_id = 0; - }/* CVC4::expr::attr namespace */ // ATTRIBUTE TRAITS ============================================================ @@ -699,13 +698,12 @@ namespace attr { template struct AttributeTraits { typedef void (*cleanup_t)(T); - static std::vector cleanup; + static std::vector& getCleanup() { + static std::vector cleanup; + return cleanup; + } }; -template -std::vector::cleanup_t> - AttributeTraits::cleanup; - }/* CVC4::expr::attr namespace */ // ATTRIBUTE DEFINITION ======================================================== @@ -765,9 +763,9 @@ public: typedef typename attr::KindValueToTableValueMapping:: table_value_type table_value_type; typedef attr::AttributeTraits traits; - uint64_t id = attr::LastAttributeId::s_id++; - //Assert(traits::cleanup.size() == id);// sanity check - traits::cleanup.push_back(attr::getCleanupStrategy::getId()++; + Assert(traits::getCleanup().size() == id);// sanity check + traits::getCleanup().push_back(attr::getCleanupStrategy::fn); return id; } @@ -827,7 +825,7 @@ public: * return the id. */ static inline uint64_t registerAttribute() { - uint64_t id = attr::LastAttributeId::s_id++; + uint64_t id = attr::LastAttributeId::getId()++; AlwaysAssert( id <= 63, "Too many boolean node attributes registered " "during initialization !" ); @@ -876,7 +874,7 @@ template const uint64_t Attribute::s_id = ( attr::AttributeTraits:: table_value_type, - context_dep>::cleanup.size(), + context_dep>::getCleanup().size(), Attribute::registerAttribute() ); /** Assign unique IDs to attributes at load time. */ diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index 7a4fcdaff..777326a26 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -105,6 +105,9 @@ public: Assert(false, "expected an NoMoreValuesException to be thrown"); } catch(NoMoreValuesException&) { // ignore the exception, we're just asserting that it would be thrown + // + // This block can crash on clang 3.0 on Mac OS, perhaps related to + // bug: http://llvm.org/bugs/show_bug.cgi?id=13359 } } else { try { diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 6cdd18403..be7074f9f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -152,6 +152,7 @@ BUG_TESTS = \ bug486.cvc \ bug497.cvc \ bug507.smt2 \ + bug512.smt2 \ bug512.minimized.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug512.smt2 b/test/regress/regress0/bug512.smt2 new file mode 100644 index 000000000..c9aadfe6e --- /dev/null +++ b/test/regress/regress0/bug512.smt2 @@ -0,0 +1,147 @@ +; COMMAND-LINE: --tlimit-per 2500 -iq +; EXPECT: unknown +; EXPECT: (:reason-unknown timeout) +; EXPECT: unsat +; EXIT: 20 +(set-option :print-success false) +(set-info :smt-lib-version 2.0) +;(set-option :AUTO_CONFIG false) +;(set-option :MODEL_HIDE_UNUSED_PARTITIONS false) +;(set-option :MODEL_V2 true) +;(set-option :ASYNC_COMMANDS false) +;(set-option :PHASE_SELECTION 0) +;(set-option :RESTART_STRATEGY 0) +;(set-option :RESTART_FACTOR |1.5|) +;(set-option :ARITH_RANDOM_INITIAL_VALUE true) +;(set-option :CASE_SPLIT 3) +;(set-option :DELAY_UNITS true) +;(set-option :DELAY_UNITS_THRESHOLD 16) +;(set-option :NNF_SK_HACK true) +;(set-option :MBQI false) +;(set-option :QI_EAGER_THRESHOLD 100) +;(set-option :QI_COST |"(+ weight generation)"|) +;(set-option :TYPE_CHECK true) +;(set-option :BV_REFLECT true) +; done setting options + +; Boogie universal background predicate +; Copyright (c) 2004-2010, Microsoft Corp. +(set-info :category "industrial") +(declare-sort |T@U| 0) +(declare-sort |T@T| 0) +(declare-fun real_pow (Real Real) Real) +(declare-fun UOrdering2 (|T@U| |T@U|) Bool) +(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool) + +(declare-fun tickleBool (Bool) Bool) +(assert (and (tickleBool true) (tickleBool false))) +(declare-fun Ctor (T@T) Int) +(declare-fun intType () T@T) +(declare-fun realType () T@T) +(declare-fun boolType () T@T) +(declare-fun int_2_U (Int) T@U) +(declare-fun U_2_int (T@U) Int) +(declare-fun type (T@U) T@T) +(declare-fun real_2_U (Real) T@U) +(declare-fun U_2_real (T@U) Real) +(declare-fun bool_2_U (Bool) T@U) +(declare-fun U_2_bool (T@U) Bool) +(declare-fun %lbl%+67 () Bool) +(declare-fun i@0 () Int) +(declare-fun x@@5 () Int) +(declare-fun y@@1 () Int) +(declare-fun i@1 () Int) +(declare-fun %lbl%@186 () Bool) +(declare-fun %lbl%+69 () Bool) +(declare-fun %lbl%@157 () Bool) +(declare-fun %lbl%+65 () Bool) +(declare-fun %lbl%+63 () Bool) +(declare-fun %lbl%@125 () Bool) +(declare-fun %lbl%+97 () Bool) +(assert (and +(= (Ctor intType) 0) +(= (Ctor realType) 1) +(= (Ctor boolType) 2) +(forall ((arg0 Int) ) (! (= (U_2_int (int_2_U arg0)) arg0) + :qid |typeInv:U_2_int| + :pattern ( (int_2_U arg0)) +)) +(forall ((x T@U) ) (! (=> (= (type x) intType) (= (int_2_U (U_2_int x)) x)) + :qid |cast:U_2_int| + :pattern ( (U_2_int x)) +)) +(forall ((arg0@@0 Int) ) (! (= (type (int_2_U arg0@@0)) intType) + :qid |funType:int_2_U| + :pattern ( (int_2_U arg0@@0)) +)) +(forall ((arg0@@1 Real) ) (! (= (U_2_real (real_2_U arg0@@1)) arg0@@1) + :qid |typeInv:U_2_real| + :pattern ( (real_2_U arg0@@1)) +)) +(forall ((x@@0 T@U) ) (! (=> (= (type x@@0) realType) (= (real_2_U (U_2_real x@@0)) x@@0)) + :qid |cast:U_2_real| + :pattern ( (U_2_real x@@0)) +)) +(forall ((arg0@@2 Real) ) (! (= (type (real_2_U arg0@@2)) realType) + :qid |funType:real_2_U| + :pattern ( (real_2_U arg0@@2)) +)) +(forall ((arg0@@3 Bool) ) (! (= (U_2_bool (bool_2_U arg0@@3)) arg0@@3) + :qid |typeInv:U_2_bool| + :pattern ( (bool_2_U arg0@@3)) +)) +(forall ((x@@1 T@U) ) (! (=> (= (type x@@1) boolType) (= (bool_2_U (U_2_bool x@@1)) x@@1)) + :qid |cast:U_2_bool| + :pattern ( (U_2_bool x@@1)) +)) +(forall ((arg0@@4 Bool) ) (! (= (type (bool_2_U arg0@@4)) boolType) + :qid |funType:bool_2_U| + :pattern ( (bool_2_U arg0@@4)) +)))) +(assert (forall ((x@@2 T@U) ) (! (UOrdering2 x@@2 x@@2) + :qid |bg:subtype-refl| + :no-pattern (U_2_int x@@2) + :no-pattern (U_2_bool x@@2) +))) +(assert (forall ((x@@3 T@U) (y T@U) (z T@U) ) (! (let ((alpha (type x@@3))) +(=> (and +(= (type y) alpha) +(= (type z) alpha) +(UOrdering2 x@@3 y) +(UOrdering2 y z)) (UOrdering2 x@@3 z))) + :qid |bg:subtype-trans| + :pattern ( (UOrdering2 x@@3 y) (UOrdering2 y z)) +))) +(assert (forall ((x@@4 T@U) (y@@0 T@U) ) (! (let ((alpha@@0 (type x@@4))) +(=> (= (type y@@0) alpha@@0) (=> (and +(UOrdering2 x@@4 y@@0) +(UOrdering2 y@@0 x@@4)) (= x@@4 y@@0)))) + :qid |bg:subtype-antisymm| + :pattern ( (UOrdering2 x@@4 y@@0) (UOrdering2 y@@0 x@@4)) +))) +(push 1) +(set-info :boogie-vc-id foo) +(assert (not +(let ((anon3_LoopBody_correct (=> (! (and %lbl%+67 true) :lblpos +67) (=> (and +(< i@0 (+ x@@5 y@@1)) +(= i@1 (+ i@0 1))) (and +(! (or %lbl%@186 (<= i@1 (+ x@@5 y@@1))) :lblneg @186) +(=> (<= i@1 (+ x@@5 y@@1)) true)))))) +(let ((anon3_LoopDone_correct (=> (! (and %lbl%+69 true) :lblpos +69) (=> (<= (+ x@@5 y@@1) i@0) (and +(! (or %lbl%@157 (= i@0 (- x@@5 y@@1))) :lblneg @157) +(=> (= i@0 (- x@@5 y@@1)) true)))))) +(let ((anon3_LoopHead_correct (=> (! (and %lbl%+65 true) :lblpos +65) (=> (<= i@0 (+ x@@5 y@@1)) (and +anon3_LoopDone_correct +anon3_LoopBody_correct))))) +(let ((anon0_correct (=> (! (and %lbl%+63 true) :lblpos +63) (and +(! (or %lbl%@125 (<= x@@5 (+ x@@5 y@@1))) :lblneg @125) +(=> (<= x@@5 (+ x@@5 y@@1)) anon3_LoopHead_correct))))) +(let ((PreconditionGeneratedEntry_correct (=> (! (and %lbl%+97 true) :lblpos +97) (=> (>= y@@1 0) anon0_correct)))) +PreconditionGeneratedEntry_correct))))) +)) +(check-sat) +(get-info :reason-unknown) +;(labels) +(assert %lbl%@157) +(check-sat) +(pop 1) diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 11a3d85c8..5ce5badd0 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -94,7 +94,7 @@ public: // and that the next ID to be assigned is strictly greater than // those that have already been assigned. - unsigned lastId = attr::LastAttributeId::s_id; + unsigned lastId = attr::LastAttributeId::getId(); TS_ASSERT_LESS_THAN(VarNameAttr::s_id, lastId); TS_ASSERT_LESS_THAN(TestStringAttr1::s_id, lastId); TS_ASSERT_LESS_THAN(TestStringAttr2::s_id, lastId); @@ -103,10 +103,10 @@ public: TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr2::s_id); TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id); - //lastId = attr::LastAttributeId::s_id; + //lastId = attr::LastAttributeId::getId(); //TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); - lastId = attr::LastAttributeId::s_id; + lastId = attr::LastAttributeId::getId(); TS_ASSERT_LESS_THAN(TestFlag1::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag2::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag3::s_id, lastId); @@ -123,14 +123,14 @@ public: TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag5::s_id); TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id); - lastId = attr::LastAttributeId::s_id; + lastId = attr::LastAttributeId::getId(); TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId); TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id); cout << "1: " << TestFlag1cd::s_id << endl; cout << "2: " << TestFlag2cd::s_id << endl; - lastId = attr::LastAttributeId::s_id; + lastId = attr::LastAttributeId::getId(); // TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId); // TS_ASSERT_LESS_THAN(theory::PostRewriteCache::s_id, lastId); // TS_ASSERT_LESS_THAN(theory::PreRewriteCacheTop::s_id, lastId); @@ -142,7 +142,7 @@ public: // TS_ASSERT_DIFFERS(theory::PostRewriteCache::s_id, theory::PostRewriteCacheTop::s_id); // TS_ASSERT_DIFFERS(theory::PreRewriteCacheTop::s_id, theory::PostRewriteCacheTop::s_id); - lastId = attr::LastAttributeId::s_id; + lastId = attr::LastAttributeId::getId(); TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId); } -- 2.30.2