Merge pull request #116 from SpencerL-Y/refactorLoadIndex

add obtainMemtrackRoots

Author: SpencerL-Y

CMakeLists.txt

@@ -190,6 +190,7 @@ add_library(smackTranslator STATIC
   lib/smack/SVNaming.cpp
         lib/smack/sesl/executor/Translator.cpp
         lib/smack/sesl/executor/BlockExecutor.cpp
+        lib/smack/sesl/executor/ExecutionState.cpp
         lib/smack/sesl/verifier/MemSafeVerifier.cpp
         lib/smack/sesl/executor/VarEquiv.cpp
         lib/smack/sesl/executor/VarFactory.cpp

include/smack/SmackModuleGenerator.h

@@ -24,6 +24,7 @@ class SmackModuleGenerator : public llvm::ModulePass {
   virtual bool runOnModule(llvm::Module &m);
   void generateProgram(llvm::Module &m);
   Program *getProgram() { return program; }
+  std::map<std::string, std::string> getIRVar2Source() {return boogieVar2SrcVarMap; }
 };
 } // namespace smack
 

include/smack/sesl/executor/BlockExecutor.h

@@ -49,6 +49,10 @@ namespace smack{
         VarFactoryPtr varFactory;
         StoreSplitterPtr storeSplit;
         std::list<std::string> callStack;
+        // for memtrack
+        std::map<std::string, std::string> IROrigVar2Src;
+        std::map<std::string, std::string> src2IRVar;
+        std::set<std::string> globalStaticVars;
         CFGPtr cfg;
 
         // ------------------ Variable Utilities
@@ -145,7 +149,7 @@ namespace smack{
     public:
         static MemoryManagerPtr ExprMemoryManager;
 
-        BlockExecutor(Program* p, CFGPtr cfgPtr, StatePtr cb) : program(p), cfg(cfgPtr) {this->setBlock(cb); this->cfg->addVarType("$Null", "ref64");}
+        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");}
 
         // --------------------- Execution for initialization
         SHExprPtr executeGlobal(SHExprPtr sh);

include/smack/sesl/executor/ExecutionState.h

@@ -18,15 +18,27 @@ namespace smack
         StoreSplitterPtr storeSplit;
         std::list<std::string> callStack;
 
+        std::map<std::string, std::string> src2IRVar;
+        std::set<std::string> globalStaticVars;
+
 
     public:
-        ExecutionState(SHExprPtr sh, VarEquivPtr veq, VarFactoryPtr varFac, StoreSplitterPtr stsplit, std::list<std::string> stack) : sh(sh), varEquiv(veq), varFactory(varFac), storeSplit(stsplit), callStack(stack){};
+        ExecutionState(SHExprPtr sh, VarEquivPtr veq, VarFactoryPtr varFac, StoreSplitterPtr stsplit, 
+                       std::list<std::string> stack,
+                       std::map<std::string, std::string> s2i, std::set<std::string> gsv) 
+                       : sh(sh), varEquiv(veq), varFactory(varFac), storeSplit(stsplit), 
+                         callStack(stack), 
+                         src2IRVar(s2i), globalStaticVars(gsv) {};
 
         SHExprPtr getSH(){return this->sh;}
         VarEquivPtr getVarEquiv(){return this->varEquiv;}
         VarFactoryPtr getVarFactory(){return this->varFactory;}
         StoreSplitterPtr getStoreSplit(){return this->storeSplit;}
         std::list<std::string> getCallStack(){return this->callStack;}
+        std::map<std::string, std::string> getSrc2IRVar() {return this->src2IRVar;}
+        std::set<std::string> getGlobalStaticVars(){return this->globalStaticVars;}
+
+        std::set<std::string> obtainMemtrackRootSet();
 
         ~ExecutionState(){};
     };

lib/smack/BoogieAst.cpp

@@ -676,7 +676,7 @@ namespace smack {
 
                     z3::expr resultEquality = z3Ctx.bool_val(true);
                     if (leftVarSize == rightVarSize) {
-                        CFDEBUG(std::cout << "leftVarSize == rightVarSize" << leftVarSize << " " << rightVarSize << std::endl;);
+                        //CFDEBUG(std::cout << "leftVarSize == rightVarSize" << leftVarSize << " " << rightVarSize << std::endl;);
                         for (int index = 0; index < leftVarSize; index++) {
                             resultEquality = (resultEquality &&
                                               (z3Ctx.int_const(
@@ -740,7 +740,7 @@ namespace smack {
                         }
                         return res;
                     } else {
-                        CFDEBUG(std::cout << "WARNING: directly let lhs == rhs ..." << std::endl;)
+                        // CFDEBUG(std::cout << "WARNING: directly let lhs == rhs ..." << std::endl;)
                         res = (left == right);
                         return res;
                     }

lib/smack/sesl/executor/BlockExecutor.cpp

@@ -34,6 +34,7 @@ namespace smack{
                 CFDEBUG(std::cout << "INFO: register global variable: " << globalVarOrigName << " : " << typeStr <<  std::endl;);
                 this->cfg->addVarType(globalVarOrigName, typeStr);
                 std::pair<const VarExpr*, std::string> usedVarNamePair = this->useVarAndName(globalVarOrigName);
+                // this->globalStaticVars.insert(globalVarOrigName);
                 const VarExpr* globalVar = usedVarNamePair.first;
                 std::string globalVarName = usedVarNamePair.second;
                 if(this->getVarType(globalVarName) == VarType::DATA){
@@ -51,6 +52,7 @@ namespace smack{
                 CFDEBUG(std::cout << "INFO: useVar " << staticVarOrigName << std::endl;);
                 this->cfg->addVarType(staticVarOrigName, typeStr);
                 std::pair<const VarExpr*, std::string> usedVarNamePair = this->useVarAndName(staticVarOrigName);
+                // this->globalStaticVars.insert(staticVarOrigName);
                 const VarExpr* staticVar = usedVarNamePair.first;
                 std::string staticVarName = usedVarNamePair.second; 
 
@@ -148,6 +150,22 @@ namespace smack{
             CFDEBUG(std::cout << "ERROR: This should not happen.");
             assert(false);
         }
+
+        // update with memtrack utils
+        
+        if(this->IROrigVar2Src.find(lhsVarOrigName) != this->IROrigVar2Src.end()){
+            // there is a main src variable corresponds to lhsVar
+            // update the srcVar  to the usedVarName
+            this->src2IRVar[this->IROrigVar2Src[lhsVarOrigName]] = lhsVarName;
+        }
+        if(lhsVarOrigName.find("$M.") != std::string::npos){
+            this->globalStaticVars.insert(lhsVarOrigName);
+        }
+
+        CFDEBUG(std::cout << "INFO: update src mapping" << std::endl;);
+        for(auto i : this->src2IRVar){
+            CFDEBUG(std::cout << "SrcVar: " << i.first << " IRVar: " << i.second << std::endl;)
+        }
         // // TODOsh: refactor to make it more compatible with varFactory
         // if(lhsVarName.find("$M") != std::string::npos){
         //     this->cfg->addVarType(lhsVarOrigName, "ref" + std::to_string(8 * PTR_BYTEWIDTH));
@@ -3592,7 +3610,10 @@ namespace smack{
         this->storeSplit = previousExecState->getStoreSplit();
         // Initialize callStack
         this->callStack = previousExecState->getCallStack();
-        
+        // Initialize memtrack utils
+        this->src2IRVar = previousExecState->getSrc2IRVar();
+        this->globalStaticVars = previousExecState->getGlobalStaticVars();
+
         StatementList newStmts;
         newStmts.push_back(Stmt::symbheap(previousSH));
         SHExprPtr currSH = previousSH;
@@ -3605,7 +3626,7 @@ namespace smack{
             currSH = newSH;
         }
 
-        ExecutionStatePtr resultExecState = std::make_shared<ExecutionState>(currSH, this->varEquiv, this->varFactory, this->storeSplit, this->callStack);
+        ExecutionStatePtr resultExecState = std::make_shared<ExecutionState>(currSH, this->varEquiv, this->varFactory, this->storeSplit, this->callStack, this->src2IRVar, this->globalStaticVars);
         return std::pair<ExecutionStatePtr, StatementList>(resultExecState, newStmts);
     }
 
@@ -3620,10 +3641,13 @@ namespace smack{
         this->storeSplit = initialExecState->getStoreSplit();
         // Initialize stack
         this->callStack = initialExecState->getCallStack();
+        // Initialize memtrack utils
+        this->src2IRVar = initialExecState->getSrc2IRVar();
+        this->globalStaticVars = initialExecState->getGlobalStaticVars();
 
         SHExprPtr newSH = this->executeGlobal(previousSH);
 
-        ExecutionStatePtr resultExecState =  std::make_shared<ExecutionState>(newSH, this->varEquiv, this->varFactory, this->storeSplit, this->callStack);
+        ExecutionStatePtr resultExecState =  std::make_shared<ExecutionState>(newSH, this->varEquiv, this->varFactory, this->storeSplit, this->callStack, this->src2IRVar, this->globalStaticVars);
         return  resultExecState;
     }
 

lib/smack/sesl/executor/ExecutionState.cpp

@@ -0,0 +1,25 @@
+// Author: Xie Li, Yutian Zhu
+// Institute: ISCAS
+// 2021/11/3
+
+#include "smack/sesl/executor/ExecutionState.h"
+
+namespace smack{
+    std::set<std::string> ExecutionState::obtainMemtrackRootSet(){
+        std::set<std::string> resultSet;
+        for(auto i : this->src2IRVar){
+            resultSet.insert(i.second);
+        }
+        for(std::string s : this->globalStaticVars){
+            const VarExpr* var = this->varFactory->getVar(s);
+            assert(var != nullptr);
+            resultSet.insert(var->name());
+        }
+        std::cout << " xxxxxxxxxxxxxxxxxxx resultSet: " << std::endl;
+        for(std::string s : resultSet){
+            std::cout << s << "  " ;
+        }
+        std::cout << std::endl;
+        return resultSet;
+    }
+}

lib/smack/sesl/verifier/MemSafeVerifier.cpp

@@ -29,6 +29,7 @@ namespace smack {
         std::cout << "-----------------START MEMSAFE ANALYSIS---------------" << std::endl;
         SmackModuleGenerator &smackGen = getAnalysis<SmackModuleGenerator>();
         Program* program = smackGen.getProgram();
+        std::map<std::string, std::string> IROrigVar2Src = smackGen.getIRVar2Source();
         // TODO: add the checking here.
         std::cout << "Begin verifying" << std::endl;
         CFGUtil cfgUtil(program);
@@ -90,14 +91,17 @@ namespace smack {
             StoreSplitterPtr storeSplit = std::make_shared<StoreSplitter>();
             // Initialize call Stack
             std::list<std::string> callStack;
+            // Initialize memtrack utils
+            std::map<std::string, std::string> src2IRVar;
+            std::set<std::string> globalStaticVars;
 
-            ExecutionStatePtr initialExecState = std::make_shared<ExecutionState>(initSH, allocEquiv, varFac, storeSplit, callStack);
+            ExecutionStatePtr initialExecState = std::make_shared<ExecutionState>(initSH, allocEquiv, varFac, storeSplit, callStack, src2IRVar, globalStaticVars);
             // initialization of the execution initial state over
             // Initialize a CFGExecutor
             SHExprPtr currSH = initSH;
             ExecutionStatePtr  currExecState = initialExecState;
             StatementList finalStmts;
-            BlockExecutorPtr be = std::make_shared<BlockExecutor>(program, mainGraph, state);
+            BlockExecutorPtr be = std::make_shared<BlockExecutor>(program, mainGraph, state, IROrigVar2Src);
             currExecState = be->initializeExec(currExecState);
             for(StatePtr s : p.getExePath()){
                 be->setBlock(s);
@@ -291,6 +295,7 @@ namespace smack {
                     }
                 }
                 int errType;
+                std::set<std::string> memtrackRoots = state->obtainMemtrackRootSet();
                 if(!checkMemTrack(state, mainGraph)) {
                     DEBUG_WITH_COLOR(std::cout << "LEAK: Memtrack!!!" << std::endl;, color::red);
                     errType = MEMTRACK;