about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--include/klee/Interpreter.h2
-rw-r--r--lib/Core/Executor.cpp16
-rw-r--r--lib/Core/Executor.h12
-rw-r--r--test/Coverage/ReplayOutDir.c2
-rw-r--r--tools/klee/main.cpp51
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 &current, 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);
       }