remove goto_programt::instructiont::function member

kroening · kroening · commit d1eae28986ed · 2018-10-09T11:21:10.000+01:00
diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp
@@ -109,7 +109,7 @@ bool symex_bmct::get_unwind(
   const goto_symex_statet::call_stackt &context,
   unsigned unwind)
 {
-  const irep_idt id=goto_programt::loop_id(*source.pc);
+  const irep_idt id = goto_programt::loop_id(source.function, *source.pc);
 
   tvt abort_unwind_decision;
   unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
diff --git a/src/goto-instrument/branch.cpp b/src/goto-instrument/branch.cpp
@@ -53,15 +53,13 @@ void branch(
         goto_programt::targett t1=body.insert_after(i_it);
         t1->make_function_call(
           function_to_call(goto_model.symbol_table, id, "taken"));
-        t1->function=f_it->first;
 
         goto_programt::targett t2=body.insert_after(t1);
         t2->make_goto(i_it->get_target());
 
         goto_programt::targett t3=body.insert_after(t2);
         t3->make_function_call(
           function_to_call(goto_model.symbol_table, id, "not-taken"));
-        t3->function=f_it->first;
         i_it->targets.clear();
         i_it->targets.push_back(t3);
       }
diff --git a/src/goto-instrument/cover_instrument.h b/src/goto-instrument/cover_instrument.h
@@ -71,7 +71,6 @@ class cover_instrumenter_baset
     t->source_location.set(ID_coverage_criterion, coverage_criterion);
     t->source_location.set_property_class(property_class);
     t->source_location.set_function(function);
-    t->function = function;
   }
 
   bool is_non_cover_assertion(goto_programt::const_targett t) const
diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp
@@ -668,7 +668,6 @@ void cover_mcdc_instrumentert::instrument(
       i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
       i_it->source_location.set_property_class(property_class);
       i_it->source_location.set_function(function);
-      i_it->function = function;
 
       std::string comment_f = description + " `" + p_string + "' false";
       goto_program.insert_before_swap(i_it);
@@ -678,7 +677,6 @@ void cover_mcdc_instrumentert::instrument(
       i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
       i_it->source_location.set_property_class(property_class);
       i_it->source_location.set_function(function);
-      i_it->function = function;
     }
 
     std::set<exprt> controlling;
diff --git a/src/goto-programs/generate_function_bodies.cpp b/src/goto-programs/generate_function_bodies.cpp
@@ -71,7 +71,6 @@ class assume_false_generate_function_bodiest : public generate_function_bodiest
     // NOLINTNEXTLINE
     auto add_instruction = [&]() {
       auto instruction = function.body.add_instruction();
-      instruction->function = function_name;
       instruction->source_location = function_symbol.location;
       return instruction;
     };
@@ -94,7 +93,6 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest
     // NOLINTNEXTLINE
     auto add_instruction = [&]() {
       auto instruction = function.body.add_instruction();
-      instruction->function = function_name;
       instruction->source_location = function_symbol.location;
       instruction->source_location.set_function(function_name);
       return instruction;
@@ -125,7 +123,6 @@ class assert_false_then_assume_false_generate_function_bodiest
     // NOLINTNEXTLINE
     auto add_instruction = [&]() {
       auto instruction = function.body.add_instruction();
-      instruction->function = function_name;
       instruction->source_location = function_symbol.location;
       instruction->source_location.set_function(function_name);
       return instruction;
@@ -261,7 +258,6 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
     // NOLINTNEXTLINE
     auto add_instruction = [&]() {
       auto instruction = function.body.add_instruction();
-      instruction->function = function_name;
       instruction->source_location = function_symbol.location;
       return instruction;
     };
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
@@ -204,9 +204,6 @@ void goto_convert_functionst::convert_function(
   // add "end of function"
   f.body.destructive_append(tmp_end_function);
 
-  // do function tags (they are empty at this point)
-  f.update_instructions_function(identifier);
-
   f.body.update();
 
   if(hide(f.body))
diff --git a/src/goto-programs/goto_function.h b/src/goto-programs/goto_function.h
@@ -71,14 +71,6 @@ class goto_functiont
     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_functiont &other)
   {
     body.swap(other.body);
diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h
@@ -82,23 +82,12 @@ class goto_functionst
   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();
   }
 
   /// Get the identifier of the entry point to a goto model
diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp
@@ -244,14 +244,12 @@ void goto_function_inline(
   const irep_idt function,
   const namespacet &ns,
   message_handlert &message_handler,
-  bool adjust_function,
   bool caching)
 {
   goto_inlinet goto_inline(
     goto_functions,
     ns,
     message_handler,
-    adjust_function,
     caching);
 
   goto_functionst::function_mapt::iterator f_it=
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
@@ -66,7 +66,6 @@ void goto_inlinet::parameter_assignments(
       decl->code=code_declt(symbol.symbol_expr());
       decl->code.add_source_location()=source_location;
       decl->source_location=source_location;
-      decl->function=adjust_function?target->function:function_name;
     }
 
     // this is the actual parameter
@@ -129,8 +128,6 @@ void goto_inlinet::parameter_assignments(
       dest.add_instruction(ASSIGN);
       dest.instructions.back().source_location=source_location;
       dest.instructions.back().code.swap(assignment);
-      dest.instructions.back().function=
-        adjust_function?target->function:function_name;
     }
 
     if(it1!=arguments.end())
@@ -174,7 +171,6 @@ void goto_inlinet::parameter_destruction(
       dead->code=code_deadt(symbol.symbol_expr());
       dead->code.add_source_location()=source_location;
       dead->source_location=source_location;
-      dead->function=adjust_function?target->function:function_name;
     }
   }
 }
@@ -281,10 +277,6 @@ void goto_inlinet::insert_function_body(
     "final instruction of a function must be an END_FUNCTION");
   end.type=LOCATION;
 
-  if(adjust_function)
-    for(auto &instruction : body.instructions)
-      instruction.function=target->function;
-
   // make sure the inlined function does not introduce hiding
   if(goto_function.is_hidden())
   {
diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h
@@ -172,13 +172,6 @@ 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
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
@@ -178,9 +178,6 @@ class goto_programt
   public:
     codet code;
 
-    /// The function this instruction belongs to
-    irep_idt function;
-
     /// The location of the instruction in the source file
     source_locationt source_location;
 
@@ -347,7 +344,6 @@ class goto_programt
       swap(instruction.type, type);
       swap(instruction.guard, guard);
       swap(instruction.targets, targets);
-      swap(instruction.function, function);
     }
 
     #if (defined _MSC_VER && _MSC_VER <= 1800)
@@ -424,42 +420,6 @@ class goto_programt
     return t;
   }
 
-  /// Get the id of the function that contains the instruction pointed-to by the
-  /// given instruction iterator.
-  ///
-  /// \param l: instruction iterator
-  /// \return id of the function that contains the pointed-to goto instruction
-  static const irep_idt get_function_id(
-    const_targett l)
-  {
-    // The field `function` of an instruction may not always contain the id of
-    // the function it is currently in, due to goto program modifications such
-    // as inlining. For example, if an instruction in a function `f` is inlined
-    // into a function `g`, the instruction may, depending on the arguments to
-    // the inliner, retain the original value of `f` in the function field.
-    // However, instructions of type END_FUNCTION are never inlined into other
-    // functions, hence they contain the id of the function they are in. Thus,
-    // this function takes the END_FUNCTION instruction of the goto program and
-    // returns the value of its function field.
-
-    while(!l->is_end_function())
-      ++l;
-
-    return l->function;
-  }
-
-  /// Get the id of the function that contains the given goto program.
-  ///
-  /// \param p: the goto program
-  /// \return id of the function that contains the goto program
-  static const irep_idt get_function_id(
-    const goto_programt &p)
-  {
-    PRECONDITION(!p.empty());
-
-    return get_function_id(--p.instructions.end());
-  }
-
   template <typename Target>
   std::list<Target> get_successors(Target target) const;
 
@@ -578,22 +538,6 @@ class goto_programt
     }
   }
 
-  /// 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()
   {
@@ -608,9 +552,10 @@ class goto_programt
   void update();
 
   /// Human-readable loop name
-  static irep_idt loop_id(const instructiont &instruction)
+  static irep_idt
+  loop_id(const irep_idt &function_id, const instructiont &instruction)
   {
-    return id2string(instruction.function)+"."+
+    return id2string(function_id) + "." +
            std::to_string(instruction.loop_number);
   }
 
diff --git a/src/goto-programs/parameter_assignments.cpp b/src/goto-programs/parameter_assignments.cpp
@@ -76,7 +76,6 @@ void parameter_assignmentst::do_function_calls(
           if(rhs.type()!=lhs.type())
             rhs.make_typecast(lhs.type());
           t->code=code_assignt(lhs, rhs);
-          t->function=i_it->function;
         }
       }
 
diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp
@@ -100,7 +100,7 @@ static bool read_bin_goto_object_v4(
       goto_programt::instructiont &instruction=*itarget;
 
       irepconverter.reference_convert(in, instruction.code);
-      instruction.function = irepconverter.read_string_ref(in);
+      irepconverter.read_string_ref(in); // former function
       irepconverter.reference_convert(in, instruction.source_location);
       instruction.type = (goto_program_instruction_typet)
                               irepconverter.read_gb_word(in);
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
@@ -82,8 +82,10 @@ void goto_symext::symex_goto(statet &state)
       return;
     }
 
-    unsigned &unwind=
-      frame.loop_iterations[goto_programt::loop_id(*state.source.pc)].count;
+    const auto &loop_id =
+      goto_programt::loop_id(state.source.function, *state.source.pc);
+
+    unsigned &unwind = frame.loop_iterations[loop_id].count;
     unwind++;
 
     // continue unwinding?

Original file line number	Diff line number	Diff line change
`@@ -109,7 +109,7 @@ bool symex_bmct::get_unwind(`
`109`	`109`	`const goto_symex_statet::call_stackt &context,`
`110`	`110`	`unsigned unwind)`
`111`	`111`	`{`
`112`		`- const irep_idt id=goto_programt::loop_id(*source.pc);`
	`112`	`+ const irep_idt id = goto_programt::loop_id(source.function, *source.pc);`
`113`	`113`
`114`	`114`	`tvt abort_unwind_decision;`
`115`	`115`	`unsigned this_loop_limit=std::numeric_limits<unsigned>::max();`
Original file line number	Diff line number	Diff line change
`@@ -71,7 +71,6 @@ class cover_instrumenter_baset`
`71`	`71`	`t->source_location.set(ID_coverage_criterion, coverage_criterion);`
`72`	`72`	`t->source_location.set_property_class(property_class);`
`73`	`73`	`t->source_location.set_function(function);`
`74`		`- t->function = function;`
`75`	`74`	`}`
`76`	`75`
`77`	`76`	`bool is_non_cover_assertion(goto_programt::const_targett t) const`
Original file line number	Diff line number	Diff line change
`@@ -71,14 +71,6 @@ class goto_functiont`
`71`	`71`	`parameter_identifiers.clear();`
`72`	`72`	`}`
`73`	`73`
`74`		`- /// update the function member in each instruction`
`75`		- /// \param function_id: the `function_id` used for assigning empty function
`76`		`- /// members`
`77`		`- void update_instructions_function(const irep_idt &function_id)`
`78`		`- {`
`79`		`- body.update_instructions_function(function_id);`
`80`		`- }`
`81`		`-`
`82`	`74`	`void swap(goto_functiont &other)`
`83`	`75`	`{`
`84`	`76`	`body.swap(other.body);`
Original file line number	Diff line number	Diff line change
`@@ -66,7 +66,6 @@ void goto_inlinet::parameter_assignments(`
`66`	`66`	`decl->code=code_declt(symbol.symbol_expr());`
`67`	`67`	`decl->code.add_source_location()=source_location;`
`68`	`68`	`decl->source_location=source_location;`
`69`		`- decl->function=adjust_function?target->function:function_name;`
`70`	`69`	`}`
`71`	`70`
`72`	`71`	`// this is the actual parameter`
`@@ -129,8 +128,6 @@ void goto_inlinet::parameter_assignments(`
`129`	`128`	`dest.add_instruction(ASSIGN);`
`130`	`129`	`dest.instructions.back().source_location=source_location;`
`131`	`130`	`dest.instructions.back().code.swap(assignment);`
`132`		`- dest.instructions.back().function=`
`133`		`- adjust_function?target->function:function_name;`
`134`	`131`	`}`
`135`	`132`
`136`	`133`	`if(it1!=arguments.end())`
`@@ -174,7 +171,6 @@ void goto_inlinet::parameter_destruction(`
`174`	`171`	`dead->code=code_deadt(symbol.symbol_expr());`
`175`	`172`	`dead->code.add_source_location()=source_location;`
`176`	`173`	`dead->source_location=source_location;`
`177`		`- dead->function=adjust_function?target->function:function_name;`
`178`	`174`	`}`
`179`	`175`	`}`
`180`	`176`	`}`
`@@ -281,10 +277,6 @@ void goto_inlinet::insert_function_body(`
`281`	`277`	`"final instruction of a function must be an END_FUNCTION");`
`282`	`278`	`end.type=LOCATION;`
`283`	`279`
`284`		`- if(adjust_function)`
`285`		`- for(auto &instruction : body.instructions)`
`286`		`- instruction.function=target->function;`
`287`		`-`
`288`	`280`	`// make sure the inlined function does not introduce hiding`
`289`	`281`	`if(goto_function.is_hidden())`
`290`	`282`	`{`