about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--include/klee/ExecutionState.h105
-rw-r--r--lib/Core/ExecutionState.cpp93
-rw-r--r--lib/Core/Executor.cpp32
-rw-r--r--tools/klee/main.cpp7
4 files changed, 0 insertions, 237 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 54915843..09999110 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -31,7 +31,6 @@ namespace klee {
   class MemoryObject;
   class PTreeNode;
   class InstructionInfo;
-  class ExecutionTraceEvent;
 
 std::ostream &operator<<(std::ostream &os, const MemoryMap &mm);
 
@@ -62,32 +61,6 @@ struct StackFrame {
   ~StackFrame();
 };
 
-// FIXME: Redo execution trace stuff to use a TreeStream, there is no
-// need to keep this stuff in memory as far as I can tell.
-
-// each state should have only one of these guys ...
-class ExecutionTraceManager {
-public:
-  ExecutionTraceManager() : hasSeenUserMain(false) {}
-
-  void addEvent(ExecutionTraceEvent* evt);
-  void printAllEvents(std::ostream &os) const;
-
-private:
-  // have we seen a call to __user_main() yet?
-  // don't bother tracing anything until we see this,
-  // or else we'll get junky prologue shit
-  bool hasSeenUserMain;
-
-  // ugh C++ only supports polymorphic calls thru pointers
-  //
-  // WARNING: these are NEVER FREED, because they are shared
-  // across different states (when states fork), so we have 
-  // an *intentional* memory leak, but oh wellz ;)
-  std::vector<ExecutionTraceEvent*> events;
-};
-
-
 class ExecutionState {
 public:
   typedef std::vector<StackFrame> stack_ty;
@@ -115,9 +88,6 @@ public:
   unsigned instsSinceCovNew;
   bool coveredNew;
 
-  // for printing execution traces when this state terminates
-  ExecutionTraceManager exeTraceMgr;
-
   /// Disables forking, set by user code.
   bool forkDisabled;
 
@@ -166,81 +136,6 @@ public:
   bool merge(const ExecutionState &b);
 };
 
-
-// for producing abbreviated execution traces to help visualize
-// paths and diagnose bugs
-
-class ExecutionTraceEvent {
-public:
-  // the location of the instruction:
-  std::string file;
-  unsigned line;
-  std::string funcName;
-  unsigned stackDepth;
-
-  unsigned consecutiveCount; // init to 1, increase for CONSECUTIVE
-                             // repetitions of the SAME event
-
-  ExecutionTraceEvent()
-    : file("global"), line(0), funcName("global_def"),
-      consecutiveCount(1) {}
-
-  ExecutionTraceEvent(ExecutionState& state, KInstruction* ki);
-
-  virtual ~ExecutionTraceEvent() {}
-
-  void print(std::ostream &os) const;
-
-  // return true if it shouldn't be added to ExecutionTraceManager
-  //
-  virtual bool ignoreMe() const;
-
-private:
-  virtual void printDetails(std::ostream &os) const = 0;
-};
-
-
-class FunctionCallTraceEvent : public ExecutionTraceEvent {
-public:
-  std::string calleeFuncName;
-
-  FunctionCallTraceEvent(ExecutionState& state, KInstruction* ki,
-                         const std::string& _calleeFuncName)
-    : ExecutionTraceEvent(state, ki), calleeFuncName(_calleeFuncName) {}
-
-private:
-  virtual void printDetails(std::ostream &os) const {
-    os << "CALL " << calleeFuncName;
-  }
-
-};
-
-class FunctionReturnTraceEvent : public ExecutionTraceEvent {
-public:
-  FunctionReturnTraceEvent(ExecutionState& state, KInstruction* ki)
-    : ExecutionTraceEvent(state, ki) {}
-
-private:
-  virtual void printDetails(std::ostream &os) const {
-    os << "RETURN";
-  }
-};
-
-class BranchTraceEvent : public ExecutionTraceEvent {
-public:
-  bool trueTaken;         // which side taken?
-  bool canForkGoBothWays;
-
-  BranchTraceEvent(ExecutionState& state, KInstruction* ki,
-                   bool _trueTaken, bool _isTwoWay)
-    : ExecutionTraceEvent(state, ki),
-      trueTaken(_trueTaken),
-      canForkGoBothWays(_isTwoWay) {}
-
-private:
-  virtual void printDetails(std::ostream &os) const;
-};
-
 }
 
 #endif
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 694b21b1..57f9bca9 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -302,96 +302,3 @@ bool ExecutionState::merge(const ExecutionState &b) {
 
   return true;
 }
