use event_idt for graph nodes

Author: Daniel Kroening

src/goto-instrument/wmm/cycle_collection.cpp

@@ -45,7 +45,7 @@ void event_grapht::graph_explorert::filter_thin_air(
   }
 
 #ifdef DEBUG
-  for(std::set<unsigned>::const_iterator it=thin_air_events.begin();
+  for(std::set<event_idt>::const_iterator it=thin_air_events.begin();
     it!=thin_air_events.end();
     ++it)
     egraph.message.debug()<<egraph[*it]<<";";
@@ -71,10 +71,10 @@ void event_grapht::graph_explorert::collect_cycles(
   memory_modelt model)
 {
   /* all the events initially unmarked */
-  for(unsigned i = 0; i<egraph.size(); i++)
+  for(std::size_t i = 0; i<egraph.size(); i++)
     mark[i] = false;
 
-  std::list<unsigned>* order=0;
+  std::list<event_idt>* order=0;
   /* on Power, rfe pairs are also potentially unsafe */
   switch(model)
   {
@@ -100,17 +100,19 @@ void event_grapht::graph_explorert::collect_cycles(
   if(order->empty())
     return;
 
-  for(std::list<unsigned>::const_iterator st_it=order->begin();
-    st_it!=order->end(); ++st_it)
+  for(std::list<event_idt>::const_iterator
+      st_it=order->begin();
+      st_it!=order->end();
+      ++st_it)
   {
-    unsigned source=*st_it;
+    event_idt source=*st_it;
     egraph.message.debug() << "explore " << egraph[source].id << messaget::eom;
     backtrack(set_of_cycles, source, source,
       false, max_po_trans, false, false, false, "", model);
 
     while(!marked_stack.empty())
     {
-      unsigned up=marked_stack.top();
+      event_idt up=marked_stack.top();
       mark[up]=false;
       marked_stack.pop();
     }
@@ -136,17 +138,17 @@ Function: event_grapht::graph_explorert::extract_cycle
 \*******************************************************************/
 
 event_grapht::critical_cyclet event_grapht::graph_explorert::extract_cycle(
-  unsigned vertex,
-  unsigned source,
+  event_idt vertex,
+  event_idt source,
   unsigned number)
 {
   critical_cyclet new_cycle(egraph, number);
   bool incycle=false;
-  std::stack<unsigned> stack(point_stack);
+  std::stack<event_idt> stack(point_stack);
 
   while(!stack.empty())
   {
-    unsigned current_vertex=stack.top();
+    event_idt current_vertex=stack.top();
     stack.pop();
 
     egraph.message.debug() << "extract: " << egraph[current_vertex].get_operation()
@@ -186,22 +188,22 @@ Function: event_grapht::graph_explorert::backtrack
 
 bool event_grapht::graph_explorert::backtrack(
   std::set<critical_cyclet> &set_of_cycles,
-  unsigned source,
-  unsigned vertex,
+  event_idt source,
+  event_idt vertex,
   bool unsafe_met, /* unsafe pair for the model met in the visited path */
-  unsigned po_trans, /* po-transition skips still allowed */
+  event_idt po_trans, /* po-transition skips still allowed */
   bool same_var_pair, /* in a thread, tells if we already met one rfi wsi fri */
   bool lwfence_met, /* if we try to skip a lwsync (only valid for lwsyncWR) */
   bool has_to_be_unsafe,
   irep_idt var_to_avoid,
   memory_modelt model)
 {
 #ifdef DEBUG
-  for(unsigned i=0; i<80; egraph.message.debug() << "-", ++i);
+  for(std::size_t i=0; i<80; egraph.message.debug() << "-", ++i);
   egraph.message.debug() << messaget::eom;
   egraph.message.debug() << "marked size:" << marked_stack.size()
     << messaget::eom;
-  std::stack<unsigned> tmp;
+  std::stack<event_idt> tmp;
   while(!point_stack.empty())
   {
     egraph.message.debug() << point_stack.top() << " | ";
@@ -286,9 +288,9 @@ bool event_grapht::graph_explorert::backtrack(
          re-order also the two writes, which is not permitted on TSO. */
       if(has_to_be_unsafe && point_stack.size() >= 2)
       {
-        const unsigned previous = point_stack.top();
+        const event_idt previous = point_stack.top();
         point_stack.pop();
-        const unsigned preprevious = point_stack.top();
+        const event_idt preprevious = point_stack.top();
         point_stack.push(previous);
         if(!egraph[preprevious].unsafe_pair(this_vertex,model)
           && !(this_vertex.operation==abstract_eventt::Fence
@@ -397,7 +399,7 @@ bool event_grapht::graph_explorert::backtrack(
         w_it=egraph.po_out(vertex).begin();
         w_it!=egraph.po_out(vertex).end(); w_it++)
       {
-        const unsigned w = w_it->first;
+        const event_idt w = w_it->first;
         if(w == source && point_stack.size()>=4
           && (unsafe_met_updated
             || this_vertex.unsafe_pair(egraph[source],model)) )
@@ -440,7 +442,7 @@ bool event_grapht::graph_explorert::backtrack(
       w_it=egraph.com_out(vertex).begin();
       w_it!=egraph.com_out(vertex).end(); w_it++)
     {
-      const unsigned w = w_it->first;
+      const event_idt w = w_it->first;
       if(w < source)
         egraph.remove_com_edge(vertex,w);
       else if(w == source && point_stack.size()>=4
@@ -481,7 +483,7 @@ bool event_grapht::graph_explorert::backtrack(
     {
       while(!marked_stack.empty() && marked_stack.top()!=vertex)
       {
-        unsigned up = marked_stack.top();
+        event_idt up = marked_stack.top();
         marked_stack.pop();
         mark[up] = false;
       }
@@ -526,7 +528,7 @@ bool event_grapht::graph_explorert::backtrack(
   {
     skip_tracked.insert(vertex);
 
-    std::stack<unsigned> tmp;
+    std::stack<event_idt> tmp;
 
     while(marked_stack.size()>0 && marked_stack.top()!=vertex)
     {
@@ -572,7 +574,7 @@ bool event_grapht::graph_explorert::backtrack(
       egraph.po_out(vertex).begin();
       w_it!=egraph.po_out(vertex).end(); w_it++)
     {
-      const unsigned w = w_it->first;
+      const event_idt w = w_it->first;
       f |= backtrack(set_of_cycles, source, w,
         unsafe_met/*_updated*/, (po_trans==0?0:po_trans-1),
         same_var_pair/*_updated*/, is_lwfence, has_to_be_unsafe, avoid_at_the_end,
@@ -583,7 +585,7 @@ bool event_grapht::graph_explorert::backtrack(
     {
       while(!marked_stack.empty() && marked_stack.top()!=vertex)
       {
-        unsigned up = marked_stack.top();
+        event_idt up = marked_stack.top();
         marked_stack.pop();
         mark[up] = false;
       }

src/goto-instrument/wmm/instrumenter_strategies.cpp

@@ -62,7 +62,7 @@ void instrumentert::instrument_with_strategy(instrumentation_strategyt strategy)
   }
   else if(num_sccs!=0)
   {
-    for(unsigned i=0; i<num_sccs; ++i)
+    for(std::size_t i=0; i<num_sccs; ++i)
     {
       switch(strategy)
       {
@@ -319,11 +319,11 @@ void inline instrumentert::instrument_minimum_interference_inserter(
 
   /* sets the variables and coefficients */
   glp_add_cols(lp, edges.size());
-  unsigned i=0;
+  std::size_t i=0;
   for(std::set<event_grapht::critical_cyclet::delayt>::iterator
-    e_i=edges.begin();
-    e_i!=edges.end();
-    ++e_i)
+      e_i=edges.begin();
+      e_i!=edges.end();
+      ++e_i)
   {
     ++i;
     std::string name="e_"+std::to_string(i);
@@ -347,7 +347,7 @@ void inline instrumentert::instrument_minimum_interference_inserter(
     glp_set_row_bnds(lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/
   }
 
-  const unsigned mat_size=set_of_cycles.size()*edges.size();
+  const std::size_t mat_size=set_of_cycles.size()*edges.size();
   message.debug() << "size of the system: " << mat_size
     << messaget::eom;
   int* imat=(int*)malloc(sizeof(int)*(mat_size+1));
@@ -356,8 +356,8 @@ void inline instrumentert::instrument_minimum_interference_inserter(
 
   /* fills the constraints coeff */
   /* tables read from 1 in glpk -- first row/column ignored */
-  unsigned col=1;
-  unsigned row=1;
+  std::size_t col=1;
+  std::size_t row=1;
   i=1;
   for(std::set<event_grapht::critical_cyclet::delayt>::iterator
     e_i=edges.begin();
@@ -442,7 +442,7 @@ Function: instrumentert::instrument_my_events_inserter
 
 void inline instrumentert::instrument_my_events_inserter(
   const std::set<event_grapht::critical_cyclet>& set,
-  const std::set<unsigned>& my_events)
+  const std::set<event_idt>& my_events)
 {
   for(std::set<event_grapht::critical_cyclet>::const_iterator
     it=set.begin();
@@ -483,7 +483,8 @@ Function: instrumentert::instrument_my_events
 
 \*******************************************************************/
 
-void instrumentert::instrument_my_events(const std::set<unsigned>& my_events)
+void instrumentert::instrument_my_events(
+  const std::set<event_idt>& my_events)
 {
   var_to_instr.clear();
   id2loc.clear();
@@ -493,7 +494,7 @@ void instrumentert::instrument_my_events(const std::set<unsigned>& my_events)
     instrument_my_events_inserter(set_of_cycles, my_events);
   else if(num_sccs!=0)
   {
-    for(unsigned i=0; i<num_sccs; ++i)
+    for(std::size_t i=0; i<num_sccs; ++i)
       instrument_my_events_inserter(set_of_cycles_per_SCC[i], my_events);
   }
   else
@@ -512,18 +513,18 @@ Function: extract_my_events
 
 \*******************************************************************/
 
-std::set<unsigned> instrumentert::extract_my_events()
+std::set<event_idt> instrumentert::extract_my_events()
 {
   std::ifstream file;
   file.open("inst.evt");
-  std::set<unsigned> this_set;
+  std::set<event_idt> this_set;
 
-  unsigned size;
+  std::size_t size;
   file >> size;
 
-  unsigned tmp;
+  std::size_t tmp;
 
-  for(unsigned i=0; i<size; i++)
+  for(std::size_t i=0; i<size; i++)
   {
     file>>tmp;
     this_set.insert(tmp);

src/goto-instrument/wmm/weak_memory.cpp

@@ -220,7 +220,7 @@ void weak_memory(
   // collects instructions to instrument, depending on the strategy selected
   if(event_strategy == my_events)
   {
-    const std::set<unsigned> events_set = instrumentert::extract_my_events();
+    const std::set<event_idt> events_set = instrumentert::extract_my_events();
     instrumenter.instrument_my_events(events_set);
   }
   else