Replace use of deprecated nil_typet in java_type_from_string

Use optionalt<typet> as recommended in the deprecation note.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -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_method.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_parser.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()
@@ -548,8 +548,8 @@ void java_bytecode_parsert::get_class_refs()
 
     case CONSTANT_NameAndType:
       {
-        typet t=java_type_from_string(id2string(pool_entry(c.ref2).s));
-        get_class_refs_rec(t);
+        const auto t = java_type_from_string(id2string(pool_entry(c.ref2).s));
+        get_class_refs_rec(*t);
       }
       break;
 
@@ -562,59 +562,57 @@ 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);
+    else if(const auto field_type = java_type_from_string(field.descriptor))
+      get_class_refs_rec(*field_type);
   }
 
   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);
+    else if(const auto method_type = java_type_from_string(method.descriptor))
+      get_class_refs_rec(*method_type);
 
-    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);
+      else if(const auto var_type = java_type_from_string(var.descriptor))
+        get_class_refs_rec(*var_type);
     }
   }
 }
@@ -672,8 +670,9 @@ 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);
+    const auto value_type = java_type_from_string(id2string(value_id));
+    if(value_type.has_value())
+      get_class_refs_rec(*value_type);
   }
   else if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(value))
   {

jbmc/src/java_bytecode/java_entry_point.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_local_variable_table.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;

jbmc/src/java_bytecode/java_types.cpp

@@ -350,9 +350,9 @@ std::vector<typet> parse_list_types(
   for(const std::string &raw_type :
       parse_raw_list_types(src, opening_bracket, closing_bracket))
   {
-    const typet new_type = java_type_from_string(raw_type, class_name_prefix);
-    INVARIANT(new_type != nil_typet(), "Failed to parse type");
-    type_list.push_back(new_type);
+    auto new_type = java_type_from_string(raw_type, class_name_prefix);
+    INVARIANT(new_type.has_value(), "Failed to parse type");
+    type_list.push_back(std::move(*new_type));
   }
   return type_list;
 }
@@ -500,12 +500,12 @@ size_t find_closing_semi_colon_for_reference_type(
 /// \param class_name_prefix: name of class to append to generic type
 ///   variables/parameters
 /// \return internal type representation for GOTO programs
-typet java_type_from_string(
+optionalt<typet> java_type_from_string(
   const std::string &src,
   const std::string &class_name_prefix)
 {
   if(src.empty())
-    return nil_typet();
+    return {};
 
   // a java type is encoded in different ways
   //  - a method type is encoded as '(...)R' where the parenthesis include the
@@ -549,15 +549,15 @@ typet java_type_from_string(
           "Cannot currently parse bounds on generic types");
       }
 
-      const typet &method_type=java_type_from_string(
-        src.substr(closing_generic+1, std::string::npos), class_name_prefix);
+      auto method_type = java_type_from_string(
+        src.substr(closing_generic + 1, std::string::npos), class_name_prefix);
 
       // This invariant being violated means that tkiley has not understood
       // part of the signature spec.
       // Only class and method signatures can start with a '<' and classes are
       // handled separately.
       INVARIANT(
-        method_type.id()==ID_code,
+        method_type.has_value() && method_type->id() == ID_code,
         "This should correspond to method signatures only");
 
       return method_type;
@@ -566,9 +566,9 @@ typet java_type_from_string(
     {
       std::size_t e_pos=src.rfind(')');
       if(e_pos==std::string::npos)
-        return nil_typet();
+        return {};
 
-      typet return_type = java_type_from_string(
+      auto return_type = java_type_from_string(
         std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
 
       std::vector<typet> param_types =
@@ -582,26 +582,25 @@ typet java_type_from_string(
         std::back_inserter(parameters),
         [](const typet &type) { return java_method_typet::parametert(type); });
 
-      return java_method_typet(std::move(parameters), std::move(return_type));
+      return java_method_typet(std::move(parameters), std::move(*return_type));
     }
 
   case '[': // array type
     {
       // If this is a reference array, we generate a plain array[reference]
       // with void* members, but note the real type in ID_element_type.
       if(src.size()<=1)
-        return nil_typet();
+        return {};
       char subtype_letter=src[1];
-      const typet subtype=
-        java_type_from_string(src.substr(1, std::string::npos),
-                              class_name_prefix);
+      auto subtype = java_type_from_string(
+        src.substr(1, std::string::npos), class_name_prefix);
       if(subtype_letter=='L' || // [L denotes a reference array of some sort.
          subtype_letter=='[' || // Array-of-arrays
          subtype_letter=='T')   // Array of generic types
         subtype_letter='A';
       typet tmp=java_array_type(std::tolower(subtype_letter));
-      tmp.subtype().set(ID_element_type, subtype);
-      return tmp;
+      tmp.subtype().set(ID_element_type, std::move(*subtype));
+      return std::move(tmp);
     }
 
   case 'B': return java_byte_type();
@@ -622,7 +621,7 @@ typet java_type_from_string(
     return java_generic_parametert(
       type_var_name,
       to_struct_tag_type(
-        java_type_from_string("Ljava/lang/Object;").subtype()));
+        java_type_from_string("Ljava/lang/Object;")->subtype()));
   }
   case 'L':
     {
@@ -638,7 +637,7 @@ typet java_type_from_string(
     throw unsupported_java_class_signature_exceptiont("wild card generic");
   }
   default:
-    return nil_typet();
+    return {};
   }
 }
 
@@ -723,7 +722,7 @@ std::vector<typet> java_generic_type_from_string(
     java_generic_parametert type_var_type(
       type_var_name,
       to_struct_tag_type(
-        java_type_from_string(bound_type, class_name).subtype()));
+        java_type_from_string(bound_type, class_name)->subtype()));
 
     types.push_back(type_var_type);
     signature=signature.substr(var_sep+1, std::string::npos);
@@ -745,7 +744,7 @@ static std::string slash_to_dot(const std::string &src)
 struct_tag_typet java_classname(const std::string &id)
 {
   if(!id.empty() && id[0]=='[')
-    return to_struct_tag_type(java_type_from_string(id).subtype());
+    return to_struct_tag_type(java_type_from_string(id)->subtype());
 
   std::string class_name=id;
 
@@ -899,9 +898,9 @@ void get_dependencies_from_generic_parameters(
     // class signature without bounds and without wildcards
     else if(signature.find('*') == std::string::npos)
     {
-      get_dependencies_from_generic_parameters_rec(
-        java_type_from_string(signature, erase_type_arguments(signature)),
-        refs);
+      auto type_from_string =
+        java_type_from_string(signature, erase_type_arguments(signature));
+      get_dependencies_from_generic_parameters_rec(*type_from_string, refs);
     }
   }
   catch(unsupported_java_class_signature_exceptiont &)
@@ -939,9 +938,9 @@ java_generic_struct_tag_typet::java_generic_struct_tag_typet(
   : struct_tag_typet(type)
 {
   set(ID_C_java_generic_symbol, true);
-  const typet &base_type = java_type_from_string(base_ref, class_name_prefix);
-  PRECONDITION(is_java_generic_type(base_type));
-  const java_generic_typet &gen_base_type = to_java_generic_type(base_type);
+  const auto base_type = java_type_from_string(base_ref, class_name_prefix);
+  PRECONDITION(is_java_generic_type(*base_type));
+  const java_generic_typet &gen_base_type = to_java_generic_type(*base_type);
   INVARIANT(
     type.get_identifier() ==
       to_struct_tag_type(gen_base_type.subtype()).get_identifier(),