Fix clang static initialization order issue; fixes bug 512.

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 70f04be851f9e813d26a8d95951145dedd20a4dc..969843ddd7db95b5ef6167ce800766fc603eca13 100644 (file)
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -522,14 +522,14 @@ AttributeManager::setAttribute(NodeValue* nv,
 template <class T>
 inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
                                               NodeValue* nv) {
-  for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
+  for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::getId(); ++id) {
     typedef AttributeTraits<T, false> traits_t;
     typedef AttrHash<T> hash_t;
     std::pair<uint64_t, NodeValue*> 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<T>& table,
 template <class T>
 inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table,
                                               NodeValue* nv) {
-  for(unsigned id = 0; id < attr::LastAttributeId<T, true>::s_id; ++id) {
+  for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) {
     table.obliterate(std::make_pair(id, nv));
   }
 }
@@ -558,8 +558,8 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
   bool anyRequireClearing = false;
   typedef AttributeTraits<T, false> traits_t;
   typedef AttrHash<T> hash_t;
-  for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
-    if(traits_t::cleanup[id] != NULL) {
+  for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::getId(); ++id) {
+    if(traits_t::getCleanup()[id] != NULL) {
       anyRequireClearing = true;
     }
   }
@@ -575,8 +575,8 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& 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 4893075c323e9ede60de3c0a03e944ac614b59a4..a0086440bf075b421132a7650aa7d1d8b0ec72ae 100644 (file)
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -679,13 +679,12 @@ namespace attr {
  */
 template <class T, bool context_dep>
 struct LastAttributeId {
-  static uint64_t s_id;
+  static uint64_t& getId() {
+    static uint64_t s_id = 0;
+    return s_id;
+  }
 };
 
-/** Initially zero. */
-template <class T, bool context_dep>
-uint64_t LastAttributeId<T, context_dep>::s_id = 0;
-
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE TRAITS ============================================================
@@ -699,13 +698,12 @@ namespace attr {
 template <class T, bool context_dep>
 struct AttributeTraits {
   typedef void (*cleanup_t)(T);
-  static std::vector<cleanup_t> cleanup;
+  static std::vector<cleanup_t>& getCleanup() {
+    static std::vector<cleanup_t> cleanup;
+    return cleanup;
+  }
 };
 
-template <class T, bool context_dep>
-std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
-  AttributeTraits<T, context_dep>::cleanup;
-
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE DEFINITION ========================================================
@@ -765,9 +763,9 @@ public:
     typedef typename attr::KindValueToTableValueMapping<value_t>::
                      table_value_type table_value_type;
     typedef attr::AttributeTraits<table_value_type, context_dep> traits;
-    uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
-    //Assert(traits::cleanup.size() == id);// sanity check
-    traits::cleanup.push_back(attr::getCleanupStrategy<value_t,
+    uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::getId()++;
+    Assert(traits::getCleanup().size() == id);// sanity check
+    traits::getCleanup().push_back(attr::getCleanupStrategy<value_t,
                                                        CleanupStrategy>::fn);
     return id;
   }
@@ -827,7 +825,7 @@ public:
    * return the id.
    */
   static inline uint64_t registerAttribute() {
-    uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++;
+    uint64_t id = attr::LastAttributeId<bool, context_dep>::getId()++;
     AlwaysAssert( id <= 63,
                   "Too many boolean node attributes registered "
                   "during initialization !" );
@@ -876,7 +874,7 @@ template <class T, class value_t, class CleanupStrategy, bool context_dep>
 const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id =
   ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::
                                    table_value_type,
-                          context_dep>::cleanup.size(),
+                          context_dep>::getCleanup().size(),
     Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() );
 
 /** Assign unique IDs to attributes at load time. */

diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index 7a4fcdaff2b29af7c111c4f85d8f45d936823149..777326a267e785f2a0eb319748a95deefef84d38 100644 (file)
--- 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 6cdd184030cd75d1ec4723ded9d65790ce30a8dd..be7074f9f3c2c2027cdcce6c72002c847b32e489 100644 (file)
--- 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 (file)
index 0000000..c9aadfe
--- /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 11a3d85c81831d4bede6ba2ff9c75c086d9d3dfd..5ce5badd012d4b2c7e173bc80f14f864fa7c68f4 100644 (file)
--- 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<string, false>::s_id;
+    unsigned lastId = attr::LastAttributeId<string, false>::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<void*, false>::s_id;
+    //lastId = attr::LastAttributeId<void*, false>::getId();
     //TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
 
-    lastId = attr::LastAttributeId<bool, false>::s_id;
+    lastId = attr::LastAttributeId<bool, false>::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<bool, true>::s_id;
+    lastId = attr::LastAttributeId<bool, true>::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<Node, false>::s_id;
+    lastId = attr::LastAttributeId<Node, false>::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<TypeNode, false>::s_id;
+    lastId = attr::LastAttributeId<TypeNode, false>::getId();
     TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
 
   }