7 #ifndef IR_SEG_SYMBOLICEXPRGRAPHSOLVER_H
8 #define IR_SEG_SYMBOLICEXPRGRAPHSOLVER_H
10 #include <llvm/IR/BasicBlock.h>
11 #include <llvm/IR/Dominators.h>
14 #include <unordered_map>
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"
28 #include "Utils/ADT/PushPopCache.h"
33 class ExternalMemorySpec;
55 ExternalMemorySpec *MemSpec =
nullptr;
56 ExternalIOSpec *IOSpec =
nullptr;
60 ExternalMemorySpec *MemSepc, ExternalIOSpec *IOSpec);
64 SMTExprVec getCtrlDeps(
const SEGNodeBase *N,
void *Args =
nullptr);
68 void *Args =
nullptr);
75 virtual std::pair<SMTExprVec, SMTExprVec>
77 void *Args =
nullptr) {
78 return __getCtrlDeps(B, G);
82 virtual SMTExprVec getDataDeps(
const SEGNodeBase *N,
void *Args =
nullptr);
87 virtual SMTExprVec getPhiGated(
const SEGPhiNode *PhiNode,
89 void *Args =
nullptr);
93 BasicBlock *BB,
void *Args =
nullptr);
99 void *Args =
nullptr);
110 virtual std::pair<SMTExprVec, SMTExprVec> getDepsPair(
const SEGNodeBase *N,
116 std::pair<SMTExprVec, SMTExprVec>
119 std::pair<SMTExprVec, SMTExprVec>
124 SMTExprVec __getDataDeps(
const SEGNodeBase *N,
size_t Depth = 0);
129 virtual void pop(
unsigned N = 1);
131 virtual void reset();
133 virtual SMTResultType check();
136 PushPopCache<const SEGNodeBase *> ConstraintCache;
137 PushPopCache<BasicBlock *> BBCache;
140 PushPopCache<const SEGArgumentNode *> FunctionArgumentCache;
141 PushPopCache<const SEGCallSiteOutputNode *> CallSiteOutputCache;
143 std::unordered_map<BasicBlock *, SMTExprVec> CtrlCacheMap;
144 std::unordered_map<const SEGOpcodeNode *, SMTExpr> OpcodeConstraintsCacheMap;
147 const std::unordered_set<const SEGArgumentNode *> &
148 getUsedFunctionArguments() {
149 return FunctionArgumentCache.getCacheSet();
153 std::pair<std::vector<const SEGCallSiteOutputNode *>::iterator,
154 std::vector<const SEGCallSiteOutputNode *>::iterator>
155 getUsedCallSiteOutputs(
bool Restart =
false) {
156 return CallSiteOutputCache.getCacheVector(Restart);
162 auto It = NodeSymbolNameMap.find(Symbol);
163 if (It == NodeSymbolNameMap.end()) {
169 virtual SMTExpr getOrInsertExpr(
const SEGNodeBase *N);
186 virtual SMTExpr encodeBinaryOpcodeNode(
const SEGOpcodeNode *N);
187 virtual SMTExpr encodeCompareOpcodeNode(
const SEGOpcodeNode *N);
188 virtual SMTExpr encodeCastOpcodeNode(
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);
202 std::unordered_map<BasicBlock *, std::pair<SMTExprVec, BasicBlock *>>
207 ExternalMemorySpec *MemSpec, ExternalIOSpec *IOSpec,
215 void *Args =
nullptr);
217 virtual std::pair<SMTExprVec, SMTExprVec>
219 void *Args =
nullptr) {
220 BasicBlock *PrevB = (BasicBlock *)Args;
221 return __getCtrlDepsWrapper(B, G, PrevB);
226 virtual SMTExprVec getDataDeps(
const SEGNodeBase *N,
void *Args =
nullptr);
232 virtual SMTExprVec getPhiGated(
const SEGPhiNode *PhiNode,
234 void *Args =
nullptr);
236 virtual void reset();
246 std::pair<SMTExprVec, SMTExprVec>
253 std::pair<SMTExprVec, SMTExprVec>
256 std::pair<SMTExprVec, SMTExprVec>
263 SMTExprVec __getDataDeps(
const SEGNodeBase *N, BasicBlock *PrevB);