Fixes for Win32 (closes bugs 488 and 489)

* timer statistics now supported (closes bug 488)
* use of --mmap doesn't crash anymore (closes bug 489)

diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c
index e9d3474384fcbdc55b8ef135153e24522fdf0ac4..054a8c1122d4f3490619c9b5cbdde341179991ce 100644 (file)
--- a/src/lib/clock_gettime.c
+++ b/src/lib/clock_gettime.c
@@ -36,7 +36,7 @@ extern "C" {
 
 static double s_clockconv = 0.0;
 
-long clock_gettime(clockid_t which_clock, struct timespec *tp) {
+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);
@@ -66,8 +66,17 @@ long clock_gettime(clockid_t which_clock, struct timespec *tp) {
 
 #else /* else we're __WIN32__ */
 
-long clock_gettime(clockid_t which_clock, struct timespec *tp) {
-  // unsupported on Windows
+#include <time.h>
+#include <windows.h>
+
+long clock_gettime(clockid_t which_clock, struct timespec* tp) {
+  if(tp != NULL) {
+    FILETIME ft;
+    GetSystemTimeAsFileTime(&ft);
+    uint64_t nanos = ((((uint64_t)ft.dwHighDateTime) << 32) | ft.dwLowDateTime) * 100;
+    tp->tv_sec = nanos / 1000000000ul;
+    tp->tv_nsec = nanos % 1000000000ul;
+  }
   return 0;
 }
 

diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h
index ea14f885c708df2c7e749b5d3a67b334a1798ba0..6a8dd57ff9d4d535f1ddc5ae54d9db9c26d64e3b 100644 (file)
--- a/src/lib/clock_gettime.h
+++ b/src/lib/clock_gettime.h
@@ -30,12 +30,27 @@
 
 /* otherwise, we have to define it */
 
-#ifndef __WIN32__
+#ifdef __WIN32__
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+struct timespec {
+  uint64_t tv_sec;
+  int32_t tv_nsec;
+};/* struct timespec */
+
+#ifdef __cplusplus
+}/* extern "C" */
+#endif /* __cplusplus */
+
+#else /* ! __WIN32__ */
 
 /* get timespec from <time.h> */
 #include <time.h>
 
-#endif /* ! __WIN32__ */
+#endif /* __WIN32__ */
 
 #ifdef __cplusplus
 extern "C" {
@@ -50,7 +65,7 @@ typedef enum {
   CLOCK_MONOTONIC_HR
 } clockid_t;
 
-long clock_gettime(clockid_t which_clock, struct timespec *tp);
+long clock_gettime(clockid_t which_clock, struct timespec* tp);
 
 #ifdef __cplusplus
 }/* extern "C" */
@@ -58,4 +73,3 @@ long clock_gettime(clockid_t which_clock, struct timespec *tp);
 
 #endif /* HAVE_CLOCK_GETTIME */
 #endif /*__CVC4__LIB__CLOCK_GETTIME_H */
-

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 8987a75722fcf6d7e533d3e002aab75cfef61382..fbf2b86507d975f0dfdd2af3334be2430d705cf1 100644 (file)
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -63,8 +63,13 @@ AntlrInputStream*
 AntlrInputStream::newFileInputStream(const std::string& name,
                                      bool useMmap)
   throw (InputStreamException) {
+#ifdef _WIN32
+  if(useMmap) {
+    useMmap = false;
+  }
+#endif
   pANTLR3_INPUT_STREAM input = NULL;
-  if( useMmap ) {
+  if(useMmap) {
     input = MemoryMappedInputBufferNew(name);
   } else {
     // libantlr3c v3.2 isn't source-compatible with v3.4
@@ -74,7 +79,7 @@ AntlrInputStream::newFileInputStream(const std::string& name,
     input = antlr3FileStreamNew((pANTLR3_UINT8) name.c_str(), ANTLR3_ENC_8BIT);
 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
   }
-  if( input == NULL ) {
+  if(input == NULL) {
     throw InputStreamException("Couldn't open file: " + name);
   }
   return new AntlrInputStream( name, input );

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 8f9f05031c47fe3cb5bf15e1433e01262da67517..b86b557e212481d4c50a8d6244de077ae231bd95 100644 (file)
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -17,9 +17,7 @@
 
 #include "util/statistics_registry.h"
 #include "expr/expr_manager.h"
-#ifndef __WIN32__
-#  include "lib/clock_gettime.h"
-#endif /* ! __WIN32__ */
+#include "lib/clock_gettime.h"
 #include "smt/smt_engine.h"
 
 #ifndef __BUILDING_STATISTICS_FOR_EXPORT
@@ -104,17 +102,14 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const {
 }
 
 void TimerStat::start() {
-#ifndef __WIN32__
   if(__CVC4_USE_STATISTICS) {
     CheckArgument(!d_running, *this, "timer already running");
     clock_gettime(CLOCK_MONOTONIC, &d_start);
     d_running = true;
   }
-#endif /* ! __WIN32__ */
 }/* TimerStat::start() */
 
 void TimerStat::stop() {
-#ifndef __WIN32__
   if(__CVC4_USE_STATISTICS) {
     CheckArgument(d_running, *this, "timer not running");
     ::timespec end;
@@ -122,7 +117,6 @@ void TimerStat::stop() {
     d_data += end - d_start;
     d_running = false;
   }
-#endif /* ! __WIN32__ */
 }/* TimerStat::stop() */
 
 RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 32aa33bed6cc0611f8ded94c29328a64de0fcf1a..474abfea37bddbba1c1e9de15bbc379e4af04833 100644 (file)
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -23,6 +23,7 @@
 
 #include "util/statistics.h"
 #include "util/exception.h"
+#include "lib/clock_gettime.h"
 
 #include <sstream>
 #include <iomanip>
@@ -612,8 +613,6 @@ public:
 
 };/* class StatisticsRegistry */
 
-#ifndef __WIN32__
-
 /****************************************************************************/
 /* Some utility functions for timespec                                    */
 /****************************************************************************/
@@ -769,26 +768,6 @@ public:
 
 };/* class TimerStat */
 
-#else /* __WIN32__ */
-
-class CodeTimer;
-
-class TimerStat : public IntStat {
-public:
-
-  typedef CVC4::CodeTimer CodeTimer;
-
-  TimerStat(const std::string& name) :
-    IntStat(name, 0) {
-  }
-
-  void start();
-  void stop();
-
-};/* class TimerStat */
-
-#endif /* __WIN32__ */
-
 /**
  * Utility class to make it easier to call stop() at the end of a
  * code block.  When constructed, it starts the timer.  When