Weak-memory-model instrumentation: do not use instructiont::function

We are working towards removing the "function" field from
goto_programt::instructionst::instructiont, and thus need to pass the identifier
of the function whenever it actually is required. Consistently use "function_id"
as that identifier.

Author: tautschnig

src/goto-instrument/wmm/goto2graph.cpp

@@ -145,31 +145,32 @@ unsigned instrumentert::goto2graph_cfg(
 }
 
 void instrumentert::cfg_visitort::visit_cfg_function(
-    value_setst &value_sets,
-    memory_modelt model,
-    bool no_dependencies,
-    loop_strategyt replicate_body,
-    const irep_idt &function,
-    std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)
+  value_setst &value_sets,
+  memory_modelt model,
+  bool no_dependencies,
+  loop_strategyt replicate_body,
+  const irep_idt &function_id,
+  std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)
 {
   /* flow: egraph */
 
-  instrumenter.message.debug() << "visit function "
-                               << function << messaget::eom;
+  instrumenter.message.debug()
+    << "visit function " << function_id << messaget::eom;
 
-  if(function == INITIALIZE_FUNCTION)
+  if(function_id == INITIALIZE_FUNCTION)
   {
     return;
   }
 
 #ifdef LOCAL_MAY
   local_may_aliast local_may(
-    instrumenter.goto_functions.function_map[function]);
+    instrumenter.goto_functions.function_map[function_id]);
 #endif
 
   /* goes through the function */
