Merge pull request #7856 from tautschnig/bugfixes/linking-location

Add missing source locations

jbmc/src/java_bytecode/nondet.cpp

@@ -123,7 +123,9 @@ code_blockt generate_nondet_switch(
     this_block.add(switch_case);
     this_block.add(code_breakt());
     code_switch_caset this_case(
-      from_integer(case_number, switch_value.type()), this_block);
+      from_integer(case_number, switch_value.type())
+        .with_source_location(source_location),
+      this_block);
     switch_block.add(std::move(this_case));
     ++case_number;
   }

regression/CMakeLists.txt

@@ -77,6 +77,7 @@ add_subdirectory(k-induction)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-harness-multi-file-project)
 add_subdirectory(goto-cc-file-local)
+add_subdirectory(goto-cc-multi-file)
 add_subdirectory(goto-cc-regression-gh-issue-5380)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)

regression/Makefile

@@ -50,6 +50,7 @@ DIRS = cbmc-shadow-memory \
        goto-harness \
        goto-harness-multi-file-project \
        goto-cc-file-local \
+       goto-cc-multi-file \
        goto-cc-regression-gh-issue-5380 \
        linking-goto-binaries \
        symtab2gb \

regression/cbmc-cover/location3/main.c

@@ -0,0 +1,22 @@
+int main()
+{
+  int b, c;
+
+  if(b)
+  {
+    if(c)
+    {
+      c = 1;
+    }
+    else
+    {
+      c = 2;
+    }
+  }
+  else
+  {
+    b = 0;
+  }
+
+  return 1;
+}

regression/cbmc-cover/location3/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.\d+\] file main.c line 9 function main block \d+ \(lines main.c:main:9,10\): SATISFIED$
+^\[main.coverage.\d+\] file main.c line 15 function main block \d+ \(lines main.c:main:15\): SATISFIED$
+^\*\* 7 of 7 covered \(100.0%\)
+--
+^warning: ignoring
+--
+All gotos must have a source location annotated.

regression/goto-cc-multi-file/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}"
+)

regression/goto-cc-multi-file/maintain-location/main.c

@@ -0,0 +1,11 @@
+int foo()
+{
+  return 0;
+}
+
+int main()
+{
+  int result;
+  result = foo();
+  return result;
+}

regression/goto-cc-multi-file/maintain-location/other.c

@@ -0,0 +1,6 @@
+int foo();
+
+int bar()
+{
+  return foo();
+}

regression/goto-cc-multi-file/maintain-location/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+other.c
+file main.c line 9 function main
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+We previously lost the location attached to the call of `foo` in function main.

src/ansi-c/c_typecheck_expr.cpp

@@ -1044,15 +1044,16 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
     new_expr = size_of_opt.value();
   }
 
+  source_locationt location = expr.source_location();
   new_expr.swap(expr);
-
+  expr.add_source_location() = location;
   expr.add(ID_C_c_sizeof_type)=type;
 
   // The type may contain side-effects.
   if(!clean_code.empty())
   {
     side_effect_exprt side_effect_expr(
-      ID_statement_expression, void_type(), expr.source_location());
+      ID_statement_expression, void_type(), location);
     auto decl_block=code_blockt::from_list(clean_code);
     decl_block.set_statement(ID_decl_block);
     side_effect_expr.copy_to_operands(decl_block);
@@ -1064,8 +1065,9 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
     // It is not obvious whether the type or 'e' should be evaluated
     // first.
 
-    binary_exprt comma_expr{
-      std::move(side_effect_expr), ID_comma, expr, expr.type()};
+    exprt comma_expr =
+      binary_exprt{std::move(side_effect_expr), ID_comma, expr, expr.type()}
+        .with_source_location(location);
     expr.swap(comma_expr);
   }
 }
@@ -4656,6 +4658,8 @@ class is_compile_time_constantt
 
 void c_typecheck_baset::make_constant(exprt &expr)
 {
+  source_locationt location = expr.find_source_location();
+
   // Floating-point expressions may require a rounding mode.
   // ISO 9899:1999 F.7.2 says that the default is "round to nearest".
   // Some compilers have command-line options to override.
@@ -4664,10 +4668,11 @@ void c_typecheck_baset::make_constant(exprt &expr)
   adjust_float_expressions(expr, rounding_mode);
 
   simplify(expr, *this);
+  expr.add_source_location() = location;
 
   if(!is_compile_time_constantt(*this)(expr))
   {
-    error().source_location=expr.find_source_location();
+    error().source_location = location;
     error() << "expected constant expression, but got '" << to_string(expr)
             << "'" << eom;
     throw 0;
@@ -4676,13 +4681,15 @@ void c_typecheck_baset::make_constant(exprt &expr)
 
 void c_typecheck_baset::make_constant_index(exprt &expr)
 {
+  source_locationt location = expr.find_source_location();
   make_constant(expr);
   make_index_type(expr);
   simplify(expr, *this);
+  expr.add_source_location() = location;
 
   if(!is_compile_time_constantt(*this)(expr))
   {
-    error().source_location=expr.find_source_location();
+    error().source_location = location;
     error() << "conversion to integer constant failed" << eom;
     throw 0;
   }

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/goto-programs/goto_clean_expr.cpp

@@ -284,7 +284,14 @@ void goto_convertt::clean_expr(
 
     // generate guard for argument side-effects
     generate_ifthenelse(
-      if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode);
+      if_expr.cond(),
+      source_location,
+      tmp_true,
+      if_expr.true_case().source_location(),
+      tmp_false,
+      if_expr.false_case().source_location(),
+      dest,
+      mode);
 
     return;
   }