Merge pull request #2975 from mgudemann/feature/jbmc/local_variables_generic_types

Use generic signature for local variables with entry in LVTT

Author: Matthias Güdemann

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -768,9 +768,20 @@ void java_bytecode_convert_methodt::setup_local_variables(
             << " name " << v.var.name << " v.var.descriptor '"
             << v.var.descriptor << "' holes " << v.holes.size() << eom;
 #endif
-    typet t;
-    // TODO: might need changing once descriptor/signature issue is resolved
-    t=java_type_from_string(v.var.descriptor);
+
+    const std::string &method_name = id2string(method_id);
+    const size_t method_name_end = method_name.rfind(":(");
+    const size_t class_name_end = method_name.rfind('.', method_name_end);
+    INVARIANT(
+      method_name_end != std::string::npos &&
+        class_name_end != std::string::npos,
+      "A method name has the format class `.` method `:(`signature`)`.");
+    const std::string class_name = method_name.substr(0, class_name_end);
+
+    const typet t = v.var.signature.has_value()
+                      ? java_type_from_string_with_exception(
+                          v.var.descriptor, v.var.signature, class_name)
+                      : java_type_from_string(v.var.descriptor);
 
     std::ostringstream id_oss;
     id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name;

jbmc/unit/Makefile

@@ -33,6 +33,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
        java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \

jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericLocalVar.class

@@ -0,0 +1,5 @@
+public class GenericLocalVar {
+  public void f() {
+    java.util.ArrayList<Double> l = null;
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericLocalVar.java

@@ -0,0 +1,35 @@
+/*******************************************************************\
+
+ Module: Unit tests for parsing generic local variables from the LVTT
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <java-testing-utils/load_java_class.h>
+#include <java-testing-utils/require_type.h>
+#include <testing-utils/catch.hpp>
+
+SCENARIO(
+  "parse_lvtt_generic_local_vars",
+  "[core][java_bytecode][java_bytecode_parse_generics]")
+{
+  const symbol_tablet &new_symbol_table = load_java_class(
+    "GenericLocalVar", "./java_bytecode/java_bytecode_parse_generics");
+
+  const std::string var_name("java::GenericLocalVar.f:()V::1::l");
+  REQUIRE(new_symbol_table.has_symbol(var_name));
+
+  WHEN("Local variable has an entry in the LVTT")
+  {
+    THEN("The type should be generic and instantiated with Double")
+    {
+      const symbolt &var_symbol = new_symbol_table.lookup_ref(var_name);
+      java_generic_typet local_var_type =
+        require_type::require_java_generic_type(
+          var_symbol.type,
+          {{require_type::type_argument_kindt::Inst,
+            "java::java.lang.Double"}});
+    }
+  }
+}