From 73760b3c213733fc98d67f9ceeb74d06b01a3777 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 18 Dec 2012 15:33:43 -0500 Subject: Add win32 support (merge from mdeters/win32, with some cleanup). --- src/include/cvc4_public.h | 14 +---------- src/lib/Makefile.am | 7 ++++-- src/lib/clock_gettime.c | 23 +++++++++++------ src/lib/clock_gettime.h | 6 +++++ src/lib/ffs.c | 40 +++++++++++++++++++++++++++++ src/lib/ffs.h | 42 +++++++++++++++++++++++++++++++ src/lib/strtok_r.c | 41 ++++++++++++++++++++++++++++++ src/lib/strtok_r.h | 42 +++++++++++++++++++++++++++++++ src/main/util.cpp | 20 ++++++++++++--- src/parser/memory_mapped_input_buffer.cpp | 17 ++++++++++++- src/smt/options_handlers.h | 1 + src/theory/theory.h | 1 + src/util/statistics_registry.cpp | 8 +++++- src/util/statistics_registry.h | 22 +++++++++++++++- 14 files changed, 255 insertions(+), 29 deletions(-) create mode 100644 src/lib/ffs.c create mode 100644 src/lib/ffs.h create mode 100644 src/lib/strtok_r.c create mode 100644 src/lib/strtok_r.h (limited to 'src') diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index 6c546a147..9993e5f18 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -22,19 +22,7 @@ #include #if defined _WIN32 || defined __CYGWIN__ -# ifdef BUILDING_DLL -# ifdef __GNUC__ -# define CVC4_PUBLIC __attribute__((__dllexport__)) -# else /* ! __GNUC__ */ -# define CVC4_PUBLIC __declspec(dllexport) -# endif /* __GNUC__ */ -# else /* BUILDING_DLL */ -# ifdef __GNUC__ -# define CVC4_PUBLIC __attribute__((__dllimport__)) -# else /* ! __GNUC__ */ -# define CVC4_PUBLIC __declspec(dllimport) -# endif /* __GNUC__ */ -# endif /* BUILDING_DLL */ +# define CVC4_PUBLIC #else /* !( defined _WIN32 || defined __CYGWIN__ ) */ # if __GNUC__ >= 4 # define CVC4_PUBLIC __attribute__ ((__visibility__("default"))) diff --git a/src/lib/Makefile.am b/src/lib/Makefile.am index a6ea59e95..61f9e2d70 100644 --- a/src/lib/Makefile.am +++ b/src/lib/Makefile.am @@ -15,5 +15,8 @@ libreplacements_la_LIBADD = \ EXTRA_DIST = \ replacements.h \ clock_gettime.c \ - clock_gettime.h - + clock_gettime.h \ + strtok_r.c \ + strtok_r.h \ + ffs.c \ + ffs.h diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c index 77409c71a..e9d347438 100644 --- a/src/lib/clock_gettime.c +++ b/src/lib/clock_gettime.c @@ -18,20 +18,20 @@ #include "cvc4_private.h" -#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__ */ +#if !(defined(__APPLE__) || defined(__WIN32__)) +# warning "This code assumes you're on Mac OS X or Win32, and you don't seem to be. You'll likely have problems." +#endif /* !(__APPLE__ || __WIN32__) */ +#ifdef __APPLE__ + +#include +#include #include static double s_clockconv = 0.0; @@ -64,6 +64,15 @@ long clock_gettime(clockid_t which_clock, struct timespec *tp) { return 0; } +#else /* else we're __WIN32__ */ + +long clock_gettime(clockid_t which_clock, struct timespec *tp) { + // unsupported on Windows + return 0; +} + +#endif /* __APPLE__ / __WIN32__ */ + #ifdef __cplusplus }/* extern "C" */ #endif /* __cplusplus */ diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h index ac4ca1f85..ea14f885c 100644 --- a/src/lib/clock_gettime.h +++ b/src/lib/clock_gettime.h @@ -30,13 +30,19 @@ /* otherwise, we have to define it */ +#ifndef __WIN32__ + /* get timespec from */ #include +#endif /* ! __WIN32__ */ + #ifdef __cplusplus extern "C" { #endif /* __cplusplus */ +struct timespec; + typedef enum { CLOCK_REALTIME, CLOCK_MONOTONIC, diff --git a/src/lib/ffs.c b/src/lib/ffs.c new file mode 100644 index 000000000..5c25211ce --- /dev/null +++ b/src/lib/ffs.c @@ -0,0 +1,40 @@ +/********************* */ +/*! \file ffs.c + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Replacement for ffs() for systems without it (like Win32) + ** + ** Replacement for ffs() for systems without it (like Win32). + **/ + +#include "cvc4_private.h" + +#include "lib/ffs.h" + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +int ffs(int i) { + long mask = 0x1; + int pos = 1; + while(pos <= sizeof(int) * 8) { + if((mask & i) != 0) { + return pos; + } + ++pos; + mask <<= 1; + } + return 0; +} + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ diff --git a/src/lib/ffs.h b/src/lib/ffs.h new file mode 100644 index 000000000..9b038d429 --- /dev/null +++ b/src/lib/ffs.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file ffs.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Replacement for ffs() for systems without it (like Win32) + ** + ** Replacement for ffs() for systems without it (like Win32). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LIB__FFS_H +#define __CVC4__LIB__FFS_H + +#ifdef HAVE_FFS + +// available in strings.h +#include + +#else /* ! HAVE_FFS */ + +#include "lib/replacements.h" + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +int ffs(int i); + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ + +#endif /* HAVE_FFS */ +#endif /* __CVC4__LIB__FFS_H */ diff --git a/src/lib/strtok_r.c b/src/lib/strtok_r.c new file mode 100644 index 000000000..b8df95359 --- /dev/null +++ b/src/lib/strtok_r.c @@ -0,0 +1,41 @@ +/********************* */ +/*! \file strtok_r.c + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Replacement for strtok_r() for systems without it (like Win32) + ** + ** Replacement for strtok_r() for systems without it (like Win32). + **/ + +#include "cvc4_private.h" + +#include "lib/strtok_r.h" +#include +#include + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +char* strtok_r(char *str, const char *delim, char **saveptr) { + if(str == NULL) { + char* retval = strtok(*saveptr, delim); + *saveptr = retval + strlen(retval) + 1; + return retval; + } else { + char* retval = strtok(str, delim); + *saveptr = retval + strlen(retval) + 1; + return retval; + } +} + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ diff --git a/src/lib/strtok_r.h b/src/lib/strtok_r.h new file mode 100644 index 000000000..6b3387e6b --- /dev/null +++ b/src/lib/strtok_r.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file strtok_r.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Replacement for strtok_r() for systems without it (like Win32) + ** + ** Replacement for strtok_r() for systems without it (like Win32). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LIB__STRTOK_R_H +#define __CVC4__LIB__STRTOK_R_H + +#ifdef HAVE_STRTOK_R + +// available in string.h +#include + +#else /* ! HAVE_STRTOK_R */ + +#include "lib/replacements.h" + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +char* strtok_r(char *str, const char *delim, char **saveptr); + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ + +#endif /* HAVE_STRTOK_R */ +#endif /* __CVC4__LIB__STRTOK_R_H */ diff --git a/src/main/util.cpp b/src/main/util.cpp index 5e7436580..9ade23630 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -19,10 +19,15 @@ #include #include #include + +#ifndef __WIN32__ + #include #include #include +#endif /* __WIN32__ */ + #include "util/exception.h" #include "options/options.h" #include "util/statistics.h" @@ -44,9 +49,6 @@ namespace CVC4 { namespace main { -size_t cvc4StackSize; -void* cvc4StackBase; - /** * If true, will not spin on segfault even when CVC4_DEBUG is on. * Useful for nightly regressions, noninteractive performance runs @@ -54,6 +56,11 @@ void* cvc4StackBase; */ bool segvNoSpin = false; +#ifndef __WIN32__ + +size_t cvc4StackSize; +void* cvc4StackBase; + /** Handler for SIGXCPU, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by timeout.\n"); @@ -144,10 +151,12 @@ void ill_handler(int sig, siginfo_t* info, void*) { #endif /* CVC4_DEBUG */ } +#endif /* __WIN32__ */ + static terminate_handler default_terminator; void cvc4unexpected() { -#ifdef CVC4_DEBUG +#if defined(CVC4_DEBUG) && !defined(__WIN32__) fprintf(stderr, "\n" "CVC4 threw an \"unexpected\" exception (one that wasn't properly " "specified\nin the throws() specifier for the throwing function)." @@ -204,6 +213,7 @@ void cvc4terminate() { /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(Exception) { +#ifndef __WIN32__ stack_t ss; ss.ss_sp = malloc(SIGSTKSZ); if(ss.ss_sp == NULL) { @@ -262,6 +272,8 @@ void cvc4_init() throw(Exception) { throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno)); } +#endif /* __WIN32__ */ + set_unexpected(cvc4unexpected); default_terminator = set_terminate(cvc4terminate); } diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index 9f72ac51c..f110b1145 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -18,10 +18,15 @@ #include #include +#include + +#ifndef _WIN32 + #include #include #include -#include + +#endif /* _WIN32 */ #include "parser/memory_mapped_input_buffer.h" #include "util/exception.h" @@ -31,6 +36,14 @@ namespace parser { extern "C" { +#ifdef _WIN32 + +pANTLR3_INPUT_STREAM MemoryMappedInputBufferNew(const std::string& filename) { + return 0; +} + +#else /* ! _WIN32 */ + static ANTLR3_UINT32 MemoryMapFile(pANTLR3_INPUT_STREAM input, const std::string& filename); @@ -112,6 +125,8 @@ void UnmapFile(pANTLR3_INPUT_STREAM input) { input->close(input); } +#endif /* _WIN32 */ + }/* extern "C" */ }/* CVC4::parser namespace */ diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index a3065f29b..a0a6429a8 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -23,6 +23,7 @@ #include "util/dump.h" #include "smt/modal_exception.h" #include "smt/smt_engine.h" +#include "lib/strtok_r.h" #include #include diff --git a/src/theory/theory.h b/src/theory/theory.h index f317d4b92..e76441f6b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -33,6 +33,7 @@ #include "options/options.h" #include "util/statistics_registry.h" #include "util/dump.h" +#include "lib/ffs.h" #include #include diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index b86b557e2..8f9f05031 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -17,7 +17,9 @@ #include "util/statistics_registry.h" #include "expr/expr_manager.h" -#include "lib/clock_gettime.h" +#ifndef __WIN32__ +# include "lib/clock_gettime.h" +#endif /* ! __WIN32__ */ #include "smt/smt_engine.h" #ifndef __BUILDING_STATISTICS_FOR_EXPORT @@ -102,14 +104,17 @@ 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; @@ -117,6 +122,7 @@ 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 3bf990dbb..0a5450b8a 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -612,6 +612,8 @@ public: };/* class StatisticsRegistry */ +#ifndef __WIN32__ + /****************************************************************************/ /* Some utility functions for timespec */ /****************************************************************************/ @@ -765,6 +767,25 @@ 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 @@ -788,7 +809,6 @@ public: } };/* class CodeTimer */ - /** * To use a statistic, you need to declare it, initialize it in your * constructor, register it in your constructor, and deregister it in -- cgit v1.2.3