Updated witness generator to produce function sequence

genWitness/main.cpp

@@ -29,6 +29,8 @@ int main(int argc, char** argv)
   if (ifs) {
     string s;
     vector<Node> nodes; // Store all the nodes
+    vector<tuple<int, bool, string>> funcSeq; // XXX Store the function sequence 
+                                     // XXX bool = 0 : entry, 1: return 
     map<string, pair<int, int>> functions; // Store all the functions
     vector<string> ext; // Store external function names
     int sink_id = 0; // same as violation
@@ -137,7 +139,7 @@ int main(int argc, char** argv)
       }
     }
     // Set the scope of each called functions
-    traverse(nodes, functions, entry_id, nodes.size()-1, "main", -1);
+    traverse(nodes, funcSeq, functions, entry_id, nodes.size()-1, "main", -1);
 
 #ifdef DEBUG
     for (auto i = nodes.begin(); i != nodes.end(); i++) {
@@ -149,9 +151,16 @@ int main(int argc, char** argv)
     }
     cout << "\n\n\n============= HUMAN READABLE ============\n";
     printGraph(nodes, functions, entry_id, nodes.size()-1);
+    for (auto i = funcSeq.begin(); i != funcSeq.end(); i++) {
+      cout << get<0>(*i) << "   ";
+      if (get<1>(*i)) cout << "return";
+      else cout << "entrance";
+      cout << "   " << get<2>(*i) << endl;
+    }
 #else
     printMisc(filename);
-    printGraph(nodes, functions, entry_id, nodes.size()-1);
+    // printGraph(nodes, functions, entry_id, nodes.size()-1);
+    printFuncSeq(funcSeq);
     cout << "</graph>\n</graphml>";
 #endif
   }

genWitness/utils.cpp

@@ -70,20 +70,53 @@ void printGraph(vector<Node>& nodes, map<string, pair<int, int>>& f, int b, int
   }
 }
 
-void traverse(vector<Node>& nodes, map<string, pair<int, int>>& f, int b, int e, string s, int p) {
+void printFuncSeq(vector<tuple<int, bool, string>>& funcSeq) {
+  vector<string> funcName;
+  cout << "<node id=\"ENTRY\">\n"
+       << "<data key=\"entry\">true</data>\n"
+       << "</node>\n";
+  cout << "<edge source=\"ENTRY\" target=\"" << get<0>(funcSeq[0]) << "\"/>\n";
+  for (size_t i = 0; i < funcSeq.size()-1; i++) {
+    cout << "<node id=\"" << get<0>(funcSeq[i]) << "\"/>\n";
+    cout << "<edge source=\"" << get<0>(funcSeq[i]) << "\" target=\"" << get<0>(funcSeq[i+1]) << "\">\n";
+    if (get<1>(funcSeq[i]) == 0) {
+      cout << "<data key=\"enterFunction\">" << get<2>(funcSeq[i]) << "</data>\n"
+           << "</edge>\n";
+      funcName.push_back(get<2>(funcSeq[i]));
+    }
+    else {
+      cout << "<data key=\"returnFrom\">" << funcName.back() << "</data>\n"
+           << "</edge>\n";
+      funcName.pop_back();
+    }
+  }
+  cout << "<node id=\"" << get<0>(funcSeq.back()) << "\"/>\n";
+  cout << "<edge source=\"" << get<0>(funcSeq.back()) << "\" target=\"ERROR\">\n";
+  cout << "<data key=\"returnFrom\">" << funcName.back() << "</data>\n"
+       << "</edge>\n";
+  funcName.pop_back();
+  cout << "<node id=\"ERROR\">\n"
+       << "<data key=\"violation\">true</data>\n"
+       << "</node>\n";
+}
+
+void traverse(vector<Node>& nodes, vector<tuple<int, bool, string>>& funcSeq, map<string, pair<int, int>>& f, int b, int e, string s, int p) {
   for (int i = b; i <= e; i++) {
     if (!nodes[i].isExtern()) {
       nodes[i].setScope(s);
       if (nodes[i].isFuncCall()) {
         string n = nodes[i].getFunc();
         int bn = f[n].first, en = f[n].second;
         if (n.find("VERIFIER") == string::npos) {
+          funcSeq.push_back(make_tuple(nodes[i].getId(), 0, n));
           nodes[i].setNext(bn);
-          traverse(nodes, f, bn, en, n, i);
+          traverse(nodes, funcSeq, f, bn, en, n, i);
         }
       }
       else if (nodes[i].isFuncReturn()) {
         nodes[i].setNext(p+1);
+        string n = nodes[i].getFunc();
+        funcSeq.push_back(make_tuple(nodes[i].getId(),1, n));
       }
     }
   }

genWitness/utils.h

@@ -4,13 +4,17 @@
 #include <vector>
 #include <map>
 #include <string>
+#include <tuple>
 #include "nodes.h"
 
 bool checkTrivial(const std::string&);
 bool checkFunctionEntrance(const std::string &);
 bool checkFunctionReturn(const std::string &);
 void printGraph(std::vector<Node>&, std::map<std::string, std::pair<int, int>>&, int, int) ;
+void printFuncSeq(std::vector<std::tuple<int, bool, std::string>>&);
 void printMisc(std::string);
-void traverse(std::vector<Node>&, std::map<std::string, std::pair<int, int>>&, int, int, std::string, int ) ;
+void traverse(std::vector<Node>&, 
+    std::vector<std::tuple<int, bool, std::string>>&,
+    std::map<std::string, std::pair<int, int>>&, int, int, std::string, int ) ;
 void changeOperator(std::string&);
 #endif// __UTILS_H__

scripts/gen_witness.sh

@@ -9,7 +9,10 @@ if [ -d output ]; then
   rm -rf output
 fi
 mkdir output
-cp template.graphml output/witness.graphml
+#cp template.graphml output/witness.graphml
+genWitness/genWitness $1 > witness.graphml
+sed -i 's/_call[0-9]//g' witness.graphml
+mv witness.graphml output
 date2=$(date +"%s")
 diff=$(($date2-$date1))
 echo -e "\n*** Witness Generation: $(($diff / 60)) minutes and $(($diff % 60)) seconds elapsed."