Kill off ExecutionTrace stuff, it is too messy.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@98466 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 0 insertions, 125 deletions

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