Skip to content

Commit a73c325

Browse files
SpencerL-YSpencerL-Y
committed
add obtainMemtrackRoots
1 parent 7d4e013 commit a73c325

File tree

8 files changed

+81
-9
lines changed

8 files changed

+81
-9
lines changed

‎CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -190,6 +190,7 @@ add_library(smackTranslator STATIC
190190
lib/smack/SVNaming.cpp
191191
lib/smack/sesl/executor/Translator.cpp
192192
lib/smack/sesl/executor/BlockExecutor.cpp
193+
lib/smack/sesl/executor/ExecutionState.cpp
193194
lib/smack/sesl/verifier/MemSafeVerifier.cpp
194195
lib/smack/sesl/executor/VarEquiv.cpp
195196
lib/smack/sesl/executor/VarFactory.cpp

‎include/smack/SmackModuleGenerator.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ class SmackModuleGenerator : public llvm::ModulePass {
2424
virtual bool runOnModule(llvm::Module &m);
2525
void generateProgram(llvm::Module &m);
2626
Program *getProgram() { return program; }
27+
std::map<std::string, std::string> getIRVar2Source() {return boogieVar2SrcVarMap; }
2728
};
2829
} // namespace smack
2930

‎include/smack/sesl/executor/BlockExecutor.h‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,10 @@ namespace smack{
4949
VarFactoryPtr varFactory;
5050
StoreSplitterPtr storeSplit;
5151
std::list<std::string> callStack;
52+
// for memtrack
53+
std::map<std::string, std::string> IROrigVar2Src;
54+
std::map<std::string, std::string> src2IRVar;
55+
std::set<std::string> globalStaticVars;
5256
CFGPtr cfg;
5357

5458
// ------------------ Variable Utilities
@@ -145,7 +149,7 @@ namespace smack{
145149
public:
146150
static MemoryManagerPtr ExprMemoryManager;
147151

148-
BlockExecutor(Program* p, CFGPtr cfgPtr, StatePtr cb) : program(p), cfg(cfgPtr) {this->setBlock(cb); this->cfg->addVarType("$Null", "ref64");}
152+
BlockExecutor(Program* p, CFGPtr cfgPtr, StatePtr cb, std::map<std::string, std::string> IR2Src) : program(p), cfg(cfgPtr), IROrigVar2Src(IR2Src) {this->setBlock(cb); this->cfg->addVarType("$Null", "ref64");}
149153

150154
// --------------------- Execution for initialization
151155
SHExprPtr executeGlobal(SHExprPtr sh);

‎include/smack/sesl/executor/ExecutionState.h‎

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,15 +18,27 @@ namespace smack
1818
StoreSplitterPtr storeSplit;
1919
std::list<std::string> callStack;
2020

21+
std::map<std::string, std::string> src2IRVar;
22+
std::set<std::string> globalStaticVars;
23+
2124

2225
public:
23-
ExecutionState(SHExprPtr sh, VarEquivPtr veq, VarFactoryPtr varFac, StoreSplitterPtr stsplit, std::list<std::string> stack) : sh(sh), varEquiv(veq), varFactory(varFac), storeSplit(stsplit), callStack(stack){};
26+
ExecutionState(SHExprPtr sh, VarEquivPtr veq, VarFactoryPtr varFac, StoreSplitterPtr stsplit,
27+
std::list<std::string> stack,
28+
std::map<std::string, std::string> s2i, std::set<std::string> gsv)
29+
: sh(sh), varEquiv(veq), varFactory(varFac), storeSplit(stsplit),
30+
callStack(stack),
31+
src2IRVar(s2i), globalStaticVars(gsv) {};
2432

2533
SHExprPtr getSH(){return this->sh;}
2634
VarEquivPtr getVarEquiv(){return this->varEquiv;}
2735
VarFactoryPtr getVarFactory(){return this->varFactory;}
2836
StoreSplitterPtr getStoreSplit(){return this->storeSplit;}
2937
std::list<std::string> getCallStack(){return this->callStack;}
38+
std::map<std::string, std::string> getSrc2IRVar() {return this->src2IRVar;}
39+
std::set<std::string> getGlobalStaticVars(){return this->globalStaticVars;}
40+
41+
std::set<std::string> obtainMemtrackRootSet();
3042

3143
~ExecutionState(){};
3244
};

‎lib/smack/BoogieAst.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -676,7 +676,7 @@ namespace smack {
676676

677677
z3::expr resultEquality = z3Ctx.bool_val(true);
678678
if (leftVarSize == rightVarSize) {
679-
CFDEBUG(std::cout << "leftVarSize == rightVarSize" << leftVarSize << " " << rightVarSize << std::endl;);
679+
//CFDEBUG(std::cout << "leftVarSize == rightVarSize" << leftVarSize << " " << rightVarSize << std::endl;);
680680
for (int index = 0; index < leftVarSize; index++) {
681681
resultEquality = (resultEquality &&
682682
(z3Ctx.int_const(
@@ -740,7 +740,7 @@ namespace smack {
740740
}
741741
return res;
742742
} else {
743-
CFDEBUG(std::cout << "WARNING: directly let lhs == rhs ..." << std::endl;)
743+
// CFDEBUG(std::cout << "WARNING: directly let lhs == rhs ..." << std::endl;)
744744
res = (left == right);
745745
return res;
746746
}

‎lib/smack/sesl/executor/BlockExecutor.cpp‎

Lines changed: 27 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ namespace smack{
3434
CFDEBUG(std::cout << "INFO: register global variable: " << globalVarOrigName << " : " << typeStr << std::endl;);
3535
this->cfg->addVarType(globalVarOrigName, typeStr);
3636
std::pair<const VarExpr*, std::string> usedVarNamePair = this->useVarAndName(globalVarOrigName);
37+
// this->globalStaticVars.insert(globalVarOrigName);
3738
const VarExpr* globalVar = usedVarNamePair.first;
3839
std::string globalVarName = usedVarNamePair.second;
3940
if(this->getVarType(globalVarName) == VarType::DATA){
@@ -51,6 +52,7 @@ namespace smack{
5152
CFDEBUG(std::cout << "INFO: useVar " << staticVarOrigName << std::endl;);
5253
this->cfg->addVarType(staticVarOrigName, typeStr);
5354
std::pair<const VarExpr*, std::string> usedVarNamePair = this->useVarAndName(staticVarOrigName);
55+
// this->globalStaticVars.insert(staticVarOrigName);
5456
const VarExpr* staticVar = usedVarNamePair.first;
5557
std::string staticVarName = usedVarNamePair.second;
5658

@@ -148,6 +150,22 @@ namespace smack{
148150
CFDEBUG(std::cout << "ERROR: This should not happen.");
149151
assert(false);
150152
}
153+
154+
// update with memtrack utils
155+
156+
if(this->IROrigVar2Src.find(lhsVarOrigName) != this->IROrigVar2Src.end()){
157+
// there is a main src variable corresponds to lhsVar
158+
// update the srcVar to the usedVarName
159+
this->src2IRVar[this->IROrigVar2Src[lhsVarOrigName]] = lhsVarName;
160+
}
161+
if(lhsVarOrigName.find("$M.") != std::string::npos){
162+
this->globalStaticVars.insert(lhsVarOrigName);
163+
}
164+
165+
CFDEBUG(std::cout << "INFO: update src mapping" << std::endl;);
166+
for(auto i : this->src2IRVar){
167+
CFDEBUG(std::cout << "SrcVar: " << i.first << " IRVar: " << i.second << std::endl;)
168+
}
151169
// // TODOsh: refactor to make it more compatible with varFactory
152170
// if(lhsVarName.find("$M") != std::string::npos){
153171
// this->cfg->addVarType(lhsVarOrigName, "ref" + std::to_string(8 * PTR_BYTEWIDTH));
@@ -3592,7 +3610,10 @@ namespace smack{
35923610
this->storeSplit = previousExecState->getStoreSplit();
35933611
// Initialize callStack
35943612
this->callStack = previousExecState->getCallStack();
3595-
3613+
// Initialize memtrack utils
3614+
this->src2IRVar = previousExecState->getSrc2IRVar();
3615+
this->globalStaticVars = previousExecState->getGlobalStaticVars();
3616+
35963617
StatementList newStmts;
35973618
newStmts.push_back(Stmt::symbheap(previousSH));
35983619
SHExprPtr currSH = previousSH;
@@ -3605,7 +3626,7 @@ namespace smack{
36053626
currSH = newSH;
36063627
}
36073628

3608-
ExecutionStatePtr resultExecState = std::make_shared<ExecutionState>(currSH, this->varEquiv, this->varFactory, this->storeSplit, this->callStack);
3629+
ExecutionStatePtr resultExecState = std::make_shared<ExecutionState>(currSH, this->varEquiv, this->varFactory, this->storeSplit, this->callStack, this->src2IRVar, this->globalStaticVars);
36093630
return std::pair<ExecutionStatePtr, StatementList>(resultExecState, newStmts);
36103631
}
36113632

@@ -3620,10 +3641,13 @@ namespace smack{
36203641
this->storeSplit = initialExecState->getStoreSplit();
36213642
// Initialize stack
36223643
this->callStack = initialExecState->getCallStack();
3644+
// Initialize memtrack utils
3645+
this->src2IRVar = initialExecState->getSrc2IRVar();
3646+
this->globalStaticVars = initialExecState->getGlobalStaticVars();
36233647

36243648
SHExprPtr newSH = this->executeGlobal(previousSH);
36253649

3626-
ExecutionStatePtr resultExecState = std::make_shared<ExecutionState>(newSH, this->varEquiv, this->varFactory, this->storeSplit, this->callStack);
3650+
ExecutionStatePtr resultExecState = std::make_shared<ExecutionState>(newSH, this->varEquiv, this->varFactory, this->storeSplit, this->callStack, this->src2IRVar, this->globalStaticVars);
36273651
return resultExecState;
36283652
}
36293653

‎lib/smack/sesl/executor/ExecutionState.cpp‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
// Author: Xie Li, Yutian Zhu
2+
// Institute: ISCAS
3+
// 2021/11/3
4+
5+
#include "smack/sesl/executor/ExecutionState.h"
6+
7+
namespace smack{
8+
std::set<std::string> ExecutionState::obtainMemtrackRootSet(){
9+
std::set<std::string> resultSet;
10+
for(auto i : this->src2IRVar){
11+
resultSet.insert(i.second);
12+
}
13+
for(std::string s : this->globalStaticVars){
14+
const VarExpr* var = this->varFactory->getVar(s);
15+
assert(var != nullptr);
16+
resultSet.insert(var->name());
17+
}
18+
std::cout << " xxxxxxxxxxxxxxxxxxx resultSet: " << std::endl;
19+
for(std::string s : resultSet){
20+
std::cout << s << " " ;
21+
}
22+
std::cout << std::endl;
23+
return resultSet;
24+
}
25+
}

‎lib/smack/sesl/verifier/MemSafeVerifier.cpp‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ namespace smack {
2929
std::cout << "-----------------START MEMSAFE ANALYSIS---------------" << std::endl;
3030
SmackModuleGenerator &smackGen = getAnalysis<SmackModuleGenerator>();
3131
Program* program = smackGen.getProgram();
32+
std::map<std::string, std::string> IROrigVar2Src = smackGen.getIRVar2Source();
3233
// TODO: add the checking here.
3334
std::cout << "Begin verifying" << std::endl;
3435
CFGUtil cfgUtil(program);
@@ -90,14 +91,17 @@ namespace smack {
9091
StoreSplitterPtr storeSplit = std::make_shared<StoreSplitter>();
9192
// Initialize call Stack
9293
std::list<std::string> callStack;
94+
// Initialize memtrack utils
95+
std::map<std::string, std::string> src2IRVar;
96+
std::set<std::string> globalStaticVars;
9397

94-
ExecutionStatePtr initialExecState = std::make_shared<ExecutionState>(initSH, allocEquiv, varFac, storeSplit, callStack);
98+
ExecutionStatePtr initialExecState = std::make_shared<ExecutionState>(initSH, allocEquiv, varFac, storeSplit, callStack, src2IRVar, globalStaticVars);
9599
// initialization of the execution initial state over
96100
// Initialize a CFGExecutor
97101
SHExprPtr currSH = initSH;
98102
ExecutionStatePtr currExecState = initialExecState;
99103
StatementList finalStmts;
100-
BlockExecutorPtr be = std::make_shared<BlockExecutor>(program, mainGraph, state);
104+
BlockExecutorPtr be = std::make_shared<BlockExecutor>(program, mainGraph, state, IROrigVar2Src);
101105
currExecState = be->initializeExec(currExecState);
102106
for(StatePtr s : p.getExePath()){
103107
be->setBlock(s);
@@ -291,6 +295,7 @@ namespace smack {
291295
}
292296
}
293297
int errType;
298+
std::set<std::string> memtrackRoots = state->obtainMemtrackRootSet();
294299
if(!checkMemTrack(state, mainGraph)) {
295300
DEBUG_WITH_COLOR(std::cout << "LEAK: Memtrack!!!" << std::endl;, color::red);
296301
errType = MEMTRACK;

0 commit comments

Comments
 (0)