-
-/***/
-
-ExecutionTraceEvent::ExecutionTraceEvent(ExecutionState& state, 
-                                         KInstruction* ki)
-  : consecutiveCount(1) 
-{
-  file = ki->info->file;
-  line = ki->info->line;
-  funcName = state.stack.back().kf->function->getName();
-  stackDepth = state.stack.size();
-}
-
-bool ExecutionTraceEvent::ignoreMe() const {
-  // ignore all events occurring in certain pesky uclibc files:
-  if (file.find("libc/stdio/") != std::string::npos) {
-    return true;
-  }
-
-  return false;
-}
-
-void ExecutionTraceEvent::print(std::ostream &os) const {
-  os.width(stackDepth);
-  os << ' ';
-  printDetails(os);
-  os << ' ' << file << ':' << line << ':' << funcName;
-  if (consecutiveCount > 1)
-    os << " (" << consecutiveCount << "x)\n";
-  else
-    os << '\n';
-}
-
-
-bool ExecutionTraceEventEquals(ExecutionTraceEvent* e1, ExecutionTraceEvent* e2) {
-  // first see if their base class members are identical:
-  if (!((e1->file == e2->file) &&
-        (e1->line == e2->line) &&
-        (e1->funcName == e2->funcName)))
-    return false;
-
-  // fairly ugly, but i'm no OOP master, so this is the way i'm
-  // doing it for now ... lemme know if there's a cleaner way:
-  BranchTraceEvent* be1 = dynamic_cast<BranchTraceEvent*>(e1);
-  BranchTraceEvent* be2 = dynamic_cast<BranchTraceEvent*>(e2);
-  if (be1 && be2) {
-    return ((be1->trueTaken == be2->trueTaken) &&
-            (be1->canForkGoBothWays == be2->canForkGoBothWays));
-  }
-
-  // don't tolerate duplicates in anything else:
-  return false;
-}
-
-
-void BranchTraceEvent::printDetails(std::ostream &os) const {
-  os << "BRANCH " << (trueTaken ? "T" : "F") << ' ' <<
-        (canForkGoBothWays ? "2-way" : "1-way");
-}
-
-void ExecutionTraceManager::addEvent(ExecutionTraceEvent* evt) {
-  // don't trace anything before __user_main, except for global events
-  if (!hasSeenUserMain) {
-    if (evt->funcName == "__user_main") {
-      hasSeenUserMain = true;
-    }
-    else if (evt->funcName != "global_def") {
-      return;
-    }
-  }
-
-  // custom ignore events:
-  if (evt->ignoreMe())
-    return;
-
-  if (events.size() > 0) {
-    // compress consecutive duplicates:
-    ExecutionTraceEvent* last = events.back();
-    if (ExecutionTraceEventEquals(last, evt)) {
-      last->consecutiveCount++;
-      return;
-    }
-  }
-
-  events.push_back(evt);
-}
-
-void ExecutionTraceManager::printAllEvents(std::ostream &os) const {
-  for (unsigned i = 0; i != events.size(); ++i)
-    events[i]->print(os);
-}
-
-/***/
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 87e6bb29..26c082af 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -75,9 +75,6 @@
 using namespace llvm;
 using namespace klee;
 
-// omg really hard to share cl opts across files ...
-bool WriteTraces = false;
-
 namespace {
   cl::opt<bool>
   DumpStatesOnHalt("dump-states-on-halt",
@@ -246,13 +243,6 @@ namespace {
             cl::desc("Inhibit forking at memory cap (vs. random terminate)"),
             cl::init(true));
 
-  // use 'external storage' because also needed by tools/klee/main.cpp
-  cl::opt<bool, true>
-  WriteTracesProxy("write-traces", 
-           cl::desc("Write .trace file for each terminated state"),
-           cl::location(WriteTraces),
-           cl::init(false));
-
   cl::opt<bool>
   UseForkedSTP("use-forked-stp", 
                  cl::desc("Run STP in forked process"));
@@ -1096,10 +1086,6 @@ void Executor::executeCall(ExecutionState &state,
                            KInstruction *ki,
                            Function *f,
                            std::vector< ref<Expr> > &arguments) {
-  if (WriteTraces)
-    state.exeTraceMgr.addEvent(new FunctionCallTraceEvent(state, ki,
-                                                          f->getName()));
-
   Instruction *i = ki->inst;
   if (f && f->isDeclaration()) {
     switch(f->getIntrinsicID()) {
@@ -1320,10 +1306,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     Instruction *caller = kcaller ? kcaller->inst : 0;
     bool isVoidReturn = (ri->getNumOperands() == 0);
     ref<Expr> result = ConstantExpr::alloc(0, Expr::Bool);
-
-    if (WriteTraces) {
-      state.exeTraceMgr.addEvent(new FunctionReturnTraceEvent(state, ki));
-    }
     
     if (!isVoidReturn) {
       result = eval(ki, 0, state).value;
@@ -1409,20 +1391,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       ref<Expr> cond = eval(ki, 0, state).value;
       Executor::StatePair branches = fork(state, cond, false);
 
-      if (WriteTraces) {
-        bool isTwoWay = (branches.first && branches.second);
-
-        if (branches.first) {
-          branches.first->exeTraceMgr.addEvent(
-            new BranchTraceEvent(state, ki, true, isTwoWay));
-        }
-
-        if (branches.second) {
-          branches.second->exeTraceMgr.addEvent(
-            new BranchTraceEvent(state, ki, false, isTwoWay));
-        }
-      }
-
       // NOTE: There is a hidden dependency here, markBranchVisited
       // requires that we still be in the context of the branch
       // instruction (it reuses its statistic id). Should be cleaned
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 8b788b9d..b0b44bb8 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -185,7 +185,6 @@ namespace {
            cl::init(0));
 }
 
-extern bool WriteTraces;
 extern cl::opt<double> MaxTime;
 
 /***/
@@ -476,12 +475,6 @@ void KleeHandler::processTestCase(const ExecutionState &state,
       delete f;
     }
 
-    if (WriteTraces) {
-      std::ostream *f = openTestFile("trace", id);
-      state.exeTraceMgr.printAllEvents(*f);
-      delete f;
-    }
-
     if (m_testIndex == StopAfterNTests)
       m_interpreter->setHaltExecution(true);