Merge pull request #3929 from tautschnig/deprecation-nil_typet

Replace use of deprecated nil_typet in java_type_from_string [blocks: #3800]

Author: tautschnig

jbmc/regression/jbmc/stack_var12/stack_typecast.class

@@ -6,14 +6,14 @@
 
 .method public <init>()V
         aload_0
-        invokevirtual java/lang/Object/<init>()V
+        invokespecial java/lang/Object/<init>()V
         return
 .end method
 
 .method public f()I
         .limit stack 6
         .limit locals 1
-        .var 0 is this stack_typecast from begin to end
+        .var 0 is this Lstack_typecast; from begin to end
         .line 0
 begin:
 

jbmc/regression/jbmc/stack_var12/stack_typecast.j

@@ -637,10 +637,8 @@ void java_bytecode_convert_classt::convert(
   typet field_type;
   if(f.signature.has_value())
   {
-    field_type=java_type_from_string_with_exception(
-      f.descriptor,
-      f.signature,
-      id2string(class_symbol.name));
+    field_type = *java_type_from_string_with_exception(
+      f.descriptor, f.signature, id2string(class_symbol.name));
 
     /// this is for a free type variable, e.g., a field of the form `T f;`
     if(is_java_generic_parameter(field_type))
@@ -670,7 +668,7 @@ void java_bytecode_convert_classt::convert(
     }
   }
   else
-    field_type=java_type_from_string(f.descriptor);
+    field_type = *java_type_from_string(f.descriptor);
 
   // is this a static field?
   if(f.is_static)

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -259,21 +259,26 @@ java_method_typet member_type_lazy(
 
   messaget message(message_handler);
 
-  typet member_type_from_descriptor=java_type_from_string(descriptor);
-  INVARIANT(member_type_from_descriptor.id()==ID_code, "Must be code type");
+  auto member_type_from_descriptor = java_type_from_string(descriptor);
+  INVARIANT(
+    member_type_from_descriptor.has_value() &&
+      member_type_from_descriptor->id() == ID_code,
+    "Must be code type");
   if(signature.has_value())
   {
     try
     {
-      typet member_type_from_signature=java_type_from_string(
-        signature.value(),
-        class_name);
-      INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type");
+      auto member_type_from_signature =
+        java_type_from_string(signature.value(), class_name);
+      INVARIANT(
+        member_type_from_signature.has_value() &&
+          member_type_from_signature->id() == ID_code,
+        "Must be code type");
       if(
-        to_java_method_type(member_type_from_signature).parameters().size() ==
-        to_java_method_type(member_type_from_descriptor).parameters().size())
+        to_java_method_type(*member_type_from_signature).parameters().size() ==
+        to_java_method_type(*member_type_from_descriptor).parameters().size())
       {
-        return to_java_method_type(member_type_from_signature);
+        return to_java_method_type(*member_type_from_signature);
       }
       else
       {
@@ -294,7 +299,7 @@ java_method_typet member_type_lazy(
                         << message.eom;
     }
   }
-  return to_java_method_type(member_type_from_descriptor);
+  return to_java_method_type(*member_type_from_descriptor);
 }
 
 /// Retrieves the symbol of the lambda method associated with the given
@@ -460,24 +465,10 @@ void java_bytecode_convert_methodt::convert(
     if(!is_parameter(v))
       continue;
 
-    // Construct a fully qualified name for the parameter v,
-    // e.g. my.package.ClassName.myMethodName:(II)I::anIntParam, and then a
-    // symbol_exprt with the parameter and its type
-    typet t;
-    if(v.signature.has_value())
-    {
-      t=java_type_from_string_with_exception(
-        v.descriptor,
-        v.signature,
-        id2string(class_symbol.name));
-    }
-    else
-      t=java_type_from_string(v.descriptor);
-
     std::ostringstream id_oss;
     id_oss << method_id << "::" << v.name;
     irep_idt identifier(id_oss.str());
-    symbol_exprt result(identifier, t);
+    symbol_exprt result = symbol_exprt::typeless(identifier);
     result.set(ID_C_base_name, v.name);
 
     // Create a new variablet in the variables vector; in fact this entry will

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -100,7 +100,7 @@ class java_bytecode_parsert:public parsert
 
   const typet type_entry(u2 index)
   {
-    return java_type_from_string(id2string(pool_entry(index).s));
+    return *java_type_from_string(id2string(pool_entry(index).s));
   }
 
   void populate_bytecode_mnemonics_table()
@@ -547,10 +547,8 @@ void java_bytecode_parsert::get_class_refs()
       break;
 
     case CONSTANT_NameAndType:
-      {
-        typet t=java_type_from_string(id2string(pool_entry(c.ref2).s));
-        get_class_refs_rec(t);
-      }
+      get_class_refs_rec(
+        *java_type_from_string(id2string(pool_entry(c.ref2).s)));
       break;
 
     default: {}
@@ -562,59 +560,63 @@ void java_bytecode_parsert::get_class_refs()
   for(const auto &field : parse_tree.parsed_class.fields)
   {
     get_annotation_class_refs(field.annotations);
-    typet field_type;
+
     if(field.signature.has_value())
     {
-      field_type=java_type_from_string_with_exception(
+      typet field_type = *java_type_from_string_with_exception(
         field.descriptor,
         field.signature,
-        "java::"+id2string(parse_tree.parsed_class.name));
+        "java::" + id2string(parse_tree.parsed_class.name));
 
       // add generic type args to class refs as dependencies, same below for
       // method types and entries from the local variable type table
       get_dependencies_from_generic_parameters(
         field_type, parse_tree.class_refs);
+      get_class_refs_rec(field_type);
     }
     else
-      field_type=java_type_from_string(field.descriptor);
-
-    get_class_refs_rec(field_type);
+    {
+      get_class_refs_rec(*java_type_from_string(field.descriptor));
+    }
   }
 
   for(const auto &method : parse_tree.parsed_class.methods)
   {
     get_annotation_class_refs(method.annotations);
     for(const auto &parameter_annotations : method.parameter_annotations)
       get_annotation_class_refs(parameter_annotations);
-    typet method_type;
+
     if(method.signature.has_value())
     {
-      method_type=java_type_from_string_with_exception(
+      typet method_type = *java_type_from_string_with_exception(
         method.descriptor,
         method.signature,
-        "java::"+id2string(parse_tree.parsed_class.name));
+        "java::" + id2string(parse_tree.parsed_class.name));
       get_dependencies_from_generic_parameters(
         method_type, parse_tree.class_refs);
+      get_class_refs_rec(method_type);
     }
     else
-      method_type=java_type_from_string(method.descriptor);
+    {
+      get_class_refs_rec(*java_type_from_string(method.descriptor));
+    }
 
-    get_class_refs_rec(method_type);
     for(const auto &var : method.local_variable_table)
     {
-      typet var_type;
       if(var.signature.has_value())
       {
-        var_type=java_type_from_string_with_exception(
+        typet var_type = *java_type_from_string_with_exception(
           var.descriptor,
           var.signature,
-          "java::"+id2string(parse_tree.parsed_class.name));
+          "java::" + id2string(parse_tree.parsed_class.name));
         get_dependencies_from_generic_parameters(
           var_type, parse_tree.class_refs);
+        get_class_refs_rec(var_type);
       }
       else
-        var_type=java_type_from_string(var.descriptor);
-      get_class_refs_rec(var_type);
+      {
+        get_class_refs_rec(*java_type_from_string(var.descriptor));
+      }
     }
   }
 }
@@ -672,8 +674,7 @@ void java_bytecode_parsert::get_annotation_value_class_refs(const exprt &value)
   if(const auto &symbol_expr = expr_try_dynamic_cast<symbol_exprt>(value))
   {
     const irep_idt &value_id = symbol_expr->get_identifier();
-    const typet value_type = java_type_from_string(id2string(value_id));
-    get_class_refs_rec(value_type);
+    get_class_refs_rec(*java_type_from_string(id2string(value_id)));
   }
   else if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(value))
   {

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -267,14 +267,14 @@ bool is_java_main(const symbolt &function)
 {
   bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD);
   const java_method_typet &function_type = to_java_method_type(function.type);
-  const typet &string_array_type = java_type_from_string("[Ljava/lang/String;");
+  const auto string_array_type = java_type_from_string("[Ljava/lang/String;");
   // checks whether the function is static and has a single String[] parameter
   bool is_static = !function_type.has_this();
   // this should be implied by the signature
   const java_method_typet::parameterst &parameters = function_type.parameters();
   bool has_correct_type = function_type.return_type().id() == ID_empty &&
                           parameters.size() == 1 &&
-                          parameters[0].type().full_eq(string_array_type);
+                          parameters[0].type().full_eq(*string_array_type);
   bool public_access = function_type.get(ID_access) == ID_public;
   return named_main && is_static && has_correct_type && public_access;
 }

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -794,9 +794,9 @@ void java_bytecode_convert_methodt::setup_local_variables(
     const std::string class_name = method_name.substr(0, class_name_end);
 
     const typet t = v.var.signature.has_value()
-                      ? java_type_from_string_with_exception(
+                      ? *java_type_from_string_with_exception(
                           v.var.descriptor, v.var.signature, class_name)
-                      : java_type_from_string(v.var.descriptor);
+                      : *java_type_from_string(v.var.descriptor);
 
     std::ostringstream id_oss;
     id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name;