Use thread_local instead of compiler extensions (#210)

C++11 introduced the thread_local keyword, so we don't need to use
non-standard extensions or our custom pthread extension anymore.
The behavior was previously introduced as a workaround in commit
753a072c542c1c254d7c6adbf10e091ba585ede5. This commit
introduces the macro CVC4_THREAD_LOCAL that can be used to
declare variables as thread local. For Swig, this macro is defined to
be empty.

7 files changed, 40 insertions, 215 deletions

diff --git a/src/base/Makefile.am b/src/base/Makefile.am
index 491baaa90..5537bbbdd 100644
--- a/src/base/Makefile.am
+++ b/src/base/Makefile.am
@@ -5,7 +5,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libbase.la
 
-# Do not list built sources (like tls.h) here!
+# Do not list built sources here!
 # Rather, list them under BUILT_SOURCES, and their .in versions under
 # EXTRA_DIST.  Otherwise, they're packaged up in the tarball, which is
 # no good---they belong in the configured builds/ directory.  If they
@@ -26,17 +26,14 @@ libbase_la_SOURCES = \
 	listener.h \
 	modal_exception.h \
 	output.cpp \
-	output.h
-
-
-BUILT_SOURCES = \
+	output.h \
 	tls.h
 
 # listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it
 # after building (if it does, we don't get the "cached" effect with
 # the .tmp files below, and we have to re-compile and re-link each
 # time, even when there are no changes).
-BUILT_SOURCES += \
+BUILT_SOURCES = \
 	Debug_tags.h \
 	Debug_tags \
 	Trace_tags.h \
@@ -55,12 +52,7 @@ EXTRA_DIST = \
 	exception.i \
 	mktagheaders \
 	mktags \
-	modal_exception.i \
-	tls.h.in
-
-DISTCLEANFILES = \
-	tls.h.tmp \
-	tls.h
+	modal_exception.i
 
 %_tags.h: %_tags mktagheaders
 	$(AM_V_at)chmod +x @srcdir@/mktagheaders
diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp
index c122667f3..f342f5562 100644
--- a/src/base/cvc4_assert.cpp
+++ b/src/base/cvc4_assert.cpp
@@ -20,13 +20,14 @@
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
+#include "base/tls.h"
 
 using namespace std;
 
 namespace CVC4 {
 
 #ifdef CVC4_DEBUG
-//CVC4_THREADLOCAL(const char*) s_debugLastException = NULL;
+//CVC4_THREAD_LOCAL const char* s_debugLastException = NULL;
 #endif /* CVC4_DEBUG */
 
 
@@ -140,7 +141,7 @@ void AssertionException::construct(const char* header, const char* extra,
  */
 void debugAssertionFailed(const AssertionException& thisException,
                           const char* propagatingException) {
-  static CVC4_THREADLOCAL(bool) alreadyFired = false;
+  static CVC4_THREAD_LOCAL bool alreadyFired = false;
 
   if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) {
     throw thisException;
diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h
index d4942f47c..bb4d57170 100644
--- a/src/base/cvc4_assert.h
+++ b/src/base/cvc4_assert.h
@@ -26,7 +26,6 @@
 #include <string>
 
 #include "base/exception.h"
-#include "base/tls.h"
 
 // output.h not strictly needed for this header, but it _is_ needed to
 // actually _use_ anything in this header, so let's include it.
diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index 7df050726..990ae77c6 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -28,7 +28,7 @@ using namespace std;
 
 namespace CVC4 {
 
-CVC4_THREADLOCAL(LastExceptionBuffer*) LastExceptionBuffer::s_currentBuffer = NULL;
+CVC4_THREAD_LOCAL LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = NULL;
 
 LastExceptionBuffer::LastExceptionBuffer() : d_contents(NULL) {}
 
diff --git a/src/base/exception.h b/src/base/exception.h
index 1ce2ae757..01a054b19 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -160,7 +160,7 @@ private:
 
   char* d_contents;
 
-  static CVC4_THREADLOCAL(LastExceptionBuffer*) s_currentBuffer;
+  static CVC4_THREAD_LOCAL LastExceptionBuffer* s_currentBuffer;
 }; /* class LastExceptionBuffer */
 
 }/* CVC4 namespace */
diff --git a/src/base/tls.h b/src/base/tls.h
new file mode 100644
index 000000000..a60b0d8f9
--- /dev/null
+++ b/src/base/tls.h
@@ -0,0 +1,31 @@
+/*********************                                                        */
+/*! \file tls.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Definiton of CVC4_THREAD_LOCAL
+ **
+ ** This header defines CVC4_THREAD_LOCAL, which should be used instead of
+ ** thread_local because it is not supported by all build types (e.g. Swig).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__BASE__TLS_H
+#define __CVC4__BASE__TLS_H
+
+#if SWIG && (!defined(SWIG_VERSION) || SWIG_VERSION < 0x030000)
+// SWIG versions older than 3.0 do not support thread_local, so just redefine
+// CVC4_THREAD_LOCAL to be empty for those versions.
+#define CVC4_THREAD_LOCAL
+#else
+#define CVC4_THREAD_LOCAL thread_local
+#endif
+
+#endif /* __CVC4__BASE__TLS_H */
diff --git a/src/base/tls.h.in b/src/base/tls.h.in
deleted file mode 100644
index c66aef767..000000000
--- a/src/base/tls.h.in
+++ /dev/null
@@ -1,198 +0,0 @@
-/*********************                                                        */
-/*! \file tls.h.in
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, ACSYS, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  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
-
-// A bit obnoxious: we have to take varargs to support multi-argument
-// template types in the threadlocals.
-// E.g. "CVC4_THREADLOCAL(hash_set<type, hasher>*)" fails otherwise,
-// due to the embedded comma.
-#if @CVC4_TLS_SUPPORTED@
-#  define CVC4_THREADLOCAL(__type...) @CVC4_TLS@ __type
-#  define CVC4_THREADLOCAL_PUBLIC(__type...) @CVC4_TLS@ CVC4_PUBLIC __type
-#  define CVC4_THREADLOCAL_TYPE(__type...) __type
-#else
-#  include <pthread.h>
-#  define CVC4_THREADLOCAL(__type...) ::CVC4::ThreadLocal< __type >
-#  define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC ::CVC4::ThreadLocal< __type >
-#  define CVC4_THREADLOCAL_TYPE(__type...) ::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(const 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 static_cast<T>(reinterpret_cast<size_t>(pthread_getspecific(d_key)));
-  }
-};/* class ThreadLocalImpl<T, true> */
-
-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(const 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 static_cast<T*>(pthread_getspecific(d_key));
-  }
-
-  T operator*() {
-    return *static_cast<T*>(pthread_getspecific(d_key));
-  }
-  T* operator->() {
-    return static_cast<T*>(pthread_getspecific(d_key));
-  }
-};/* class ThreadLocalImpl<T*, true> */
-
-template <class T>
-class ThreadLocalImpl<T, false> {
-};/* class ThreadLocalImpl<T, false> */
-
-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) {}
-
-  ThreadLocal<T>& operator=(const T& t) {
-    return static_cast< ThreadLocal<T>& >(super::operator=(t));
-  }
-  ThreadLocal<T>& operator=(const ThreadLocal<T>& tl) {
-    return static_cast< ThreadLocal<T>& >(super::operator=(tl));
-  }
-};/* class ThreadLocal<T> */
-
-template <class T>
-class ThreadLocal<T*> : public ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> {
-  typedef ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> super;
-
-public:
-  ThreadLocal() : super() {}
-  ThreadLocal(T* t) : super(t) {}
-  ThreadLocal(const ThreadLocal<T*>& tl) : super(tl) {}
-
-  ThreadLocal<T*>& operator=(T* t) {
-    return static_cast< ThreadLocal<T*>& >(super::operator=(t));
-  }
-  ThreadLocal<T*>& operator=(const ThreadLocal<T*>& tl) {
-    return static_cast< ThreadLocal<T*>& >(super::operator=(tl));
-  }
-  // special operators for pointers
-  T& operator*() {
-    return *static_cast<T*>(*this);
-  }
-  const T& operator*() const {
-    return *static_cast<const T*>(*this);
-  }
-  T* operator->() {
-    return static_cast<T*>(*this);
-  }
-  const T* operator->() const {
-    return static_cast<const T*>(*this);
-  }
-  T* operator++() {
-    T* p = *this;
-    *this = ++p;
-    return p;
-  }
-  T* operator++(int) {
-    T* p = *this;
-    *this = p + 1;
-    return p;
-  }
-  T* operator--() {
-    T* p = *this;
-    *this = --p;
-    return p;
-  }
-  T* operator--(int) {
-    T* p = *this;
-    *this = p - 1;
-    return p;
-  }
-};/* class ThreadLocal<T*> */
-
-}/* CVC4 namespace */
-
-#endif /* @CVC4_TLS_SUPPORTED@ */
-
-#endif /* __CVC4__TLS_H */