diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-04-08 09:50:44 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-04-08 13:09:45 +0100 |
commit | 5fbbd8a6ea51c81419b29ccfd133b4a9789fd638 (patch) | |
tree | 44fc2a65d5ab8fcc706f8eeecf5f86837a839ec3 | |
parent | 93dd487b972743a3081b311a07a66bc499a9b723 (diff) | |
download | klee-5fbbd8a6ea51c81419b29ccfd133b4a9789fd638.tar.gz |
Rename KLEE command line options from
* ``-replay-out`` to ``-replay-ktest-file`` * ``-replay-out-dir`` to ``-replay-ktest-dir`` and also rename * help descriptions * global variables corresponding to these options. * Names used in ``KleeHandler``, ``Interpreter``, ``Executor`` and in KLEE's ``main()`` function. The old name for the options/code was very unhelpful as it wasn't obvious that "out" files are ``.ktest`` files unless you examine KLEE's source code.
-rw-r--r-- | include/klee/Interpreter.h | 2 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 16 | ||||
-rw-r--r-- | lib/Core/Executor.h | 12 | ||||
-rw-r--r-- | test/Coverage/ReplayOutDir.c | 2 | ||||
-rw-r--r-- | tools/klee/main.cpp | 51 |
5 files changed, 42 insertions, 41 deletions
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h index abd454b1..b40ad0d5 100644 --- a/include/klee/Interpreter.h +++ b/include/klee/Interpreter.h @@ -113,7 +113,7 @@ public: // supply a test case to replay from. this can be used to drive the // interpretation down a user specified path. use null to reset. - virtual void setReplayOut(const struct KTest *out) = 0; + virtual void setReplayKTest(const struct KTest *out) = 0; // supply a list of branch decisions specifying which direction to // take on forks. this can be used to drive the interpretation down diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index dc9edf5f..47c1be02 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -282,7 +282,7 @@ Executor::Executor(const InterpreterOptions &opts, symPathWriter(0), specialFunctionHandler(0), processTree(0), - replayOut(0), + replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), @@ -736,7 +736,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { } } } else if (res==Solver::Unknown) { - assert(!replayOut && "in replay mode, only one branch can be true."); + assert(!replayKTest && "in replay mode, only one branch can be true."); if ((MaxMemoryInhibit && atMemoryLimit) || current.forkDisabled || @@ -2652,8 +2652,8 @@ std::string Executor::getAddressInfo(ExecutionState &state, } void Executor::terminateState(ExecutionState &state) { - if (replayOut && replayPosition!=replayOut->numObjects) { - klee_warning_once(replayOut, + if (replayKTest && replayPosition!=replayKTest->numObjects) { + klee_warning_once(replayKTest, "replay did not consume all objects in test input."); } @@ -2875,7 +2875,7 @@ void Executor::callExternalFunction(ExecutionState &state, ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state, ref<Expr> e) { unsigned n = interpreterOpts.MakeConcreteSymbolic; - if (!n || replayOut || replayPath) + if (!n || replayKTest || replayPath) return e; // right now, we don't replace symbolics (is there any reason to?) @@ -3221,7 +3221,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo, const std::string &name) { // Create a new object state for the memory object (instead of a copy). - if (!replayOut) { + if (!replayKTest) { // Find a unique name for this array. First try the original name, // or if that fails try adding a unique identifier. unsigned id = 0; @@ -3281,10 +3281,10 @@ void Executor::executeMakeSymbolic(ExecutionState &state, } } else { ObjectState *os = bindObjectInState(state, mo, false); - if (replayPosition >= replayOut->numObjects) { + if (replayPosition >= replayKTest->numObjects) { terminateStateOnError(state, "replay count mismatch", "user.err"); } else { - KTestObject *obj = &replayOut->objects[replayPosition++]; + KTestObject *obj = &replayKTest->objects[replayPosition++]; if (obj->numBytes != mo->size) { terminateStateOnError(state, "replay size mismatch", "user.err"); } else { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 8bfa278a..1997bad2 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -150,10 +150,10 @@ private: /// When non-null the bindings that will be used for calls to /// klee_make_symbolic in order replay. - const struct KTest *replayOut; + const struct KTest *replayKTest; /// When non-null a list of branch decisions to be used for replay. const std::vector<bool> *replayPath; - /// The index into the current \ref replayOut or \ref replayPath + /// The index into the current \ref replayKTest or \ref replayPath /// object. unsigned replayPosition; @@ -417,16 +417,16 @@ public: } virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) { symPathWriter = tsw; - } + } - virtual void setReplayOut(const struct KTest *out) { + virtual void setReplayKTest(const struct KTest *out) { assert(!replayPath && "cannot replay both buffer and path"); - replayOut = out; + replayKTest = out; replayPosition = 0; } virtual void setReplayPath(const std::vector<bool> *path) { - assert(!replayOut && "cannot replay both buffer and path"); + assert(!replayKTest && "cannot replay both buffer and path"); replayPath = path; replayPosition = 0; } diff --git a/test/Coverage/ReplayOutDir.c b/test/Coverage/ReplayOutDir.c index ca7e590a..d9bffea0 100644 --- a/test/Coverage/ReplayOutDir.c +++ b/test/Coverage/ReplayOutDir.c @@ -1,7 +1,7 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: rm -rf %t1.out %t1.replay // RUN: %klee --output-dir=%t1.out %t1.bc -// RUN: %klee --output-dir=%t1.replay --replay-out-dir=%t1.out %t1.bc +// RUN: %klee --output-dir=%t1.replay --replay-ktest-dir=%t1.out %t1.bc int main() { int i; diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 33d62d4d..e34dd52d 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -179,14 +179,14 @@ namespace { "the bytes, not necessarily making them concrete.")); cl::list<std::string> - ReplayOutFile("replay-out", - cl::desc("Specify an out file to replay"), - cl::value_desc("out file")); + ReplayKTestFile("replay-ktest-file", + cl::desc("Specify a ktest file to use for replay"), + cl::value_desc("ktest file")); cl::list<std::string> - ReplayOutDir("replay-out-dir", - cl::desc("Specify a directory to replay .out files from"), - cl::value_desc("output directory")); + ReplayKTestDir("replay-ktest-dir", + cl::desc("Specify a directory to replay ktest files from"), + cl::value_desc("output directory")); cl::opt<std::string> ReplayPathFile("replay-path", @@ -265,8 +265,8 @@ public: static void loadPathFile(std::string name, std::vector<bool> &buffer); - static void getOutFiles(std::string path, - std::vector<std::string> &results); + static void getKTestFilesInDir(std::string directoryPath, + std::vector<std::string> &results); static std::string getRunTimeLibraryPath(const char *argv0); }; @@ -562,14 +562,15 @@ void KleeHandler::loadPathFile(std::string name, } } -void KleeHandler::getOutFiles(std::string path, - std::vector<std::string> &results) { +void KleeHandler::getKTestFilesInDir(std::string directoryPath, + std::vector<std::string> &results) { #if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) error_code ec; #else std::error_code ec; #endif - for (llvm::sys::fs::directory_iterator i(path,ec),e; i!=e && !ec; i.increment(ec)){ + for (llvm::sys::fs::directory_iterator i(directoryPath, ec), e; i != e && !ec; + i.increment(ec)) { std::string f = (*i).path(); if (f.substr(f.size()-6,f.size()) == ".ktest") { results.push_back(f); @@ -577,8 +578,8 @@ void KleeHandler::getOutFiles(std::string path, } if (ec) { - llvm::errs() << "ERROR: unable to read output directory: " << path << ": " - << ec.message() << "\n"; + llvm::errs() << "ERROR: unable to read output directory: " << directoryPath + << ": " << ec.message() << "\n"; exit(1); } } @@ -1402,18 +1403,18 @@ int main(int argc, char **argv, char **envp) { infoFile << buf; infoFile.flush(); - if (!ReplayOutDir.empty() || !ReplayOutFile.empty()) { + if (!ReplayKTestDir.empty() || !ReplayKTestFile.empty()) { assert(SeedOutFile.empty()); assert(SeedOutDir.empty()); - std::vector<std::string> outFiles = ReplayOutFile; + std::vector<std::string> kTestFiles = ReplayKTestFile; for (std::vector<std::string>::iterator - it = ReplayOutDir.begin(), ie = ReplayOutDir.end(); + it = ReplayKTestDir.begin(), ie = ReplayKTestDir.end(); it != ie; ++it) - KleeHandler::getOutFiles(*it, outFiles); + KleeHandler::getKTestFilesInDir(*it, kTestFiles); std::vector<KTest*> kTests; for (std::vector<std::string>::iterator - it = outFiles.begin(), ie = outFiles.end(); + it = kTestFiles.begin(), ie = kTestFiles.end(); it != ie; ++it) { KTest *out = kTest_fromFile(it->c_str()); if (out) { @@ -1435,15 +1436,15 @@ int main(int argc, char **argv, char **envp) { it = kTests.begin(), ie = kTests.end(); it != ie; ++it) { KTest *out = *it; - interpreter->setReplayOut(out); + interpreter->setReplayKTest(out); llvm::errs() << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out) << " bytes)" - << " (" << ++i << "/" << outFiles.size() << ")\n"; + << " (" << ++i << "/" << kTestFiles.size() << ")\n"; // XXX should put envp in .ktest ? interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp); if (interrupted) break; } - interpreter->setReplayOut(0); + interpreter->setReplayKTest(0); while (!kTests.empty()) { kTest_free(kTests.back()); kTests.pop_back(); @@ -1463,10 +1464,10 @@ int main(int argc, char **argv, char **envp) { for (std::vector<std::string>::iterator it = SeedOutDir.begin(), ie = SeedOutDir.end(); it != ie; ++it) { - std::vector<std::string> outFiles; - KleeHandler::getOutFiles(*it, outFiles); + std::vector<std::string> kTestFiles; + KleeHandler::getKTestFilesInDir(*it, kTestFiles); for (std::vector<std::string>::iterator - it2 = outFiles.begin(), ie = outFiles.end(); + it2 = kTestFiles.begin(), ie = kTestFiles.end(); it2 != ie; ++it2) { KTest *out = kTest_fromFile(it2->c_str()); if (!out) { @@ -1475,7 +1476,7 @@ int main(int argc, char **argv, char **envp) { } seeds.push_back(out); } - if (outFiles.empty()) { + if (kTestFiles.empty()) { llvm::errs() << "KLEE: seeds directory is empty: " << *it << "\n"; exit(1); } |