Merge pull request #4137 from smowton/smowton/fix/java-static-field-generic-types

Java frontend: get qualified generic types of static fields

Author: smowton

jbmc/regression/jbmc/generic_static_field/Test.class

@@ -0,0 +1,12 @@
+
+public class Test<T> {
+
+  public static Test<Integer> static_field;
+
+  public static Test<Integer> test() {
+
+    return static_field;
+
+  }
+
+}

jbmc/regression/jbmc/generic_static_field/Test.java

@@ -0,0 +1,15 @@
+CORE
+Test.class
+--function Test.test --validate-goto-model --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+Test\.test:\(\)LTest;#return_value = static_field;
+--
+^warning: ignoring
+--
+This checks that the return value type matches the static field -- if it didn't,
+either --validate-goto-model would throw because of a mismatching assignment, or
+a cast would be used to adjust the type.
+
+The original motivation for this test was that generic field references could
+accidentally omit generic arguments that were present in function types.

jbmc/regression/jbmc/generic_static_field/test.desc

@@ -1529,12 +1529,12 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       const bool is_assertions_disabled_field=
         field_name.find("$assertionsDisabled")!=std::string::npos;
 
-      const symbol_exprt symbol_expr(
-        get_static_field(arg0.get_string(ID_class), field_name), arg0.type());
+      const irep_idt field_id(
+        get_static_field(arg0.get_string(ID_class), field_name));
 
-      INVARIANT(
-        symbol_table.has_symbol(symbol_expr.get_identifier()),
-        "getstatic symbol should have been created before method conversion");
+      // Symbol should have been populated by java_bytecode_convert_class:
+      const symbol_exprt symbol_expr(
+        symbol_table.lookup_ref(field_id).symbol_expr());
 
       convert_getstatic(
         arg0, symbol_expr, is_assertions_disabled_field, c, results);
@@ -1549,12 +1549,12 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       PRECONDITION(op.size() == 1 && results.empty());
       const auto &field_name=arg0.get_string(ID_component_name);
 
-      const symbol_exprt symbol_expr(
-        get_static_field(arg0.get_string(ID_class), field_name), arg0.type());
+      const irep_idt field_id(
+        get_static_field(arg0.get_string(ID_class), field_name));
 
-      INVARIANT(
-        symbol_table.has_symbol(symbol_expr.get_identifier()),
-        "putstatic symbol should have been created before method conversion");
+      // Symbol should have been populated by java_bytecode_convert_class:
+      const symbol_exprt symbol_expr(
+        symbol_table.lookup_ref(field_id).symbol_expr());
 
       c = convert_putstatic(i_it->source_location, arg0, op, symbol_expr);
     }