Merge pull request #1555 from thk123/feature/remove-redundant-specalisation-code

[TG-1338] Remove redundant specialisation code

Author: Thomas Kiley

regression/cbmc-java/generics_symtab1/generics$bound_element.class

@@ -126,46 +126,3 @@ irep_idt generate_java_generic_typet::build_generic_tag(
 
   return new_tag_buffer.str();
 }
-
-
-/// Activate the generic instantiation code.
-/// \param message_handler
-/// \param symbol_table The symbol table so far.
-void
-instantiate_generics(
-  message_handlert &message_handler,
-  symbol_tablet &symbol_table)
-{
-  generate_java_generic_typet instantiate_generic_type(message_handler);
-  // check out the symbols in the symbol table at this point to see if we
-  // have a a generic type in.
-  for(const auto &symbol : symbol_table.symbols)
-  {
-    if(symbol.second.type.id()==ID_struct)
-    {
-      auto symbol_struct=to_struct_type(symbol.second.type);
-      auto &components=symbol_struct.components();
-
-      for(const auto &component : components)
-      {
-        if(is_java_generic_type(component.type()))
-        {
-          const auto &type_vars=to_java_generic_type(component.type()).
-            generic_type_variables();
-
-          // Before we can instantiate a generic component, we need
-          // its type variables to be instantiated parameters
-          if(all_of(type_vars.cbegin(), type_vars.cend(),
-                    [](const typet &type)
-                    {
-                      return is_java_generic_inst_parameter(type);
-                    }))
-          {
-            instantiate_generic_type(
-              to_java_generic_type(component.type()), symbol_table);
-          }
-        }
-      }
-    }
-  }
-}

regression/cbmc-java/generics_symtab1/generics$element.class

@@ -31,8 +31,4 @@ class generate_java_generic_typet
   message_handlert &message_handler;
 };
 
-void instantiate_generics(
-  message_handlert &message_handler,
-  symbol_tablet &symbol_table);
-
 #endif // CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H

regression/cbmc-java/generics_symtab1/generics.class

@@ -240,21 +240,8 @@ bool java_bytecode_languaget::typecheck(
     get_message_handler());
 
   // now typecheck all
-  bool res=java_bytecode_typecheck(
+  return java_bytecode_typecheck(
     symbol_table, get_message_handler(), string_refinement_enabled);
-  // NOTE (FOTIS): There is some unintuitive logic here, where
-  // java_bytecode_check will return TRUE if typechecking failed, and FALSE
-  // if everything went well...
-  if(res)
-  {
-    // there is no point in continuing to concretise
-    // the generic types if typechecking failed.
-    return res;
-  }
-
-  instantiate_generics(get_message_handler(), symbol_table);
-
-  return res;
 }
 
 bool java_bytecode_languaget::generate_support_functions(

regression/cbmc-java/generics_symtab1/generics.java

@@ -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 "
@@ -100,27 +126,6 @@ SCENARIO(
   }
 }
 
-
-SCENARIO(
-  "generate_java_generic_type_from_file_uninstantiated_param",
-  "[core][java_bytecode][generate_java_generic_type]")
-{
-  GIVEN("A generic java type with a field that refers to another generic with"
-          " an uninstantiated parameter.")
-  {
-    symbol_tablet new_symbol_table=
-      load_java_class("generic_unknown_field",
-                      "./java_bytecode/generate_concrete_generic_type");
-
-    // It's illegal to create an instantiation of a field that refers
-    // to a (still) uninstantiated generic class, so this is checking that
-    // this hasn't happened.
-    REQUIRE_FALSE(new_symbol_table.has_symbol
-      ("java::generic_unknown_field$element<T>"));
-  }
-}
-
-
 SCENARIO(
   "generate_java_generic_type_from_file_two_instances",
   "[core][java_bytecode][generate_java_generic_type]")
@@ -140,6 +145,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);

regression/cbmc-java/generics_symtab1/test.desc

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

src/java_bytecode/generate_java_generic_type.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);
+}

src/java_bytecode/generate_java_generic_type.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