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);
70 virtual SMTExprVec getCtrlDeps(WrappedBasicBlock *B,
72 void *Args =
nullptr);
79 virtual std::pair<SMTExprVec, SMTExprVec>
81 void *Args =
nullptr) {
82 return __getCtrlDeps(B, G);
86 virtual SMTExprVec getDataDeps(
const SEGNodeBase *N,
void *Args =
nullptr);
91 virtual SMTExprVec getPhiGated(
const SEGPhiNode *PhiNode,
93 void *Args =
nullptr);
97 WrappedBasicBlock *BB,
void *Args =
nullptr);
103 void *Args =
nullptr);
114 virtual std::pair<SMTExprVec, SMTExprVec> getDepsPair(
const SEGNodeBase *N,
120 std::pair<SMTExprVec, SMTExprVec> __getCtrlDeps(WrappedBasicBlock *B,
124 std::pair<SMTExprVec, SMTExprVec>
128 SMTExprVec __getDataDeps(
const SEGNodeBase *N,
size_t Depth = 0);
133 virtual void pop(
unsigned N = 1);
135 virtual void reset();
137 virtual SMTResultType check();
140 PushPopCache<const SEGNodeBase *> ConstraintCache;
141 PushPopCache<WrappedBasicBlock *> BBCache;
144 PushPopCache<const SEGArgumentNode *> FunctionArgumentCache;
145 PushPopCache<const SEGCallSiteOutputNode *> CallSiteOutputCache;
147 std::unordered_map<WrappedBasicBlock *, SMTExprVec> CtrlCacheMap;
148 std::unordered_map<const SEGOpcodeNode *, SMTExpr> OpcodeConstraintsCacheMap;
151 const std::unordered_set<const SEGArgumentNode *> &
152 getUsedFunctionArguments() {
153 return FunctionArgumentCache.getCacheSet();
157 std::pair<std::vector<const SEGCallSiteOutputNode *>::iterator,
158 std::vector<const SEGCallSiteOutputNode *>::iterator>
159 getUsedCallSiteOutputs(
bool Restart =
false) {
160 return CallSiteOutputCache.getCacheVector(Restart);
166 auto It = NodeSymbolNameMap.find(Symbol);
167 if (It == NodeSymbolNameMap.end()) {
190 virtual SMTExpr encodeBinaryOpcodeNode(
const SEGOpcodeNode *N);
191 virtual SMTExpr encodeCompareOpcodeNode(
const SEGOpcodeNode *N);
192 virtual SMTExpr encodeCastOpcodeNode(
const SEGOpcodeNode *N);
194 virtual SMTExpr encodeExtractElementOpcodeNode(
const SEGOpcodeNode *N);
195 virtual SMTExpr encodeInsertElementOpcodeNode(
const SEGOpcodeNode *N);
196 virtual SMTExpr encodeSelectOpcodeNode(
const SEGOpcodeNode *N);
197 virtual SMTExpr encodeConcatOpcodeNode(
const SEGOpcodeNode *N);
206 std::unordered_map<WrappedBasicBlock *,
207 std::pair<SMTExprVec, WrappedBasicBlock *>>
212 ExternalMemorySpec *MemSpec, ExternalIOSpec *IOSpec,
219 virtual SMTExprVec getCtrlDeps(WrappedBasicBlock *B,
221 void *Args =
nullptr);
223 virtual std::pair<SMTExprVec, SMTExprVec>
225 void *Args =
nullptr) {
226 WrappedBasicBlock *PrevB = (WrappedBasicBlock *)Args;
227 return __getCtrlDepsWrapper(B, G, PrevB);
232 virtual SMTExprVec getDataDeps(
const SEGNodeBase *N,
void *Args =
nullptr);
238 virtual SMTExprVec getPhiGated(
const SEGPhiNode *PhiNode,
240 void *Args =
nullptr);
242 virtual void reset();
252 std::pair<SMTExprVec, SMTExprVec>
254 WrappedBasicBlock *PrevB);
259 std::pair<SMTExprVec, SMTExprVec> __getCtrlDeps(WrappedBasicBlock *B,
261 WrappedBasicBlock *PrevB);
263 std::pair<SMTExprVec, SMTExprVec>
265 WrappedBasicBlock *PrevB);
270 SMTExprVec __getDataDeps(
const SEGNodeBase *N, WrappedBasicBlock *PrevB);