From 65af88c6392f90d8e18ebe3957226b837e617581 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 6 Mar 2019 13:26:43 -0800 Subject: Use TMPDIR environment variable for temp files Previosuly, 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. --- src/proof/clausal_bitvector_proof.cpp | 33 +++++++++------------ src/proof/er/er_proof.cpp | 33 +++++++++------------ src/proof/lrat/lrat_proof.cpp | 33 +++++++++------------ src/proof/lrat/lrat_proof.h | 4 --- src/util/CMakeLists.txt | 1 + src/util/utility.cpp | 54 +++++++++++++++++++++++++++++++++++ src/util/utility.h | 16 ++++++++++- test/unit/proof/lrat_proof_black.h | 5 ++-- 8 files changed, 114 insertions(+), 65 deletions(-) create mode 100644 src/util/utility.cpp diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp index 25e519bfb..9e45bb42b 100644 --- a/src/proof/clausal_bitvector_proof.cpp +++ b/src/proof/clausal_bitvector_proof.cpp @@ -29,6 +29,7 @@ #include "proof/lfsc_proof_printer.h" #include "proof/lrat/lrat_proof.h" #include "theory/bv/theory_bv.h" +#include "util/utility.h" #if CVC4_USE_DRAT2ER #include "drat2er_options.h" @@ -111,24 +112,17 @@ void ClausalBitVectorProof::calculateAtomsInBitblastingProof() void ClausalBitVectorProof::optimizeDratProof() { 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"; - 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); - std::ofstream formStream(formulaFilename); + std::string formulaFilename("cvc4-dimacs-XXXXXX"); + std::string dratFilename("cvc4-drat-XXXXXX"); + std::string optDratFilename("cvc4-optimized-drat-XXXXXX"); + + std::fstream formStream; + openTmpFile(&formStream, &formulaFilename); printDimacs(formStream, d_usedClauses); formStream.close(); - std::ofstream dratStream(dratFilename); + std::fstream dratStream; + openTmpFile(&dratStream, &dratFilename); dratStream << d_binaryDratProof.str(); dratStream.close(); @@ -144,13 +138,14 @@ void ClausalBitVectorProof::optimizeDratProof() d_binaryDratProof = std::ostringstream{}; Assert(d_binaryDratProof.str().size() == 0); - std::ifstream lratStream(optDratFilename); + std::fstream lratStream; + openTmpFile(&lratStream, &optDratFilename); std::copy(std::istreambuf_iterator(lratStream), std::istreambuf_iterator(), std::ostreambuf_iterator(d_binaryDratProof)); - remove(formulaFilename); - remove(dratFilename); - remove(optDratFilename); + remove(formulaFilename.c_str()); + remove(dratFilename.c_str()); + remove(optDratFilename.c_str()); Debug("bv::clausal") << "Optimized DRAT" << std::endl; } diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp index 7215312c7..9de48b018 100644 --- a/src/proof/er/er_proof.cpp +++ b/src/proof/er/er_proof.cpp @@ -34,6 +34,7 @@ #include "proof/dimacs_printer.h" #include "proof/lfsc_proof_printer.h" #include "proof/proof_manager.h" +#include "util/utility.h" #if CVC4_USE_DRAT2ER #include "drat2er.h" @@ -84,29 +85,20 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, 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("/tmp/cvc4-dimacs-XXXXXX"); + std::string dratFilename("/tmp/cvc4-drat-XXXXXX"); + std::string tracecheckFilename("/tmp/cvc4-tracecheck-er-XXXXXX"); // Write the formula - std::ofstream formStream(formulaFilename); + std::fstream formStream; + openTmpFile(&formStream, &formulaFilename); printDimacs(formStream, usedClauses); formStream.close(); // Write the (binary) DRAT proof - std::ofstream dratStream(dratFilename); + std::fstream dratStream; + openTmpFile(&dratStream, &dratFilename); dratStream << dratBinary; dratStream.close(); @@ -126,14 +118,15 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses, #endif // Parse the resulting TRACECHECK proof into an ER proof. - std::ifstream tracecheckStream(tracecheckFilename); + std::fstream tracecheckStream; + openTmpFile(&tracecheckStream, &tracecheckFilename); TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream); ErProof proof(usedClauses, std::move(pf)); tracecheckStream.close(); - unlink(formulaFilename); - unlink(dratFilename); - unlink(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 0b7af7aa5..ba93209d1 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_printer.h" #include "proof/lfsc_proof_printer.h" +#include "util/utility.h" #if CVC4_USE_DRAT2ER #include "drat2er_options.h" @@ -127,24 +128,17 @@ 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(&formStream, &formulaFilename); printDimacs(formStream, usedClauses); formStream.close(); - std::ofstream dratStream(dratFilename); + std::fstream dratStream; + openTmpFile(&dratStream, &dratFilename); dratStream << dratBinary; dratStream.close(); @@ -157,11 +151,12 @@ LratProof LratProof::fromDratProof( "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); #endif - std::ifstream lratStream(lratFilename); + std::fstream lratStream; + openTmpFile(&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/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h index a999e5ca6..7cd773409 100644 --- a/src/proof/lrat/lrat_proof.h +++ b/src/proof/lrat/lrat_proof.h @@ -130,10 +130,6 @@ class LratProof * @brief Construct an LRAT proof from a DRAT proof, using drat-trim * * @param usedClauses The CNF formula that we're deriving bottom from. - * It's a map because other parts of the system represent - * it this way. - * @param clauseOrder A record of the order in which those clauses were - * given to the SAT solver. * @param dratBinary The DRAT proof from the SAT solver, as a binary stream. */ static LratProof fromDratProof( 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..93c36d662 --- /dev/null +++ b/src/util/utility.cpp @@ -0,0 +1,54 @@ +/********************* */ +/*! \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 + +#include + +#include "base/cvc4_check.h" + +namespace CVC4 { + +void openTmpFile(std::fstream* stream, 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; + } + stream->open(tmpName); + close(r); + *pattern = std::string(tmpName); + delete[] tmpName; +} + +} // namespace CVC4 diff --git a/src/util/utility.h b/src/util/utility.h index 56a68ca40..524397ee6 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -20,8 +20,10 @@ #define __CVC4__UTILITY_H #include -#include +#include #include +#include +#include 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 A filestream for the temporary file. + * @param pattern The filename pattern. This string is modified to contain the + * name of the temporary file. + * + */ +void openTmpFile(std::fstream* stream, 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> instructions; -- cgit v1.2.3