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

@@ -444,14 +444,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);
+  slots_for_parameters=java_method_parameter_slots(method_type);
 
   debug() << "Generating codet: class "
              << class_symbol.name << ", method "
@@ -587,14 +587,14 @@ void java_bytecode_convert_methodt::convert(
   method_symbol.location=m.source_location;
   method_symbol.location.set_function(method_identifier);
 
-  code_typet::exceptionst &exceptions_list = code_type.throws_exceptions();
+  java_method_typet::exceptionst &exceptions_list = method_type.throws_exceptions();
   for(const auto &p : m.throws_exception_table)
   {
     if(!p.empty())
       exceptions_list.push_back(irept(p));
   }
 
-  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
@@ -608,7 +608,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
@@ -617,14 +617,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,33 @@ 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:
+  typedef std::vector<irept> exceptionst;
+  const exceptionst &throws_exceptions() const
+  {
+    return find(ID_exceptions_thrown_list).get_sub();
+  }
+
+  exceptionst &throws_exceptions()
+  {
+    return add(ID_exceptions_thrown_list).get_sub();
+  }
+};
+
+inline const java_method_typet &to_java_method_type(const typet &type)
+{
+  assert(type.id()==ID_code);
+  return static_cast<const java_method_typet &>(type);
+}
+
+inline java_method_typet &to_java_method_type(typet &type)
+{
+  assert(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(id2string(exceptions.at(0).id()) == "CustomException");
         REQUIRE(id2string(exceptions.at(1).id()) == "java.io.IOException");

src/util/std_types.h

@@ -767,8 +767,6 @@ class code_typet:public typet
   class parametert;
   typedef std::vector<parametert> parameterst;
 
-  typedef std::vector<irept> exceptionst;
-
   /// Constructs a new code type, i.e. function type
   /// \param _parameters: the vector of function parameters
   /// \param _return_type: the return type
@@ -914,16 +912,6 @@ class code_typet:public typet
     return (parameterst &)add(ID_parameters).get_sub();
   }
 
-  const exceptionst &throws_exceptions() const
-  {
-    return find(ID_exceptions_thrown_list).get_sub();
-  }
-
-  exceptionst &throws_exceptions()
-  {
-    return add(ID_exceptions_thrown_list).get_sub();
-  }
-
   bool get_inlined() const
   {
     return get_bool(ID_C_inlined);