add workaround for systems (i.e., Mac OS X) that don't support __thread; also configure script auto-detection of __thread support and syntax

10 files changed, 145 insertions, 30 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1f15f7e29..31b848885 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -28,6 +28,7 @@
 #include "theory/bv/theory_bv_type_rules.h"
 
 #include "util/Assert.h"
+#include "util/tls.h"
 
 #include <ext/hash_set>
 #include <algorithm>
@@ -38,7 +39,7 @@ using __gnu_cxx::hash_set;
 
 namespace CVC4 {
 
-__thread NodeManager* NodeManager::s_current = 0;
+CVC4_THREADLOCAL(NodeManager*) NodeManager::s_current = 0;
 
 /**
  * This class sets it reference argument to true and ensures that it gets set
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index bf1bed5f0..5fb7c57ad 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -38,6 +38,7 @@
 #include "expr/node_value.h"
 #include "context/context.h"
 #include "util/configuration_private.h"
+#include "util/tls.h"
 
 namespace CVC4 {
 
@@ -70,7 +71,7 @@ class NodeManager {
                               expr::NodeValueIDHashFunction,
                               expr::NodeValueEq> ZombieSet;
 
-  static __thread NodeManager* s_current;
+  static CVC4_THREADLOCAL(NodeManager*) s_current;
 
   NodeValuePool d_nodeValuePool;
 
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 968563b97..ddb9f84c8 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -94,7 +94,8 @@ void cvc4unexpected() {
     fprintf(stderr,
             "The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
   } else {
-    fprintf(stderr, "The exception is:\n%s\n\n", CVC4::s_debugLastException);
+    fprintf(stderr, "The exception is:\n%s\n\n",
+            static_cast<const char*>(CVC4::s_debugLastException));
   }
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index 7856b3da4..01c40aca2 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -22,13 +22,14 @@
 
 #include "util/Assert.h"
 #include "util/exception.h"
+#include "util/tls.h"
 
 using namespace std;
 
 namespace CVC4 {
 
 #ifdef CVC4_DEBUG
-__thread CVC4_PUBLIC const char* s_debugLastException = NULL;
+CVC4_PUBLIC CVC4_THREADLOCAL(const char*) s_debugLastException = NULL;
 #endif /* CVC4_DEBUG */
 
 void AssertionException::construct(const char* header, const char* extra,
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 62375daff..65c067b7e 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -29,6 +29,7 @@
 
 #include "util/exception.h"
 #include "util/output.h"
+#include "util/tls.h"
 
 namespace CVC4 {
 
@@ -199,7 +200,7 @@ public:
 #ifdef CVC4_DEBUG
 
 #ifdef CVC4_DEBUG
-extern __thread CVC4_PUBLIC const char* s_debugLastException;
+extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException;
 #endif /* CVC4_DEBUG */
 
 /**
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index bac0064bf..78f91edc5 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -39,7 +39,8 @@ libutil_la_SOURCES = \
 
 BUILT_SOURCES = \
 	rational.h \
-	integer.h
+	integer.h \
+	tls.h
 
 if CVC4_CLN_IMP
 libutil_la_SOURCES += \
@@ -62,4 +63,5 @@ EXTRA_DIST = \
 	rational_gmp_imp.cpp \
 	integer_gmp_imp.cpp \
 	rational.h.in \
-	integer.h.in
+	integer.h.in \
+	tls.h.in
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 072a93b18..499b0c8e2 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -78,11 +78,15 @@ string Configuration::about() {
 }
 
 bool Configuration::isBuiltWithGmp() {
- return IS_GMP_BUILD;
+  return IS_GMP_BUILD;
 }
 
 bool Configuration::isBuiltWithCln() {
- return IS_CLN_BUILD;
+  return IS_CLN_BUILD;
+}
+
+bool Configuration::isBuiltWithTlsSupport() {
+  return USING_TLS;
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/configuration.h b/src/util/configuration.h
index cca9202bf..ff89a3d6c 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -66,6 +66,8 @@ public:
   static bool isBuiltWithGmp();
 
   static bool isBuiltWithCln();
+
+  static bool isBuiltWithTlsSupport();
 };
 
 }/* CVC4 namespace */
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 913fcc3e9..227250745 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -11,10 +11,15 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Provides compile-time configuration information about the 
+ ** \brief Provides compile-time configuration information about the
  ** CVC4 library.
  **/
 
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONFIGURATION_PRIVATE_H
+#define __CVC4__CONFIGURATION_PRIVATE_H
+
 #include "cvc4autoconfig.h"
 
 using namespace std;
@@ -22,59 +27,65 @@ using namespace std;
 namespace CVC4 {
 
 #ifdef CVC4_DEBUG
-#define IS_DEBUG_BUILD true
+#  define IS_DEBUG_BUILD true
 #else /* CVC4_DEBUG */
-#define IS_DEBUG_BUILD false
+#  define IS_DEBUG_BUILD false
 #endif /* CVC4_DEBUG */
-  
+
 #ifdef CVC4_TRACING
-#define IS_TRACING_BUILD true
+#  define IS_TRACING_BUILD true
 #else /* CVC4_TRACING */
-#define IS_TRACING_BUILD false
+#  define IS_TRACING_BUILD false
 #endif /* CVC4_TRACING */
 
 #ifdef CVC4_MUZZLE
-#define IS_MUZZLED_BUILD true
+#  define IS_MUZZLED_BUILD true
 #else /* CVC4_MUZZLE */
-#define IS_MUZZLED_BUILD false
+#  define IS_MUZZLED_BUILD false
 #endif /* CVC4_MUZZLE */
 
 #ifdef CVC4_ASSERTIONS
-#define IS_ASSERTIONS_BUILD true
+#  define IS_ASSERTIONS_BUILD true
 #else /* CVC4_ASSERTIONS */
-#define IS_ASSERTIONS_BUILD false
+#  define IS_ASSERTIONS_BUILD false
 #endif /* CVC4_ASSERTIONS */
 
 #ifdef CVC4_COVERAGE
-#define IS_COVERAGE_BUILD true
+#  define IS_COVERAGE_BUILD true
 #else /* CVC4_COVERAGE */
-#define IS_COVERAGE_BUILD false
+#  define IS_COVERAGE_BUILD false
 #endif /* CVC4_COVERAGE */
 
 #ifdef CVC4_PROFILING
-#define IS_PROFILING_BUILD true
+#  define IS_PROFILING_BUILD true
 #else /* CVC4_PROFILING */
-#define IS_PROFILING_BUILD false
+#  define IS_PROFILING_BUILD false
 #endif /* CVC4_PROFILING */
 
 #ifdef CVC4_COMPETITION_MODE
-#define IS_COMPETITION_BUILD true
+#  define IS_COMPETITION_BUILD true
 #else /* CVC4_COMPETITION_MODE */
-#define IS_COMPETITION_BUILD false
+#  define IS_COMPETITION_BUILD false
 #endif /* CVC4_COMPETITION_MODE */
 
 #ifdef CVC4_GMP_IMP
-#define IS_GMP_BUILD true
+#  define IS_GMP_BUILD true
 #else /* CVC4_GMP_IMP */
-#define IS_GMP_BUILD false
+#  define IS_GMP_BUILD false
 #endif /* CVC4_GMP_IMP */
 
 #ifdef CVC4_CLN_IMP
-#define IS_CLN_BUILD true
+#  define IS_CLN_BUILD true
 #else /* CVC4_CLN_IMP */
-#define IS_CLN_BUILD false
+#  define IS_CLN_BUILD false
 #endif /* CVC4_CLN_IMP */
 
+#ifdef TLS
+#  define USING_TLS true
+#else /* TLS */
+#  define USING_TLS false
+#endif /* TLS */
+
 #define CVC4_ABOUT_STRING string("\
 This is a pre-release of CVC4.\n\
 Copyright (C) 2009, 2010\n\
@@ -92,5 +103,6 @@ of CVC4 that links against GMP, and can be used in such applications.\n" : \
 "This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
 CVC4 is open-source and is covered by the BSD license (modified).\n")
 
-
 }/* CVC4 namespace */
+
+#endif /* __CVC4__CONFIGURATION_PRIVATE_H */
diff --git a/src/util/tls.h.in b/src/util/tls.h.in
new file mode 100644
index 000000000..29a52497a
--- /dev/null
+++ b/src/util/tls.h.in
@@ -0,0 +1,90 @@
+/*********************                                                        */
+/*! \file tls.h.in
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Header to define CVC4_THREAD whether or not TLS is
+ ** supported by the compiler/runtime platform
+ **
+ ** Header to define CVC4_THREAD whether or not TLS is supported by
+ ** the compiler/runtime platform.  If not, an implementation based on
+ ** pthread_getspecific() / pthread_setspecific() is given.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__TLS_H
+#define __CVC4__TLS_H
+
+#if @CVC4_TLS_SUPPORTED@
+#  define CVC4_THREADLOCAL(__type) @CVC4_TLS@ __type
+#  define CVC4_THREADLOCAL_PUBLIC(__type) @CVC4_TLS@ CVC4_PUBLIC __type
+#else
+#  include <pthread.h>
+#  define CVC4_THREADLOCAL(__type) ::CVC4::ThreadLocal< __type >
+#  define CVC4_THREADLOCAL_PUBLIC(__type) CVC4_PUBLIC ::CVC4::ThreadLocal< __type >
+
+namespace CVC4 {
+
+template <class T, bool small>
+class ThreadLocalImpl;
+
+template <class T>
+class ThreadLocalImpl<T, true> {
+  pthread_key_t d_key;
+
+  static void cleanup(void*) {
+  }
+
+public:
+  ThreadLocalImpl() {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+  }
+
+  ThreadLocalImpl(T t) {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
+  }
+
+  ThreadLocalImpl(const ThreadLocalImpl& tl) {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T&>(tl))));
+  }
+
+  ThreadLocalImpl& operator=(const T& t) {
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
+    return *this;
+  }
+  ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) {
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T&>(tl))));
+    return *this;
+  }
+
+  operator T() const {
+    return reinterpret_cast<T>(pthread_getspecific(d_key));
+  }
+};/* class ThreadLocalImpl<T, true> */
+
+template <class T>
+class ThreadLocal : public ThreadLocalImpl<T, sizeof(T) <= sizeof(void*)> {
+  typedef ThreadLocalImpl<T, sizeof(T) <= sizeof(void*)> super;
+
+public:
+  ThreadLocal() : super() {}
+  ThreadLocal(const T& t) : super(t) {}
+  ThreadLocal(const ThreadLocal<T>& tl) : super(tl) {}
+};/* class ThreadLocal<T> */
+
+}/* CVC4 namespace */
+
+#endif /* @CVC4_TLS_SUPPORTED@ */
+
+#endif /* _CVC4__TLS_H */