aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp13
-rw-r--r--lib/Core/Executor.h3
-rw-r--r--lib/Core/ExecutorTimers.cpp21
-rw-r--r--lib/Core/StatsTracker.cpp33
-rw-r--r--lib/Core/StatsTracker.h17
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp25
-rw-r--r--lib/Solver/QueryLoggingSolver.h2
-rw-r--r--lib/Solver/Z3Solver.cpp12
-rw-r--r--lib/Support/CompressionStream.cpp3
-rw-r--r--lib/Support/FileHandling.cpp33
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
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-26 00:56:26 +0000