SymbolicExprGraphSolver.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_SYMBOLICEXPRGRAPHSOLVER_H
#define IR_SEG_SYMBOLICEXPRGRAPHSOLVER_H
 
#include <llvm/IR/BasicBlock.h>
#include <llvm/IR/Dominators.h>
 
#include <string>
#include <unordered_map>
 
#include "Analysis/Bitcode/TSDataLayout.h"
#include "Analysis/Graph/DomTreePass.h"
 
#include "IR/SEG/SEGArgumentNode.h"
#include "IR/SEG/SEGLoadMemNode.h"
#include "IR/SEG/SEGPhiNode.h"
#include "IR/SEG/SEGRegionNode.h"
#include "IR/SEG/SEGReturnNode.h"
#include "IR/SEG/SEGStoreMemNode.h"
 
#include "IR/SEG/SEGBinaryWithIntConstNode.h"
#include "IR/SEG/SEGCastNode.h"
 
#include "SMT/SMTFactory.h"
 
#include "Utils/ADT/PushPopCache.h"
 
using namespace llvm;
 
class MessageQueue;
class ExternalMemorySpec;
class ExternalIOSpec;
 
class SymbolicExprGraphSolver : public SMTSolver {
protected:
  std::unordered_map<const SEGNodeBase *, SMTExpr> NodeExprMap;
 
  std::unordered_map<std::string, const SEGNodeBase *> NodeSymbolNameMap;
 
  TSDataLayout &DL;
 
  ExternalMemorySpec *MemSpec = nullptr;
  ExternalIOSpec *IOSpec = nullptr;
 
public:
  SymbolicExprGraphSolver(SMTFactory &Fcty, TSDataLayout &D,
                          ExternalMemorySpec *MemSepc, ExternalIOSpec *IOSpec);
  virtual ~SymbolicExprGraphSolver();
 
  SMTExprVec getCtrlDeps(const SEGNodeBase *N, void *Args = nullptr);
 
  virtual SMTExprVec getCtrlDeps(BasicBlock *B, const SymbolicExprGraph *G,
                                 void *Args = nullptr);
 
  virtual std::pair<SMTExprVec, SMTExprVec>
  getCtrlDepsPair(BasicBlock *B, const SymbolicExprGraph *G,
                  void *Args = nullptr) {
    return __getCtrlDeps(B, G);
  }
 
  virtual SMTExprVec getDataDeps(const SEGNodeBase *N, void *Args = nullptr);
 
  // Return gated function for a child of a phiNode
  // This is the most accurate for a phi incoming node, since it is identified
  // with incoming BB and the value.
  virtual SMTExprVec getPhiGated(const SEGPhiNode *PhiNode,
                                 const SEGPhiNode::IncomeNode InNode,
                                 void *Args = nullptr);
 
  // This function first try to find the inNode then call the inNode version.
  SMTExprVec getPhiGated(const SEGPhiNode *PhiNode, const SEGNodeBase *Value,
                         BasicBlock *BB, void *Args = nullptr);
 
  // This is a less accurate version since one value could come from several
  // different BBs. We collect their ctrl dep + immediate cond and then OR all
  // of them.
  SMTExprVec getPhiGated(const SEGPhiNode *PhiNode, const SEGNodeBase *Value,
                         void *Args = nullptr);
 
  virtual SMTExprVec getDeps(const SEGNodeBase *N, const SEGNodeBase *M);
 
  virtual std::pair<SMTExprVec, SMTExprVec> getDepsPair(const SEGNodeBase *N,
                                                        const SEGNodeBase *M);
 
private:
  std::pair<SMTExprVec, SMTExprVec>
  __getCtrlDeps(BasicBlock *B, const SymbolicExprGraph *G, size_t Depth = 0);
 
  std::pair<SMTExprVec, SMTExprVec>
  __getPhiGated(const SEGPhiNode *PhiNd, const SEGPhiNode::IncomeNode In);
 
  SMTExprVec __getDataDeps(const SEGNodeBase *N, size_t Depth = 0);
 
public:
  virtual void push();
 
  virtual void pop(unsigned N = 1);
 
  virtual void reset();
 
  virtual SMTResultType check();
 
protected:
  PushPopCache<const SEGNodeBase *> ConstraintCache;
  PushPopCache<BasicBlock *> BBCache;
 
private:
  PushPopCache<const SEGArgumentNode *> FunctionArgumentCache;
  PushPopCache<const SEGCallSiteOutputNode *> CallSiteOutputCache;
 
