CVC4 contains the pkg.m4 autoconf module by Scott James Remnant.
+CVC4 contains the ax_tls.m4 autoconf module by Alan Woodland and
+Diego Elio Petteno.
+
CVC4 maintainer versions contain the script autogen.sh, by the
U.S. Army Research Laboratory
Copyright (c) 2005-2009 United States Government as represented by
the U.S. Army Research Laboratory.
-
+
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions
are met:
-
+
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
-
+
2. Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials provided
with the distribution.
-
+
3. The name of the author may not be used to endorse or promote
products derived from this software without specific prior written
permission.
-
+
THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS
OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 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, write to the Free Software
Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
-
+
As a special exception to the GNU General Public License, if you
distribute this file as part of a program that contains a
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 <ajw05@aber.ac.uk>
+ Copyright (c) 2010 Diego Elio Pettenò <flameeyes@gmail.com>
+
+ 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 <http://www.gnu.org/licenses/>.
+
+ 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 code from ANTLR3, excluded from the above copyright.
See http://www.antlr.org/, and the files src/parser/bounded_token_buffer.h,
src/parser/bounded_token_buffer.cpp, and src/parser/antlr_input_imports.cpp.
Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC
http://www.temporal-wave.com
http://www.linkedin.com/in/jimidle
-
+
All rights reserved.
-
+
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions
are met:
documentation and/or other materials provided with the distribution.
3. The name of the author may not be used to endorse or promote products
derived from this software without specific prior written permission.
-
+
THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
--- /dev/null
+# ===========================================================================
+# 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 <ajw05@aber.ac.uk>
+# Copyright (c) 2010 Diego Elio Pettenò <flameeyes@gmail.com>
+#
+# 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 <http://www.gnu.org/licenses/>.
+#
+# 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 8
+
+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 <stdlib.h>
+ 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])
+ )
+])
#AC_TYPE_UINT64_T
#AC_TYPE_SIZE_T
+# Check for availability of TLS support (e.g. __thread storage class)
+AC_MSG_CHECKING([whether user wants wants to use compiler-supported TLS])
+AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
+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
+else
+ CVC4_TLS='pthread_getspecific()'
+ CVC4_TLS_SUPPORTED=0
+fi
+AC_SUBST([CVC4_TLS])
+AC_SUBST([CVC4_TLS_SUPPORTED])
+
# Checks for library functions.
# (empty)
m4_esyscmd([find contrib src test -name Makefile.am | sort | sed 's,\.am$,,'])
src/util/rational.h
src/util/integer.h
+ src/util/tls.h
)
AC_OUTPUT
Static libs : $enable_static
Shared libs : $enable_shared
Static binary: $enable_static_binary
+TLS support : $CVC4_TLS
MP library : $mplibrary
(setq c-basic-offset 2)
(c-set-offset 'innamespace 0)
(setq indent-tabs-mode nil))
-(setq auto-mode-alist (cons '("/home/mdeters/cvc4.*/.*\\.\\(cc\\|cpp\\|h\\|hh\\|hpp\\|y\\|yy\\|ypp\\|lex\\|l\\|ll\\|lpp\\)$" . cvc4-c++-editing-mode) auto-mode-alist))
+(setq auto-mode-alist (cons '("/home/mdeters/cvc4.*/.*\\.\\(cc\\|cpp\\|h\\|hh\\|hpp\\|y\\|yy\\|ypp\\|lex\\|l\\|ll\\|lpp\\)\\(\\.in\\)?$" . cvc4-c++-editing-mode) auto-mode-alist))
--- Morgan Deters <mdeters@cs.nyu.edu> Mon, 02 Nov 2009 18:19:22 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 27 Sep 2010 17:35:38 -0400
#include "theory/bv/theory_bv_type_rules.h"
#include "util/Assert.h"
+#include "util/tls.h"
#include <ext/hash_set>
#include <algorithm>
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
#include "expr/node_value.h"
#include "context/context.h"
#include "util/configuration_private.h"
+#include "util/tls.h"
namespace CVC4 {
expr::NodeValueIDHashFunction,
expr::NodeValueEq> ZombieSet;
- static __thread NodeManager* s_current;
+ static CVC4_THREADLOCAL(NodeManager*) s_current;
NodeValuePool d_nodeValuePool;
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");
#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,
#include "util/exception.h"
#include "util/output.h"
+#include "util/tls.h"
namespace CVC4 {
#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 */
/**
BUILT_SOURCES = \
rational.h \
- integer.h
+ integer.h \
+ tls.h
if CVC4_CLN_IMP
libutil_la_SOURCES += \
rational_gmp_imp.cpp \
integer_gmp_imp.cpp \
rational.h.in \
- integer.h.in
+ integer.h.in \
+ tls.h.in
}
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 */
static bool isBuiltWithGmp();
static bool isBuiltWithCln();
+
+ static bool isBuiltWithTlsSupport();
};
}/* CVC4 namespace */
** 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;
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\
"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 */
--- /dev/null
+/********************* */
+/*! \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 */
projects / cvc5.git / commitdiff