From 96d1c3daff7efdd2d853864fb820bc7cf413624e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 1 Oct 2010 21:35:31 +0000 Subject: [PATCH] replacement implementation for clock_gettime() on mac os x, build portability (resolving mac os x issues), code cleanup, fix compiler warnings --- config/cvc4.m4 | 19 ++++++----- configure.ac | 12 ++++--- src/Makefile.am | 7 ++-- src/include/cvc4_public.h | 4 +-- src/lib/Makefile.am | 19 +++++++++++ src/lib/clock_gettime.c | 69 +++++++++++++++++++++++++++++++++++++++ src/lib/clock_gettime.h | 55 +++++++++++++++++++++++++++++++ src/lib/replacements.h | 36 ++++++++++++++++++++ src/main/Makefile.am | 4 ++- src/main/util.cpp | 37 +++++++++++++++++++-- src/parser/Makefile.am | 20 ++++++------ src/util/stats.h | 32 +----------------- test/unit/Makefile.am | 11 +++++-- 13 files changed, 259 insertions(+), 66 deletions(-) create mode 100644 src/lib/Makefile.am create mode 100644 src/lib/clock_gettime.c create mode 100644 src/lib/clock_gettime.h create mode 100644 src/lib/replacements.h diff --git a/config/cvc4.m4 b/config/cvc4.m4 index ea7d77223..718cdadd3 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -19,34 +19,35 @@ do case $ac_option in -*|*=*) ;; production|production-*|debug|debug-*|default|default-*|competition|competition-*) - ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\?'` + # regexp `\?' not supported on Mac OS X + ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'` ac_cvc4_build_profile_set=yes AC_MSG_NOTICE([CVC4: building profile $ac_option_build]) for x in optimized statistics assertions tracing muzzle coverage profiling; do - if expr "$ac_option" : '.*-no'$x'-\|.*-no'$x'$' >/dev/null; then + if expr "$ac_option" : '.*-no'$x'-\{0,1\}$' >/dev/null; then eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-$x\""' fi - if expr "$ac_option" : '.*-'$x'-\|.*-'$x'$' >/dev/null; then + if expr "$ac_option" : '.*-'$x'-\{0,1\}$' >/dev/null; then eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-$x\""' fi done - if expr "$ac_option" : '.*-nostaticbinary-\|.*-nostaticbinary$' >/dev/null; then + if expr "$ac_option" : '.*-nostaticbinary-\{0,1\}$' >/dev/null; then eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-static-binary\""' fi - if expr "$ac_option" : '.*-staticbinary-\|.*-staticbinary$' >/dev/null; then + if expr "$ac_option" : '.*-staticbinary-\{0,1\}$' >/dev/null; then eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-static-binary\""' fi - if expr "$ac_option" : '.*-nodebugsymbols-\|.*-nodebugsymbols$' >/dev/null; then + if expr "$ac_option" : '.*-nodebugsymbols-\{0,1\}$' >/dev/null; then eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-debug-symbols\""' fi - if expr "$ac_option" : '.*-debugsymbols-\|.*-debugsymbols$' >/dev/null; then + if expr "$ac_option" : '.*-debugsymbols-\{0,1\}$' >/dev/null; then eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-debug-symbols\""' fi for x in cln gmp; do - if expr "$ac_option" : '.*-no'$x'-\|.*-no'$x'$' >/dev/null; then + if expr "$ac_option" : '.*-no'$x'-\{0,1\}$' >/dev/null; then eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-$x\""' fi - if expr "$ac_option" : '.*-'$x'-\|.*-'$x'$' >/dev/null; then + if expr "$ac_option" : '.*-'$x'-\{0,1\}$' >/dev/null; then eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--with-$x\""' fi done diff --git a/configure.ac b/configure.ac index f22ae595a..249122d25 100644 --- a/configure.ac +++ b/configure.ac @@ -14,6 +14,7 @@ AC_INIT([cvc4], _CVC4_RELEASE_STRING) AC_CONFIG_SRCDIR([src/include/cvc4_public.h]) AC_CONFIG_AUX_DIR([config]) AC_CONFIG_MACRO_DIR([config]) +AC_CONFIG_LIBOBJ_DIR([src/lib]) m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])]) @@ -639,7 +640,10 @@ fi AC_CHECK_LIB(z, gzread, , [AC_MSG_ERROR([zlib required, install your distro's zlib-dev package or see www.zlib.net])]) AC_CHECK_HEADER(zlib.h, , [AC_MSG_ERROR([zlib required, install your distro's zlib-dev package or see www.zlib.net])]) -AC_CHECK_LIB(rt, clock_gettime, , [AC_MSG_ERROR([can't find clock_gettime() in librt])]) +AC_SEARCH_LIBS([clock_gettime], [rt], + [AC_DEFINE([HAVE_CLOCK_GETTIME], [1], + [Defined to 1 if clock_gettime() is supported by the platform.])], + [AC_LIBOBJ([clock_gettime])]) # Check for antlr C++ runtime (defined in config/antlr.m4) AC_LIB_ANTLR @@ -656,7 +660,7 @@ AC_CHECK_HEADERS([getopt.h unistd.h]) #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_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 -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then AC_MSG_RESULT([yes]) @@ -701,7 +705,7 @@ AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full releas CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS" CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated" -CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions" +CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -fexceptions" LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" AC_SUBST(FLAG_VISIBILITY_HIDDEN) @@ -742,7 +746,7 @@ AC_SUBST(CVC4_USE_GMP_IMP) AC_CONFIG_FILES([ Makefile.builds Makefile] - m4_esyscmd([find contrib src test -name Makefile.am | sort | sed 's,\.am$,,']) + m4_esyscmd([find contrib lib src test -name Makefile.am | sort | sed 's,\.am$,,']) src/util/rational.h src/util/integer.h src/util/tls.h diff --git a/src/Makefile.am b/src/Makefile.am index e436971fa..fb337e204 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -12,12 +12,12 @@ # LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@ -AM_CPPFLAGS = +AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/include -I@srcdir@ -I@builddir@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = expr util context theory prop smt . parser main +SUBDIRS = lib expr util context theory prop smt . parser main lib_LTLIBRARIES = libcvc4.la @@ -40,7 +40,8 @@ libcvc4_noinst_la_LIBADD = \ @builddir@/prop/libprop.la \ @builddir@/prop/minisat/libminisat.la \ @builddir@/smt/libsmt.la \ - @builddir@/theory/libtheory.la + @builddir@/theory/libtheory.la \ + @builddir@/lib/libreplacements.la EXTRA_DIST = \ include/cvc4parser_private.h \ diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index 8375f7571..714c32e29 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -45,8 +45,8 @@ # endif /* __GNUC__ >= 4 */ #endif /* defined _WIN32 || defined __CYGWIN__ */ -#define EXPECT_TRUE(x) __builtin_expect( (x), true) -#define EXPECT_FALSE(x) __builtin_expect( (x), false) +#define EXPECT_TRUE(x) __builtin_expect( (x), true ) +#define EXPECT_FALSE(x) __builtin_expect( (x), false ) #define NORETURN __attribute__ ((noreturn)) #ifndef NULL diff --git a/src/lib/Makefile.am b/src/lib/Makefile.am new file mode 100644 index 000000000..ba0ebdd20 --- /dev/null +++ b/src/lib/Makefile.am @@ -0,0 +1,19 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. +AM_CFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libreplacements.la + +libreplacements_la_SOURCES = empty.c +libreplacements_la_LIBADD = \ + $(LTLIBOBJS) + +EXTRA_DIST = \ + replacements.h \ + clock_gettime.c \ + clock_gettime.h + +# empty.c hack -- need *some* source file so that library make rules are built +empty.c:; touch empty.c diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c new file mode 100644 index 000000000..682269458 --- /dev/null +++ b/src/lib/clock_gettime.c @@ -0,0 +1,69 @@ +/********************* */ +/*! \file clock_gettime.c + ** \verbatim + ** Original author: + ** 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 Replacement for clock_gettime() for systems without it (like + ** Mac OS X) + ** + ** Replacement for clock_gettime() for systems without it (like Mac + ** OS X). + **/ + +#include +#include +#include + +#include "lib/clock_gettime.h" + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +#ifndef __APPLE__ +# warning This code assumes you're on Mac OS X, and you don't seem to be. You'll likely have problems. +#endif /* __APPLE__ */ + +#include + +static double s_clockconv = 0.0; + +long clock_gettime(clockid_t which_clock, struct timespec *tp) { + if( s_clockconv == 0.0 ) { + mach_timebase_info_data_t tb; + kern_return_t err = mach_timebase_info(&tb); + if(err == 0) { + s_clockconv = ((double) tb.numer) / tb.denom; + } else { + return -EINVAL; + } + } + + switch(which_clock) { + case CLOCK_REALTIME: + case CLOCK_REALTIME_HR: + case CLOCK_MONOTONIC: + case CLOCK_MONOTONIC_HR: { + uint64_t t = mach_absolute_time() * s_clockconv; + tp->tv_sec = t / 1000000000ul; + tp->tv_nsec = t % 1000000000ul; + } + break; + default: + return -EINVAL; + } + + return 0; +} + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h new file mode 100644 index 000000000..aac80dadf --- /dev/null +++ b/src/lib/clock_gettime.h @@ -0,0 +1,55 @@ +/********************* */ +/*! \file clock_gettime.h + ** \verbatim + ** Original author: + ** 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 Replacement for clock_gettime() for systems without it (like Mac OS X) + ** + ** Replacement for clock_gettime() for systems without it (like Mac OS X). + **/ + +#ifndef __CVC4__LIB__CLOCK_GETTIME_H +#define __CVC4__LIB__CLOCK_GETTIME_H + +#include "lib/replacements.h" + +#ifdef HAVE_CLOCK_GETTIME + +/* it should be available from */ +#include + +#else /* HAVE_CLOCK_GETTIME */ + +/* otherwise, we have to define it */ + +/* get timespec from */ +#include + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +typedef enum { + CLOCK_REALTIME, + CLOCK_MONOTONIC, + CLOCK_REALTIME_HR, + CLOCK_MONOTONIC_HR +} clockid_t; + +long clock_gettime(clockid_t which_clock, struct timespec *tp); + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ + +#endif /* HAVE_CLOCK_GETTIME */ +#endif /*__CVC4__LIB__CLOCK_GETTIME_H */ + diff --git a/src/lib/replacements.h b/src/lib/replacements.h new file mode 100644 index 000000000..d38331b66 --- /dev/null +++ b/src/lib/replacements.h @@ -0,0 +1,36 @@ +/********************* */ +/*! \file replacements.h + ** \verbatim + ** Original author: + ** 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 Common header for replacement function sources + ** + ** Common header for replacement function sources. + **/ + +#ifndef __CVC4__LIB__REPLACEMENTS_H +#define __CVC4__LIB__REPLACEMENTS_H + +#if defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) +# include "cvc4_private.h" +#else +# if defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) +# include "cvc4parser_private.h" +# else +# if defined(__BUILDING_CVC4DRIVER) +# include "cvc4autoconfig.h" +# else +# error Must be building libcvc4 or libcvc4parser to use replacement functions. This is because replacement function headers should never be publicly-depended upon, as they should not be installed on user machines with 'make install'. +# endif +# endif +#endif + +#endif /* __CVC4__LIB__REPLACEMENTS_H */ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 82ff00a60..3cd062158 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -1,4 +1,5 @@ AM_CPPFLAGS = \ + -D__BUILDING_CVC4DRIVER \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas @@ -13,7 +14,8 @@ cvc4_SOURCES = \ cvc4_LDADD = \ ../parser/libcvc4parser.la \ - ../libcvc4.la + ../libcvc4.la \ + ../lib/libreplacements.la if STATIC_BINARY cvc4_LINK = $(CXXLINK) -all-static diff --git a/src/main/util.cpp b/src/main/util.cpp index ddb9f84c8..e91e80c3f 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -82,6 +82,26 @@ void segv_handler(int sig, siginfo_t* info, void*) { #endif /* CVC4_DEBUG */ } +/** Handler for SIGILL (illegal instruction). */ +void ill_handler(int sig, siginfo_t* info, void*) { +#ifdef CVC4_DEBUG + fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n"); + if(segvNoSpin) { + fprintf(stderr, "No-spin requested, aborting...\n"); + abort(); + } else { + fprintf(stderr, "Spinning so that a debugger can be connected.\n"); + fprintf(stderr, "Try: gdb %s %u\n", progName, getpid()); + for(;;) { + sleep(60); + } + } +#else /* CVC4_DEBUG */ + fprintf(stderr, "CVC4 executed an illegal instruction.\n"); + abort(); +#endif /* CVC4_DEBUG */ +} + static terminate_handler default_terminator; void cvc4unexpected() { @@ -134,22 +154,33 @@ void cvc4_init() throw() { act1.sa_sigaction = sigint_handler; act1.sa_flags = SA_SIGINFO; sigemptyset(&act1.sa_mask); - if(sigaction(SIGINT, &act1, NULL)) + if(sigaction(SIGINT, &act1, NULL)) { throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno)); + } struct sigaction act2; act2.sa_sigaction = timeout_handler; act2.sa_flags = SA_SIGINFO; sigemptyset(&act2.sa_mask); - if(sigaction(SIGXCPU, &act2, NULL)) + if(sigaction(SIGXCPU, &act2, NULL)) { throw Exception(string("sigaction(SIGXCPU) failure: ") + strerror(errno)); + } struct sigaction act3; act3.sa_sigaction = segv_handler; act3.sa_flags = SA_SIGINFO; sigemptyset(&act3.sa_mask); - if(sigaction(SIGSEGV, &act3, NULL)) + if(sigaction(SIGSEGV, &act3, NULL)) { throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); + } + + struct sigaction act4; + act4.sa_sigaction = segv_handler; + act4.sa_flags = SA_SIGINFO; + sigemptyset(&act4.sa_mask); + if(sigaction(SIGILL, &act4, NULL)) { + throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno)); + } set_unexpected(cvc4unexpected); default_terminator = set_terminate(cvc4terminate); diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index b1f265b56..51a833c26 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -30,13 +30,13 @@ libcvc4parser_la_LINK = $(CXXLINK) libcvc4parser_noinst_la_LDFLAGS = $(ANTLR_LDFLAGS) libcvc4parser_noinst_la_LIBADD = \ @builddir@/smt/libparsersmt.la \ - @builddir@/smt2/libparsersmt2.la \ - @builddir@/cvc/libparsercvc.la + @builddir@/smt2/libparsersmt2.la \ + @builddir@/../lib/libreplacements.la libcvc4parser_la_SOURCES = libcvc4parser_noinst_la_SOURCES = \ - antlr_input.h \ - antlr_input.cpp \ + antlr_input.h \ + antlr_input.cpp \ antlr_input_imports.cpp \ bounded_token_buffer.h \ bounded_token_buffer.cpp \ @@ -46,10 +46,10 @@ libcvc4parser_noinst_la_SOURCES = \ input.cpp \ memory_mapped_input_buffer.h \ memory_mapped_input_buffer.cpp \ - parser.h \ - parser.cpp \ - parser_builder.h \ - parser_builder.cpp \ - parser_options.h \ - parser_exception.h + parser.h \ + parser.cpp \ + parser_builder.h \ + parser_builder.cpp \ + parser_options.h \ + parser_exception.h diff --git a/src/util/stats.h b/src/util/stats.h index f8c10c79f..3a1b85506 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -29,6 +29,7 @@ #include #include "util/Assert.h" +#include "lib/clock_gettime.h" namespace CVC4 { @@ -310,36 +311,6 @@ inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) { } -#ifdef __APPLE__ - -class TimerStat : public BackedStat< ::timespec > { - bool d_running; - -public: - - TimerStat(const std::string& s) : - BackedStat< ::timespec >(s, ::timespec()), - d_running(false) { - } - - void start() { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(!d_running); - d_running = true; - } - } - - void stop() { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_running); - ++d_data.tv_sec; - d_running = false; - } - } -};/* class TimerStat */ - -#else /* __APPLE__ */ - class TimerStat : public BackedStat< ::timespec > { // strange: timespec isn't placed in 'std' namespace ?! ::timespec d_start; @@ -371,7 +342,6 @@ public: } };/* class TimerStat */ -#endif /* __APPLE__ */ #undef __CVC4_USE_STATISTICS diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index d5bf66496..059d1d163 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -50,12 +50,17 @@ TEST_DEPS_DIST = \ if HAVE_CXXTESTGEN AM_CPPFLAGS = \ - -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" \ - "-I@top_srcdir@/src" "-I@top_builddir@/src" \ + -I. \ + "-I@CXXTEST@" \ + "-I@top_srcdir@/src/include" \ + "-I@top_srcdir@/lib" \ + "-I@top_srcdir@/src" \ + "-I@top_builddir@/src" \ "-I@top_srcdir@/src/prop/minisat" \ -D __STDC_LIMIT_MACROS \ -D __STDC_FORMAT_MACROS \ - $(ANTLR_INCLUDES) $(TEST_CPPFLAGS) + $(ANTLR_INCLUDES) \ + $(TEST_CPPFLAGS) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS) AM_LDFLAGS = $(TEST_LDFLAGS) -- 2.30.2