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

4 files changed, 179 insertions, 0 deletions

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 */