From 7e28299b514c7c1feff71c12a1372fdf2acdb3cc Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 19 Dec 2018 12:21:10 +0000 Subject: [PATCH 1/4] Add parsing of the names of inner java classes This is required for correctly printing the names of inner classes. --- .../java_bytecode/java_bytecode_convert_class.cpp | 1 + jbmc/src/java_bytecode/java_bytecode_parse_tree.h | 2 +- jbmc/src/java_bytecode/java_bytecode_parser.cpp | 2 ++ jbmc/src/java_bytecode/java_types.h | 12 ++++++++++++ src/util/irep_ids.def | 1 + 5 files changed, 17 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 6200190276f..d370672d76f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -303,6 +303,7 @@ void java_bytecode_convert_classt::convert( } class_type.set_tag(c.name); + class_type.set_inner_name(c.inner_name); class_type.set(ID_abstract, c.is_abstract); class_type.set(ID_is_annotation, c.is_annotation); class_type.set(ID_interface, c.is_interface); diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 9a9fe8c0c20..5efbfcc22f5 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -213,7 +213,7 @@ struct java_bytecode_parse_treet classt &operator=(classt &&) = default; #endif - irep_idt name, super_class; + irep_idt name, super_class, inner_name; 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 2c7f8f4eb2b..c6ed74717d8 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1696,6 +1696,8 @@ void java_bytecode_parsert::rinner_classes_attribute( // This is a marker that a class is anonymous. if(inner_name_index == 0) parsed_class.is_anonymous_class = true; + else + parsed_class.inner_name = pool_entry_lambda(inner_name_index).s; // Note that if outer_class_info_index == 0, the inner class is an anonymous // or local class, and is treated as private. if(outer_class_info_index == 0) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 0fa28f8cdf1..9319c918255 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -241,6 +241,18 @@ class java_class_typet:public class_typet { set(ID_name, name); } + + /// Get the name of a java inner class. + const irep_idt &get_inner_name() const + { + return get(ID_inner_name); + } + + /// Set the name of a java inner class. + void set_inner_name(const irep_idt &name) + { + set(ID_inner_name, name); + } }; inline const java_class_typet &to_java_class_type(const typet &type) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 190f892d725..2fdfad6e5a8 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -131,6 +131,7 @@ IREP_ID_ONE(incomplete_c_enum) IREP_ID_TWO(C_incomplete, #incomplete) IREP_ID_ONE(identifier) IREP_ID_ONE(name) +IREP_ID_ONE(inner_name) IREP_ID_ONE(cpp_name) IREP_ID_ONE(component_cpp_name) IREP_ID_TWO(C_id_class, #id_class) From 2dcbb00e214beaf3809228b9ae5739197233fc78 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 19 Dec 2018 13:43:29 +0000 Subject: [PATCH 2/4] Add unit test for inner class names Added because it is good to test new features. --- jbmc/unit/Makefile | 1 + .../java_bytecode_parser/Outer$1.class | Bin 0 -> 357 bytes .../java_bytecode_parser/Outer$Inner.class | Bin 0 -> 367 bytes .../Outer$RedHerring.class | Bin 0 -> 273 bytes .../Outer$RedHerring.java | 2 + .../java_bytecode_parser/Outer.class | Bin 0 -> 386 bytes .../java_bytecode_parser/Outer.java | 7 + .../parse_inner_class.cpp | 121 ++++++++++++++++++ 8 files changed, 131 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/Outer$1.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/Outer$Inner.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/Outer$RedHerring.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/Outer$RedHerring.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/Outer.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/Outer.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index f569358baae..d1e009b831c 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -38,6 +38,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \ java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \ java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp \ + java_bytecode/java_bytecode_parser/parse_inner_class.cpp \ java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \ java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \ java_bytecode/java_bytecode_parser/parse_java_class.cpp \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$1.class b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$1.class new file mode 100644 index 0000000000000000000000000000000000000000..2e2d935ee62dc18cd287679aafe0f0bad89a507e GIT binary patch literal 357 zcmXX>Jx{|h6g;O+LQJ5cKv@|wv_(QxVr$i<0tqR=0Lt#B7Bvcvln?$F143fp2k@g1 z&u(qm@7=xAo&Edw{R7|{XAycB2yh&SI0ZD z7wT4958<*eU*)@`h#OOsRin+zy=phrI);xRMu;K3(h1WkgYPi!4d3 z*miV6>`{%VTfn0Yh{?q#*yIb|2O$rF?!ak%>{CD7su1Il5b2#8g`iK!LxLl!++`iO Ixt+Q756x6PxBvhE literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$Inner.class b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$Inner.class new file mode 100644 index 0000000000000000000000000000000000000000..182f2dcd1e699ceab00de4e51705dd28a16e4b88 GIT binary patch literal 367 zcmXYsu};G<5QhItlbE_G4Fw8p3>``*|Klttm{sAjrv% zU91WIvV7KrL1GI1(7dI(dQxf5WSEqh%Gatgw%$SC+7g2MqRaI2q1) zR-ebFIJP!6<1MhqvCG*49xp&nXP=yP4El#rq+_T_>3if=#~RJW|s6fcs954*FK+SeZ*! b1ImJx07Gl%AhgU)_!L9ZaN@05j4t3G7g0rB literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/Outer.java b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer.java new file mode 100644 index 00000000000..4842cf0e2c8 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer.java @@ -0,0 +1,7 @@ +class Outer { + class Inner { + } + + Outer anonymous = new Outer() { + }; +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp new file mode 100644 index 00000000000..6c9fa15ddc7 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp @@ -0,0 +1,121 @@ +/*******************************************************************\ + + Module: Unit tests for converting inner classes + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Parsing inner java classes", + "[core][java_bytecode][java_bytecode_parser]") +{ + GIVEN("A class file of an inner class.") + { + WHEN("Parsing an inner class called \"Inner\".") + { + const symbol_tablet &symbol_table = load_java_class( + "Outer$Inner", "./java_bytecode/java_bytecode_parser"); + const symbolt *class_symbol = symbol_table.lookup("java::Outer$Inner"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The inner class should have the inner name \"Inner\".") + { + REQUIRE(id2string(class_type->get_inner_name()) == "Inner"); + } + THEN("The inner class is not considered to be an anonymous class.") + { + REQUIRE_FALSE(class_type->get_is_anonymous_class()); + } + THEN("The inner class has the outer class \"Outer\".") + { + REQUIRE(id2string(class_type->get_outer_class()) == "Outer"); + } + } + } + GIVEN("A class file of a class which is not an inner class.") + { + WHEN("Parsing an outer class.") + { + const symbol_tablet &symbol_table = + load_java_class("Outer", "./java_bytecode/java_bytecode_parser"); + const symbolt *class_symbol = symbol_table.lookup("java::Outer"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The outer class should not have an inner name.") + { + REQUIRE(id2string(class_type->get_inner_name()).empty()); + } + THEN("The outer class is not considered to be an anonymous class.") + { + REQUIRE_FALSE(class_type->get_is_anonymous_class()); + } + THEN("The outer class does not have an outer class.") + { + REQUIRE(id2string(class_type->get_outer_class()).empty()); + } + } + } + GIVEN("A class file of an anonymous class.") + { + WHEN("Parsing an anonymous class.") + { + const symbol_tablet &symbol_table = load_java_class( + "Outer$1", "./java_bytecode/java_bytecode_parser"); + const symbolt *class_symbol = symbol_table.lookup("java::Outer$1"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The anonymous class should not have an inner name.") + { + REQUIRE(id2string(class_type->get_inner_name()).empty()); + } + THEN("The anonymous class is considered to be an anonymous class.") + { + REQUIRE(class_type->get_is_anonymous_class()); + } + THEN("The anonymous class does not have an outer class.") + { + REQUIRE(id2string(class_type->get_outer_class()).empty()); + } + } + } + GIVEN("A class file of an outer class which is named with a '$'.") + { + WHEN("Parsing an outer class named with a '$'.") + { + const symbol_tablet &symbol_table = load_java_class( + "Outer$RedHerring", "./java_bytecode/java_bytecode_parser"); + const auto *class_symbol = symbol_table.lookup("java::Outer$RedHerring"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The outer class should not have an inner name.") + { + REQUIRE(id2string(class_type->get_inner_name()).empty()); + } + THEN("The inner class is not considered to be an anonymous class.") + { + REQUIRE_FALSE(class_type->get_is_anonymous_class()); + } + THEN("The outer class does not have an outer class.") + { + REQUIRE(id2string(class_type->get_outer_class()).empty()); + } + } + } +} From 61e4d5866d551c72ba8a91067480bca2df69c1e7 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 20 Dec 2018 13:02:01 +0000 Subject: [PATCH 3/4] Add checks of `get_name()` to inner class unit test --- .../java_bytecode_parser/parse_inner_class.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp index 6c9fa15ddc7..437681b86db 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp @@ -26,6 +26,10 @@ SCENARIO( type_try_dynamic_cast(class_symbol->type); REQUIRE(class_type); + THEN("The inner class should have the name \"java::Outer$Inner\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer$Inner"); + } THEN("The inner class should have the inner name \"Inner\".") { REQUIRE(id2string(class_type->get_inner_name()) == "Inner"); @@ -52,6 +56,10 @@ SCENARIO( type_try_dynamic_cast(class_symbol->type); REQUIRE(class_type); + THEN("The outer class should have the name \"java::Outer\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer"); + } THEN("The outer class should not have an inner name.") { REQUIRE(id2string(class_type->get_inner_name()).empty()); @@ -78,6 +86,10 @@ SCENARIO( type_try_dynamic_cast(class_symbol->type); REQUIRE(class_type); + THEN("The anonymous class should have the name \"java::Outer$1\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer$1"); + } THEN("The anonymous class should not have an inner name.") { REQUIRE(id2string(class_type->get_inner_name()).empty()); @@ -104,6 +116,10 @@ SCENARIO( type_try_dynamic_cast(class_symbol->type); REQUIRE(class_type); + THEN("The outer class should have the name \"java::Outer$RedHerring\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer$RedHerring"); + } THEN("The outer class should not have an inner name.") { REQUIRE(id2string(class_type->get_inner_name()).empty()); From 28fbcce828e8f8c2cc05c67242c4cdce471aacf4 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 20 Dec 2018 13:15:03 +0000 Subject: [PATCH 4/4] Rerun inner class unit test with outer and inner loaded first --- .../parse_inner_class.cpp | 158 +++++++++--------- 1 file changed, 82 insertions(+), 76 deletions(-) diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp index 437681b86db..e6a4d11a525 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp @@ -10,97 +10,103 @@ #include #include +#include +#include + SCENARIO( "Parsing inner java classes", "[core][java_bytecode][java_bytecode_parser]") { - GIVEN("A class file of an inner class.") + for(const auto &load_first : std::vector{"Outer$Inner", "Outer"}) { - WHEN("Parsing an inner class called \"Inner\".") - { - const symbol_tablet &symbol_table = load_java_class( - "Outer$Inner", "./java_bytecode/java_bytecode_parser"); - const symbolt *class_symbol = symbol_table.lookup("java::Outer$Inner"); - REQUIRE(class_symbol); - const java_class_typet *class_type = - type_try_dynamic_cast(class_symbol->type); - REQUIRE(class_type); + const symbol_tablet &symbol_table = + load_java_class(load_first, "./java_bytecode/java_bytecode_parser"); - THEN("The inner class should have the name \"java::Outer$Inner\".") - { - REQUIRE(id2string(class_type->get_name()) == "java::Outer$Inner"); - } - THEN("The inner class should have the inner name \"Inner\".") - { - REQUIRE(id2string(class_type->get_inner_name()) == "Inner"); - } - THEN("The inner class is not considered to be an anonymous class.") - { - REQUIRE_FALSE(class_type->get_is_anonymous_class()); - } - THEN("The inner class has the outer class \"Outer\".") + GIVEN("A class file of an inner class and " + load_first + " loaded first.") + { + WHEN("Parsing an inner class called \"Inner\".") { - REQUIRE(id2string(class_type->get_outer_class()) == "Outer"); + const symbolt *class_symbol = symbol_table.lookup("java::Outer$Inner"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The inner class should have the name \"java::Outer$Inner\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer$Inner"); + } + THEN("The inner class should have the inner name \"Inner\".") + { + REQUIRE(id2string(class_type->get_inner_name()) == "Inner"); + } + THEN("The inner class is not considered to be an anonymous class.") + { + REQUIRE_FALSE(class_type->get_is_anonymous_class()); + } + THEN("The inner class has the outer class \"Outer\".") + { + REQUIRE(id2string(class_type->get_outer_class()) == "Outer"); + } } } - } - GIVEN("A class file of a class which is not an inner class.") - { - WHEN("Parsing an outer class.") + GIVEN( + "A class file of a class which is not an inner class and " + load_first + + " loaded first.") { - const symbol_tablet &symbol_table = - load_java_class("Outer", "./java_bytecode/java_bytecode_parser"); - const symbolt *class_symbol = symbol_table.lookup("java::Outer"); - REQUIRE(class_symbol); - const java_class_typet *class_type = - type_try_dynamic_cast(class_symbol->type); - REQUIRE(class_type); - - THEN("The outer class should have the name \"java::Outer\".") - { - REQUIRE(id2string(class_type->get_name()) == "java::Outer"); - } - THEN("The outer class should not have an inner name.") + WHEN("Parsing an outer class.") { - REQUIRE(id2string(class_type->get_inner_name()).empty()); - } - THEN("The outer class is not considered to be an anonymous class.") - { - REQUIRE_FALSE(class_type->get_is_anonymous_class()); - } - THEN("The outer class does not have an outer class.") - { - REQUIRE(id2string(class_type->get_outer_class()).empty()); + const symbolt *class_symbol = symbol_table.lookup("java::Outer"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The outer class should have the name \"java::Outer\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer"); + } + THEN("The outer class should not have an inner name.") + { + REQUIRE(id2string(class_type->get_inner_name()).empty()); + } + THEN("The outer class is not considered to be an anonymous class.") + { + REQUIRE_FALSE(class_type->get_is_anonymous_class()); + } + THEN("The outer class does not have an outer class.") + { + REQUIRE(id2string(class_type->get_outer_class()).empty()); + } } } - } - GIVEN("A class file of an anonymous class.") - { - WHEN("Parsing an anonymous class.") + GIVEN( + "A class file of an anonymous class and " + load_first + " loaded first.") { - const symbol_tablet &symbol_table = load_java_class( - "Outer$1", "./java_bytecode/java_bytecode_parser"); - const symbolt *class_symbol = symbol_table.lookup("java::Outer$1"); - REQUIRE(class_symbol); - const java_class_typet *class_type = - type_try_dynamic_cast(class_symbol->type); - REQUIRE(class_type); - - THEN("The anonymous class should have the name \"java::Outer$1\".") + WHEN("Parsing an anonymous class.") { - REQUIRE(id2string(class_type->get_name()) == "java::Outer$1"); - } - THEN("The anonymous class should not have an inner name.") - { - REQUIRE(id2string(class_type->get_inner_name()).empty()); - } - THEN("The anonymous class is considered to be an anonymous class.") - { - REQUIRE(class_type->get_is_anonymous_class()); - } - THEN("The anonymous class does not have an outer class.") - { - REQUIRE(id2string(class_type->get_outer_class()).empty()); + const symbolt *class_symbol = symbol_table.lookup("java::Outer$1"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The anonymous class should have the name \"java::Outer$1\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer$1"); + } + THEN("The anonymous class should not have an inner name.") + { + REQUIRE(id2string(class_type->get_inner_name()).empty()); + } + THEN("The anonymous class is considered to be an anonymous class.") + { + REQUIRE(class_type->get_is_anonymous_class()); + } + THEN("The anonymous class does not have an outer class.") + { + REQUIRE(id2string(class_type->get_outer_class()).empty()); + } } } }