-  Forall_goto_program_instructions(i_it,
-    instrumenter.goto_functions.function_map[function].body)
+  goto_programt &goto_program =
+    instrumenter.goto_functions.function_map[function_id].body;
+  Forall_goto_program_instructions(i_it, goto_program)
   {
     goto_programt::instructiont &instruction=*i_it;
 
@@ -243,17 +244,22 @@ void instrumentert::cfg_visitort::visit_cfg_function(
     }
     else if(instruction.is_goto())
     {
-      visit_cfg_goto(i_it, replicate_body, value_sets
+      visit_cfg_goto(
+        goto_program,
+        i_it,
+        replicate_body,
+        value_sets
 #ifdef LOCAL_MAY
-        , local_may
+        ,
+        local_may
 #endif
       ); // NOLINT(whitespace/parens)
     }
 #ifdef CONTEXT_INSENSITIVE
     else if(instruction.is_return())
     {
       visit_cfg_propagate(i_it);
-      add_all_pos(it, out_nodes[function], in_pos[i_it]);
+      add_all_pos(it, out_nodes[function_id], in_pos[i_it]);
     }
 #endif
     else
@@ -267,15 +273,16 @@ void instrumentert::cfg_visitort::visit_cfg_function(
   egraph.map_data_dp.insert(new_dp);
   data_dp.print(instrumenter.message);
 
-  if(instrumenter.goto_functions.function_map[function]
-     .body.instructions.empty())
+  if(instrumenter.goto_functions.function_map[function_id]
+       .body.instructions.empty())
   {
     /* empty set of ending edges */
   }
   else
   {
-    goto_programt::instructionst::iterator it=instrumenter
-      .goto_functions.function_map[function].body.instructions.end();
+    goto_programt::instructionst::iterator it =
+      instrumenter.goto_functions.function_map[function_id]
+        .body.instructions.end();
     --it;
     ending_vertex=in_pos[it];
   }
@@ -445,11 +452,13 @@ bool instrumentert::cfg_visitort::contains_shared_array(
 
 /// strategy: fwd/bwd alternation
 void inline instrumentert::cfg_visitort::visit_cfg_body(
+  const goto_programt &goto_program,
   goto_programt::const_targett i_it,
   loop_strategyt replicate_body,
   value_setst &value_sets
 #ifdef LOCAL_MAY
-  , local_may_aliast &local_may
+  ,
+  local_may_aliast &local_may
 #endif
 )
 {
@@ -482,29 +491,27 @@ void inline instrumentert::cfg_visitort::visit_cfg_body(
       }
 
       if(duplicate_this)
-        visit_cfg_duplicate(target, i_it);
+        visit_cfg_duplicate(goto_program, target, i_it);
       else
         visit_cfg_backedge(target, i_it);
     }
   }
 }
 
 void inline instrumentert::cfg_visitort::visit_cfg_duplicate(
+  const goto_programt &goto_program,
   goto_programt::const_targett targ,
   goto_programt::const_targett i_it)
 {
   instrumenter.message.status() << "Duplication..." << messaget::eom;
-  const goto_functionst::goto_functiont &fun=
-    instrumenter.goto_functions.function_map[i_it->function];
 
   bool found_pos=false;
   goto_programt::const_targett new_targ=targ;
 
   if(in_pos[targ].empty())
   {
     /* tries to find the next node after the back edge */
-    for(; new_targ!=fun.body.instructions.end();
-      ++new_targ)
+    for(; new_targ != goto_program.instructions.end(); ++new_targ)
     {
       if(in_pos.find(new_targ)!=in_pos.end() && !in_pos[new_targ].empty())
       {
@@ -620,11 +627,13 @@ void inline instrumentert::cfg_visitort::visit_cfg_backedge(
 }
 
 void instrumentert::cfg_visitort::visit_cfg_goto(
+  const goto_programt &goto_program,
   goto_programt::instructionst::iterator i_it,
   loop_strategyt replicate_body,
   value_setst &value_sets
 #ifdef LOCAL_MAY
-  , local_may_aliast &local_may
+  ,
+  local_may_aliast &local_may
 #endif
 )
 {
@@ -640,9 +649,14 @@ void instrumentert::cfg_visitort::visit_cfg_goto(
   if(instruction.is_backwards_goto())
   {
     instrumenter.message.debug() << "backward goto" << messaget::eom;
-    visit_cfg_body(i_it, replicate_body, value_sets
+    visit_cfg_body(
+      goto_program,
+      i_it,
+      replicate_body,
+      value_sets
 #ifdef LOCAL_MAY
-    , local_may
+      ,
+      local_may
 #endif
     ); // NOLINT(whitespace/parens)
   }

src/goto-instrument/wmm/goto2graph.h

@@ -114,16 +114,20 @@ class instrumentert
     void visit_cfg_thread() const;
     void visit_cfg_propagate(goto_programt::instructionst::iterator i_it);
     void visit_cfg_body(
+      const goto_programt &goto_program,
       goto_programt::const_targett i_it,
       loop_strategyt replicate_body,
       value_setst &value_sets
-      #ifdef LOCAL_MAY
-      , local_may_aliast &local_may
-      #endif
+#ifdef LOCAL_MAY
+      ,
+      local_may_aliast &local_may
+#endif
     ); // deprecated  NOLINT(whitespace/parens)
     void inline visit_cfg_backedge(goto_programt::const_targett targ,
       goto_programt::const_targett i_it);
-    void inline visit_cfg_duplicate(goto_programt::const_targett targ,
+    void inline visit_cfg_duplicate(
+      const goto_programt &goto_program,
+      goto_programt::const_targett targ,
       goto_programt::const_targett i_it);
     void visit_cfg_assign(
       value_setst &value_sets,
@@ -144,14 +148,16 @@ class instrumentert
       bool no_dependenciess,
       loop_strategyt duplicate_body);
     void visit_cfg_goto(
+      const goto_programt &goto_program,
       goto_programt::instructionst::iterator i_it,
       /* forces the duplication of all the loops, with array or not
          otherwise, duplication of loops with array accesses only */
       loop_strategyt replicate_body,
       value_setst &value_sets
-      #ifdef LOCAL_MAY
-      , local_may_aliast &local_may
-      #endif
+#ifdef LOCAL_MAY
+      ,
+      local_may_aliast &local_may
+#endif
     ); // NOLINT(whitespace/parens)
     void visit_cfg_reference_function(irep_idt id_function);
 
@@ -224,34 +230,39 @@ class instrumentert
       coming_from = 0;
     }
 
-    void inline enter_function(const irep_idt &function)
+    void inline enter_function(const irep_idt &function_id)
     {
-      if(functions_met.find(function)!=functions_met.end())
+      if(functions_met.find(function_id) != functions_met.end())
         throw "sorry, doesn't handle recursive function for the moment";
-      functions_met.insert(function);
+      functions_met.insert(function_id);
     }
 
-    void inline leave_function(const irep_idt &function)
+    void inline leave_function(const irep_idt &function_id)
     {
-      functions_met.erase(function);
+      functions_met.erase(function_id);
     }
 
     void inline visit_cfg(
       value_setst &value_sets,
       memory_modelt model,
       bool no_dependencies,
       loop_strategyt duplicate_body,
-      const irep_idt &function)
+      const irep_idt &function_id)
     {
       /* ignore recursive calls -- underapproximation */
       try
       {
         /* forbids recursive function */
-        enter_function(function);
+        enter_function(function_id);
         std::set<nodet> end_out;
-        visit_cfg_function(value_sets, model, no_dependencies, duplicate_body,
-          function, end_out);
-        leave_function(function);
+        visit_cfg_function(
+          value_sets,
+          model,
+          no_dependencies,
+          duplicate_body,
+          function_id,
+          end_out);
+        leave_function(function_id);
       }
       catch(const std::string &s)
       {
@@ -265,14 +276,14 @@ class instrumentert
     /// \param no_dependencies: Option to disable dependency analysis
     /// \param duplicate_body: Control which loop body segments should
     ///   be duplicated
-    /// \param function: Function to analyse
+    /// \param function_id: Function to analyse
     /// \param ending_vertex: Outcoming edges
     virtual void visit_cfg_function(
       value_setst &value_sets,
       memory_modelt model,
       bool no_dependencies,
       loop_strategyt duplicate_body,
-      const irep_idt &function,
+      const irep_idt &function_id,
       std::set<nodet> &ending_vertex);
 
     bool inline local(const irep_idt &i);

src/goto-instrument/wmm/shared_buffers.cpp

@@ -447,6 +447,7 @@ void shared_bufferst::det_flush(
 
 /// instruments read
 void shared_bufferst::nondet_flush(
+  const irep_idt &function_id,
   goto_programt &goto_program,
   goto_programt::targett &target,
   const source_locationt &source_location,
@@ -463,8 +464,8 @@ void shared_bufferst::nondet_flush(
   const varst &vars=(*this)(object);
 
   // Non deterministic choice
-  irep_idt choice0=choice(target->function, "0");
-  irep_idt choice2=choice(target->function, "2"); // delays the write flush
+  irep_idt choice0 = choice(function_id, "0");
+  irep_idt choice2 = choice(function_id, "2"); // delays the write flush
 
   const symbol_exprt choice0_expr=symbol_exprt(choice0, bool_typet());
   const symbol_exprt delay_expr=symbol_exprt(choice2, bool_typet());
@@ -690,7 +691,7 @@ void shared_bufferst::nondet_flush(
     // a thread can read the other threads' buffers
 
     // One extra non-deterministic choice needed
-    irep_idt choice1=choice(target->function, "1");
+    irep_idt choice1 = choice(function_id, "1");
     const symbol_exprt choice1_expr=symbol_exprt(choice1, bool_typet());
 
     // throw Boolean dice
@@ -1056,19 +1057,19 @@ void shared_bufferst::affected_by_delay(
 /// instruments the program for the pairs detected through the CFG
 void shared_bufferst::cfg_visitort::weak_memory(
   value_setst &value_sets,
-  const irep_idt &function,
+  const irep_idt &function_id,
   memory_modelt model)
 {
-  shared_buffers.message.debug() << "visit function "<< function
-                                 << messaget::eom;
-  if(function == INITIALIZE_FUNCTION)
+  shared_buffers.message.debug()
+    << "visit function " << function_id << messaget::eom;
+  if(function_id == INITIALIZE_FUNCTION)
     return;
 
   namespacet ns(symbol_table);
-  goto_programt &goto_program=goto_functions.function_map[function].body;
+  goto_programt &goto_program = goto_functions.function_map[function_id].body;
 
 #ifdef LOCAL_MAY
-  local_may_aliast local_may(goto_functions.function_map[function]);
+  local_may_aliast local_may(goto_functions.function_map[function_id]);
 #endif
 
   Forall_goto_program_instructions(i_it, goto_program)
@@ -1127,9 +1128,13 @@ void shared_bufferst::cfg_visitort::weak_memory(
 
           if(shared_buffers.is_buffered(ns, e_it->second.symbol_expr, false))
             shared_buffers.nondet_flush(
-              goto_program, i_it, source_location, e_it->second.object,
+              function_id,
+              goto_program,
+              i_it,
+              source_location,
+              e_it->second.object,
               current_thread,
-              (model==TSO || model==PSO || model==RMO));
+              (model == TSO || model == PSO || model == RMO));
         }
 
         // Now perform the write(s).
@@ -1184,8 +1189,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
                     vars.read_delayed, bool_typet());
 
                   // One extra non-deterministic choice needed
-                  irep_idt choice1=shared_buffers.choice(
-                    instruction.function, "1");
+                  irep_idt choice1 = shared_buffers.choice(function_id, "1");
                   const symbol_exprt choice1_expr=symbol_exprt(choice1,
                     bool_typet());
                   const exprt nondet_bool_expr =

src/goto-instrument/wmm/shared_buffers.h

@@ -117,6 +117,7 @@ class shared_bufferst
     const unsigned current_thread);
 
   void nondet_flush(
+    const irep_idt &function_id,
     goto_programt &goto_program,
     goto_programt::targett &t,
     const source_locationt &source_location,
@@ -156,9 +157,9 @@ class shared_bufferst
     return true;
   }
 
-  irep_idt choice(const irep_idt &function, const std::string &suffix)
+  irep_idt choice(const irep_idt &function_id, const std::string &suffix)
   {
-    const auto maybe_symbol=symbol_table.lookup(function);
+    const auto maybe_symbol = symbol_table.lookup(function_id);
     const std::string function_base_name =
       maybe_symbol
         ? id2string(maybe_symbol->base_name)
@@ -213,10 +214,10 @@ class shared_bufferst
       max_thread = 0;
     }
 
-  void weak_memory(
-    value_setst &value_sets,
-    const irep_idt &function,
-    memory_modelt model);
+    void weak_memory(
+      value_setst &value_sets,
+      const irep_idt &function_id,
+      memory_modelt model);
   };
 
 protected: