Merge pull request #1406 from NlightNFotis/fotis/generics_support

[TG-375] Fotis/generics support

Author: Thomas Kiley

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

@@ -25,6 +25,7 @@ SRC = bytecode_info.cpp \
       java_string_library_preprocess.cpp \
       java_types.cpp \
       java_utils.cpp \
+      generate_java_generic_type.cpp \
       mz_zip_archive.cpp \
       select_pointer_type.cpp \
       # Empty last line

regression/cbmc-java/generics_symtab1/generics.java

@@ -0,0 +1,171 @@
+/*******************************************************************\
+
+ Module: Generate Java Generic Type - Instantiate a generic class with
+         concrete type information.
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+#include "generate_java_generic_type.h"
+#include <util/namespace.h>
+#include <java_bytecode/java_types.h>
+#include <java_bytecode/java_utils.h>
+
+
+generate_java_generic_typet::generate_java_generic_typet(
+  message_handlert &message_handler):
+    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_generic_typet &existing_generic_type,
+  symbol_tablet &symbol_table) const
+{
+  namespacet ns(symbol_table);
+
+  const typet &pointer_subtype=ns.follow(existing_generic_type.subtype());
+
+  INVARIANT(
+    pointer_subtype.id()==ID_struct, "Only pointers to classes in java");
+
+  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)
+    {
+      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(
+    pre_modification_size==after_modification_size,
+    "All components in the original class should be in the new class");
+
+  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_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.generic_type_variables())
+  {
+    if(!first)
+      new_tag_buffer << ",";
+    first=false;
+
+    INVARIANT(
+      is_java_generic_inst_parameter(param),
+      "Only create full concretized generic types");
+    new_tag_buffer << param.subtype().get(ID_identifier);
+  }
+
+  new_tag_buffer << ">";
+
+  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/test.desc

@@ -0,0 +1,38 @@
+/*******************************************************************\
+
+ Module: Generate Java Generic Type - Instantiate a generic class with
+         concrete type information.
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+#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>
+#include <util/std_types.h>
+#include <java_bytecode/java_types.h>
+
+class generate_java_generic_typet
+{
+public:
+  generate_java_generic_typet(
+    message_handlert &message_handler);
+
+  symbolt operator()(
+    const java_generic_typet &existing_generic_type,
+    symbol_tablet &symbol_table) const;
+private:
+  irep_idt build_generic_tag(
+    const java_generic_typet &existing_generic_type,
+    const java_class_typet &original_class) const;
+
+  message_handlert &message_handler;
+};
+
+void instantiate_generics(
+  message_handlert &message_handler,
+  symbol_tablet &symbol_table);
+
+#endif // CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H

src/java_bytecode/Makefile

@@ -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

src/java_bytecode/java_bytecode_instrument.cpp

@@ -67,7 +67,8 @@ const std::string java_class_to_package(const std::string &canonical_classname)
 void generate_class_stub(
   const irep_idt &class_name,
   symbol_tablet &symbol_table,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const struct_union_typet::componentst &componentst)
 {
   class_typet class_type;
 
@@ -100,6 +101,7 @@ void generate_class_stub(
   {
     // create the class identifier etc
     java_root_class(res.first);
+    java_add_components_to_class(res.first, componentst);
   }
 }
 
@@ -230,3 +232,22 @@ size_t find_closing_delimiter(
   // did not find corresponding closing '>'
   return std::string::npos;
 }
+
+/// Add the components in components_to_add to the class denoted by
+/// class symbol.
+/// \param class_symbol The symbol representing the class we want to modify.
+/// \param components_to_add The vector with the components we want to add.
+void java_add_components_to_class(
+  symbolt &class_symbol,
+  const struct_union_typet::componentst &components_to_add)
+{
+  PRECONDITION(class_symbol.is_type);
+  PRECONDITION(class_symbol.type.id()==ID_struct);
+  struct_typet &struct_type=to_struct_type(class_symbol.type);
+  struct_typet::componentst &components=struct_type.components();
+
+  for(const struct_union_typet::componentt &component : components_to_add)
+  {
+    components.push_back(component);
+  }
+}