SymbolicExprGraphModel.h

/*
 * Developed by Qingkai Shi
 * Copy Right by Prism Research Group, HKUST and State Key Lab for Novel
 * Software Tech., Nanjing University.
 */
 
#ifndef IR_SEG_SYMBOLICEXPRGRAPHMODEL_H
#define IR_SEG_SYMBOLICEXPRGRAPHMODEL_H
 
#include <cstdbool>
#include <iostream>
#include <llvm/IR/BasicBlock.h>
#include <map>
#include <string>
#include <unordered_map>
#include <utility>
 
#include "IR/SEG/SymbolicExprGraph.h"
#include "IR/SEG/SymbolicExprGraphSolver.h"
#include "SMT/SMTFactory.h"
#include "SMT/SMTModel.h"
 
using namespace llvm;
 
class SymbolicExprGraphModel {
private:
  typedef std::unordered_map<const SEGNodeBase *,
                             std::pair<std::string, std::string>>
      ModelMapTy;
  ModelMapTy SEGModel;
 
public:
  SymbolicExprGraphModel(SymbolicExprGraphSolver &Solver, SMTModel &SMTModel) {
    for (unsigned int i = 0; i < SMTModel.size(); i++) {
      // Trigger move ctor of pair to reduce string copy overhead
      std::pair<std::string, std::string> DebugInfo(
          SMTModel.getModelDbgInfo(i));
 
      if (DebugInfo.first != "") {
        // Here we capture only assignment to string symbols (i.e. Terminal
        // nodes)
        // TODO: Assignment for other types of symbols to be handled if required
        const SEGNodeBase *n = Solver.getNodeFromSymbol(DebugInfo.first);
        if (n != nullptr)
          SEGModel[n] = DebugInfo;
      }
    }
  }
 
  typedef ModelMapTy::const_iterator const_iterator;
 
  inline const_iterator begin() const { return SEGModel.begin(); }
 
  inline const_iterator end() const { return SEGModel.end(); }
};
 
#endif