rw_set: store function identifier alongside instruction reference

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. rw_set does not yet make use
of this, but will need to once dereferencing is updated to require a function
name.

Author: tautschnig

src/goto-instrument/interrupt.cpp

@@ -19,7 +19,7 @@ Date: September 2011
 #include <analyses/local_may_alias.h>
 #endif
 
-bool potential_race_on_read(
+static bool potential_race_on_read(
   const rw_set_baset &code_rw_set,
   const rw_set_baset &isr_rw_set)
 {
@@ -33,7 +33,7 @@ bool potential_race_on_read(
   return false;
 }
 
-bool potential_race_on_write(
+static bool potential_race_on_write(
   const rw_set_baset &code_rw_set,
   const rw_set_baset &isr_rw_set)
 {
@@ -50,9 +50,10 @@ bool potential_race_on_write(
   return false;
 }
 
-void interrupt(
+static void interrupt(
   value_setst &value_sets,
   const symbol_tablet &symbol_table,
+  const irep_idt &function_id,
 #ifdef LOCAL_MAY
   const goto_functionst::goto_functiont &goto_function,
 #endif
@@ -69,11 +70,16 @@ void interrupt(
 #ifdef LOCAL_MAY
   local_may_aliast local_may(goto_function);
 #endif
-    rw_set_loct rw_set(ns, value_sets, i_it
+  rw_set_loct rw_set(
+    ns,
+    value_sets,
+    function_id,
+    i_it
 #ifdef LOCAL_MAY
-      , local_may
+    ,
+    local_may
 #endif
-    ); // NOLINT(whitespace/parens)
+  ); // NOLINT(whitespace/parens)
 
     // potential race?
     bool race_on_read=potential_race_on_read(rw_set, isr_rw_set);
@@ -143,9 +149,8 @@ void interrupt(
   }
 }
 
-symbol_exprt get_isr(
-  const symbol_tablet &symbol_table,
-  const irep_idt &interrupt_handler)
+static symbol_exprt
+get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
 {
   std::list<symbol_exprt> matches;
 
@@ -197,11 +202,15 @@ void interrupt(
        f_it->first!=goto_functionst::entry_point() &&
        f_it->first!=isr.get_identifier())
       interrupt(
-        value_sets, goto_model.symbol_table,
+        value_sets,
+        goto_model.symbol_table,
+        f_it->first,
 #ifdef LOCAL_MAY
         f_it->second,
 #endif
-        f_it->second.body, isr, isr_rw_set);
+        f_it->second.body,
+        isr,
+        isr_rw_set);
 
   goto_model.goto_functions.update();
 }

src/goto-instrument/mmio.cpp

@@ -21,9 +21,10 @@ Date: September 2011
 #include <analyses/local_may_alias.h>
 #endif
 
-void mmio(
+static void mmio(
   value_setst &value_sets,
   const symbol_tablet &symbol_table,
+  const irep_idt &function_id,
 #ifdef LOCAL_MAY
   const goto_functionst::goto_functiont &goto_function,
 #endif
@@ -41,9 +42,14 @@ void mmio(
 
     if(instruction.is_assign())
     {
-      rw_set_loct rw_set(ns, value_sets, i_it
+      rw_set_loct rw_set(
+        ns,
+        value_sets,
+        function_id,
+        i_it
 #ifdef LOCAL_MAY
-        , local_may
+        ,
+        local_may
 #endif
       ); // NOLINT(whitespace/parens)
 
@@ -159,7 +165,10 @@ void mmio(
   Forall_goto_functions(f_it, goto_model.goto_functions)
     if(f_it->first != INITIALIZE_FUNCTION &&
        f_it->first!=goto_functionst::entry_point())
-      mmio(value_sets, goto_model.symbol_table,
+      mmio(
+        value_sets,
+        goto_model.symbol_table,
+        f_it->first,
 #ifdef LOCAL_MAY
         f_it->second,
 #endif

src/goto-instrument/race_check.cpp

@@ -104,7 +104,7 @@ void w_guardst::add_initialization(goto_programt &goto_program) const
   }
 }
 
-std::string comment(const rw_set_baset::entryt &entry, bool write)
+static std::string comment(const rw_set_baset::entryt &entry, bool write)
 {
   std::string result;
   if(write)
@@ -117,9 +117,7 @@ std::string comment(const rw_set_baset::entryt &entry, bool write)
   return result;
 }
 
-bool is_shared(
-  const namespacet &ns,
-  const symbol_exprt &symbol_expr)
+static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
 {
   const irep_idt &identifier=symbol_expr.get_identifier();
 
@@ -137,9 +135,7 @@ bool is_shared(
   return symbol.is_shared();
 }
 
-bool has_shared_entries(
-  const namespacet &ns,
-  const rw_set_baset &rw_set)
+static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
 {
   for(rw_set_baset::entriest::const_iterator
       it=rw_set.r_entries.begin();
@@ -158,12 +154,17 @@ bool has_shared_entries(
   return false;
 }
 
-void race_check(
+// clang-format off
+// clang-format is confused by the L_M_ARG macro and wants to indent the line
+// after
+static void race_check(
   value_setst &value_sets,
   symbol_tablet &symbol_table,
+  const irep_idt &function_id,
   L_M_ARG(const goto_functionst::goto_functiont &goto_function)
   goto_programt &goto_program,
   w_guardst &w_guards)
+// clang-format on
 {
   namespacet ns(symbol_table);
 
@@ -177,7 +178,8 @@ void race_check(
 
     if(instruction.is_assign())
     {
-      rw_set_loct rw_set(ns, value_sets, i_it L_M_LAST_ARG(local_may));
+      rw_set_loct rw_set(
+        ns, value_sets, function_id, i_it L_M_LAST_ARG(local_may));
 
       if(!has_shared_entries(ns, rw_set))
         continue;
@@ -266,6 +268,7 @@ void race_check(
 void race_check(
   value_setst &value_sets,
   symbol_tablet &symbol_table,
+  const irep_idt &function_id,
 #ifdef LOCAL_MAY
   const goto_functionst::goto_functiont &goto_function,
 #endif
@@ -276,8 +279,8 @@ void race_check(
   race_check(
     value_sets,
     symbol_table,
-    L_M_ARG(goto_function)
-    goto_program,
+    function_id,
+    L_M_ARG(goto_function) goto_program,
     w_guards);
 
   w_guards.add_initialization(goto_program);
@@ -296,8 +299,8 @@ void race_check(
       race_check(
         value_sets,
         goto_model.symbol_table,
-        L_M_ARG(f_it->second)
-        f_it->second.body,
+        f_it->first,
+        L_M_ARG(f_it->second) f_it->second.body,
         w_guards);
 
   // get "main"

src/goto-instrument/race_check.h

@@ -20,11 +20,11 @@ Date: February 2006
 void race_check(
   value_setst &,
   class symbol_tablet &,
+  const irep_idt &function_id,
 #ifdef LOCAL_MAY
   const goto_functionst::goto_functiont &goto_function,
 #endif
-  goto_programt &goto_program
-);
+  goto_programt &goto_program);
 
 void race_check(value_setst &, goto_modelt &);
 

src/goto-instrument/rw_set.cpp

@@ -199,10 +199,10 @@ void rw_set_functiont::compute_rec(const exprt &function)
 {
   if(function.id()==ID_symbol)
   {
-    const irep_idt &id=to_symbol_expr(function).get_identifier();
+    const irep_idt &function_id = to_symbol_expr(function).get_identifier();
 
-    goto_functionst::function_mapt::const_iterator f_it=
-      goto_functions.function_map.find(id);
+    goto_functionst::function_mapt::const_iterator f_it =
+      goto_functions.function_map.find(function_id);
 
     if(f_it!=goto_functions.function_map.end())
     {
@@ -220,9 +220,14 @@ void rw_set_functiont::compute_rec(const exprt &function)
 
       forall_goto_program_instructions(i_it, body)
       {
-        *this+=rw_set_loct(ns, value_sets, i_it
+        *this += rw_set_loct(
+          ns,
+          value_sets,
+          function_id,
+          i_it
 #ifdef LOCAL_MAY
-        , local_may
+          ,
+          local_may
 #endif
         ); // NOLINT(whitespace/parens)
       }

src/goto-instrument/rw_set.h

@@ -121,26 +121,31 @@ class _rw_set_loct:public rw_set_baset
   _rw_set_loct(
     const namespacet &_ns,
     value_setst &_value_sets,
+    const irep_idt &_function_id,
     goto_programt::const_targett _target,
-    local_may_aliast &may):
-    rw_set_baset(_ns),
-    value_sets(_value_sets),
-    target(_target),
-    local_may(may)
+    local_may_aliast &may)
+    : rw_set_baset(_ns),
+      value_sets(_value_sets),
+      function_id(_function_id),
+      target(_target),
+      local_may(may)
 #else
   _rw_set_loct(
     const namespacet &_ns,
     value_setst &_value_sets,
-    goto_programt::const_targett _target):
-    rw_set_baset(_ns),
-    value_sets(_value_sets),
-    target(_target)
+    const irep_idt &_function_id,
+    goto_programt::const_targett _target)
+    : rw_set_baset(_ns),
+      value_sets(_value_sets),
+      function_id(_function_id),
+      target(_target)
 #endif
   {
   }
 
 protected:
   value_setst &value_sets;
+  const irep_idt function_id;
   const goto_programt::const_targett target;
 
 #ifdef LOCAL_MAY
@@ -180,15 +185,17 @@ class rw_set_loct:public _rw_set_loct
   rw_set_loct(
     const namespacet &_ns,
     value_setst &_value_sets,
+    const irep_idt &_function_id,
     goto_programt::const_targett _target,
-    local_may_aliast &may):
-    _rw_set_loct(_ns, _value_sets, _target, may)
+    local_may_aliast &may)
+    : _rw_set_loct(_ns, _value_sets, _function_id, _target, may)
 #else
   rw_set_loct(
     const namespacet &_ns,
     value_setst &_value_sets,
-    goto_programt::const_targett _target):
-    _rw_set_loct(_ns, _value_sets, _target)
+    const irep_idt &_function_id,
+    goto_programt::const_targett _target)
+    : _rw_set_loct(_ns, _value_sets, _function_id, _target)
 #endif
   {
     compute();
@@ -239,17 +246,19 @@ class rw_set_with_trackt:public _rw_set_loct
   rw_set_with_trackt(
     const namespacet &_ns,
     value_setst &_value_sets,
+    const irep_idt &_function_id,
     goto_programt::const_targett _target,
-    local_may_aliast &may):
-    _rw_set_loct(_ns, _value_sets, _target, may),
-    dereferencing(false)
+    local_may_aliast &may)
+    : _rw_set_loct(_ns, _value_sets, _function_id, _target, may),
+      dereferencing(false)
 #else
   rw_set_with_trackt(
     const namespacet &_ns,
     value_setst &_value_sets,
-    goto_programt::const_targett _target):
-    _rw_set_loct(_ns, _value_sets, _target),
-    dereferencing(false)
+    const irep_idt &_function_id,
+    goto_programt::const_targett _target)
+    : _rw_set_loct(_ns, _value_sets, _function_id, _target),
+      dereferencing(false)
 #endif
   {
     compute();