From 546d795470ca7c30fc62fe9b6c7b8e5838e1eed4 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 30 Aug 2017 20:55:27 -0700 Subject: [PATCH] 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. --- COPYING | 34 ---- config/ax_tls.m4 | 76 --------- configure.ac | 31 ---- src/Makefile.am | 2 - src/base/Makefile.am | 16 +- src/base/cvc4_assert.cpp | 5 +- src/base/cvc4_assert.h | 1 - src/base/exception.cpp | 2 +- src/base/exception.h | 2 +- src/base/tls.h | 31 ++++ src/base/tls.h.in | 198 ---------------------- src/bindings/swig.h | 10 +- src/expr/node_manager.cpp | 3 +- src/expr/node_manager.h | 2 +- src/main/driver_unified.cpp | 3 +- src/main/main.h | 4 +- src/main/util.cpp | 1 - src/options/options.h | 4 +- src/options/options_public_functions.cpp | 1 - src/options/options_template.cpp | 8 +- src/smt/smt_engine_scope.cpp | 3 +- src/smt_util/node_visitor.h | 7 +- src/theory/arith/dual_simplex.cpp | 3 +- src/theory/arith/fc_simplex.cpp | 3 +- src/theory/arith/soi_simplex.cpp | 3 +- src/theory/arith/theory_arith_private.cpp | 5 +- src/theory/rewriter.cpp | 2 +- 27 files changed, 70 insertions(+), 390 deletions(-) delete mode 100644 config/ax_tls.m4 create mode 100644 src/base/tls.h delete mode 100644 src/base/tls.h.in diff --git a/COPYING b/COPYING index 4e3e64bce..b251f6c77 100644 --- a/COPYING +++ b/COPYING @@ -130,40 +130,6 @@ copyright. See config/pkg.m4. Its copyright: configuration script generated by Autoconf, you may include it under the same distribution terms that you use for the rest of that program. -CVC4 incorporates the m4 macro file "ax_tls.m4", excluded from the above -copyright and downloaded from -http://www.gnu.org/software/autoconf-archive/ax_tls.html. -See config/ax_tls.m4. Its copyright: - - Copyright (c) 2008 Alan Woodland - Copyright (c) 2010 Diego Elio Petteno` - - This program is free software: you can redistribute it and/or modify it - under the terms of the GNU General Public License as published by the - Free Software Foundation, either version 3 of the License, or (at your - option) any later version. - - This program is distributed in the hope that it will be useful, but - WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General - Public License for more details. - - You should have received a copy of the GNU General Public License along - with this program. If not, see . - - As a special exception, the respective Autoconf Macro's copyright owner - gives unlimited permission to copy, distribute and modify the configure - scripts that are the output of Autoconf when processing the Macro. You - need not follow the terms of the GNU General Public License when using - or distributing such scripts, even though portions of the text of the - Macro appear in them. The GNU General Public License (GPL) does govern - all other use of the material that constitutes the Autoconf Macro. - - This special exception to the GPL applies to versions of the Autoconf - Macro released by the Autoconf Archive. When you make and distribute a - modified version of the Autoconf Macro, you may extend this special - exception to the GPL to apply to your modified version as well. - CVC4 incorporates the m4 macro file "boost.m4", excluded from the above copyright and downloaded from http://github.com/tsuna/boost.m4 . See config/boost.m4. Its copyright: diff --git a/config/ax_tls.m4 b/config/ax_tls.m4 deleted file mode 100644 index 033e3b135..000000000 --- a/config/ax_tls.m4 +++ /dev/null @@ -1,76 +0,0 @@ -# =========================================================================== -# http://www.gnu.org/software/autoconf-archive/ax_tls.html -# =========================================================================== -# -# SYNOPSIS -# -# AX_TLS([action-if-found], [action-if-not-found]) -# -# DESCRIPTION -# -# Provides a test for the compiler support of thread local storage (TLS) -# extensions. Defines TLS if it is found. Currently knows about GCC/ICC -# and MSVC. I think SunPro uses the same as GCC, and Borland apparently -# supports either. -# -# LICENSE -# -# Copyright (c) 2008 Alan Woodland -# Copyright (c) 2010 Diego Elio Petteno` -# -# This program is free software: you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by the -# Free Software Foundation, either version 3 of the License, or (at your -# option) any later version. -# -# This program is distributed in the hope that it will be useful, but -# WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General -# Public License for more details. -# -# You should have received a copy of the GNU General Public License along -# with this program. If not, see . -# -# As a special exception, the respective Autoconf Macro's copyright owner -# gives unlimited permission to copy, distribute and modify the configure -# scripts that are the output of Autoconf when processing the Macro. You -# need not follow the terms of the GNU General Public License when using -# or distributing such scripts, even though portions of the text of the -# Macro appear in them. The GNU General Public License (GPL) does govern -# all other use of the material that constitutes the Autoconf Macro. -# -# This special exception to the GPL applies to versions of the Autoconf -# Macro released by the Autoconf Archive. When you make and distribute a -# modified version of the Autoconf Macro, you may extend this special -# exception to the GPL to apply to your modified version as well. - -#serial 10 - -AC_DEFUN([AX_TLS], [ - AC_MSG_CHECKING(for thread local storage (TLS) class) - AC_CACHE_VAL(ac_cv_tls, [ - ax_tls_keywords="__thread __declspec(thread) none" - for ax_tls_keyword in $ax_tls_keywords; do - AS_CASE([$ax_tls_keyword], - [none], [ac_cv_tls=none ; break], - [AC_TRY_COMPILE( - [#include - static void - foo(void) { - static ] $ax_tls_keyword [ int bar; - exit(1); - }], - [], - [ac_cv_tls=$ax_tls_keyword ; break], - ac_cv_tls=none - )]) - done - ]) - AC_MSG_RESULT($ac_cv_tls) - - AS_IF([test "$ac_cv_tls" != "none"], - AC_DEFINE_UNQUOTED([TLS], $ac_cv_tls, [If the compiler supports a TLS storage class define it to that here]) - m4_ifnblank([$1], [$1]), - m4_ifnblank([$2], [$2]) - ) -]) diff --git a/configure.ac b/configure.ac index 1c0240f36..a46585a77 100644 --- a/configure.ac +++ b/configure.ac @@ -1213,35 +1213,6 @@ fi AC_SUBST(CVC4_BUILD_LIBCOMPAT) AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes]) -# Check for availability of TLS support (e.g. __thread storage class) -AC_MSG_CHECKING([whether to use compiler-supported TLS if available]) -AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS])) -if test $cvc4_has_threads = no; then - # We disable TLS entirely by simply telling the build system that - # the empty string is the __thread keyword. - AC_MSG_RESULT([multithreading disabled]) - CVC4_TLS_SUPPORTED=1 - CVC4_TLS= - CVC4_TLS_explanation='disabled (no multithreading support)' -else - if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then - AC_MSG_RESULT([yes]) - AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=]) - else - AC_MSG_RESULT([no]) - CVC4_TLS= - fi - if test -n "$CVC4_TLS"; then - CVC4_TLS_SUPPORTED=1 - CVC4_TLS_explanation="$CVC4_TLS" - else - CVC4_TLS_explanation='pthread_getspecific()' - CVC4_TLS_SUPPORTED=0 - fi -fi -AC_SUBST([CVC4_TLS]) -AC_SUBST([CVC4_TLS_SUPPORTED]) - # Whether to compile with google profiling tools cvc4_use_google_perftools=0 AC_ARG_WITH( @@ -1499,7 +1470,6 @@ if test -n "$CVC4_LANGUAGE_BINDINGS"; then fi fi -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/base/tls.h]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h]) @@ -1540,7 +1510,6 @@ Compat lib : $CVC4_BUILD_LIBCOMPAT Bindings : $bindings_to_be_built Multithreaded: $support_multithreaded -TLS support : $CVC4_TLS_explanation Portfolio : $with_portfolio MP library : $mplibrary diff --git a/src/Makefile.am b/src/Makefile.am index 916733016..974f599e4 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -620,7 +620,6 @@ install-data-local: (echo include/cvc4.h; \ echo include/cvc4_public.h; \ echo include/cvc4parser_public.h; \ - echo base/tls.h; \ echo util/integer.h; \ echo util/rational.h; \ find * -name '*.h' | \ @@ -653,7 +652,6 @@ uninstall-local: -(echo include/cvc4.h; \ echo include/cvc4_public.h; \ echo include/cvc4parser_public.h; \ - echo base/tls.h; \ echo util/integer.h; \ echo util/rational.h; \ find * -name '*.h' | \ 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 #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*)" 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 -# 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 ThreadLocalImpl; - -template -class ThreadLocalImpl { - 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(reinterpret_cast(t))); - } - - ThreadLocalImpl(const ThreadLocalImpl& tl) { - pthread_key_create(&d_key, ThreadLocalImpl::cleanup); - pthread_setspecific(d_key, const_cast(reinterpret_cast(static_cast(tl)))); - } - - ThreadLocalImpl& operator=(const T& t) { - pthread_setspecific(d_key, const_cast(reinterpret_cast(t))); - return *this; - } - ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) { - pthread_setspecific(d_key, const_cast(reinterpret_cast(static_cast(tl)))); - return *this; - } - - operator T() const { - return static_cast(reinterpret_cast(pthread_getspecific(d_key))); - } -};/* class ThreadLocalImpl */ - -template -class ThreadLocalImpl { - 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(reinterpret_cast(t))); - } - - ThreadLocalImpl(const ThreadLocalImpl& tl) { - pthread_key_create(&d_key, ThreadLocalImpl::cleanup); - pthread_setspecific(d_key, const_cast(reinterpret_cast(static_cast(tl)))); - } - - ThreadLocalImpl& operator=(const T* t) { - pthread_setspecific(d_key, const_cast(reinterpret_cast(t))); - return *this; - } - ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) { - pthread_setspecific(d_key, const_cast(reinterpret_cast(static_cast(tl)))); - return *this; - } - - operator T*() const { - return static_cast(pthread_getspecific(d_key)); - } - - T operator*() { - return *static_cast(pthread_getspecific(d_key)); - } - T* operator->() { - return static_cast(pthread_getspecific(d_key)); - } -};/* class ThreadLocalImpl */ - -template -class ThreadLocalImpl { -};/* class ThreadLocalImpl */ - -template -class ThreadLocal : public ThreadLocalImpl { - typedef ThreadLocalImpl super; - -public: - ThreadLocal() : super() {} - ThreadLocal(const T& t) : super(t) {} - ThreadLocal(const ThreadLocal& tl) : super(tl) {} - - ThreadLocal& operator=(const T& t) { - return static_cast< ThreadLocal& >(super::operator=(t)); - } - ThreadLocal& operator=(const ThreadLocal& tl) { - return static_cast< ThreadLocal& >(super::operator=(tl)); - } -};/* class ThreadLocal */ - -template -class ThreadLocal : public ThreadLocalImpl { - typedef ThreadLocalImpl super; - -public: - ThreadLocal() : super() {} - ThreadLocal(T* t) : super(t) {} - ThreadLocal(const ThreadLocal& tl) : super(tl) {} - - ThreadLocal& operator=(T* t) { - return static_cast< ThreadLocal& >(super::operator=(t)); - } - ThreadLocal& operator=(const ThreadLocal& tl) { - return static_cast< ThreadLocal& >(super::operator=(tl)); - } - // special operators for pointers - T& operator*() { - return *static_cast(*this); - } - const T& operator*() const { - return *static_cast(*this); - } - T* operator->() { - return static_cast(*this); - } - const T* operator->() const { - return static_cast(*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 */ - -}/* CVC4 namespace */ - -#endif /* @CVC4_TLS_SUPPORTED@ */ - -#endif /* __CVC4__TLS_H */ diff --git a/src/bindings/swig.h b/src/bindings/swig.h index f73ddd9bb..053cb7172 100644 --- a/src/bindings/swig.h +++ b/src/bindings/swig.h @@ -26,15 +26,9 @@ #endif /* SWIG_VERSION */ %import "cvc4_public.h" -#warning "Working around a SWIG segfault in C++ template parsing." -//%import "base/tls.h" -#define CVC4_THREADLOCAL(__type...) __type -#define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC __type -#define CVC4_THREADLOCAL_TYPE(__type...) __type +%import "base/tls.h" -// swig doesn't like the __thread storage class... -#define __thread -// ...or GCC attributes +// swig doesn't like GCC attributes #define __attribute__(x) #endif /* __CVC4__BINDINGS__SWIG_H */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e440261cb..33f057274 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -23,7 +23,6 @@ #include "base/cvc4_assert.h" #include "base/listener.h" -#include "base/tls.h" #include "expr/attribute.h" #include "expr/node_manager_attributes.h" #include "expr/node_manager_listeners.h" @@ -38,7 +37,7 @@ using namespace CVC4::expr; namespace CVC4 { -CVC4_THREADLOCAL(NodeManager*) NodeManager::s_current = NULL; +CVC4_THREAD_LOCAL NodeManager* NodeManager::s_current = NULL; namespace { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index fab5d4688..b1b0bc974 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -101,7 +101,7 @@ class NodeManager { expr::NodeValueIDHashFunction, expr::NodeValueIDEquality> NodeValueIDSet; - static CVC4_THREADLOCAL(NodeManager*) s_current; + static CVC4_THREAD_LOCAL NodeManager* s_current; Options* d_options; StatisticsRegistry* d_statisticsRegistry; diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 2a9202898..cad662d90 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -26,6 +26,7 @@ // This must come before PORTFOLIO_BUILD. #include "cvc4autoconfig.h" +#include "base/tls.h" #include "base/configuration.h" #include "base/output.h" #include "expr/expr_iomanip.h" @@ -55,7 +56,7 @@ using namespace CVC4::main; namespace CVC4 { namespace main { /** Global options variable */ - CVC4_THREADLOCAL(Options*) pOptions; + CVC4_THREAD_LOCAL Options* pOptions; /** Full argv[0] */ const char *progPath; diff --git a/src/main/main.h b/src/main/main.h index dcb5c2a0a..8a5d0971e 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -17,8 +17,8 @@ #include #include -#include "base/exception.h" #include "base/tls.h" +#include "base/exception.h" #include "cvc4autoconfig.h" #include "expr/expr_manager.h" #include "options/options.h" @@ -54,7 +54,7 @@ extern CVC4::TimerStat* pTotalTime; extern bool segvSpin; /** A pointer to the options in play */ -extern CVC4_THREADLOCAL(Options*) pOptions; +extern CVC4_THREAD_LOCAL Options* pOptions; /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(Exception); diff --git a/src/main/util.cpp b/src/main/util.cpp index e08628848..110fc2c67 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -33,7 +33,6 @@ #endif /* __WIN32__ */ #include "base/exception.h" -#include "base/tls.h" #include "cvc4autoconfig.h" #include "main/command_executor.h" #include "main/main.h" diff --git a/src/options/options.h b/src/options/options.h index 6b2bfedad..f93663095 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -29,8 +29,8 @@ #include "base/tls.h" #include "options/argument_extender.h" #include "options/language.h" -#include "options/printer_modes.h" #include "options/option_exception.h" +#include "options/printer_modes.h" namespace CVC4 { @@ -47,7 +47,7 @@ class CVC4_PUBLIC Options { options::OptionsHandler* d_handler; /** The current Options in effect */ - static CVC4_THREADLOCAL(Options*) s_current; + static CVC4_THREAD_LOCAL Options* s_current; /** Listeners for options::forceLogicString being set. */ ListenerCollection d_forceLogicListeners; diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 54fbd3c81..7d71c267a 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -25,7 +25,6 @@ #include "base/listener.h" #include "base/modal_exception.h" -#include "base/tls.h" #include "options/base_options.h" #include "options/language.h" #include "options/main_options.h" diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index bc97e6028..a48b22625 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -48,10 +48,10 @@ extern int optreset; #include #include +#include "base/tls.h" #include "base/cvc4_assert.h" #include "base/exception.h" #include "base/output.h" -#include "base/tls.h" #include "options/argument_extender.h" #include "options/argument_extender_implementation.h" #include "options/didyoumean.h" @@ -75,7 +75,7 @@ using namespace CVC4::options; namespace CVC4 { -CVC4_THREADLOCAL(Options*) Options::s_current = NULL; +CVC4_THREAD_LOCAL Options* Options::s_current = NULL; @@ -532,10 +532,10 @@ namespace options { /** Set a given Options* as "current" just for a particular scope. */ class OptionsGuard { - CVC4_THREADLOCAL_TYPE(Options*)* d_field; + Options** d_field; Options* d_old; public: - OptionsGuard(CVC4_THREADLOCAL_TYPE(Options*)* field, Options* opts) : + OptionsGuard(Options** field, Options* opts) : d_field(field), d_old(*field) { *field = opts; diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 6c360cdc9..d5fb87dbc 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -17,6 +17,7 @@ #include "smt/smt_engine_scope.h" +#include "base/tls.h" #include "base/configuration_private.h" #include "base/cvc4_assert.h" #include "base/output.h" @@ -27,7 +28,7 @@ namespace CVC4 { namespace smt { -CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL; +CVC4_THREAD_LOCAL SmtEngine* s_smtEngine_current = NULL; SmtEngine* currentSmtEngine() { Assert(s_smtEngine_current != NULL); diff --git a/src/smt_util/node_visitor.h b/src/smt_util/node_visitor.h index 8c02af82d..ffd05c83f 100644 --- a/src/smt_util/node_visitor.h +++ b/src/smt_util/node_visitor.h @@ -20,6 +20,7 @@ #include +#include "base/tls.h" #include "expr/node.h" namespace CVC4 { @@ -32,7 +33,7 @@ template class NodeVisitor { /** For re-entry checking */ - static CVC4_THREADLOCAL(bool) s_inRun; + static CVC4_THREAD_LOCAL bool s_inRun; /** * Guard against NodeVisitor<> being re-entrant. @@ -73,7 +74,7 @@ public: */ static typename Visitor::return_type run(Visitor& visitor, TNode node) { - GuardReentry guard(s_inRun); + GuardReentry guard(s_inRun); // Notify of a start visitor.start(node); @@ -115,6 +116,6 @@ public: };/* class NodeVisitor<> */ template -CVC4_THREADLOCAL(bool) NodeVisitor::s_inRun = false; +CVC4_THREAD_LOCAL bool NodeVisitor::s_inRun = false; }/* CVC4 namespace */ diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index a40db89a7..ccab94221 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -17,6 +17,7 @@ #include "theory/arith/dual_simplex.h" #include "base/output.h" +#include "base/tls.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" @@ -62,7 +63,7 @@ DualSimplexDecisionProcedure::Statistics::~Statistics(){ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ Assert(d_conflictVariables.empty()); - static CVC4_THREADLOCAL(unsigned int) instance = 0; + static CVC4_THREAD_LOCAL unsigned int instance = 0; instance = instance + 1; d_pivots = 0; diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 59bb35293..db40f3580 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -17,6 +17,7 @@ #include "theory/arith/fc_simplex.h" #include "base/output.h" +#include "base/tls.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" @@ -91,7 +92,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ Assert(d_sgnDisagreements.empty()); d_pivots = 0; - static CVC4_THREADLOCAL(unsigned int) instance = 0; + static CVC4_THREAD_LOCAL unsigned int instance = 0; instance = instance + 1; static const bool verbose = false; diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index b2f7b08b5..60c7ed56f 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -19,6 +19,7 @@ #include #include "base/output.h" +#include "base/tls.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" @@ -103,7 +104,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ Assert(d_sgnDisagreements.empty()); d_pivots = 0; - static CVC4_THREADLOCAL(unsigned int) instance = 0; + static CVC4_THREAD_LOCAL unsigned int instance = 0; instance = instance + 1; static const bool verbose = false; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index ab5a19858..a3e2d8ee4 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -24,6 +24,7 @@ #include #include "base/output.h" +#include "base/tls.h" #include "context/cdhashset.h" #include "context/cdinsert_hashmap.h" #include "context/cdlist.h" @@ -56,12 +57,12 @@ #include "theory/arith/linear_equality.h" #include "theory/arith/matrix.h" #include "theory/arith/matrix.h" +#include "theory/arith/nonlinear_extension.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "theory/arith/partial_model.h" #include "theory/arith/simplex.h" #include "theory/arith/theory_arith.h" -#include "theory/arith/nonlinear_extension.h" #include "theory/ite_utilities.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/rewriter.h" @@ -4389,7 +4390,7 @@ void TheoryArithPrivate::presolve(){ if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } - static CVC4_THREADLOCAL(unsigned) callCount = 0; + static CVC4_THREAD_LOCAL unsigned callCount = 0; if(Debug.isOn("arith::presolve")) { Debug("arith::presolve") << "TheoryArithPrivate::presolve #" << callCount << endl; callCount = callCount + 1; diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 0c20c48a4..fe58f658d 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -35,7 +35,7 @@ static TheoryId theoryOf(TNode node) { } #ifdef CVC4_ASSERTIONS -static CVC4_THREADLOCAL(std::unordered_set*) s_rewriteStack = NULL; +static CVC4_THREAD_LOCAL std::unordered_set* s_rewriteStack = NULL; #endif /* CVC4_ASSERTIONS */ class RewriterInitializer { -- 2.30.2