Merge pull request diffblue#4439 from svorenova/opaque-fields-final

[TG-6381] Set opaque fields as final

Author: svorenova

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -297,6 +297,7 @@ bool java_bytecode_languaget::parse(
 /// without realising that is in fact the same field, inherited from that
 /// ancestor. This can lead to incorrect results when opaque types are cast
 /// to other opaque types and their fields do not alias as intended.
+/// We set opaque fields as final to avoid assuming they can be overridden.
 /// \param parse_tree: class parse tree
 /// \param symbol_table: global symbol table
 static void infer_opaque_type_fields(
@@ -335,6 +336,7 @@ static void infer_opaque_type_fields(
             components.emplace_back(component_name, fieldref.type());
             components.back().set_base_name(component_name);
             components.back().set_pretty_name(component_name);
+            components.back().set_is_final(true);
             break;
           }
           else
@@ -501,6 +503,8 @@ static void create_stub_global_symbol(
   // whereas a more restricted visbility would encourage separating them.
   // Neither is correct, as without the class file we can't know the truth.
   new_symbol.type.set(ID_C_access, ID_public);
+  // We set the field as final to avoid assuming they can be overridden.
+  new_symbol.type.set(ID_C_constant, true);
   new_symbol.pretty_name = new_symbol.name;
   new_symbol.mode = ID_java;
   new_symbol.is_type = false;

jbmc/unit/Makefile

@@ -20,6 +20,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
        java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
        java_bytecode/java_bytecode_convert_method/convert_method.cpp \
        java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp \
+       java_bytecode/java_bytecode_language/language.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \

jbmc/unit/java_bytecode/java_bytecode_language/ClassUsingOpaqueField.class

@@ -0,0 +1,6 @@
+public class ClassUsingOpaqueField {
+  public static int opaqueFieldMethod() {
+    OpaqueClass o = new OpaqueClass();
+    return OpaqueClass.field1 + o.field2;
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_language/ClassUsingOpaqueField.java

@@ -0,0 +1,5 @@
+// .class file must be deleted
+public class OpaqueClass {
+  public static int field1 = 1;
+  public int field2;
+}

jbmc/unit/java_bytecode/java_bytecode_language/OpaqueClass.java

@@ -0,0 +1,47 @@
+/*******************************************************************\
+
+Module: Unit tests for java_bytecode_language.
+
+Author: Diffblue Limited.
+
+\*******************************************************************/
+
+#include <testing-utils/use_catch.h>
+
+#include <util/symbol_table.h>
+
+#include <java-testing-utils/load_java_class.h>
+#include <java-testing-utils/require_type.h>
+
+SCENARIO(
+  "java_bytecode_language_opaque_field",
+  "[core][java_bytecode][java_bytecode_language]")
+{
+  GIVEN("A class that accesses opaque fields")
+  {
+    const symbol_tablet symbol_table = load_java_class(
+      "ClassUsingOpaqueField", "./java_bytecode/java_bytecode_language");
+    std::string opaque_class_prefix = "java::OpaqueClass";
+
+    WHEN("When parsing opaque class with fields")
+    {
+      THEN("Static field field1 is marked as final")
+      {
+        const symbolt &opaque_field_symbol =
+          symbol_table.lookup_ref(opaque_class_prefix + ".field1");
+        REQUIRE(opaque_field_symbol.type.get_bool(ID_C_constant));
+      }
+
+      THEN("Non-static field field2 is marked final")
+      {
+        const symbolt &opaque_class_symbol =
+          symbol_table.lookup_ref(opaque_class_prefix);
+        const struct_typet &opaque_class_struct =
+          to_struct_type(opaque_class_symbol.type);
+        const struct_union_typet::componentt &field =
+          require_type::require_component(opaque_class_struct, "field2");
+        REQUIRE(field.get_is_final());
+      }
+    }
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_language/language.cpp

@@ -0,0 +1,3 @@
+java-testing-utils
+testing-utils
+util