Merge pull request #1155 from JasonZhongZexin/update-from-master-0615…

…-WIP fix issue 1139
SVF-tools · Jul 31, 2023 · d1d843a · d1d843a
2 parents be87f78 + 74a1671
commit d1d843a
Show file tree

Hide file tree

Showing 5 changed files with 108 additions and 40 deletions.
diff --git a/svf/include/WPA/Andersen.h b/svf/include/WPA/Andersen.h
@@ -69,6 +69,12 @@ class AndersenBase:  public WPAConstraintSolver, public BVDataPTAImpl
     /// Andersen analysis
     virtual void analyze() override;
 
+    virtual void solveAndwritePtsToFile(const std::string& filename);
+
+    virtual void readPtsFromFile(const std::string& filename);
+
+    virtual void solveConstraints();
+
     /// Initialize analysis
     virtual void initialize() override;
 

diff --git a/svf/include/WPA/FlowSensitive.h b/svf/include/WPA/FlowSensitive.h
@@ -101,6 +101,12 @@ class FlowSensitive : public WPASVFGFSSolver, public BVDataPTAImpl
     /// Flow sensitive analysis
     void analyze() override;
 
+    virtual void solveAndwritePtsToFile(const std::string& filename);
+
+    virtual void readPtsFromFile(const std::string& filename);
+
+    virtual void solveConstraints();
+
     /// Initialize analysis
     void initialize() override;
 

diff --git a/svf/lib/MemoryModel/PointerAnalysisImpl.cpp b/svf/lib/MemoryModel/PointerAnalysisImpl.cpp
@@ -169,7 +169,7 @@ void BVDataPTAImpl::writeObjVarToFile(const string& filename)
         outs() << "  error opening file for writing!\n";
         return;
     }
-
+    
     // Write BaseNodes insensitivity to file
     NodeBS NodeIDs;
     for (auto it = pag->begin(), ie = pag->end(); it != ie; ++it)
@@ -185,14 +185,14 @@ void BVDataPTAImpl::writeObjVarToFile(const string& filename)
 
     f << "------\n";
 
-    // Job finish and close file
     f.close();
     if (f.good())
     {
         outs() << "\n";
         return;
     }
 
+
 }
 
 /*!

diff --git a/svf/lib/WPA/Andersen.cpp b/svf/lib/WPA/Andersen.cpp
@@ -97,28 +97,9 @@ void AndersenBase::finalize()
     BVDataPTAImpl::finalize();
 }
 
-/*!
- * Andersen analysis
- */
-void AndersenBase::analyze()
+void AndersenBase::solveConstraints()
 {
-    /// Initialization for the Solver
-    initialize();
-
-    bool readResultsFromFile = false;
-    if(!Options::ReadAnder().empty())
-    {
-        readResultsFromFile = this->readFromFile(Options::ReadAnder());
-        // Finalize the analysis
-        PointerAnalysis::finalize();
-    }
-
-    if (!Options::WriteAnder().empty())
-        this->writeObjVarToFile(Options::WriteAnder());
-
-    if(!readResultsFromFile)
-    {
-        // Start solving constraints
+     // Start solving constraints
         DBOUT(DGENERAL, outs() << SVFUtil::pasMsg("Start Solving Constraints\n"));
 
         bool limitTimerSet = SVFUtil::startAnalysisLimitTimer(Options::AnderTimeLimit());
@@ -144,17 +125,53 @@ void AndersenBase::analyze()
         SVFUtil::stopAnalysisLimitTimer(limitTimerSet);
 
         DBOUT(DGENERAL, outs() << SVFUtil::pasMsg("Finish Solving Constraints\n"));
+}
 
-    }
-
-    if (!Options::WriteAnder().empty())
+/*!
+ * Andersen analysis
+ */
+void AndersenBase::analyze()
+{
+    if(!Options::ReadAnder().empty())
     {
-        this->writeToFile(Options::WriteAnder());
+        readPtsFromFile(Options::ReadAnder());
     }
+    else{
+        if(Options::WriteAnder().empty())
+        {
+            initialize();
+            solveConstraints();
+            finalize();
+        }else{
+            solveAndwritePtsToFile(Options::WriteAnder());
+        }
+    }
+}
+
+/*!
+ * Andersen analysis: read pointer analysis result from file
+ */
+void AndersenBase::readPtsFromFile(const std::string& filename)
+{
+    initialize();
+    if (!filename.empty())
+        this->readFromFile(filename);
+    PointerAnalysis::finalize();
+}
 
-    if (!readResultsFromFile)
-        // Finalize the analysis
-        finalize();
+/*!
+ * Andersen analysis: solve constraints and write pointer analysis result to file
+ */
+void AndersenBase:: solveAndwritePtsToFile(const std::string& filename)
+{
+    /// Initialization for the Solver
+    initialize();
+    if (!filename.empty())
+        this->writeObjVarToFile(filename);
+    solveConstraints();
+    if (!filename.empty())
+        this->writeToFile(filename);
+    finalize();
 }
 
 void AndersenBase::cleanConsCG(NodeID id)

diff --git a/svf/lib/WPA/FlowSensitive.cpp b/svf/lib/WPA/FlowSensitive.cpp
@@ -74,17 +74,10 @@ void FlowSensitive::initialize()
     setGraph(svfg);
     //AndersenWaveDiff::releaseAndersenWaveDiff();
 }
-
-/*!
- * Start analysis
- */
-void FlowSensitive::analyze()
+void FlowSensitive::solveConstraints()
 {
     bool limitTimerSet = SVFUtil::startAnalysisLimitTimer(Options::FsTimeLimit());
-
-    /// Initialization for the Solver
-    initialize();
-
+
     double start = stat->getClk(true);
     /// Start solving constraints
     DBOUT(DGENERAL, outs() << SVFUtil::pasMsg("Start Solving Constraints\n"));
@@ -104,17 +97,63 @@ void FlowSensitive::analyze()
     while (updateCallGraph(getIndirectCallsites()));
 
     DBOUT(DGENERAL, outs() << SVFUtil::pasMsg("Finish Solving Constraints\n"));
-
+    
     // Reset the time-up alarm; analysis is done.
     SVFUtil::stopAnalysisLimitTimer(limitTimerSet);
 
     double end = stat->getClk(true);
     solveTime += (end - start) / TIMEINTERVAL;
 
+}
+
+/*!
+ * Start analysis
+ */
+void FlowSensitive::solveAndwritePtsToFile(const std::string& filename)
+{
+    /// Initialization for the Solver
+    initialize();
+    if(!filename.empty())
+        writeObjVarToFile(filename);
+    solveConstraints();
+    if(!filename.empty())
+        writeToFile(filename);
     /// finalize the analysis
     finalize();
 }
 
+/*!
+ * Start analysis
+ */
+void FlowSensitive::analyze()
+{
+    if(!Options::ReadAnder().empty())
+    {
+        readPtsFromFile(Options::ReadAnder());
+    }
+    else{
+        if(Options::WriteAnder().empty())
+        {
+            initialize();
+            solveConstraints();
+            finalize();
+        }else{
+            solveAndwritePtsToFile(Options::WriteAnder());
+        }
+    }
+}
+
+void FlowSensitive::readPtsFromFile(const std::string& filename)
+{
+    /// Initialization for the Solver
+    initialize();
+    /// Load the pts from file
+    if(!filename.empty())
+        this->readFromFile(filename);
+     /// finalize the analysis
+    finalize();
+}
+
 /*!
  * Finalize analysis
  */