From 047e75b485ad16a729083c210ba4064943d2e7c5 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 7 Aug 2018 23:24:07 -0700 Subject: [PATCH] Require Swig 3 (#2283) Removes some hacks due to Swig 2's incomplete C++11 support and adds checks for version 3 at configuration time as well as in swig.h --- config/bindings.m4 | 4 +-- src/base/Makefile.am | 3 +-- src/base/cvc4_assert.cpp | 5 ++-- src/base/exception.cpp | 2 +- src/base/exception.h | 4 +-- src/base/tls.h | 31 ----------------------- src/bindings/swig.h | 5 ++-- src/cvc4.i | 8 ------ src/expr/node_manager.cpp | 2 +- src/expr/node_manager.h | 3 +-- src/main/driver_unified.cpp | 3 +-- src/main/interactive_shell.cpp | 5 ++-- src/main/main.h | 3 +-- src/options/options.h | 3 +-- src/options/options_template.cpp | 3 +-- src/smt/smt_engine_scope.cpp | 3 +-- src/smt_util/node_visitor.h | 5 ++-- 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 | 3 +-- src/theory/bv/bitblast/aig_bitblaster.cpp | 2 +- src/theory/bv/bitblast/aig_bitblaster.h | 4 +-- src/theory/bv/theory_bv_rewriter.cpp | 4 +-- src/theory/rewriter.cpp | 2 +- src/util/random.h | 4 +-- 26 files changed, 30 insertions(+), 90 deletions(-) delete mode 100644 src/base/tls.h diff --git a/config/bindings.m4 b/config/bindings.m4 index 5941d81cd..bc7c0e2b8 100644 --- a/config/bindings.m4 +++ b/config/bindings.m4 @@ -58,7 +58,7 @@ else AC_MSG_CHECKING([compatibility with version of swig]) cat > conftest.c << _CVC4EOF %module conftest -#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x020000 +#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x030000 #error bad version #endif _CVC4EOF @@ -66,7 +66,7 @@ _CVC4EOF AC_MSG_RESULT([compatible version]) else AC_MSG_RESULT([incompatible version]) - AC_MSG_WARN([swig version 2.0.0 or later is required to build native API bindings]) + AC_MSG_WARN([swig version 3.0.0 or later is required to build native API bindings]) SWIG= echo '===Failed swig input was:' >&AS_MESSAGE_LOG_FD cat conftest.c >&AS_MESSAGE_LOG_FD diff --git a/src/base/Makefile.am b/src/base/Makefile.am index 7dd6f47e5..3619b226e 100644 --- a/src/base/Makefile.am +++ b/src/base/Makefile.am @@ -28,8 +28,7 @@ libbase_la_SOURCES = \ listener.h \ modal_exception.h \ output.cpp \ - output.h \ - tls.h + output.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 diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp index 1e92670b4..3af6a9909 100644 --- a/src/base/cvc4_assert.cpp +++ b/src/base/cvc4_assert.cpp @@ -20,14 +20,13 @@ #include "base/cvc4_assert.h" #include "base/output.h" -#include "base/tls.h" using namespace std; namespace CVC4 { #ifdef CVC4_DEBUG -//CVC4_THREAD_LOCAL const char* s_debugLastException = NULL; +//thread_local const char* s_debugLastException = NULL; #endif /* CVC4_DEBUG */ @@ -141,7 +140,7 @@ void AssertionException::construct(const char* header, const char* extra, */ void debugAssertionFailed(const AssertionException& thisException, const char* propagatingException) { - static CVC4_THREAD_LOCAL bool alreadyFired = false; + static thread_local bool alreadyFired = false; if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) { throw thisException; diff --git a/src/base/exception.cpp b/src/base/exception.cpp index 0a651f773..831220a2b 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -28,7 +28,7 @@ using namespace std; namespace CVC4 { -CVC4_THREAD_LOCAL LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = NULL; +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 983a59572..54f6aa92d 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -27,8 +27,6 @@ #include #include -#include "base/tls.h" - namespace CVC4 { class CVC4_PUBLIC Exception : public std::exception { @@ -163,7 +161,7 @@ private: char* d_contents; - static CVC4_THREAD_LOCAL LastExceptionBuffer* s_currentBuffer; + static thread_local LastExceptionBuffer* s_currentBuffer; }; /* class LastExceptionBuffer */ }/* CVC4 namespace */ diff --git a/src/base/tls.h b/src/base/tls.h deleted file mode 100644 index d80d66d30..000000000 --- a/src/base/tls.h +++ /dev/null @@ -1,31 +0,0 @@ -/********************* */ -/*! \file tls.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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/bindings/swig.h b/src/bindings/swig.h index 76a64a75f..5316eef12 100644 --- a/src/bindings/swig.h +++ b/src/bindings/swig.h @@ -21,12 +21,11 @@ # error This file should only be included when generating swig interfaces. #endif /* SWIG */ -#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x020000 -# error CVC4 bindings require swig version 2.0.0 or later, sorry. +#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x030000 +# error CVC4 bindings require swig version 3.0.0 or later, sorry. #endif /* SWIG_VERSION */ %import "cvc4_public.h" -%import "base/tls.h" // swig doesn't like GCC attributes #define __attribute__(x) diff --git a/src/cvc4.i b/src/cvc4.i index bc5f5fdfe..c0112c9b0 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -1,11 +1,3 @@ -// We safely ignore some C++11 keywords that older versions of SWIG cannot -// handle. -#if SWIG_VERSION < 0x030000 -%define final %enddef -%define override %enddef -%define noexcept %enddef -#endif - %import "bindings/swig.h" %include "stdint.i" diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 74701cf11..a40d1511b 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -37,7 +37,7 @@ using namespace CVC4::expr; namespace CVC4 { -CVC4_THREAD_LOCAL NodeManager* NodeManager::s_current = NULL; +thread_local NodeManager* NodeManager::s_current = NULL; namespace { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f7f3fb144..8bbf905a9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -32,7 +32,6 @@ #include #include -#include "base/tls.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" @@ -101,7 +100,7 @@ class NodeManager { expr::NodeValueIDHashFunction, expr::NodeValueIDEquality> NodeValueIDSet; - static CVC4_THREAD_LOCAL NodeManager* s_current; + static 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 816b40daa..f97b037eb 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -26,7 +26,6 @@ // 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" @@ -56,7 +55,7 @@ using namespace CVC4::main; namespace CVC4 { namespace main { /** Global options variable */ - CVC4_THREAD_LOCAL Options* pOptions; + thread_local Options* pOptions; /** Full argv[0] */ const char *progPath; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index f1220b961..2cec42fbf 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -37,7 +37,6 @@ # endif /* HAVE_EXT_STDIO_FILEBUF_H */ #endif /* HAVE_LIBREADLINE */ -#include "base/tls.h" #include "base/output.h" #include "options/language.h" #include "options/options.h" @@ -384,8 +383,8 @@ struct StringPrefix2Less { };/* struct StringPrefix2Less */ char* commandGenerator(const char* text, int state) { - static CVC4_THREAD_LOCAL const std::string* rlCommand; - static CVC4_THREAD_LOCAL set::const_iterator* rlDeclaration; + static thread_local const std::string* rlCommand; + static thread_local set::const_iterator* rlDeclaration; const std::string* i = lower_bound(commandsBegin, commandsEnd, text, StringPrefix2Less()); const std::string* j = upper_bound(commandsBegin, commandsEnd, text, StringPrefix1Less()); diff --git a/src/main/main.h b/src/main/main.h index 57c00ffc0..ee5341b87 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -17,7 +17,6 @@ #include #include -#include "base/tls.h" #include "base/exception.h" #include "cvc4autoconfig.h" #include "expr/expr_manager.h" @@ -54,7 +53,7 @@ extern CVC4::TimerStat* pTotalTime; extern bool segvSpin; /** A pointer to the options in play */ -extern CVC4_THREAD_LOCAL Options* pOptions; +extern thread_local Options* pOptions; /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. * This can throw a CVC4::Exception. diff --git a/src/options/options.h b/src/options/options.h index 16210e1a3..474fe3a4b 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -26,7 +26,6 @@ #include "base/listener.h" #include "base/modal_exception.h" -#include "base/tls.h" #include "options/argument_extender.h" #include "options/language.h" #include "options/option_exception.h" @@ -47,7 +46,7 @@ class CVC4_PUBLIC Options { options::OptionsHandler* d_handler; /** The current Options in effect */ - static CVC4_THREAD_LOCAL Options* s_current; + static thread_local Options* s_current; /** Listeners for options::forceLogicString being set. */ ListenerCollection d_forceLogicListeners; diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index d2ccd37ca..609713ce8 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -48,7 +48,6 @@ extern int optreset; #include #include -#include "base/tls.h" #include "base/cvc4_assert.h" #include "base/exception.h" #include "base/output.h" @@ -73,7 +72,7 @@ using namespace CVC4::options; namespace CVC4 { -CVC4_THREAD_LOCAL Options* Options::s_current = NULL; +thread_local Options* Options::s_current = NULL; diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 288a07bde..a4a0967b2 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -17,7 +17,6 @@ #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 +26,7 @@ namespace CVC4 { namespace smt { -CVC4_THREAD_LOCAL SmtEngine* s_smtEngine_current = NULL; +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 0517e9d2c..31a436f81 100644 --- a/src/smt_util/node_visitor.h +++ b/src/smt_util/node_visitor.h @@ -20,7 +20,6 @@ #include -#include "base/tls.h" #include "expr/node.h" namespace CVC4 { @@ -33,7 +32,7 @@ template class NodeVisitor { /** For re-entry checking */ - static CVC4_THREAD_LOCAL bool s_inRun; + static thread_local bool s_inRun; /** * Guard against NodeVisitor<> being re-entrant. @@ -116,6 +115,6 @@ public: };/* class NodeVisitor<> */ template -CVC4_THREAD_LOCAL bool NodeVisitor::s_inRun = false; +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 1f855b1dd..c2b95890a 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -17,7 +17,6 @@ #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" @@ -63,7 +62,7 @@ DualSimplexDecisionProcedure::Statistics::~Statistics(){ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ Assert(d_conflictVariables.empty()); - static CVC4_THREAD_LOCAL unsigned int instance = 0; + static 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 198c22e77..07c6b1691 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -17,7 +17,6 @@ #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" @@ -92,7 +91,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ Assert(d_sgnDisagreements.empty()); d_pivots = 0; - static CVC4_THREAD_LOCAL unsigned int instance = 0; + static 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 43ea51384..31301df61 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -19,7 +19,6 @@ #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" @@ -104,7 +103,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ Assert(d_sgnDisagreements.empty()); d_pivots = 0; - static CVC4_THREAD_LOCAL unsigned int instance = 0; + static 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 ad0ce2e86..6db246b8b 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -24,7 +24,6 @@ #include #include "base/output.h" -#include "base/tls.h" #include "context/cdhashset.h" #include "context/cdinsert_hashmap.h" #include "context/cdlist.h" @@ -4400,7 +4399,7 @@ void TheoryArithPrivate::presolve(){ if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } - static CVC4_THREAD_LOCAL unsigned callCount = 0; + static 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/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index f2417deb6..b06062cf4 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -116,7 +116,7 @@ Abc_Obj_t* mkIte(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) { return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b); } -CVC4_THREAD_LOCAL Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr; +thread_local Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr; Abc_Ntk_t* AigBitblaster::currentAigNtk() { if (!AigBitblaster::s_abcAigNetwork) { diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index bd624bf92..6d21b69e6 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -21,8 +21,6 @@ #include "theory/bv/bitblast/bitblaster.h" -#include "base/tls.h" - class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; @@ -57,7 +55,7 @@ class AigBitblaster : public TBitblaster typedef std::unordered_map TNodeAigMap; typedef std::unordered_map NodeAigMap; - static CVC4_THREAD_LOCAL Abc_Ntk_t* s_abcAigNetwork; + static thread_local Abc_Ntk_t* s_abcAigNetwork; std::unique_ptr d_nullContext; std::unique_ptr d_satSolver; TNodeAigMap d_aigCache; diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 8b5d34cf4..2c9ccf46a 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -30,8 +30,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::bv; -// CVC4_THREAD_LOCAL AllRewriteRules* TheoryBVRewriter::s_allRules = NULL; -// CVC4_THREAD_LOCAL TimerStat* TheoryBVRewriter::d_rewriteTimer = NULL; +// thread_local AllRewriteRules* TheoryBVRewriter::s_allRules = NULL; +// thread_local TimerStat* TheoryBVRewriter::d_rewriteTimer = NULL; RewriteFunction TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; void TheoryBVRewriter::init() { // s_allRules = new AllRewriteRules; diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 6319e1196..58f4832c0 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_THREAD_LOCAL std::unordered_set* s_rewriteStack = NULL; +static thread_local std::unordered_set* s_rewriteStack = NULL; #endif /* CVC4_ASSERTIONS */ class RewriterInitializer { diff --git a/src/util/random.h b/src/util/random.h index 031ef06b7..480271c03 100644 --- a/src/util/random.h +++ b/src/util/random.h @@ -21,8 +21,6 @@ #ifndef __CVC4__UTIL__RANDOM_H #define __CVC4__UTIL__RANDOM_H -#include "base/tls.h" - namespace CVC4 { class Random @@ -33,7 +31,7 @@ class Random /* Get current RNG (singleton). */ static Random& getRandom() { - static CVC4_THREAD_LOCAL Random s_current(0); + static thread_local Random s_current(0); return s_current; } -- 2.30.2