Merge pull request #1843 from peterschrammel/instructions-function

Set function member in instructions

Author: smowton

src/analyses/dependence_graph.cpp

@@ -76,7 +76,7 @@ void dep_graph_domaint::control_dependencies(
      from->is_assume())
     control_deps.insert(from);
 
-  const irep_idt id=goto_programt::get_function_id(from);
+  const irep_idt id=from->function;
   const cfg_post_dominatorst &pd=dep_graph.cfg_post_dominators().at(id);
 
   // check all candidates for M

src/goto-instrument/full_slicer.cpp

@@ -150,7 +150,7 @@ void full_slicert::add_jumps(
       continue;
     }
 
-    const irep_idt id=goto_programt::get_function_id(j.PC);
+    const irep_idt id=j.PC->function;
     const cfg_post_dominatorst &pd=post_dominators.at(id);
 
     cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e=
@@ -184,7 +184,7 @@ void full_slicert::add_jumps(
 
         if(cfg[entry->second].node_required)
         {
-          const irep_idt id2=goto_programt::get_function_id(*d_it);
+          const irep_idt id2=(*d_it)->function;
           INVARIANT(id==id2,
                     "goto/jump expected to be within a single function");
 

src/goto-programs/goto_convert_functions.cpp

@@ -213,9 +213,8 @@ void goto_convert_functionst::convert_function(
   // add "end of function"
   f.body.destructive_append(tmp_end_function);
 
-  // do function tags
-  Forall_goto_program_instructions(i_it, f.body)
-    i_it->function=identifier;
+  // do function tags (they are empty at this point)
+  f.update_instructions_function(identifier);
 
   f.body.update();
 

src/goto-programs/goto_functions_template.h

@@ -62,6 +62,14 @@ class goto_function_templatet
     parameter_identifiers.clear();
   }
 
+  /// update the function member in each instruction
+  /// \param function_id: the `function_id` used for assigning empty function
+  ///   members
+  void update_instructions_function(const irep_idt &function_id)
+  {
+    body.update_instructions_function(function_id);
+  }
+
   void swap(goto_function_templatet &other)
   {
     body.swap(other.body);
@@ -149,12 +157,23 @@ class goto_functions_templatet
   void compute_target_numbers();
   void compute_incoming_edges();
 
+  /// update the function member in each instruction by setting it to
+  /// the goto function's identifier
+  void update_instructions_function()
+  {
+    for(auto &func : function_map)
+    {
+      func.second.update_instructions_function(func.first);
+    }
+  }
+
   void update()
   {
     compute_incoming_edges();
     compute_target_numbers();
     compute_location_numbers();
     compute_loop_numbers();
+    update_instructions_function();
   }
 
   static inline irep_idt entry_point()

src/goto-programs/goto_model.h

@@ -103,6 +103,13 @@ class goto_model_functiont
     goto_functions.compute_location_numbers(goto_function.body);
   }
 
+  /// Updates the empty function member of each instruction by setting them
+  /// to `function_id`
+  void update_instructions_function()
+  {
+    goto_function.update_instructions_function(function_id);
+  }
+
   /// Get symbol table
   /// \return journalling symbol table that (a) wraps the global symbol table,
   ///   and (b) has recorded all symbol mutations (insertions, updates and

src/goto-programs/goto_program_template.h

@@ -386,21 +386,12 @@ class goto_program_templatet
     return t;
   }
 
-  static const irep_idt get_function_id(
-    const_targett l)
-  {
-    while(!l->is_end_function())
-      ++l;
-
-    return l->function;
-  }
-
   static const irep_idt get_function_id(
     const goto_program_templatet<codeT, guardT> &p)
   {
-    assert(!p.empty());
+    PRECONDITION(!p.empty());
 
-    return get_function_id(--p.instructions.end());
+    return p.instructions.back().function;
   }
 
   template <typename Target>
@@ -521,6 +512,22 @@ class goto_program_templatet
     }
   }
 
+  /// Sets the `function` member of each instruction if not yet set
+  /// Note that a goto program need not be a goto function and therefore,
+  /// we cannot do this in update(), but only at the level of
+  /// of goto_functionst where goto programs are guaranteed to be
+  /// named functions.
+  void update_instructions_function(const irep_idt &function_id)
+  {
+    for(auto &instruction : instructions)
+    {
+      if(instruction.function.empty())
+      {
+        instruction.function = function_id;
+      }
+    }
+  }
+
   /// Compute location numbers
   void compute_location_numbers()
   {

src/goto-programs/remove_returns.cpp

@@ -244,8 +244,7 @@ void remove_returnst::operator()(
   if(goto_function.body.empty())
     return;
 
-  replace_returns(
-    goto_programt::get_function_id(goto_function.body), goto_function);
+  replace_returns(model_function.get_function_id(), goto_function);
   do_function_calls(function_is_stub, goto_function.body);
 }
 

src/jbmc/jbmc_parse_options.cpp

@@ -721,6 +721,9 @@ void jbmc_parse_optionst::process_goto_function(
         symbol_table.lookup_ref(new_symbol_name),
         symbol_table);
     }
+
+    // update the function member in each instruction
+    function.update_instructions_function();
   }
 
   catch(const char *e)