[TG-1422] Bugfix for a precondition fail in the interpreter after generics support has been introduced

src/goto-programs/interpreter_evaluate.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/pointer_offset_size.h>
 #include <string.h>
+#include <java_bytecode/java_types.h>
 
 /// Reads a memory address and loads it into the `dest` variable.
 /// Marks cell as `READ_BEFORE_WRITTEN` if cell has never been written.
@@ -1196,7 +1197,15 @@ mp_integer interpretert::evaluate_address(
     if(expr.operands().size()!=1)
       throw "typecast expects one operand";
 
-    PRECONDITION(expr.type().id()==ID_pointer);
+    PRECONDITION(expr.type().id()==ID_pointer ||
+      // with generics support, we get some weird typecast expressions,
+      // in the goto program, where the first operand is typecast into a
+      // struct that resembles the same type, and is of type "struct" instead
+      // "pointer" so the precondition above would fail. This makes sure to
+      // proceed the evaluation in the case where the operand is a generic
+      // instantiated type.
+      (expr.type().id()==ID_struct &&
+        java_is_specialised_generic_class_type(expr.op0().type())));
 
     return evaluate_address(expr.op0(), fail_quietly);
   }

src/java_bytecode/generate_java_generic_type.cpp

@@ -13,7 +13,7 @@
 
 generate_java_generic_typet::generate_java_generic_typet(
   message_handlert &message_handler):
-    message_handler(message_handler)
+  message_handler(message_handler)
 {}
 
 /// Generate a concrete instantiation of a generic type.
@@ -32,25 +32,23 @@ symbolt generate_java_generic_typet::operator()(
 
   INVARIANT(
     pointer_subtype.id()==ID_struct, "Only pointers to classes in java");
-  INVARIANT(
-    is_java_generic_class_type(pointer_subtype),
-    "Generic references type must be a generic class");
-
-  const java_generic_class_typet &generic_class_definition =
-    to_java_generic_class_type(to_java_class_type(pointer_subtype));
 
-  const irep_idt new_tag =
-    build_generic_tag(existing_generic_type, generic_class_definition);
-  struct_union_typet::componentst replacement_components =
-    generic_class_definition.components();
+  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) {
 
       component.type() = substitute_type(
-        component.type(), generic_class_definition, existing_generic_type);
+        component.type(),
+        to_java_generic_class_type(replacement_type),
+        existing_generic_type);
 
       return component;
     };
@@ -63,27 +61,51 @@ symbolt generate_java_generic_typet::operator()(
     replacement_components.end(),
     replace_type_for_generic_field);
 
-  std::size_t after_modification_size =
-    generic_class_definition.components().size();
+  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 java_class_typet &new_java_class = construct_specialised_generic_type(
-    generic_class_definition, new_tag, replacement_components);
-  const type_symbolt &class_symbol =
-    build_symbol_from_specialised_class(new_java_class);
-
-  std::pair<symbolt &, bool> res = symbol_table.insert(std::move(class_symbol));
-  if(!res.second)
+  const auto expected_symbol="java::"+id2string(new_tag);
+//
+//  generate_class_stub(
+//    new_tag,
+//    symbol_table,
+//    message_handler,
+//    replacement_components);
+
+  // inlined the generate_class_stub for now
   {
-    messaget message(message_handler);
-    message.warning() << "stub class symbol " << class_symbol.name
-                      << " already exists" << messaget::eom;
+    java_specialised_generic_class_typet specialised_class;
+    specialised_class.set_tag(replacement_type.get_tag());
+    // NOTE: the tag absolutely has to be BasicGeneric
+    specialised_class.set(ID_base_name, new_tag);
+
+    // produce class symbol
+    symbolt new_symbol;
+    new_symbol.base_name = new_tag;
+    new_symbol.pretty_name = new_tag;
+    new_symbol.name = "java::" + id2string(new_tag);
+    specialised_class.set(ID_name, new_symbol.name);
+    new_symbol.type = specialised_class;
+    new_symbol.mode = ID_java;
+    new_symbol.is_type = true;
+
+    std::pair<symbolt &, bool> res = symbol_table.insert(std::move(new_symbol));
+
+    if(!res.second)
+    {
+      messaget message(message_handler);
+      message.warning() << "stub class symbol " << new_symbol.name
+                        << " already exists" << messaget::eom;
+    }
+    else
+    {
+      java_add_components_to_class(res.first, replacement_components);
+    }
   }
-
-  const auto expected_symbol="java::"+id2string(new_tag);
   auto symbol=symbol_table.lookup(expected_symbol);
   INVARIANT(symbol, "New class not created");
   return *symbol;
