Use TMPDIR environment variable for temp files (#2849)

Previously, we were just writing temporary files to `/tmp/` but this
commit allows the user to use the `TMPDIR` environment variable to
determine which directory the temporary file should be written to. The
commit adds a helper function for this and also includes some minor
cleanup of existing code.

7 files changed, 114 insertions, 72 deletions

diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index 07589fd07..5d6641e49 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -120,32 +120,22 @@ void ClausalBitVectorProof::optimizeDratProof()
                     BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
   {
     Debug("bv::clausal") << "Optimizing DRAT" << std::endl;
-    char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
-    char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
-    char optDratFilename[] = "/tmp/cvc4-optimized-drat-XXXXXX";
-    char optFormulaFilename[] = "/tmp/cvc4-optimized-formula-XXXXXX";
-    int r;
-    r = mkstemp(formulaFilename);
-    AlwaysAssert(r > 0);
-    close(r);
-    r = mkstemp(dratFilename);
-    AlwaysAssert(r > 0);
-    close(r);
-    r = mkstemp(optDratFilename);
-    AlwaysAssert(r > 0);
-    close(r);
-    r = mkstemp(optFormulaFilename);
-    AlwaysAssert(r > 0);
-    close(r);
-
-    std::ofstream formStream(formulaFilename);
+    std::string formulaFilename("cvc4-dimacs-XXXXXX");
+    std::string dratFilename("cvc4-drat-XXXXXX");
+    std::string optDratFilename("cvc4-optimized-drat-XXXXXX");
+    std::string optFormulaFilename("cvc4-optimized-formula-XXXXXX");
+
+    std::fstream formStream = openTmpFile(&formulaFilename);
     printDimacs(formStream, d_clauses, d_originalClauseIndices);
     formStream.close();
 
-    std::ofstream dratStream(dratFilename);
+    std::fstream dratStream = openTmpFile(&dratFilename);
     dratStream << d_binaryDratProof.str();
     dratStream.close();
 
+    std::fstream optDratStream = openTmpFile(&optDratFilename);
+    std::fstream optFormulaStream = openTmpFile(&optFormulaFilename);
+
 #if CVC4_USE_DRAT2ER
     int dratTrimExitCode =
         drat2er::drat_trim::OptimizeWithDratTrim(formulaFilename,
@@ -164,17 +154,14 @@ void ClausalBitVectorProof::optimizeDratProof()
     d_binaryDratProof.str("");
     Assert(d_binaryDratProof.str().size() == 0);
 
-    std::ifstream lratStream(optDratFilename);
-    std::copy(std::istreambuf_iterator<char>(lratStream),
+    std::copy(std::istreambuf_iterator<char>(optDratStream),
               std::istreambuf_iterator<char>(),
               std::ostreambuf_iterator<char>(d_binaryDratProof));
 
     if (options::bvOptimizeSatProof()
         == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
     {
-      std::ifstream optFormulaStream{optFormulaFilename};
       std::vector<prop::SatClause> core = parseDimacs(optFormulaStream);
-      optFormulaStream.close();
 
       // Now we need to compute the clause indices for the UNSAT core. This is a
       // bit difficult because drat-trim may have reordered clauses, and/or
@@ -213,11 +200,13 @@ void ClausalBitVectorProof::optimizeDratProof()
       d_coreClauseIndices = d_originalClauseIndices;
     }
 
+    optFormulaStream.close();
+
     Assert(d_coreClauseIndices.size() > 0);
-    remove(formulaFilename);
-    remove(dratFilename);
-    remove(optDratFilename);
-    remove(optFormulaFilename);
+    remove(formulaFilename.c_str());
+    remove(dratFilename.c_str());
+    remove(optDratFilename.c_str());
+    remove(optFormulaFilename.c_str());
     Debug("bv::clausal") << "Optimized DRAT" << std::endl;
   }
   else
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 7b966f2c6..9952e6b3e 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -85,32 +85,22 @@ ErProof ErProof::fromBinaryDratProof(
     const std::vector<ClauseId>& usedIds,
     const std::string& dratBinary)
 {
-  std::ostringstream cmd;
-  char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
-  char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
-  char tracecheckFilename[] = "/tmp/cvc4-tracecheck-er-XXXXXX";
-
-  int r;
-  r = mkstemp(formulaFilename);
-  AlwaysAssert(r > 0);
-  close(r);
-  r = mkstemp(dratFilename);
-  AlwaysAssert(r > 0);
-  close(r);
-  r = mkstemp(tracecheckFilename);
-  AlwaysAssert(r > 0);
-  close(r);
+  std::string formulaFilename("cvc4-dimacs-XXXXXX");
+  std::string dratFilename("cvc4-drat-XXXXXX");
+  std::string tracecheckFilename("cvc4-tracecheck-er-XXXXXX");
 
   // Write the formula
-  std::ofstream formStream(formulaFilename);
+  std::fstream formStream = openTmpFile(&formulaFilename);
   printDimacs(formStream, clauses, usedIds);
   formStream.close();
 
   // Write the (binary) DRAT proof
-  std::ofstream dratStream(dratFilename);
+  std::fstream dratStream = openTmpFile(&dratFilename);
   dratStream << dratBinary;
   dratStream.close();
 
+  std::fstream tracecheckStream = openTmpFile(&tracecheckFilename);
+
   // Invoke drat2er
 #if CVC4_USE_DRAT2ER
   drat2er::TransformDRATToExtendedResolution(formulaFilename,
@@ -119,7 +109,6 @@ ErProof ErProof::fromBinaryDratProof(
                                              false,
                                              drat2er::options::QUIET,
                                              false);
-
 #else
   Unimplemented(
       "ER proof production requires drat2er.\n"
@@ -127,14 +116,13 @@ ErProof ErProof::fromBinaryDratProof(
 #endif
 
   // Parse the resulting TRACECHECK proof into an ER proof.
-  std::ifstream tracecheckStream(tracecheckFilename);
   TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream);
   ErProof proof(clauses, usedIds, std::move(pf));
   tracecheckStream.close();
 
-  remove(formulaFilename);
-  remove(dratFilename);
-  remove(tracecheckFilename);
+  remove(formulaFilename.c_str());
+  remove(dratFilename.c_str());
+  remove(tracecheckFilename.c_str());
 
   return proof;
 }
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index e414c64c9..d2f347807 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -28,6 +28,7 @@
 #include "base/output.h"
 #include "proof/dimacs.h"
 #include "proof/lfsc_proof_printer.h"
+#include "util/utility.h"
 
 #if CVC4_USE_DRAT2ER
 #include "drat2er_options.h"
@@ -129,27 +130,20 @@ LratProof LratProof::fromDratProof(
     const std::string& dratBinary)
 {
   std::ostringstream cmd;
-  char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
-  char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
-  char lratFilename[] = "/tmp/cvc4-lrat-XXXXXX";
-  int r;
-  r = mkstemp(formulaFilename);
-  AlwaysAssert(r > 0);
-  close(r);
-  r = mkstemp(dratFilename);
-  AlwaysAssert(r > 0);
-  close(r);
-  r = mkstemp(lratFilename);
-  AlwaysAssert(r > 0);
-  close(r);
-  std::ofstream formStream(formulaFilename);
+  std::string formulaFilename("cvc4-dimacs-XXXXXX");
+  std::string dratFilename("cvc4-drat-XXXXXX");
+  std::string lratFilename("cvc4-lrat-XXXXXX");
+
+  std::fstream formStream = openTmpFile(&formulaFilename);
   printDimacs(formStream, clauses, usedIds);
   formStream.close();
 
-  std::ofstream dratStream(dratFilename);
+  std::fstream dratStream = openTmpFile(&dratFilename);
   dratStream << dratBinary;
   dratStream.close();
 
+  std::fstream lratStream = openTmpFile(&lratFilename);
+
 #if CVC4_USE_DRAT2ER
   drat2er::drat_trim::CheckAndConvertToLRAT(
       formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET);
@@ -159,11 +153,10 @@ LratProof LratProof::fromDratProof(
       "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
 #endif
 
-  std::ifstream lratStream(lratFilename);
   LratProof lrat(lratStream);
-  remove(formulaFilename);
-  remove(dratFilename);
-  remove(lratFilename);
+  remove(formulaFilename.c_str());
+  remove(dratFilename.c_str());
+  remove(lratFilename.c_str());
   return lrat;
 }
 
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index a17f7c510..f107ad95f 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -47,6 +47,7 @@ libcvc4_add_sources(
   statistics_registry.h
   tuple.h
   unsafe_interrupt_exception.h
+  utility.cpp
   utility.h
 )
 
diff --git a/src/util/utility.cpp b/src/util/utility.cpp
new file mode 100644
index 000000000..9936504d2
--- /dev/null
+++ b/src/util/utility.cpp
@@ -0,0 +1,56 @@
+/*********************                                                        */
+/*! \file utility.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Some standard STL-related utility functions for CVC4
+ **
+ ** Some standard STL-related utility functions for CVC4.
+ **/
+
+#include "util/utility.h"
+
+#include <unistd.h>
+
+#include <cstdlib>
+#include <iostream>
+
+#include "base/cvc4_check.h"
+
+namespace CVC4 {
+
+std::fstream openTmpFile(std::string* pattern)
+{
+  char* tmpDir = getenv("TMPDIR");
+  if (tmpDir != nullptr)
+  {
+    *pattern = std::string(tmpDir) + "/" + *pattern;
+  }
+  else
+  {
+    *pattern = "/tmp/" + *pattern;
+  }
+
+  // Note: With C++17, we can avoid creating a copy using std::string::data().
+  char* tmpName = new char[pattern->size() + 1];
+  pattern->copy(tmpName, pattern->size());
+  tmpName[pattern->size()] = '\0';
+  int r = mkstemp(tmpName);
+  if (r == -1)
+  {
+    CVC4_FATAL() << "Could not create temporary file " << *pattern;
+  }
+  std::fstream tmpStream(tmpName);
+  close(r);
+  *pattern = std::string(tmpName);
+  delete[] tmpName;
+  return tmpStream;
+}
+
+}  // namespace CVC4
diff --git a/src/util/utility.h b/src/util/utility.h
index 275efd9d0..a606648bd 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -20,8 +20,10 @@
 #define CVC4__UTILITY_H
 
 #include <algorithm>
-#include <utility>
+#include <fstream>
 #include <functional>
+#include <string>
+#include <utility>
 
 namespace CVC4 {
 
@@ -85,6 +87,18 @@ void container_to_stream(std::ostream& out,
   out << postfix;
 }
 
+/**
+ * Opens a new temporary file with a given filename pattern and returns an
+ * fstream to it. The directory that the file is created in is either TMPDIR or
+ * /tmp/ if TMPDIR is not set.
+ *
+ * @param pattern The filename pattern. This string is modified to contain the
+ * name of the temporary file.
+ *
+ * @return A filestream for the temporary file.
+ */
+std::fstream openTmpFile(std::string* pattern);
+
 }/* CVC4 namespace */
 
 #endif /* CVC4__UTILITY_H */
diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h
index 398c551fe..b4b41922f 100644
--- a/test/unit/proof/lrat_proof_black.h
+++ b/test/unit/proof/lrat_proof_black.h
@@ -22,10 +22,11 @@
 #include "prop/sat_solver_types.h"
 #include "utils.h"
 
+using namespace CVC4;
 using namespace CVC4::proof::lrat;
 using namespace CVC4::prop;
 
-class LfscProofBlack : public CxxTest::TestSuite
+class LratProofBlack : public CxxTest::TestSuite
 {
  public:
   void setUp() override {}
@@ -34,7 +35,7 @@ class LfscProofBlack : public CxxTest::TestSuite
   void testOutputAsLfsc();
 };
 
-void LfscProofBlack::testOutputAsLfsc()
+void LratProofBlack::testOutputAsLfsc()
 {
   std::vector<std::unique_ptr<LratInstruction>> instructions;