Replace all uses of deprecated nil_typet

Use typet or optionalt<typet>.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -670,7 +670,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,21 @@ 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(
+      auto member_type_from_signature=java_type_from_string(
         signature.value(),
         class_name);
-      INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type");
+      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 +294,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
@@ -472,7 +472,7 @@ void java_bytecode_convert_methodt::convert(
         id2string(class_symbol.name));
     }
     else
-      t=java_type_from_string(v.descriptor);
+      t=*java_type_from_string(v.descriptor);
 
     std::ostringstream id_oss;
     id_oss << method_id << "::" << v.name;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -100,7 +100,9 @@ class java_bytecode_parsert:public parsert
 
   const typet type_entry(u2 index)
   {
-    return java_type_from_string(id2string(pool_entry(index).s));
+    auto type_from_string = java_type_from_string(id2string(pool_entry(index).s));
+    CHECK_RETURN(type_from_string.has_value());
+    return std::move(*type_from_string);
   }
 
   void populate_bytecode_mnemonics_table()
@@ -548,8 +550,9 @@ 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));
+        CHECK_RETURN(t.has_value());
+        get_class_refs_rec(*t);
       }
       break;
 
@@ -576,7 +579,11 @@ void java_bytecode_parsert::get_class_refs()
         field_type, parse_tree.class_refs);
     }
     else
-      field_type=java_type_from_string(field.descriptor);
+    {
+      auto type_from_string = java_type_from_string(field.descriptor);
+      CHECK_RETURN(type_from_string.has_value());
+      field_type=std::move(*type_from_string);
+    }
 
     get_class_refs_rec(field_type);
   }
@@ -597,7 +604,11 @@ void java_bytecode_parsert::get_class_refs()
         method_type, parse_tree.class_refs);
     }
     else
-      method_type=java_type_from_string(method.descriptor);
+    {
+      auto type_from_string = java_type_from_string(method.descriptor);
+      CHECK_RETURN(type_from_string.has_value());
+      method_type=std::move(*type_from_string);
+    }
 
     get_class_refs_rec(method_type);
     for(const auto &var : method.local_variable_table)
@@ -613,7 +624,11 @@ void java_bytecode_parsert::get_class_refs()
           var_type, parse_tree.class_refs);
       }
       else
-        var_type=java_type_from_string(var.descriptor);
+      {
+        auto type_from_string = java_type_from_string(var.descriptor);
+        CHECK_RETURN(type_from_string.has_value());
+        var_type=std::move(*type_from_string);
+      }
       get_class_refs_rec(var_type);
     }
   }
@@ -672,8 +687,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));
+    CHECK_RETURN(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,15 @@ 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;");
+  CHECK_RETURN(string_array_type.has_value());
   // 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

@@ -796,7 +796,7 @@ void java_bytecode_convert_methodt::setup_local_variables(
     const typet t = v.var.signature.has_value()
                       ? 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

@@ -199,7 +199,7 @@ typet java_type_from_char(char t)
   case 'd': return java_double_type();
   case 'z': return java_boolean_type();
   case 'a': return java_reference_type(void_typet());
-  default: UNREACHABLE; return nil_typet();
+  default: UNREACHABLE;
   }
 }
 
@@ -339,9 +339,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;
 }
@@ -489,12 +489,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
@@ -538,15 +538,15 @@ typet java_type_from_string(
           "Cannot currently parse bounds on generic types");
       }
 
-      const typet &method_type=java_type_from_string(
+      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;
@@ -555,10 +555,11 @@ 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);
+      CHECK_RETURN(return_type.has_value());
 
       std::vector<typet> param_types =
         parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
@@ -571,26 +572,27 @@ 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=
+      auto subtype=
         java_type_from_string(src.substr(1, std::string::npos),
                               class_name_prefix);
+      CHECK_RETURN(subtype.has_value());
       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();
@@ -611,7 +613,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':
     {
@@ -627,7 +629,7 @@ typet java_type_from_string(
     throw unsupported_java_class_signature_exceptiont("wild card generic");
   }
   default:
-    return nil_typet();
+    return {};
   }
 }
 
@@ -712,7 +714,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);
@@ -734,7 +736,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;
 
@@ -888,8 +890,10 @@ void get_dependencies_from_generic_parameters(
     // class signature without bounds and without wildcards
     else if(signature.find('*') == std::string::npos)
     {
+      auto type_from_string = java_type_from_string(signature, erase_type_arguments(signature));
+      CHECK_RETURN(type_from_string.has_value());
       get_dependencies_from_generic_parameters_rec(
-        java_type_from_string(signature, erase_type_arguments(signature)),
+        *type_from_string,
         refs);
     }
   }
@@ -928,9 +932,10 @@ 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);
+  CHECK_RETURN(base_type.has_value());
+  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(),

jbmc/src/java_bytecode/java_types.h

@@ -380,7 +380,7 @@ bool is_java_array_type(const typet &type);
 bool is_multidim_java_array_type(const typet &type);
 
 typet java_type_from_char(char t);
-typet java_type_from_string(
+optionalt<typet> java_type_from_string(
   const std::string &,
   const std::string &class_name_prefix="");
 char java_char_from_type(const typet &type);
@@ -722,11 +722,15 @@ inline typet java_type_from_string_with_exception(
 {
   try
   {
-    return java_type_from_string(signature.value(), class_name);
+    const auto type_from_string = java_type_from_string(signature.value(), class_name);
+    CHECK_RETURN(type_from_string.has_value());
+    return *type_from_string;
   }
   catch(unsupported_java_class_signature_exceptiont &)
   {
-    return java_type_from_string(descriptor, class_name);
+    const auto type_from_string = java_type_from_string(descriptor, class_name);
+    CHECK_RETURN(type_from_string.has_value());
+    return *type_from_string;
   }
 }