replacement implementation for clock_gettime() on mac os x, build portability (resolving mac os x issues), code cleanup, fix compiler warnings

13 files changed, 259 insertions, 66 deletions

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 <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
 
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)