Build and test suite fixes for Windows (#186)

- Build fixes for Windows
- Make proof checking tempfile handling portable
- Test suite fixes for Windows

5 files changed, 49 insertions, 18 deletions

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 <io.h>
+#endif
+#include <sys/types.h>
+#include <sys/stat.h>
+#include <fcntl.h>
 #include <unistd.h>
 
 #include <cstdlib>
@@ -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"`