Creates java_method_typet which extends code_typet

This is so that we do not need to have java-specific fields and related methods, like those relating to throws exceptions, in std_types

Author: jeannielynnmoulton

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -445,14 +445,14 @@ void java_bytecode_convert_methodt::convert(
 
   // Obtain a std::vector of code_typet::parametert objects from the
   // (function) type of the symbol
-  code_typet code_type = to_code_type(method_symbol.type);
-  code_type.set(ID_C_class, class_symbol.name);
-  method_return_type = code_type.return_type();
-  code_typet::parameterst &parameters = code_type.parameters();
+  java_method_typet method_type = to_java_method_type(method_symbol.type);
+  method_type.set(ID_C_class, class_symbol.name);
+  method_return_type=method_type.return_type();
+  code_typet::parameterst &parameters=method_type.parameters();
 
-  // Determine the number of local variable slots used by the JVM to maintan the
-  // formal parameters
-  slots_for_parameters = java_method_parameter_slots(code_type);
+  // Determine the number of local variable slots used by the JVM to maintain
+  // the formal parameters
+  slots_for_parameters=java_method_parameter_slots(method_type);
 
   debug() << "Generating codet: class " << class_symbol.name << ", method "
           << m.name << eom;
@@ -584,11 +584,11 @@ void java_bytecode_convert_methodt::convert(
   method_symbol.location = m.source_location;
   method_symbol.location.set_function(method_identifier);
 
-  std::vector<irept> &exceptions_list = code_type.throws_exceptions();
+  std::vector<irept> &exceptions_list = method_type.throws_exceptions();
   for(const auto &exception_name : m.throws_exception_table)
       exceptions_list.push_back(irept(exception_name));
 
-  const std::string signature_string = pretty_signature(code_type);
+  const std::string signature_string = pretty_signature(method_type);
 
   // Set up the pretty name for the method entry in the symbol table.
   // The pretty name of a constructor includes the base name of the class
@@ -602,7 +602,7 @@ void java_bytecode_convert_methodt::convert(
     method_symbol.pretty_name =
       id2string(class_symbol.pretty_name) + signature_string;
     INVARIANT(
-      code_type.get_is_constructor(),
+      method_type.get_is_constructor(),
       "Member type should have already been marked as a constructor");
   }
   else
@@ -611,14 +611,14 @@ void java_bytecode_convert_methodt::convert(
                                 id2string(m.base_name) + signature_string;
   }
 
-  method_symbol.type = code_type;
-
+  method_symbol.type = method_type;
+  
   current_method = method_symbol.name;
-  method_has_this = code_type.has_this();
+  method_has_this = method_type.has_this();
   if((!m.is_abstract) && (!m.is_native))
     method_symbol.value = convert_instructions(
       m,
-      code_type,
+      method_type,
       method_symbol.name,
       to_java_class_type(class_symbol.type).lambda_method_handles());
 }

jbmc/src/java_bytecode/java_types.h

@@ -242,6 +242,32 @@ inline bool can_cast_type<java_class_typet>(const typet &type)
   return can_cast_type<class_typet>(type);
 }
 
+class java_method_typet:public code_typet
+{
+  public:
+  const std::vector<irept> &throws_exceptions() const
+  {
+    return find(ID_exceptions_thrown_list).get_sub();
+  }
+
+  std::vector<irept> &throws_exceptions()
+  {
+    return add(ID_exceptions_thrown_list).get_sub();
+  }
+};
+
+inline const java_method_typet &to_java_method_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_code);
+  return static_cast<const java_method_typet &>(type);
+}
+
+inline java_method_typet &to_java_method_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_code);
+  return static_cast<java_method_typet &>(type);
+}
+
 typet java_int_type();
 typet java_long_type();
 typet java_short_type();

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp

@@ -610,7 +610,7 @@ SCENARIO(
           new_symbol_table.lookup_ref("java::ThrowsExceptions");
         const symbolt &method_symbol =
           new_symbol_table.lookup_ref("java::ThrowsExceptions.test:()V");
-        const code_typet method = to_code_type(method_symbol.type);
+        const java_method_typet method = to_java_method_type(method_symbol.type);
         const std::vector<irept> exceptions = method.throws_exceptions();
         REQUIRE(exceptions.size() == 2);
         REQUIRE(

src/util/std_types.h

@@ -912,16 +912,6 @@ class code_typet:public typet
     return (parameterst &)add(ID_parameters).get_sub();
   }
 
-  const std::vector<irept> &throws_exceptions() const
-  {
-    return find(ID_exceptions_thrown_list).get_sub();
-  }
-
-  std::vector<irept> &throws_exceptions()
-  {
-    return add(ID_exceptions_thrown_list).get_sub();
-  }
-
   bool get_inlined() const
   {
     return get_bool(ID_C_inlined);