Java frontend: record source locations of read static variables

This enables trace-source-location reports not to vary depending on whether static initializer
calls were produced or not (at present the call would result in a statement at the getstatic
location, while the variable read itself would disappear; a 'putstatic' instruction by contrast
always generates an assignment and so is accounted for by a source location).

Author: smowton

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1619,7 +1619,12 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
         symbol_table.lookup_ref(field_id).symbol_expr());
 
       convert_getstatic(
-        arg0, symbol_expr, is_assertions_disabled_field, c, results);
+        i_it->source_location,
+        arg0,
+        symbol_expr,
+        is_assertions_disabled_field,
+        c,
+        results);
     }
     else if(bytecode == BC_putfield)
     {
@@ -2624,6 +2629,7 @@ code_blockt java_bytecode_convert_methodt::convert_putfield(
 }
 
 void java_bytecode_convert_methodt::convert_getstatic(
+  const source_locationt &source_location,
   const exprt &arg0,
   const symbol_exprt &symbol_expr,
   const bool is_assertions_disabled_field,
@@ -2651,7 +2657,9 @@ void java_bytecode_convert_methodt::convert_getstatic(
       needed_lazy_methods->add_needed_class(arg0.get_string(ID_class));
     }
   }
-  results[0] = java_bytecode_promotion(symbol_expr);
+  symbol_exprt symbol_with_location = symbol_expr;
+  symbol_with_location.add_source_location() = source_location;
+  results[0] = java_bytecode_promotion(symbol_with_location);
 
   // Note this initializer call deliberately inits the class used to make
   // the reference, which may be a child of the class that actually defines

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -432,6 +432,7 @@ class java_bytecode_convert_methodt:public messaget
     exprt::operandst &results) const;
 
   void convert_getstatic(
+    const source_locationt &source_location,
     const exprt &arg0,
     const symbol_exprt &symbol_expr,
     bool is_assertions_disabled_field,

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassReadingStaticField.class

@@ -0,0 +1,11 @@
+public class ClassReadingStaticField {
+
+  static int x;
+
+  public static int test() {
+
+    return x;
+
+  }
+
+}

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassReadingStaticField.java

@@ -290,6 +290,45 @@ SCENARIO(
   }
 }
 
+SCENARIO(
+  "java_bytecode_convert_method_with_getstatic",
+  "[core][java_bytecode][java_bytecode_convert_method]")
+{
+  GIVEN("A class that reads a static field.")
+  {
+    const symbol_tablet symbol_table = load_java_class(
+      "ClassReadingStaticField",
+      "./java_bytecode/java_bytecode_convert_method");
+
+    WHEN("Converting the method that reads said field")
+    {
+      const auto &method_symbol =
+        symbol_table.lookup_ref("java::ClassReadingStaticField.test:()I");
+
+      THEN(
+        "There should be a symbol expression attributed to bytecode index "
+        "0 (the getstatic instruction)")
+      {
+        bool found = false;
+        method_symbol.value.visit_pre([&found](const exprt &subexpr) {
+          if(
+            const auto symbol_expr =
+              expr_try_dynamic_cast<symbol_exprt>(subexpr))
+          {
+            if(
+              symbol_expr->source_location().get_java_bytecode_index() == "0" &&
+              symbol_expr->get_identifier() ==
+                "java::ClassReadingStaticField.x")
+              found = true;
+          }
+        });
+
+        REQUIRE(found);
+      }
+    }
+  }
+}
+
 /// Allow access to private methods so that they can be unit tested
 class java_bytecode_convert_method_unit_testt
 {