diff options
author | Julian Büning <julian.buening@rwth-aachen.de> | 2018-10-03 14:42:37 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-10-23 18:57:53 +0300 |
commit | 2b34877c5dbf24eabf331a124b1e68d901a72cba (patch) | |
tree | 4d6f4a753d9d36a18c482cf0c8d4b8dc550bafb8 /lib | |
parent | d032742a963e7d8e83dad509dd1c95b4e1a34436 (diff) | |
download | klee-2b34877c5dbf24eabf331a124b1e68d901a72cba.tar.gz |
refactor klee_open_output_file to return std::unique_ptr
and introduce klee_open_compressed_output_file with similar behavior along some other minor improvements
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 13 | ||||
-rw-r--r-- | lib/Core/Executor.h | 3 | ||||
-rw-r--r-- | lib/Core/ExecutorTimers.cpp | 21 | ||||
-rw-r--r-- | lib/Core/StatsTracker.cpp | 33 | ||||
-rw-r--r-- | lib/Core/StatsTracker.h | 17 | ||||
-rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 25 | ||||
-rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 2 | ||||
-rw-r--r-- | lib/Solver/Z3Solver.cpp | 12 | ||||
-rw-r--r-- | lib/Support/CompressionStream.cpp | 3 | ||||
-rw-r--r-- | lib/Support/FileHandling.cpp | 33 |
10 files changed, 79 insertions, 83 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 475beacb..0506b685 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -76,10 +76,6 @@ #include "llvm/IR/CallSite.h" #endif -#ifdef HAVE_ZLIB_H -#include "klee/Internal/Support/CompressionStream.h" -#endif - #include <cassert> #include <algorithm> #include <iomanip> @@ -336,7 +332,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0 ? std::min(MaxCoreSolverTime, MaxInstructionTime) : std::max(MaxCoreSolverTime, MaxInstructionTime)), - debugInstFile(0), debugLogBuffer(debugBufferString) { + debugLogBuffer(debugBufferString) { if (coreSolverTimeout) UseForkedCoreSolver = true; Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse); @@ -371,11 +367,11 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, debugInstFile = klee_open_output_file(debug_file_name, error); #ifdef HAVE_ZLIB_H } else { - debugInstFile = new compressed_fd_ostream( - (debug_file_name + ".gz").c_str(), error); + debug_file_name.append(".gz"); + debugInstFile = klee_open_compressed_output_file(debug_file_name, error); } #endif - if (!error.empty()) { + if (!debugInstFile) { klee_error("Could not open file %s : %s", debug_file_name.c_str(), error.c_str()); } @@ -455,7 +451,6 @@ Executor::~Executor() { delete timers.back(); timers.pop_back(); } - delete debugInstFile; } /***/ diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index d9e20f1e..3643c3f4 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -27,6 +27,7 @@ #include "../Expr/ArrayExprOptimizer.h" #include <map> +#include <memory> #include <set> #include <string> #include <vector> @@ -221,7 +222,7 @@ private: ArrayCache arrayCache; /// File to print executed instructions to - llvm::raw_ostream *debugInstFile; + std::unique_ptr<llvm::raw_ostream> debugInstFile; // @brief Buffer used by logBuffer std::string debugBufferString; diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index dd0d824e..a3c13530 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -116,28 +116,25 @@ void Executor::processTimers(ExecutionState *current, if (dumpPTree) { char name[32]; sprintf(name, "ptree%08d.dot", (int) stats::instructions); - llvm::raw_ostream *os = interpreterHandler->openOutputFile(name); + auto os = interpreterHandler->openOutputFile(name); if (os) { processTree->dump(*os); - delete os; } - + dumpPTree = 0; } if (dumpStates) { - llvm::raw_ostream *os = interpreterHandler->openOutputFile("states.txt"); - + auto os = interpreterHandler->openOutputFile("states.txt"); + if (os) { - for (std::set<ExecutionState*>::const_iterator it = states.begin(), - ie = states.end(); it != ie; ++it) { - ExecutionState *es = *it; + for (ExecutionState *es : states) { *os << "(" << es << ","; *os << "["; - ExecutionState::stack_ty::iterator next = es->stack.begin(); + auto next = es->stack.begin(); ++next; - for (ExecutionState::stack_ty::iterator sfIt = es->stack.begin(), - sf_ie = es->stack.end(); sfIt != sf_ie; ++sfIt) { + for (auto sfIt = es->stack.begin(), sf_ie = es->stack.end(); + sfIt != sf_ie; ++sfIt) { *os << "('" << sfIt->kf->function->getName().str() << "',"; if (next == es->stack.end()) { *os << es->prevPC->info->line << "), "; @@ -167,8 +164,6 @@ void Executor::processTimers(ExecutionState *current, *os << "}"; *os << ")\n"; } - - delete os; } dumpStates = 0; diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 6ad5b89f..dee14e61 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -176,8 +176,6 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, bool _updateMinDistToUncovered) : executor(_executor), objectFilename(_objectFilename), - statsFile(0), - istatsFile(0), startWallTime(util::getWallTime()), numBranches(0), fullBranches(0), @@ -243,12 +241,15 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, if (OutputStats) { statsFile = executor.interpreterHandler->openOutputFile("run.stats"); - assert(statsFile && "unable to open statistics trace file"); - writeStatsHeader(); - writeStatsLine(); + if (statsFile) { + writeStatsHeader(); + writeStatsLine(); - if (StatsWriteInterval > 0) - executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval); + if (StatsWriteInterval > 0) + executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval); + } else { + klee_error("Unable to open statistics trace file (run.stats)."); + } } // Add timer to calculate uncovered instructions if needed by the solver @@ -259,18 +260,15 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, if (OutputIStats) { istatsFile = executor.interpreterHandler->openOutputFile("run.istats"); - assert(istatsFile && "unable to open istats file"); - - if (IStatsWriteInterval > 0) - executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval); + if (istatsFile) { + if (IStatsWriteInterval > 0) + executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval); + } else { + klee_error("Unable to open instruction level stats file (run.istats)."); + } } } -StatsTracker::~StatsTracker() { - delete statsFile; - delete istatsFile; -} - void StatsTracker::done() { if (statsFile) writeStatsLine(); @@ -278,7 +276,8 @@ void StatsTracker::done() { if (OutputIStats) { if (updateMinDistToUncovered) computeReachableUncovered(); - writeIStats(); + if (istatsFile) + writeIStats(); } } diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h index 23abac06..e352bb91 100644 --- a/lib/Core/StatsTracker.h +++ b/lib/Core/StatsTracker.h @@ -12,6 +12,7 @@ #include "CallPathManager.h" +#include <memory> #include <set> namespace llvm { @@ -23,7 +24,7 @@ namespace llvm { namespace klee { class ExecutionState; - class Executor; + class Executor; class InstructionInfoTable; class InterpreterHandler; struct KInstruction; @@ -36,13 +37,13 @@ namespace klee { Executor &executor; std::string objectFilename; - llvm::raw_fd_ostream *statsFile, *istatsFile; + std::unique_ptr<llvm::raw_fd_ostream> statsFile, istatsFile; double startWallTime; - + unsigned numBranches; unsigned fullBranches, partialBranches; - CallPathManager callPathManager; + CallPathManager callPathManager; bool updateMinDistToUncovered; @@ -59,20 +60,20 @@ namespace klee { public: StatsTracker(Executor &_executor, std::string _objectFilename, bool _updateMinDistToUncovered); - ~StatsTracker(); + ~StatsTracker() = default; // called after a new StackFrame has been pushed (for callpath tracing) void framePushed(ExecutionState &es, StackFrame *parentFrame); - // called after a StackFrame has been popped + // called after a StackFrame has been popped void framePopped(ExecutionState &es); // called when some side of a branch has been visited. it is // imperative that this be called when the statistics index is at // the index for the branch itself. - void markBranchVisited(ExecutionState *visitedTrue, + void markBranchVisited(ExecutionState *visitedTrue, ExecutionState *visitedFalse); - + // called when execution is done and stats files should be flushed void done(); diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index 7e4d8fe0..0fb145d7 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -7,18 +7,11 @@ // //===----------------------------------------------------------------------===// #include "QueryLoggingSolver.h" -#include "klee/Config/config.h" -#include "klee/Internal/System/Time.h" #include "klee/Statistics.h" -#ifdef HAVE_ZLIB_H -#include "klee/Internal/Support/CompressionStream.h" +#include "klee/Config/config.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Internal/Support/FileHandling.h" -#endif - -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) -#include "llvm/Support/FileSystem.h" -#endif +#include "klee/Internal/System/Time.h" using namespace klee::util; @@ -37,9 +30,9 @@ llvm::cl::opt<bool> CreateCompressedQueryLog( QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, const std::string &commentSign, int queryTimeToLog) - : solver(_solver), os(0), BufferString(""), logBuffer(BufferString), - queryCount(0), minQueryTimeToLog(queryTimeToLog), startTime(0.0f), - lastQueryTime(0.0f), queryCommentSign(commentSign) { + : solver(_solver), BufferString(""), logBuffer(BufferString), queryCount(0), + minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f), + queryCommentSign(commentSign) { std::string error; #ifdef HAVE_ZLIB_H if (!CreateCompressedQueryLog) { @@ -47,18 +40,18 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, os = klee_open_output_file(path, error); #ifdef HAVE_ZLIB_H } else { - os = new compressed_fd_ostream((path + ".gz").c_str(), error); + path.append(".gz"); + os = klee_open_compressed_output_file(path, error); } - if (!error.empty()) { +#endif + if (!os) { klee_error("Could not open file %s : %s", path.c_str(), error.c_str()); } -#endif assert(0 != solver); } QueryLoggingSolver::~QueryLoggingSolver() { delete solver; - delete os; } void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) { diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 68edfe55..4da3c129 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -25,7 +25,7 @@ class QueryLoggingSolver : public SolverImpl { protected: Solver *solver; - llvm::raw_ostream *os; + std::unique_ptr<llvm::raw_ostream> os; // @brief Buffer used by logBuffer std::string BufferString; // @brief buffer to store logs before flushing to file diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 72a15c50..f127de9b 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -49,7 +49,7 @@ private: Z3Builder *builder; double timeout; SolverRunStatus runStatusCode; - llvm::raw_fd_ostream* dumpedQueriesFile; + std::unique_ptr<llvm::raw_fd_ostream> dumpedQueriesFile; ::Z3_params solverParameters; // Parameter symbols ::Z3_symbol timeoutParamStrSymbol; @@ -96,8 +96,7 @@ Z3SolverImpl::Z3SolverImpl() /*z3LogInteractionFileArg=*/Z3LogInteractionFile.size() > 0 ? Z3LogInteractionFile.c_str() : NULL)), - timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE), - dumpedQueriesFile(0) { + timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE) { assert(builder && "unable to create Z3Builder"); solverParameters = Z3_mk_params(builder->ctx); Z3_params_inc_ref(builder->ctx, solverParameters); @@ -107,7 +106,7 @@ Z3SolverImpl::Z3SolverImpl() if (!Z3QueryDumpFile.empty()) { std::string error; dumpedQueriesFile = klee_open_output_file(Z3QueryDumpFile, error); - if (!error.empty()) { + if (!dumpedQueriesFile) { klee_error("Error creating file for dumping Z3 queries: %s", error.c_str()); } @@ -127,11 +126,6 @@ Z3SolverImpl::Z3SolverImpl() Z3SolverImpl::~Z3SolverImpl() { Z3_params_dec_ref(builder->ctx, solverParameters); delete builder; - - if (dumpedQueriesFile) { - dumpedQueriesFile->close(); - delete dumpedQueriesFile; - } } Z3Solver::Z3Solver() : Solver(new Z3SolverImpl()) {} diff --git a/lib/Support/CompressionStream.cpp b/lib/Support/CompressionStream.cpp index 01fe1352..d17e1df1 100644 --- a/lib/Support/CompressionStream.cpp +++ b/lib/Support/CompressionStream.cpp @@ -23,7 +23,7 @@ namespace klee { -compressed_fd_ostream::compressed_fd_ostream(const char *Filename, +compressed_fd_ostream::compressed_fd_ostream(const std::string &Filename, std::string &ErrorInfo) : llvm::raw_ostream(), pos(0) { ErrorInfo = ""; @@ -38,6 +38,7 @@ compressed_fd_ostream::compressed_fd_ostream(const char *Filename, if (EC) { ErrorInfo = EC.message(); FD = -1; + return; } // Initialize the compression library strm.zalloc = Z_NULL; diff --git a/lib/Support/FileHandling.cpp b/lib/Support/FileHandling.cpp index 3e156f3c..068ce44b 100644 --- a/lib/Support/FileHandling.cpp +++ b/lib/Support/FileHandling.cpp @@ -7,6 +7,7 @@ // //===----------------------------------------------------------------------===// #include "klee/Internal/Support/FileHandling.h" + #include "klee/Config/Version.h" #include "klee/Config/config.h" #include "klee/Internal/Support/ErrorHandling.h" @@ -15,25 +16,41 @@ #include "llvm/Support/FileSystem.h" #endif +#ifdef HAVE_ZLIB_H +#include "klee/Internal/Support/CompressionStream.h" +#endif + namespace klee { -llvm::raw_fd_ostream *klee_open_output_file(std::string &path, - std::string &error) { - llvm::raw_fd_ostream *f; +std::unique_ptr<llvm::raw_fd_ostream> +klee_open_output_file(const std::string &path, std::string &error) { + error = ""; + std::unique_ptr<llvm::raw_fd_ostream> f; #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) std::error_code ec; - f = new llvm::raw_fd_ostream(path.c_str(), ec, llvm::sys::fs::F_None); + f = std::unique_ptr<llvm::raw_fd_ostream>(new llvm::raw_fd_ostream(path.c_str(), ec, llvm::sys::fs::F_None)); // FIXME C++14 if (ec) error = ec.message(); #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) - f = new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_None); + f = std::unique_ptr<llvm::raw_fd_ostream>(new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_None)); // FIXME C++14 #else - f = new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_Binary); + f = std::unique_ptr<llvm::raw_fd_ostream>(new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_Binary)); // FIXME C++14 #endif if (!error.empty()) { - delete f; - f = NULL; + f.reset(nullptr); } return f; } + +#ifdef HAVE_ZLIB_H +std::unique_ptr<llvm::raw_ostream> +klee_open_compressed_output_file(const std::string &path, std::string &error) { + error = ""; + std::unique_ptr<llvm::raw_ostream> f(new compressed_fd_ostream(path, error)); + if (!error.empty()) { + f.reset(nullptr); + } + return f; +} +#endif } |