diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 36ad3bff30d..6105841a75c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/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); } diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 330f90ef019..651ab62c0ce 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/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 ¶meters=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 ¶meters = 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()); } diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp index bbd985182fc..75698dc0d31 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/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 diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 641fba16bc3..3e415f4f85d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -114,6 +114,8 @@ struct java_bytecode_parse_treet typedef std::vector exception_tablet; exception_tablet exception_table; + std::vector 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; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 71307324aed..1c7fb6e7e2e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/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 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 java_bytecode_parsert::rexceptions_attribute() +{ + u2 number_of_exceptions = read_u2(); + + std::vector 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(); diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index fa696ed49e3..c0d07df88fa 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/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(const typet &type) return can_cast_type(type); } +class java_method_typet : public code_typet +{ +public: + const std::vector throws_exceptions() const + { + std::vector 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(type); +} + +inline java_method_typet &to_java_method_type(typet &type) +{ + PRECONDITION(type.id() == ID_code); + return static_cast(type); +} + typet java_int_type(); typet java_long_type(); typet java_short_type(); diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 4c04bf031ee..6c491f75827 100644 --- a/jbmc/unit/Makefile +++ b/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 \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ChildClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ChildClass.class new file mode 100644 index 00000000000..89b2cf76e02 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ChildClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ChildClass.java b/jbmc/unit/java_bytecode/java_bytecode_parser/ChildClass.java new file mode 100644 index 00000000000..3147d618196 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/ChildClass.java @@ -0,0 +1,8 @@ +public class ChildClass extends ParentClass { +} + +class ParentClass extends GrandparentClass { +} + +class GrandparentClass { +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class b/jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class new file mode 100644 index 00000000000..2e0071e101a Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/GrandparentClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/GrandparentClass.class new file mode 100644 index 00000000000..8a7804e5dd8 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/GrandparentClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ParentClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ParentClass.class new file mode 100644 index 00000000000..b0edeb7f30f Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ParentClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.class new file mode 100644 index 00000000000..9e80d119b3a Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java b/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java new file mode 100644 index 00000000000..46bee61c6cf --- /dev/null +++ b/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 { +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp index 367e343acb8..0c6fec89b60 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp @@ -8,6 +8,7 @@ #include #include +#include #include #include #include @@ -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 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 exceptions = method.throws_exceptions(); + REQUIRE(exceptions.size() == 0); + } + } + } } diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_class.cpp new file mode 100644 index 00000000000..1d65d189549 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_class.cpp @@ -0,0 +1,83 @@ +/*******************************************************************\ + + Module: Unit tests for converting annotations + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +SCENARIO( + "java_bytecode_parse_class", + "[core][java_bytecode][java_bytecode_parser]") +{ + GIVEN("Some class with a class hierarchy") + { + const symbol_tablet &new_symbol_table = + load_java_class("ChildClass", "./java_bytecode/java_bytecode_parser"); + WHEN("Parsing the class file structure") + { + THEN("We should be able to get the first super class") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::ChildClass"); + const java_class_typet &java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_super_class() == "ParentClass"); + } + THEN("We should be able to get the second super class") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::ChildClass"); + const java_class_typet &java_class = + to_java_class_type(class_symbol.type); + const symbolt &class_symbol1 = new_symbol_table.lookup_ref( + "java::" + id2string(java_class.get_super_class())); + const java_class_typet &java_class1 = + to_java_class_type(class_symbol1.type); + REQUIRE(java_class1.get_super_class() == "GrandparentClass"); + } + THEN("We should be able to get the third super class") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::ChildClass"); + const java_class_typet &java_class = + to_java_class_type(class_symbol.type); + const symbolt &class_symbol1 = new_symbol_table.lookup_ref( + "java::" + id2string(java_class.get_super_class())); + const java_class_typet &java_class1 = + to_java_class_type(class_symbol1.type); + const symbolt &class_symbol2 = new_symbol_table.lookup_ref( + "java::" + id2string(java_class1.get_super_class())); + const java_class_typet &java_class2 = + to_java_class_type(class_symbol2.type); + REQUIRE(java_class2.get_super_class() == "java.lang.Object"); + } + THEN("We should be able to get the fourth super class") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::ChildClass"); + const java_class_typet &java_class = + to_java_class_type(class_symbol.type); + const symbolt &class_symbol1 = new_symbol_table.lookup_ref( + "java::" + id2string(java_class.get_super_class())); + const java_class_typet &java_class1 = + to_java_class_type(class_symbol1.type); + const symbolt &class_symbol2 = new_symbol_table.lookup_ref( + "java::" + id2string(java_class1.get_super_class())); + const java_class_typet &java_class2 = + to_java_class_type(class_symbol2.type); + const symbolt &class_symbol3 = new_symbol_table.lookup_ref( + "java::" + id2string(java_class2.get_super_class())); + const java_class_typet &java_class3 = + to_java_class_type(class_symbol3.type); + REQUIRE(java_class3.get_super_class().empty()); + } + } + } +} diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index fbba1b6b2e6..3d9c0873754 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -693,6 +693,8 @@ IREP_ID_TWO(C_qualifier, #qualifier) IREP_ID_TWO(C_array_ini, #array_ini) IREP_ID_ONE(r_ok) IREP_ID_ONE(w_ok) +IREP_ID_ONE(super_class) +IREP_ID_ONE(exceptions_thrown_list) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree