Merge pull request #5784 from tautschnig/forall-rw_set

Remove forall_rw_set_{r,w}_entries

Author: tautschnig

.clang-format

@@ -30,8 +30,6 @@ DerivePointerAlignment: 'false'
 DisableFormat: 'false'
 ExperimentalAutoDetectBinPacking: 'false'
 ForEachMacros: [
-  'forall_rw_set_r_entries',
-  'forall_rw_set_w_entries',
   'forall_goto_functions',
   'Forall_goto_functions',
   'forall_goto_program_instructions',

src/goto-instrument/interrupt.cpp

@@ -24,9 +24,9 @@ static bool potential_race_on_read(
   const rw_set_baset &isr_rw_set)
 {
   // R/W race?
-  forall_rw_set_r_entries(e_it, code_rw_set)
+  for(const auto &r_entry : code_rw_set.r_entries)
   {
-    if(isr_rw_set.has_w_entry(e_it->first))
+    if(isr_rw_set.has_w_entry(r_entry.first))
       return true;
   }
 
@@ -38,12 +38,12 @@ static bool potential_race_on_write(
   const rw_set_baset &isr_rw_set)
 {
   // W/R or W/W?
-  forall_rw_set_w_entries(e_it, code_rw_set)
+  for(const auto &w_entry : code_rw_set.w_entries)
   {
-    if(isr_rw_set.has_r_entry(e_it->first))
+    if(isr_rw_set.has_r_entry(w_entry.first))
       return true;
 
-    if(isr_rw_set.has_w_entry(e_it->first))
+    if(isr_rw_set.has_w_entry(w_entry.first))
       return true;
   }
 

src/goto-instrument/race_check.cpp

@@ -193,16 +193,16 @@ static void race_check(
       i_it++;
 
       // now add assignments for what is written -- set
-      forall_rw_set_w_entries(e_it, rw_set)
+      for(const auto &w_entry : rw_set.w_entries)
       {
-        if(!is_shared(ns, e_it->second.symbol_expr))
+        if(!is_shared(ns, w_entry.second.symbol_expr))
           continue;
 
         goto_programt::targett t = goto_program.insert_before(
           i_it,
           goto_programt::make_assignment(
-            w_guards.get_w_guard_expr(e_it->second),
-            e_it->second.guard,
+            w_guards.get_w_guard_expr(w_entry.second),
+            w_entry.second.guard,
             original_instruction.source_location));
         i_it=++t;
       }
@@ -215,46 +215,46 @@ static void race_check(
       }
 
       // now add assignments for what is written -- reset
-      forall_rw_set_w_entries(e_it, rw_set)
+      for(const auto &w_entry : rw_set.w_entries)
       {
-        if(!is_shared(ns, e_it->second.symbol_expr))
+        if(!is_shared(ns, w_entry.second.symbol_expr))
           continue;
 
         goto_programt::targett t = goto_program.insert_before(
           i_it,
           goto_programt::make_assignment(
-            w_guards.get_w_guard_expr(e_it->second),
+            w_guards.get_w_guard_expr(w_entry.second),
             false_exprt(),
             original_instruction.source_location));
         i_it = std::next(t);
       }
 
       // now add assertions for what is read and written
-      forall_rw_set_r_entries(e_it, rw_set)
+      for(const auto &r_entry : rw_set.r_entries)
       {
-        if(!is_shared(ns, e_it->second.symbol_expr))
+        if(!is_shared(ns, r_entry.second.symbol_expr))
           continue;
 
         goto_programt::targett t = goto_program.insert_before(
           i_it,
           goto_programt::make_assertion(
-            w_guards.get_assertion(e_it->second),
+            w_guards.get_assertion(r_entry.second),
             original_instruction.source_location));
-        t->source_location.set_comment(comment(e_it->second, false));
+        t->source_location.set_comment(comment(r_entry.second, false));
         i_it=++t;
       }
 
-      forall_rw_set_w_entries(e_it, rw_set)
+      for(const auto &w_entry : rw_set.w_entries)
       {
-        if(!is_shared(ns, e_it->second.symbol_expr))
+        if(!is_shared(ns, w_entry.second.symbol_expr))
           continue;
 
         goto_programt::targett t = goto_program.insert_before(
           i_it,
           goto_programt::make_assertion(
-            w_guards.get_assertion(e_it->second),
+            w_guards.get_assertion(w_entry.second),
             original_instruction.source_location));
-        t->source_location.set_comment(comment(e_it->second, true));
+        t->source_location.set_comment(comment(w_entry.second, true));
         i_it=++t;
       }
 

src/goto-instrument/rw_set.h

@@ -107,14 +107,6 @@ inline std::ostream &operator<<(
   return out;
 }
 
-#define forall_rw_set_r_entries(it, rw_set) \
-  for(rw_set_baset::entriest::const_iterator it=(rw_set).r_entries.begin(); \
-      it!=(rw_set).r_entries.end(); it++)
-
-#define forall_rw_set_w_entries(it, rw_set) \
-  for(rw_set_baset::entriest::const_iterator it=(rw_set).w_entries.begin(); \
-      it!=(rw_set).w_entries.end(); it++)
-
 // a producer of read/write sets
 
 class _rw_set_loct:public rw_set_baset

src/goto-instrument/wmm/goto2graph.cpp

@@ -436,19 +436,19 @@ bool instrumentert::cfg_visitort::contains_shared_array(
     instrumenter.message.debug() << "Writes: "<<rw_set.w_entries.size()
       <<"; Reads:"<<rw_set.r_entries.size() << messaget::eom;
 
-    forall_rw_set_r_entries(r_it, rw_set)
+    for(const auto &r_entry : rw_set.r_entries)
     {
-      const irep_idt var=r_it->second.object;
+      const irep_idt var = r_entry.second.object;
       instrumenter.message.debug() << "Is "<<var<<" an array?"
         << messaget::eom;
       if(id2string(var).find("[]")!=std::string::npos
         && !instrumenter.local(var))
         return true;
     }
 
-    forall_rw_set_w_entries(w_it, rw_set)
+    for(const auto &w_entry : rw_set.w_entries)
     {
-      const irep_idt var=w_it->second.object;
+      const irep_idt var = w_entry.second.object;
       instrumenter.message.debug()<<"Is "<<var<<" an array?"<<messaget::eom;
       if(id2string(var).find("[]")!=std::string::npos
         && !instrumenter.local(var))
@@ -874,13 +874,13 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
     continue; // return;
 #endif
 
-  forall_rw_set_r_entries(r_it, rw_set)
+  for(const auto &r_entry : rw_set.r_entries)
   {
     /* creates Read:
        read is the irep_id of the read in the code;
        new_read_event is the corresponding abstract event;
        new_read_node is the node in the graph */
-    const irep_idt &read=r_it->second.object;
+    const irep_idt &read = r_entry.second.object;
 
     /* skip local variables */
     if(local(read))
@@ -976,13 +976,13 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
   }
 
   /* Write (Wa) */
-  forall_rw_set_w_entries(w_it, rw_set)
+  for(const auto &w_entry : rw_set.w_entries)
   {
     /* creates Write:
        write is the irep_id in the code;
        new_write_event is the corresponding abstract event;
        new_write_node is the node in the graph */
-    const irep_idt &write=w_it->second.object;
+    const irep_idt &write = w_entry.second.object;
 
     instrumenter.message.debug() << "WRITE: " << write << messaget::eom;
 
@@ -1142,30 +1142,34 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
   /* data dependency analysis */
   if(!no_dependencies)
   {
-    forall_rw_set_w_entries(write_it, rw_set)
-      forall_rw_set_r_entries(read_it, rw_set)
+    for(const auto &w_entry : rw_set.w_entries)
+    {
+      for(const auto &r_entry : rw_set.r_entries)
       {
-        const irep_idt &write=write_it->second.object;
-        const irep_idt &read=read_it->second.object;
+        const irep_idt &write = w_entry.second.object;
+        const irep_idt &read = r_entry.second.object;
         instrumenter.message.debug() << "dp: Write:"<<write<<"; Read:"<<read
           << messaget::eom;
         const datat read_p(read, instruction.source_location);
         const datat write_p(write, instruction.source_location);
           data_dp.dp_analysis(read_p, local(read), write_p, local(write));
         }
+    }
     data_dp.dp_merge();
 
-    forall_rw_set_r_entries(read2_it, rw_set)
-      forall_rw_set_r_entries(read_it, rw_set)
+    for(const auto &r_entry : rw_set.r_entries)
+    {
+      for(const auto &r_entry2 : rw_set.r_entries)
       {
-        const irep_idt &read2=read2_it->second.object;
-        const irep_idt &read=read_it->second.object;
+        const irep_idt &read2 = r_entry2.second.object;
+        const irep_idt &read = r_entry.second.object;
         if(read2==read)
           continue;
         const datat read_p(read, instruction.source_location);
         const datat read2_p(read2, instruction.source_location);
         data_dp.dp_analysis(read_p, local(read), read2_p, local(read2));
       }
+    }
     data_dp.dp_merge();
   }
 }