Merge pull request #3530 from allredj/java-struct-tag2

Java now uses struct_tag types (2nd edition)

Author: Joel Allred

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -65,7 +65,7 @@ ci_lazy_methodst::ci_lazy_methodst(
 ///   class
 static bool references_class_model(const exprt &expr)
 {
-  static const symbol_typet class_type("java::java.lang.Class");
+  static const struct_tag_typet class_type("java::java.lang.Class");
 
   for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
   {

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -101,7 +101,7 @@ void ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(
   const pointer_typet &pointer_type,
   const namespacet &ns)
 {
-  const symbol_typet &class_type = to_symbol_type(pointer_type.subtype());
+  const auto &class_type = to_struct_tag_type(pointer_type.subtype());
   const auto &param_classid = class_type.get_identifier();
 
   // Note here: different arrays may have different element types, so we should
@@ -139,10 +139,10 @@ void ci_lazy_methods_neededt::gather_field_types(
   {
     // If class_type is not a symbol this may be a reference array,
     // but we can't tell what type.
-    if(class_type.id() == ID_symbol_type)
+    if(class_type.id() == ID_struct_tag)
     {
       const typet &element_type =
-        java_array_element_type(to_symbol_type(class_type));
+        java_array_element_type(to_struct_tag_type(class_type));
       if(element_type.id() == ID_pointer)
       {
         // This is a reference array -- mark its element type available.
@@ -154,11 +154,11 @@ void ci_lazy_methods_neededt::gather_field_types(
   {
     for(const auto &field : underlying_type.components())
     {
-      if(field.type().id() == ID_struct || field.type().id() == ID_symbol_type)
+      if(field.type().id() == ID_struct || field.type().id() == ID_struct_tag)
         gather_field_types(field.type(), ns);
       else if(field.type().id() == ID_pointer)
       {
-        if(field.type().subtype().id() == ID_symbol_type)
+        if(field.type().subtype().id() == ID_struct_tag)
         {
           add_all_needed_classes(to_pointer_type(field.type()));
         }

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp

@@ -136,29 +136,30 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
 /// in the form of a symbol rather than a pointer (as opposed to the function
 /// insert_pairs_for_pointer). Own the keys and pop from their stack
 /// on destruction; otherwise do nothing.
-/// \param symbol_type symbol type to get the specialized generic types from
+/// \param struct_tag_type symbol type to get the specialized generic types from
 /// \param symbol_struct struct type of the symbol type, must be generic if
 /// the symbol is generic
 void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
-  const symbol_typet &symbol_type,
+  const struct_tag_typet &struct_tag_type,
   const typet &symbol_struct)
 {
   // If the struct is:
   // - an incomplete class or
   // - a class that is neither generic nor implicitly generic (this
   //  may be due to unsupported class signature)
-  // then ignore the generic types in the symbol_type and do not add any pairs.
+  // then ignore the generic types in the struct_tag_type and do not add any
+  // pairs.
   // TODO TG-1996 should decide how mocking and generics should work
   // together. Currently an incomplete class is never marked as generic. If
   // this changes in TG-1996 then the condition below should be updated.
   if(
-    is_java_generic_symbol_type(symbol_type) &&
+    is_java_generic_struct_tag_type(struct_tag_type) &&
     !to_java_class_type(symbol_struct).get_is_stub() &&
     (is_java_generic_class_type(symbol_struct) ||
      is_java_implicitly_generic_class_type(symbol_struct)))
   {
-    const java_generic_symbol_typet &generic_symbol =
-      to_java_generic_symbol_type(symbol_type);
+    const java_generic_struct_tag_typet &generic_symbol =
+      to_java_generic_struct_tag_type(struct_tag_type);
 
     const std::vector<java_generic_parametert> &generic_parameters =
       get_all_generic_parameters(symbol_struct);

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h

@@ -1,3 +1,4 @@
+
 /// Author: Diffblue Ltd.
 
 #ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
@@ -50,9 +51,8 @@ class generic_parameter_specialization_map_keyst
   void insert_pairs_for_pointer(
     const pointer_typet &pointer_type,
     const typet &pointer_subtype_struct);
-  void insert_pairs_for_symbol(
-    const symbol_typet &symbol_type,
-    const typet &symbol_struct);
+  void
+  insert_pairs_for_symbol(const struct_tag_typet &, const typet &symbol_struct);
 
 private:
   /// Generic parameter specialization map to modify

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -230,7 +230,7 @@ static void instrument_synchronized_code(
 
   // Create the finally block with the same label targeted in the catch-push
   const symbolt &tmp_symbol = get_fresh_aux_symbol(
-    java_reference_type(symbol_typet("java::java.lang.Throwable")),
+    java_reference_type(struct_tag_typet("java::java.lang.Throwable")),
     id2string(symbol.name),
     "caught-synchronized-exception",
     code.source_location(),

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -338,7 +338,7 @@ void java_bytecode_convert_classt::convert(
 
   if(!c.super_class.empty())
   {
-    const symbol_typet base("java::" + id2string(c.super_class));
+    const struct_tag_typet base("java::" + id2string(c.super_class));
 
     // if the superclass is generic then the class has the superclass reference
     // including the generic info in its signature
@@ -350,7 +350,7 @@ void java_bytecode_convert_classt::convert(
     {
       try
       {
-        const java_generic_symbol_typet generic_base(
+        const java_generic_struct_tag_typet generic_base(
           base, superclass_ref.value(), qualified_classname);
         class_type.add_base(generic_base);
       }
@@ -378,7 +378,7 @@ void java_bytecode_convert_classt::convert(
   // interfaces are recorded as bases
   for(const auto &interface : c.implements)
   {
-    const symbol_typet base("java::" + id2string(interface));
+    const struct_tag_typet base("java::" + id2string(interface));
 
     // if the interface is generic then the class has the interface reference
     // including the generic info in its signature
@@ -390,7 +390,7 @@ void java_bytecode_convert_classt::convert(
     {
       try
       {
-        const java_generic_symbol_typet generic_base(
+        const java_generic_struct_tag_typet generic_base(
           base, interface_ref.value(), qualified_classname);
         class_type.add_base(generic_base);
       }
@@ -774,26 +774,27 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
   for(const char l : letters)
   {
-    symbol_typet symbol_type=
-      to_symbol_type(java_array_type(l).subtype());
+    struct_tag_typet struct_tag_type =
+      to_struct_tag_type(java_array_type(l).subtype());
 
-    const irep_idt &symbol_type_identifier=symbol_type.get_identifier();
-    if(symbol_table.has_symbol(symbol_type_identifier))
+    const irep_idt &struct_tag_type_identifier =
+      struct_tag_type.get_identifier();
+    if(symbol_table.has_symbol(struct_tag_type_identifier))
       return;
 
     java_class_typet class_type;
     // we have the base class, java.lang.Object, length and data
     // of appropriate type
-    class_type.set_tag(symbol_type_identifier);
+    class_type.set_tag(struct_tag_type_identifier);
     // Note that non-array types don't have "java::" at the beginning of their
     // tag, and their name is "java::" + their tag. Since arrays do have
     // "java::" at the beginning of their tag we set the name to be the same as
     // the tag.
-    class_type.set_name(symbol_type_identifier);
+    class_type.set_name(struct_tag_type_identifier);
 
     class_type.components().reserve(3);
     class_typet::componentt base_class_component(
-      "@java.lang.Object", symbol_typet("java::java.lang.Object"));
+      "@java.lang.Object", struct_tag_typet("java::java.lang.Object"));
     base_class_component.set_pretty_name("@java.lang.Object");
     base_class_component.set_base_name("@java.lang.Object");
     class_type.components().push_back(base_class_component);
@@ -809,16 +810,16 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     data_component.set_base_name("data");
     class_type.components().push_back(data_component);
 
-    class_type.add_base(symbol_typet("java::java.lang.Object"));
+    class_type.add_base(struct_tag_typet("java::java.lang.Object"));
 
     INVARIANT(
       is_valid_java_array(class_type),
       "Constructed a new type representing a Java Array "
       "object that doesn't match expectations");
 
     symbolt symbol;
-    symbol.name=symbol_type_identifier;
-    symbol.base_name=symbol_type.get(ID_C_base_name);
+    symbol.name = struct_tag_type_identifier;
+    symbol.base_name = struct_tag_type.get(ID_C_base_name);
     symbol.is_type=true;
     symbol.type = class_type;
     symbol.mode = ID_java;
@@ -827,13 +828,13 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     // Also provide a clone method:
     // ----------------------------
 
-    const irep_idt clone_name=
-      id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;";
+    const irep_idt clone_name =
+      id2string(struct_tag_type_identifier) + ".clone:()Ljava/lang/Object;";
     java_method_typet::parametert this_param;
     this_param.set_identifier(id2string(clone_name)+"::this");
     this_param.set_base_name("this");
     this_param.set_this();
-    this_param.type()=java_reference_type(symbol_type);
+    this_param.type() = java_reference_type(struct_tag_type);
     const java_method_typet clone_type({this_param}, java_lang_object_type());
 
     parameter_symbolt this_symbol;
@@ -850,7 +851,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     local_symbol.name=local_name;
     local_symbol.base_name="cloned_array";
     local_symbol.pretty_name=local_symbol.base_name;
-    local_symbol.type=java_reference_type(symbol_type);
+    local_symbol.type = java_reference_type(struct_tag_type);
     local_symbol.mode=ID_java;
     symbol_table.add(local_symbol);
     const auto &local_symexpr=local_symbol.symbol_expr();
@@ -860,9 +861,9 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     source_locationt location;
     location.set_function(local_name);
     side_effect_exprt java_new_array(
-      ID_java_new_array, java_reference_type(symbol_type), location);
-    dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
-    dereference_exprt new_array(local_symexpr, symbol_type);
+      ID_java_new_array, java_reference_type(struct_tag_type), location);
+    dereference_exprt old_array(this_symbol.symbol_expr(), struct_tag_type);
+    dereference_exprt new_array(local_symexpr, struct_tag_type);
     member_exprt old_length(
       old_array, length_component.get_name(), length_component.type());
     java_new_array.copy_to_operands(old_length);
@@ -923,8 +924,8 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
     symbolt clone_symbol;
     clone_symbol.name=clone_name;
-    clone_symbol.pretty_name=
-      id2string(symbol_type_identifier)+".clone:()";
+    clone_symbol.pretty_name =
+      id2string(struct_tag_type_identifier) + ".clone:()";
     clone_symbol.base_name="clone";
     clone_symbol.type=clone_type;
     clone_symbol.value=clone_body;
@@ -1053,9 +1054,10 @@ static void find_and_replace_parameters(
       find_and_replace_parameters(argument, replacement_parameters);
     }
   }
-  else if(is_java_generic_symbol_type(type))
+  else if(is_java_generic_struct_tag_type(type))
   {
-    java_generic_symbol_typet &generic_base = to_java_generic_symbol_type(type);
+    java_generic_struct_tag_typet &generic_base =
+      to_java_generic_struct_tag_type(type);
     std::vector<reference_typet> &gen_types = generic_base.generic_types();
     for(auto &gen_type : gen_types)
     {

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -380,8 +380,8 @@ void java_bytecode_convert_method_lazy(
   {
     java_method_typet::parameterst &parameters = member_type.parameters();
     java_method_typet::parametert this_p;
-    const reference_typet object_ref_type=
-      java_reference_type(symbol_typet(class_symbol.name));
+    const reference_typet object_ref_type =
+      java_reference_type(struct_tag_typet(class_symbol.name));
     this_p.type()=object_ref_type;
     this_p.set_this();
     parameters.insert(parameters.begin(), this_p);
@@ -655,7 +655,7 @@ static irep_idt get_if_cmp_operator(const irep_idt &stmt)
 
 static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
 {
-  symbol_typet class_type(fieldref.get(ID_class));
+  struct_tag_typet class_type(fieldref.get(ID_class));
 
   const typecast_exprt pointer2(pointer, java_reference_type(class_type));
 
@@ -1181,9 +1181,11 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     {
       if(cur_pc==it->handler_pc)
       {
-        if(catch_type != typet() || it->catch_type == symbol_typet(irep_idt()))
+        if(
+          catch_type != typet() ||
+          it->catch_type == struct_tag_typet(irep_idt()))
         {
-          catch_type=symbol_typet("java::java.lang.Throwable");
+          catch_type = struct_tag_typet("java::java.lang.Throwable");
           break;
         }
         else
@@ -1617,7 +1619,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       const typecast_exprt pointer(op[0], java_array_type(statement[0]));
 
       dereference_exprt array(pointer, pointer.type().subtype());
-      PRECONDITION(pointer.type().subtype().id() == ID_symbol_type);
+      PRECONDITION(pointer.type().subtype().id() == ID_struct_tag);
       array.set(ID_java_member_access, true);
 
       const member_exprt length(array, "length", java_int_type());
@@ -2088,7 +2090,7 @@ void java_bytecode_convert_methodt::convert_invoke(
     if(parameters.empty() || !parameters[0].get_this())
     {
       irep_idt classname = arg0.get(ID_C_class);
-      typet thistype = symbol_typet(classname);
+      typet thistype = struct_tag_typet(classname);
       // Note invokespecial is used for super-method calls as well as
       // constructors.
       if(statement == "invokespecial")
@@ -2504,7 +2506,7 @@ void java_bytecode_convert_methodt::convert_new(
   c = code_assignt(tmp, java_new_expr);
   c.add_source_location() = location;
   codet clinit_call =
-    get_clinit_call(to_symbol_type(arg0.type()).get_identifier());
+    get_clinit_call(to_struct_tag_type(arg0.type()).get_identifier());
   if(clinit_call.get_statement() != ID_skip)
   {
     c = code_blockt({clinit_call, c});
@@ -2518,10 +2520,10 @@ code_blockt java_bytecode_convert_methodt::convert_putstatic(
   const exprt::operandst &op,
   const symbol_exprt &symbol_expr)
 {
-  if(needed_lazy_methods && arg0.type().id() == ID_symbol_type)
+  if(needed_lazy_methods && arg0.type().id() == ID_struct_tag)
   {
     needed_lazy_methods->add_needed_class(
-      to_symbol_type(arg0.type()).get_identifier());
+      to_struct_tag_type(arg0.type()).get_identifier());
   }
 
   code_blockt block;
@@ -2566,18 +2568,18 @@ void java_bytecode_convert_methodt::convert_getstatic(
 {
   if(needed_lazy_methods)
   {
-    if(arg0.type().id() == ID_symbol_type)
+    if(arg0.type().id() == ID_struct_tag)
     {
       needed_lazy_methods->add_needed_class(
-        to_symbol_type(arg0.type()).get_identifier());
+        to_struct_tag_type(arg0.type()).get_identifier());
     }
     else if(arg0.type().id() == ID_pointer)
     {
       const auto &pointer_type = to_pointer_type(arg0.type());
-      if(pointer_type.subtype().id() == ID_symbol_type)
+      if(pointer_type.subtype().id() == ID_struct_tag)
       {
         needed_lazy_methods->add_needed_class(
-          to_symbol_type(pointer_type.subtype()).get_identifier());
+          to_struct_tag_type(pointer_type.subtype()).get_identifier());
       }
     }
     else if(is_assertions_disabled_field)

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -108,8 +108,7 @@ code_ifthenelset java_bytecode_instrumentt::throw_exception(
       struct_union_typet::componentst{});
   }
 
-  pointer_typet exc_ptr_type=
-    pointer_type(symbol_typet(exc_class_name));
+  pointer_typet exc_ptr_type = pointer_type(struct_tag_typet(exc_class_name));
 
   // Allocate and throw an instance of the exception class:
 

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -362,7 +362,7 @@ static void infer_opaque_type_fields(
 static symbol_exprt get_or_create_class_literal_symbol(
   const irep_idt &class_id, symbol_tablet &symbol_table)
 {
-  symbol_typet java_lang_Class("java::java.lang.Class");
+  struct_tag_typet java_lang_Class("java::java.lang.Class");
   symbol_exprt symbol_expr(
     id2string(class_id) + JAVA_CLASS_MODEL_SUFFIX,
     java_lang_Class);

jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -105,8 +105,8 @@ java_bytecode_parse_treet::find_annotation(
       if(annotation.type.id() != ID_pointer)
         return false;
       const typet &type = annotation.type.subtype();
-      return type.id() == ID_symbol_type &&
-             to_symbol_type(type).get_identifier() == annotation_type_name;
+      return type.id() == ID_struct_tag &&
+             to_struct_tag_type(type).get_identifier() == annotation_type_name;
     });
   if(annotation_it == annotations.end())
     return {};