differentiate between partial and completed paths in summary and fix …

…paths stats when not dumping states

include/klee/Core/Interpreter.h

@@ -40,7 +40,8 @@ class InterpreterHandler {
  virtual std::string getOutputFilename(const std::string &filename) = 0;
  virtual std::unique_ptr<llvm::raw_fd_ostream> openOutputFile(const std::string &filename) = 0;
 
- virtual void incPathsExplored() = 0;
+ virtual void incPathsCompleted() = 0;
+ virtual void incPathsExplored(std::uint32_t num = 1) = 0;
 
  virtual void processTestCase(const ExecutionState &state,
  const char *err,

lib/Core/Executor.cpp

@@ -3436,8 +3436,10 @@ bool Executor::checkMemoryUsage() {
 }
 
 void Executor::doDumpStates() {
- if (!DumpStatesOnHalt || states.empty())
+ if (!DumpStatesOnHalt || states.empty()) {
+ interpreterHandler->incPathsExplored(states.size());
  return;
+ }
 
  klee_message("halting execution, dumping remaining states");
  for (const auto &state : states)
@@ -3638,6 +3640,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
  if (!OnlyOutputStatesCoveringNew || state.coveredNew || 
  (AlwaysOutputSeeds && seedMap.count(&state)))
  interpreterHandler->processTestCase(state, 0, 0);
+ interpreterHandler->incPathsCompleted();
  terminateState(state);
 }
 

tools/klee/main.cpp

@@ -308,7 +308,8 @@ class KleeHandler : public InterpreterHandler {
 
  unsigned m_numTotalTests; // Number of tests received from the interpreter
  unsigned m_numGeneratedTests; // Number of tests successfully generated
- unsigned m_pathsExplored; // number of paths explored so far
+ unsigned m_pathsCompleted; // number of completed paths
+ unsigned m_pathsExplored; // number of partially explored and completed paths
 
  // used for writing .ktest files
  int m_argc;
@@ -321,8 +322,11 @@ class KleeHandler : public InterpreterHandler {
  llvm::raw_ostream &getInfoStream() const { return *m_infoFile; }
  /// Returns the number of test cases successfully generated so far
  unsigned getNumTestCases() { return m_numGeneratedTests; }
+ unsigned getNumPathsCompleted() { return m_pathsCompleted; }
  unsigned getNumPathsExplored() { return m_pathsExplored; }
- void incPathsExplored() { m_pathsExplored++; }
+ void incPathsCompleted() { ++m_pathsCompleted; }
+ void incPathsExplored(std::uint32_t num = 1) {
+ m_pathsExplored += num; }
 
  void setInterpreter(Interpreter *i);
 
@@ -348,7 +352,7 @@ class KleeHandler : public InterpreterHandler {
 KleeHandler::KleeHandler(int argc, char **argv)
  : m_interpreter(0), m_pathWriter(0), m_symPathWriter(0),
  m_outputDirectory(), m_numTotalTests(0), m_numGeneratedTests(0),
- m_pathsExplored(0), m_argc(argc), m_argv(argv) {
+ m_pathsCompleted(0), m_pathsExplored(0), m_argc(argc), m_argv(argv) {
 
  // create output directory (OutputDir or "klee-out-<i>")
  bool dir_given = OutputDir != "";
@@ -1583,13 +1587,15 @@ int main(int argc, char **argv, char **envp) {
  << "KLEE: done: query cex = " << queryCounterexamples << "\n";
 
  std::stringstream stats;
- stats << "\n";
- stats << "KLEE: done: total instructions = "
- << instructions << "\n";
- stats << "KLEE: done: completed paths = "
- << handler->getNumPathsExplored() << "\n";
- stats << "KLEE: done: generated tests = "
- << handler->getNumTestCases() << "\n";
+ stats << '\n'
+ << "KLEE: done: total instructions = " << instructions << '\n'
+ << "KLEE: done: completed paths = " << handler->getNumPathsCompleted()
+ << '\n'
+ << "KLEE: done: partially completed paths = "
+ << handler->getNumPathsExplored() - handler->getNumPathsCompleted()
+ << '\n'
+ << "KLEE: done: generated tests = " << handler->getNumTestCases()
+ << '\n';
 
  bool useColors = llvm::errs().is_displayed();
  if (useColors)