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"
19 #include "IR/SEG/SEGArgumentNode.h"
20 #include "IR/SEG/SEGLoadMemNode.h"
21 #include "IR/SEG/SEGPhiNode.h"
22 #include "IR/SEG/SEGRegionNode.h"
23 #include "IR/SEG/SEGReturnNode.h"
24 #include "IR/SEG/SEGStoreMemNode.h"
26 #include "IR/SEG/SEGBinaryWithIntConstNode.h"
27 #include "IR/SEG/SEGCastNode.h"
29 #include "SMT/SMTFactory.h"
31 #include "Utils/ADT/PushPopCache.h"
36 class ExternalMemorySpec;
58 ExternalMemorySpec *MemSpec =
nullptr;
59 ExternalIOSpec *IOSpec =
nullptr;
63 ExternalMemorySpec *MemSepc, ExternalIOSpec *IOSpec);
67 SMTExprVec getCtrlDeps(
const SEGNodeBase *N,
void *Args =
nullptr);
71 void *Args =
nullptr);
78 virtual std::pair<SMTExprVec, SMTExprVec>
80 void *Args =
nullptr) {
81 return __getCtrlDeps(B, G);
85 virtual SMTExprVec getDataDeps(
const SEGNodeBase *N,
void *Args =
nullptr);
90 virtual SMTExprVec getPhiGated(
const SEGPhiNode *PhiNode,
92 void *Args =
nullptr);
96 BasicBlock *BB,
void *Args =
nullptr);
102 void *Args =
nullptr);
113 virtual std::pair<SMTExprVec, SMTExprVec> getDepsPair(
const SEGNodeBase *N,
119 std::pair<SMTExprVec, SMTExprVec>
122 std::pair<SMTExprVec, SMTExprVec>
127 SMTExprVec __getDataDeps(
const SEGNodeBase *N,
size_t Depth = 0);
132 virtual void pop(
unsigned N = 1);
134 virtual void reset();
136 virtual SMTResultType check();
139 PushPopCache<const SEGNodeBase *> ConstraintCache;
140 PushPopCache<BasicBlock *> BBCache;
143 PushPopCache<const SEGArgumentNode *> FunctionArgumentCache;
144 PushPopCache<const SEGCallSiteOutputNode *> CallSiteOutputCache;
146 std::unordered_map<BasicBlock *, SMTExprVec> CtrlCacheMap;
147 std::unordered_map<const SEGOpcodeNode *, SMTExpr> OpcodeConstraintsCacheMap;
150 const std::unordered_set<const SEGArgumentNode *> &
151 getUsedFunctionArguments() {
152 return FunctionArgumentCache.getCacheSet();
156 std::pair<std::vector<const SEGCallSiteOutputNode *>::iterator,
157 std::vector<const SEGCallSiteOutputNode *>::iterator>
158 getUsedCallSiteOutputs(
bool Restart =
false) {
159 return CallSiteOutputCache.getCacheVector(Restart);
165 auto It = NodeSymbolNameMap.find(Symbol);
166 if (It == NodeSymbolNameMap.end()) {
189 virtual SMTExpr encodeBinaryOpcodeNode(
const SEGOpcodeNode *N);
190 virtual SMTExpr encodeCompareOpcodeNode(
const SEGOpcodeNode *N);
191 virtual SMTExpr encodeCastOpcodeNode(
const SEGOpcodeNode *N);
193 virtual SMTExpr encodeExtractElementOpcodeNode(
const SEGOpcodeNode *N);
194 virtual SMTExpr encodeInsertElementOpcodeNode(
const SEGOpcodeNode *N);
195 virtual SMTExpr encodeSelectOpcodeNode(
const SEGOpcodeNode *N);
196 virtual SMTExpr encodeConcatOpcodeNode(
const SEGOpcodeNode *N);
205 std::unordered_map<BasicBlock *, std::pair<SMTExprVec, BasicBlock *>>
210 ExternalMemorySpec *MemSpec, ExternalIOSpec *IOSpec,
218 void *Args =
nullptr);
220 virtual std::pair<SMTExprVec, SMTExprVec>
222 void *Args =
nullptr) {
223 BasicBlock *PrevB = (BasicBlock *)Args;
224 return __getCtrlDepsWrapper(B, G, PrevB);
229 virtual SMTExprVec getDataDeps(
const SEGNodeBase *N,
void *Args =
nullptr);
235 virtual SMTExprVec getPhiGated(
const SEGPhiNode *PhiNode,
237 void *Args =
nullptr);
239 virtual void reset();
249 std::pair<SMTExprVec, SMTExprVec>
256 std::pair<SMTExprVec, SMTExprVec>
259 std::pair<SMTExprVec, SMTExprVec>
266 SMTExprVec __getDataDeps(
const SEGNodeBase *N, BasicBlock *PrevB);