From: Mark Laws Date: Mon, 14 Aug 2017 16:44:54 +0000 (+0900) Subject: Build and test suite fixes for Windows (#186) X-Git-Tag: cvc5-1.0.0~5682 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=93b2aef9e21adb05ec4a1aa2b0cf7fb39c408b51;p=cvc5.git Build and test suite fixes for Windows (#186) - Build fixes for Windows - Make proof checking tempfile handling portable - Test suite fixes for Windows --- diff --git a/src/Makefile.am b/src/Makefile.am index 847eecedc..151bcaaa6 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -25,7 +25,7 @@ include @top_srcdir@/src/Makefile.theories lib_LTLIBRARIES = libcvc4.la -libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) +libcvc4_la_LDFLAGS = -no-undefined -version-info $(LIBCVC4_VERSION) # This "tricks" automake into linking us as a C++ library (rather than # as a C library, which messes up exception handling support) diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index 9a336dd4d..f25dd5a51 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -15,6 +15,12 @@ ** \todo document this file **/ +#if defined(_MSC_VER) || defined(__MINGW32__) || defined(__MINGW64__) +#include +#endif +#include +#include +#include #include #include @@ -81,16 +87,24 @@ void SmtEngine::checkProof() { return; } - char const* tempDir = getenv("TMPDIR"); - if (!tempDir) { - tempDir = "/tmp"; + char *pfFile = tempnam(NULL, "cvc4_"); + if (!pfFile) { + Notice() << "Error: couldn't get path from tempnam() during proof checking" << endl; + return; + } +#if defined(_MSC_VER) || defined(__MINGW32__) || defined(__MINGW64__) + int fd = _open(pfFile, + _O_CREAT | _O_EXCL | _O_SHORT_LIVED | _O_RDWR, + _S_IREAD | _S_IWRITE); +#else + mode_t openmode = S_IRUSR | S_IWUSR; + int fd = open(pfFile, O_CREAT | O_EXCL | O_RDWR, openmode); +#endif + if (fd == -1) { + free(pfFile); + Notice() << "Error: failed to open temporary file during proof checking" << endl; + return; } - - stringstream pfPath; - pfPath << tempDir << "/cvc4_proof.XXXXXX"; - - char* pfFile = strdup(pfPath.str().c_str()); - int fd = mkstemp(pfFile); // ensure this temp file is removed after smt::UnlinkProofFile unlinker(pfFile); @@ -109,6 +123,7 @@ void SmtEngine::checkProof() { a.compile_lib = false; init(); check_file(pfFile, a); + free(pfFile); close(fd); #else /* IS_PROOFS_BUILD */ diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc index de4d8e1a7..8f76c798a 100644 --- a/test/regress/regress0/error.cvc +++ b/test/regress/regress0/error.cvc @@ -1,8 +1,7 @@ +% ERROR-SCRUBBER: sed -e '/^[[:space:]]*$/d' % EXPECT-ERROR: CVC4 Error: -% EXPECT-ERROR: Parse Error: error.cvc:7.8: Symbol 'BOOL' not declared as a type -% EXPECT-ERROR: +% EXPECT-ERROR: Parse Error: error.cvc:6.8: Symbol 'BOOL' not declared as a type % EXPECT-ERROR: p : BOOL; % EXPECT-ERROR: ^ -% EXPECT-ERROR: p : BOOL; % EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.06.cvc b/test/regress/regress0/expect/scrub.06.cvc index 2656c71b3..071a2278f 100644 --- a/test/regress/regress0/expect/scrub.06.cvc +++ b/test/regress/regress0/expect/scrub.06.cvc @@ -1,5 +1,5 @@ % COMMAND-LINE: --force-logic=QF_LRA -% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -e '/^$/d' +% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -e '/^[[:space:]]*$/d' % EXPECT: A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXIT: 1 diff --git a/test/regress/run_regression b/test/regress/run_regression index f6dc00b3f..536a3e8a5 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -94,6 +94,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then lang=smt1 if test -e "$benchmark.expect"; then scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'` + errscrubber=`grep '^% ERROR-SCRUBBER: ' "$benchmark.expect" | sed 's,^% ERROR-SCRUBBER: ,,'` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -101,8 +102,9 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then expected_exit_status=0 fi - elif grep '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then + elif grep '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\|ERROR-SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then scrubber=`grep '^% SCRUBBER: ' "$benchmark" | sed 's,^% SCRUBBER: ,,'` + errscrubber=`grep '^% ERROR-SCRUBBER: ' "$benchmark" | sed 's,^% ERROR-SCRUBBER: ,,'` expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -110,7 +112,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle # this frustrates our auto-language-detection gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX - grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" >"$tmpbenchmark" + grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\|ERROR-SCRUBBER\): ' "$benchmark" >"$tmpbenchmark" if [ -z "$expected_exit_status" ]; then expected_exit_status=0 fi @@ -130,6 +132,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then lang=smt2 if test -e "$benchmark.expect"; then scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'` + errscrubber=`grep '^% ERROR-SCRUBBER: ' "$benchmark.expect" | sed 's,^% ERROR-SCRUBBER: ,,'` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -137,8 +140,9 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then expected_exit_status=0 fi - elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then + elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\|ERROR-SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then scrubber=`grep '^; SCRUBBER: ' "$benchmark" | sed 's,^; SCRUBBER: ,,'` + errscrubber=`grep '^; ERROR-SCRUBBER: ' "$benchmark" | sed 's,^; ERROR-SCRUBBER: ,,'` expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'` expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'` @@ -160,6 +164,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then lang=cvc4 scrubber=`grep '^% SCRUBBER: ' "$benchmark" | sed 's,^% SCRUBBER: ,,'` + errscrubber=`grep '^% ERROR-SCRUBBER: ' "$benchmark" | sed 's,^% ERROR-SCRUBBER: ,,'` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then @@ -176,6 +181,7 @@ elif expr "$benchmark" : '.*\.p$' &>/dev/null; then lang=tptp command_line=--finite-model-find scrubber=`grep '^% SCRUBBER: ' "$benchmark" | sed 's,^% SCRUBBER: ,,'` + errscrubber=`grep '^% ERROR-SCRUBBER: ' "$benchmark" | sed 's,^% ERROR-SCRUBBER: ,,'` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then @@ -205,6 +211,7 @@ elif expr "$benchmark" : '.*\.sy$' &>/dev/null; then lang=sygus if test -e "$benchmark.expect"; then scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'` + errscrubber=`grep '^% ERROR-SCRUBBER: ' "$benchmark.expect" | sed 's,^% ERROR-SCRUBBER: ,,'` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -212,8 +219,9 @@ elif expr "$benchmark" : '.*\.sy$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then expected_exit_status=0 fi - elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then + elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\|ERROR-SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then scrubber=`grep '^; SCRUBBER: ' "$benchmark" | sed 's,^; SCRUBBER: ,,'` + errscrubber=`grep '^; ERROR-SCRUBBER: ' "$benchmark" | sed 's,^; ERROR-SCRUBBER: ,,'` expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'` expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'` @@ -339,6 +347,15 @@ else echo "not scrubbing" fi +# Scrub the error file if a scrubber has been specified. +if [ -n "$errscrubber" ]; then + echo "About to scrub $errfilefix using $errscrubber" + mv "$errfilefix" "$errfilefix.prescrub" + cat "$errfilefix.prescrub" | eval $errscrubber >"$errfilefix" +else + echo "not scrubbing error file" +fi + diffs=`diff -u --strip-trailing-cr "$expoutfile" "$outfile"` diffexit=$? diffserr=`diff -u --strip-trailing-cr "$experrfile" "$errfilefix"`