Java frontend: Set source locations on instructions in code_blocks

regression/cbmc-java/putstatic_source_location/test.desc

@@ -0,0 +1,6 @@
+CORE
+test.class
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+test\.java line 5 function java::test.main:\(\)V bytecode_index 1

regression/cbmc-java/putstatic_source_location/test.java

@@ -0,0 +1,11 @@
+public class test {
+
+  public static int x;
+  public static void main() {
+    x = 1;
+  }
+  static {
+    x = 0;
+  }
+
+}

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -982,6 +982,24 @@ 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,
@@ -2376,7 +2394,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
 
     if(!i_it->source_location.get_line().empty())
-      c.add_source_location()=i_it->source_location;
+      merge_source_location_rec(c, i_it->source_location);
 
     push(results);
 

src/util/source_location.cpp

@@ -62,6 +62,15 @@ std::string source_locationt::as_string(bool print_cwd) const
   return dest;
 }
 
+void source_locationt::merge(const source_locationt &from)
+{
+  forall_named_irep(it, from.get_named_sub())
+  {
+    if(get(it->first).empty())
+      set(it->first, it->second);
+  }
+}
+
 std::ostream &operator << (
   std::ostream &out,
   const source_locationt &source_location)

src/util/source_location.h

@@ -162,6 +162,10 @@ class source_locationt:public irept
     return is_built_in(id2string(get_file()));
   }
 
+  /// Set all unset source-location fields in this object to their values in
+  /// 'from'. Leave set fields in this object alone.
+  void merge(const source_locationt &from);
+
   static const source_locationt &nil()
   {
     return static_cast<const source_locationt &>(get_nil_irep());