diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-01 21:35:31 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-01 21:35:31 +0000 |
commit | 96d1c3daff7efdd2d853864fb820bc7cf413624e (patch) | |
tree | b995c98a2be18182d6cb52e81de5bf712b475f06 /src | |
parent | d0b49d588033ab8140bdf297c9cdf73b1088fe68 (diff) |
replacement implementation for clock_gettime() on mac os x, build portability (resolving mac os x issues), code cleanup, fix compiler warnings
Diffstat (limited to 'src')
-rw-r--r-- | src/Makefile.am | 7 | ||||
-rw-r--r-- | src/include/cvc4_public.h | 4 | ||||
-rw-r--r-- | src/lib/Makefile.am | 19 | ||||
-rw-r--r-- | src/lib/clock_gettime.c | 69 | ||||
-rw-r--r-- | src/lib/clock_gettime.h | 55 | ||||
-rw-r--r-- | src/lib/replacements.h | 36 | ||||
-rw-r--r-- | src/main/Makefile.am | 4 | ||||
-rw-r--r-- | src/main/util.cpp | 37 | ||||
-rw-r--r-- | src/parser/Makefile.am | 20 | ||||
-rw-r--r-- | src/util/stats.h | 32 |
10 files changed, 233 insertions, 50 deletions
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 <stdio.h> +#include <errno.h> +#include <time.h> + +#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 <mach/mach_time.h> + +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 <time.h> */ +#include <time.h> + +#else /* HAVE_CLOCK_GETTIME */ + +/* otherwise, we have to define it */ + +/* get timespec from <time.h> */ +#include <time.h> + +#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 <ctime> #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 |