Java bytecode front-end: do not crash upon invalid class names

Do not make unchecked use of the result of `java_type_from_string`.

Fixes: #728
Fixes: #849

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -677,7 +677,11 @@ void java_bytecode_convert_classt::convert(
     }
   }
   else
-    field_type = *java_type_from_string(f.descriptor);
+  {
+    auto type_opt = java_type_from_string(f.descriptor);
+    CHECK_RETURN(type_opt.has_value());
+    field_type = *type_opt;
+  }
 
   // determine access
   irep_idt access;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -85,7 +85,9 @@ class java_bytecode_parsert final : public parsert
 
   const typet type_entry(u2 index)
   {
-    return *java_type_from_string(id2string(pool_entry(index).s));
+    auto type_opt = java_type_from_string(id2string(pool_entry(index).s));
+    CHECK_RETURN(type_opt.has_value());
+    return std::move(*type_opt);
   }
 
   void rClassFile();
@@ -408,6 +410,12 @@ bool java_bytecode_parsert::parse()
     return true;
   }
 
+  catch(const unsupported_java_class_signature_exceptiont &e)
+  {
+    log.error() << e.str() << messaget::eom;
+    return true;
+  }
+
   catch(...)
   {
     log.error() << "parsing error" << messaget::eom;
@@ -514,8 +522,11 @@ void java_bytecode_parsert::get_class_refs()
       break;
 
     case CONSTANT_NameAndType:
-      get_class_refs_rec(
-        *java_type_from_string(id2string(pool_entry(c.ref2).s)));
+    {
+      auto type_opt = java_type_from_string(id2string(pool_entry(c.ref2).s));
+      CHECK_RETURN(type_opt.has_value());
+      get_class_refs_rec(*type_opt);
+    }
       break;
 
     default: {}
@@ -543,7 +554,9 @@ void java_bytecode_parsert::get_class_refs()
     }
     else
     {
-      get_class_refs_rec(*java_type_from_string(field.descriptor));
+      auto type_opt = java_type_from_string(field.descriptor);
+      CHECK_RETURN(type_opt);
+      get_class_refs_rec(*type_opt);
     }
   }
 
@@ -565,7 +578,9 @@ void java_bytecode_parsert::get_class_refs()
     }
     else
     {
-      get_class_refs_rec(*java_type_from_string(method.descriptor));
+      auto type_opt = java_type_from_string(method.descriptor);
+      CHECK_RETURN(type_opt);
+      get_class_refs_rec(*type_opt);
     }
 
     for(const auto &var : method.local_variable_table)
@@ -582,7 +597,9 @@ void java_bytecode_parsert::get_class_refs()
       }
       else
       {
-        get_class_refs_rec(*java_type_from_string(var.descriptor));
+        auto type_opt = java_type_from_string(var.descriptor);
+        CHECK_RETURN(type_opt.has_value());
+        get_class_refs_rec(*type_opt);
       }
     }
   }
@@ -637,7 +654,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();
-    get_class_refs_rec(*java_type_from_string(id2string(value_id)));
+    auto type_opt = java_type_from_string(id2string(value_id));
+    CHECK_RETURN(type_opt.has_value());
+    get_class_refs_rec(*type_opt);
   }
   else if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(value))
   {
@@ -1967,13 +1986,14 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
   irep_idt method_name = name_and_type.get_name(pool_entry_lambda);
   std::string descriptor = name_and_type.get_descriptor(pool_entry_lambda);
   irep_idt mangled_method_name = id2string(method_name) + ":" + descriptor;
-  typet method_type = *java_type_from_string(descriptor);
+  auto method_type_opt = java_type_from_string(descriptor);
+  CHECK_RETURN(method_type_opt.has_value());
 
   method_handle_typet handle_type =
     get_method_handle_type(entry.get_handle_kind());
 
   class_method_descriptor_exprt method_descriptor{
-    method_type, mangled_method_name, class_name, method_name};
+    *method_type, mangled_method_name, class_name, method_name};
   lambda_method_handlet lambda_method_handle{method_descriptor, handle_type};
 
   return lambda_method_handle;

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -307,6 +307,7 @@ 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 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

jbmc/src/java_bytecode/java_types.cpp

@@ -624,10 +624,14 @@ std::optional<typet> java_type_from_string(
     {
       std::size_t e_pos=src.rfind(')');
       if(e_pos==std::string::npos)
-        return {};
+      {
+        throw unsupported_java_class_signature_exceptiont(
+          "Failed to find function signature closing delimiter");
+      }
 
       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, '(', ')');
@@ -648,10 +652,14 @@ std::optional<typet> java_type_from_string(
       // 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 {};
+      {
+        throw unsupported_java_class_signature_exceptiont(
+          "Failed to find array signature closing delimiter");
+      }
       char subtype_letter=src[1];
       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
@@ -681,11 +689,11 @@ std::optional<typet> java_type_from_string(
     INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'.");
     PRECONDITION(!class_name_prefix.empty());
     irep_idt type_var_name(class_name_prefix+"::"+src.substr(1, src.size()-2));
+    auto lang_object = java_type_from_string("Ljava/lang/Object;");
+    CHECK_RETURN(lang_object.has_value());
     return java_generic_parametert(
       type_var_name,
-      to_struct_tag_type(
-        to_java_reference_type(*java_type_from_string("Ljava/lang/Object;"))
-          .base_type()));
+      to_struct_tag_type(to_java_reference_type(*lang_object).base_type()));
   }
   case 'L':
     {
@@ -781,13 +789,13 @@ std::vector<typet> java_generic_type_from_string(
 
     std::string type_var_name(
       "java::"+class_name+"::"+signature.substr(0, bound_sep));
-    std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep));
-
+    std::string bound_type_str(
+      signature.substr(bound_sep + 1, var_sep - bound_sep));
+    auto bound_type = java_type_from_string(bound_type_str, class_name);
+    CHECK_RETURN(bound_type.has_value());
     java_generic_parametert type_var_type(
       type_var_name,
-      to_struct_tag_type(
-        to_java_reference_type(*java_type_from_string(bound_type, class_name))
-          .base_type()));
+      to_struct_tag_type(to_java_reference_type(*bound_type).base_type()));
 
     types.push_back(type_var_type);
     signature=signature.substr(var_sep+1, std::string::npos);
@@ -809,8 +817,11 @@ 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(
-      to_java_reference_type(*java_type_from_string(id)).base_type());
+  {
+    auto array_type = java_type_from_string(id);
+    CHECK_RETURN(array_type.has_value());
+    return to_struct_tag_type(to_java_reference_type(*array_type).base_type());
+  }
 
   std::string class_name=id;
 
@@ -1014,6 +1025,7 @@ void get_dependencies_from_generic_parameters(
     {
       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(*type_from_string, refs);
     }
   }
@@ -1053,6 +1065,7 @@ java_generic_struct_tag_typet::java_generic_struct_tag_typet(
 {
   set(ID_C_java_generic_symbol, true);
   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(