[TG-4345] Parse thrown exceptions in java

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -280,6 +280,7 @@ void java_bytecode_convert_classt::convert(
   class_type.set_is_static_class(c.is_static_class);
   class_type.set_is_anonymous_class(c.is_anonymous_class);
   class_type.set_outer_class(c.outer_class);
+  class_type.set_super_class(c.super_class);
   if(c.is_enum)
   {
     if(max_array_length != 0 && c.enum_elements > max_array_length)
@@ -303,9 +304,9 @@ void java_bytecode_convert_classt::convert(
   else
     class_type.set_access(ID_default);
 
-  if(!c.extends.empty())
+  if(!c.super_class.empty())
   {
-    const symbol_typet base("java::" + id2string(c.extends));
+    const symbol_typet base("java::" + id2string(c.super_class));
 
     // if the superclass is generic then the class has the superclass reference
     // including the generic info in its signature
@@ -323,7 +324,7 @@ void java_bytecode_convert_classt::convert(
       }
       catch(const unsupported_java_class_signature_exceptiont &e)
       {
-        warning() << "Superclass: " << c.extends << " of class: " << c.name
+        warning() << "Superclass: " << c.super_class << " of class: " << c.name
                   << "\n could not parse signature: " << superclass_ref.value()
                   << "\n " << e.what()
                   << "\n ignoring that the superclass is generic" << eom;
@@ -336,9 +337,9 @@ void java_bytecode_convert_classt::convert(
     }
     class_typet::componentt base_class_field;
     base_class_field.type() = class_type.bases().at(0).type();
-    base_class_field.set_name("@"+id2string(c.extends));
-    base_class_field.set_base_name("@"+id2string(c.extends));
-    base_class_field.set_pretty_name("@"+id2string(c.extends));
+    base_class_field.set_name("@" + id2string(c.super_class));
+    base_class_field.set_base_name("@" + id2string(c.super_class));
+    base_class_field.set_pretty_name("@" + id2string(c.super_class));
     class_type.components().push_back(base_class_field);
   }
 
@@ -561,7 +562,7 @@ void java_bytecode_convert_classt::convert(
   }
 
   // is this a root class?
-  if(c.extends.empty())
+  if(c.super_class.empty())
     java_root_class(*class_symbol);
 }
 

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);
+  // 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 "
@@ -587,7 +587,10 @@ void java_bytecode_convert_methodt::convert(
   method_symbol.location=m.source_location;
   method_symbol.location.set_function(method_identifier);
 
-  const std::string signature_string = pretty_signature(code_type);
+  for(const auto &exception_name : m.throws_exception_table)
+    method_type.add_throws_exceptions(exception_name);
+
+  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
@@ -601,7 +604,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
@@ -610,14 +613,13 @@ void java_bytecode_convert_methodt::convert(
                                 id2string(m.base_name) + signature_string;
   }
 
-  method_symbol.type = code_type;
-
-  current_method=method_symbol.name;
-  method_has_this=code_type.has_this();
+  method_symbol.type = method_type;
+  current_method = method_symbol.name;
+  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_bytecode_parse_tree.cpp

@@ -38,8 +38,8 @@ void java_bytecode_parse_treet::classt::output(std::ostream &out) const
   }
 
   out << "class " << name;
-  if(!extends.empty())
-    out << " extends " << extends;
+  if(!super_class.empty())
+    out << " extends " << super_class;
   out << " {" << '\n';
 
   for(fieldst::const_iterator

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -114,6 +114,8 @@ struct java_bytecode_parse_treet
     typedef std::vector<exceptiont> exception_tablet;
     exception_tablet exception_table;
 
+    std::vector<irep_idt> throws_exception_table;
+
     struct local_variablet
     {
       irep_idt name;
@@ -197,7 +199,7 @@ struct java_bytecode_parse_treet
     classt &operator=(classt &&) = default;
     #endif
 
-    irep_idt name, extends;
+    irep_idt name, super_class;
     bool is_abstract=false;
     bool is_enum=false;
     bool is_public=false, is_protected=false, is_private=false;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -121,6 +121,7 @@ class java_bytecode_parsert:public parsert
   void rmethod(classt &parsed_class);
   void
   rinner_classes_attribute(classt &parsed_class, const u4 &attribute_length);
+  std::vector<irep_idt> rexceptions_attribute();
   void rclass_attribute(classt &parsed_class);
   void rRuntimeAnnotation_attribute(annotationst &);
   void rRuntimeAnnotation(annotationt &);
@@ -503,8 +504,7 @@ void java_bytecode_parsert::rClassFile()
     constant(this_class).type().get(ID_C_base_name);
 
   if(super_class!=0)
-    parsed_class.extends=
-      constant(super_class).type().get(ID_C_base_name);
+    parsed_class.super_class = constant(super_class).type().get(ID_C_base_name);
 
   rinterfaces(parsed_class);
   rfields(parsed_class);
@@ -1243,6 +1243,10 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
   {
     rRuntimeAnnotation_attribute(method.annotations);
   }
+  else if(attribute_name == "Exceptions")
+  {
+    method.throws_exception_table = rexceptions_attribute();
+  }
   else
     skip_bytes(attribute_length);
 }
@@ -1655,6 +1659,26 @@ void java_bytecode_parsert::rinner_classes_attribute(
   }
 }
 
+/// Corresponds to the element_value structure
+/// Described in Java 8 specification 4.7.5
+/// https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.7.5
+/// Parses the Exceptions attribute for the current method,
+/// and returns a vector of exceptions.
+std::vector<irep_idt> java_bytecode_parsert::rexceptions_attribute()
+{
+  u2 number_of_exceptions = read_u2();
+
+  std::vector<irep_idt> exceptions;
+  for(size_t i = 0; i < number_of_exceptions; i++)
+  {
+    u2 exception_index_table = read_u2();
+    const irep_idt exception_name =
+      constant(exception_index_table).type().get(ID_C_base_name);
+    exceptions.push_back(exception_name);
+  }
+  return exceptions;
+}
+
 void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
 {
   u2 attribute_name_index=read_u2();

jbmc/src/java_bytecode/java_types.h

@@ -121,16 +121,26 @@ class java_class_typet:public class_typet
     return set(ID_is_inner_class, is_inner_class);
   }
 
-  const irep_idt get_outer_class() const
+  const irep_idt &get_outer_class() const
   {
     return get(ID_outer_class);
   }
 
-  void set_outer_class(irep_idt outer_class)
+  void set_outer_class(const irep_idt &outer_class)
   {
     return set(ID_outer_class, outer_class);
   }
 
+  const irep_idt &get_super_class() const
+  {
+    return get(ID_super_class);
+  }
+
+  void set_super_class(const irep_idt &super_class)
+  {
+    return set(ID_super_class, super_class);
+  }
+
   const bool get_is_static_class() const
   {
     return get_bool(ID_is_static);
@@ -232,6 +242,35 @@ 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<irep_idt> throws_exceptions() const
+  {
+    std::vector<irep_idt> exceptions;
+    for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
+      exceptions.push_back(e.id());
+    return exceptions;
+  }
+
+  void add_throws_exceptions(irep_idt exception)
+  {
+    add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
+  }
+};
+
+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/Makefile

@@ -12,6 +12,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
        java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \
        java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
+       java_bytecode/java_bytecode_parser/parse_java_class.cpp \
        java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \
        java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \

jbmc/unit/java_bytecode/java_bytecode_parser/ChildClass.java

@@ -0,0 +1,8 @@
+public class ChildClass extends ParentClass {
+}
+
+class ParentClass extends GrandparentClass {
+}
+
+class GrandparentClass {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java

@@ -0,0 +1,18 @@
+import java.io.*;
+
+public class ThrowsExceptions {
+
+  public static void test() throws CustomException, IOException {
+     StringReader sr = new StringReader("");
+     sr.read();
+     throw new CustomException();
+  }
+
+  public static void testNoExceptions() {
+    StringReader sr = new StringReader("");
+  }
+
+}
+
+class CustomException extends Exception {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp

@@ -8,6 +8,7 @@
 
 #include <java-testing-utils/load_java_class.h>
 #include <java_bytecode/java_bytecode_convert_class.h>
+#include <java_bytecode/java_bytecode_convert_method.h>
 #include <java_bytecode/java_bytecode_parse_tree.h>
 #include <java_bytecode/java_types.h>
 #include <testing-utils/catch.hpp>
@@ -596,4 +597,45 @@ SCENARIO(
       }
     }
   }
+
+  GIVEN("A method that may or may not throw exceptions")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "ThrowsExceptions", "./java_bytecode/java_bytecode_parser");
+    WHEN("Parsing the exceptions attribute for a method that throws exceptions")
+    {
+      THEN("We should be able to get the list of exceptions it throws")
+      {
+        const symbolt &method_symbol =
+          new_symbol_table.lookup_ref("java::ThrowsExceptions.test:()V");
+        const java_method_typet method =
+          to_java_method_type(method_symbol.type);
+        const std::vector<irep_idt> exceptions = method.throws_exceptions();
+        REQUIRE(exceptions.size() == 2);
+        REQUIRE(
+          std::find(
+            exceptions.begin(),
+            exceptions.end(),
+            irept("CustomException").id()) != exceptions.end());
+        REQUIRE(
+          std::find(
+            exceptions.begin(),
+            exceptions.end(),
+            irept("java.io.IOException").id()) != exceptions.end());
+      }
+    }
+    WHEN(
+      "Parsing the exceptions attribute for a method that throws no exceptions")
+    {
+      THEN("We should be able to get the list of exceptions it throws")
+      {
+        const symbolt &method_symbol = new_symbol_table.lookup_ref(
+          "java::ThrowsExceptions.testNoExceptions:()V");
+        const java_method_typet method =
+          to_java_method_type(method_symbol.type);
+        const std::vector<irep_idt> exceptions = method.throws_exceptions();
+        REQUIRE(exceptions.size() == 0);
+      }
+    }
+  }
 }