Reduce the number of symbol_exprt without a source location

Create or maintain source location information in symbol expressions.

Author: tautschnig

src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

@@ -673,7 +673,8 @@ static void instantiate_atomic_fetch_op(
   block.add(code_frontend_assignt{deref_ptr, std::move(op_expr)});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[2]},
     typet{},
     source_location}});
@@ -736,7 +737,8 @@ static void instantiate_atomic_op_fetch(
 
   // this instruction implies an mfence, i.e., WRfence
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[2]},
     typet{},
     source_location}});
@@ -767,11 +769,11 @@ static void instantiate_sync_fetch(
     parameter_exprs[1],
     from_integer(std::memory_order_seq_cst, signed_int_type())};
 
-  block.add(code_returnt{
-    side_effect_expr_function_callt{symbol_exprt::typeless(atomic_name),
-                                    std::move(arguments),
-                                    typet{},
-                                    source_location}});
+  block.add(code_returnt{side_effect_expr_function_callt{
+    symbol_exprt::typeless(atomic_name).with_source_location(source_location),
+    std::move(arguments),
+    typet{},
+    source_location}});
 }
 
 static void instantiate_sync_bool_compare_and_swap(
@@ -790,7 +792,8 @@ static void instantiate_sync_bool_compare_and_swap(
   // _Bool __sync_bool_compare_and_swap(type *ptr, type old, type new, ...)
 
   block.add(code_returnt{side_effect_expr_function_callt{
-    symbol_exprt::typeless(ID___atomic_compare_exchange),
+    symbol_exprt::typeless(ID___atomic_compare_exchange)
+      .with_source_location(source_location),
     {parameter_exprs[0],
      address_of_exprt{parameter_exprs[1]},
      address_of_exprt{parameter_exprs[2]},
@@ -968,7 +971,8 @@ static void instantiate_atomic_load(
                                   dereference_exprt{parameter_exprs[0]}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[2]},
     typet{},
     source_location}});
@@ -999,7 +1003,8 @@ static void instantiate_atomic_load_n(
   block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless(ID___atomic_load),
+    symbol_exprt::typeless(ID___atomic_load)
+      .with_source_location(source_location),
     {parameter_exprs[0], address_of_exprt{result}, parameter_exprs[1]},
     typet{},
     source_location}});
@@ -1028,7 +1033,8 @@ static void instantiate_atomic_store(
                                   dereference_exprt{parameter_exprs[1]}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[2]},
     typet{},
     source_location}});
@@ -1051,13 +1057,14 @@ static void instantiate_atomic_store_n(
   // This built-in function implements an atomic store operation. It writes
   // val into *ptr.
 
-  block.add(code_expressiont{
-    side_effect_expr_function_callt{symbol_exprt::typeless(ID___atomic_store),
-                                    {parameter_exprs[0],
-                                     address_of_exprt{parameter_exprs[1]},
-                                     parameter_exprs[2]},
-                                    typet{},
-                                    source_location}});
+  block.add(code_expressiont{side_effect_expr_function_callt{
+    symbol_exprt::typeless(ID___atomic_store)
+      .with_source_location(source_location),
+    {parameter_exprs[0],
+     address_of_exprt{parameter_exprs[1]},
+     parameter_exprs[2]},
+    typet{},
+    source_location}});
 }
 
 static void instantiate_atomic_exchange(
@@ -1083,7 +1090,8 @@ static void instantiate_atomic_exchange(
                                   dereference_exprt{parameter_exprs[1]}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[3]},
     typet{},
     source_location}});
@@ -1114,7 +1122,8 @@ static void instantiate_atomic_exchange_n(
   block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless(ID___atomic_exchange),
+    symbol_exprt::typeless(ID___atomic_exchange)
+      .with_source_location(source_location),
     {parameter_exprs[0],
      address_of_exprt{parameter_exprs[1]},
      address_of_exprt{result},
@@ -1171,7 +1180,8 @@ static void instantiate_atomic_compare_exchange(
                                dereference_exprt{parameter_exprs[2]}};
   assign.add_source_location() = source_location;
   code_expressiont success_fence{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[4]},
     typet{},
     source_location}};
@@ -1181,7 +1191,8 @@ static void instantiate_atomic_compare_exchange(
                                          deref_ptr};
   assign_not_equal.add_source_location() = source_location;
   code_expressiont failure_fence{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[5]},
     typet{},
     source_location}};
@@ -1212,7 +1223,8 @@ static void instantiate_atomic_compare_exchange_n(
   // desired, bool weak, int success_memorder, int failure_memorder)
 
   block.add(code_returnt{side_effect_expr_function_callt{
-    symbol_exprt::typeless(ID___atomic_compare_exchange),
+    symbol_exprt::typeless(ID___atomic_compare_exchange)
+      .with_source_location(source_location),
     {parameter_exprs[0],
      parameter_exprs[1],
      address_of_exprt{parameter_exprs[2]},

src/assembler/remove_asm.cpp

@@ -133,7 +133,8 @@ void remove_asmt::gcc_asm_function_call(
       arguments.size(), code_typet::parametert{void_pointer}},
     empty_typet()};
 
-  symbol_exprt fkt(function_identifier, fkt_type);
+  auto fkt = symbol_exprt{function_identifier, fkt_type}.with_source_location(
+    code.source_location());
 
   code_function_callt function_call(std::move(fkt), std::move(arguments));
 
@@ -189,8 +190,8 @@ void remove_asmt::msc_asm_function_call(
       arguments.size(), code_typet::parametert{void_pointer}},
     empty_typet()};
 
-  symbol_exprt fkt(function_identifier, fkt_type);
-
+  auto fkt = symbol_exprt{function_identifier, fkt_type}.with_source_location(
+    code.source_location());
   code_function_callt function_call(std::move(fkt), std::move(arguments));
 
   dest.add(

src/pointer-analysis/value_set_dereference.cpp

@@ -236,7 +236,7 @@ exprt value_set_dereferencet::handle_dereference_base_case(
       pointer.type(),
       "derefd_pointer",
       "derefd_pointer",
-      source_locationt(),
+      pointer.find_source_location(),
       language_mode,
       new_symbol_table);
 

src/util/ssa_expr.cpp

@@ -41,6 +41,7 @@ ssa_exprt::ssa_exprt(const exprt &expr) : symbol_exprt(expr.type())
 {
   set(ID_C_SSA_symbol, true);
   add(ID_expression, expr);
+  with_source_location(expr.source_location());
   std::ostringstream os;
   initialize_ssa_identifier(os, expr);
   const std::string id = os.str();

src/util/symbol.cpp

@@ -120,7 +120,7 @@ void symbolt::swap(symbolt &b)
 ///   type of the symbol object.
 symbol_exprt symbolt::symbol_expr() const
 {
-  return symbol_exprt(name, type);
+  return symbol_exprt(name, type).with_source_location(location);
 }
 
 /// Check that the instance object is well formed.

unit/path_strategies.cpp

@@ -337,8 +337,13 @@ void symex_eventt::validate_resume(
   REQUIRE(!events.empty());
 
   int dst = 0;
-  if(!state.saved_target->source_location().get_line().empty())
+  if(
+    state.saved_target->source_location().get_file() !=
+      "<built-in-additions>" &&
+    !state.saved_target->source_location().get_line().empty())
+  {
     dst = std::stoi(state.saved_target->source_location().get_line().c_str());
+  }
 
   if(state.has_saved_next_instruction)
   {