[Module] Fix handling of instructions without debug info.

 - The change in 6829fb9 caused us to not allocation InstructionInfo objects for
   instructions without source-level debug info, however, that means that all
   such instructions end up sharing the one dummy InstructionInfo object, which
   really breaks statistics tracking.

 - This commit basically reverts that change, and also changes the code so we
   don't ever use the dummy InstructionInfo object for instructions, so that
   this problem can't be hit in other ways (e.g., if someone modifies the module
   after the InstructionInfoTable construction). There is a FIXME for checking
   the same thing for functions.

 - Fixes #144.

2 files changed, 57 insertions, 22 deletions

diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
index 19d7e511..82d60708 100644
--- a/lib/Module/InstructionInfoTable.cpp
+++ b/lib/Module/InstructionInfoTable.cpp
@@ -34,6 +34,7 @@
 #endif
 #include "llvm/Analysis/ValueTracking.h"
 #include "llvm/Support/Debug.h"
+#include "llvm/Support/ErrorHandling.h"
 
 #include <map>
 #include <string>
@@ -121,23 +122,12 @@ InstructionInfoTable::InstructionInfoTable(Module *m)
         lineTable.find(instr);
       if (ltit!=lineTable.end())
         assemblyLine = ltit->second;
-      if (getInstructionDebugInfo(instr, initialFile, initialLine))
-      {
-        infos.insert(std::make_pair(instr,
-                                    InstructionInfo(id++,
-                                                    *initialFile,
-                                                    initialLine,
-                                                    assemblyLine)));
-        DEBUG_WITH_TYPE("klee_obtained_debug", dbgs() <<
-          "Instruction: \"" << *instr << "\" (assembly line " << assemblyLine <<
-          ") has debug location " << *initialFile << ":" << initialLine << "\n");
-      }
-      else
-      {
-        DEBUG_WITH_TYPE("klee_missing_debug", dbgs() <<
-          "Instruction: \"" << *instr << "\" (assembly line " << assemblyLine <<
-          ") is missing debug info.\n");
-      }
+      getInstructionDebugInfo(instr, initialFile, initialLine);
+      infos.insert(std::make_pair(instr,
+                                  InstructionInfo(id++,
+                                                  *initialFile,
+                                                  initialLine,
+                                                  assemblyLine)));
     }
   }
 }
@@ -168,16 +158,20 @@ const InstructionInfo &
 InstructionInfoTable::getInfo(const Instruction *inst) const {
   std::map<const llvm::Instruction*, InstructionInfo>::const_iterator it = 
     infos.find(inst);
-  if (it==infos.end()) {
-    return dummyInfo;
-  } else {
-    return it->second;
-  }
+  if (it == infos.end())
+    llvm::report_fatal_error("invalid instruction, not present in "
+                             "initial module!");
+  return it->second;
 }
 
 const InstructionInfo &
 InstructionInfoTable::getFunctionInfo(const Function *f) const {
   if (f->isDeclaration()) {
+    // FIXME: We should probably eliminate this dummyInfo object, and instead
+    // allocate a per-function object to track the stats for that function
+    // (otherwise, anyone actually trying to use those stats is getting ones
+    // shared across all functions). I'd like to see if this matters in practice
+    // and construct a test case for it if it does, though.
     return dummyInfo;
   } else {
     return getInfo(f->begin()->begin());
diff --git a/test/Feature/StatesCoveringNew.c b/test/Feature/StatesCoveringNew.c
new file mode 100644
index 00000000..e372e89e
--- /dev/null
+++ b/test/Feature/StatesCoveringNew.c
@@ -0,0 +1,41 @@
+// Check that we properly detect states covering new instructions.
+//
+// RUN: %llvmgcc -I../../../include %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --only-output-states-covering-new %t1.bc
+
+// We expect 4 different output states, one for each named value and one "other"
+// one with the prefered CEX. We verify this by using ktest-tool to dump the
+// values, and then checking the output.
+//
+// RUN: /bin/sh -c "ktest-tool --write-int %t.klee-out/*.ktest" | sort > %t.data-values
+// RUN: FileCheck < %t.data-values %s
+
+// CHECK: object 0: data: 0
+// CHECK: object 0: data: 17
+// CHECK: object 0: data: 32
+// CHECK: object 0: data: 99
+
+#include <klee/klee.h>
+
+void f0(void) {}
+void f1(void) {}
+void f2(void) {}
+void f3(void) {}
+
+int main() {
+  int x = klee_range(0, 256, "x");
+
+  if (x == 17) {
+    f0();
+  } else if (x == 32) {
+    f1();
+  } else if (x == 99) {
+    f2();
+  } else {
+    klee_prefer_cex(&x, x == 0);
+    f3();
+  }
+
+  return 0;
+}