InstructionInfoTable.cpp
Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010 #include "klee/Internal/Module/InstructionInfoTable.h"
00011
00012 #include "llvm/Function.h"
00013 #include "llvm/Instructions.h"
00014 #include "llvm/IntrinsicInst.h"
00015 #include "llvm/Linker.h"
00016 #include "llvm/Module.h"
00017 #include "llvm/Assembly/AsmAnnotationWriter.h"
00018 #include "llvm/Support/CFG.h"
00019 #include "llvm/Support/InstIterator.h"
00020 #include "llvm/Support/raw_ostream.h"
00021 #include "llvm/Analysis/ValueTracking.h"
00022
00023 #include <map>
00024 #include <iostream>
00025 #include <fstream>
00026 #include <sstream>
00027 #include <string>
00028
00029 using namespace llvm;
00030 using namespace klee;
00031
00032 class InstructionToLineAnnotator : public llvm::AssemblyAnnotationWriter {
00033 public:
00034 void emitInstructionAnnot(const Instruction *i, llvm::raw_ostream &os) {
00035 os << "%%%" << (uintptr_t) i;
00036 }
00037 };
00038
00039 static void buildInstructionToLineMap(Module *m,
00040 std::map<const Instruction*, unsigned> &out) {
00041 InstructionToLineAnnotator a;
00042 std::ostringstream buffer;
00043 m->print(buffer, &a);
00044 std::string str = buffer.str();
00045 const char *s;
00046
00047 unsigned line = 1;
00048 for (s=str.c_str(); *s; s++) {
00049 if (*s=='\n') {
00050 line++;
00051 if (s[1]=='%' && s[2]=='%' && s[3]=='%') {
00052 s += 4;
00053 char *end;
00054 unsigned long long value = strtoull(s, &end, 10);
00055 if (end!=s) {
00056 out.insert(std::make_pair((const Instruction*) value, line));
00057 }
00058 s = end;
00059 }
00060 }
00061 }
00062 }
00063
00064 static std::string getDSPIPath(DbgStopPointInst *dspi) {
00065 std::string dir, file;
00066 bool res = GetConstantStringInfo(dspi->getDirectory(), dir);
00067 assert(res && "GetConstantStringInfo failed");
00068 res = GetConstantStringInfo(dspi->getFileName(), file);
00069 assert(res && "GetConstantStringInfo failed");
00070 if (dir.empty()) {
00071 return file;
00072 } else if (*dir.rbegin() == '/') {
00073 return dir + file;
00074 } else {
00075 return dir + "/" + file;
00076 }
00077 }
00078
00079 InstructionInfoTable::InstructionInfoTable(Module *m)
00080 : dummyString(""), dummyInfo(0, dummyString, 0, 0) {
00081 unsigned id = 0;
00082 std::map<const Instruction*, unsigned> lineTable;
00083 buildInstructionToLineMap(m, lineTable);
00084
00085 for (Module::iterator fnIt = m->begin(), fn_ie = m->end();
00086 fnIt != fn_ie; ++fnIt) {
00087 const std::string *initialFile = &dummyString;
00088 unsigned initialLine = 0;
00089
00090
00091
00092
00093 for (inst_iterator it = inst_begin(fnIt), ie = inst_end(fnIt);
00094 it != ie; ++it) {
00095 if (DbgStopPointInst *dspi = dyn_cast<DbgStopPointInst>(&*it)) {
00096 initialFile = internString(getDSPIPath(dspi));
00097 initialLine = dspi->getLine();
00098 break;
00099 }
00100 }
00101
00102 typedef std::map<BasicBlock*, std::pair<const std::string*,unsigned> >
00103 sourceinfo_ty;
00104 sourceinfo_ty sourceInfo;
00105 for (llvm::Function::iterator bbIt = fnIt->begin(), bbie = fnIt->end();
00106 bbIt != bbie; ++bbIt) {
00107 std::pair<sourceinfo_ty::iterator, bool>
00108 res = sourceInfo.insert(std::make_pair(bbIt,
00109 std::make_pair(initialFile,
00110 initialLine)));
00111 if (!res.second)
00112 continue;
00113
00114 std::vector<BasicBlock*> worklist;
00115 worklist.push_back(bbIt);
00116
00117 do {
00118 BasicBlock *bb = worklist.back();
00119 worklist.pop_back();
00120
00121 sourceinfo_ty::iterator si = sourceInfo.find(bb);
00122 assert(si != sourceInfo.end());
00123 const std::string *file = si->second.first;
00124 unsigned line = si->second.second;
00125
00126 for (BasicBlock::iterator it = bb->begin(), ie = bb->end();
00127 it != ie; ++it) {
00128 Instruction *instr = it;
00129 unsigned assemblyLine = 0;
00130 std::map<const Instruction*, unsigned>::const_iterator ltit =
00131 lineTable.find(instr);
00132 if (ltit!=lineTable.end())
00133 assemblyLine = ltit->second;
00134 if (DbgStopPointInst *dspi = dyn_cast<DbgStopPointInst>(instr)) {
00135 file = internString(getDSPIPath(dspi));
00136 line = dspi->getLine();
00137 }
00138 infos.insert(std::make_pair(instr,
00139 InstructionInfo(id++,
00140 *file,
00141 line,
00142 assemblyLine)));
00143 }
00144
00145 for (succ_iterator it = succ_begin(bb), ie = succ_end(bb);
00146 it != ie; ++it) {
00147 if (sourceInfo.insert(std::make_pair(*it,
00148 std::make_pair(file, line))).second)
00149 worklist.push_back(*it);
00150 }
00151 } while (!worklist.empty());
00152 }
00153 }
00154 }
00155
00156 InstructionInfoTable::~InstructionInfoTable() {
00157 for (std::set<const std::string *, ltstr>::iterator
00158 it = internedStrings.begin(), ie = internedStrings.end();
00159 it != ie; ++it)
00160 delete *it;
00161 }
00162
00163 const std::string *InstructionInfoTable::internString(std::string s) {
00164 std::set<const std::string *, ltstr>::iterator it = internedStrings.find(&s);
00165 if (it==internedStrings.end()) {
00166 std::string *interned = new std::string(s);
00167 internedStrings.insert(interned);
00168 return interned;
00169 } else {
00170 return *it;
00171 }
00172 }
00173
00174 unsigned InstructionInfoTable::getMaxID() const {
00175 return infos.size();
00176 }
00177
00178 const InstructionInfo &
00179 InstructionInfoTable::getInfo(const Instruction *inst) const {
00180 std::map<const llvm::Instruction*, InstructionInfo>::const_iterator it =
00181 infos.find(inst);
00182 if (it==infos.end()) {
00183 return dummyInfo;
00184 } else {
00185 return it->second;
00186 }
00187 }
00188
00189 const InstructionInfo &
00190 InstructionInfoTable::getFunctionInfo(const Function *f) const {
00191 if (f->isDeclaration()) {
00192 return dummyInfo;
00193 } else {
00194 return getInfo(f->begin()->begin());
00195 }
00196 }