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.

Part 2: Wherever we generate fresh symbols or function-specific objects we
should use the actual function name to ensure fewer name collisions (for fresh
symbols) or actually unique objects.

Author: tautschnig

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -206,7 +206,12 @@ 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/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
@@ -310,9 +315,12 @@ void code_contractst::add_contract_check(
     goto_programt::targett d=check.add_instruction(DECL);
     d->source_location=skip->source_location;
 
-    symbol_exprt r=
-      new_tmp_symbol(gf.type.return_type(),
-                     d->source_location).symbol_expr();
+    symbol_exprt r = new_tmp_symbol(
+                       gf.type.return_type(),
+                       d->source_location,
+                       function,
+                       function_symbol.mode)
+                       .symbol_expr();
     d->code=code_declt(r);
 
     call.lhs()=r;
@@ -330,9 +338,10 @@ void code_contractst::add_contract_check(
     goto_programt::targett d=check.add_instruction(DECL);
     d->source_location=skip->source_location;
 
-    symbol_exprt p=
-      new_tmp_symbol(p_it->type(),
-                     d->source_location).symbol_expr();
+    symbol_exprt p =
+      new_tmp_symbol(
+        p_it->type(), d->source_location, function, function_symbol.mode)
+        .symbol_expr();
     d->code=code_declt(p);
 
     call.arguments().push_back(p);

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/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
@@ -61,10 +62,20 @@ class abstract_eventt:public graph_nodet<empty_edget>
   }
 
   abstract_eventt(
-    operationt _op, unsigned _th, irep_idt _var,
-    unsigned _id, source_locationt _loc, bool _local)
-    :operation(_op), thread(_th), variable(_var), id(_id),
-    source_location(_loc), local(_local)
+    operationt _op,
+    unsigned _th,
+    irep_idt _var,
+    unsigned _id,
+    source_locationt _loc,
+    irep_idt _function_id,
+    bool _local)
+    : operation(_op),
+      thread(_th),
+      variable(_var),
+      id(_id),
+      source_location(_loc),
+      function_id(_function_id),
+      local(_local)
   {
   }
 
@@ -74,27 +85,29 @@ 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,
     bool RRf,
     bool RWf,
     bool WWc,
     bool RWc,
-    bool RRc):
-    operation(_op),
-    thread(_th),
-    variable(_var),
-    id(_id),
-    source_location(_loc),
-    local(_local),
-    WRfence(RWf),
-    WWfence(WWf),
-    RRfence(RRf),
-    RWfence(WRf),
-    WWcumul(WWc),
-    RWcumul(RWc),
-    RRcumul(RRc)
+    bool RRc)
+    : operation(_op),
+      thread(_th),
+      variable(_var),
+      id(_id),
+      source_location(_loc),
+      function_id(_function_id),
+      local(_local),
+      WRfence(RWf),
+      WWfence(WWf),
+      RRfence(RRf),
+      RWfence(WRf),
+      WWcumul(WWc),
+      RWcumul(RWc),
+      RRcumul(RRc)
   {
   }
 
@@ -106,6 +119,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

@@ -94,10 +94,10 @@ event_idt event_grapht::copy_segment(event_idt begin, event_idt end)
   const abstract_eventt &end_event=operator[](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())
