Typedef wmm_grapht instead of repeating template instantiation

The typedef increases maintainability and will also enable proper use
of node identifier types in place of "unsigned".

Author: tautschnig

src/goto-instrument/wmm/cycle_collection.cpp

@@ -393,7 +393,7 @@ bool event_grapht::graph_explorert::backtrack(
     if(!get_com_only)
     {
       /* we first visit via po transition, if existing */
-      for(graph<abstract_eventt>::edgest::const_iterator
+      for(wmm_grapht::edgest::const_iterator
         w_it=egraph.po_out(vertex).begin();
         w_it!=egraph.po_out(vertex).end(); w_it++)
       {
@@ -436,7 +436,7 @@ bool event_grapht::graph_explorert::backtrack(
 
     if(!no_comm)
     /* we then visit via com transitions, if existing */
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       w_it=egraph.com_out(vertex).begin();
       w_it!=egraph.com_out(vertex).end(); w_it++)
     {
@@ -568,7 +568,7 @@ bool event_grapht::graph_explorert::backtrack(
          (!this_vertex.WRfence
            && egraph[point_stack.top()].operation==abstract_eventt::Write));
 
-    for(graph<abstract_eventt>::edgest::const_iterator w_it=
+    for(wmm_grapht::edgest::const_iterator w_it=
       egraph.po_out(vertex).begin();
       w_it!=egraph.po_out(vertex).end(); w_it++)
     {

src/goto-instrument/wmm/event_graph.cpp

@@ -42,7 +42,7 @@ void event_grapht::print_rec_graph(std::ofstream& file, unsigned node_id,
     "\"];" << std::endl;
   visited.insert(node_id);
 
-  for(graph<abstract_eventt>::edgest::const_iterator
+  for(wmm_grapht::edgest::const_iterator
     it=po_out(node_id).begin();
     it!=po_out(node_id).end(); ++it)
   {
@@ -52,7 +52,7 @@ void event_grapht::print_rec_graph(std::ofstream& file, unsigned node_id,
       print_rec_graph(file, it->first, visited);
   }
 
-  for(graph<abstract_eventt>::edgest::const_iterator
+  for(wmm_grapht::edgest::const_iterator
     it=com_out(node_id).begin();
     it!=com_out(node_id).end(); ++it)
   {
@@ -111,7 +111,7 @@ void event_grapht::explore_copy_segment(std::set<unsigned>& explored,
   if(begin==end)
     return;
 
-  for(graph<abstract_eventt>::edgest::const_iterator it=po_out(begin).begin();
+  for(wmm_grapht::edgest::const_iterator it=po_out(begin).begin();
     it!=po_out(begin).end();
     ++it)
     explore_copy_segment(explored, it->first, end);

src/goto-instrument/wmm/event_graph.h

@@ -29,6 +29,8 @@ class namespacet;
                      graph of abstract events
 \*******************************************************************/
 
+typedef graph<abstract_eventt> wmm_grapht;
+
 class event_grapht
 {
 public:
@@ -194,14 +196,14 @@ class event_grapht
 
     inline bool operator<(const critical_cyclet& other) const
     {
-      return ( ((std::list<unsigned>) *this) < (std::list<unsigned>)other);
+      return ( ((std::list<event_idt>) *this) < (std::list<event_idt>)other);
     }
   };
 
 protected:
   /* graph contains po and com transitions */
-  graph<abstract_eventt> po_graph;
-  graph<abstract_eventt> com_graph;
+  wmm_grapht po_graph;
+  wmm_grapht com_graph;
 
   /* parameters limiting the exploration */
   unsigned max_var;
@@ -365,7 +367,7 @@ class event_grapht
     return po_no;
   }
 
-  inline graph<abstract_eventt>::nodet &operator[](unsigned n)
+  inline wmm_grapht::nodet &operator[](unsigned n)
   {
     return po_graph[n];
   }
@@ -385,22 +387,22 @@ class event_grapht
     return po_graph.size();
   }
 
-  inline const graph<abstract_eventt>::edgest &po_in(unsigned n) const
+  inline const wmm_grapht::edgest &po_in(unsigned n) const
   {
     return po_graph.in(n);
   }
 
-  inline const graph<abstract_eventt>::edgest &po_out(unsigned n) const
+  inline const wmm_grapht::edgest &po_out(unsigned n) const
   {
     return po_graph.out(n);
   }
 
-  inline const graph<abstract_eventt>::edgest &com_in(unsigned n) const
+  inline const wmm_grapht::edgest &com_in(unsigned n) const
   {
     return com_graph.in(n);
   }
 
-  inline const graph<abstract_eventt>::edgest &com_out(unsigned n) const
+  inline const wmm_grapht::edgest &com_out(unsigned n) const
   {
     return com_graph.out(n);
   }

src/goto-instrument/wmm/goto2graph.cpp

@@ -477,7 +477,7 @@ Function: alt_copy_segment
 
 \*******************************************************************/
 
-unsigned alt_copy_segment(graph<abstract_eventt>& alt_egraph,
+unsigned alt_copy_segment(wmm_grapht& alt_egraph,
   unsigned begin, unsigned end)
 {
   /* no need to duplicate the loop nodes for the SCC-detection graph -- a
@@ -1457,13 +1457,13 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet& cyc)
     }
     assert(current_po);
 
-    const graph<abstract_eventt>::edgest& pos_cur = egraph.po_out(*e_it);
-    const graph<abstract_eventt>::edgest& pos_next = egraph.po_out(*(++e_it));
+    const wmm_grapht::edgest& pos_cur = egraph.po_out(*e_it);
+    const wmm_grapht::edgest& pos_next = egraph.po_out(*(++e_it));
     --e_it;
 
     bool exists_n = false;
 
-    for(graph<abstract_eventt>::edgest::const_iterator edge_it=pos_cur.begin();
+    for(wmm_grapht::edgest::const_iterator edge_it=pos_cur.begin();
       edge_it!=pos_cur.end(); edge_it++)
     {
       if(pos_next.find(edge_it->first)!=pos_next.end())

src/goto-instrument/wmm/goto2graph.h

@@ -38,7 +38,7 @@ class instrumentert
 
   /* alternative representation of graph (SCC) */
   std::map<unsigned,unsigned> map_vertex_gnode;
-  graph<abstract_eventt> egraph_alt;
+  wmm_grapht egraph_alt;
 
   unsigned unique_id;
 
@@ -93,7 +93,7 @@ class instrumentert
     /* pointer to the egraph(s) that we construct */
     event_grapht& egraph;
     std::vector<std::set<unsigned> >& egraph_SCCs;
-    graph<abstract_eventt>& egraph_alt;
+    wmm_grapht& egraph_alt;
 
     /* for thread marking (dynamic) */
     unsigned current_thread;

src/goto-instrument/wmm/pair_collection.cpp

@@ -89,7 +89,7 @@ bool event_grapht::graph_pensieve_explorert::find_second_event(
 
   visited_nodes.insert(current);
 
-  for(graph<abstract_eventt>::edgest::const_iterator
+  for(wmm_grapht::edgest::const_iterator
     it=egraph.po_out(current).begin();
     it!=egraph.po_out(current).end(); ++it)
   {

src/musketeer/cycles_visitor.cpp

@@ -61,7 +61,7 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
         {
           /* also add pos of non-delaying pos+ of cycles, as they could AC or
              BC */
-          for(graph<abstract_eventt>::edgest::const_iterator
+          for(wmm_grapht::edgest::const_iterator
             next_it=egraph.po_in(e_i->first).begin();
             next_it!=egraph.po_in(e_i->first).end();
             ++next_it)
@@ -73,7 +73,7 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
               next_it->first, new_path);
           }
 
-          for(graph<abstract_eventt>::edgest::const_iterator
+          for(wmm_grapht::edgest::const_iterator
             next_it=egraph.po_out(e_i->second).begin();
             next_it!=egraph.po_out(e_i->second).end();
             ++next_it)
@@ -105,7 +105,7 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
       else
       {
         /* adds basic pos from this pos^+ */
-        for(graph<abstract_eventt>::edgest::const_iterator
+        for(wmm_grapht::edgest::const_iterator
           next_it=egraph.po_out(e_i.first).begin();
           next_it!=egraph.po_out(e_i.first).end();
           ++next_it)
@@ -129,7 +129,7 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
         else
         {
           /* adds basic pos from this pos^+ */
-          for(graph<abstract_eventt>::edgest::const_iterator
+          for(wmm_grapht::edgest::const_iterator
             next_it=egraph.po_out(e_i.first).begin();
             next_it!=egraph.po_out(e_i.first).end();
             ++next_it)

src/musketeer/graph_visitor.cpp

@@ -43,7 +43,7 @@ void const_graph_visitort::graph_explore(event_grapht& egraph, unsigned next,
     /* this path is not connecting a to b => return */
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(next).begin();
       next_it!=egraph.po_out(next).end();
       ++next_it)
@@ -90,7 +90,7 @@ void const_graph_visitort::const_graph_explore(event_grapht& egraph, unsigned ne
     /* this path is not connecting a to b => return */
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(next).begin();
       next_it!=egraph.po_out(next).end();
       ++next_it)
@@ -133,7 +133,7 @@ void const_graph_visitort::graph_explore_BC(event_grapht& egraph, unsigned next,
 
   /* if all the incoming pos were already visited, add */
   bool no_other_pos = true;
-  for(graph<abstract_eventt>::edgest::const_iterator it=
+  for(wmm_grapht::edgest::const_iterator it=
     egraph.po_out(next).begin();
     it!=egraph.po_out(next).end();
     ++it)
@@ -159,7 +159,7 @@ void const_graph_visitort::graph_explore_BC(event_grapht& egraph, unsigned next,
     assert(it!=old_path.end());
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(next).begin();
       next_it!=egraph.po_out(next).end();
       ++next_it)
@@ -195,7 +195,7 @@ void const_graph_visitort::const_graph_explore_BC(event_grapht& egraph,
 
   /* if all the incoming pos were already visited, add */
   bool no_other_pos = true;
-  for(graph<abstract_eventt>::edgest::const_iterator it=
+  for(wmm_grapht::edgest::const_iterator it=
     egraph.po_out(next).begin();
     it!=egraph.po_out(next).end();
     ++it)
@@ -222,7 +222,7 @@ void const_graph_visitort::const_graph_explore_BC(event_grapht& egraph,
     assert(it!=old_path.end());
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(next).begin();
       next_it!=egraph.po_out(next).end();
       ++next_it)
@@ -261,7 +261,7 @@ void const_graph_visitort::graph_explore_AC(event_grapht& egraph, unsigned next,
 
   /* if all the incoming pos were already visited, add */
   bool no_other_pos = true;
-  for(graph<abstract_eventt>::edgest::const_iterator it=
+  for(wmm_grapht::edgest::const_iterator it=
     egraph.po_in(next).begin();
     it!=egraph.po_in(next).end();
     ++it)
@@ -287,7 +287,7 @@ void const_graph_visitort::graph_explore_AC(event_grapht& egraph, unsigned next,
     assert(it!=old_path.end());
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_in(next).begin();
       next_it!=egraph.po_in(next).end();
       ++next_it)
@@ -323,7 +323,7 @@ void const_graph_visitort::const_graph_explore_AC(event_grapht& egraph,
 
   /* if all the incoming pos were already visited, add */
   bool no_other_pos = true;
-  for(graph<abstract_eventt>::edgest::const_iterator it=
+  for(wmm_grapht::edgest::const_iterator it=
     egraph.po_in(next).begin();
     it!=egraph.po_in(next).end();
     ++it)
@@ -351,7 +351,7 @@ void const_graph_visitort::const_graph_explore_AC(event_grapht& egraph,
     assert(it!=old_path.end());
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_in(next).begin();
       next_it!=egraph.po_in(next).end();
       ++next_it)
@@ -380,15 +380,15 @@ void const_graph_visitort::PT(const edget& e, std::set<unsigned>& edges) {
 
 //  if(!e.is_po) /* e is in po^+\po */ is_po is a flag set manually, do not
 //  use it for checks!!
-  const graph<abstract_eventt>::edgest& list_po_out=
+  const wmm_grapht::edgest& list_po_out=
     fence_inserter.instrumenter.egraph.po_out(e.first);
   if(list_po_out.find(e.second)==list_po_out.end())
   {
 #ifdef BTWN1
     event_grapht& egraph=fence_inserter.instrumenter.egraph;
 
     /* all the pos inbetween */
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(e.first).begin();
       next_it!=egraph.po_out(e.first).end();
       ++next_it)
@@ -444,7 +444,7 @@ void const_graph_visitort::CT(const edget& edge, std::set<unsigned>& edges) {
 
   /* if one event only on this thread of the cycle, discard */
   if(egraph.po_in(first).size() > 0)
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_in(first).begin();
       next_it!=egraph.po_in(first).end();
       ++next_it)
@@ -456,7 +456,7 @@ void const_graph_visitort::CT(const edget& edge, std::set<unsigned>& edges) {
     }
 
   if(egraph.po_out(second).size() > 0)
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(second).begin();
       next_it!=egraph.po_out(second).end();
       ++next_it)
@@ -499,7 +499,7 @@ void const_graph_visitort::CT_not_powr(const edget& edge,
   visited_nodes.clear();
 
   if(egraph.po_in(first).size() > 0)
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_in(first).begin();
       next_it!=egraph.po_in(first).end();
       ++next_it)
@@ -511,7 +511,7 @@ void const_graph_visitort::CT_not_powr(const edget& edge,
     }
 
   if(egraph.po_out(second).size() > 0)
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(second).begin();
       next_it!=egraph.po_out(second).end();
       ++next_it)