Only use source_locationt's get_function() for user output

A source location is a place in a text file, and the function
information stored in there need not coincide with the name we use in
the goto model.

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -869,7 +869,7 @@ void jbmc_parse_optionst::process_goto_function(
     if(using_symex_driven_loading)
     {
       // label the assertions
-      label_properties(goto_function.body);
+      label_properties(goto_function.body, function.get_function_id());
 
       goto_function.body.update();
       function.compute_location_numbers();

src/analyses/constant_propagator.cpp

@@ -478,7 +478,7 @@ void constant_propagator_domaint::valuest::set_dirty_to_top(
 
     const symbolt &symbol=ns.lookup(id);
 
-    if((!symbol.is_procedure_local() || dirty(id)) &&
+    if((symbol.is_static_lifetime || dirty(id)) &&
        !symbol.type.get_bool(ID_C_constant))
     {
       it = replace_const.erase(it);

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -206,7 +206,7 @@ symbol_exprt c_nondet_symbol_factory(
   bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
   CHECK_RETURN(!moving_symbol_failed);
 
-  symbol_factoryt state(symbol_table, loc, object_factory_parameters, lifetime);
+  symbol_factoryt state(symbol_table, loc, goto_functionst::entry_point(), object_factory_parameters, lifetime);
 
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);

src/ansi-c/c_nondet_symbol_factory.h

@@ -38,13 +38,14 @@ class symbol_factoryt
   symbol_factoryt(
     symbol_tablet &_symbol_table,
     const source_locationt &loc,
+    const irep_idt &name_prefix,
     const c_object_factory_parameterst &object_factory_params,
     const lifetimet lifetime)
     : symbol_table(_symbol_table),
       loc(loc),
       ns(_symbol_table),
       object_factory_params(object_factory_params),
-      allocate_objects(ID_C, loc, loc.get_function(), symbol_table),
+      allocate_objects(ID_C, loc, name_prefix, symbol_table),
       lifetime(lifetime)
   {
   }

src/ansi-c/expr2c.cpp

@@ -160,6 +160,8 @@ void expr2ct::get_shorthands(const exprt &expr)
       irep_idt func;
 
       const symbolt *symbol;
+      // we use the source-level function name as a means to detect collisions,
+      // which is ok, because this is about generating user-visible output
       if(!ns.lookup(symbol_id, symbol))
         func=symbol->location.get_function();
 

src/ansi-c/type2name.cpp

@@ -38,19 +38,26 @@ static std::string type2name_tag(
   if(ns.lookup(identifier, symbol))
     return "SYM#"+id2string(identifier)+"#";
 
+  std::string result;
+
+  // this isn't really a qualifier, but the linker needs to
+  // distinguish these - should likely be fixed in the linker instead
+  if(!symbol->is_static_lifetime)
+    result+='l';
+
   assert(symbol && symbol->is_type);
 
   if(symbol->type.id()!=ID_struct &&
      symbol->type.id()!=ID_union)
-    return type2name(symbol->type, ns, symbol_number);
+    return result + type2name(symbol->type, ns, symbol_number);
 
   // assign each symbol a number when seen for the first time
   std::pair<symbol_numbert::iterator, bool> entry=
     symbol_number.insert(std::make_pair(
         identifier,
         std::make_pair(symbol_number.size(), true)));
 
-  std::string result = "SYM" +
+  result += "SYM" +
                        id2string(to_struct_union_type(symbol->type).get_tag()) +
                        '#' + std::to_string(entry.first->second.first);
 
@@ -99,11 +106,6 @@ static std::string type2name(
   if(type.get_bool(ID_C_noreturn))
     result+='n';
 
-  // this isn't really a qualifier, but the linker needs to
-  // distinguish these - should likely be fixed in the linker instead
-  if(!type.source_location().get_function().empty())
-    result+='l';
-
   if(type.id().empty())
     throw "empty type encountered";
   else if(type.id()==ID_empty)

src/goto-instrument/aggressive_slicer.cpp

@@ -92,7 +92,7 @@ void aggressive_slicert::doit()
     auto property_loc = find_property(p, goto_model.goto_functions);
     if(!property_loc.has_value())
       throw "unable to find property in call graph";
-    note_functions_to_keep(property_loc.value().get_function());
+    note_functions_to_keep(property_loc->first);
   }
 
   // Add functions within distance of shortest path functions

src/goto-instrument/code_contracts.cpp

@@ -61,7 +61,9 @@ class code_contractst
 
   const symbolt &new_tmp_symbol(
     const typet &type,
-    const source_locationt &source_location);
+    const source_locationt &source_location,
+    const irep_idt &function_id,
+    const irep_idt &mode);
 };
 
 static void check_apply_invariants(
@@ -248,14 +250,16 @@ void code_contractst::code_contracts(
 
 const symbolt &code_contractst::new_tmp_symbol(
   const typet &type,
-  const source_locationt &source_location)
+  const source_locationt &source_location,
+  const irep_idt &function_id,
+  const irep_idt &mode)
 {
   return get_fresh_aux_symbol(
     type,
-    id2string(source_location.get_function()),
+    id2string(function_id) + "::tmp_cc",
     "tmp_cc",
     source_location,
-    irep_idt(),
+    mode,
     symbol_table);
 }
 
@@ -301,7 +305,8 @@ void code_contractst::add_contract_check(
   g->source_location=skip->source_location;
 
   // prepare function call including all declarations
-  code_function_callt call(ns.lookup(function).symbol_expr());
+  const symbolt &function_symbol = ns.lookup(function);
+  code_function_callt call(function_symbol.symbol_expr());
   replace_symbolt replace;
 
   // decl ret
@@ -312,7 +317,7 @@ void code_contractst::add_contract_check(
 
     symbol_exprt r=
       new_tmp_symbol(gf.type.return_type(),
-                     d->source_location).symbol_expr();
+                     d->source_location, function, function_symbol.mode).symbol_expr();
     d->code=code_declt(r);
 
     call.lhs()=r;
@@ -332,7 +337,7 @@ void code_contractst::add_contract_check(
 
     symbol_exprt p=
       new_tmp_symbol(p_it->type(),
-                     d->source_location).symbol_expr();
+                     d->source_location, function, function_symbol.mode).symbol_expr();
     d->code=code_declt(p);
 
     call.arguments().push_back(p);

src/goto-instrument/dump_c.cpp

@@ -169,7 +169,7 @@ void dump_ct::operator()(std::ostream &os)
     const irep_idt &type_id=symbol.type.id();
 
     if(symbol.is_type &&
-       symbol.location.get_function().empty() &&
+       !symbol.is_static_lifetime &&
        (type_id==ID_struct ||
         type_id==ID_union ||
         type_id==ID_c_enum))
@@ -293,7 +293,7 @@ void dump_ct::convert_compound_declaration(
     const symbolt &symbol,
     std::ostream &os_body)
 {
-  if(!symbol.location.get_function().empty())
+  if(!symbol.is_static_lifetime)
     return;
 
   // do compound type body
@@ -738,7 +738,7 @@ void dump_ct::gather_global_typedefs()
     const symbolt &symbol=symbol_entry.second;
 
     if(symbol.is_macro && symbol.is_type &&
-       symbol.location.get_function().empty())
+       !symbol.is_static_lifetime)
     {
       const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
       PRECONDITION(!typedef_str.empty());
@@ -843,8 +843,8 @@ void dump_ct::convert_global_variable(
     std::ostream &os,
     local_static_declst &local_static_decls)
 {
-  const irep_idt &func=symbol.location.get_function();
-  if((func.empty() || symbol.is_extern || symbol.value.is_not_nil()) &&
+  const bool global = symbol.is_static_lifetime;
+  if((global || symbol.is_extern || symbol.value.is_not_nil()) &&
       !converted_global.insert(symbol.name).second)
     return;
 
@@ -856,7 +856,7 @@ void dump_ct::convert_global_variable(
 
   // add a tentative declaration to cater for symbols in the initializer
   // relying on it this symbol
-  if((func.empty() || symbol.is_extern) &&
+  if((global || symbol.is_extern) &&
      (symbol.value.is_nil() || !syms.empty()))
   {
     os << "// " << symbol.name << '\n';
@@ -889,7 +889,7 @@ void dump_ct::convert_global_variable(
     d.copy_to_operands(symbol.value);
   }
 
-  if(!func.empty() && !symbol.is_extern)
+  if(!global && !symbol.is_extern)
   {
     local_static_decls.emplace(symbol.name, d);
   }

src/goto-instrument/generate_function_bodies.cpp

@@ -169,12 +169,14 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
     const exprt &lhs,
     const std::size_t initial_depth,
     const source_locationt &source_location,
+    const irep_idt &function_id,
     symbol_tablet &symbol_table,
     goto_programt &dest) const
   {
     symbol_factoryt symbol_factory(
       symbol_table,
       source_location,
+      function_id,
       object_factory_parameters,
       lifetimet::DYNAMIC);
 
@@ -235,6 +237,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
           dereference_expr,
           1, // depth 1 since we pass the dereferenced pointer
           function_symbol.location,
+          function_name,
           symbol_table,
           dest);
 
@@ -260,6 +263,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
         symbol_exprt(global_sym.name, global_sym.type),
         0,
         function_symbol.location,
+        irep_idt(),
         symbol_table,
         dest);
 
@@ -291,6 +295,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
         aux_symbol.symbol_expr(),
         0,
         function_symbol.location,
+        function_name,
         symbol_table,
         dest);
 

src/goto-instrument/goto_program2code.cpp

@@ -1416,7 +1416,7 @@ void goto_program2codet::add_local_types(const typet &type)
       const irep_idt &identifier=to_symbol_type(type).get_identifier();
       const symbolt &symbol=ns.lookup(identifier);
 
-      if(symbol.location.get_function().empty() ||
+      if(!symbol.is_static_lifetime ||
          !type_names_set.insert(identifier).second)
         return;
 
@@ -1432,7 +1432,7 @@ void goto_program2codet::add_local_types(const typet &type)
     const irep_idt &identifier=to_c_enum_tag_type(type).get_identifier();
     const symbolt &symbol=ns.lookup(identifier);
 
-    if(symbol.location.get_function().empty() ||
+    if(!symbol.is_static_lifetime ||
        !type_names_set.insert(identifier).second)
       return;
 
@@ -1982,7 +1982,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
       if(symbol.is_static_lifetime &&
          symbol.type.id()!=ID_code &&
          !symbol.is_extern &&
-         !symbol.location.get_function().empty() &&
+         !symbol.is_static_lifetime &&
          local_static_set.insert(identifier).second)
       {
         if(symbol.value.is_not_nil())

src/goto-instrument/wmm/abstract_event.h

@@ -34,6 +34,7 @@ class abstract_eventt:public graph_nodet<empty_edget>
   irep_idt variable;
   unsigned id;
   source_locationt source_location;
+  irep_idt function_id;
   bool local;
 
   // for ASMfence
@@ -62,9 +63,9 @@ class abstract_eventt:public graph_nodet<empty_edget>
 
   abstract_eventt(
     operationt _op, unsigned _th, irep_idt _var,
-    unsigned _id, source_locationt _loc, bool _local)
+    unsigned _id, source_locationt _loc, irep_idt _function_id, bool _local)
     :operation(_op), thread(_th), variable(_var), id(_id),
-    source_location(_loc), local(_local)
+    source_location(_loc), function_id(_function_id), local(_local)
   {
   }
 
@@ -74,6 +75,7 @@ class abstract_eventt:public graph_nodet<empty_edget>
     irep_idt _var,
     unsigned _id,
     source_locationt _loc,
+    irep_idt _function_id,
     bool _local,
     bool WRf,
     bool WWf,
@@ -87,6 +89,7 @@ class abstract_eventt:public graph_nodet<empty_edget>
     variable(_var),
     id(_id),
     source_location(_loc),
+    function_id(_function_id),
     local(_local),
     WRfence(RWf),
     WWfence(WWf),
@@ -106,6 +109,7 @@ class abstract_eventt:public graph_nodet<empty_edget>
     variable=other.variable;
     id=other.id;
     source_location=other.source_location;
+    function_id=other.function_id;
     local=other.local;
   }
 

src/goto-instrument/wmm/event_graph.cpp

@@ -96,8 +96,7 @@ event_idt event_grapht::copy_segment(event_idt begin, event_idt end)
   /* not sure -- we should allow cross function cycles */
   if(begin_event.source_location.get_file()!=end_event.source_location
     .get_file()
-    || begin_event.source_location.get_function()!=end_event.source_location
-    .get_function())
+    || begin_event.function_id!=end_event.function_id)
     return end;
 
   if(duplicated_bodies.find(std::make_pair(begin_event, end_event))