From b5a6607ceb5ab206e019d1d17f5a1cfca8b7dfc7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Ke=C3=9Fler?= Date: Sat, 28 Sep 2024 14:26:43 +0200 Subject: [PATCH] Fix windows build. --- platform.mk | 2 +- src/comp/.ghci | 1 - src/comp/BluesimLoader.hs | 143 +++++++++++------- src/comp/GHC/posix/TmpNam.hs | 17 ++- src/comp/Makefile | 10 +- src/comp/SimFileUtils.hs | 24 +-- src/comp/bluetcl.hs | 4 +- src/comp/bsc.hs | 2 +- src/vendor/stp/HaskellIfc/STP.hs | 8 +- src/vendor/stp/Makefile | 7 +- src/vendor/stp/src/AST/ASTmisc.cpp | 24 ++- src/vendor/stp/src/Makefile | 5 +- .../stp/src/c_interface/c_interface.cpp | 15 +- src/vendor/stp/src/extlib-abc/aig.h | 11 +- src/vendor/stp/src/main/main.cpp | 4 +- .../stp/src/sat/cryptominisat2/time_mem.h | 47 ++++-- src/vendor/stp/src/sat/mtl/template.mk | 26 ++-- src/vendor/yices/Makefile | 12 +- src/vendor/yices/v2.6/Makefile | 6 +- 19 files changed, 233 insertions(+), 135 deletions(-) diff --git a/platform.mk b/platform.mk index ca38496c3..097ed55e0 100644 --- a/platform.mk +++ b/platform.mk @@ -29,7 +29,7 @@ endif OSTYPE = $(shell $(TOP)/platform.sh ostype) export OSTYPE -ifneq ($(OSTYPE), $(findstring $(OSTYPE), Linux Darwin Freebsd)) +ifneq ($(OSTYPE), $(findstring $(OSTYPE), Linux Darwin Freebsd MSYS Mingw)) $(error OSTYPE environment not recognized: $(OSTYPE)) endif diff --git a/src/comp/.ghci b/src/comp/.ghci index c8edd0a8f..8355eeb3f 100644 --- a/src/comp/.ghci +++ b/src/comp/.ghci @@ -7,7 +7,6 @@ :set -package containers :set -package array :set -package mtl -:set -package unix :set -package regex-compat :set -package bytestring :set -package directory diff --git a/src/comp/BluesimLoader.hs b/src/comp/BluesimLoader.hs index c282ee956..d853d4e35 100644 --- a/src/comp/BluesimLoader.hs +++ b/src/comp/BluesimLoader.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE ForeignFunctionInterface, ScopedTypeVariables, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-} +{-# LANGUAGE ForeignFunctionInterface, ScopedTypeVariables, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances, CPP #-} module BluesimLoader ( BluesimModel(..) , loadBluesimModel , unloadBluesimModel @@ -23,8 +23,12 @@ import FileNameUtil(dirName,baseName) import ErrorUtil(internalError) import HTcl import SimCCBlock(pfxModel) - +#if !defined(windows_HOST_OS) && !defined(mingw32_HOST_OS) import System.Posix.DynamicLinker +#else +import System.Win32.DLL +import System.Win32.Types +#endif import Data.Bits import Data.List(intercalate, isPrefixOf) import Data.Int @@ -379,8 +383,14 @@ foreign import ccall "dynamic" -- normal Haskell types, so that it presents an abstract Haskell view -- of the Bluesim model. +#ifdef mingw32_HOST_OS +type DLType = HINSTANCE +#else +type DLType = DL +#endif + data BluesimModel = - BS { model_so :: DL + BS { model_so :: DLType , model_hdl :: WordPtr , sim_hdl :: WordPtr , current_clock :: BSClock @@ -435,6 +445,37 @@ data BluesimModel = , bk_shutdown :: IO () } +#if defined(windows_HOST_OS) || defined(mingw32_HOST_OS) +openSharedObject :: String -> IO DLType +openSharedObject fname = do + loadLibrary fname +#else +openSharedObject :: String -> IO DLType +openSharedObject fname = do + dlopen fname [RTLD_NOW] +#endif + +#if defined(windows_HOST_OS) || defined(mingw32_HOST_OS) +loadSymbol :: DLType -> String -> IO (FunPtr a) +loadSymbol dl sym = do + ptr <- getProcAddress dl sym + return (castPtrToFunPtr ptr) +#else +loadSymbol :: DLType -> String -> IO (FunPtr a) +loadSymbol dl sym = do + dlsym dl sym +#endif + +#if defined(windows_HOST_OS) || defined(mingw32_HOST_OS) +closeShared :: DLType -> IO () +closeShared dl = do + freeLibrary dl +#else +closeShared :: DLType -> IO () +closeShared dl = do + dlclose dl +#endif + -- Routine which dynamically loads a Bluesim .so file and creates -- a BluesimModel value which allows access to the Bluesim object. -- Returns Nothing if an error occurs during loading @@ -443,54 +484,54 @@ loadBluesimModel :: String -> String -> IO (Maybe BluesimModel) loadBluesimModel fname top_name = do -- load the shared object let fname' = (dirName fname) ++ "/" ++ (baseName fname) - dl <- dlopen fname' [RTLD_NOW] + dl <- openSharedObject fname' -- lookup symbols in the shared object - c_new_model <- dlsym dl ("new_" ++ pfxModel ++ top_name) - c_bk_init <- dlsym dl "bk_init" - c_bk_now <- dlsym dl "bk_now" - c_bk_set_timescale <- dlsym dl "bk_set_timescale" - c_bk_version <- dlsym dl "bk_version" - c_bk_append_argument <- dlsym dl "bk_append_argument" - c_bk_define_clock <- dlsym dl "bk_define_clock" - c_bk_num_clocks <- dlsym dl "bk_num_clocks" - c_bk_get_nth_clock <- dlsym dl "bk_get_nth_clock" - c_bk_clock_name <- dlsym dl "bk_clock_name" - c_bk_get_clock_by_name <- dlsym dl "bk_get_clock_by_name" - c_bk_clock_initial_value <- dlsym dl "bk_clock_initial_value" - c_bk_clock_first_edge <- dlsym dl "bk_clock_first_edge" - c_bk_clock_duration <- dlsym dl "bk_clock_duration" - c_bk_clock_val <- dlsym dl "bk_clock_val" - c_bk_clock_cycle_count <- dlsym dl "bk_clock_cycle_count" - c_bk_clock_edge_count <- dlsym dl "bk_clock_edge_count" - c_bk_clock_last_edge <- dlsym dl "bk_clock_last_edge" - c_bk_quit_after_edge <- dlsym dl "bk_quit_after_edge" - c_bk_schedule_ui_event <- dlsym dl "bk_schedule_ui_event" - c_bk_remove_ui_event <- dlsym dl "bk_remove_ui_event" - c_bk_set_interactive <- dlsym dl "bk_set_interactive" - c_bk_advance <- dlsym dl "bk_advance" - c_bk_is_running <- dlsym dl "bk_is_running" - c_bk_sync <- dlsym dl "bk_sync" - c_bk_abort_now <- dlsym dl "bk_abort_now" - c_bk_finished <- dlsym dl "bk_finished" - c_bk_exit_status <- dlsym dl "bk_exit_status" - c_bk_top_symbol <- dlsym dl "bk_top_symbol" - c_bk_lookup_symbol <- dlsym dl "bk_lookup_symbol" - c_bk_get_size <- dlsym dl "bk_get_size" - c_bk_get_key <- dlsym dl "bk_get_key" - c_bk_is_module <- dlsym dl "bk_is_module" - c_bk_is_rule <- dlsym dl "bk_is_rule" - c_bk_is_single_value <- dlsym dl "bk_is_single_value" - c_bk_is_value_range <- dlsym dl "bk_is_value_range" - c_bk_peek_symbol_value <- dlsym dl "bk_peek_symbol_value" - c_bk_get_range_min_addr <- dlsym dl "bk_get_range_min_addr" - c_bk_get_range_max_addr <- dlsym dl "bk_get_range_max_addr" - c_bk_peek_range_value <- dlsym dl "bk_peek_range_value" - c_bk_num_symbols <- dlsym dl "bk_num_symbols" - c_bk_get_nth_symbol <- dlsym dl "bk_get_nth_symbol" - c_bk_set_VCD_file <- dlsym dl "bk_set_VCD_file" - c_bk_enable_VCD_dumping <- dlsym dl "bk_enable_VCD_dumping" - c_bk_disable_VCD_dumping <- dlsym dl "bk_disable_VCD_dumping" - c_bk_shutdown <- dlsym dl "bk_shutdown" + c_new_model <- loadSymbol dl ("new_" ++ pfxModel ++ top_name) + c_bk_init <- loadSymbol dl "bk_init" + c_bk_now <- loadSymbol dl "bk_now" + c_bk_set_timescale <- loadSymbol dl "bk_set_timescale" + c_bk_version <- loadSymbol dl "bk_version" + c_bk_append_argument <- loadSymbol dl "bk_append_argument" + c_bk_define_clock <- loadSymbol dl "bk_define_clock" + c_bk_num_clocks <- loadSymbol dl "bk_num_clocks" + c_bk_get_nth_clock <- loadSymbol dl "bk_get_nth_clock" + c_bk_clock_name <- loadSymbol dl "bk_clock_name" + c_bk_get_clock_by_name <- loadSymbol dl "bk_get_clock_by_name" + c_bk_clock_initial_value <- loadSymbol dl "bk_clock_initial_value" + c_bk_clock_first_edge <- loadSymbol dl "bk_clock_first_edge" + c_bk_clock_duration <- loadSymbol dl "bk_clock_duration" + c_bk_clock_val <- loadSymbol dl "bk_clock_val" + c_bk_clock_cycle_count <- loadSymbol dl "bk_clock_cycle_count" + c_bk_clock_edge_count <- loadSymbol dl "bk_clock_edge_count" + c_bk_clock_last_edge <- loadSymbol dl "bk_clock_last_edge" + c_bk_quit_after_edge <- loadSymbol dl "bk_quit_after_edge" + c_bk_schedule_ui_event <- loadSymbol dl "bk_schedule_ui_event" + c_bk_remove_ui_event <- loadSymbol dl "bk_remove_ui_event" + c_bk_set_interactive <- loadSymbol dl "bk_set_interactive" + c_bk_advance <- loadSymbol dl "bk_advance" + c_bk_is_running <- loadSymbol dl "bk_is_running" + c_bk_sync <- loadSymbol dl "bk_sync" + c_bk_abort_now <- loadSymbol dl "bk_abort_now" + c_bk_finished <- loadSymbol dl "bk_finished" + c_bk_exit_status <- loadSymbol dl "bk_exit_status" + c_bk_top_symbol <- loadSymbol dl "bk_top_symbol" + c_bk_lookup_symbol <- loadSymbol dl "bk_lookup_symbol" + c_bk_get_size <- loadSymbol dl "bk_get_size" + c_bk_get_key <- loadSymbol dl "bk_get_key" + c_bk_is_module <- loadSymbol dl "bk_is_module" + c_bk_is_rule <- loadSymbol dl "bk_is_rule" + c_bk_is_single_value <- loadSymbol dl "bk_is_single_value" + c_bk_is_value_range <- loadSymbol dl "bk_is_value_range" + c_bk_peek_symbol_value <- loadSymbol dl "bk_peek_symbol_value" + c_bk_get_range_min_addr <- loadSymbol dl "bk_get_range_min_addr" + c_bk_get_range_max_addr <- loadSymbol dl "bk_get_range_max_addr" + c_bk_peek_range_value <- loadSymbol dl "bk_peek_range_value" + c_bk_num_symbols <- loadSymbol dl "bk_num_symbols" + c_bk_get_nth_symbol <- loadSymbol dl "bk_get_nth_symbol" + c_bk_set_VCD_file <- loadSymbol dl "bk_set_VCD_file" + c_bk_enable_VCD_dumping <- loadSymbol dl "bk_enable_VCD_dumping" + c_bk_disable_VCD_dumping <- loadSymbol dl "bk_disable_VCD_dumping" + c_bk_shutdown <- loadSymbol dl "bk_shutdown" -- convert functions to Haskell types and build BluesimModel let new_model :: IO WordPtr new_model = fromC $ dl_ret_ptr c_new_model @@ -624,7 +665,7 @@ loadBluesimModel fname top_name = do unloadBluesimModel :: BluesimModel -> IO () unloadBluesimModel bs = do bk_shutdown bs - dlclose (model_so bs) + closeShared (model_so bs) -- fields are: clock handle, currently active, name, initial value, -- first edge, low duration, high_duration, cycles elapsed, diff --git a/src/comp/GHC/posix/TmpNam.hs b/src/comp/GHC/posix/TmpNam.hs index f2b799a14..75c70f1ee 100644 --- a/src/comp/GHC/posix/TmpNam.hs +++ b/src/comp/GHC/posix/TmpNam.hs @@ -1,12 +1,17 @@ -module TmpNam(tmpNam, localTmpNam) where -import System.Posix +{-# LANGUAGE CPP #-} + +module TmpNam (tmpNam, localTmpNam) where + +import System.Directory (getTemporaryDirectory) +import System.Process (getCurrentPid) tmpNam :: IO String tmpNam = do - x <- localTmpNam - return $ "/tmp/bsc" ++ x + tmpDir <- getTemporaryDirectory -- Cross-platform temporary directory + x <- localTmpNam + return $ tmpDir ++ "/bsc" ++ x localTmpNam :: IO String localTmpNam = do - x <- getProcessID - return $ show x + x <- getCurrentPid + return $ show x \ No newline at end of file diff --git a/src/comp/Makefile b/src/comp/Makefile index ac57e3e55..05dbd0173 100644 --- a/src/comp/Makefile +++ b/src/comp/Makefile @@ -3,7 +3,7 @@ WANT_TCL=yes include $(TOP)/platform.mk -TMPDIR=/tmp +TMPDIR=./tmp # ----- # System tools @@ -127,7 +127,6 @@ PACKAGES = \ -package containers \ -package array \ -package mtl \ - -package unix \ -package regex-compat \ -package bytestring \ -package directory \ @@ -140,8 +139,13 @@ PACKAGES = \ -package syb \ -package integer-gmp \ -package text \ + -package signal \ $(GHCEXTRAPKGS) +ifeq ($(OSTYPE), Mingw) +PACKAGES += -package Win32 \ + -package unix-compat +endif # GHC can compile either a single file (use GHCCOMPILEFLAGS) or # in make mode where it follows dependencies (use GHCMAKEFLAGS). # @@ -291,6 +295,7 @@ endif .PHONY: bsc bsc: $(SOURCES) + mkdir -p $(TMPDIR) $(PREBUILDCOMMAND) # to force updating of BuildVersion/BuildSystem when necessary ./update-build-version.sh @@ -405,5 +410,6 @@ clean: full_clean: clean $(RM) -f BuildSystem.hs BuildVersion.hs $(RM) tags TAGS + $(RM) -rf $(TMPDIR) # ----- diff --git a/src/comp/SimFileUtils.hs b/src/comp/SimFileUtils.hs index 67084d86d..c7715e401 100644 --- a/src/comp/SimFileUtils.hs +++ b/src/comp/SimFileUtils.hs @@ -13,8 +13,11 @@ import Version(bscVersionStr) import FileNameUtil import ErrorUtil(internalError) -import System.Posix.Files -import System.Posix.Types(EpochTime) +import System.Directory (doesFileExist, getModificationTime) +import System.FilePath (FilePath) +import Data.Time.Clock.POSIX (POSIXTime, utcTimeToPOSIXSeconds) +import Data.Time.Clock (UTCTime) + import System.IO(openFile, hGetContents, hClose, IOMode(..)) import Control.Monad(filterM) import Control.Exception(bracketOnError) @@ -23,13 +26,14 @@ import qualified Data.Map as M -- import Debug.Trace(traceM) -getModTime :: FilePath -> IO (Maybe EpochTime) -getModTime f = - do ok <- fileExist f - if ok - then do s <- getFileStatus f - return $ Just (modificationTime s) - else return Nothing +getModTime :: FilePath -> IO (Maybe POSIXTime) +getModTime f = do + ok <- doesFileExist f + if ok + then do + modTime <- getModificationTime f + return $ Just (utcTimeToPOSIXSeconds modTime) + else return Nothing codeGenOptionDescr :: Flags -> Bool -> String codeGenOptionDescr flags is_top = @@ -39,7 +43,7 @@ codeGenOptionDescr flags is_top = readCodeGenOptionDescr :: FilePath -> IO (Maybe String) readCodeGenOptionDescr f = - do ok <- fileExist f + do ok <- doesFileExist f if ok then do bracketOnError (openFile f ReadMode) (\hdl -> do hClose hdl diff --git a/src/comp/bluetcl.hs b/src/comp/bluetcl.hs index 7353ebcbe..731da7796 100644 --- a/src/comp/bluetcl.hs +++ b/src/comp/bluetcl.hs @@ -27,7 +27,7 @@ import Data.Ord(comparing) import System.IO.Unsafe(unsafePerformIO) import System.Environment(getEnv) import System.Mem(performGC) -import System.Posix.Signals +import System.Signal import Text.Regex import Data.Generics (listify) import qualified Data.Map as M @@ -113,7 +113,7 @@ blueshell_Init interp = -- setup a Ctrl-C handler mv <- newEmptyMVar _ <- forkIO (handleCtrlC mv) - _ <- installHandler sigINT (Catch $ recordCtrlC mv) Nothing + _ <- installHandler sigINT (\_ -> recordCtrlC mv) -- return 0) -- TCL_OK handler diff --git a/src/comp/bsc.hs b/src/comp/bsc.hs index 2014b763c..da25389af 100644 --- a/src/comp/bsc.hs +++ b/src/comp/bsc.hs @@ -10,7 +10,7 @@ import System.Exit(ExitCode(ExitFailure, ExitSuccess)) import System.FilePath(takeDirectory) import System.IO(hFlush, stdout, hPutStr, stderr, hGetContents, hClose, hSetBuffering, BufferMode(LineBuffering)) import System.IO(hSetEncoding, utf8) -import System.Posix.Files(fileMode, unionFileModes, ownerExecuteMode, groupExecuteMode, setFileMode, getFileStatus, fileAccess) +import System.PosixCompat.Files(fileMode, unionFileModes, ownerExecuteMode, groupExecuteMode, setFileMode, getFileStatus, fileAccess) import System.Directory(getDirectoryContents, doesFileExist, getCurrentDirectory) import System.Time(getClockTime, ClockTime(TOD)) -- XXX: from old-time package import Data.Char(isSpace, toLower, ord) diff --git a/src/vendor/stp/HaskellIfc/STP.hs b/src/vendor/stp/HaskellIfc/STP.hs index 59fa198e1..5c433dea1 100644 --- a/src/vendor/stp/HaskellIfc/STP.hs +++ b/src/vendor/stp/HaskellIfc/STP.hs @@ -102,7 +102,7 @@ import qualified Foreign.Concurrent as F import MVarStrict import ErrorUtil(internalError) -import System.Posix.Env(getEnvDefault) +import System.Environment (lookupEnv) --import Util(traceM) @@ -170,6 +170,12 @@ checkVersion = do ptr <- vc_createValidityChecker return (ptr /= nullPtr) +-- | Cross-platform replacement for 'getEnvDefault' +getEnvDefault :: String -> String -> IO String +getEnvDefault var def = do + value <- lookupEnv var + return $ maybe def id value + ------------------------------------------------------------------------ -- Context manipulation diff --git a/src/vendor/stp/Makefile b/src/vendor/stp/Makefile index 092995d7f..07653fd17 100644 --- a/src/vendor/stp/Makefile +++ b/src/vendor/stp/Makefile @@ -13,6 +13,8 @@ endif ifeq ($(OSTYPE), Darwin) SNAME=libstp.dylib +else ifeq ($(OSTYPE), Mingw) +SNAME=libstp.dll else SNAME=libstp.so.1 endif @@ -21,7 +23,8 @@ all: install install: $(MAKE) -C $(SRC) install - ln -fsn HaskellIfc include_hs + rm -rf include_hs + ln -sfn HaskellIfc include_hs install -m 755 -d $(PREFIX)/lib/SAT install -m 644 lib/$(SNAME) $(PREFIX)/lib/SAT @@ -30,4 +33,4 @@ clean: full_clean: $(MAKE) -C $(SRC) full_clean - rm -f include_hs + rm -rf include_hs diff --git a/src/vendor/stp/src/AST/ASTmisc.cpp b/src/vendor/stp/src/AST/ASTmisc.cpp index aecb98c4c..1350c79b8 100644 --- a/src/vendor/stp/src/AST/ASTmisc.cpp +++ b/src/vendor/stp/src/AST/ASTmisc.cpp @@ -10,6 +10,8 @@ #include "AST.h" #include "../STPManager/STPManager.h" #include "../STPManager/NodeIterator.h" +#include +#include namespace BEEV { @@ -582,22 +584,18 @@ namespace BEEV } - itimerval timeout; - void setHardTimeout(int sec) - { - signal(SIGVTALRM, handle_time_out); - timeout.it_interval.tv_usec = 0; - timeout.it_interval.tv_sec = 0; - timeout.it_value.tv_usec = 0; - timeout.it_value.tv_sec = sec; - setitimer(ITIMER_VIRTUAL, &timeout, NULL); - } +std::thread timeout_thread; +void setHardTimeout(int sec) { + timeout_thread = std::thread([sec]() { + std::this_thread::sleep_for(std::chrono::seconds(sec)); + handle_time_out(0); + }); +} long getCurrentTime() { - timeval t; - gettimeofday(&t, NULL); - return (1000 * t.tv_sec) + (t.tv_usec / 1000); + auto ms = std::chrono::duration_cast(std::chrono::system_clock::now().time_since_epoch()); + return ms.count(); } };//end of namespace diff --git a/src/vendor/stp/src/Makefile b/src/vendor/stp/src/Makefile index 988253af1..c269539f6 100644 --- a/src/vendor/stp/src/Makefile +++ b/src/vendor/stp/src/Makefile @@ -17,6 +17,9 @@ endif ifeq ($(OSTYPE), Darwin) LIBRARIES=lib/libstp.dylib SNAME = libstp.dylib +else ifeq ($(OSTYPE), Mingw) +LIBRARIES = lib/libstp.dll +SNAME = libstp.dll else LIBRARIES=lib/libstp.so.1 lib/libstp.so SNAME = libstp.so.1 @@ -72,7 +75,7 @@ lib/$(SNAME): c_interface/c_interface.o \ @# We use --whole-archive to ensure that all symbols in to-sat are used $(CXX) $(CFLAGS) $(SHAREDFLAG) -Wl,$(SONAMEFLAG),$(SNAME) -o $@ $(LIBCCARGS) -ifneq ($(OSTYPE), Darwin) +ifneq ($(OSTYPE), Darwin, Mingw) lib/libstp.so: lib/libstp.so.1 -rm -f $@ (cd lib; ln -s libstp.so.1 libstp.so) diff --git a/src/vendor/stp/src/c_interface/c_interface.cpp b/src/vendor/stp/src/c_interface/c_interface.cpp index ab83d3b86..5e912673a 100644 --- a/src/vendor/stp/src/c_interface/c_interface.cpp +++ b/src/vendor/stp/src/c_interface/c_interface.cpp @@ -10,6 +10,7 @@ #include #include +#include #include "fdstream.h" #include "../printer/printers.h" #include "../cpp_interface/cpp_interface.h" @@ -445,6 +446,7 @@ int vc_query(VC vc, Expr e) return vc_query_with_timeout(vc,e,-1); } +static std::thread timeout_thread; int vc_query_with_timeout(VC vc, Expr e, int timeout_ms) { nodestar a = (nodestar)e; stpstar stp = ((stpstar)vc); @@ -453,13 +455,10 @@ int vc_query_with_timeout(VC vc, Expr e, int timeout_ms) { assert(!BEEV::ParserBM->soft_timeout_expired); if (timeout_ms != -1) { - itimerval timeout; - signal(SIGVTALRM, soft_time_out); - timeout.it_interval.tv_usec = 0; - timeout.it_interval.tv_sec = 0; - timeout.it_value.tv_usec = 1000 * (timeout_ms % 1000); - timeout.it_value.tv_sec = timeout_ms / 1000; - setitimer(ITIMER_VIRTUAL, &timeout, NULL); + timeout_thread = std::thread([timeout_ms] { + std::this_thread::sleep_for(std::chrono::milliseconds(timeout_ms)); + soft_time_out(0); + }); } if(!BEEV::is_Form_kind(a->GetKind())) @@ -493,7 +492,7 @@ int vc_query_with_timeout(VC vc, Expr e, int timeout_ms) { if (timeout_ms !=-1) { // Reset the timer. - setitimer(ITIMER_VIRTUAL, NULL, NULL); + timeout_thread = {}; BEEV::ParserBM->soft_timeout_expired = false; } diff --git a/src/vendor/stp/src/extlib-abc/aig.h b/src/vendor/stp/src/extlib-abc/aig.h index e1c871e64..cf88abbeb 100644 --- a/src/vendor/stp/src/extlib-abc/aig.h +++ b/src/vendor/stp/src/extlib-abc/aig.h @@ -21,6 +21,7 @@ #ifndef __AIG_H__ #define __AIG_H__ +#include #ifdef __cplusplus extern "C" { #endif @@ -176,10 +177,12 @@ static inline int Aig_WordCountOnes( unsigned uWord ) return (uWord & 0x0000FFFF) + (uWord>>16); } -static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) & ~01); } -static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) ^ 01); } -static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((unsigned long)(p) ^ (c)); } -static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int )(((unsigned long)p) & 01); } +static inline unsigned long bitcast_long(void* f) {unsigned long t; memcpy(&t, &f, sizeof(unsigned long)); return t; } + +static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)(bitcast_long(p) & ~01); } +static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)(bitcast_long(p) ^ 01); } +static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)(bitcast_long(p) ^ (c)); } +static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int )((bitcast_long(p)) & 01); } static inline int Aig_ManPiNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PI]; } static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PO]; } diff --git a/src/vendor/stp/src/main/main.cpp b/src/vendor/stp/src/main/main.cpp index 03a2bb24c..b01fa59a2 100644 --- a/src/vendor/stp/src/main/main.cpp +++ b/src/vendor/stp/src/main/main.cpp @@ -72,13 +72,15 @@ int main(int argc, char ** argv) { extern FILE *smtin; extern FILE *smt2in; +// Windows doesn't have sbrk. Closest thing is VirtualAlloc. +#ifndef _WIN32 // Grab some memory from the OS upfront to reduce system time when // individual hash tables are being allocated if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void *) -1)) { FatalError("Initial allocation of memory failed."); } - +#endif STPMgr * bm = new STPMgr(); diff --git a/src/vendor/stp/src/sat/cryptominisat2/time_mem.h b/src/vendor/stp/src/sat/cryptominisat2/time_mem.h index f923c9a07..74c444a6d 100644 --- a/src/vendor/stp/src/sat/cryptominisat2/time_mem.h +++ b/src/vendor/stp/src/sat/cryptominisat2/time_mem.h @@ -21,34 +21,54 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef TIME_MEM_H #define TIME_MEM_H -#ifdef _MSC_VER - #include - #include +#ifdef _WIN32 + #ifndef WIN32_LEAN_AND_MEAN + #define WIN32_LEAN_AND_MEAN + #endif + #include + // Include windows.h first + #include #else #include #include #include - #include #endif +#include +#include namespace MINISAT { using namespace MINISAT; /*************************************************************************************/ -#ifdef _MSC_VER - +#ifdef _WIN32 static inline double cpuTime(void) { - return (double)clock() / CLOCKS_PER_SEC; } + constexpr uint64_t FILETIME_to_s = 1e7; // 100 ns / FILETIME + FILETIME creationTime, undefined, kernelTime, userTime; + if (GetProcessTimes(GetCurrentProcess(), &creationTime, &undefined + , &kernelTime, &userTime) == 0) { + return 0; + } + return (double)(userTime.dwLowDateTime | ((uint64_t)userTime.dwHighDateTime << 32)) / FILETIME_to_s; } #else - static inline double cpuTime(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } #endif -#if defined(__linux__) + +#ifdef _WIN32 + +static inline uint64_t memUsed() { + PROCESS_MEMORY_COUNTERS pmc; + auto err = GetProcessMemoryInfo(GetCurrentProcess(), &pmc, sizeof(pmc)); + if (err == 0) return 0; + return pmc.WorkingSetSize; +} + +#elif defined(__linux__) + static inline int memReadStat(int field) { char name[256]; @@ -62,18 +82,21 @@ static inline int memReadStat(int field) fclose(in); return value; } -static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); } +static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); } #elif defined(__FreeBSD__) + static inline uint64_t memUsed(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); - return ru.ru_maxrss*1024; } - + return ru.ru_maxrss*1024; +} #else + static inline uint64_t memUsed() { return 0; } + #endif #if defined(__linux__) diff --git a/src/vendor/stp/src/sat/mtl/template.mk b/src/vendor/stp/src/sat/mtl/template.mk index 103582ea7..105bc7ff5 100644 --- a/src/vendor/stp/src/sat/mtl/template.mk +++ b/src/vendor/stp/src/sat/mtl/template.mk @@ -40,21 +40,15 @@ libp: lib$(LIB)_profile.a libd: lib$(LIB)_debug.a libr: lib$(LIB)_release.a -## Compile options -%.o: CFLAGS +=$(COPTIMIZE) -g -D DEBUG -%.op: CFLAGS +=$(COPTIMIZE) -pg -g -D NDEBUG -%.od: CFLAGS +=-O0 -g -D DEBUG -%.or: CFLAGS +=$(COPTIMIZE) -g -D NDEBUG - ## Link options -$(EXEC): LFLAGS += -g +$(EXEC): LFLAGS += -g $(EXEC)_profile: LFLAGS += -g -pg $(EXEC)_debug: LFLAGS += -g #$(EXEC)_release: LFLAGS += ... $(EXEC)_static: LFLAGS += --static ## Dependencies -$(EXEC): $(COBJS) +$(EXEC): $(COBJS) $(EXEC)_profile: $(PCOBJS) $(EXEC)_debug: $(DCOBJS) $(EXEC)_release: $(RCOBJS) @@ -62,11 +56,17 @@ $(EXEC)_static: $(RCOBJS) lib$(LIB)_standard.a: $(filter-out %/Main.o, $(COBJS)) lib$(LIB)_profile.a: $(filter-out %/Main.op, $(PCOBJS)) -lib$(LIB)_debug.a: $(filter-out %/Main.od, $(DCOBJS)) +lib$(LIB)_debug.a: $(filter-out %/Main.od, $(DCOBJS)) lib$(LIB)_release.a: $(filter-out %/Main.or, $(RCOBJS)) ## Build rule +## Compile options +%.o: $(CXX) $(CFLAGS) $(COPTIMIZE) -g -D DEBUG -c -o $@ $< +%.op: $(CXX) $(CFLAGS) $(COPTIMIZE) -pg -g -D NDEBUG -c -o $@ $< +%.od: $(CXX) $(CFLAGS) -O0 -g -D DEBUG -c -o $@ $< +%.or: $(CXX) $(CFLAGS) $(COPTIMIZE) -g -D NDEBUG -c -o $@ $< + %.o %.op %.od %.or: %.cc @echo Compiling: $(subst $(MROOT)/,,$@) @$(CXX) $(CFLAGS) -c -o $@ $< @@ -94,10 +94,10 @@ clean: ## Make dependencies depend.mk: $(CSRCS) $(CHDRS) - @echo Making dependencies - @$(CXX) $(CFLAGS) -I$(MROOT) \ - $(CSRCS) -MM | sed 's|\(.*\):|$(PWD)/\1 $(PWD)/\1r $(PWD)/\1d $(PWD)/\1p:|' > depend.mk - @for dir in $(DEPDIR); do \ + echo Making dependencies + $(CXX) $(CFLAGS) -I$(MROOT) \ + $(CSRCS) -MM | sed 's|\(.*\): |$(PWD)/\1 $(PWD)/\1r $(PWD)/\1d $(PWD)/\1p:|' > depend.mk + for dir in $(DEPDIR); do \ if [ -r $(MROOT)/$${dir}/depend.mk ]; then \ echo Depends on: $${dir}; \ cat $(MROOT)/$${dir}/depend.mk >> depend.mk; \ diff --git a/src/vendor/yices/Makefile b/src/vendor/yices/Makefile index b8dbdeafa..1f64ac873 100644 --- a/src/vendor/yices/Makefile +++ b/src/vendor/yices/Makefile @@ -11,24 +11,28 @@ VERSION = v$(VER_MAJ).$(VER_MIN) all: install +$(info OSTYPE: $(OSTYPE)) ifeq ($(OSTYPE), Darwin) -SNAME=libyices.$(VER_MAJ).dylib +SNAME=lib/libyices.$(VER_MAJ).dylib +else ifeq ($(OSTYPE), Mingw) +SNAME=$(VERSION)/yices2-inst/bin/libyices.dll else -SNAME=libyices.so.$(VER_MAJ).$(VER_MIN) +SNAME=lib/libyices.so.$(VER_MAJ).$(VER_MIN) endif install: $(MAKE) -C $(VERSION) install + rm -rf include lib include_hs ln -fsn $(VERSION)/include ln -fsn $(VERSION)/lib ln -fsn $(VERSION)/include_hs install -m 755 -d $(PREFIX)/lib/SAT - install -m 644 lib/$(SNAME) $(PREFIX)/lib/SAT + install -m 644 $(SNAME) $(PREFIX)/lib/SAT clean: $(MAKE) -C $(VERSION) clean full_clean: $(MAKE) -C $(VERSION) full_clean - rm -f include lib include_hs + rm -rf include lib include_hs diff --git a/src/vendor/yices/v2.6/Makefile b/src/vendor/yices/v2.6/Makefile index 53f95857c..8d451b88a 100644 --- a/src/vendor/yices/v2.6/Makefile +++ b/src/vendor/yices/v2.6/Makefile @@ -51,6 +51,8 @@ ifeq ($(YICES_STUB),) else (cd stub ; make install) endif +# ln -fn is implementation-defined, use rm -rf before ln + rm -rf include lib include_hs ln -fsn $(YICES_INST)/include ln -fsn $(YICES_INST)/lib ln -fsn HaskellIfc include_hs @@ -65,6 +67,6 @@ endif .PHONY: full_clean full_clean: clean - rm -f include_hs + rm -rf include_hs rm -rf $(YICES_INST) - rm -f include lib + rm -rf include lib