@@ -109,16 +131,25 @@ typet generate_java_generic_typet::substitute_type(
   if(is_java_generic_parameter(parameter_type))
   {
     auto component_identifier = to_java_generic_parameter(parameter_type)
-                                  .type_variable()
-                                  .get_identifier();
+      .type_variable()
+      .get_identifier();
 
     optionalt<size_t> results =
       java_generics_get_index_for_subtype(generic_class, component_identifier);
 
     INVARIANT(results.has_value(), "generic component type not found");
-    return generic_reference.generic_type_arguments()[*results];
+
+    if(results)
+    {
+      return generic_reference.generic_type_variables()[*results];
+    }
+    else
+    {
+      return parameter_type;
+    }
   }
-  else if(parameter_type.id() == ID_pointer)
+  else if(
+    parameter_type.id() == ID_pointer)
   {
     if(is_java_generic_type(parameter_type))
     {
@@ -132,8 +163,8 @@ typet generate_java_generic_typet::substitute_type(
         generic_type.generic_type_arguments().begin(),
         generic_type.generic_type_arguments().end(),
         std::back_inserter(replaced_type_variables),
-        [&](const reference_typet &generic_param) -> reference_typet
-        {
+        [&](const java_generic_parametert &generic_param)
+          -> java_generic_parametert {
           const typet &replacement_type =
             substitute_type(generic_param, generic_class, generic_reference);
 
@@ -148,12 +179,13 @@ typet generate_java_generic_typet::substitute_type(
             INVARIANT(
               is_reference(replacement_type),
               "All generic parameters should be references");
-            return to_reference_type(replacement_type);
+            return java_generic_inst_parametert(
+              to_symbol_type(replacement_type.subtype()));
           }
         });
 
-      java_generic_typet new_type = generic_type;
-      new_type.generic_type_arguments() = replaced_type_variables;
+      java_generic_typet new_type=generic_type;
+      new_type.generic_type_variables()=replaced_type_variables;
       return new_type;
     }
     else if(parameter_type.subtype().id() == ID_symbol)
@@ -162,14 +194,14 @@ typet generate_java_generic_typet::substitute_type(
         to_symbol_type(parameter_type.subtype());
       if(is_java_array_tag(array_subtype.get_identifier()))
       {
-        const typet &array_element_type =
-          java_array_element_type(array_subtype);
+        const typet &array_element_type = java_array_element_type(array_subtype);
 
         const typet &new_array_type =
           substitute_type(array_element_type, generic_class, generic_reference);
 
         typet replacement_array_type = java_array_type('a');
-        replacement_array_type.subtype().set(ID_C_element_type, new_array_type);
+        replacement_array_type.subtype().set(
+          ID_C_element_type, new_array_type);
         return replacement_array_type;
       }
     }
@@ -199,62 +231,10 @@ irep_idt generate_java_generic_typet::build_generic_tag(
     INVARIANT(
       !is_java_generic_parameter(type_argument),
       "Only create full concretized generic types");
-    const irep_idt &id(id2string(type_argument.subtype().get(ID_identifier)));
-    new_tag_buffer << id2string(id);
-    if(is_java_array_tag(id))
-    {
-      const typet &element_type =
-        java_array_element_type(to_symbol_type(type_argument.subtype()));
-
-      // If this is an array of references then we will specialize its
-      // identifier using the type of the objects in the array. Else, there can
-      // be a problem with the same symbols for different instantiations using
-      // arrays with different types.
-      if(element_type.id() == ID_pointer)
-      {
-        const symbol_typet element_symbol =
-          to_symbol_type(element_type.subtype());
-        new_tag_buffer << "of_" << id2string(element_symbol.get_identifier());
-      }
-    }
+    new_tag_buffer << param.subtype().get(ID_identifier);
   }
 
   new_tag_buffer << ">";
 
   return new_tag_buffer.str();
-}
-
-/// Build the specalised version of the specific class, with the specified
-/// parameters and name.
-/// \param generic_class_definition: The generic class we are specialising
-/// \param new_tag: The new name for the class (like Generic<java::Float>)
-/// \param new_components: The specialised components
-/// \return The newly constructed class.
-java_class_typet
-generate_java_generic_typet::construct_specialised_generic_type(
-  const java_generic_class_typet &generic_class_definition,
-  const irep_idt &new_tag,
-  const struct_typet::componentst &new_components) const
-{
-  java_class_typet specialised_class = generic_class_definition;
-  // We are specialising the logic - so we don't want to be marked as generic
-  specialised_class.set(ID_C_java_generics_class_type, false);
-  specialised_class.set(ID_name, "java::" + id2string(new_tag));
-  specialised_class.set(ID_base_name, new_tag);
-  specialised_class.components() = new_components;
-  return specialised_class;
-}
-
-/// Construct the symbol to be moved into the symbol table
-/// \param specialised_class: The newly constructed specialised class
-/// \return The symbol to add to the symbol table
-type_symbolt generate_java_generic_typet::build_symbol_from_specialised_class(
-  const java_class_typet &specialised_class) const
-{
-  type_symbolt new_symbol(specialised_class);
-  new_symbol.base_name = specialised_class.get(ID_base_name);
-  new_symbol.pretty_name = specialised_class.get(ID_base_name);
-  new_symbol.name = specialised_class.get(ID_name);
-  new_symbol.mode = ID_java;
-  return new_symbol;
-}
+}

src/java_bytecode/java_types.h

@@ -366,4 +366,29 @@ inline const optionalt<size_t> java_generics_get_index_for_subtype(
   return std::distance(gen_types.cbegin(), iter);
 }
 
+class java_specialised_generic_class_typet : public java_class_typet
+{
+  // note the constructor could take the components and construct it itself
+  // note vector of generic parameter of symbol type
+public:
+  // TODO: to be defined more appropriately.
+  java_specialised_generic_class_typet()
+  {
+    set(ID_C_specialised_generic_java_class, true);
+  }
+};
+
+inline const bool java_is_specialised_generic_class_type(const typet &type)
+{
+  return type.get_bool(ID_C_specialised_generic_java_class);
+}
+
+inline java_specialised_generic_class_typet
+to_java_specialised_class_typet(const typet &type)
+{
+  INVARIANT(java_is_specialised_generic_class_type(type),
+            "Tried to convert a type that was not a specialised generic java class");
+  return static_cast<const java_specialised_generic_class_typet &>(type);
+}
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H

src/util/irep_ids.def

@@ -832,6 +832,7 @@ IREP_ID_TWO(C_java_generic_type, #java_generic_type)
 IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type)
 IREP_ID_TWO(generic_types, #generic_types)
 IREP_ID_TWO(type_variables, #type_variables)
+IREP_ID_TWO(C_specialised_generic_java_class, #specialised_class)
 IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)