From: trevor_hansen Date: Thu, 9 Jun 2011 04:28:54 +0000 (+0000) Subject: A windows patch to r446 from Hume. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=82651da81950f2f3b9c9d6c43df03eed80c93aa6;p=francis%2Fstp.git A windows patch to r446 from Hume. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1336 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/windows/README b/windows/README new file mode 100644 index 0000000..062dba1 --- /dev/null +++ b/windows/README @@ -0,0 +1,2 @@ +This patch to revision 446 was provided by Hume and tested under cygwin/mingw/centos 5.4/msvc9.0. + diff --git a/windows/cmakemods/msvcmt.cmake b/windows/cmakemods/msvcmt.cmake new file mode 100644 index 0000000..7549d00 --- /dev/null +++ b/windows/cmakemods/msvcmt.cmake @@ -0,0 +1,41 @@ +# version 1.00 +# usage of macro is tricky, so you may refer to the .orig file for inline form + +# here we must use macro because only macro can modify the arg in outer scope +macro(replace_msvs_mtmd_flags the_cflags bflag) + set(loc_flag ${bflag}) + if(loc_flag) + if(${the_cflags} MATCHES "/MD") + #message("before replace :", "${${the_cflags}}") + string(REGEX REPLACE "/MD" "/MT" ${the_cflags} "${${the_cflags}}") + #message("After replace :", "${${the_cflags}}") + endif(${the_cflags} MATCHES "/MD") + else(loc_flag) + # pass + if(${the_cflags} MATCHES "/MT") + string(REGEX REPLACE "/MT" "/MD" ${the_cflags} "${${the_cflags}}") + endif(${the_cflags} MATCHES "/MT") + endif(loc_flag) +endmacro(replace_msvs_mtmd_flags the_cflags bflag) + +if(WIN32 AND MSVC) + # using macro or function wpn't do the correct thing + option(MSVC_MD "Using /MD when compiling using msvc toolchains" OFF) + + # get all CMAKE_CXX_FLAGS CMAKE_C_FLAGS variants + set(BldList CMAKE_CXX_FLAGS CMAKE_C_FLAGS) + foreach(build_typ DEBUG RELEASE MINSIZEREL RELWITHDEBINFO) + list(APPEND BldList CMAKE_CXX_FLAGS_${build_typ} CMAKE_C_FLAGS_${build_typ}) + endforeach(build_typ DEBUG RELEASE MINSIZEREL RELWITHDEBINFO) + + # note that function or macro won't work must use global code + if(NOT MSVC_MD) + foreach(flag_var ${BldList}) + replace_msvs_mtmd_flags(${flag_var} ON) + endforeach(flag_var ${BldList}) + else(NOT MSVC_MD) + foreach(flag_var ${BldList}) + replace_msvs_mtmd_flags(${flag_var} OFF) + endforeach(flag_var ${BldList}) + endif(NOT MSVC_MD) +endif(WIN32 AND MSVC) diff --git a/windows/cmakemods/slibgcc.cmake b/windows/cmakemods/slibgcc.cmake new file mode 100644 index 0000000..c5be3d3 --- /dev/null +++ b/windows/cmakemods/slibgcc.cmake @@ -0,0 +1,45 @@ +# version 1.00 +# gcc -static-libgcc should be specified + +# here we must use macro because only macro can modify the arg in outer scope +macro(replace_gcc_flags the_cflags bflag) + set(loc_flag ${bflag}) + if(loc_flag) + if(${the_cflags} MATCHES "-shared-libgcc") + string(REGEX REPLACE "-shared-libgcc" "-static-libgcc" ${the_cflags} "${${the_cflags}}") + else(${the_cflags} MATCHES "-shared-libgcc") + set(${the_cflags} "${${the_cflags}} -static-libgcc") + endif(${the_cflags} MATCHES "-shared-libgcc") + else(loc_flag) + # pass + if(${the_cflags} MATCHES "-static-libgcc") + string(REGEX REPLACE "-static-libgcc" "-shared-libgcc" ${the_cflags} "${${the_cflags}}") + else(${the_cflags} MATCHES "-static-libgcc") + set(${the_cflags} "${${the_cflags}} -shared-libgcc") + endif(${the_cflags} MATCHES "-static-libgcc") + endif(loc_flag) +endmacro(replace_gcc_flags the_cflags bflag) + +if(UNIX) + # using macro or function wpn't do the correct thing + option(USING_GCC_SHARED_RUNTIME_LIB "Using -shared-libgcc not -static-libgcc when compiling using gcc toolchains" OFF) + + # get all CMAKE_CXX_FLAGS CMAKE_C_FLAGS variants + set(BldList CMAKE_CXX_FLAGS CMAKE_C_FLAGS) + foreach(build_typ DEBUG RELEASE MINSIZEREL RELWITHDEBINFO) + list(APPEND BldList CMAKE_CXX_FLAGS_${build_typ} CMAKE_C_FLAGS_${build_typ}) + endforeach(build_typ DEBUG RELEASE MINSIZEREL RELWITHDEBINFO) + + # note that if function or macro not work we must use global code + if(NOT USING_GCC_SHARED_RUNTIME_LIB) + foreach(flag_var ${BldList}) + replace_gcc_flags(${flag_var} ON) + endforeach(flag_var ${BldList}) + else(NOT USING_GCC_SHARED_RUNTIME_LIB) + foreach(flag_var ${BldList}) + replace_gcc_flags(${flag_var} OFF) + endforeach(flag_var ${BldList}) + endif(NOT USING_GCC_SHARED_RUNTIME_LIB) +endif(UNIX) + + diff --git a/windows/cmakemods/staticrt.cmake b/windows/cmakemods/staticrt.cmake new file mode 100644 index 0000000..2946ccd --- /dev/null +++ b/windows/cmakemods/staticrt.cmake @@ -0,0 +1,6 @@ +# version 1.00 +# to make msvc/gcc to link statically the runtime libraries +get_filename_component(MYMODESDIR ${CMAKE_CURRENT_LIST_FILE} PATH) +include("${MYMODESDIR}/msvcmt.cmake") +include("${MYMODESDIR}/slibgcc.cmake") + diff --git a/windows/r446-winport.patch b/windows/r446-winport.patch new file mode 100644 index 0000000..6bc9331 --- /dev/null +++ b/windows/r446-winport.patch @@ -0,0 +1,913 @@ +diff -Nur stp/CMakeLists.txt r446port/CMakeLists.txt +--- stp/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,139 @@ ++cmake_minimum_required(VERSION 2.6) ++ ++# base common definitions ++set(TargetName "stp") ++set(ProjectName "stp") ++ ++########################################################################## ++project(${ProjectName}) ++ ++#set(CMAKE_BUILD_TYPE Release) ++ ++# static build settings for MSVC/gcc ++include("../cmakemods/staticrt.cmake") ++ ++set(PHINTS "") ++set(STP_DEFS_COMM -DCRYPTOMINISAT) ++set(STP_INCL_COMM src/sat/mtl src/AST) ++ ++option(BUILD_SHARED_LIB "Whether to Build shared libstp or not" ON) ++ ++set(OPTIMIZITION_FLAGS "-O3") ++ ++# bison and flex is needed for buiding ++if(WIN32) ++ # build shared lib on windows is not prepared at source level ++ set(BUILD_SHARED_LIB OFF) ++ set(FLEX_PATH_HINT "e:/cygwin/bin" CACHE STRING "Flex path hints, can be null if on your path") ++ set(FLEX_PATH_HINT "e:/cygwin/bin" CACHE STRING "Bison path hints, can be null if on your path") ++ set(FLEX_PATH_HINT "C:/Perl/bin" CACHE STRING "Perl path hints, can be null if on your pat") ++ ++ set(PHINTS ${PERL_PATH_HINT} ${FLEX_PATH_HINT} ${BISON_PATH_HINT}) ++ ++ if(MSVC) ++ set(OPTIMIZITION_FLAGS "/GL /Ox /Oi /Ot /Oy") ++ set(STP_DEFS_COMM ${STP_DEFS_COMM} -D_CRT_SECURE_NO_WARNINGS) ++ set(STP_INCL_COMM ../winports ../winports/msc99hdr ${STP_INCL_COMM}) ++ ++ # stack size of MSVC must be specified ++ string(REGEX REPLACE "/STACK:[0-9]+" "" CMAKE_EXE_LINKER_FLAGS ${CMAKE_EXE_LINKER_FLAGS}) ++ set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} /STACK:256000000") ++ else(MSVC) ++ # mingw ++ set(STP_DEFS_COMM ${STP_DEFS_COMM} -DEXT_HASH_MAP) ++ endif(MSVC) ++elseif(UNIX) ++ set(STP_DEFS_COMM ${STP_DEFS_COMM} -DEXT_HASH_MAP) ++endif(WIN32) ++ ++find_program(PERLP perl) ++find_program(FLEXP flex HINTS ${PHINTS}) ++find_program(BISONP bison HINTS ${PHINTS}) ++ ++#message(${PERLP}) ++#message(${FLEXP}) ++#message(${BISONP}) ++ ++ ++if(NOT FLEXP OR NOT BISONP OR NOT PERLP) ++message(FATAL_ERROR "Flex/Bison/Perl is not found and is required, Abort!") ++endif(NOT FLEXP OR NOT BISONP OR NOT PERLP) ++ ++## ++## add rules generate the custom files in AST ++## ++set(ASTD_PREFIX ${CMAKE_CURRENT_SOURCE_DIR}/src/AST) ++ ++set(OUTFILES ${ASTD_PREFIX}/ASTKind.h ${ASTD_PREFIX}/ASTKind.cpp) ++set(GenKindsScript ${ASTD_PREFIX}/genkinds.pl) ++add_custom_command(OUTPUT ${OUTFILES} ++ COMMAND ${PERLP} ${GenKindsScript} ++ DEPENDS ${GenKindsScript} ++ WORKING_DIRECTORY ${ASTD_PREFIX} ++ ) ++ ++## ++## add rules generate the custom files in parser ++## ++set(PARSERD_PREFIX ${CMAKE_CURRENT_SOURCE_DIR}/src/parser) ++set(OUTFILES ${PARSERD_PREFIX}/lexCVC.cpp ${PARSERD_PREFIX}/lexSMT.cpp ++ ${PARSERD_PREFIX}/parseCVC.cpp ${PARSERD_PREFIX}/parseCVC_defs.h ++ ${PARSERD_PREFIX}/parseSMT.cpp ${PARSERD_PREFIX}/parseSMT_defs.h) ++add_custom_command(OUTPUT ${OUTFILES} ++ COMMAND ${FLEXP} -olexCVC.cpp -Pcvc CVC.lex ++ COMMAND ${FLEXP} -olexSMT.cpp -Psmt smtlib.lex ++ COMMAND ${BISONP} -y -v --defines=parseCVC_defs.h -oparseCVC.cpp -pcvc CVC.y ++ COMMAND ${BISONP} -y -v --defines=parseSMT_defs.h -oparseSMT.cpp -psmt smtlib.y ++ DEPENDS ${PARSERD_PREFIX}/CVC.lex ${PARSERD_PREFIX}/smtlib.lex ${PARSERD_PREFIX}/CVC.y ${PARSERD_PREFIX}/smtlib.y ++ WORKING_DIRECTORY ${PARSERD_PREFIX} ++ ) ++ ++# ++add_definitions(${STP_DEFS_COMM}) ++include_directories(${STP_INCL_COMM}) ++ ++macro(add_stp_library lib_name, filelist) ++ source_group(${lib_name} FILES ${filelist}) ++ set(LIBSTP_SRCLIST ${LIBSTP_SRCLIST} ${${filelist}} PARENT_SCOPE) ++endmacro(add_stp_library) ++ ++ ++set(SDIRLIST ++ sat ++ AST ++ STPManager ++ parser ++ absrefine_counterexample ++ to-sat ++ simplifier ++ printer ++ c_interface ++ extlib-constbv ++ ) ++ ++foreach(cdir ${SDIRLIST}) ++ add_subdirectory(src/${cdir}) ++endforeach(cdir ${SDIRLIST}) ++ ++# the stp library ++add_library(${TargetName}_lib ${STP_LIBTYPE} ${LIBSTP_SRCLIST}) ++set_target_properties(${TargetName}_lib ++ PROPERTIES OUTPUT_NAME ${TargetName} ++ COMPILE_DEFINITIONS_RELEASE ${OPTIMIZITION_FLAGS} ++ COMPILE_DEFINITIONS_RELWITHDEBINFO ${OPTIMIZITION_FLAGS} ++ ) ++ ++set(DEPLIBS ${TargetName}_lib) ++ ++# generate the stp main program ++file(GLOB SRC_LIST ${PROJECT_SOURCE_DIR}/src/main/*.c* ${PROJECT_SOURCE_DIR}/src/main/*.h) ++add_executable(${TargetName} ${SRC_LIST}) ++set_target_properties(${TargetName} ++ PROPERTIES ++ COMPILE_DEFINITIONS_RELEASE ${OPTIMIZITION_FLAGS} ++ COMPILE_DEFINITIONS_RELWITHDEBINFO ${OPTIMIZITION_FLAGS} ++ ) ++ ++add_dependencies(${TargetName} ${DEPLIBS}) ++target_link_libraries(${TargetName} ${DEPLIBS}) ++ +diff -Nur stp/scripts/dotest.py r446port/scripts/dotest.py +--- stp/scripts/dotest.py 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/scripts/dotest.py 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,316 @@ ++#! /usr/bin/python ++# -*- coding: iso-8859-1 -*- ++ ++# Run STP regression tests of a given level (default: 0, meaning ++# minimum amount of tests). The higher the regression level, the more ++# tests to run, and the harder they get. ++# Each test may contain information about its regression level, ++# expected outcome, expected runtime, whether it produces a proof, ++# etc. in the format given below. This script will scan the first 100 ++# lines of each test and try to collect this information. ++# If some info is not found, defaults are assumed. Default regression ++# level is 0, expected runtime is unbounded, outcome is undefined ++# (whatever it returns is OK), proof should be produced if outcome is ++# Valid, and if it is produced, it'll be verified. ++# Test info is given in the comments; here are examples ++# ++# %%% Regression level = 2 ++# %%% Result = Valid %% or Invalid, or Unknown ++# %%% Runtime = 10 %% in seconds ++# %%% Proof = yes %% or 'no', if it doesn't produce a proof ++# %%% Language = presentation %% or 'internal' ++ ++# The number of '%' and following spaces can vary, case is not ++# important. Any text after the value is ignored. Any comments that ++# are not recognized are also ignored. ++ ++import os, sys, subprocess, glob, re ++import logging, optparse ++from os import path ++from mtimeit import * ++ ++gprofiler = profiler() ++line_len = 75 ++ ++class test_context: ++ def __init__ (self): ++ self.num_total = 0 ++ self.time_total = 0 ++ self.proofs_checked = 0 ++ self.num_problems = 0 ++ self.test_problems = {} ++ ++ def add_keyval (self, k, v): ++ if not k in self.test_problems: ++ self.test_problems[k] = [v] ++ else: ++ self.test_problems[k].append(v) ++ ++ def get_key (self, k): ++ if k in self.test_problems: ++ return self.test_problems[k] ++ return [] ++ ++ def add_problems (self, catig, dat): ++ self.add_keyval(catig, dat) ++ self.num_problems += 1 ++ ++ def add_errors (self, fn, expect_res, act_res): ++ self.add_problems("errors", (fn, expect_res, act_res)) ++ ++ def print_errors (self): ++ logging.info("Total tested %d and found %d problems", self.num_total, self.num_problems) ++ if self.num_problems: ++ for k, v in self.test_problems.iteritems(): ++ logging.info("%s test total %d", k, len(v)) ++ for i in v: ++ logging.info("\t%s", i[0]) ++ ++class expected_test_args: ++ def __init__ (self): ++ self.level = None ++ self.result = None ++ self.runtime = None ++ self.proof = None ++ self.sat_mode = None ++ self.lang = None ++ self.stp_opts = "" ++ ++ def set_default(self, opts): ++ pass ++ ++def parse_cmdline(permit_null_args=True): ++ the_usage = "usage: %prog [options] [test path] [test path]..." ++ the_version = "version 0.1" ++ parser = optparse.OptionParser(usage = the_usage, version = the_version) ++ ++ # logging options ++ parser.add_option("-v", "--verbose", action="store_const", const=logging.INFO, dest="log_level", default=logging.INFO) ++ parser.add_option("-q", "--quiet", action="store_const", const=logging.ERROR, dest="log_level") ++ parser.add_option("--log-format", dest="log_format", metavar="FMT", default="%(asctime)s %(levelname)s %(message)s") ++ parser.add_option("--log-file", dest="log_file", metavar="FILE") ++ parser.add_option("--log-syslog", dest="log_syslog", metavar="HOST") ++ ++ # timeouts ++ parser.add_option("-t", "--timeout", dest="timeout", action="store_const", default=0, ++ help = "Timeouts in seconds 0 = no limit (default: %default)") ++ parser.add_option("-l", "--testlevel", dest="level", action="store_const", default=4, ++ help = "Max regression test level (default: %default)") ++ parser.add_option("--lang", dest="lang", action="store", default="all", ++ help = "Language: presentation/internal/smt-lib (default: %default)") ++ parser.add_option("-p", "--stppath", dest="stppath", action="store", default="", ++ help = "Stp path (default: %default)") ++ parser.add_option("--stpopt", dest="stpopt", action="store", default="-d", ++ help = "Options passed to stp command line (default: %default)") ++ parser.add_option("--vc", dest="vc", action="store", default="bin/stp", ++ help = "Verification program (default: %default)") ++ parser.add_option("--rt", dest="checkruntime", action="store_true", default=True, ++ help = "Check that each test finishes within the specified runtime (default: %default)") ++ parser.add_option("--no-rt", dest="checkruntime", action="store_false", ++ help = "Don't check that each test finishes within the specified runtime") ++ parser.add_option("--max-info-lines", dest="maxinfolines", action="store_const", default=4, ++ help = "Max info lines to check per testcase file (default: %default)") ++ parser.add_option("--proofs", dest="proofs", action="store_true", ++ help = "Produce and verify proofs, None means depends on testcase(default: %default)") ++ parser.add_option("--no-proofs", dest="proofs", action="store_false", ++ help = "Do not produce / verify proofs ") ++ parser.add_option("-f", "--list-file", dest="listfile", action="store", ++ help = "Check test case listed in file") ++ parser.add_option("-r", "--recursive", dest="recursive", action="store_true", default=False, ++ help = "Do test recursively (default: %default)") ++ ++ opts, args = parser.parse_args() ++ if len(args) == 0 and not permit_null_args: ++ parser.print_help() ++ parser.exit() ++ return (opts, args) ++ ++def parse_cmdline_and_logging(permit_null_args=True): ++ opts, args = parse_cmdline(permit_null_args) ++ # process logging support ++ logging.basicConfig(level=opts.log_level, format=opts.log_format, filename=opts.log_file, stream=sys.stdout) ++ if opts.log_syslog: ++ from logging.handlers import SysLogHandler ++ logging.info("redirect log to syslogd at %s", opts.log_syslog) ++ logging.getLogger().addHandler(SysLogHandler((opts.log_syslog, 514), SysLogHandler.LOG_LOCAL0)) ++ return (opts, args) ++ ++def log_basic_test_info(opts): ++ logging.info("Base Test Options:") ++ logging.info("*"*line_len) ++ logging.info("Regression level: %d"%opts.level) ++ logging.info("Language: %s"%opts.lang) ++ if None == opts.proofs: s = "depends on testcase" ++ elif opts.proofs: s = "yes" ++ else: s = "no" ++ logging.info("Whether to produce / check proofs: %s"%s) ++ ++ if opts.timeout == 0: s = "no limit" ++ else: s = "%d seconds"%opts.timeout ++ logging.info("Time limit per test: %s"%s) ++ logging.info("*"*line_len) ++ logging.info("\n\n") ++ ++def get_test_opt(opts, test_fn): ++ targs = expected_test_args() ++ with open(test_fn, "rt") as f: ++ for idx, ln in enumerate(f): ++ if idx > opts.maxinfolines: ++ break ++ so = re.search(r"^(\s|%|\#)*Regression level\s*=\s*(\d+)", ln, re.I) ++ if so: ++ targs.level = int(so.group(2)) ++ continue ++ so = re.search(r"^(\s|%|\#)*Result\s*=\s*(Invalid|Valid|Unknown)", ln, re.I) ++ if so: ++ targs.result = so.group(2) ++ continue ++ so = re.search(r"^(\s|%|\#)*Runtime\s*=\s*(\d+)", ln, re.I) ++ if so: ++ targs.runtime = int(so.group(2)) ++ continue ++ so = re.search(r"^(\s|%|\#)*Proof\s*=\s*(yes|no)", ln, re.I) ++ if so: ++ targs.proofs = so.group(2) ++ continue ++ so = re.search(r"^(\s|%|\#)*SAT mode\s*=\s*(on|off)", ln, re.I) ++ if so: ++ targs.sat_mode = so.group(2) ++ continue ++ so = re.search(r"^(\s|%|\#)*Language\s*=\s*((\w|\d|\_)+)", ln, re.I) ++ if so: ++ targs.lang = so.group(2) ++ continue ++ so = re.search(r"^(\s|%|\#)*STP Options\s*=\s*(.*)$", ln, re.I) ++ if so: ++ targs.stp_opts = so.group(2) ++ continue ++ # guess the level and lang ++ if targs.level == None: targs.level = 3 ++ if targs.lang == None: ++ if re.search(r"\.(stp|svc)$", test_fn, re.I): targs.lang = "presentation" ++ if re.search(r"\.(li?sp)$", test_fn, re.I): targs.lang = "internal" ++ if re.search(r"\.(smt)$", test_fn, re.I): targs.lang = "smt-lib" ++ if targs.result == None: ++ targs.result = "Unknown" ++ return targs ++ ++def do_test (opts, tfn): ++ if path.exists(tfn): tfn = path.abspath(tfn) ++ targs = get_test_opt(opts, tfn) ++ ++ # test only levels that below current or no level hints ++ if targs.level and targs.level > opts.level: ++ logging.warn("Skip test case %s at level %d", tfn, targs.level); ++ return ++ if opts.lang != "all" and targs.lang and targs.lang != opts.lang: ++ logging.warn("Skip test case %s with lang %d", tfn, targs.lang); ++ return ++ ++ cmd = [opts.stppath] ++ if opts.stpopt: cmd.append(opts.stpopt) ++ ++ logging.info("\n") ++ logging.info("="*line_len) ++ logging.info("checking %s"%tfn) ++ logging.info("Language: %s", targs.lang) ++ logging.info("Checking proofs: %s", "yes" if opts.proofs else "no") ++ if targs.runtime: ++ logging.info("Expected runtime: %d sec", targs.runtime) ++ if targs.result: ++ logging.info("Expected result: %s", targs.result) ++ if targs.stp_opts: ++ logging.info("STP options: ", targs.stp_opts) ++ cmd.append(targs.stp_opts) ++ cmd.append(tfn) ++ ++ opts.text_ctx.num_total += 1 ++ test_tim = accum_time() ++ try: ++ with mtimeit_ctxmgr(test_tim): ++ subp = subprocess.Popen(cmd, stdout = subprocess.PIPE, stderr = subprocess.PIPE) ++ sout, serr = subp.communicate() ++ if opts.timeout: ++ test_runtime = opts.timeout ++ if targs.runtime and targs.runtime > opts.timeout: ++ test_runtime = targs.runtime ++ while True: ++ if subp.poll(): ++ break ++ if test_tim() > test_runtime: ++ subp.terminate() ++ opts.text_ctx.add_problems("timedout->killed", (tfn, test_runtime)) ++ time.sleep(0.05) ++ else: ++ subp.wait() ++ ++ if targs.result: ++ so = re.search(targs.result, sout, re.M|re.I) ++ if not so: ++ logging.error("%s result not conform!"%tfn) ++ s = (sout+serr) ++ if s: s.strip("\r\n ") ++ opts.text_ctx.add_problems("Result error", (tfn, targs.result, s)) ++ else: ++ logging.info("test passed") ++ ++ except: ++ logging.error("Exception when testing: %s", tfn) ++ raise ++ opts.text_ctx.add_problems("Failed tests", (tfn, targs.runtime)) ++ ++ if targs.runtime: ++ if test_tim() > targs.runtime: ++ opts.text_ctx.add_problems("Longer tests", (tfn, targs.runtime)) ++ if targs.runtime > 5 and test_tim() < targs.runtime/2: ++ opts.text_ctx.add_problems("Faster tests", (tfn, targs.runtime)) ++ ++ logging.info("-"*(line_len/2)) ++ logging.info("Runtime is: %d", test_tim()) ++ logging.info("="*line_len+"\n") ++ ++@fun_profile("Time Total", gprofiler) ++def do_task_test (opts, args): ++ for arg in args: ++ if os.path.isfile(arg): do_test(opts, arg) ++ elif os.path.isdir(arg): ++ fns = os.path.join(arg, "*.*") ++ testcases = glob.glob(fns) ++ for fn in testcases: ++ do_test(opts, fn) ++ ++ if opts.listfile: ++ with open(opts.listfile, "rt") as f: ++ for ln in f: ++ ln = ln.strip("\r\n ") ++ if ln: ++ do_test(opts, ln) ++ ++if __name__=='__main__': ++ opts, args = parse_cmdline_and_logging() ++ ++ # guess some predefined paths ++ defp1 = path.join("..", "bin", "stp.exe") ++ defp2 = path.join("..", "bin", "stp") ++ if not opts.stppath: ++ if path.exists(defp1): opts.stppath = defp1 ++ elif path.exists(defp2): opts.stppath = defp2 ++ else: opts.stppath = path.join("bin", "stp") ++ ++ log_basic_test_info(opts) ++ opts.text_ctx = test_context() ++ try: ++ do_task_test(opts, args) ++ except KeyboardInterrupt: ++ logging.error("="*line_len) ++ logging.error("!!! User aborted by keyboard interrupt!") ++ logging.error("="*line_len) ++ finally: ++ logging.getLogger('').setLevel(logging.INFO) ++ logging.info("\n\n") ++ logging.info("Statistics:") ++ logging.info("="*line_len) ++ opts.text_ctx.print_errors() ++ gprofiler.print_percent() ++ logging.info("="*line_len) ++ logging.info("\n\n") +diff -Nur stp/scripts/mtimeit.py r446port/scripts/mtimeit.py +--- stp/scripts/mtimeit.py 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/scripts/mtimeit.py 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,136 @@ ++#! /usr/bin/python ++# -*- coding: iso-8859-1 -*- ++# assuming python 2.6+ we use with statement without ++import os, sys, time ++import logging ++ ++class mtimeit: ++ def __init__ (self): ++ # to make sure that these should not be un-initialized ++ self.stt = None ++ self.edt = None ++ ++ def start (self): ++ self.stt = time.time() #time.clock() #time.time() ++ ++ def end_and_get_length(self): ++ self.end() ++ return self.length() ++ ++ def end (self): ++ self.edt = time.time() #time.clock() #time.time() ++ ++ def length (self): ++ return self.edt - self.stt ++ ++ def get_srepr (self): ++ tstr = "" ++ ttim = self.length() ++ if ttim >= 3110400000.0: ++ tstr = "%f centuries"%(ttim/3110400000.0) ++ elif ttim >= 31104000: ++ tstr = "%f years"%(ttim/31104000.0) ++ elif ttim >= 2592000: ++ tstr = "%f months"%(ttim/2592000.0) ++ elif ttim >= 86400: ++ tstr = "%f days"%(ttim/86400.0) ++ elif ttim >= 3600: ++ tstr = "%f hours"%(ttim/3600.0) ++ elif ttim >= 60: ++ tstr = "%f minutes"%(ttim/60) ++ else: ++ tstr = "%f seconds"%ttim ++ return tstr ++ ++ def print_srepr(self): ++ print(self.get_srepr()) ++ return True ++ ++ show_time = print_srepr ++ ++class accum_time: ++ def __init__(self, val=0): ++ self.val = val ++ ++ def __iadd__( self, n): ++ self.val += n ++ ++ def __add__( self, n): ++ self.val += n ++ ++ def __call__( self): ++ return self.val ++ ++ ++class mtimeit_ctxmgr(): ++ def __init__(self, tacc): ++ self.val = tacc ++ ++ def __enter__(self): ++ self.tobj = mtimeit() ++ self.tobj.start() ++ return self.tobj ++ ++ def __exit__(self, exc_type, exc_value, traceback): ++ self.val += self.tobj.end_and_get_length() ++ return False ++ ++class profiler(): ++ def __init__(self): ++ self.tot_tim = 0 ++ self.profd = {} ++ ++ def __getitem__( self, key): ++ if self.profd.has_key(key): ++ return self.profd[key] ++ names = [name for name in self.profd.keys() if name.startswith(key + '.')] ++ if names: ++ return accum_time(sum([self.profd[name]() for name in names])) ++ else: ++ return self.profd.setdefault(key, accum_time()) ++ ++ def __setitem__( self, key, value): ++ self.profd[key] = value ++ ++ def print_percent(self, tval = None): ++ self.tot_tim = tval ++ tt = 0 ++ if not self.tot_tim: ++ self.tot_tim = 0 ++ for k, v in self.profd.iteritems(): ++ self.tot_tim += v() ++ for k, v in self.profd.iteritems(): ++ tt += v() ++ logging.info("%-20s: time: %5.2f seconds percent: %2.2f%%"%(k, v(), self.get_percent(v()))) ++ logging.info("%-20s: time: %5.2f seconds percent: %2.2f%%"%("All monitored events", tt, self.get_percent(tt))) ++ ++ def get_percent(self, v): ++ rv = 0.0 ++ if self.tot_tim: ++ rv = v*100 / self.tot_tim ++ return rv ++ ++def class_profile(name): ++ def wrapper(func): ++ def newf(self, *args, **kwds): ++ if not hasattr(self, "profiler"): self.profiler = profiler() ++ with mtimeit_ctxmgr(self.profiler[name]): ++ return func(self, *args, **kwds) ++ return newf ++ return wrapper ++ ++def fun_profile(name, the_profiler): ++ def wrapper(func): ++ def newf(self, *args, **kwds): ++ with mtimeit_ctxmgr(the_profiler[name]): ++ return func(self, *args, **kwds) ++ return newf ++ return wrapper ++ ++ ++if __name__=='__main__': ++ tim = mtimeit() ++ tim.start() ++ time.sleep(2.5) ++ tim.end() ++ tim.print_srepr() +diff -Nur stp/src/absrefine_counterexample/CMakeLists.txt r446port/src/absrefine_counterexample/CMakeLists.txt +--- stp/src/absrefine_counterexample/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/absrefine_counterexample/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,2 @@ ++file(GLOB SRCS *.h *.c*) ++add_stp_library(absrefine_counterexample, SRCS) +diff -Nur stp/src/AST/CMakeLists.txt r446port/src/AST/CMakeLists.txt +--- stp/src/AST/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/AST/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,9 @@ ++set(OUTFILES ${CMAKE_CURRENT_SOURCE_DIR}/ASTKind.h ${CMAKE_CURRENT_SOURCE_DIR}/ASTKind.cpp) ++ ++file(GLOB SRCS *.h *.c*) ++string(REGEX MATCH HasAstKindFile "ASTKind.(h|cpp)" ${SRCS}) ++if(NOT HasAstKindFile) ++ set(SRCS ${SRCS} ${OUTFILES}) ++endif(NOT HasAstKindFile) ++ ++add_stp_library(ast, SRCS) +diff -Nur stp/src/AST/UsefulDefs.h r446port/src/AST/UsefulDefs.h +--- stp/src/AST/UsefulDefs.h 2009-11-27 14:47:14.484375000 +0800 ++++ r446port/src/AST/UsefulDefs.h 2009-12-07 12:51:46.000000000 +0800 +@@ -29,12 +29,19 @@ + #ifdef EXT_HASH_MAP + #include + #include +-#elif defined(TR1_UNORDERED_MAP) ++#elif defined(TR1_UNORDERED_MAP) || defined(_GLIBCXX_UNORDERED_MAP) + #include + #include + #define hash_map tr1::unordered_map + #define hash_set tr1::unordered_set + #define hash_multiset tr1::unordered_multiset ++#elif defined(_MSC_VER) && defined(_HAS_TR1) ++#include ++#include ++#define hash_map tr1::unordered_map ++#define hash_set tr1::unordered_set ++#define hash_multiset tr1::unordered_multiset ++#define TR1_UNORDERED_MAP 1 + #else + #include + #include +diff -Nur stp/src/c_interface/CMakeLists.txt r446port/src/c_interface/CMakeLists.txt +--- stp/src/c_interface/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/c_interface/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,2 @@ ++file(GLOB SRCS *.h *.c*) ++add_stp_library(c_interface, SRCS) +diff -Nur stp/src/extlib-constbv/CMakeLists.txt r446port/src/extlib-constbv/CMakeLists.txt +--- stp/src/extlib-constbv/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/extlib-constbv/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,2 @@ ++file(GLOB SRCS *.h *.c*) ++add_stp_library(constantbv, SRCS) +diff -Nur stp/src/main/main.cpp r446port/src/main/main.cpp +--- stp/src/main/main.cpp 2009-11-13 11:49:35.859375000 +0800 ++++ r446port/src/main/main.cpp 2009-12-07 12:51:46.000000000 +0800 +@@ -26,6 +26,11 @@ + exit(0); + } + ++#if 1 ++namespace BEEV{ ++ const std::string version = "1.00"; ++} ++#endif + + // Amount of memory to ask for at beginning of main. + static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; +@@ -44,12 +49,16 @@ + extern FILE *cvcin; + extern FILE *smtin; + +- // 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."); +- } ++ ++#if !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__) ++ // 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 // !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__) ++ + + + STPMgr * bm = new STPMgr(); +@@ -59,7 +68,9 @@ + ToSAT * tosat = new ToSAT(bm, simp); + AbsRefine_CounterExample * Ctr_Example = + new AbsRefine_CounterExample(bm, simp, arrayTransformer, tosat); +- itimerval timeout; ++#if !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__) ++ itimerval timeout; ++#endif // !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__) + + ParserBM = bm; + GlobalSTP = +@@ -145,12 +156,14 @@ + bm->UserFlags.num_absrefine = atoi(argv[++i]); + break; + case 'g': +- 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 = atoi(argv[++i]); +- setitimer(ITIMER_VIRTUAL, &timeout, NULL); ++#if !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__) ++ 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 = atoi(argv[++i]); ++ setitimer(ITIMER_VIRTUAL, &timeout, NULL); ++#endif // !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__) + break; + case 'h': + fprintf(stderr,usage,prog); +Files stp/src/parser/.parsePL.cpp.swp and r446port/src/parser/.parsePL.cpp.swp differ +Files stp/src/parser/.PL.y.swp and r446port/src/parser/.PL.y.swp differ +diff -Nur stp/src/parser/CMakeLists.txt r446port/src/parser/CMakeLists.txt +--- stp/src/parser/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/parser/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,11 @@ ++set(OUTFILES ${CMAKE_CURRENT_SOURCE_DIR}/lexCVC.cpp ${CMAKE_CURRENT_SOURCE_DIR}/lexSMT.cpp ++ ${CMAKE_CURRENT_SOURCE_DIR}/parseCVC.cpp ${CMAKE_CURRENT_SOURCE_DIR}/parseCVC_defs.h ++ ${CMAKE_CURRENT_SOURCE_DIR}/parseSMT.cpp ${CMAKE_CURRENT_SOURCE_DIR}/parseSMT_defs.h) ++ ++file(GLOB SRCS *.h *.c *.cpp) ++string(REGEX MATCH HasAstKindFile "lexCVC.(h|cpp)" ${SRCS}) ++if(NOT HasAstKindFile) ++ set(SRCS ${SRCS} ${OUTFILES}) ++endif(NOT HasAstKindFile) ++ ++add_stp_library(parser, SRCS) +diff -Nur stp/src/parser/CVC.lex r446port/src/parser/CVC.lex +--- stp/src/parser/CVC.lex 2009-11-17 09:20:17.484375000 +0800 ++++ r446port/src/parser/CVC.lex 2009-12-07 12:51:46.000000000 +0800 +@@ -15,6 +15,9 @@ + using namespace BEEV; + extern char *yytext; + extern int cvcerror (const char *msg); ++#ifdef _MSC_VER ++ #include ++#endif + %} + + %option noyywrap +diff -Nur stp/src/parser/smtlib.lex r446port/src/parser/smtlib.lex +--- stp/src/parser/smtlib.lex 2009-10-21 13:36:04.937500000 +0800 ++++ r446port/src/parser/smtlib.lex 2009-12-07 12:51:46.000000000 +0800 +@@ -36,7 +36,9 @@ + #include + #include "parser.h" + #include "parseSMT_defs.h" +- ++#ifdef _MSC_VER ++ #include ++#endif + using namespace std; + using namespace BEEV; + +diff -Nur stp/src/printer/CMakeLists.txt r446port/src/printer/CMakeLists.txt +--- stp/src/printer/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/printer/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,2 @@ ++file(GLOB SRCS *.h *.c*) ++add_stp_library(printer, SRCS) +diff -Nur stp/src/sat/CMakeLists.txt r446port/src/sat/CMakeLists.txt +--- stp/src/sat/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/sat/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,2 @@ ++add_subdirectory(cryptominisat) ++add_stp_library(the_sat, SRCS) +diff -Nur stp/src/sat/cryptominisat/clause.cpp r446port/src/sat/cryptominisat/clause.cpp +--- stp/src/sat/cryptominisat/clause.cpp 2009-10-30 09:23:32.671875000 +0800 ++++ r446port/src/sat/cryptominisat/clause.cpp 2009-12-07 12:51:46.000000000 +0800 +@@ -24,14 +24,16 @@ + + Clause* Clause_new(const vec& ps, const uint group, const bool learnt) + { +- void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); ++ size_t msiz = sizeof(Clause) + sizeof(Lit)* (ps.size() ? (ps.size() - 1) : 0); ++ void* mem = malloc(msiz); + Clause* real= new (mem) Clause(ps, group, learnt); + return real; + } + + Clause* Clause_new(const vector& ps, const uint group, const bool learnt) + { +- void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); ++ size_t msiz = sizeof(Clause) + sizeof(Lit)* (ps.size() ? (ps.size() - 1) : 0); ++ void* mem = malloc(msiz); + Clause* real= new (mem) Clause(ps, group, learnt); + return real; + } +@@ -39,6 +41,8 @@ + #ifdef USE_GAUSS + Clause* Clause_new(const mpz_class& ps, const vec& assigns, const vector& col_to_var_original, const uint group, const bool learnt) + { ++ size_t msiz = sizeof(Clause) + sizeof(Lit)* (ps.size() ? (ps.size() - 1) : 0); ++ void* mem = malloc(msiz); + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + Clause* real= new (mem) Clause(ps, assigns, col_to_var_original, group, learnt); + return real; +diff -Nur stp/src/sat/cryptominisat/clause.h r446port/src/sat/cryptominisat/clause.h +--- stp/src/sat/cryptominisat/clause.h 2009-11-11 15:22:26.619365500 +0800 ++++ r446port/src/sat/cryptominisat/clause.h 2009-12-07 12:51:46.000000000 +0800 +@@ -49,7 +49,7 @@ + protected: + uint32_t size_etc; + float act; +- Lit data[0]; ++ Lit data[1]; + + public: + Clause(const vec& ps, const uint _group, const bool learnt) : +diff -Nur stp/src/sat/cryptominisat/CMakeLists.txt r446port/src/sat/cryptominisat/CMakeLists.txt +--- stp/src/sat/cryptominisat/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/sat/cryptominisat/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,3 @@ ++file(GLOB SRCS *.h *.c*) ++#add_library(minisat STATIC ${SRCS}) ++add_stp_library(minisat, SRCS) +diff -Nur stp/src/sat/cryptominisat/Solver.h r446port/src/sat/cryptominisat/Solver.h +--- stp/src/sat/cryptominisat/Solver.h 2009-10-30 09:23:32.656250000 +0800 ++++ r446port/src/sat/cryptominisat/Solver.h 2009-12-07 12:51:46.000000000 +0800 +@@ -31,7 +31,7 @@ + #include "clause.h" + #include + +-#ifdef _MSC_VER ++#if defined(_MSC_VER) || defined(__MINGW32__) || defined(__MINGW64__) + #include + #else + #include +diff -Nur stp/src/sat/mtl/Sort.h r446port/src/sat/mtl/Sort.h +--- stp/src/sat/mtl/Sort.h 2009-10-30 09:23:32.937500000 +0800 ++++ r446port/src/sat/mtl/Sort.h 2009-12-07 12:51:46.000000000 +0800 +@@ -86,7 +86,7 @@ + + + template void sort(vec& v, LessThan lt) { +- sort((T*)v, v.size(), lt); } ++ sort(v.getData(), v.size(), lt); } + template void sort(vec& v) { + sort(v, LessThan_default()); } + +diff -Nur stp/src/simplifier/CMakeLists.txt r446port/src/simplifier/CMakeLists.txt +--- stp/src/simplifier/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/simplifier/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,2 @@ ++file(GLOB SRCS *.h *.c*) ++add_stp_library(simplifier, SRCS) +diff -Nur stp/src/STPManager/CMakeLists.txt r446port/src/STPManager/CMakeLists.txt +--- stp/src/STPManager/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/STPManager/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,2 @@ ++file(GLOB SRCS *.h *.c*) ++add_stp_library(STPManager, SRCS) +diff -Nur stp/src/STPManager/STPManager.h r446port/src/STPManager/STPManager.h +--- stp/src/STPManager/STPManager.h 2009-11-18 10:56:12.484375000 +0800 ++++ r446port/src/STPManager/STPManager.h 2009-12-07 12:51:46.000000000 +0800 +@@ -13,6 +13,9 @@ + #include "UserDefinedFlags.h" + #include "../AST/AST.h" + #include "../parser/let-funcs.h" ++#if defined(_MSC_VER) ++ #include ++#endif + + namespace BEEV + { +diff -Nur stp/src/to-sat/BitBlast.cpp r446port/src/to-sat/BitBlast.cpp +--- stp/src/to-sat/BitBlast.cpp 2009-11-11 15:22:27.213107900 +0800 ++++ r446port/src/to-sat/BitBlast.cpp 2009-12-07 12:51:46.000000000 +0800 +@@ -1019,14 +1019,12 @@ + // left shift x (destructively) within width. loop backwards so + // that copy to self works correctly. (DON'T use STL insert!) + ASTVec::iterator xbeg = x.begin(); +- ASTVec::iterator xit = x.end() - 1; +- for (; xit >= xbeg; xit--) +- { +- if (xit - shift >= xbeg) +- *xit = *(xit - shift); +- else +- *xit = ASTFalse; // new LSB is zero. +- } ++ ASTVec::iterator xend = x.end(); ++ ASTVec::iterator semi_end = xbeg + shift; ++ if ( semi_end < xend ) { ++ copy_backward(xbeg, xend - shift, x.end()); ++ } ++ fill(xbeg, min(semi_end, x.end()), ASTFalse); + } + + // Right shift within fixed field inserting zeros at MSB. +diff -Nur stp/src/to-sat/CMakeLists.txt r446port/src/to-sat/CMakeLists.txt +--- stp/src/to-sat/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800 ++++ r446port/src/to-sat/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800 +@@ -0,0 +1,2 @@ ++file(GLOB SRCS *.h *.c*) ++add_stp_library(to-sat, SRCS) diff --git a/windows/winports/compdep.h b/windows/winports/compdep.h new file mode 100644 index 0000000..912aa93 --- /dev/null +++ b/windows/winports/compdep.h @@ -0,0 +1,19 @@ +#ifndef __COMPDEP_H__ +#define __COMPDEP_H__ 1 + +//some compiler related functions for porting +/************************************************************************/ +#ifdef _MSC_VER +#include +// msvc missed the log2 function +inline long double log2(long double x) +{ + return log(x)/log((long double)2); +} +// strtoull is missing too +#define strtoull _strtoui64 +#endif + +/************************************************************************/ +#endif + diff --git a/windows/winports/msc99hdr/inttypes.h b/windows/winports/msc99hdr/inttypes.h new file mode 100644 index 0000000..4b3828a --- /dev/null +++ b/windows/winports/msc99hdr/inttypes.h @@ -0,0 +1,305 @@ +// ISO C9x compliant inttypes.h for Microsoft Visual Studio +// Based on ISO/IEC 9899:TC2 Committee draft (May 6, 2005) WG14/N1124 +// +// Copyright (c) 2006 Alexander Chemeris +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions are met: +// +// 1. Redistributions of source code must retain the above copyright notice, +// this list of conditions and the following disclaimer. +// +// 2. Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// +// 3. The name of the author may be used to endorse or promote products +// derived from this software without specific prior written permission. +// +// THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED +// WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +// MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO +// EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; +// OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, +// WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR +// OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF +// ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +// +/////////////////////////////////////////////////////////////////////////////// + +#ifndef _MSC_VER // [ +#error "Use this header only with Microsoft Visual C++ compilers!" +#endif // _MSC_VER ] + +#ifndef _MSC_INTTYPES_H_ // [ +#define _MSC_INTTYPES_H_ + +#if _MSC_VER > 1000 +#pragma once +#endif + +#include "stdint.h" + +// 7.8 Format conversion of integer types + +typedef struct { + intmax_t quot; + intmax_t rem; +} imaxdiv_t; + +// 7.8.1 Macros for format specifiers + +#if !defined(__cplusplus) || defined(__STDC_FORMAT_MACROS) // [ See footnote 185 at page 198 + +// The fprintf macros for signed integers are: +#define PRId8 "d" +#define PRIi8 "i" +#define PRIdLEAST8 "d" +#define PRIiLEAST8 "i" +#define PRIdFAST8 "d" +#define PRIiFAST8 "i" + +#define PRId16 "hd" +#define PRIi16 "hi" +#define PRIdLEAST16 "hd" +#define PRIiLEAST16 "hi" +#define PRIdFAST16 "hd" +#define PRIiFAST16 "hi" + +#define PRId32 "I32d" +#define PRIi32 "I32i" +#define PRIdLEAST32 "I32d" +#define PRIiLEAST32 "I32i" +#define PRIdFAST32 "I32d" +#define PRIiFAST32 "I32i" + +#define PRId64 "I64d" +#define PRIi64 "I64i" +#define PRIdLEAST64 "I64d" +#define PRIiLEAST64 "I64i" +#define PRIdFAST64 "I64d" +#define PRIiFAST64 "I64i" + +#define PRIdMAX "I64d" +#define PRIiMAX "I64i" + +#define PRIdPTR "Id" +#define PRIiPTR "Ii" + +// The fprintf macros for unsigned integers are: +#define PRIo8 "o" +#define PRIu8 "u" +#define PRIx8 "x" +#define PRIX8 "X" +#define PRIoLEAST8 "o" +#define PRIuLEAST8 "u" +#define PRIxLEAST8 "x" +#define PRIXLEAST8 "X" +#define PRIoFAST8 "o" +#define PRIuFAST8 "u" +#define PRIxFAST8 "x" +#define PRIXFAST8 "X" + +#define PRIo16 "ho" +#define PRIu16 "hu" +#define PRIx16 "hx" +#define PRIX16 "hX" +#define PRIoLEAST16 "ho" +#define PRIuLEAST16 "hu" +#define PRIxLEAST16 "hx" +#define PRIXLEAST16 "hX" +#define PRIoFAST16 "ho" +#define PRIuFAST16 "hu" +#define PRIxFAST16 "hx" +#define PRIXFAST16 "hX" + +#define PRIo32 "I32o" +#define PRIu32 "I32u" +#define PRIx32 "I32x" +#define PRIX32 "I32X" +#define PRIoLEAST32 "I32o" +#define PRIuLEAST32 "I32u" +#define PRIxLEAST32 "I32x" +#define PRIXLEAST32 "I32X" +#define PRIoFAST32 "I32o" +#define PRIuFAST32 "I32u" +#define PRIxFAST32 "I32x" +#define PRIXFAST32 "I32X" + +#define PRIo64 "I64o" +#define PRIu64 "I64u" +#define PRIx64 "I64x" +#define PRIX64 "I64X" +#define PRIoLEAST64 "I64o" +#define PRIuLEAST64 "I64u" +#define PRIxLEAST64 "I64x" +#define PRIXLEAST64 "I64X" +#define PRIoFAST64 "I64o" +#define PRIuFAST64 "I64u" +#define PRIxFAST64 "I64x" +#define PRIXFAST64 "I64X" + +#define PRIoMAX "I64o" +#define PRIuMAX "I64u" +#define PRIxMAX "I64x" +#define PRIXMAX "I64X" + +#define PRIoPTR "Io" +#define PRIuPTR "Iu" +#define PRIxPTR "Ix" +#define PRIXPTR "IX" + +// The fscanf macros for signed integers are: +#define SCNd8 "d" +#define SCNi8 "i" +#define SCNdLEAST8 "d" +#define SCNiLEAST8 "i" +#define SCNdFAST8 "d" +#define SCNiFAST8 "i" + +#define SCNd16 "hd" +#define SCNi16 "hi" +#define SCNdLEAST16 "hd" +#define SCNiLEAST16 "hi" +#define SCNdFAST16 "hd" +#define SCNiFAST16 "hi" + +#define SCNd32 "ld" +#define SCNi32 "li" +#define SCNdLEAST32 "ld" +#define SCNiLEAST32 "li" +#define SCNdFAST32 "ld" +#define SCNiFAST32 "li" + +#define SCNd64 "I64d" +#define SCNi64 "I64i" +#define SCNdLEAST64 "I64d" +#define SCNiLEAST64 "I64i" +#define SCNdFAST64 "I64d" +#define SCNiFAST64 "I64i" + +#define SCNdMAX "I64d" +#define SCNiMAX "I64i" + +#ifdef _WIN64 // [ +# define SCNdPTR "I64d" +# define SCNiPTR "I64i" +#else // _WIN64 ][ +# define SCNdPTR "ld" +# define SCNiPTR "li" +#endif // _WIN64 ] + +// The fscanf macros for unsigned integers are: +#define SCNo8 "o" +#define SCNu8 "u" +#define SCNx8 "x" +#define SCNX8 "X" +#define SCNoLEAST8 "o" +#define SCNuLEAST8 "u" +#define SCNxLEAST8 "x" +#define SCNXLEAST8 "X" +#define SCNoFAST8 "o" +#define SCNuFAST8 "u" +#define SCNxFAST8 "x" +#define SCNXFAST8 "X" + +#define SCNo16 "ho" +#define SCNu16 "hu" +#define SCNx16 "hx" +#define SCNX16 "hX" +#define SCNoLEAST16 "ho" +#define SCNuLEAST16 "hu" +#define SCNxLEAST16 "hx" +#define SCNXLEAST16 "hX" +#define SCNoFAST16 "ho" +#define SCNuFAST16 "hu" +#define SCNxFAST16 "hx" +#define SCNXFAST16 "hX" + +#define SCNo32 "lo" +#define SCNu32 "lu" +#define SCNx32 "lx" +#define SCNX32 "lX" +#define SCNoLEAST32 "lo" +#define SCNuLEAST32 "lu" +#define SCNxLEAST32 "lx" +#define SCNXLEAST32 "lX" +#define SCNoFAST32 "lo" +#define SCNuFAST32 "lu" +#define SCNxFAST32 "lx" +#define SCNXFAST32 "lX" + +#define SCNo64 "I64o" +#define SCNu64 "I64u" +#define SCNx64 "I64x" +#define SCNX64 "I64X" +#define SCNoLEAST64 "I64o" +#define SCNuLEAST64 "I64u" +#define SCNxLEAST64 "I64x" +#define SCNXLEAST64 "I64X" +#define SCNoFAST64 "I64o" +#define SCNuFAST64 "I64u" +#define SCNxFAST64 "I64x" +#define SCNXFAST64 "I64X" + +#define SCNoMAX "I64o" +#define SCNuMAX "I64u" +#define SCNxMAX "I64x" +#define SCNXMAX "I64X" + +#ifdef _WIN64 // [ +# define SCNoPTR "I64o" +# define SCNuPTR "I64u" +# define SCNxPTR "I64x" +# define SCNXPTR "I64X" +#else // _WIN64 ][ +# define SCNoPTR "lo" +# define SCNuPTR "lu" +# define SCNxPTR "lx" +# define SCNXPTR "lX" +#endif // _WIN64 ] + +#endif // __STDC_FORMAT_MACROS ] + +// 7.8.2 Functions for greatest-width integer types + +// 7.8.2.1 The imaxabs function +#define imaxabs _abs64 + +// 7.8.2.2 The imaxdiv function + +// This is modified version of div() function from Microsoft's div.c found +// in %MSVC.NET%\crt\src\div.c +#ifdef STATIC_IMAXDIV // [ +static +#else // STATIC_IMAXDIV ][ +_inline +#endif // STATIC_IMAXDIV ] +imaxdiv_t __cdecl imaxdiv(intmax_t numer, intmax_t denom) +{ + imaxdiv_t result; + + result.quot = numer / denom; + result.rem = numer % denom; + + if (numer < 0 && result.rem > 0) { + // did division wrong; must fix up + ++result.quot; + result.rem -= denom; + } + + return result; +} + +// 7.8.2.3 The strtoimax and strtoumax functions +#define strtoimax _strtoi64 +#define strtoumax _strtoui64 + +// 7.8.2.4 The wcstoimax and wcstoumax functions +#define wcstoimax _wcstoi64 +#define wcstoumax _wcstoui64 + + +#endif // _MSC_INTTYPES_H_ ] diff --git a/windows/winports/msc99hdr/stdbool.h b/windows/winports/msc99hdr/stdbool.h new file mode 100644 index 0000000..d23f066 --- /dev/null +++ b/windows/winports/msc99hdr/stdbool.h @@ -0,0 +1,46 @@ +/* + * Copyright (c) 2000 Jeroen Ruigrok van der Werven + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + * + */ +/* + tested Under MSVC 9.0 only hume@gmail.com + */ +#ifndef _STDBOOL_H_ +#define _STDBOOL_H_ + +#define __bool_true_false_are_defined 1 + +#ifndef __cplusplus + +#define false 0 +#define true 1 + +#define bool _Bool +#if (__STDC_VERSION__ < 199901L && __GNUC__ < 3) || defined(_MSC_VER) +typedef int _Bool; +#endif + +#endif /* !__cplusplus */ +#endif /* !_STDBOOL_H_ */ diff --git a/windows/winports/msc99hdr/stdint.h b/windows/winports/msc99hdr/stdint.h new file mode 100644 index 0000000..d02608a --- /dev/null +++ b/windows/winports/msc99hdr/stdint.h @@ -0,0 +1,247 @@ +// ISO C9x compliant stdint.h for Microsoft Visual Studio +// Based on ISO/IEC 9899:TC2 Committee draft (May 6, 2005) WG14/N1124 +// +// Copyright (c) 2006-2008 Alexander Chemeris +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions are met: +// +// 1. Redistributions of source code must retain the above copyright notice, +// this list of conditions and the following disclaimer. +// +// 2. Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// +// 3. The name of the author may be used to endorse or promote products +// derived from this software without specific prior written permission. +// +// THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED +// WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +// MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO +// EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; +// OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, +// WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR +// OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF +// ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +// +/////////////////////////////////////////////////////////////////////////////// + +#ifndef _MSC_VER // [ +#error "Use this header only with Microsoft Visual C++ compilers!" +#endif // _MSC_VER ] + +#ifndef _MSC_STDINT_H_ // [ +#define _MSC_STDINT_H_ + +#if _MSC_VER > 1000 +#pragma once +#endif + +#include + +// For Visual Studio 6 in C++ mode and for many Visual Studio versions when +// compiling for ARM we should wrap include with 'extern "C++" {}' +// or compiler give many errors like this: +// error C2733: second C linkage of overloaded function 'wmemchr' not allowed +#ifdef __cplusplus +extern "C" { +#endif +# include +#ifdef __cplusplus +} +#endif + +// Define _W64 macros to mark types changing their size, like intptr_t. +#ifndef _W64 +# if !defined(__midl) && (defined(_X86_) || defined(_M_IX86)) && _MSC_VER >= 1300 +# define _W64 __w64 +# else +# define _W64 +# endif +#endif + + +// 7.18.1 Integer types + +// 7.18.1.1 Exact-width integer types + +// Visual Studio 6 and Embedded Visual C++ 4 doesn't +// realize that, e.g. char has the same size as __int8 +// so we give up on __intX for them. +#if (_MSC_VER < 1300) + typedef signed char int8_t; + typedef signed short int16_t; + typedef signed int int32_t; + typedef unsigned char uint8_t; + typedef unsigned short uint16_t; + typedef unsigned int uint32_t; +#else + typedef signed __int8 int8_t; + typedef signed __int16 int16_t; + typedef signed __int32 int32_t; + typedef unsigned __int8 uint8_t; + typedef unsigned __int16 uint16_t; + typedef unsigned __int32 uint32_t; +#endif +typedef signed __int64 int64_t; +typedef unsigned __int64 uint64_t; + + +// 7.18.1.2 Minimum-width integer types +typedef int8_t int_least8_t; +typedef int16_t int_least16_t; +typedef int32_t int_least32_t; +typedef int64_t int_least64_t; +typedef uint8_t uint_least8_t; +typedef uint16_t uint_least16_t; +typedef uint32_t uint_least32_t; +typedef uint64_t uint_least64_t; + +// 7.18.1.3 Fastest minimum-width integer types +typedef int8_t int_fast8_t; +typedef int16_t int_fast16_t; +typedef int32_t int_fast32_t; +typedef int64_t int_fast64_t; +typedef uint8_t uint_fast8_t; +typedef uint16_t uint_fast16_t; +typedef uint32_t uint_fast32_t; +typedef uint64_t uint_fast64_t; + +// 7.18.1.4 Integer types capable of holding object pointers +#ifdef _WIN64 // [ + typedef signed __int64 intptr_t; + typedef unsigned __int64 uintptr_t; +#else // _WIN64 ][ + typedef _W64 signed int intptr_t; + typedef _W64 unsigned int uintptr_t; +#endif // _WIN64 ] + +// 7.18.1.5 Greatest-width integer types +typedef int64_t intmax_t; +typedef uint64_t uintmax_t; + + +// 7.18.2 Limits of specified-width integer types + +#if !defined(__cplusplus) || defined(__STDC_LIMIT_MACROS) // [ See footnote 220 at page 257 and footnote 221 at page 259 + +// 7.18.2.1 Limits of exact-width integer types +#define INT8_MIN ((int8_t)_I8_MIN) +#define INT8_MAX _I8_MAX +#define INT16_MIN ((int16_t)_I16_MIN) +#define INT16_MAX _I16_MAX +#define INT32_MIN ((int32_t)_I32_MIN) +#define INT32_MAX _I32_MAX +#define INT64_MIN ((int64_t)_I64_MIN) +#define INT64_MAX _I64_MAX +#define UINT8_MAX _UI8_MAX +#define UINT16_MAX _UI16_MAX +#define UINT32_MAX _UI32_MAX +#define UINT64_MAX _UI64_MAX + +// 7.18.2.2 Limits of minimum-width integer types +#define INT_LEAST8_MIN INT8_MIN +#define INT_LEAST8_MAX INT8_MAX +#define INT_LEAST16_MIN INT16_MIN +#define INT_LEAST16_MAX INT16_MAX +#define INT_LEAST32_MIN INT32_MIN +#define INT_LEAST32_MAX INT32_MAX +#define INT_LEAST64_MIN INT64_MIN +#define INT_LEAST64_MAX INT64_MAX +#define UINT_LEAST8_MAX UINT8_MAX +#define UINT_LEAST16_MAX UINT16_MAX +#define UINT_LEAST32_MAX UINT32_MAX +#define UINT_LEAST64_MAX UINT64_MAX + +// 7.18.2.3 Limits of fastest minimum-width integer types +#define INT_FAST8_MIN INT8_MIN +#define INT_FAST8_MAX INT8_MAX +#define INT_FAST16_MIN INT16_MIN +#define INT_FAST16_MAX INT16_MAX +#define INT_FAST32_MIN INT32_MIN +#define INT_FAST32_MAX INT32_MAX +#define INT_FAST64_MIN INT64_MIN +#define INT_FAST64_MAX INT64_MAX +#define UINT_FAST8_MAX UINT8_MAX +#define UINT_FAST16_MAX UINT16_MAX +#define UINT_FAST32_MAX UINT32_MAX +#define UINT_FAST64_MAX UINT64_MAX + +// 7.18.2.4 Limits of integer types capable of holding object pointers +#ifdef _WIN64 // [ +# define INTPTR_MIN INT64_MIN +# define INTPTR_MAX INT64_MAX +# define UINTPTR_MAX UINT64_MAX +#else // _WIN64 ][ +# define INTPTR_MIN INT32_MIN +# define INTPTR_MAX INT32_MAX +# define UINTPTR_MAX UINT32_MAX +#endif // _WIN64 ] + +// 7.18.2.5 Limits of greatest-width integer types +#define INTMAX_MIN INT64_MIN +#define INTMAX_MAX INT64_MAX +#define UINTMAX_MAX UINT64_MAX + +// 7.18.3 Limits of other integer types + +#ifdef _WIN64 // [ +# define PTRDIFF_MIN _I64_MIN +# define PTRDIFF_MAX _I64_MAX +#else // _WIN64 ][ +# define PTRDIFF_MIN _I32_MIN +# define PTRDIFF_MAX _I32_MAX +#endif // _WIN64 ] + +#define SIG_ATOMIC_MIN INT_MIN +#define SIG_ATOMIC_MAX INT_MAX + +#ifndef SIZE_MAX // [ +# ifdef _WIN64 // [ +# define SIZE_MAX _UI64_MAX +# else // _WIN64 ][ +# define SIZE_MAX _UI32_MAX +# endif // _WIN64 ] +#endif // SIZE_MAX ] + +// WCHAR_MIN and WCHAR_MAX are also defined in +#ifndef WCHAR_MIN // [ +# define WCHAR_MIN 0 +#endif // WCHAR_MIN ] +#ifndef WCHAR_MAX // [ +# define WCHAR_MAX _UI16_MAX +#endif // WCHAR_MAX ] + +#define WINT_MIN 0 +#define WINT_MAX _UI16_MAX + +#endif // __STDC_LIMIT_MACROS ] + + +// 7.18.4 Limits of other integer types + +#if !defined(__cplusplus) || defined(__STDC_CONSTANT_MACROS) // [ See footnote 224 at page 260 + +// 7.18.4.1 Macros for minimum-width integer constants + +#define INT8_C(val) val##i8 +#define INT16_C(val) val##i16 +#define INT32_C(val) val##i32 +#define INT64_C(val) val##i64 + +#define UINT8_C(val) val##ui8 +#define UINT16_C(val) val##ui16 +#define UINT32_C(val) val##ui32 +#define UINT64_C(val) val##ui64 + +// 7.18.4.2 Macros for greatest-width integer constants +#define INTMAX_C INT64_C +#define UINTMAX_C UINT64_C + +#endif // __STDC_CONSTANT_MACROS ] + + +#endif // _MSC_STDINT_H_ ] diff --git a/windows/winports/msc99hdr/unistd.h b/windows/winports/msc99hdr/unistd.h new file mode 100644 index 0000000..39e2ec6 --- /dev/null +++ b/windows/winports/msc99hdr/unistd.h @@ -0,0 +1,3 @@ +/* this is a in-place holder + +*/ diff --git a/windows/winports/sys/time.h b/windows/winports/sys/time.h new file mode 100644 index 0000000..ffae2dc --- /dev/null +++ b/windows/winports/sys/time.h @@ -0,0 +1,55 @@ +#ifndef __TIME_H__ +#define __TIME_H__ 1 +// C++ windows related time implementation +/************************************************************************/ +#if defined(_MSC_VER) + #include + #include < time.h > + + #if defined(_MSC_EXTENSIONS) + #define DELTA_EPOCH_IN_MICROSECS 11644473600000000Ui64 + #else + #define DELTA_EPOCH_IN_MICROSECS 11644473600000000ULL + #endif + + // windows missed gettimeofday function + struct timezone { + int tz_minuteswest; /* minutes W of Greenwich */ + int tz_dsttime; /* type of dst correction */ + }; + + inline int gettimeofday(struct timeval *tv, struct timezone *tz) { + FILETIME ft; + unsigned __int64 tmpres = 0; + static int tzflag; + + if (NULL != tv) { + GetSystemTimeAsFileTime(&ft); + + tmpres |= ft.dwHighDateTime; + tmpres <<= 32; + tmpres |= ft.dwLowDateTime; + + /*converting file time to unix epoch*/ + tmpres /= 10; /*convert into microseconds*/ + tmpres -= DELTA_EPOCH_IN_MICROSECS; + tv->tv_sec = (long)(tmpres / 1000000UL); + tv->tv_usec = (long)(tmpres % 1000000UL); + } + + if (NULL != tz) { + if (!tzflag) { + _tzset(); + tzflag++; + } + tz->tz_minuteswest = _timezone / 60; + tz->tz_dsttime = _daylight; + } + return 0; + } +#endif // defined(_MSC_VER) + + +/************************************************************************/ +#endif +