ClearBlue
SymbolicExprGraphSolver.h
1 /*
2  * Developed by Qingkai Shi
3  * Copy Right by Prism Research Group, HKUST and State Key Lab for Novel
4  * Software Tech., Nanjing University.
5  */
6 
7 #ifndef IR_SEG_SYMBOLICEXPRGRAPHSOLVER_H
8 #define IR_SEG_SYMBOLICEXPRGRAPHSOLVER_H
9 
10 #include <llvm/IR/BasicBlock.h>
11 #include <llvm/IR/Dominators.h>
12 
13 #include <string>
14 #include <unordered_map>
15 
16 #include "Analysis/Bitcode/TSDataLayout.h"
17 #include "Analysis/Graph/DomTreePass.h"
18 #include "IR/SEG/SEGArgumentNode.h"
19 #include "IR/SEG/SEGBinaryWithIntConstNode.h"
20 #include "IR/SEG/SEGCastNode.h"
21 #include "IR/SEG/SEGLoadMemNode.h"
22 #include "IR/SEG/SEGPhiNode.h"
23 #include "IR/SEG/SEGRegionNode.h"
24 #include "IR/SEG/SEGReturnNode.h"
25 #include "IR/SEG/SEGStoreMemNode.h"
26 #include "SMT/SMTFactory.h"
27 
28 #include "Utils/ADT/PushPopCache.h"
29 
30 using namespace llvm;
31 
32 class MessageQueue;
33 class ExternalMemorySpec;
34 class ExternalIOSpec;
35 
45 class SymbolicExprGraphSolver : public SMTSolver {
46 protected:
48  std::unordered_map<const SEGNodeBase *, SMTExpr> NodeExprMap;
49 
51  std::unordered_map<std::string, const SEGNodeBase *> NodeSymbolNameMap;
52 
53  TSDataLayout &DL;
54 
55  ExternalMemorySpec *MemSpec = nullptr;
56  ExternalIOSpec *IOSpec = nullptr;
57 
58 public:
59  SymbolicExprGraphSolver(SMTFactory &Fcty, TSDataLayout &D,
60  ExternalMemorySpec *MemSepc, ExternalIOSpec *IOSpec);
61  virtual ~SymbolicExprGraphSolver();
62 
64  SMTExprVec getCtrlDeps(const SEGNodeBase *N, void *Args = nullptr);
65 
67  virtual SMTExprVec getCtrlDeps(BasicBlock *B, const SymbolicExprGraph *G,
68  void *Args = nullptr);
69 
75  virtual std::pair<SMTExprVec, SMTExprVec>
76  getCtrlDepsPair(BasicBlock *B, const SymbolicExprGraph *G,
77  void *Args = nullptr) {
78  return __getCtrlDeps(B, G);
79  }
80 
82  virtual SMTExprVec getDataDeps(const SEGNodeBase *N, void *Args = nullptr);
83 
84  // Return gated function for a child of a phiNode
85  // This is the most accurate for a phi incoming node, since it is identified
86  // with incoming BB and the value.
87  virtual SMTExprVec getPhiGated(const SEGPhiNode *PhiNode,
88  const SEGPhiNode::IncomeNode InNode,
89  void *Args = nullptr);
90 
91  // This function first try to find the inNode then call the inNode version.
92  SMTExprVec getPhiGated(const SEGPhiNode *PhiNode, const SEGNodeBase *Value,
93  BasicBlock *BB, void *Args = nullptr);
94 
95  // This is a less accurate version since one value could come from several
96  // different BBs. We collect their ctrl dep + immediate cond and then OR all
97  // of them.
98  SMTExprVec getPhiGated(const SEGPhiNode *PhiNode, const SEGNodeBase *Value,
99  void *Args = nullptr);
100 
106  virtual SMTExprVec getDeps(const SEGNodeBase *N, const SEGNodeBase *M);
107 
110  virtual std::pair<SMTExprVec, SMTExprVec> getDepsPair(const SEGNodeBase *N,
111  const SEGNodeBase *M);
112 
113 private:
116  std::pair<SMTExprVec, SMTExprVec>
117  __getCtrlDeps(BasicBlock *B, const SymbolicExprGraph *G, size_t Depth = 0);
118 
119  std::pair<SMTExprVec, SMTExprVec>
120  __getPhiGated(const SEGPhiNode *PhiNd, const SEGPhiNode::IncomeNode In,
121  size_t Depth = 0);
122 
124  SMTExprVec __getDataDeps(const SEGNodeBase *N, size_t Depth = 0);
125 
126 public:
127  virtual void push();
128 
129  virtual void pop(unsigned N = 1);
130 
131  virtual void reset();
132 
133  virtual SMTResultType check();
134 
135 protected:
136  PushPopCache<const SEGNodeBase *> ConstraintCache;
137  PushPopCache<BasicBlock *> BBCache;
138 
139 private:
140  PushPopCache<const SEGArgumentNode *> FunctionArgumentCache;
141  PushPopCache<const SEGCallSiteOutputNode *> CallSiteOutputCache;
142 
143  std::unordered_map<BasicBlock *, SMTExprVec> CtrlCacheMap;
144  std::unordered_map<const SEGOpcodeNode *, SMTExpr> OpcodeConstraintsCacheMap;
145 
146 public:
147  const std::unordered_set<const SEGArgumentNode *> &
148  getUsedFunctionArguments() {
149  return FunctionArgumentCache.getCacheSet();
150  }
151 
152  // see PushPopVector::getCacheVector(bool)
153  std::pair<std::vector<const SEGCallSiteOutputNode *>::iterator,
154  std::vector<const SEGCallSiteOutputNode *>::iterator>
155  getUsedCallSiteOutputs(bool Restart = false) {
156  return CallSiteOutputCache.getCacheVector(Restart);
157  }
158 
159 public:
161  const SEGNodeBase *getNodeFromSymbol(std::string Symbol) {
162  auto It = NodeSymbolNameMap.find(Symbol);
163  if (It == NodeSymbolNameMap.end()) {
164  return nullptr;
165  }
166  return It->second;
167  }
168 
169  virtual SMTExpr getOrInsertExpr(const SEGNodeBase *N);
170 
184  SMTExpr encodeOpcodeNode(const SEGOpcodeNode *N);
185 
186  virtual SMTExpr encodeBinaryOpcodeNode(const SEGOpcodeNode *N);
187  virtual SMTExpr encodeCompareOpcodeNode(const SEGOpcodeNode *N);
188  virtual SMTExpr encodeCastOpcodeNode(const SEGOpcodeNode *N);
189  virtual SMTExpr encodeGEPOpcodeNode(const SEGOpcodeNode *N);
190  virtual SMTExpr encodeExtractElementOpcodeNode(const SEGOpcodeNode *N);
191  virtual SMTExpr encodeInsertElementOpcodeNode(const SEGOpcodeNode *N);
192  virtual SMTExpr encodeSelectOpcodeNode(const SEGOpcodeNode *N);
193  virtual SMTExpr encodeConcatOpcodeNode(const SEGOpcodeNode *N);
194 };
195 
196 // Using the domination relationship between basic blocks
197 // to refine the constraints.
199 private:
200  const DomTree *DT;
201 
202  std::unordered_map<BasicBlock *, std::pair<SMTExprVec, BasicBlock *>>
203  CtrlCacheMap;
204 
205 public:
206  DTSymbolicExprGraphSolver(SMTFactory &Fcty, TSDataLayout &D,
207  ExternalMemorySpec *MemSpec, ExternalIOSpec *IOSpec,
208  const DomTree *T)
209  : SymbolicExprGraphSolver(Fcty, D, MemSpec, IOSpec), DT(T) {}
210 
211 public:
214  virtual SMTExprVec getCtrlDeps(BasicBlock *B, const SymbolicExprGraph *G,
215  void *Args = nullptr);
216 
217  virtual std::pair<SMTExprVec, SMTExprVec>
218  getCtrlDepsPair(BasicBlock *B, const SymbolicExprGraph *G,
219  void *Args = nullptr) {
220  BasicBlock *PrevB = (BasicBlock *)Args;
221  return __getCtrlDepsWrapper(B, G, PrevB);
222  }
223 
226  virtual SMTExprVec getDataDeps(const SEGNodeBase *N, void *Args = nullptr);
227 
232  virtual SMTExprVec getPhiGated(const SEGPhiNode *PhiNode,
233  const SEGPhiNode::IncomeNode InNode,
234  void *Args = nullptr);
235 
236  virtual void reset();
237 
242  virtual SMTExprVec getDeps(const SEGNodeBase *N, const SEGNodeBase *M);
243 
244 private:
246  std::pair<SMTExprVec, SMTExprVec>
247  __getCtrlDepsWrapper(BasicBlock *B, const SymbolicExprGraph *G,
248  BasicBlock *PrevB);
249 
253  std::pair<SMTExprVec, SMTExprVec>
254  __getCtrlDeps(BasicBlock *B, const SymbolicExprGraph *G, BasicBlock *PrevB);
255 
256  std::pair<SMTExprVec, SMTExprVec>
257  __getPhiGated(const SEGPhiNode *PhiNd, const SEGPhiNode::IncomeNode In,
258  BasicBlock *PrevB);
259 
263  SMTExprVec __getDataDeps(const SEGNodeBase *N, BasicBlock *PrevB);
264 };
265 
266 #endif
SEGPhiNode::IncomeNode
Definition: SEGPhiNode.h:33
SymbolicExprGraphSolver::NodeSymbolNameMap
std::unordered_map< std::string, const SEGNodeBase * > NodeSymbolNameMap
map the symbol name used by Z3 in context ctx to the SEG node
Definition: SymbolicExprGraphSolver.h:51
SymbolicExprGraph
Definition: SymbolicExprGraph.h:715
SymbolicExprGraphSolver
Definition: SymbolicExprGraphSolver.h:45
SymbolicExprGraphSolver::NodeExprMap
std::unordered_map< const SEGNodeBase *, SMTExpr > NodeExprMap
each node in seg is a z3 variable
Definition: SymbolicExprGraphSolver.h:48
SymbolicExprGraphSolver::getNodeFromSymbol
const SEGNodeBase * getNodeFromSymbol(std::string Symbol)
return the SEG node for the given symbol
Definition: SymbolicExprGraphSolver.h:161
DTSymbolicExprGraphSolver
Definition: SymbolicExprGraphSolver.h:198
SymbolicExprGraphSolver::getCtrlDepsPair
virtual std::pair< SMTExprVec, SMTExprVec > getCtrlDepsPair(BasicBlock *B, const SymbolicExprGraph *G, void *Args=nullptr)
Definition: SymbolicExprGraphSolver.h:76
SEGPhiNode
Definition: SEGPhiNode.h:28
SEGOpcodeNode
Definition: SymbolicExprGraph.h:524
DTSymbolicExprGraphSolver::getCtrlDepsPair
virtual std::pair< SMTExprVec, SMTExprVec > getCtrlDepsPair(BasicBlock *B, const SymbolicExprGraph *G, void *Args=nullptr)
Definition: SymbolicExprGraphSolver.h:218
SEGNodeBase
The node base of symbolic expression graph.
Definition: SymbolicExprGraph.h:248