+  if(
+    begin_event.source_location.get_file() !=
+      end_event.source_location.get_file() ||
+    begin_event.function_id != end_event.function_id)
     return end;
 
   if(duplicated_bodies.find(std::make_pair(begin_event, end_event))

src/goto-instrument/wmm/goto2graph.cpp

@@ -199,8 +199,8 @@ void instrumentert::cfg_visitort::visit_cfg_function(
       #ifdef ATOMIC_BREAK
       visit_cfg_thread();
       #elif defined ATOMIC_FENCE
-      visit_cfg_fence(i_it);
-      #else
+      visit_cfg_fence(i_it, function_id);
+#else
       /* propagates */
       visit_cfg_propagate(i_it);
       #endif
@@ -222,11 +222,11 @@ void instrumentert::cfg_visitort::visit_cfg_function(
     else if(is_fence(instruction, instrumenter.ns))
     {
       instrumenter.message.debug() << "Constructing a fence" << messaget::eom;
-      visit_cfg_fence(i_it);
+      visit_cfg_fence(i_it, function_id);
     }
     else if(model!=TSO && is_lwfence(instruction, instrumenter.ns))
     {
-      visit_cfg_lwfence(i_it);
+      visit_cfg_lwfence(i_it, function_id);
     }
     else if(model==TSO && is_lwfence(instruction, instrumenter.ns))
     {
@@ -236,7 +236,7 @@ void instrumentert::cfg_visitort::visit_cfg_function(
     else if(instruction.is_other()
       && instruction.code.get_statement()==ID_fence)
     {
-      visit_cfg_asm_fence(i_it);
+      visit_cfg_asm_fence(i_it, function_id);
     }
     else if(instruction.is_function_call())
     {
@@ -742,11 +742,18 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(
 }
 
 void instrumentert::cfg_visitort::visit_cfg_lwfence(
-  goto_programt::instructionst::iterator i_it)
+  goto_programt::instructionst::iterator i_it,
+  const irep_idt &function_id)
 {
   const goto_programt::instructiont &instruction=*i_it;
-  const abstract_eventt new_fence_event(abstract_eventt::operationt::Lwfence,
-    thread, "f", instrumenter.unique_id++, instruction.source_location, false);
+  const abstract_eventt new_fence_event(
+    abstract_eventt::operationt::Lwfence,
+    thread,
+    "f",
+    instrumenter.unique_id++,
+    instruction.source_location,
+    function_id,
+    false);
   const event_idt new_fence_node=egraph.add_node();
   egraph[new_fence_node](new_fence_event);
   const event_idt new_fence_gnode=egraph_alt.add_node();
@@ -774,7 +781,8 @@ void instrumentert::cfg_visitort::visit_cfg_lwfence(
 }
 
 void instrumentert::cfg_visitort::visit_cfg_asm_fence(
-  goto_programt::instructionst::iterator i_it)
+  goto_programt::instructionst::iterator i_it,
+  const irep_idt &function_id)
 {
   const goto_programt::instructiont &instruction=*i_it;
   bool WRfence=instruction.code.get_bool(ID_WRfence);
@@ -784,9 +792,21 @@ void instrumentert::cfg_visitort::visit_cfg_asm_fence(
   bool WWcumul=instruction.code.get_bool(ID_WWcumul);
   bool RRcumul=instruction.code.get_bool(ID_RRcumul);
   bool RWcumul=instruction.code.get_bool(ID_RWcumul);
-  const abstract_eventt new_fence_event(abstract_eventt::operationt::ASMfence,
-    thread, "asm", instrumenter.unique_id++, instruction.source_location,
-    false, WRfence, WWfence, RRfence, RWfence, WWcumul, RWcumul, RRcumul);
+  const abstract_eventt new_fence_event(
+    abstract_eventt::operationt::ASMfence,
+    thread,
+    "asm",
+    instrumenter.unique_id++,
+    instruction.source_location,
+    function_id,
+    false,
+    WRfence,
+    WWfence,
+    RRfence,
+    RWfence,
+    WWcumul,
+    RWcumul,
+    RRcumul);
   const event_idt new_fence_node=egraph.add_node();
   egraph[new_fence_node](new_fence_event);
   const event_idt new_fence_gnode=egraph_alt.add_node();
@@ -867,9 +887,14 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
     assert(read_expr);
 #endif
 
-    const abstract_eventt new_read_event(abstract_eventt::operationt::Read,
-      thread, id2string(read), instrumenter.unique_id++,
-      instruction.source_location, local(read));
+    const abstract_eventt new_read_event(
+      abstract_eventt::operationt::Read,
+      thread,
+      id2string(read),
+      instrumenter.unique_id++,
+      instruction.source_location,
+      function_id,
+      local(read));
 
     const event_idt new_read_node=egraph.add_node();
     egraph[new_read_node]=new_read_event;
@@ -965,9 +990,14 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
     // assert(write_expr);
 
     /* creates Write */
-    const abstract_eventt new_write_event(abstract_eventt::operationt::Write,
-      thread, id2string(write), instrumenter.unique_id++,
-      instruction.source_location, local(write));
+    const abstract_eventt new_write_event(
+      abstract_eventt::operationt::Write,
+      thread,
+      id2string(write),
+      instrumenter.unique_id++,
+      instruction.source_location,
+      function_id,
+      local(write));
 
     const event_idt new_write_node=egraph.add_node();
     egraph[new_write_node](new_write_event);
@@ -1137,11 +1167,18 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
 }
 
 void instrumentert::cfg_visitort::visit_cfg_fence(
-  goto_programt::instructionst::iterator i_it)
+  goto_programt::instructionst::iterator i_it,
+  const irep_idt &function_id)
 {
   const goto_programt::instructiont &instruction=*i_it;
-  const abstract_eventt new_fence_event(abstract_eventt::operationt::Fence,
-    thread, "F", instrumenter.unique_id++, instruction.source_location, false);
+  const abstract_eventt new_fence_event(
+    abstract_eventt::operationt::Fence,
+    thread,
+    "F",
+    instrumenter.unique_id++,
+    instruction.source_location,
+    function_id,
+    false);
   const event_idt new_fence_node=egraph.add_node();
   egraph[new_fence_node](new_fence_event);
   const event_idt new_fence_gnode=egraph_alt.add_node();
@@ -1440,7 +1477,7 @@ void inline instrumentert::print_outputs_local(
       if(render_po_aligned)
         same_po[ev.thread].insert(*it_e);
       if(render_by_function)
-        same_file[ev.source_location.get_function()].insert(*it_e);
+        same_file[ev.function_id].insert(*it_e);
       else if(render_by_file)
         same_file[ev.source_location.get_file()].insert(*it_e);
       if(ev.thread>max_thread)