diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
index 5737b893692..19b5806a837 100644
--- a/include/klee/Core/Interpreter.h
+++ b/include/klee/Core/Interpreter.h
@@ -11,17 +11,18 @@
 
 #include "TerminationTypes.h"
 #include "klee/Module/Annotation.h"
-
 #include "klee/Module/SarifReport.h"
 
 #include <cstdint>
-#include <map>
 #include <memory>
+#include <map>
 #include <set>
-#include <string>
+#include <unordered_set>
 #include <unordered_map>
+#include <string>
 #include <vector>
 
+#include "llvm/ADT/StringRef.h"
 #include <nonstd/optional.hpp>
 
 using nonstd::optional;
@@ -63,6 +64,12 @@ class InterpreterHandler {
                                const char *suffix, bool isError = false) = 0;
 };
 
+// TODO remove
+using FInstructions = std::unordered_map<
+    std::string,
+    std::unordered_map<
+        unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;
+
 enum class MockStrategy {
   None,          // No mocks are generated
   Naive,         // For each function call new symbolic value is generated
@@ -161,9 +168,9 @@ class Interpreter {
   setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
             std::vector<std::unique_ptr<llvm::Module>> &libsModules,
             const ModuleOptions &opts,
-            const std::unordered_set<std::string> &mainModuleFunctions,
-            const std::unordered_set<std::string> &mainModuleGlobals,
-            std::unique_ptr<InstructionInfoTable> origInfos,
+            std::set<llvm::StringRef> &mainModuleFunctions,
+            std::set<llvm::StringRef> &mainModuleGlobals,
+            FInstructions &&origInstructions,
             const std::set<std::string> &ignoredExternals,
             std::vector<std::pair<std::string, std::string>> redefinitions) = 0;
 
@@ -217,7 +224,7 @@ class Interpreter {
 
   virtual void
   getCoveredLines(const ExecutionState &state,
-                  std::map<const std::string *, std::set<unsigned>> &res) = 0;
+                  std::map<std::string, std::set<size_t>> &res) = 0;
 
   virtual void getBlockPath(const ExecutionState &state,
                             std::string &blockPath) = 0;
diff --git a/include/klee/Module/InstructionInfoTable.h b/include/klee/Module/InstructionInfoTable.h
index 8b91c0d8c81..0f123f0315f 100644
--- a/include/klee/Module/InstructionInfoTable.h
+++ b/include/klee/Module/InstructionInfoTable.h
@@ -1,11 +1,11 @@
-//===-- InstructionInfoTable.h ----------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
+////===-- InstructionInfoTable.h ----------------------------------*- C++ -*-===//
+////
+////                     The KLEE Symbolic Virtual Machine
+////
+//// This file is distributed under the University of Illinois Open Source
+//// License. See LICENSE.TXT for details.
+////
+////===----------------------------------------------------------------------===//
 
 #ifndef KLEE_INSTRUCTIONINFOTABLE_H
 #define KLEE_INSTRUCTIONINFOTABLE_H
@@ -31,82 +31,81 @@ class Module;
 
 namespace klee {
 
-/// @brief InstructionInfo stores debug information for a KInstruction.
-struct InstructionInfo {
-  /// @brief The instruction id.
-  unsigned id;
-  /// @brief Line number in source file.
-  unsigned line;
-  /// @brief Column number in source file.
-  unsigned column;
-  /// @brief Line number in generated assembly.ll.
-  llvm::Optional<uint64_t> assemblyLine;
-  /// @brief Source file name.
-  const std::string &file;
-
-public:
-  InstructionInfo(unsigned id, const std::string &file, unsigned line,
-                  unsigned column, llvm::Optional<uint64_t> assemblyLine)
-      : id{id}, line{line}, column{column},
-        assemblyLine{assemblyLine}, file{file} {}
-};
-
-/// @brief FunctionInfo stores debug information for a KFunction.
-struct FunctionInfo {
-  /// @brief The function id.
-  unsigned id;
-  /// @brief Line number in source file.
-  unsigned line;
-  /// @brief Line number in generated assembly.ll.
-  llvm::Optional<uint64_t> assemblyLine;
-  /// @brief Source file name.
-  const std::string &file;
-
-public:
-  FunctionInfo(unsigned id, const std::string &file, unsigned line,
-               llvm::Optional<uint64_t> assemblyLine)
-      : id{id}, line{line}, assemblyLine{assemblyLine}, file{file} {}
-
-  FunctionInfo(const FunctionInfo &) = delete;
-  FunctionInfo &operator=(FunctionInfo const &) = delete;
-
-  FunctionInfo(FunctionInfo &&) = default;
+//// TODO move to methods of kInstruction
+///// @brief InstructionInfo stores debug information for a KInstruction.
+//struct InstructionInfo {
+//  /// @brief The instruction id.
+////  unsigned id; // TODO move to kInstruction
+//  /// @brief Line number in source file.
+//  //  unsigned line;
+//  /// @brief Column number in source file.
+//  //  unsigned column;
+//  /// @brief Line number in generated assembly.ll.
+////  llvm::Optional<uint64_t> assemblyLine;
+//  /// @brief Source file name.
+////  const std::string &file;
+//
+//public:
+//  InstructionInfo(unsigned id) {}
+//};
+//
+///// @brief FunctionInfo stores debug information for a KFunction.
+//struct FunctionInfo { // TODO clear this too
+//  /// @brief The function id.
+////  unsigned id; // TODO move to kFunction
+//  /// @brief Line number in source file.
+////  unsigned line;
+//  /// @brief Line number in generated assembly.ll.
+////  llvm::Optional<uint64_t> assemblyLine;
+//  /// @brief Source file name.
+////  const std::string &file;
+//
+//public:
+//  FunctionInfo(unsigned id) {}
+//
+//  FunctionInfo(const FunctionInfo &) = delete;
+//  FunctionInfo &operator=(FunctionInfo const &) = delete;
+//
+//  FunctionInfo(FunctionInfo &&) = default;
+//};
+//
+//class InstructionInfoTable {
+//public:
+//  using LocationToFunctionsMap =
+//      std::unordered_map<std::string,
+//                         std::unordered_set<const llvm::Function *>>;
+//
+//private:
+//  std::unordered_map<const llvm::Instruction *,
+//                     std::unique_ptr<InstructionInfo>> infos;
+//  std::unordered_map<const llvm::Function *, std::unique_ptr<FunctionInfo>>
+//      functionInfos;
+//  LocationToFunctionsMap fileNameToFunctions;                // TODO remove
+////  Instructions insts; // TODO remove when move prepare target to main
+//
+//public:
+//  explicit InstructionInfoTable(
+//      const llvm::Module &m);
+//
+////  unsigned getMaxID() const;
+//  const InstructionInfo &getInfo(const llvm::Instruction &) const;
+//  const FunctionInfo &getFunctionInfo(const llvm::Function &) const;
+//  const LocationToFunctionsMap &getFileNameToFunctions() const;
+////  Instructions getInstructions();
+//};
+
+struct LocationInfo {
+  std::string file;
+  size_t line;
+  size_t column;
 };
 
-class InstructionInfoTable {
-public:
-  using Instructions = std::unordered_map<
-      std::string,
-      std::unordered_map<
-          unsigned int,
-          std::unordered_map<unsigned int, std::unordered_set<unsigned int>>>>;
-  using LocationToFunctionsMap =
-      std::unordered_map<std::string,
-                         std::unordered_set<const llvm::Function *>>;
 
-private:
-  std::unordered_map<const llvm::Instruction *,
-                     std::unique_ptr<InstructionInfo>>
-      infos;
-  std::unordered_map<const llvm::Function *, std::unique_ptr<FunctionInfo>>
-      functionInfos;
-  LocationToFunctionsMap fileNameToFunctions;
-  std::vector<std::unique_ptr<std::string>> internedStrings;
-  std::unordered_set<std::string> filesNames;
-  Instructions insts;
+// TODO need unify with kFunction
+LocationInfo getLocationInfo(const llvm::Function *func);
 
-public:
-  explicit InstructionInfoTable(
-      const llvm::Module &m, std::unique_ptr<llvm::raw_fd_ostream> assemblyFS,
-      bool withInstructions = false);
-
-  unsigned getMaxID() const;
-  const InstructionInfo &getInfo(const llvm::Instruction &) const;
-  const FunctionInfo &getFunctionInfo(const llvm::Function &) const;
-  const LocationToFunctionsMap &getFileNameToFunctions() const;
-  const std::unordered_set<std::string> &getFilesNames() const;
-  Instructions getInstructions();
-};
+// TODO need unify with kInstruction
+LocationInfo getLocationInfo(const llvm::Instruction *inst);
 
 } // namespace klee
 
diff --git a/include/klee/Module/KInstruction.h b/include/klee/Module/KInstruction.h
index 865a752bfd9..3bce0104ebd 100644
--- a/include/klee/Module/KInstruction.h
+++ b/include/klee/Module/KInstruction.h
@@ -11,8 +11,6 @@
 #define KLEE_KINSTRUCTION_H
 
 #include "klee/Config/Version.h"
-#include "klee/Module/InstructionInfoTable.h"
-
 #include "klee/Support/CompilerWarning.h"
 DISABLE_WARNING_PUSH
 DISABLE_WARNING_DEPRECATED_DECLARATIONS
@@ -20,6 +18,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/raw_ostream.h"
 DISABLE_WARNING_POP
 
+#include <optional>
 #include <vector>
 
 namespace llvm {
@@ -28,34 +27,57 @@ class Instruction;
 
 namespace klee {
 class Executor;
-struct InstructionInfo;
 class KModule;
+struct KFunction;
 struct KBlock;
 
 /// KInstruction - Intermediate instruction representation used
 /// during execution.
 struct KInstruction {
   llvm::Instruction *inst;
-  const InstructionInfo *info;
+//  const InstructionInfo *info; // TODO remove it
 
   /// Value numbers for each operand. -1 is an invalid value,
   /// otherwise negative numbers are indices (negated and offset by
   /// 2) into the module constant table and positive numbers are
   /// register indices.
   int *operands;
-  /// Destination register index.
-  unsigned dest;
   KBlock *parent;
 
+private:
   // Instruction index in the basic block
-  unsigned index;
+  const unsigned globalIndex;
 
+  /// Destination register index.
+  //  unsigned dest;
 public:
-  KInstruction() = default;
-  explicit KInstruction(const KInstruction &ki);
+  /// Unique index for KFunction and KInstruction inside KModule
+  /// from 0 to [KFunction + KInstruction]
+  [[nodiscard]] unsigned getGlobalIndex() const;
+  /// Instruction index in the basic block
+  [[nodiscard]] unsigned getIndex() const;
+  /// Destination register index.
+  [[nodiscard]] unsigned getDest() const;
+
+  KInstruction(const std::unordered_map<llvm::Instruction *, unsigned>
+                   &_instructionToRegisterMap,
+               llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
+               unsigned &_globalIndexInc);
+
+  KInstruction() = delete; // TODO remove default constructor
+  explicit KInstruction(const KInstruction &ki) = delete;
   virtual ~KInstruction();
-  std::string getSourceLocation() const;
-  std::string toString() const;
+
+  [[nodiscard]] size_t getLine() const;
+  [[nodiscard]] size_t getColumn() const;
+  [[nodiscard]] std::string getSourceFilepath() const;
+
+  [[nodiscard]] std::string getSourceLocationString() const;
+  [[nodiscard]] std::string toString() const;
+
+  [[nodiscard]] KBlock *getKBlock() const;
+  [[nodiscard]] KFunction *getKFunction() const;
+  [[nodiscard]] KModule *getKModule() const;
 };
 
 struct KGEPInstruction : KInstruction {
@@ -70,8 +92,14 @@ struct KGEPInstruction : KInstruction {
   uint64_t offset;
 
 public:
-  KGEPInstruction() = default;
-  explicit KGEPInstruction(const KGEPInstruction &ki);
+  KGEPInstruction(const std::unordered_map<llvm::Instruction *, unsigned>
+                      &_instructionToRegisterMap,
+                  llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
+                  unsigned &_globalIndexInc)
+      : KInstruction(_instructionToRegisterMap, _inst, _km, _kb,
+                     _globalIndexInc) {}
+  KGEPInstruction() = delete;
+  explicit KGEPInstruction(const KGEPInstruction &ki) = delete;
 };
 } // namespace klee
 
diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h
index bfd30c019ba..3e5271d3d68 100644
--- a/include/klee/Module/KModule.h
+++ b/include/klee/Module/KModule.h
@@ -12,7 +12,6 @@
 
 #include "klee/Config/Version.h"
 #include "klee/Core/Interpreter.h"
-#include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KCallable.h"
 
 #include "klee/Support/CompilerWarning.h"
@@ -62,19 +61,19 @@ struct KBlock {
   KFunction *parent;
   llvm::BasicBlock *basicBlock;
 
-  unsigned numInstructions;
   KInstruction **instructions;
+  unsigned numInstructions;
+  //  unsigned id;
 
   /// Whether instructions in this function should count as
   /// "coverable" for statistics and search heuristics.
-  bool trackCoverage;
-
-  unsigned id;
+  //  bool trackCoverage;
 
 public:
   KBlock(KFunction *, llvm::BasicBlock *, KModule *,
-         std::unordered_map<llvm::Instruction *, unsigned> &,
-         std::unordered_map<unsigned, KInstruction *> &, KInstruction **);
+         const std::unordered_map<llvm::Instruction *, unsigned> &,
+         KInstruction **, unsigned &globalIndexInc);
+  KBlock() = delete;
   KBlock(const KBlock &) = delete;
   KBlock &operator=(const KBlock &) = delete;
   virtual ~KBlock() = default;
@@ -82,16 +81,15 @@ struct KBlock {
   virtual KBlockType getKBlockType() const { return KBlockType::Base; }
   static bool classof(const KBlock *) { return true; }
 
-  void handleKInstruction(std::unordered_map<llvm::Instruction *, unsigned>
-                              &instructionToRegisterMap,
-                          llvm::Instruction *inst, KModule *km,
-                          KInstruction *ki);
   KInstruction *getFirstInstruction() const noexcept { return instructions[0]; }
   KInstruction *getLastInstruction() const noexcept {
     return instructions[numInstructions - 1];
   }
   std::string getLabel() const;
   std::string toString() const;
+
+  /// Block id inside function
+  [[nodiscard]] uintptr_t getId() const;
 };
 
 typedef std::function<bool(KBlock *)> KBlockPredicate;
@@ -101,10 +99,11 @@ struct KCallBlock : KBlock {
   std::set<llvm::Function *> calledFunctions;
 
 public:
+  KCallBlock() = delete;
   KCallBlock(KFunction *, llvm::BasicBlock *, KModule *,
-             std::unordered_map<llvm::Instruction *, unsigned> &,
-             std::unordered_map<unsigned, KInstruction *> &,
-             std::set<llvm::Function *>, KInstruction **);
+             const std::unordered_map<llvm::Instruction *, unsigned> &,
+             std::set<llvm::Function *>, KInstruction **,
+             unsigned &globalIndexInc);
   static bool classof(const KCallBlock *) { return true; }
   static bool classof(const KBlock *E) {
     return E->getKBlockType() == KBlockType::Call;
@@ -118,9 +117,10 @@ struct KCallBlock : KBlock {
 
 struct KReturnBlock : KBlock {
 public:
+  KReturnBlock() = delete;
   KReturnBlock(KFunction *, llvm::BasicBlock *, KModule *,
-               std::unordered_map<llvm::Instruction *, unsigned> &,
-               std::unordered_map<unsigned, KInstruction *> &, KInstruction **);
+               const std::unordered_map<llvm::Instruction *, unsigned> &,
+               KInstruction **, unsigned &globalIndexInc);
   static bool classof(const KReturnBlock *) { return true; }
   static bool classof(const KBlock *E) {
     return E->getKBlockType() == KBlockType::Return;
@@ -131,33 +131,40 @@ struct KReturnBlock : KBlock {
 struct KFunction : public KCallable {
 private:
   std::unordered_map<std::string, KBlock *> labelMap;
+  const unsigned globalIndex;
 
 public:
   KModule *parent;
   llvm::Function *function;
-
-  unsigned numArgs, numRegisters;
-  unsigned id;
-
-  std::unordered_map<unsigned, KInstruction *> registerToInstructionMap;
-  unsigned numInstructions;
-  unsigned numBlocks;
   KInstruction **instructions;
 
-  bool kleeHandled = false;
+  //  std::unordered_map<unsigned, KInstruction *> registerToInstructionMap;
+  [[nodiscard]] KInstruction *getInstructionByRegister(size_t reg) const;
 
   std::unordered_map<const llvm::Instruction *, KInstruction *> instructionMap;
+  // TODO maybe change to std::unique_ptr<KBlock[]>
   std::vector<std::unique_ptr<KBlock>> blocks;
   std::unordered_map<const llvm::BasicBlock *, KBlock *> blockMap;
   KBlock *entryKBlock;
   std::vector<KBlock *> returnKBlocks;
   std::vector<KCallBlock *> kCallBlocks;
 
+  /// count of instructions in function
+  unsigned numInstructions;
+  //  unsigned numArgs;
+  [[nodiscard]] size_t getNumArgs() const;
+  //  unsigned numRegisters;
+  [[nodiscard]] size_t getNumRegisters() const;
+  //  unsigned numBlocks;
+  unsigned id;
+
+  bool kleeHandled = false;
   /// Whether instructions in this function should count as
   /// "coverable" for statistics and search heuristics.
-  bool trackCoverage;
+  //  bool trackCoverage;
 
-  explicit KFunction(llvm::Function *, KModule *);
+  explicit KFunction(llvm::Function *, KModule *, unsigned &);
+  KFunction() = delete;
   KFunction(const KFunction &) = delete;
   KFunction &operator=(const KFunction &) = delete;
 
@@ -187,6 +194,13 @@ struct KFunction : public KCallable {
   static bool classof(const KCallable *callable) {
     return callable->getKind() == CK_Function;
   }
+
+  [[nodiscard]] size_t getLine() const;
+  [[nodiscard]] std::string getSourceFilepath() const;
+
+  /// Unique index for KFunction and KInstruction inside KModule
+  /// from 0 to [KFunction + KInstruction]
+  [[nodiscard]] inline unsigned getGlobalIndex() const { return globalIndex; }
 };
 
 class KConstant {
@@ -206,7 +220,8 @@ class KConstant {
 
 class KModule {
 private:
-  bool withPosixRuntime;
+  bool withPosixRuntime; // TODO move to opts
+  unsigned maxGlobalIndex;
 
 public:
   std::unique_ptr<llvm::Module> module;
@@ -217,19 +232,26 @@ class KModule {
   std::unordered_map<const llvm::Function *, KFunction *> functionMap;
   std::unordered_map<llvm::Function *, std::set<llvm::Function *>> callMap;
   std::unordered_map<std::string, KFunction *> functionNameMap;
-  std::unordered_map<const llvm::Function *, unsigned> functionIDMap;
+  //  std::unordered_map<const llvm::Function *, unsigned> functionIDMap;
+  [[nodiscard]] unsigned getFunctionId(const llvm::Function *) const;
 
   // Functions which escape (may be called indirectly)
   // XXX change to KFunction
   std::set<llvm::Function *> escapingFunctions;
 
-  std::unordered_set<std::string> mainModuleFunctions;
+  std::set<llvm::StringRef> mainModuleFunctions;
 
-  std::unordered_set<std::string> mainModuleGlobals;
+  std::set<llvm::StringRef> mainModuleGlobals;
 
-  InstructionInfoTable::Instructions origInfos;
+  using FInstructions = std::unordered_map<
+      std::string,
+      std::unordered_map<
+          unsigned,
+          std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;
 
-  std::unique_ptr<InstructionInfoTable> infos;
+  FInstructions origInstructions;
+
+//  std::unique_ptr<InstructionInfoTable> infos;
 
   std::vector<llvm::Constant *> constants;
   std::unordered_map<const llvm::Constant *, std::unique_ptr<KConstant>>
@@ -241,6 +263,9 @@ class KModule {
   // Functions which are part of KLEE runtime
   std::set<const llvm::Function *> internalFunctions;
 
+  // instruction to assembly.ll line empty if no statistic enabled
+  std::unordered_map<uintptr_t, uint64_t> asmLineMap;
+
   // Mark function with functionName as part of the KLEE runtime
   void addInternalFunction(const char *functionName);
   // Replace std functions with KLEE intrinsics
@@ -294,6 +319,16 @@ class KModule {
   bool inMainModule(const llvm::GlobalVariable &v);
 
   bool WithPOSIXRuntime() { return withPosixRuntime; }
+
+  std::optional<size_t> getAsmLine(const uintptr_t ref) const;
+  std::optional<size_t> getAsmLine(const llvm::Function *func) const;
+  std::optional<size_t> getAsmLine(const llvm::Instruction *inst) const;
+
+  inline unsigned getMaxGlobalIndex() const {
+    return maxGlobalIndex;
+  }
+  unsigned getGlobalIndex(const llvm::Function *func) const;
+  unsigned getGlobalIndex(const llvm::Instruction *inst) const;
 };
 } // namespace klee
 
diff --git a/lib/Basic/Statistics.cpp b/lib/Basic/Statistics.cpp
index 170ea839e0c..50d9e8bf1fa 100644
--- a/lib/Basic/Statistics.cpp
+++ b/lib/Basic/Statistics.cpp
@@ -50,7 +50,7 @@ Statistic *StatisticManager::getStatisticByName(const std::string &name) const {
   return 0;
 }
 
-StatisticManager *klee::theStatisticManager = 0;
+StatisticManager *klee::theStatisticManager = nullptr;
 
 static StatisticManager &getStatisticManager() {
   static StatisticManager sm;
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index ea0abc92367..c45430a211d 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -99,13 +99,13 @@ bool CallStackFrame::equals(const CallStackFrame &other) const {
 }
 
 StackFrame::StackFrame(KFunction *kf) : kf(kf), varargs(0) {
-  locals = new Cell[kf->numRegisters];
+  locals = new Cell[kf->getNumRegisters()];
 }
 
 StackFrame::StackFrame(const StackFrame &s)
     : kf(s.kf), allocas(s.allocas), varargs(s.varargs) {
-  locals = new Cell[kf->numRegisters];
-  for (unsigned i = 0; i < kf->numRegisters; i++)
+  locals = new Cell[kf->getNumRegisters()];
+  for (unsigned i = 0; i < kf->getNumRegisters(); i++)
     locals[i] = s.locals[i];
 }
 
@@ -407,13 +407,14 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
     const StackFrame &sf = stack.valueStack().at(ri);
 
     Function *f = csf.kf->function;
-    const InstructionInfo &ii = *target->info;
+//    const InstructionInfo &ii = *target->info;
     out << "\t#" << i;
-    if (ii.assemblyLine.hasValue()) {
-      std::stringstream AssStream;
-      AssStream << std::setw(8) << std::setfill('0')
-                << ii.assemblyLine.getValue();
-      out << AssStream.str();
+    auto assemblyLine = target->getKModule()->getAsmLine(target->inst);
+    if (assemblyLine.has_value()) {
+      std::stringstream AsmStream;
+      AsmStream << std::setw(8) << std::setfill('0')
+                << assemblyLine.value();
+      out << AsmStream.str();
     }
     out << " in " << f->getName().str() << "(";
     // Yawn, we could go up and print varargs if we wanted to.
@@ -434,8 +435,9 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
       }
     }
     out << ")";
-    if (ii.file != "")
-      out << " at " << ii.file << ":" << ii.line;
+    std::string filepath = target->getSourceFilepath();
+    if (!filepath.empty())
+      out << " at " << filepath << ":" << target->getLine();
     out << "\n";
     target = csf.caller;
   }
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 21d30517785..90accc82b03 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -216,7 +216,7 @@ struct Symbolic {
   const Array *array;
   KType *type;
   Symbolic(ref<const MemoryObject> mo, const Array *a, KType *t)
-      : memoryObject(mo), array(a), type(t) {}
+      : memoryObject(std::move(mo)), array(a), type(t) {}
   Symbolic &operator=(const Symbolic &other) = default;
 
   friend bool operator==(const Symbolic &lhs, const Symbolic &rhs) {
@@ -308,7 +308,7 @@ struct MemorySubobject {
   ref<Expr> address;
   unsigned size;
   MemorySubobject(ref<Expr> address, unsigned size)
-      : address(address), size(size) {}
+      : address(std::move(address)), size(size) {}
   MemorySubobject &operator=(const MemorySubobject &other) = default;
 };
 
@@ -397,8 +397,10 @@ class ExecutionState {
   /// taken to reach/create this state
   TreeOStream symPathOS;
 
+
   /// @brief Set containing which lines in which files are covered by this state
-  std::map<const std::string *, std::set<std::uint32_t>> coveredLines;
+  // TODO change to StringRef
+  std::map<std::string, std::set<size_t>> coveredLines;
 
   /// @brief Pointer to the process tree of the current state
   /// Copies of ExecutionState should not copy ptreeNode
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 86533da7af9..84e05b71bfd 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -454,9 +454,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
                    InterpreterHandler *ih)
     : Interpreter(opts), interpreterHandler(ih), searcher(nullptr),
       externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
-      pathWriter(0), symPathWriter(0),
-      specialFunctionHandler(0), timers{time::Span(TimerInterval)},
-      guidanceKind(opts.Guidance), codeGraphDistance(new CodeGraphDistance()),
+      pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
+      timers{time::Span(TimerInterval)}, guidanceKind(opts.Guidance),
+      codeGraphDistance(new CodeGraphDistance()),
       distanceCalculator(new DistanceCalculator(*codeGraphDistance)),
       targetCalculator(new TargetCalculator(*codeGraphDistance)),
       targetManager(new TargetManager(guidanceKind, *distanceCalculator,
@@ -534,9 +534,9 @@ llvm::Module *Executor::setModule(
     std::vector<std::unique_ptr<llvm::Module>> &userModules,
     std::vector<std::unique_ptr<llvm::Module>> &libsModules,
     const ModuleOptions &opts,
-    const std::unordered_set<std::string> &mainModuleFunctions,
-    const std::unordered_set<std::string> &mainModuleGlobals,
-    std::unique_ptr<InstructionInfoTable> origInfos,
+                    std::set<llvm::StringRef> &mainModuleFunctions,
+                    std::set<llvm::StringRef> &mainModuleGlobals,
+                    FInstructions &&origInstructions,
     const std::set<std::string> &ignoredExternals,
     std::vector<std::pair<std::string, std::string>> redefinitions) {
   assert(!kmodule && !userModules.empty() &&
@@ -619,16 +619,12 @@ llvm::Module *Executor::setModule(
   kmodule->checkModule();
 
   // 4.) Manifest the module
-  kmodule->mainModuleFunctions.insert(mainModuleFunctions.begin(),
-                                      mainModuleFunctions.end());
-  kmodule->mainModuleGlobals.insert(mainModuleGlobals.begin(),
-                                    mainModuleGlobals.end());
+  std::swap(kmodule->mainModuleFunctions, mainModuleFunctions);
+  std::swap(kmodule->mainModuleGlobals, mainModuleGlobals);
   kmodule->manifest(interpreterHandler, interpreterOpts.Guidance,
                     StatsTracker::useStatistics());
 
-  if (origInfos) {
-    kmodule->origInfos = origInfos->getInstructions();
-  }
+  kmodule->origInstructions = origInstructions;
 
   specialFunctionHandler->bind();
 
@@ -1116,7 +1112,7 @@ ref<Expr> Executor::maxStaticPctChecks(ExecutionState &current,
     std::string msg("skipping fork and concretizing condition (MaxStatic*Pct "
                     "limit reached) at ");
     llvm::raw_string_ostream os(msg);
-    os << current.prevPC->getSourceLocation();
+    os << current.prevPC->getSourceLocationString();
     klee_warning_once(0, "%s", os.str().c_str());
 
     addConstraint(current, EqExpr::create(value, condition));
@@ -1534,8 +1530,8 @@ ref<klee::ConstantExpr> Executor::toConstant(ExecutionState &state, ref<Expr> e,
   std::string str;
   llvm::raw_string_ostream os(str);
   os << "silently concretizing (reason: " << reason << ") expression " << e
-     << " to value " << value << " (" << (*(state.pc)).info->file << ":"
-     << (*(state.pc)).info->line << ")";
+     << " to value " << value << " (" << state.pc->getSourceFilepath() << ":"
+     << state.pc->getLine() << ")";
 
   if (AllExternalWarnings)
     klee_warning("%s", os.str().c_str());
@@ -1614,10 +1610,13 @@ void Executor::printDebugInstructions(ExecutionState &state) {
   //   [src]     src location:asm line:state ID
   if (!DebugPrintInstructions.isSet(STDERR_COMPACT) &&
       !DebugPrintInstructions.isSet(FILE_COMPACT)) {
-    (*stream) << "     " << state.pc->getSourceLocation() << ':';
+    (*stream) << "     " << state.pc->getSourceLocationString() << ':';
   }
-  if (state.pc->info->assemblyLine.hasValue()) {
-    (*stream) << state.pc->info->assemblyLine.getValue() << ':';
+  {
+    auto asmLine = state.pc->getKModule()->getAsmLine(state.pc->inst);
+    if (asmLine.has_value()) {
+      (*stream) << asmLine.value() << ':';
+    }
   }
   (*stream) << state.getID() << ":";
   (*stream) << "[";
@@ -2582,7 +2581,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       // requires that we still be in the context of the branch
       // instruction (it reuses its statistic id). Should be cleaned
       // up with convenient instruction specific data.
-      if (statsTracker && state.stack.callStack().back().kf->trackCoverage)
+      if (statsTracker)
         statsTracker->markBranchVisited(branches.first, branches.second);
 
       if (branches.first)
@@ -4261,9 +4260,9 @@ void Executor::reportProgressTowardsTargets(std::string prefix,
     repr << "in function " +
                 target->getBlock()->parent->function->getName().str();
     repr << " (lines ";
-    repr << target->getBlock()->getFirstInstruction()->info->line;
+    repr << target->getBlock()->getFirstInstruction()->getLine();
     repr << " to ";
-    repr << target->getBlock()->getLastInstruction()->info->line;
+    repr << target->getBlock()->getLastInstruction()->getLine();
     repr << ")";
     std::string targetString = repr.str();
     klee_message("%s for %s", distance.toString().c_str(),
@@ -4611,22 +4610,20 @@ void Executor::terminateStateEarlyUser(ExecutionState &state,
   terminateStateEarly(state, message, StateTerminationType::SilentExit);
 }
 
-const InstructionInfo &
-Executor::getLastNonKleeInternalInstruction(const ExecutionState &state,
-                                            Instruction **lastInstruction) {
+const KInstruction *
+Executor::getLastNonKleeInternalInstruction(const ExecutionState &state) {
   // unroll the stack of the applications state and find
   // the last instruction which is not inside a KLEE internal function
-  ExecutionStack::call_stack_ty::const_reverse_iterator
-      it = state.stack.callStack().rbegin(),
-      itE = state.stack.callStack().rend();
+  auto it = state.stack.callStack().rbegin();
+  auto itE = state.stack.callStack().rend();
 
   // don't check beyond the outermost function (i.e. main())
   itE--;
 
-  const InstructionInfo *ii = 0;
+  const KInstruction *ki = nullptr;
   if (kmodule->internalFunctions.count(it->kf->function) == 0) {
-    ii = state.prevPC->info;
-    *lastInstruction = state.prevPC->inst;
+    ki = state.prevPC;
+//    *lastInstruction = state.prevPC->inst;
     //  Cannot return yet because even though
     //  it->function is not an internal function it might of
     //  been called from an internal function.
@@ -4640,21 +4637,21 @@ Executor::getLastNonKleeInternalInstruction(const ExecutionState &state,
     // function
     const Function *f = (*it->caller).inst->getParent()->getParent();
     if (kmodule->internalFunctions.count(f)) {
-      ii = 0;
+      ki = nullptr;
       continue;
     }
-    if (!ii) {
-      ii = (*it->caller).info;
-      *lastInstruction = (*it->caller).inst;
+    if (!ki) {
+      ki = it->caller;
+//      *lastInstruction = *it->caller;
     }
   }
 
-  if (!ii) {
+  if (!ki) {
     // something went wrong, play safe and return the current instruction info
-    *lastInstruction = state.prevPC->inst;
-    return *state.prevPC->info;
+//    *lastInstruction = state.prevPC->inst;
+    return state.prevPC;
   }
-  return *ii;
+  return ki;
 }
 
 bool shouldExitOn(StateTerminationType reason) {
@@ -4713,14 +4710,15 @@ void Executor::terminateStateOnError(ExecutionState &state,
                                      const char *suffix) {
   std::string message = messaget.str();
   static std::set<std::pair<Instruction *, std::string>> emittedErrors;
-  Instruction *lastInst;
-  const InstructionInfo &ii =
-      getLastNonKleeInternalInstruction(state, &lastInst);
+  const KInstruction *ki = getLastNonKleeInternalInstruction(state);
+//  const InstructionInfo &ii = *ki->info;
+  Instruction *lastInst = ki->inst;
 
   if (EmitAllErrors ||
       emittedErrors.insert(std::make_pair(lastInst, message)).second) {
-    if (!ii.file.empty()) {
-      klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line,
+    std::string filepath = ki->getSourceFilepath();
+    if (!filepath.empty()) {
+      klee_message("ERROR: %s:%zu: %s", filepath.c_str(), ki->getLine(),
                    message.c_str());
     } else {
       klee_message("ERROR: (location information missing) %s", message.c_str());
@@ -4731,10 +4729,14 @@ void Executor::terminateStateOnError(ExecutionState &state,
     std::string MsgString;
     llvm::raw_string_ostream msg(MsgString);
     msg << "Error: " << message << '\n';
-    if (!ii.file.empty()) {
-      msg << "File: " << ii.file << '\n' << "Line: " << ii.line << '\n';
-      if (ii.assemblyLine.hasValue()) {
-        msg << "assembly.ll line: " << ii.assemblyLine.getValue() << '\n';
+    if (!filepath.empty()) {
+      msg << "File: " << filepath << '\n'
+          << "Line: " << ki->getLine() << '\n';
+      {
+        auto asmLine = ki->getKModule()->getAsmLine(ki->inst);
+        if (asmLine.has_value()) {
+          msg << "assembly.ll line: " << asmLine.value() << '\n';
+        }
       }
       msg << "State: " << state.getID() << '\n';
     }
@@ -4823,7 +4825,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
       if (i != arguments.size() - 1)
         os << ", ";
     }
-    os << ") at " << state.pc->getSourceLocation();
+    os << ") at " << state.pc->getSourceLocationString();
 
     if (AllExternalWarnings)
       klee_warning("%s", os.str().c_str());
@@ -4942,7 +4944,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
       if (i != arguments.size() - 1)
         os << ", ";
     }
-    os << ") at " << state.pc->getSourceLocation();
+    os << ") at " << state.pc->getSourceLocationString();
 
     if (AllExternalWarnings)
       klee_warning("%s", os.str().c_str());
@@ -6820,7 +6822,8 @@ void Executor::prepareSymbolicValue(ExecutionState &state,
 
 void Executor::prepareSymbolicRegister(ExecutionState &state, StackFrame &sf,
                                        unsigned regNum) {
-  KInstruction *allocInst = sf.kf->registerToInstructionMap[regNum];
+//  KInstruction *allocInst = sf.kf->registerToInstructionMap[regNum];
+  KInstruction *allocInst = sf.kf->getInstructionByRegister(regNum);
   prepareSymbolicValue(state, sf, allocInst);
 }
 
@@ -7133,7 +7136,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
 
 void Executor::getCoveredLines(
     const ExecutionState &state,
-    std::map<const std::string *, std::set<unsigned>> &res) {
+    std::map<std::string, std::set<size_t>> &res) {
   res = state.coveredLines;
 }
 
@@ -7292,9 +7295,9 @@ void Executor::dumpStates() {
            sfIt != sf_ie; ++sfIt) {
         *os << "('" << sfIt->kf->function->getName().str() << "',";
         if (next == es->stack.callStack().end()) {
-          *os << es->prevPC->info->line << "), ";
+          *os << es->prevPC->getLine() << "), ";
         } else {
-          *os << next->caller->info->line << "), ";
+          *os << next->caller->getLine() << "), ";
           ++next;
         }
       }
@@ -7304,7 +7307,7 @@ void Executor::dumpStates() {
       uint64_t md2u =
           computeMinDistToUncovered(es->pc, sf.minDistToUncoveredOnReturn);
       uint64_t icnt = theStatisticManager->getIndexedValue(stats::instructions,
-                                                           es->pc->info->id);
+                                                           es->pc->getGlobalIndex());
       uint64_t cpicnt =
           sf.callPathNode->statistics.getValue(stats::instructions);
 
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 34b8b7bba34..1ccc41c17b0 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -483,7 +483,7 @@ class Executor : public Interpreter {
 
   ref<Expr> readDest(ExecutionState &state, StackFrame &frame,
                      const KInstruction *target) {
-    unsigned index = target->dest;
+    unsigned index = target->getDest();
     ref<Expr> reg = frame.locals[index].value;
     if (!reg) {
       prepareSymbolicRegister(state, frame, index);
@@ -497,7 +497,7 @@ class Executor : public Interpreter {
   }
 
   Cell &getDestCell(const StackFrame &frame, const KInstruction *target) {
-    return frame.locals[target->dest];
+    return frame.locals[target->getDest()];
   }
 
   const Cell &eval(const KInstruction *ki, unsigned index,
@@ -569,9 +569,8 @@ class Executor : public Interpreter {
 
   // Determines the \param lastInstruction of the \param state which is not KLEE
   // internal and returns its InstructionInfo
-  const InstructionInfo &
-  getLastNonKleeInternalInstruction(const ExecutionState &state,
-                                    llvm::Instruction **lastInstruction);
+  const KInstruction *
+  getLastNonKleeInternalInstruction(const ExecutionState &state);
 
   /// Remove state from queue and delete state
   void terminateState(ExecutionState &state,
@@ -733,9 +732,9 @@ class Executor : public Interpreter {
       std::vector<std::unique_ptr<llvm::Module>> &userModules,
       std::vector<std::unique_ptr<llvm::Module>> &libsModules,
       const ModuleOptions &opts,
-      const std::unordered_set<std::string> &mainModuleFunctions,
-      const std::unordered_set<std::string> &mainModuleGlobals,
-      std::unique_ptr<InstructionInfoTable> origInfos,
+            std::set<llvm::StringRef> &mainModuleFunctions,
+            std::set<llvm::StringRef> &mainModuleGlobals,
+            FInstructions &&origInstructions,
       const std::set<std::string> &ignoredExternals,
       std::vector<std::pair<std::string, std::string>> redefinitions) override;
 
@@ -808,7 +807,7 @@ class Executor : public Interpreter {
 
   void getCoveredLines(
       const ExecutionState &state,
-      std::map<const std::string *, std::set<unsigned>> &res) override;
+      std::map<std::string, std::set<size_t>> &res) override;
 
   void getBlockPath(const ExecutionState &state,
                     std::string &blockPath) override;
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 467982c81fb..9a4c6054a05 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -134,7 +134,7 @@ ref<klee::ConstantExpr> Executor::evalConstant(const Constant *c,
       std::string msg("Cannot handle constant ");
       llvm::raw_string_ostream os(msg);
       os << "'" << *c << "' at location "
-         << (ki ? ki->getSourceLocation() : "[unknown]");
+         << (ki ? ki->getSourceLocationString() : "[unknown]");
       klee_error("%s", os.str().c_str());
     }
   }
@@ -261,7 +261,7 @@ ref<ConstantExpr> Executor::evalConstantExpr(const llvm::ConstantExpr *ce,
       std::string msg(
           "Division/modulo by zero during constant folding at location ");
       llvm::raw_string_ostream os(msg);
-      os << (ki ? ki->getSourceLocation() : "[unknown]");
+      os << (ki ? ki->getSourceLocationString() : "[unknown]");
       klee_error("%s", os.str().c_str());
     }
     break;
@@ -271,7 +271,7 @@ ref<ConstantExpr> Executor::evalConstantExpr(const llvm::ConstantExpr *ce,
     if (op2->getLimitedValue() >= op1->getWidth()) {
       std::string msg("Overshift during constant folding at location ");
       llvm::raw_string_ostream os(msg);
-      os << (ki ? ki->getSourceLocation() : "[unknown]");
+      os << (ki ? ki->getSourceLocationString() : "[unknown]");
       klee_error("%s", os.str().c_str());
     }
   }
@@ -282,7 +282,7 @@ ref<ConstantExpr> Executor::evalConstantExpr(const llvm::ConstantExpr *ce,
   switch (ce->getOpcode()) {
   default:
     os << "'" << *ce << "' at location "
-       << (ki ? ki->getSourceLocation() : "[unknown]");
+       << (ki ? ki->getSourceLocationString() : "[unknown]");
     klee_error("%s", os.str().c_str());
 
   case Instruction::Trunc:
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 5522316555f..9200dcaf4b3 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -390,7 +390,7 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) {
     return std::pow(0.5, es->depth);
   case InstCount: {
     uint64_t count = theStatisticManager->getIndexedValue(stats::instructions,
-                                                          es->pc->info->id);
+                                                          es->pc->getGlobalIndex());
     double inv = 1. / std::max((uint64_t)1, count);
     return inv * inv;
   }
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index b45ed1a38d9..eb91576e6a6 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -1001,8 +1001,8 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
                                      executor.updateNameVersion(state, name));
         break;
       case MockStrategy::Deterministic:
-        std::vector<ref<Expr>> args(kf->numArgs);
-        for (size_t i = 0; i < kf->numArgs; i++) {
+        std::vector<ref<Expr>> args(kf->getNumArgs());
+        for (size_t i = 0; i < kf->getNumArgs(); i++) {
           args[i] = executor.getArgumentCell(state, kf, i).value;
         }
         source = SourceBuilder::mockDeterministic(executor.kmodule.get(),
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 372c6fc61b4..88edb4c6a07 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -233,27 +233,28 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
   }
 
   if (useStatistics() || userSearcherRequiresMD2U())
-    theStatisticManager->useIndexedStats(km->infos->getMaxID());
+    theStatisticManager->useIndexedStats(km->getMaxGlobalIndex());
 
   for (auto &kfp : km->functions) {
     KFunction *kf = kfp.get();
-    kf->trackCoverage = 1;
+    //    kf->trackCoverage = 1;
 
     for (unsigned i = 0; i < kf->numInstructions; ++i) {
       KInstruction *ki = kf->instructions[i];
 
       if (OutputIStats) {
-        unsigned id = ki->info->id;
+        unsigned id = ki->getGlobalIndex();
         theStatisticManager->setIndex(id);
-        if (kf->trackCoverage && instructionIsCoverable(ki->inst))
+        if (instructionIsCoverable(ki->inst)) {
           ++stats::uncoveredInstructions;
+        }
       }
 
-      if (kf->trackCoverage) {
-        if (BranchInst *bi = dyn_cast<BranchInst>(ki->inst))
-          if (!bi->isUnconditional())
-            numBranches++;
-      }
+      //      if (kf->trackCoverage) {
+      if (BranchInst *bi = dyn_cast<BranchInst>(ki->inst))
+        if (!bi->isUnconditional())
+          numBranches++;
+      //      }
     }
   }
 
@@ -393,24 +394,25 @@ void StatsTracker::stepInstruction(ExecutionState &es) {
     }
 
     Instruction *inst = es.pc->inst;
-    const InstructionInfo &ii = *es.pc->info;
+    const KInstruction *ki = es.pc;
+    //    const InstructionInfo &ii = *es.pc->info;
     InfoStackFrame &sf = es.stack.infoStack().back();
-    theStatisticManager->setIndex(ii.id);
+    theStatisticManager->setIndex(ki->getGlobalIndex());
     if (UseCallPaths)
       theStatisticManager->setContext(&sf.callPathNode->statistics);
 
     if (es.instsSinceCovNew)
       ++es.instsSinceCovNew;
 
-    if (sf.kf->trackCoverage && instructionIsCoverable(inst)) {
+    if (instructionIsCoverable(inst)) {
       if (!theStatisticManager->getIndexedValue(stats::coveredInstructions,
-                                                ii.id)) {
+                                                ki->getGlobalIndex())) {
         // Checking for actual stoppoints avoids inconsistencies due
         // to line number propogation.
         //
         // FIXME: This trick no longer works, we should fix this in the line
         // number propogation.
-        es.coveredLines[&ii.file].insert(ii.line);
+        es.coveredLines[ki->getSourceFilepath()].insert(ki->getLine());
         es.coveredNew = true;
         es.instsSinceCovNew = 1;
         ++stats::coveredInstructions;
@@ -698,8 +700,9 @@ void StatsTracker::updateStateStatistics(uint64_t addend) {
                                             ie = executor.states.end();
        it != ie; ++it) {
     ExecutionState &state = **it;
-    const InstructionInfo &ii = *state.pc->info;
-    theStatisticManager->incrementIndexedValue(stats::states, ii.id, addend);
+    //    const InstructionInfo &ii = *state.pc->info;
+    theStatisticManager->incrementIndexedValue(
+        stats::states, state.pc->getGlobalIndex(), addend);
     if (UseCallPaths)
       state.stack.infoStack().back().callPathNode->statistics.incrementValue(
           stats::states, addend);
@@ -768,36 +771,44 @@ void StatsTracker::writeIStats() {
 
   of << "ob=" << llvm::sys::path::filename(objectFilename).str() << "\n";
 
-  for (Module::iterator fnIt = m->begin(), fn_ie = m->end(); fnIt != fn_ie;
-       ++fnIt) {
-    if (!fnIt->isDeclaration()) {
+  for (auto &fnIt : *m) {
+    if (!fnIt.isDeclaration()) {
       // Always try to write the filename before the function name, as otherwise
       // KCachegrind can create two entries for the function, one with an
       // unnamed file and one without.
-      Function *fn = &*fnIt;
-      const FunctionInfo &ii = executor.kmodule->infos->getFunctionInfo(*fn);
-      if (ii.file != sourceFile) {
-        of << "fl=" << ii.file << "\n";
-        sourceFile = ii.file;
+      Function *fn = &fnIt;
+      auto fnl = getLocationInfo(fn);
+      //      const FunctionInfo &ii =
+      //      executor.kmodule->infos->getFunctionInfo(*fn);
+      if (fnl.file != sourceFile) {
+        of << "fl=" << fnl.file << "\n";
+        sourceFile = fnl.file;
       }
 
-      of << "fn=" << fnIt->getName().str() << "\n";
-      for (Function::iterator bbIt = fnIt->begin(), bb_ie = fnIt->end();
+      of << "fn=" << fnIt.getName().str() << "\n";
+      for (Function::iterator bbIt = fnIt.begin(), bb_ie = fnIt.end();
            bbIt != bb_ie; ++bbIt) {
         for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end();
              it != ie; ++it) {
           Instruction *instr = &*it;
-          const InstructionInfo &ii = executor.kmodule->infos->getInfo(*instr);
-          unsigned index = ii.id;
-          if (ii.file != sourceFile) {
-            of << "fl=" << ii.file << "\n";
-            sourceFile = ii.file;
+//          const InstructionInfo &ii = executor.kmodule->infos->getInfo(*instr);
+
+          // TODO unify with KInstrtuction
+          auto locationInfo = getLocationInfo(instr);
+
+          unsigned index = executor.kmodule->getGlobalIndex(instr);
+          if (locationInfo.file != sourceFile) {
+            of << "fl=" << locationInfo.file << "\n";
+            sourceFile = locationInfo.file;
           }
 
-          assert(ii.assemblyLine.hasValue());
-          of << ii.assemblyLine.getValue() << " ";
+          { // TODO remove copypaste
+            auto asmLine = executor.kmodule->getAsmLine(instr);
+            assert(asmLine.has_value());
+            of << asmLine.value() << " ";
+          }
 
-          of << ii.line << " ";
+          of << locationInfo.line << " ";
           for (unsigned i = 0; i < nStats; i++)
             if (istatsMask.test(i))
               of << sm.getIndexedValue(sm.getStatistic(i), index) << " ";
@@ -807,27 +818,32 @@ void StatsTracker::writeIStats() {
               (isa<CallInst>(instr) || isa<InvokeInst>(instr))) {
             CallSiteSummaryTable::iterator it = callSiteStats.find(instr);
             if (it != callSiteStats.end()) {
-              for (auto fit = it->second.begin(), fie = it->second.end();
-                   fit != fie; ++fit) {
-                const Function *f = fit->first;
-                CallSiteInfo &csi = fit->second;
-                const FunctionInfo &fii =
-                    executor.kmodule->infos->getFunctionInfo(*f);
-
-                if (fii.file != "" && fii.file != sourceFile)
-                  of << "cfl=" << fii.file << "\n";
+              for (auto &fit : it->second) {
+                const Function *f = fit.first;
+                CallSiteInfo &csi = fit.second;
+                //                const FunctionInfo &fii =
+                //                    executor.kmodule->infos->getFunctionInfo(*f);
+                auto fli = getLocationInfo(f);
+                if (fli.file != "" && fli.file != sourceFile)
+                  of << "cfl=" << fli.file << "\n";
                 of << "cfn=" << f->getName().str() << "\n";
                 of << "calls=" << csi.count << " ";
 
-                assert(fii.assemblyLine.hasValue());
-                of << fii.assemblyLine.getValue() << " ";
+                {
+                  auto asmLine = executor.kmodule->getAsmLine(f);
+                  assert(asmLine.has_value());
+                  of << asmLine.value() << " ";
+                }
 
-                of << fii.line << "\n";
+                of << fli.line << "\n";
 
-                assert(ii.assemblyLine.hasValue());
-                of << ii.assemblyLine.getValue() << " ";
+                {
+                  auto asmLine = executor.kmodule->getAsmLine(instr);
+                  assert(asmLine.has_value());
+                  of << asmLine.value() << " ";
+                }
 
-                of << ii.line << " ";
+                of << locationInfo.line << " ";
                 for (unsigned i = 0; i < nStats; i++) {
                   if (istatsMask.test(i)) {
                     Statistic &s = sm.getStatistic(i);
@@ -892,14 +908,14 @@ uint64_t klee::computeMinDistToUncovered(const KInstruction *ki,
                                          uint64_t minDistAtRA) {
   StatisticManager &sm = *theStatisticManager;
   if (minDistAtRA == 0) { // unreachable on return, best is local
-    return sm.getIndexedValue(stats::minDistToUncovered, ki->info->id);
+    return sm.getIndexedValue(stats::minDistToUncovered, ki->getGlobalIndex());
   } else {
     uint64_t minDistLocal =
-        sm.getIndexedValue(stats::minDistToUncovered, ki->info->id);
+        sm.getIndexedValue(stats::minDistToUncovered, ki->getGlobalIndex());
     uint64_t distToReturn =
-        sm.getIndexedValue(stats::minDistToReturn, ki->info->id);
+        sm.getIndexedValue(stats::minDistToReturn, ki->getGlobalIndex());
 
-    if (distToReturn == 0) { // return unreachable, best is local
+    if (distToReturn == 0) {    // return unreachable, best is local
       return minDistLocal;
     } else if (!minDistLocal) { // no local reachable
       return distToReturn + minDistAtRA;
@@ -913,7 +929,7 @@ void StatsTracker::computeReachableUncovered() {
   KModule *km = executor.kmodule.get();
   const auto m = km->module.get();
   static bool init = true;
-  const InstructionInfoTable &infos = *km->infos;
+  //  const InstructionInfoTable &infos = *km->infos;
   StatisticManager &sm = *theStatisticManager;
 
   if (init) {
@@ -976,11 +992,10 @@ void StatsTracker::computeReachableUncovered() {
       // Not sure if I should bother to preorder here. XXX I should.
       for (Function::iterator bbIt = fnIt->begin(), bb_ie = fnIt->end();
            bbIt != bb_ie; ++bbIt) {
-        for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end();
-             it != ie; ++it) {
-          Instruction *inst = &*it;
+        for (auto &it : *bbIt) {
+          Instruction *inst = &it;
           instructions.push_back(inst);
-          unsigned id = infos.getInfo(*inst).id;
+          unsigned id = km->getGlobalIndex(inst);
           sm.setIndexedValue(stats::minDistToReturn, id, isa<ReturnInst>(inst));
         }
       }
@@ -992,9 +1007,8 @@ void StatsTracker::computeReachableUncovered() {
     bool changed;
     do {
       changed = false;
-      for (auto it = instructions.begin(), ie = instructions.end(); it != ie;
-           ++it) {
-        Instruction *inst = *it;
+      for (auto &instruction : instructions) {
+        Instruction *inst = instruction;
         unsigned bestThrough = 0;
 
         if (isa<CallInst>(inst) || isa<InvokeInst>(inst)) {
@@ -1014,15 +1028,15 @@ void StatsTracker::computeReachableUncovered() {
         }
 
         if (bestThrough) {
-          unsigned id = infos.getInfo(*(*it)).id;
+          unsigned id = km->getGlobalIndex(instruction);
           uint64_t best,
               cur = best = sm.getIndexedValue(stats::minDistToReturn, id);
-          std::vector<Instruction *> succs = getSuccs(*it);
+          std::vector<Instruction *> succs = getSuccs(instruction);
           for (std::vector<Instruction *>::iterator it2 = succs.begin(),
                                                     ie = succs.end();
                it2 != ie; ++it2) {
             uint64_t dist = sm.getIndexedValue(stats::minDistToReturn,
-                                               infos.getInfo(*(*it2)).id);
+                                               km->getGlobalIndex(*it2));
             if (dist) {
               uint64_t val = bestThrough + dist;
               if (best == 0 || val < best)
@@ -1058,7 +1072,7 @@ void StatsTracker::computeReachableUncovered() {
       for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end(); it != ie;
            ++it) {
         Instruction *inst = &*it;
-        unsigned id = infos.getInfo(*inst).id;
+        unsigned id = km->getGlobalIndex(inst);
         instructions.push_back(inst);
         sm.setIndexedValue(
             stats::minDistToUncovered, id,
@@ -1073,29 +1087,24 @@ void StatsTracker::computeReachableUncovered() {
   bool changed;
   do {
     changed = false;
-    for (std::vector<Instruction *>::iterator it = instructions.begin(),
-                                              ie = instructions.end();
-         it != ie; ++it) {
-      Instruction *inst = *it;
+    for (auto inst : instructions) {
       uint64_t best, cur = best = sm.getIndexedValue(stats::minDistToUncovered,
-                                                     infos.getInfo(*inst).id);
+                                                     km->getGlobalIndex(inst));
       unsigned bestThrough = 0;
 
       if (isa<CallInst>(inst) || isa<InvokeInst>(inst)) {
         std::vector<Function *> &targets = callTargets[inst];
-        for (std::vector<Function *>::iterator fnIt = targets.begin(),
-                                               ie = targets.end();
-             fnIt != ie; ++fnIt) {
-          uint64_t dist = functionShortestPath[*fnIt];
+        for (auto &target : targets) {
+          uint64_t dist = functionShortestPath[target];
           if (dist) {
             dist = 1 + dist; // count instruction itself
             if (bestThrough == 0 || dist < bestThrough)
               bestThrough = dist;
           }
 
-          if (!(*fnIt)->isDeclaration()) {
+          if (!target->isDeclaration()) {
             uint64_t calleeDist = sm.getIndexedValue(
-                stats::minDistToUncovered, infos.getFunctionInfo(*(*fnIt)).id);
+                stats::minDistToUncovered, km->getGlobalIndex(target));
             if (calleeDist) {
               calleeDist = 1 + calleeDist; // count instruction itself
               if (best == 0 || calleeDist < best)
@@ -1109,11 +1118,9 @@ void StatsTracker::computeReachableUncovered() {
 
       if (bestThrough) {
         std::vector<Instruction *> succs = getSuccs(inst);
-        for (std::vector<Instruction *>::iterator it2 = succs.begin(),
-                                                  ie = succs.end();
-             it2 != ie; ++it2) {
+        for (auto &succ : succs) {
           uint64_t dist = sm.getIndexedValue(stats::minDistToUncovered,
-                                             infos.getInfo(*(*it2)).id);
+                                             km->getGlobalIndex(succ));
           if (dist) {
             uint64_t val = bestThrough + dist;
             if (best == 0 || val < best)
@@ -1123,7 +1130,7 @@ void StatsTracker::computeReachableUncovered() {
       }
 
       if (best != cur) {
-        sm.setIndexedValue(stats::minDistToUncovered, infos.getInfo(*inst).id,
+        sm.setIndexedValue(stats::minDistToUncovered, km->getGlobalIndex(inst),
                            best);
         changed = true;
       }
diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp
index 9b827931b2b..2bdfb4a5073 100644
--- a/lib/Core/TargetedExecutionManager.cpp
+++ b/lib/Core/TargetedExecutionManager.cpp
@@ -318,26 +318,34 @@ TargetedExecutionManager::LocationToBlocks
 TargetedExecutionManager::prepareAllLocations(KModule *kmodule,
                                               Locations &locations) const {
   LocationToBlocks locToBlocks;
-  const auto &infos = kmodule->infos;
+//  const auto &infos = kmodule->infos;
+
+  std::unordered_map<std::string, std::unordered_set<const llvm::Function *>>
+      fileNameToFunctions;
+
+  for (const auto &kfunc : kmodule->functions) {
+    fileNameToFunctions[kfunc->getSourceFilepath()].insert(kfunc->function);
+  }
+
   for (auto it = locations.begin(); it != locations.end(); ++it) {
     auto loc = *it;
     auto precision = Precision::LineLevel;
     Blocks blocks;
-    for (const auto &fileName : infos->getFilesNames()) {
-      if (kmodule->origInfos.count(fileName) == 0) {
+    for (const auto &[fileName, origInstsInFile] : kmodule->origInstructions) {
+      if (kmodule->origInstructions.count(fileName) == 0) {
         continue;
       }
       if (!loc->isInside(fileName)) {
         continue;
       }
 
-      const auto &relatedFunctions =
-          infos->getFileNameToFunctions().at(fileName);
+      const auto &relatedFunctions = fileNameToFunctions.at(fileName);
 
       for (const auto func : relatedFunctions) {
         const auto kfunc = kmodule->functionMap[func];
-        const auto &fi = infos->getFunctionInfo(*kfunc->function);
-        const auto &origInstsInFile = kmodule->origInfos.at(fi.file);
+        //        const auto &fi = infos->getFunctionInfo(*kfunc->function);
+        //        const auto &origInstsInFile =
+        //            kmodule->origInstructions.at(kfunc->getSourceFilepath());
 
         for (const auto &kblock : kfunc->blocks) {
           BlockWithPrecision bp(kblock.get(), precision);
@@ -534,7 +542,7 @@ TargetedExecutionManager::prepareTargets(KModule *kmodule, SarifReport paths) {
 void TargetedExecutionManager::reportFalseNegative(ExecutionState &state,
                                                    ReachWithError error) {
   klee_warning("100.00%% %s False Negative at: %s", getErrorString(error),
-               state.prevPC->getSourceLocation().c_str());
+               state.prevPC->getSourceLocationString().c_str());
 }
 
 bool TargetedExecutionManager::reportTruePositive(ExecutionState &state,
diff --git a/lib/Core/TargetedExecutionManager.h b/lib/Core/TargetedExecutionManager.h
index 7d5b285d41f..011cbf86b67 100644
--- a/lib/Core/TargetedExecutionManager.h
+++ b/lib/Core/TargetedExecutionManager.h
@@ -96,12 +96,6 @@ class TargetedExecutionManager {
   using StatesSet = std::unordered_set<ExecutionState *>;
   using TargetToStateUnorderedSetMap = TargetHashMap<StatesSet>;
 
-  using Instructions = std::unordered_map<
-      std::string,
-      std::unordered_map<
-          unsigned int,
-          std::unordered_map<unsigned int, std::unordered_set<unsigned int>>>>;
-
   std::unordered_set<std::string> brokenTraces;
   std::unordered_set<std::string> reportedTraces;
 
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index c544c23b263..42fb26a144c 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -409,7 +409,7 @@ class PPrinter : public ExprPPrinter {
       auto kf = s->km->functionMap.at(s->allocSite.getFunction());
       auto ki = kf->instructionMap.at(&s->allocSite);
       auto kb = ki->parent;
-      PC << ki->index << " " << kb->getLabel() << " " << kf->getName().str()
+      PC << ki->getIndex() << " " << kb->getLabel() << " " << kf->getName().str()
          << " " << s->index;
     } else if (auto s = dyn_cast<IrreproducibleSource>(source)) {
       PC << s->name;
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 1196471f712..eab66bd1aed 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -623,8 +623,8 @@ SourceResult ParserImpl::ParseMockDeterministicSource() {
   ConsumeExpectedToken(Token::Identifier);
   ConsumeLParen();
   std::vector<ref<Expr>> args;
-  args.reserve(kf->numArgs);
-  for (unsigned i = 0; i < kf->numArgs; i++) {
+  args.reserve(kf->getNumArgs());
+  for (unsigned i = 0; i < kf->getNumArgs(); i++) {
     auto expr = ParseExpr(TypeResult());
     if (!expr.isValid()) {
       return {false, nullptr};
diff --git a/lib/Expr/Path.cpp b/lib/Expr/Path.cpp
index 7b578aa30c7..e67abd51b46 100644
--- a/lib/Expr/Path.cpp
+++ b/lib/Expr/Path.cpp
@@ -15,8 +15,8 @@ using namespace llvm;
 
 void Path::advance(KInstruction *ki) {
   if (KBlocks.empty()) {
-    firstInstruction = ki->index;
-    lastInstruction = ki->index;
+    firstInstruction = ki->getIndex();
+    lastInstruction = ki->getIndex();
     KBlocks.push_back(ki->parent);
     return;
   }
@@ -24,8 +24,7 @@ void Path::advance(KInstruction *ki) {
   if (ki->parent != lastBlock) {
     KBlocks.push_back(ki->parent);
   }
-  lastInstruction = ki->index;
-  return;
+  lastInstruction = ki->getIndex();
 }
 
 unsigned Path::KBlockSize() const { return KBlocks.size(); }
diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp
index 0831277d96b..3bda4955743 100644
--- a/lib/Expr/SymbolicSource.cpp
+++ b/lib/Expr/SymbolicSource.cpp
@@ -98,8 +98,8 @@ int ArgumentSource::internalCompare(const SymbolicSource &b) const {
   assert(km == ab.km);
   auto parent = allocSite.getParent();
   auto bParent = ab.allocSite.getParent();
-  if (km->functionIDMap.at(parent) != km->functionIDMap.at(bParent)) {
-    return km->functionIDMap.at(parent) < km->functionIDMap.at(bParent) ? -1
+  if (km->getFunctionId(parent) != km->getFunctionId(bParent)) {
+    return km->getFunctionId(parent) < km->getFunctionId(bParent) ? -1
                                                                         : 1;
   }
   if (allocSite.getArgNo() != ab.allocSite.getArgNo()) {
@@ -119,20 +119,21 @@ int InstructionSource::internalCompare(const SymbolicSource &b) const {
   assert(km == ib.km);
   auto function = allocSite.getParent()->getParent();
   auto bFunction = ib.allocSite.getParent()->getParent();
-  if (km->functionIDMap.at(function) != km->functionIDMap.at(bFunction)) {
-    return km->functionIDMap.at(function) < km->functionIDMap.at(bFunction) ? -1
+  if (km->getFunctionId(function) != km->getFunctionId(bFunction)) {
+    return km->getFunctionId(function) < km->getFunctionId(bFunction) ? -1
                                                                             : 1;
   }
   auto kf = km->functionMap.at(function);
   auto block = allocSite.getParent();
   auto bBlock = ib.allocSite.getParent();
-  if (kf->blockMap[block]->id != kf->blockMap[bBlock]->id) {
-    return kf->blockMap[block]->id < kf->blockMap[bBlock]->id ? -1 : 1;
+  if (kf->blockMap[block]->getId() != kf->blockMap[bBlock]->getId()) {
+    return kf->blockMap[block]->getId() < kf->blockMap[bBlock]->getId() ? -1
+                                                                        : 1;
   }
-  if (kf->instructionMap[&allocSite]->index !=
-      kf->instructionMap[&ib.allocSite]->index) {
-    return kf->instructionMap[&allocSite]->index <
-                   kf->instructionMap[&ib.allocSite]->index
+  if (kf->instructionMap[&allocSite]->getIndex() !=
+      kf->instructionMap[&ib.allocSite]->getIndex()) {
+    return kf->instructionMap[&allocSite]->getIndex() <
+                   kf->instructionMap[&ib.allocSite]->getIndex()
                ? -1
                : 1;
   }
@@ -143,7 +144,7 @@ unsigned ArgumentSource::computeHash() {
   unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + index;
   auto parent = allocSite.getParent();
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) +
-        km->functionIDMap.at(parent);
+        km->getFunctionId(parent);
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + allocSite.getArgNo();
   hashValue = res;
   return hashValue;
@@ -155,17 +156,18 @@ unsigned InstructionSource::computeHash() {
   auto kf = km->functionMap.at(function);
   auto block = allocSite.getParent();
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) +
-        km->functionIDMap.at(function);
-  res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + kf->blockMap[block]->id;
+        km->getFunctionId(function);
+  res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) +
+        kf->blockMap[block]->getId();
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) +
-        kf->instructionMap[&allocSite]->index;
+        kf->instructionMap[&allocSite]->getIndex();
   hashValue = res;
   return hashValue;
 }
 
 unsigned MockNaiveSource::computeHash() {
   unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + version;
-  unsigned funcID = km->functionIDMap.at(&function);
+  unsigned funcID = km->functionMap.at(&function)->getGlobalIndex();
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + funcID;
   hashValue = res;
   return res;
@@ -179,8 +181,8 @@ int MockNaiveSource::internalCompare(const SymbolicSource &b) const {
   if (version != mnb.version) {
     return version < mnb.version ? -1 : 1;
   }
-  unsigned funcID = km->functionIDMap.at(&function);
-  unsigned bFuncID = mnb.km->functionIDMap.at(&mnb.function);
+  unsigned funcID = km->functionMap.at(&function)->getGlobalIndex();
+  unsigned bFuncID = mnb.km->functionMap.at(&mnb.function)->getGlobalIndex();
   if (funcID != bFuncID) {
     return funcID < bFuncID ? -1 : 1;
   }
@@ -195,7 +197,7 @@ MockDeterministicSource::MockDeterministicSource(
 unsigned MockDeterministicSource::computeHash() {
   unsigned res = getKind();
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) +
-        km->functionIDMap.at(&function);
+        km->functionMap.at(&function)->getGlobalIndex();
   for (const auto &arg : args) {
     res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + arg->hash();
   }
@@ -209,8 +211,8 @@ int MockDeterministicSource::internalCompare(const SymbolicSource &b) const {
   }
   const MockDeterministicSource &mdb =
       static_cast<const MockDeterministicSource &>(b);
-  unsigned funcID = km->functionIDMap.at(&function);
-  unsigned bFuncID = mdb.km->functionIDMap.at(&mdb.function);
+  unsigned funcID = km->functionMap.at(&function)->getGlobalIndex();
+  unsigned bFuncID = mdb.km->functionMap.at(&mdb.function)->getGlobalIndex();
   if (funcID != bFuncID) {
     return funcID < bFuncID ? -1 : 1;
   }
diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
index ee66e91cbf0..3c2b613e874 100644
--- a/lib/Module/InstructionInfoTable.cpp
+++ b/lib/Module/InstructionInfoTable.cpp
@@ -34,197 +34,126 @@ DISABLE_WARNING_POP
 #include <map>
 #include <string>
 
-using namespace klee;
-
-class InstructionToLineAnnotator : public llvm::AssemblyAnnotationWriter {
-private:
-  std::unordered_map<uintptr_t, uint64_t> mapping = {};
-
-public:
-  void emitInstructionAnnot(const llvm::Instruction *i,
-                            llvm::formatted_raw_ostream &os) override {
-    os.flush();
-    mapping.emplace(reinterpret_cast<std::uintptr_t>(i), os.getLine() + 1);
-  }
-
-  void emitFunctionAnnot(const llvm::Function *f,
-                         llvm::formatted_raw_ostream &os) override {
-    os.flush();
-    mapping.emplace(reinterpret_cast<std::uintptr_t>(f), os.getLine() + 1);
-  }
-
-  std::unordered_map<uintptr_t, uint64_t> getMapping() const { return mapping; }
-};
-
-static std::unordered_map<uintptr_t, uint64_t>
-buildInstructionToLineMap(const llvm::Module &m,
-                          std::unique_ptr<llvm::raw_fd_ostream> assemblyFS) {
-
-  InstructionToLineAnnotator a;
-
-  m.print(*assemblyFS, &a);
-  assemblyFS->flush();
-
-  return a.getMapping();
-}
+namespace klee {
 
 class DebugInfoExtractor {
-  std::vector<std::unique_ptr<std::string>> &internedStrings;
-  std::unordered_map<uintptr_t, uint64_t> lineTable;
 
   const llvm::Module &module;
-  bool withAsm = false;
 
 public:
-  DebugInfoExtractor(
-      std::vector<std::unique_ptr<std::string>> &_internedStrings,
-      const llvm::Module &_module,
-      std::unique_ptr<llvm::raw_fd_ostream> assemblyFS)
-      : internedStrings(_internedStrings), module(_module) {
-    if (assemblyFS) {
-      withAsm = true;
-      lineTable = buildInstructionToLineMap(module, std::move(assemblyFS));
-    }
-  }
-
-  std::string &getInternedString(const std::string &s) {
-    auto found = std::find_if(internedStrings.begin(), internedStrings.end(),
-                              [&s](const std::unique_ptr<std::string> &item) {
-                                return *item.get() == s;
-                              });
-    if (found != internedStrings.end())
-      return *found->get();
-
-    auto newItem = std::unique_ptr<std::string>(new std::string(s));
-    auto result = newItem.get();
-
-    internedStrings.emplace_back(std::move(newItem));
-    return *result;
-  }
-
-  std::unique_ptr<FunctionInfo> getFunctionInfo(const llvm::Function &Func) {
-    llvm::Optional<uint64_t> asmLine;
-    if (withAsm) {
-      asmLine = lineTable.at(reinterpret_cast<std::uintptr_t>(&Func));
-    }
-    auto dsub = Func.getSubprogram();
+  DebugInfoExtractor(const llvm::Module &_module)
+      : module(_module) {}
+
+//  std::unique_ptr<FunctionInfo> getFunctionInfo(const llvm::Function &Func) {
+//    // Fallback: Mark as unknown
+//    return std::make_unique<FunctionInfo>(FunctionInfo(0));
+//  }
+
+//  std::unique_ptr<InstructionInfo>
+//  getInstructionInfo(const llvm::Instruction &Inst, const FunctionInfo *f) {
+//    return std::make_unique<InstructionInfo>(InstructionInfo(0));
+//  }
+};
 
-    if (dsub != nullptr) {
-      auto path = dsub->getFilename();
-      return std::make_unique<FunctionInfo>(FunctionInfo(
-          0, getInternedString(path.str()), dsub->getLine(), asmLine));
-    }
+// TODO need some unify with kFunction
+LocationInfo getLocationInfo(const llvm::Function *func) {
+  const auto dsub = func->getSubprogram();
 
-    // Fallback: Mark as unknown
-    return std::make_unique<FunctionInfo>(
-        FunctionInfo(0, getInternedString(""), 0, asmLine));
+  if (dsub != nullptr) {
+    auto path = dsub->getFilename();
+    return {path.str(), dsub->getLine(), 0}; // TODO why not use column here?
   }
 
-  std::unique_ptr<InstructionInfo>
-  getInstructionInfo(const llvm::Instruction &Inst, const FunctionInfo *f) {
-    llvm::Optional<uint64_t> asmLine;
-    if (withAsm) {
-      asmLine = lineTable.at(reinterpret_cast<std::uintptr_t>(&Inst));
-    }
-
-    // Retrieve debug information associated with instruction
-    auto dl = Inst.getDebugLoc();
-
-    // Check if a valid debug location is assigned to the instruction.
-    if (dl.get() != nullptr) {
-      auto full_path = dl.get()->getFilename();
-      auto line = dl.getLine();
-      auto column = dl.getCol();
-
-      // Still, if the line is unknown, take the context of the instruction to
-      // narrow it down
-      if (line == 0) {
-        if (auto LexicalBlock =
-                llvm::dyn_cast<llvm::DILexicalBlock>(dl.getScope())) {
-          line = LexicalBlock->getLine();
-          column = LexicalBlock->getColumn();
-        }
-      }
-      return std::make_unique<InstructionInfo>(InstructionInfo(
-          0, getInternedString(full_path.str()), line, column, asmLine));
-    }
-
-    if (f != nullptr)
-      // If nothing found, use the surrounding function
-      return std::make_unique<InstructionInfo>(
-          InstructionInfo(0, f->file, f->line, 0, asmLine));
-    // If nothing found, use the surrounding function
-    return std::make_unique<InstructionInfo>(
-        InstructionInfo(0, getInternedString(""), 0, 0, asmLine));
-  }
-};
+  return {"", 0, 0};
+}
 
-InstructionInfoTable::InstructionInfoTable(
-    const llvm::Module &m, std::unique_ptr<llvm::raw_fd_ostream> assemblyFS,
-    bool withInstructions) {
-  // Generate all debug instruction information
-  DebugInfoExtractor DI(internedStrings, m, std::move(assemblyFS));
-
-  for (const auto &Func : m) {
-    auto F = DI.getFunctionInfo(Func);
-    auto FR = F.get();
-    functionInfos.emplace(&Func, std::move(F));
-
-    for (auto it = llvm::inst_begin(Func), ie = llvm::inst_end(Func); it != ie;
-         ++it) {
-      auto instr = &*it;
-      auto instInfo = DI.getInstructionInfo(*instr, FR);
-      if (withInstructions) {
-        insts[instInfo->file][instInfo->line][instInfo->column].insert(
-            instr->getOpcode());
+// TODO need some unify with kInstruction
+LocationInfo getLocationInfo(const llvm::Instruction *inst) {
+  // Retrieve debug information associated with instruction
+  const auto &dl = inst->getDebugLoc();
+
+  // Check if a valid debug location is assigned to the instruction.
+  if (dl.get() != nullptr) {
+    auto full_path = dl->getFilename();
+    auto line = dl.getLine();
+    auto column = dl.getCol();
+
+    // Still, if the line is unknown, take the context of the instruction to
+    // narrow it down
+    if (line == 0) {
+      if (auto LexicalBlock =
+              llvm::dyn_cast<llvm::DILexicalBlock>(dl.getScope())) {
+        line = LexicalBlock->getLine();
+        column = LexicalBlock->getColumn();
       }
-      filesNames.insert(instInfo->file);
-      fileNameToFunctions[instInfo->file].insert(&Func);
-      infos.emplace(instr, std::move(instInfo));
     }
+    return {full_path.str(), line, column};
   }
 
-  // Make sure that every item has a unique ID
-  size_t idCounter = 0;
-  for (auto &item : infos)
-    item.second->id = idCounter++;
-  for (auto &item : functionInfos)
-    item.second->id = idCounter++;
-}
-
-unsigned InstructionInfoTable::getMaxID() const {
-  return infos.size() + functionInfos.size();
+  return getLocationInfo(inst->getParent()->getParent());
 }
 
-const InstructionInfo &
-InstructionInfoTable::getInfo(const llvm::Instruction &inst) const {
-  auto it = infos.find(&inst);
-  if (it == infos.end())
-    llvm::report_fatal_error("invalid instruction, not present in "
-                             "initial module!");
-  return *it->second.get();
-}
-
-const FunctionInfo &
-InstructionInfoTable::getFunctionInfo(const llvm::Function &f) const {
-  auto found = functionInfos.find(&f);
-  if (found == functionInfos.end())
-    llvm::report_fatal_error("invalid instruction, not present in "
-                             "initial module!");
-
-  return *found->second.get();
-}
-
-const InstructionInfoTable::LocationToFunctionsMap &
-InstructionInfoTable::getFileNameToFunctions() const {
-  return fileNameToFunctions;
-}
+//InstructionInfoTable::InstructionInfoTable(const llvm::Module &m) {
+//  // Generate all debug instruction information
+//  DebugInfoExtractor DI(m);
+//
+//  for (const auto &Func : m) {
+//    auto F = DI.getFunctionInfo(Func);
+//    auto FR = F.get();
+//    functionInfos.emplace(&Func, std::move(F));
+//
+//    for (auto it = llvm::inst_begin(Func), ie = llvm::inst_end(Func); it != ie;
+//         ++it) {
+//      auto instr = &*it;
+//      auto instInfo = DI.getInstructionInfo(*instr, FR);
+//      auto locationInfo = getLocationInfo(instr);
+////      if (withInstructions) {
+////        insts[locationInfo.file][locationInfo.line][locationInfo.column].insert(
+////            instr->getOpcode());
+////      }
+//      fileNameToFunctions[locationInfo.file].insert(&Func);
+//      infos.emplace(instr, std::move(instInfo));
+//    }
+//  }
+//
+//  // Make sure that every item has a unique ID
+//  size_t idCounter = 0;
+////  for (auto &item : infos)
+////    item.second->id = idCounter++;
+////  for (auto &item : functionInfos)
+////    item.second->id = idCounter++;
+//}
+
+//unsigned InstructionInfoTable::getMaxID() const {
+//  return infos.size() + functionInfos.size();
+//}
+
+//const InstructionInfo &
+//InstructionInfoTable::getInfo(const llvm::Instruction &inst) const {
+//  auto it = infos.find(&inst);
+//  if (it == infos.end())
+//    llvm::report_fatal_error("invalid instruction, not present in "
+//                             "initial module!");
+//  return *it->second.get();
+//}
+//
+//const FunctionInfo &
+//InstructionInfoTable::getFunctionInfo(const llvm::Function &f) const {
+//  auto found = functionInfos.find(&f);
+//  if (found == functionInfos.end())
+//    llvm::report_fatal_error("invalid instruction, not present in "
+//                             "initial module!");
+//
+//  return *found->second.get();
+//}
+//
+//const InstructionInfoTable::LocationToFunctionsMap &
+//InstructionInfoTable::getFileNameToFunctions() const {
+//  return fileNameToFunctions;
+//}
 
-const std::unordered_set<std::string> &
-InstructionInfoTable::getFilesNames() const {
-  return filesNames;
-}
+//InstructionInfoTable::Instructions InstructionInfoTable::getInstructions() {
+//  return std::move(insts);
+//}
 
-InstructionInfoTable::Instructions InstructionInfoTable::getInstructions() {
-  return std::move(insts);
-}
+} // namespace klee
diff --git a/lib/Module/KInstruction.cpp b/lib/Module/KInstruction.cpp
index f7159c4bd66..fa3028c3efb 100644
--- a/lib/Module/KInstruction.cpp
+++ b/lib/Module/KInstruction.cpp
@@ -8,14 +8,19 @@
 //===----------------------------------------------------------------------===//
 
 #include "klee/Module/KInstruction.h"
+#include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KModule.h"
 
 #include "klee/Support/CompilerWarning.h"
 DISABLE_WARNING_PUSH
 DISABLE_WARNING_DEPRECATED_DECLARATIONS
+#include "klee/Support/ErrorHandling.h"
 #include "llvm/ADT/StringExtras.h"
+#include "llvm/IR/DebugInfoMetadata.h"
 DISABLE_WARNING_POP
 
+#include <llvm/IR/InstrTypes.h>
+#include <llvm/IR/Instructions.h>
 #include <string>
 
 using namespace llvm;
@@ -23,17 +28,98 @@ using namespace klee;
 
 /***/
 
+static int getOperandNum(
+    Value *v,
+    const std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
+    KModule *km, KInstruction *ki) {
+  if (Instruction *inst = dyn_cast<Instruction>(v)) {
+    return instructionToRegisterMap.at(inst);
+  } else if (Argument *a = dyn_cast<Argument>(v)) {
+    return a->getArgNo();
+  } else if (isa<BasicBlock>(v) || isa<InlineAsm>(v) ||
+             isa<MetadataAsValue>(v)) {
+    return -1;
+  } else {
+    assert(isa<Constant>(v));
+    Constant *c = cast<Constant>(v);
+    return -(km->getConstantID(c, ki) + 2);
+  }
+}
+
+KInstruction::KInstruction(
+    const std::unordered_map<llvm::Instruction *, unsigned>
+        &_instructionToRegisterMap,
+    llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
+    unsigned &_globalIndexInc)
+    : inst(_inst), parent(_kb), globalIndex(_globalIndexInc++) {
+  //  ki->parent = this;
+  //  ki->index = i;
+  //  ki->dest = instructionToRegisterMap[inst];
+  if (isa<llvm::CallInst>(inst) || isa<llvm::InvokeInst>(inst)) {
+    const llvm::CallBase &cs = cast<llvm::CallBase>(*inst);
+    Value *val = cs.getCalledOperand();
+    unsigned numArgs = cs.arg_size();
+    operands = new int[numArgs + 1];
+    operands[0] = getOperandNum(val, _instructionToRegisterMap, _km, this);
+    for (unsigned j = 0; j < numArgs; j++) {
+      Value *v = cs.getArgOperand(j);
+      operands[j + 1] = getOperandNum(v, _instructionToRegisterMap, _km, this);
+    }
+  } else {
+    unsigned numOperands = inst->getNumOperands();
+    operands = new int[numOperands];
+    for (unsigned j = 0; j < numOperands; j++) {
+      Value *v = inst->getOperand(j);
+      operands[j] = getOperandNum(v, _instructionToRegisterMap, _km, this);
+    }
+  }
+}
+
 KInstruction::~KInstruction() { delete[] operands; }
 
-std::string KInstruction::getSourceLocation() const {
-  if (!info->file.empty())
-    return info->file + ":" + std::to_string(info->line) + " " +
-           std::to_string(info->column);
-  else
+size_t KInstruction::getLine() const {
+  auto locationInfo = getLocationInfo(inst);
+  return locationInfo.line;
+}
+
+size_t KInstruction::getColumn() const {
+  auto locationInfo = getLocationInfo(inst);
+  return locationInfo.column;
+}
+
+// TODO problem files with same name
+std::string KInstruction::getSourceFilepath() const {
+  auto locationInfo = getLocationInfo(inst);
+  return locationInfo.file;
+}
+
+std::string KInstruction::getSourceLocationString() const {
+  std::string filePath = getSourceFilepath();
+  if (!filePath.empty()) {
+    // TODO change format to file:line:column
+    return filePath + ":" + std::to_string(getLine()) + " " +
+           std::to_string(getColumn());
+  } else {
     return "[no debug info]";
+  }
 }
 
 std::string KInstruction::toString() const {
-  return llvm::utostr(index) + " at " + parent->toString() + " (" +
+  return llvm::utostr(getIndex()) + " at " + parent->toString() + " (" +
          inst->getOpcodeName() + ")";
 }
+
+unsigned KInstruction::getGlobalIndex() const { return globalIndex; }
+
+unsigned KInstruction::getIndex() const {
+  return getGlobalIndex() - getKFunction()->getGlobalIndex() -
+         getKBlock()->getId() - 1;
+}
+
+unsigned KInstruction::getDest() const {
+  return parent->parent->getNumArgs() + getIndex() +
+         (parent->instructions - parent->parent->instructions);
+}
+KBlock *KInstruction::getKBlock() const { return parent; }
+KFunction *KInstruction::getKFunction() const { return getKBlock()->parent; }
+KModule *KInstruction::getKModule() const { return getKFunction()->parent; }
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 2ab1059a8f3..75df8097ba8 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -26,6 +26,7 @@
 DISABLE_WARNING_PUSH
 DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Bitcode/BitcodeWriter.h"
+#include "llvm/IR/AssemblyAnnotationWriter.h"
 #include "llvm/IR/DataLayout.h"
 #include "llvm/IR/Function.h"
 #include "llvm/IR/IRBuilder.h"
@@ -37,6 +38,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/IR/Verifier.h"
 #include "llvm/Linker/Linker.h"
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/FormattedStream.h"
 #include "llvm/Support/Path.h"
 #include "llvm/Support/raw_os_ostream.h"
 #include "llvm/Support/raw_ostream.h"
@@ -46,7 +48,10 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Transforms/Utils/Cloning.h"
 DISABLE_WARNING_POP
 
+#include <llvm/Support/FormattedStream.h>
+#include <memory>
 #include <sstream>
+#include <utility>
 
 using namespace llvm;
 using namespace klee;
@@ -337,6 +342,38 @@ void KModule::optimiseAndPrepare(
   pm3.run(*module);
 }
 
+class InstructionToLineAnnotator : public llvm::AssemblyAnnotationWriter {
+private:
+  std::unordered_map<uintptr_t, uint64_t> mapping = {};
+
+public:
+  void emitInstructionAnnot(const llvm::Instruction *i,
+                            llvm::formatted_raw_ostream &os) override {
+    os.flush();
+    mapping.emplace(reinterpret_cast<std::uintptr_t>(i), os.getLine() + 1);
+  }
+
+  void emitFunctionAnnot(const llvm::Function *f,
+                         llvm::formatted_raw_ostream &os) override {
+    os.flush();
+    mapping.emplace(reinterpret_cast<std::uintptr_t>(f), os.getLine() + 1);
+  }
+
+  std::unordered_map<uintptr_t, uint64_t> getMapping() const { return mapping; }
+};
+
+static std::unordered_map<uintptr_t, uint64_t>
+buildInstructionToLineMap(const llvm::Module &m,
+                          std::unique_ptr<llvm::raw_fd_ostream> assemblyFS) {
+
+  InstructionToLineAnnotator a;
+
+  m.print(*assemblyFS, &a);
+  assemblyFS->flush();
+
+  return a.getMapping();
+}
+
 void KModule::manifest(InterpreterHandler *ih,
                        Interpreter::GuidanceKind guidance,
                        bool forceSourceOutput) {
@@ -351,20 +388,21 @@ void KModule::manifest(InterpreterHandler *ih,
     std::unique_ptr<llvm::raw_fd_ostream> assemblyFS;
     if (OutputSource || forceSourceOutput) {
       assemblyFS = ih->openOutputFile("assembly.ll");
+      asmLineMap = buildInstructionToLineMap(*module, std::move(assemblyFS));
     }
-    infos =
-        std::make_unique<InstructionInfoTable>(*module, std::move(assemblyFS));
+//    infos = std::make_unique<InstructionInfoTable>(*module);
   }
 
   std::vector<Function *> declarations;
 
   unsigned functionID = 0;
+  maxGlobalIndex = 0;
   for (auto &Function : module->functions()) {
     if (Function.isDeclaration()) {
       declarations.push_back(&Function);
     }
 
-    auto kf = std::unique_ptr<KFunction>(new KFunction(&Function, this));
+    auto kf = std::make_unique<KFunction>(&Function, this, maxGlobalIndex);
 
     llvm::Function *function = &Function;
     for (auto &BasicBlock : *function) {
@@ -372,11 +410,11 @@ void KModule::manifest(InterpreterHandler *ih,
       KBlock *kb = kf->blockMap[&BasicBlock];
       for (unsigned i = 0; i < numInstructions; ++i) {
         KInstruction *ki = kb->instructions[i];
-        ki->info = &infos->getInfo(*ki->inst);
+//        ki->info = &infos->getInfo(*ki->inst);
       }
     }
 
-    functionIDMap.insert({&Function, functionID});
+    //    functionIDMap[&Function] = functionID;
     kf->id = functionID;
     functionID++;
     functionNameMap.insert({kf->getName().str(), kf.get()});
@@ -426,6 +464,19 @@ void KModule::manifest(InterpreterHandler *ih,
   }
 }
 
+std::optional<size_t> KModule::getAsmLine(const uintptr_t ref) const {
+  if (!asmLineMap.empty()) {
+    return asmLineMap.at(ref);
+  }
+  return std::nullopt;
+}
+std::optional<size_t> KModule::getAsmLine(const llvm::Function *func) const {
+  return getAsmLine(reinterpret_cast<std::uintptr_t>(func));
+}
+std::optional<size_t> KModule::getAsmLine(const llvm::Instruction *inst) const {
+  return getAsmLine(reinterpret_cast<std::uintptr_t>(inst));
+}
+
 void KModule::checkModule() {
   InstructionOperandTypeCheckPass *operandTypeCheckPass =
       new InstructionOperandTypeCheckPass();
@@ -502,6 +553,18 @@ unsigned KModule::getConstantID(Constant *c, KInstruction *ki) {
   return id;
 }
 
+unsigned KModule::getFunctionId(const llvm::Function *func) const {
+  return functionMap.at(func)->id;
+}
+unsigned KModule::getGlobalIndex(const llvm::Function *func) const {
+  return functionMap.at(func)->getGlobalIndex();
+}
+unsigned KModule::getGlobalIndex(const llvm::Instruction *inst) const {
+  return functionMap.at(inst->getFunction())
+      ->instructionMap.at(inst)
+      ->getGlobalIndex();
+}
+
 /***/
 
 KConstant::KConstant(llvm::Constant *_ct, unsigned _id, KInstruction *_ki) {
@@ -510,76 +573,28 @@ KConstant::KConstant(llvm::Constant *_ct, unsigned _id, KInstruction *_ki) {
   ki = _ki;
 }
 
-/***/
-
-static int getOperandNum(
-    Value *v,
-    std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
-    KModule *km, KInstruction *ki) {
-  if (Instruction *inst = dyn_cast<Instruction>(v)) {
-    return instructionToRegisterMap[inst];
-  } else if (Argument *a = dyn_cast<Argument>(v)) {
-    return a->getArgNo();
-  } else if (isa<BasicBlock>(v) || isa<InlineAsm>(v) ||
-             isa<MetadataAsValue>(v)) {
-    return -1;
-  } else {
-    assert(isa<Constant>(v));
-    Constant *c = cast<Constant>(v);
-    return -(km->getConstantID(c, ki) + 2);
-  }
-}
-
-void KBlock::handleKInstruction(
-    std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
-    llvm::Instruction *inst, KModule *km, KInstruction *ki) {
-  ki->parent = this;
-  ki->inst = inst;
-  ki->dest = instructionToRegisterMap[inst];
-  if (isa<CallInst>(inst) || isa<InvokeInst>(inst)) {
-    const CallBase &cs = cast<CallBase>(*inst);
-    Value *val = cs.getCalledOperand();
-    unsigned numArgs = cs.arg_size();
-    ki->operands = new int[numArgs + 1];
-    ki->operands[0] = getOperandNum(val, instructionToRegisterMap, km, ki);
-    for (unsigned j = 0; j < numArgs; j++) {
-      Value *v = cs.getArgOperand(j);
-      ki->operands[j + 1] = getOperandNum(v, instructionToRegisterMap, km, ki);
-    }
-  } else {
-    unsigned numOperands = inst->getNumOperands();
-    ki->operands = new int[numOperands];
-    for (unsigned j = 0; j < numOperands; j++) {
-      Value *v = inst->getOperand(j);
-      ki->operands[j] = getOperandNum(v, instructionToRegisterMap, km, ki);
-    }
-  }
-}
-
-KFunction::KFunction(llvm::Function *_function, KModule *_km)
-    : KCallable(CK_Function), parent(_km), function(_function),
-      numArgs(function->arg_size()), numInstructions(0), numBlocks(0),
-      entryKBlock(nullptr), trackCoverage(true) {
+KFunction::KFunction(llvm::Function *_function, KModule *_km,
+                     unsigned &globalIndexInc)
+    : KCallable(CK_Function), globalIndex(globalIndexInc++), parent(_km),
+      function(_function), entryKBlock(nullptr), numInstructions(0) {
   for (auto &BasicBlock : *function) {
     numInstructions += BasicBlock.size();
-    numBlocks++;
+    //    numBlocks++;
   }
   instructions = new KInstruction *[numInstructions];
+  // TODO may be deleted [numArgs + instructionId]
   std::unordered_map<Instruction *, unsigned> instructionToRegisterMap;
   // Assign unique instruction IDs to each basic block
   unsigned n = 0;
   // The first arg_size() registers are reserved for formals.
-  unsigned rnum = numArgs;
-  for (llvm::Function::iterator bbit = function->begin(),
-                                bbie = function->end();
-       bbit != bbie; ++bbit) {
-    for (llvm::BasicBlock::iterator it = bbit->begin(), ie = bbit->end();
-         it != ie; ++it)
-      instructionToRegisterMap[&*it] = rnum++;
+  unsigned rnum = getNumArgs();
+  for (auto &bbit : *function) {
+    for (auto &it : bbit) {
+      instructionToRegisterMap[&it] = rnum++;
+    }
   }
-  numRegisters = rnum;
 
-  unsigned blockID = 0;
+  //  unsigned blockID = 0;
   for (llvm::Function::iterator bbit = function->begin(),
                                 bbie = function->end();
        bbit != bbie; ++bbit) {
@@ -594,32 +609,44 @@ KFunction::KFunction(llvm::Function *_function, KModule *_km)
       if (f) {
         calledFunctions.insert(f);
       }
-      KCallBlock *ckb = new KCallBlock(
-          this, &*bbit, parent, instructionToRegisterMap,
-          registerToInstructionMap, calledFunctions, &instructions[n]);
+      auto *ckb =
+          new KCallBlock(this, &*bbit, parent, instructionToRegisterMap,
+                         calledFunctions, &instructions[n], globalIndexInc);
       kCallBlocks.push_back(ckb);
       kb = ckb;
     } else if (SplitReturns && isa<ReturnInst>(lit)) {
       kb = new KReturnBlock(this, &*bbit, parent, instructionToRegisterMap,
-                            registerToInstructionMap, &instructions[n]);
+                            &instructions[n], globalIndexInc);
       returnKBlocks.push_back(kb);
-    } else
+    } else {
       kb = new KBlock(this, &*bbit, parent, instructionToRegisterMap,
-                      registerToInstructionMap, &instructions[n]);
+                      &instructions[n], globalIndexInc);
+    }
     for (unsigned i = 0; i < kb->numInstructions; i++, n++) {
       instructionMap[instructions[n]->inst] = instructions[n];
     }
-    kb->id = blockID++;
+    //    kb->id = blockID++;
     blockMap[&*bbit] = kb;
     blocks.push_back(std::unique_ptr<KBlock>(kb));
   }
 
-  if (numBlocks > 0) {
+  if (blocks.size() > 0) {
     assert(function->begin() != function->end());
     entryKBlock = blockMap[&*function->begin()];
   }
 }
 
+size_t KFunction::getLine() const {
+  auto locationInfo = getLocationInfo(function);
+  return locationInfo.line;
+}
+
+// TODO problem files with same name
+std::string KFunction::getSourceFilepath() const {
+  auto locationInfo = getLocationInfo(function);
+  return locationInfo.file;
+}
+
 KFunction::~KFunction() {
   for (unsigned i = 0; i < numInstructions; ++i)
     delete instructions[i];
@@ -628,47 +655,43 @@ KFunction::~KFunction() {
 
 KBlock::KBlock(
     KFunction *_kfunction, llvm::BasicBlock *block, KModule *km,
-    std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
-    std::unordered_map<unsigned, KInstruction *> &registerToInstructionMap,
-    KInstruction **instructionsKF)
-    : parent(_kfunction), basicBlock(block), numInstructions(0),
-      trackCoverage(true) {
+    const std::unordered_map<Instruction *, unsigned>
+        &instructionToRegisterMap, // TODO remove instructionToRegisterMap
+    KInstruction **instructionsKF, unsigned &globalIndexInc)
+    : parent(_kfunction), basicBlock(block), numInstructions(0) {
   numInstructions += block->size();
   instructions = instructionsKF;
 
-  unsigned i = 0;
-  for (llvm::BasicBlock::iterator it = block->begin(), ie = block->end();
-       it != ie; ++it) {
+//  size_t i = 0;
+  for (auto &it : *block) {
     KInstruction *ki;
 
-    switch (it->getOpcode()) {
+    switch (it.getOpcode()) {
     case Instruction::GetElementPtr:
     case Instruction::InsertValue:
     case Instruction::ExtractValue:
-      ki = new KGEPInstruction();
+      ki = new KGEPInstruction(instructionToRegisterMap, &it, km, this,
+                               globalIndexInc);
       break;
     default:
-      ki = new KInstruction();
+      ki = new KInstruction(instructionToRegisterMap, &it, km, this,
+                            globalIndexInc);
       break;
     }
-
-    Instruction *inst = &*it;
-    handleKInstruction(instructionToRegisterMap, inst, km, ki);
-    ki->index = i;
-    instructions[i++] = ki;
-    registerToInstructionMap[instructionToRegisterMap[&*it]] = ki;
+    instructions[ki->getIndex()] = ki;
+    //    registerToInstructionMap[ki->getDest()] = ki;
   }
 }
 
 KCallBlock::KCallBlock(
     KFunction *_kfunction, llvm::BasicBlock *block, KModule *km,
-    std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
-    std::unordered_map<unsigned, KInstruction *> &registerToInstructionMap,
-    std::set<llvm::Function *> _calledFunctions, KInstruction **instructionsKF)
+    const std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
+    std::set<llvm::Function *> _calledFunctions, KInstruction **instructionsKF,
+    unsigned &globalIndexInc)
     : KBlock::KBlock(_kfunction, block, km, instructionToRegisterMap,
-                     registerToInstructionMap, instructionsKF),
+                     instructionsKF, globalIndexInc),
       kcallInstruction(this->instructions[0]),
-      calledFunctions(_calledFunctions) {}
+      calledFunctions(std::move(_calledFunctions)) {}
 
 bool KCallBlock::intrinsic() const {
   if (calledFunctions.size() != 1) {
@@ -695,11 +718,10 @@ KFunction *KCallBlock::getKFunction() const {
 
 KReturnBlock::KReturnBlock(
     KFunction *_kfunction, llvm::BasicBlock *block, KModule *km,
-    std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
-    std::unordered_map<unsigned, KInstruction *> &registerToInstructionMap,
-    KInstruction **instructionsKF)
+    const std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
+    KInstruction **instructionsKF, unsigned &globalIndexInc)
     : KBlock::KBlock(_kfunction, block, km, instructionToRegisterMap,
-                     registerToInstructionMap, instructionsKF) {}
+                     instructionsKF, globalIndexInc) {}
 
 std::string KBlock::getLabel() const {
   std::string _label;
@@ -712,3 +734,13 @@ std::string KBlock::getLabel() const {
 std::string KBlock::toString() const {
   return getLabel() + " in function " + parent->function->getName().str();
 }
+
+uintptr_t KBlock::getId() const { return instructions - parent->instructions; }
+
+KInstruction *KFunction::getInstructionByRegister(size_t reg) const {
+  return instructions[reg - function->arg_size()];
+}
+size_t KFunction::getNumArgs() const { return function->arg_size(); }
+size_t KFunction::getNumRegisters() const {
+  return function->arg_size() + numInstructions;
+}
diff --git a/lib/Module/SarifReport.cpp b/lib/Module/SarifReport.cpp
index 286ca322579..f06834af18b 100644
--- a/lib/Module/SarifReport.cpp
+++ b/lib/Module/SarifReport.cpp
@@ -121,8 +121,9 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName,
   }
 }
 
-void
-tryConvertMessage(const std::string &toolName, const optional<Message> &errorMessage, ref<Location> &loc) {
+void tryConvertMessage(const std::string &toolName,
+                       const optional<Message> &errorMessage,
+                       ref<Location> &loc) {
   if (toolName != "Cooddy" || !errorMessage.has_value())
     return;
   std::string start = "Dereferencing of \"";
@@ -341,13 +342,14 @@ bool Location::isInside(const std::string &name) const {
                                      : (m == -1 && isOSSeparator(filename[n])));
 }
 
-void Location::isInside(InstrWithPrecision &kp, const Instructions &origInsts) const {
+void Location::isInside(InstrWithPrecision &kp,
+                        const Instructions &origInsts) const {
   auto ki = kp.ptr;
-  auto inst = ki->info;
-  if (!isa<DbgInfoIntrinsic>(ki->inst) && startLine <= inst->line && inst->line <= endLine) {
+  if (!isa<DbgInfoIntrinsic>(ki->inst) && startLine <= ki->getLine() &&
+      ki->getLine() <= endLine) {
     auto opCode = ki->inst->getOpcode();
-    if (*startColumn <= inst->column && inst->column <= *endColumn &&
-        origInsts.at(inst->line).at(inst->column).count(opCode) != 0)
+    if (*startColumn <= ki->getColumn() && ki->getColumn() <= *endColumn &&
+        origInsts.at(ki->getLine()).at(ki->getColumn()).count(opCode) != 0)
       kp.precision = Precision::ColumnLevel;
     else
       kp.precision = Precision::LineLevel;
@@ -357,9 +359,9 @@ void Location::isInside(InstrWithPrecision &kp, const Instructions &origInsts) c
 
 void Location::isInside(BlockWithPrecision &bp, const Instructions &origInsts) {
   if (!startColumn.has_value()) {
-    auto first = bp.ptr->getFirstInstruction()->info;
-    auto last = bp.ptr->getLastInstruction()->info;
-    if (first->line <= endLine && startLine <= last->line)
+    auto firstKi = bp.ptr->getFirstInstruction();
+    auto lastKi = bp.ptr->getLastInstruction();
+    if (firstKi->getLine() <= endLine && startLine <= lastKi->getLine())
       bp.precision = Precision::LineLevel;
     else
       bp.setNotFound();
@@ -377,7 +379,8 @@ void Location::isInside(BlockWithPrecision &bp, const Instructions &origInsts) {
   }
 }
 
-void CoodyNPELocation::isInside(BlockWithPrecision &bp, const Instructions &origInsts) {
+void CoodyNPELocation::isInside(BlockWithPrecision &bp,
+                                const Instructions &origInsts) {
   // if (x + y > z && aaa->bbb->ccc->ddd)
   // ^^^^^^^^^^^^^^^^^ first, skip all this
   // second skip this ^^^^^^^^ (where Cooddy event points)
@@ -391,11 +394,11 @@ void CoodyNPELocation::isInside(BlockWithPrecision &bp, const Instructions &orig
     ki = block->instructions[start];
     InstrWithPrecision kp(ki);
     Location::isInside(kp, origInsts);
-    if (kp.precision >= precision) {  // first: go until Cooddy event
+    if (kp.precision >= precision) { // first: go until Cooddy event
       precision = kp.precision;
-      if (!inside)                    // first: reached Cooddy event
+      if (!inside)                   // first: reached Cooddy event
         inside = true;
-    } else if (inside)                // second: skip until left Coody event
+    } else if (inside)               // second: skip until left Coody event
       break;
   }
   if (!inside) { // no Cooddy event in this Block
@@ -409,8 +412,8 @@ void CoodyNPELocation::isInside(BlockWithPrecision &bp, const Instructions &orig
   // finally: Load instruction
   if (ki->inst->getOpcode() == Instruction::Load) {
     // we got precise instruction, so redefine the location
-    startLine = (endLine = ki->info->line);
-    startColumn = (endColumn = ki->info->column);
+    startLine = (endLine = ki->getLine());
+    startColumn = (endColumn = ki->getColumn());
     bp.precision = Precision::ColumnLevel;
     return;
   }
diff --git a/lib/Module/Target.cpp b/lib/Module/Target.cpp
index 633d27f2a66..e04d36a9d09 100644
--- a/lib/Module/Target.cpp
+++ b/lib/Module/Target.cpp
@@ -93,11 +93,11 @@ ref<Target> CoverBranchTarget::create(KBlock *_block, unsigned _branchCase) {
 
 bool ReproduceErrorTarget::isTheSameAsIn(const KInstruction *instr) const {
   const auto &errLoc = loc;
-  return instr->info->line >= errLoc.startLine &&
-         instr->info->line <= errLoc.endLine &&
+  return instr->getLine() >= errLoc.startLine &&
+         instr->getLine() <= errLoc.endLine &&
          (!LocationAccuracy || !errLoc.startColumn.has_value() ||
-          (instr->info->column >= *errLoc.startColumn &&
-           instr->info->column <= *errLoc.endColumn));
+          (instr->getColumn() >= *errLoc.startColumn &&
+           instr->getColumn() <= *errLoc.endColumn));
 }
 
 int Target::compare(const Target &b) const { return internalCompare(b); }
@@ -117,8 +117,8 @@ int ReachBlockTarget::internalCompare(const Target &b) const {
   if (block->parent->id != other.block->parent->id) {
     return block->parent->id < other.block->parent->id ? -1 : 1;
   }
-  if (block->id != other.block->id) {
-    return block->id < other.block->id ? -1 : 1;
+  if (block->getId() != other.block->getId()) {
+    return block->getId() < other.block->getId() ? -1 : 1;
   }
 
   if (atEnd != other.atEnd) {
@@ -137,8 +137,8 @@ int CoverBranchTarget::internalCompare(const Target &b) const {
   if (block->parent->id != other.block->parent->id) {
     return block->parent->id < other.block->parent->id ? -1 : 1;
   }
-  if (block->id != other.block->id) {
-    return block->id < other.block->id ? -1 : 1;
+  if (block->getId() != other.block->getId()) {
+    return block->getId() < other.block->getId() ? -1 : 1;
   }
 
   if (branchCase != other.branchCase) {
@@ -161,8 +161,8 @@ int ReproduceErrorTarget::internalCompare(const Target &b) const {
   if (block->parent->id != other.block->parent->id) {
     return block->parent->id < other.block->parent->id ? -1 : 1;
   }
-  if (block->id != other.block->id) {
-    return block->id < other.block->id ? -1 : 1;
+  if (block->getId() != other.block->getId()) {
+    return block->getId() < other.block->getId() ? -1 : 1;
   }
 
   if (errors.size() != other.errors.size()) {
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index bed3fc6db67..abb9447d1f6 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -48,6 +48,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/Path.h"
 #include "llvm/Support/raw_ostream.h"
 
+#include "klee/Module/InstructionInfoTable.h"
 #include "llvm/Support/Signals.h"
 #include "llvm/Support/TargetSelect.h"
 DISABLE_WARNING_POP
@@ -64,6 +65,7 @@ DISABLE_WARNING_POP
 #include <fstream>
 #include <iomanip>
 #include <iterator>
+#include <llvm/IR/InstIterator.h>
 #include <sstream>
 
 using json = nlohmann::json;
@@ -703,13 +705,13 @@ void KleeHandler::processTestCase(const ExecutionState &state,
   }
 
   if (WriteCov) {
-    std::map<const std::string *, std::set<unsigned>> cov;
+    std::map<std::string, std::set<size_t>> cov;
     m_interpreter->getCoveredLines(state, cov);
     auto f = openTestFile("cov", id);
     if (f) {
       for (const auto &entry : cov) {
         for (const auto &line : entry.second) {
-          *f << *entry.first << ':' << line << '\n';
+          *f << entry.first << ':' << line << '\n';
         }
       }
     }
@@ -1232,7 +1234,7 @@ createLibCWrapper(std::vector<std::unique_ptr<llvm::Module>> &userModules,
   args.push_back(llvm::ConstantExpr::getBitCast(
       cast<llvm::Constant>(inModuleReference.getCallee()),
       ft->getParamType(0)));
-  args.push_back(&*(stub->arg_begin())); // argc
+  args.push_back(&*(stub->arg_begin()));                       // argc
   auto arg_it = stub->arg_begin();
   args.push_back(&*(++arg_it));                                // argv
   args.push_back(Constant::getNullValue(ft->getParamType(3))); // app_init
@@ -1618,13 +1620,19 @@ int main(int argc, char **argv, char **envp) {
   }
 
   llvm::Module *mainModule = loadedUserModules.front().get();
-  std::unique_ptr<InstructionInfoTable> origInfos;
-  std::unique_ptr<llvm::raw_fd_ostream> assemblyFS;
+  KModule::FInstructions origInstructions;
 
   if (UseGuidedSearch == Interpreter::GuidanceKind::ErrorGuidance) {
+    for (const auto &Func : *mainModule) {
+      for (const auto &instr : llvm::instructions(Func)) {
+        auto locationInfo = getLocationInfo(&instr);
+        origInstructions[locationInfo.file][locationInfo.line]
+                        [locationInfo.column]
+                            .insert(instr.getOpcode());
+      }
+    }
+
     std::vector<llvm::Type *> args;
-    origInfos = std::make_unique<InstructionInfoTable>(
-        *mainModule, std::move(assemblyFS), true);
     args.push_back(llvm::Type::getInt32Ty(ctx)); // argc
     args.push_back(llvm::PointerType::get(
         Type::getInt8PtrTy(ctx),
@@ -1643,15 +1651,16 @@ int main(int argc, char **argv, char **envp) {
     EntryPoint = stubEntryPoint;
   }
 
-  std::unordered_set<std::string> mainModuleFunctions;
+  std::set<llvm::StringRef> mainModuleFunctions;
   for (auto &Function : *mainModule) {
     if (!Function.isDeclaration()) {
-      mainModuleFunctions.insert(Function.getName().str());
+      mainModuleFunctions.insert(Function.getName());
     }
   }
-  std::unordered_set<std::string> mainModuleGlobals;
-  for (const auto &gv : mainModule->globals())
-    mainModuleGlobals.insert(gv.getName().str());
+  std::set<llvm::StringRef> mainModuleGlobals;
+  for (const auto &gv : mainModule->globals()) {
+    mainModuleGlobals.insert(gv.getName());
+  }
 
   const std::string &module_triple = mainModule->getTargetTriple();
   std::string host_triple = llvm::sys::getDefaultTargetTriple();
@@ -1926,7 +1935,7 @@ int main(int argc, char **argv, char **envp) {
 
   auto finalModule = interpreter->setModule(
       loadedUserModules, loadedLibsModules, Opts, mainModuleFunctions,
-      mainModuleGlobals, std::move(origInfos), ignoredExternals, redefinitions);
+      mainModuleGlobals, std::move(origInstructions), ignoredExternals, redefinitions);
   Function *mainFn = finalModule->getFunction(EntryPoint);
   if (!mainFn) {
     klee_error("Entry function '%s' not found in module.", EntryPoint.c_str());