Ensure source locations are kept across code instrumentation

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -998,24 +998,6 @@ static unsigned get_bytecode_type_width(const typet &ty)
   return ty.get_unsigned_int(ID_width);
 }
 
-/// Merge code's source location with source_location, and recursively
-/// do the same to operand code. Typically this is used for a code_blockt
-/// as is generated for some Java operations such as "putstatic", but will
-/// also work if they generate conditionals, loops, etc.
-/// Merge means that any fields already set in code.add_source_location()
-/// remain so; any new ones from source_location are added.
-static void merge_source_location_rec(
-  codet &code,
-  const source_locationt &source_location)
-{
-  code.add_source_location().merge(source_location);
-  for(exprt &op : code.operands())
-  {
-    if(op.id()==ID_code)
-      merge_source_location_rec(to_code(op), source_location);
-  }
-}
-
 codet java_bytecode_convert_methodt::convert_instructions(
   const methodt &method,
   const code_typet &method_type,

src/java_bytecode/java_bytecode_instrument.cpp

@@ -300,6 +300,7 @@ codet java_bytecode_instrumentt::check_array_length(
 void java_bytecode_instrumentt::instrument_code(exprt &expr)
 {
   codet &code=to_code(expr);
+  source_locationt old_source_location=code.source_location();
 
   const irep_idt &statement=code.get_statement();
 
@@ -405,6 +406,10 @@ void java_bytecode_instrumentt::instrument_code(exprt &expr)
     block.copy_to_operands(code);
     code=block;
   }
+
+  // Ensure source location is retained:
+  if(!old_source_location.get_line().empty())
+    merge_source_location_rec(code, old_source_location);
 }
 
 /// Computes the instrumentation for `expr` in the form of

src/java_bytecode/java_utils.cpp

@@ -55,7 +55,6 @@ unsigned java_method_parameter_slots(const code_typet &t)
   return slots;
 }
 
-
 const std::string java_class_to_package(const std::string &canonical_classname)
 {
   return trim_from_last_delimiter(canonical_classname, '.');
@@ -99,3 +98,12 @@ void generate_class_stub(
     java_root_class(*class_symbol);
   }
 }
+
+void merge_source_location_rec(
+  exprt &expr,
+  const source_locationt &source_location)
+{
+  expr.add_source_location().merge(source_location);
+  for(exprt &op : expr.operands())
+    merge_source_location_rec(op, source_location);
+}

src/java_bytecode/java_utils.h

@@ -32,4 +32,17 @@ unsigned java_method_parameter_slots(const code_typet &t);
 
 const std::string java_class_to_package(const std::string &canonical_classname);
 
+/// Attaches a source location to an expression and all of its subexpressions.
+/// Usually only codet needs this, but there are a few known examples of
+/// expressions needing a location, such as
+/// `goto_convertt::do_function_call_symbol` (function() needs a location)
+/// and `goto_convertt::clean_expr` (any subexpression being split into a
+/// separate instruction needs a location), so for safety we give every
+/// mentioned expression a location.
+/// Any code or expressions with source location fields already set keep those
+/// fields using rules of source_locationt::merge.
+void merge_source_location_rec(
+  exprt &expr,
+  const source_locationt &source_location);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H