Added support for concretising a generic and adding it into the symbol

table.

Author: NlightNFotis

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

@@ -0,0 +1,31 @@
+public class generics {
+
+  class element<E> {
+    E elem;
+  }
+
+  class bound_element<NUM extends java.lang.Number> {
+    NUM elem;
+    NUM f() {
+      return elem;
+    }
+    void g(NUM e) {
+      elem=e;
+    }
+  }
+
+  bound_element<Integer> belem;
+
+  Integer f(int n) {
+
+    element<Integer> e=new element<>();
+    e.elem=n;
+    bound_element<Integer> be=new bound_element<>();
+    belem=new bound_element<>();
+    be.elem=new Integer(n+1);
+    if(n>0)
+      return e.elem;
+    else
+      return be.elem;
+  }
+}

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

@@ -0,0 +1,8 @@
+CORE
+generics.class
+--show-symbol-table 
+^EXIT=0$
+^SIGNAL=0$
+^Type........: struct generics\$bound_element\<java::java.lang.Integer\> \{
+__CPROVER_string \@class_identifier; boolean \@lock; struct java.lang.Object \@java.lang.Object; struct java.lang.Integer \*elem; struct generics \*this\$0; \}$
+--

regression/cbmc-java/generics_symtab1/generics.class

@@ -1,6 +1,7 @@
 /*******************************************************************\
 
- Module: MODULE NAME
+ Module: Generate Java Generic Type - Instantiate a generic class with
+         concrete type information.
 
  Author: DiffBlue Limited. All rights reserved.
 
@@ -10,18 +11,21 @@
 #include <java_bytecode/java_types.h>
 #include <java_bytecode/java_utils.h>
 
-#include <iostream>
-#include <sstream>
 
 generate_java_generic_typet::generate_java_generic_typet(
-  symbol_tablet &symbol_table,
   message_handlert &message_handler):
-    symbol_table(symbol_table),
     message_handler(message_handler)
 {}
 
+/// Generate a concrete instantiation of a generic type.
+/// \param existing_generic_type The type to be concretised
+/// \param symbol_table The symbol table that the concrete type will be
+/// inserted into.
+/// \return The symbol as it was retrieved from the symbol table after
+/// it has been inserted into.
 symbolt generate_java_generic_typet::operator()(
-  const java_type_with_generic_typet &existing_generic_type)
+  const java_generic_typet &existing_generic_type,
+  symbol_tablet &symbol_table) const
 {
   namespacet ns(symbol_table);
 
@@ -30,58 +34,90 @@ symbolt generate_java_generic_typet::operator()(
   INVARIANT(
     pointer_subtype.id()==ID_struct, "Only pointers to classes in java");
 
-  const java_class_typet &java_class=to_java_class_type(pointer_subtype);
-
-  java_class_typet replacement_type=java_class;
-  replacement_type.components().clear();
-
-  const irep_idt new_tag=build_generic_tag(existing_generic_type, java_class);
-  replacement_type.set_tag(new_tag);
-
-  for(const struct_union_typet::componentt &component_type :
-    java_class.components())
-  {
-    if(!is_java_generic_type(component_type.type()))
+  const java_class_typet &replacement_type=
+    to_java_class_type(pointer_subtype);
+  const irep_idt new_tag=build_generic_tag(
+    existing_generic_type, replacement_type);
+  struct_union_typet::componentst replacement_components=
+    replacement_type.components();
+
+  // Small auxiliary function, to perform the inplace
+  // modification of the generic fields.
+  auto replace_type_for_generic_field=
+    [&](struct_union_typet::componentt &component)
     {
-      replacement_type.components().push_back(component_type);
-      continue;
-    }
+      if(is_java_generic_parameter(component.type()))
+      {
+        auto replacement_type_param=
+          to_java_generics_class_type(replacement_type);
+
+        auto component_identifier=
+          to_java_generic_parameter(component.type()).type_variable()
+            .get_identifier();
+
+        optionalt<size_t> results=java_generics_get_index_for_subtype(
+          replacement_type_param, component_identifier);
+
+        INVARIANT(
+          results.has_value(),
+          "generic component type not found");
+
+        if(results)
+        {
+          component.type()=
+            existing_generic_type.generic_type_variables()[*results];
+        }
+      }
+      return component;
+    };
+
+  std::size_t pre_modification_size=to_java_class_type(
+    ns.follow(existing_generic_type.subtype())).components().size();
+
+  std::for_each(
+    replacement_components.begin(),
+    replacement_components.end(),
+    replace_type_for_generic_field);
+
+  std::size_t after_modification_size=
+    replacement_type.components().size();
 
-    INVARIANT(
-      existing_generic_type.type_parameters.size()==1,
-      "Must have a type parameter");
-
-    struct_union_typet::componentt replacement_comp=component_type;
-    replacement_comp.type()=existing_generic_type.type_parameters[0];
-
-    replacement_type.components().push_back(replacement_comp);
-
-  }
   INVARIANT(
-    replacement_type.components().size()==java_class.components().size(),
+    pre_modification_size==after_modification_size,
     "All components in the original class should be in the new class");
 
-  generate_class_stub(new_tag, symbol_table, message_handler);
-  INVARIANT(symbol_table.has_symbol("java::"+id2string(new_tag)), "New class not created");
-  return symbol_table.lookup("java::"+id2string(new_tag));
+  const auto expected_symbol="java::"+id2string(new_tag);
+
+  generate_class_stub(
+    new_tag,
+    symbol_table,
+    message_handler,
+    replacement_components);
+  auto symbol=symbol_table.lookup(expected_symbol);
+  INVARIANT(symbol, "New class not created");
+  return *symbol;
 }
 
+/// Build a unique tag for the generic to be instantiated.
+/// \param existing_generic_type The type we want to concretise
+/// \param original_class
+/// \return A tag for the new generic we want a unique tag for.
 irep_idt generate_java_generic_typet::build_generic_tag(
-  const java_type_with_generic_typet &existing_generic_type,
-  const java_class_typet &original_class)
+  const java_generic_typet &existing_generic_type,
+  const java_class_typet &original_class) const
 {
   std::ostringstream new_tag_buffer;
   new_tag_buffer << original_class.get_tag();
   new_tag_buffer << "<";
   bool first=true;
-  for(const typet &param : existing_generic_type.type_parameters)
+  for(const typet &param : existing_generic_type.generic_type_variables())
   {
     if(!first)
-      new_tag_buffer << ", ";
+      new_tag_buffer << ",";
     first=false;
 
     INVARIANT(
-      is_java_inst_generic_type(param),
+      is_java_generic_inst_parameter(param),
       "Only create full concretized generic types");
     new_tag_buffer << param.subtype().get(ID_identifier);
   }
@@ -90,3 +126,46 @@ 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.java

@@ -1,12 +1,13 @@
 /*******************************************************************\
 
- Module: MODULE NAME
+ Module: Generate Java Generic Type - Instantiate a generic class with
+         concrete type information.
 
  Author: DiffBlue Limited. All rights reserved.
 
 \*******************************************************************/