  std::unordered_map<BasicBlock *, SMTExprVec> CtrlCacheMap;
  std::unordered_map<const SEGOpcodeNode *, SMTExpr> OpcodeConstraintsCacheMap;
 
public:
  const std::unordered_set<const SEGArgumentNode *> &
  getUsedFunctionArguments() {
    return FunctionArgumentCache.getCacheSet();
  }
 
  // see PushPopVector::getCacheVector(bool)
  std::pair<std::vector<const SEGCallSiteOutputNode *>::iterator,
            std::vector<const SEGCallSiteOutputNode *>::iterator>
  getUsedCallSiteOutputs(bool Restart = false) {
    return CallSiteOutputCache.getCacheVector(Restart);
  }
 
public:
  const SEGNodeBase *getNodeFromSymbol(std::string Symbol) {
    auto It = NodeSymbolNameMap.find(Symbol);
    if (It == NodeSymbolNameMap.end()) {
      return nullptr;
    }
    return It->second;
  }
 
  SMTExpr getOrInsertExpr(const SEGNodeBase *N);
 
  SMTExpr encodeOpcodeNode(const SEGOpcodeNode *N);
 
  virtual SMTExpr encodeBinaryOpcodeNode(const SEGOpcodeNode *N);
  virtual SMTExpr encodeCompareOpcodeNode(const SEGOpcodeNode *N);
  virtual SMTExpr encodeCastOpcodeNode(const SEGOpcodeNode *N);
  virtual SMTExpr encodeGEPOpcodeNode(const SEGOpcodeNode *N);
  virtual SMTExpr encodeExtractElementOpcodeNode(const SEGOpcodeNode *N);
  virtual SMTExpr encodeInsertElementOpcodeNode(const SEGOpcodeNode *N);
  virtual SMTExpr encodeSelectOpcodeNode(const SEGOpcodeNode *N);
  virtual SMTExpr encodeConcatOpcodeNode(const SEGOpcodeNode *N);
};
 
// Using the domination relationship between basic blocks
// to refine the constraints.
class DTSymbolicExprGraphSolver : public SymbolicExprGraphSolver {
private:
  const DomTree *DT;
 
  std::unordered_map<BasicBlock *, std::pair<SMTExprVec, BasicBlock *>>
      CtrlCacheMap;
 
public:
  DTSymbolicExprGraphSolver(SMTFactory &Fcty, TSDataLayout &D,
                            ExternalMemorySpec *MemSpec, ExternalIOSpec *IOSpec,
                            const DomTree *T)
      : SymbolicExprGraphSolver(Fcty, D, MemSpec, IOSpec), DT(T) {}
 
public:
  virtual SMTExprVec getCtrlDeps(BasicBlock *B, const SymbolicExprGraph *G,
                                 void *Args = nullptr);
 
  virtual std::pair<SMTExprVec, SMTExprVec>
  getCtrlDepsPair(BasicBlock *B, const SymbolicExprGraph *G,
                  void *Args = nullptr) {
    BasicBlock *PrevB = (BasicBlock *)Args;
    return __getCtrlDepsWrapper(B, G, PrevB);
  }
 
  virtual SMTExprVec getDataDeps(const SEGNodeBase *N, void *Args = nullptr);
 
  virtual SMTExprVec getPhiGated(const SEGPhiNode *PhiNode,
                                 const SEGPhiNode::IncomeNode InNode,
                                 void *Args = nullptr);
 
  virtual void reset();
 
  virtual SMTExprVec getDeps(const SEGNodeBase *N, const SEGNodeBase *M);
 
private:
  std::pair<SMTExprVec, SMTExprVec>
  __getCtrlDepsWrapper(BasicBlock *B, const SymbolicExprGraph *G,
                       BasicBlock *PrevB);
 
  std::pair<SMTExprVec, SMTExprVec>
  __getCtrlDeps(BasicBlock *B, const SymbolicExprGraph *G, BasicBlock *PrevB);
 
  std::pair<SMTExprVec, SMTExprVec>
  __getPhiGated(const SEGPhiNode *PhiNd, const SEGPhiNode::IncomeNode In,
                BasicBlock *PrevB);
 
  SMTExprVec __getDataDeps(const SEGNodeBase *N, BasicBlock *PrevB);
};
 
#endif