Manually call specalisation code

Author: thk123

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

@@ -9,13 +9,33 @@
 
 #include <testing-utils/catch.hpp>
 #include <testing-utils/load_java_class.h>
+#include <testing-utils/require_type.h>
 
 #include <util/symbol_table.h>
 
 #include <java_bytecode/generate_java_generic_type.h>
 #include <testing-utils/require_type.h>
+#include <testing-utils/generic_utils.h>
 #include <util/ui_message.h>
 
+/// Helper function to specalise a generic class from a named component of a
+/// named class
+/// \param class_name: The name of the class that has a generic component.
+/// \param component_name: The name of the generic component
+/// \param new_symbol_table: The symbol table to use.
+void specialise_generic_from_component(
+  const irep_idt &class_name,
+  const irep_idt &component_name,
+  symbol_tablet &new_symbol_table)
+{
+  const symbolt &harness_symbol = new_symbol_table.lookup_ref(class_name);
+  const struct_typet::componentt &harness_component =
+    require_type::require_component(
+      to_struct_type(harness_symbol.type), component_name);
+  generic_utils::specialise_generic(
+    to_java_generic_type(harness_component.type()), new_symbol_table);
+}
+
 SCENARIO(
   "generate_java_generic_type_from_file",
   "[core][java_bytecode][generate_java_generic_type]")
@@ -30,6 +50,9 @@ SCENARIO(
       load_java_class("generic_two_fields",
                       "./java_bytecode/generate_concrete_generic_type");
 
+    specialise_generic_from_component(
+      "java::generic_two_fields", "belem", new_symbol_table);
+
     REQUIRE(new_symbol_table.has_symbol(expected_symbol));
     THEN("The class should contain two instantiated fields.")
     {
@@ -77,6 +100,9 @@ SCENARIO(
       load_java_class("generic_two_parameters",
                       "./java_bytecode/generate_concrete_generic_type");
 
+    specialise_generic_from_component(
+      "java::generic_two_parameters", "bomb", new_symbol_table);
+
     REQUIRE(new_symbol_table.has_symbol(
       "java::generic_two_parameters$KeyValuePair"));
     THEN("The class should have two subtypes in the vector of the types of "
@@ -140,6 +166,11 @@ SCENARIO(
       load_java_class("generic_two_instances",
                       "./java_bytecode/generate_concrete_generic_type");
 
+    specialise_generic_from_component(
+      "java::generic_two_instances", "bool_element", new_symbol_table);
+    specialise_generic_from_component(
+      "java::generic_two_instances", "int_element", new_symbol_table);
+
     REQUIRE(new_symbol_table.has_symbol(first_expected_symbol));
     auto first_symbol=new_symbol_table.lookup(first_expected_symbol);
     REQUIRE(first_symbol->type.id()==ID_struct);

unit/testing-utils/Makefile

@@ -1,5 +1,6 @@
 SRC = \
   c_to_expr.cpp \
+  generic_utils.cpp \
   load_java_class.cpp \
   require_expr.cpp \
   require_goto_statements.cpp \

unit/testing-utils/generic_utils.cpp

@@ -0,0 +1,37 @@
+/*******************************************************************\
+
+ Module: Unit test utilities
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <util/ui_message.h>
+#include <java_bytecode/generate_java_generic_type.h>
+#include "generic_utils.h"
+#include "catch.hpp"
+#include "require_type.h"
+
+/// Generic a specalised version of a Java generic class and add it to the
+/// symbol table.
+/// \param example_type: A reference type that is a specalised generic to use
+/// as the base for the specalised version (e.g. a variable of type
+/// `Generic<Integer>`
+/// \param new_symbol_table: The symbol table to store the new type in
+void generic_utils::specialise_generic(
+  const java_generic_typet &example_type,
+  symbol_tablet &new_symbol_table)
+{
+  // Should be a fully instantiated generic type
+  REQUIRE(
+    std::all_of(
+      example_type.generic_type_variables().begin(),
+      example_type.generic_type_variables().end(),
+      is_java_generic_inst_parameter));
+
+  // Generate the specialised version.
+  ui_message_handlert message_handler;
+  generate_java_generic_typet instantiate_generic_type(message_handler);
+  instantiate_generic_type(
+    to_java_generic_type(example_type), new_symbol_table);
+}

unit/testing-utils/generic_utils.h

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+ Module: Unit test utilities
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Utility methods for dealing with Java generics in unit tests
+
+#ifndef CPROVER_TESTING_UTILS_GENERIC_UTILS_H
+#define CPROVER_TESTING_UTILS_GENERIC_UTILS_H
+
+#include <util/irep.h>
+#include <util/symbol_table.h>
+
+// NOLINTNEXTLINE(readability/namespace)
+namespace generic_utils
+{
+void specialise_generic(
+  const java_generic_typet &example_type,
+  symbol_tablet &new_symbol_table);
+}
+
+#endif // CPROVER_TESTING_UTILS_GENERIC_UTILS_H