From fbad2d921a8f19b2df14f38aa8a8444a54023ddf Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Tue, 24 Jul 2018 14:21:30 +0100 Subject: [PATCH 01/10] Rename variable extends to super_class This better reflects the bytecode. --- .../java_bytecode/java_bytecode_convert_class.cpp | 14 +++++++------- .../src/java_bytecode/java_bytecode_parse_tree.cpp | 4 ++-- jbmc/src/java_bytecode/java_bytecode_parse_tree.h | 2 +- jbmc/src/java_bytecode/java_bytecode_parser.cpp | 2 +- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 36ad3bff30d..d14104737d9 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -303,9 +303,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 +323,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 +336,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 +561,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_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..bb28375dbfb 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -197,7 +197,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..7b4445620f0 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -503,7 +503,7 @@ void java_bytecode_parsert::rClassFile() constant(this_class).type().get(ID_C_base_name); if(super_class!=0) - parsed_class.extends= + parsed_class.super_class= constant(super_class).type().get(ID_C_base_name); rinterfaces(parsed_class); From 5994dd85ad17ccc788bd97e08faa90a5f8256640 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Tue, 24 Jul 2018 14:24:15 +0100 Subject: [PATCH 02/10] Add method to get super class from java class type. --- jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 1 + jbmc/src/java_bytecode/java_bytecode_parser.cpp | 3 +-- jbmc/src/java_bytecode/java_types.h | 10 ++++++++++ src/util/irep_ids.def | 1 + 4 files changed, 13 insertions(+), 2 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index d14104737d9..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) diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 7b4445620f0..48a3db6369f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -503,8 +503,7 @@ void java_bytecode_parsert::rClassFile() constant(this_class).type().get(ID_C_base_name); if(super_class!=0) - parsed_class.super_class= - 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); diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index fa696ed49e3..da23b17aad5 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -131,6 +131,16 @@ class java_class_typet:public class_typet 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); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index fbba1b6b2e6..9457d209bf8 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -693,6 +693,7 @@ 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) // 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 From 7fcc42dfe66610e1f980d3249246b1e5eabceb42 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Thu, 26 Jul 2018 13:07:41 +0100 Subject: [PATCH 03/10] Adds const to get/set_outer_class --- jbmc/src/java_bytecode/java_types.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index da23b17aad5..131922f383d 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -121,12 +121,12 @@ 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); } From 5c7dcacf40ab82daecd40750a268d3572c7a9cb5 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Thu, 26 Jul 2018 16:11:13 +0100 Subject: [PATCH 04/10] Parses the exception attribute 4.7.5. The Exceptions Attribute --- .../java_bytecode/java_bytecode_parse_tree.h | 2 ++ .../java_bytecode/java_bytecode_parser.cpp | 25 +++++++++++++++++++ src/util/irep_ids.def | 1 + src/util/std_types.h | 10 ++++++++ 4 files changed, 38 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index bb28375dbfb..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; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 48a3db6369f..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 &); @@ -1242,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); } @@ -1654,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/src/util/irep_ids.def b/src/util/irep_ids.def index 9457d209bf8..3d9c0873754 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -694,6 +694,7 @@ 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 diff --git a/src/util/std_types.h b/src/util/std_types.h index 792f7e40ab8..020fb8719a0 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -912,6 +912,16 @@ class code_typet:public typet return (parameterst &)add(ID_parameters).get_sub(); } + const std::vector &throws_exceptions() const + { + return find(ID_exceptions_thrown_list).get_sub(); + } + + std::vector &throws_exceptions() + { + return add(ID_exceptions_thrown_list).get_sub(); + } + bool get_inlined() const { return get_bool(ID_C_inlined); From eb885099ec5cfbd7696839e9042b497765f37d09 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Mon, 23 Jul 2018 11:36:10 +0100 Subject: [PATCH 05/10] Use parsed information for thrown exceptions. --- jbmc/src/java_bytecode/java_bytecode_convert_method.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 330f90ef019..55ea86e0a66 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -587,6 +587,10 @@ void java_bytecode_convert_methodt::convert( method_symbol.location=m.source_location; method_symbol.location.set_function(method_identifier); + std::vector &exceptions_list = code_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); // Set up the pretty name for the method entry in the symbol table. From 565c999742eaec23cb5c5e7969b0767eddddd58b Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Tue, 24 Jul 2018 13:52:03 +0100 Subject: [PATCH 06/10] Unit tests throws exceptions parsing. --- .../CustomException.class | Bin 0 -> 208 bytes .../ThrowsExceptions.class | Bin 0 -> 447 bytes .../ThrowsExceptions.java | 14 ++++++ .../parse_java_attributes.cpp | 47 ++++++++++++++++++ 4 files changed, 61 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java 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 0000000000000000000000000000000000000000..0fd68b551321324591f0a99a949541ea689f139d GIT binary patch literal 208 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj8j?|zUta85k(^pkl9``Zte2HomdL}v!oUjD z>s(q~lAjBgWMmKq$?E4M=B4YyMHv(rn1Jp80Y)GO>IBkkK$a|!28pn0ZD(NI2$p6C Rl5Ai>ULeT<y)7n;~5-1FmL$ghOdRQi*^e+pNU zWhAfNYgs9~Slw&F1I=Su^I!hcJml+n!b#?7uf z1 #include +#include #include #include #include @@ -596,4 +597,50 @@ 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 &class_symbol = + 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 std::vector exceptions = method.throws_exceptions(); + REQUIRE(exceptions.size() == 2); + REQUIRE( + std::find( + exceptions.begin(), exceptions.end(), irept("CustomException")) != + exceptions.end()); + REQUIRE( + std::find( + exceptions.begin(), + exceptions.end(), + irept("java.io.IOException")) != exceptions.end()); + } + } + } + + const symbol_tablet &new_symbol_table2 = load_java_class( + "ThrowsExceptions", "./java_bytecode/java_bytecode_parser"); + 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 &class_symbol = + new_symbol_table2.lookup_ref("java::ThrowsExceptions"); + const symbolt &method_symbol = + new_symbol_table2.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() == 0); + } + } + } } From aa83622435c65bd912c9ce8d1df1e0bab71e7014 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Tue, 24 Jul 2018 13:53:53 +0100 Subject: [PATCH 07/10] Unit tests method get_super_class --- jbmc/unit/Makefile | 1 + .../java_bytecode_parser/ChildClass.class | Bin 0 -> 189 bytes .../java_bytecode_parser/ChildClass.java | 8 ++ .../GrandparentClass.class | Bin 0 -> 200 bytes .../java_bytecode_parser/ParentClass.class | Bin 0 -> 195 bytes .../java_bytecode_parser/parse_java_class.cpp | 83 ++++++++++++++++++ 6 files changed, 92 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ChildClass.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ChildClass.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/GrandparentClass.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ParentClass.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_class.cpp 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 0000000000000000000000000000000000000000..89b2cf76e02b2cb1a27f4efc09daf34cdbae3f95 GIT binary patch literal 189 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ@0^jDlj59{SX``^l~|U@!@$D83RHs-W@O+F zNGwXtD*-EFP-I{NS_%S;KnPR}B-wyGSumf0fmLfe1LH=pG&_)F0}4ZwasX*222KEu C>moJ) literal 0 HcmV?d00001 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/GrandparentClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/GrandparentClass.class new file mode 100644 index 0000000000000000000000000000000000000000..8a7804e5dd8b17a9bf639fa0eef65606d1db0324 GIT binary patch literal 200 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ@0^jDlj59{SX``^l~|U@!@$D8%E%z#UX+-Z zQjl1bnpXmr1PXzq^>Y&Q()In5vQm>v7!(+ofcAp`BM<}i0ckcMOBP6jL|C=9Gcaxh TOS1z>Hn1Q&kmLaJm>4(#Cf_D- literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..b0edeb7f30f70da50c44df277ffa82102651bce4 GIT binary patch literal 195 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ@0^jDlj59{SX``^l~|U@!@$D8%E-VSkXV$O zR{|DiWDsyKO3X_sKnO7?FfakF1_4GO25JG)Y(SPQkOqmcYHep=+z6It2a;@1WsD3Q JKpqnVCjbSuB+mc< literal 0 HcmV?d00001 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()); + } + } + } +} From 1134bbacaf3f42446f9090a266cbf573259ebe1e Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Tue, 24 Jul 2018 14:56:37 +0100 Subject: [PATCH 08/10] 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 --- .../java_bytecode_convert_method.cpp | 29 +++++++++---------- jbmc/src/java_bytecode/java_types.h | 26 +++++++++++++++++ .../parse_java_attributes.cpp | 3 +- src/util/std_types.h | 10 ------- 4 files changed, 42 insertions(+), 26 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 55ea86e0a66..f7e48c9b5b5 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,11 +587,11 @@ void java_bytecode_convert_methodt::convert( method_symbol.location=m.source_location; method_symbol.location.set_function(method_identifier); - std::vector &exceptions_list = code_type.throws_exceptions(); + std::vector &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 @@ -605,7 +605,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 @@ -614,14 +614,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_types.h b/jbmc/src/java_bytecode/java_types.h index 131922f383d..89184101e36 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -242,6 +242,32 @@ 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 + { + return find(ID_exceptions_thrown_list).get_sub(); + } + + std::vector &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(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/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp index 7fa8008fa8f..b3b3b178138 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 @@ -610,7 +610,8 @@ 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 exceptions = method.throws_exceptions(); REQUIRE(exceptions.size() == 2); REQUIRE( diff --git a/src/util/std_types.h b/src/util/std_types.h index 020fb8719a0..792f7e40ab8 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -912,16 +912,6 @@ class code_typet:public typet return (parameterst &)add(ID_parameters).get_sub(); } - const std::vector &throws_exceptions() const - { - return find(ID_exceptions_thrown_list).get_sub(); - } - - std::vector &throws_exceptions() - { - return add(ID_exceptions_thrown_list).get_sub(); - } - bool get_inlined() const { return get_bool(ID_C_inlined); From a6e7c4be0d2601fdd111be1214e3292c6fc68b6e Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Tue, 31 Jul 2018 11:16:56 +0100 Subject: [PATCH 09/10] Refactors interface for exceptions to not use irepts. --- .../java_bytecode/java_bytecode_convert_method.cpp | 3 +-- jbmc/src/java_bytecode/java_types.h | 11 +++++++---- .../java_bytecode_parser/parse_java_attributes.cpp | 9 +++++---- 3 files changed, 13 insertions(+), 10 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index f7e48c9b5b5..651ab62c0ce 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -587,9 +587,8 @@ void java_bytecode_convert_methodt::convert( method_symbol.location=m.source_location; method_symbol.location.set_function(method_identifier); - std::vector &exceptions_list = method_type.throws_exceptions(); for(const auto &exception_name : m.throws_exception_table) - exceptions_list.push_back(irept(exception_name)); + method_type.add_throws_exceptions(exception_name); const std::string signature_string = pretty_signature(method_type); diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 89184101e36..c0d07df88fa 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -245,14 +245,17 @@ inline bool can_cast_type(const typet &type) class java_method_typet : public code_typet { public: - const std::vector &throws_exceptions() const + const std::vector throws_exceptions() const { - return find(ID_exceptions_thrown_list).get_sub(); + std::vector exceptions; + for(const auto &e : find(ID_exceptions_thrown_list).get_sub()) + exceptions.push_back(e.id()); + return exceptions; } - std::vector &throws_exceptions() + void add_throws_exceptions(irep_idt exception) { - return add(ID_exceptions_thrown_list).get_sub(); + add(ID_exceptions_thrown_list).get_sub().push_back(irept(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 b3b3b178138..2e066aaeb3f 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 @@ -612,17 +612,18 @@ SCENARIO( 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(); + const std::vector exceptions = method.throws_exceptions(); REQUIRE(exceptions.size() == 2); REQUIRE( std::find( - exceptions.begin(), exceptions.end(), irept("CustomException")) != - exceptions.end()); + exceptions.begin(), + exceptions.end(), + irept("CustomException").id()) != exceptions.end()); REQUIRE( std::find( exceptions.begin(), exceptions.end(), - irept("java.io.IOException")) != exceptions.end()); + irept("java.io.IOException").id()) != exceptions.end()); } } } From 655248a0bd3aeb05fa24e569773da2362f8756a8 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Tue, 31 Jul 2018 11:17:14 +0100 Subject: [PATCH 10/10] Add unit test for when there are no exceptions. --- .../CustomException.class | Bin 208 -> 208 bytes .../ThrowsExceptions.class | Bin 447 -> 519 bytes .../ThrowsExceptions.java | 4 +++ .../parse_java_attributes.cpp | 29 +++++++----------- 4 files changed, 15 insertions(+), 18 deletions(-) diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class b/jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class index 0fd68b551321324591f0a99a949541ea689f139d..2e0071e101a9f63e61158e7aed20da9a6394743b 100644 GIT binary patch delta 18 Zcmcb>c!6=kQEov7Mg|TB1_mYuP5>`L11JCh delta 18 Zcmcb>c!6=kQEpxaMg|TB1_mYuP5>_!10(ff$?3=9k=3<_KfoD3rD45AziVq6SN4B{X{f}KHff$?3=9k=4DwtIoD9P33?dv1qFfA23}PTcoSi{}i-8R!F3HXyHBr}& jQF>y%2b&BJgDivG#ItpbOp|>WYdIMi1c8PyF$e(wPVfwP diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java b/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java index 0836b1c3647..46bee61c6cf 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java @@ -8,6 +8,10 @@ public static void test() throws CustomException, IOException { 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 2e066aaeb3f..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 @@ -606,8 +606,6 @@ SCENARIO( { THEN("We should be able to get the list of exceptions it throws") { - const symbolt &class_symbol = - new_symbol_table.lookup_ref("java::ThrowsExceptions"); const symbolt &method_symbol = new_symbol_table.lookup_ref("java::ThrowsExceptions.test:()V"); const java_method_typet method = @@ -626,23 +624,18 @@ SCENARIO( irept("java.io.IOException").id()) != exceptions.end()); } } - } - - const symbol_tablet &new_symbol_table2 = load_java_class( - "ThrowsExceptions", "./java_bytecode/java_bytecode_parser"); - 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") + WHEN( + "Parsing the exceptions attribute for a method that throws no exceptions") { - const symbolt &class_symbol = - new_symbol_table2.lookup_ref("java::ThrowsExceptions"); - const symbolt &method_symbol = - new_symbol_table2.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() == 0); - } + 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); + } } } }