-#ifndef GENERATE_JAVA_GENERIC_TYPE_H
-#define GENERATE_JAVA_GENERIC_TYPE_H
+#ifndef CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H
+#define CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H
 
 #include <util/message.h>
 #include <util/symbol_table.h>
@@ -17,20 +18,21 @@ class generate_java_generic_typet
 {
 public:
   generate_java_generic_typet(
-    symbol_tablet &symbol_table,
     message_handlert &message_handler);
 
   symbolt operator()(
-    const java_type_with_generic_typet &existing_generic_type);
+    const java_generic_typet &existing_generic_type,
+    symbol_tablet &symbol_table) const;
 private:
   irep_idt build_generic_tag(
-    const java_type_with_generic_typet &existing_generic_type,
-    const java_class_typet &original_class);
-
-  symbol_tablet &symbol_table;
+    const java_generic_typet &existing_generic_type,
+    const java_class_typet &original_class) const;
 
   message_handlert &message_handler;
-
 };
 
-#endif // GENERATE_JAVA_GENERIC_TYPE_H
+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/test.desc

@@ -63,7 +63,8 @@ class java_bytecode_convert_classt:public messaget
       generate_class_stub(
         parse_tree.parsed_class.name,
         symbol_table,
-        get_message_handler());
+        get_message_handler(),
+        struct_union_typet::componentst{});
   }
 
   typedef java_bytecode_parse_treet::classt classt;

src/java_bytecode/generate_java_generic_type.cpp

@@ -100,7 +100,8 @@ codet java_bytecode_instrumentt::throw_exception(
     generate_class_stub(
       exc_name,
       symbol_table,
-      get_message_handler());
+      get_message_handler(),
+      struct_union_typet::componentst{});
   }
 
   pointer_typet exc_ptr_type=

src/java_bytecode/generate_java_generic_type.h

@@ -30,6 +30,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_class_loader.h"
 #include "java_utils.h"
 #include <java_bytecode/ci_lazy_methods.h>
+#include <java_bytecode/generate_java_generic_type.h>
 
 #include "expr2java.h"
 
@@ -238,11 +239,21 @@ bool java_bytecode_languaget::typecheck(
     get_message_handler());
 
   // now typecheck all
-  if(java_bytecode_typecheck(
-       symbol_table, get_message_handler(), string_refinement_enabled))
-    return true;
+  bool res=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;
+  }
 
-  return false;
+  instantiate_generics(get_message_handler(), symbol_table);
+
+  return res;
 }
 
 bool java_bytecode_languaget::generate_support_functions(

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
 
 #include <util/invariant.h>
+#include <algorithm>
+
 #include <util/type.h>
 #include <util/std_types.h>
 #include <util/c_types.h>
@@ -379,4 +381,30 @@ inline typet java_type_from_string_with_exception(
   }
 }
 
+/// Get the index in the subtypes array for a given component.
+/// \param t The type we search for the subtypes in.
+/// \param identifier The string identifier of the type of the component.
+/// \return Optional with the size if the identifier was found.
+inline const optionalt<size_t> java_generics_get_index_for_subtype(
+  const java_generics_class_typet &t,
+  const irep_idt &identifier)
+{
+  const std::vector<java_generic_parametert> &gen_types=t.generic_types();
+
+  const auto iter = std::find_if(
+    gen_types.cbegin(),
+    gen_types.cend(),
+    [&identifier](const java_generic_parametert &ref)
+    {
+      return ref.type_variable().get_identifier()==identifier;
+    });
+
+  if(iter==gen_types.cend())
+  {
+    return {};
+  }
+
+  return std::distance(gen_types.cbegin(), iter);
+}
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H