From 4b7a195bd1cf7d18a557fa4a4f353a229e533126 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Fri, 25 May 2018 11:03:11 +0100 Subject: [PATCH 1/4] Improve naming of annotation variables This makes it easier to distinguish between variables of type annotationt and java_annotationt. --- jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 178dddad5ea..915f536e5cf 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -1015,19 +1015,18 @@ static void find_and_replace_parameters( /// \param annotations: The java_annotationt collection to populate void convert_annotations( const java_bytecode_parse_treet::annotationst &parsed_annotations, - std::vector &annotations) + std::vector &java_annotations) { for(const auto &annotation : parsed_annotations) { - annotations.emplace_back(annotation.type); + java_annotations.emplace_back(annotation.type); std::vector &values = - annotations.back().get_values(); + java_annotations.back().get_values(); std::transform( annotation.element_value_pairs.begin(), annotation.element_value_pairs.end(), std::back_inserter(values), - [](const decltype(annotation.element_value_pairs)::value_type &value) - { + [](const decltype(annotation.element_value_pairs)::value_type &value) { return java_annotationt::valuet(value.element_name, value.value); }); } From 1db0af4771ba4710c7aec31e776da4eb2a9727c4 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Fri, 25 May 2018 11:57:47 +0100 Subject: [PATCH 2/4] Define inverse function of convert_annotations This function can be used to retrieve annotations from a symbol table. A unit test is added for this functionality. --- .../java_bytecode_convert_class.cpp | 25 ++++++ .../java_bytecode_convert_class.h | 4 + jbmc/unit/Makefile | 1 + .../ClassWithClassAnnotation.class | Bin 0 -> 304 bytes .../ClassWithClassAnnotation.java | 3 + .../ClassWithMethodAnnotation.class | Bin 0 -> 363 bytes .../ClassWithMethodAnnotation.java | 7 ++ .../MyClassAnnotation.class | Bin 0 -> 176 bytes .../MyClassAnnotation.java | 3 + .../MyMethodAnnotation.class | Bin 0 -> 184 bytes .../MyMethodAnnotation.java | 3 + .../convert_java_annotations.cpp | 76 ++++++++++++++++++ 12 files changed, 122 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 915f536e5cf..13533e7933b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -1032,6 +1032,31 @@ void convert_annotations( } } +/// Convert java annotations, e.g. as retrieved from the symbol table, back +/// to type annotationt (inverse of convert_annotations()) +/// \param java_annotations: The java_annotationt collection to convert +/// \param annotations: The annotationt collection to populate +void convert_java_annotations( + const std::vector &java_annotations, + java_bytecode_parse_treet::annotationst &annotations) +{ + for(const auto &java_annotation : java_annotations) + { + annotations.emplace_back(java_bytecode_parse_treet::annotationt()); + auto &annotation = annotations.back(); + annotation.type = java_annotation.get_type(); + + std::transform( + java_annotation.get_values().begin(), + java_annotation.get_values().end(), + std::back_inserter(annotation.element_value_pairs), + [](const java_annotationt::valuet &value) + -> java_bytecode_parse_treet::annotationt::element_value_pairt { + return {value.get_name(), value.get_value()}; + }); + } +} + /// Checks if the class is implicitly generic, i.e., it is an inner class of /// any generic class. All uses of the implicit generic type parameters within /// the inner class are updated to point to the type parameters of the diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_class.h index 3693290491f..6fad2c8c17a 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.h @@ -33,6 +33,10 @@ void convert_annotations( const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector &annotations); +void convert_java_annotations( + const std::vector &java_annotations, + java_bytecode_parse_treet::annotationst &annotations); + void mark_java_implicitly_generic_class_type( const irep_idt &class_name, symbol_tablet &symbol_table); diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 4614a36e024..16da78dcda2 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -9,6 +9,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \ java_bytecode/goto-programs/class_hierarchy_graph.cpp \ java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp \ java_bytecode/java_bytecode_convert_class/convert_abstract_class.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_object_factory/gen_nondet_string_init.cpp \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.class new file mode 100644 index 0000000000000000000000000000000000000000..e24c8e6889675d8f24951d813bfb4ddb45bfe322 GIT binary patch literal 304 zcmZ`!O>4qH5Pf65+SIDWOF=yJWr9E%#q9btwW)tvd^;GDgKfoU) zPI3_n&M+VE?LKB^fB5|a@Q9lb4jKWP0a^tAnGM?)g44VIAh=Qbr3uXm8$Hc8vEI&A zoCp)Xr}=iFM_ht#l&CEGWV@=Gp)sjdmQ(YvR)r#TX1TGv(PL9^#-cy{$O!Gp>+YZK ziQp9~$+aUZ`gOSQ2)E~^5L)G&L88oZ@D{K2!r~4!Ijb}h7rkU(P`AQ>*Z%>1SI>cD VUucM=hKs6RB9wY1Y#H@2u8+($MCkwk literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.java new file mode 100644 index 00000000000..3bc08c8de17 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.java @@ -0,0 +1,3 @@ +@MyClassAnnotation(6) +public class ClassWithClassAnnotation { +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.class new file mode 100644 index 0000000000000000000000000000000000000000..4d3c00d3b06c8e4614f7875484b0020163b2e264 GIT binary patch literal 363 zcmZ{f!AiqG5QhIrnxrPxR`F6q!JB%p7jG4z6of*npiA!3XF= ziIXT41Q&K@_y50{-PwG7d;++_K@1=52%QM~gz%aTyBmUkc0MIEhIXzA?J*mDSLUf+ zJ*hMkrJ27@v|HFY;pm|>j&nUSYc5#afic!8$JP{t!|~*o+{%4IlGoK!m6h6;e gVVW8v10w?y5HkZ^#mK_Qz{0=^Vll7*NhSt%0MgkkvH$=8 literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.java new file mode 100644 index 00000000000..2e9ece03aea --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.java @@ -0,0 +1,3 @@ +public @interface MyClassAnnotation { + int value(); +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.class new file mode 100644 index 0000000000000000000000000000000000000000..7c9b3a732855572b5478e22952a516b714edcdd2 GIT binary patch literal 184 zcmX^0Z`VEs1_l!bZgvI^b_Py%1};Vh?%dRpjQo_a#GKMpMh0dLO;1J!uHgLAqU2P! z%p9PQxNoH|Sczj^UVcepNoIbYURGjRA|rzkrVJy407yCSz{0=^Vll7*NhSt%0O+MJ@c;k- literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.java new file mode 100644 index 00000000000..9aa2e0be0e0 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.java @@ -0,0 +1,3 @@ +public @interface MyMethodAnnotation { + int methodValue(); +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp new file mode 100644 index 00000000000..6ecbe704bf2 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp @@ -0,0 +1,76 @@ +/*******************************************************************\ + + Module: Unit tests for converting annotations + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +SCENARIO( + "java_bytecode_convert_annotations", + "[core][java_bytecode][java_bytecode_convert_class]") +{ + GIVEN("Some class files in the class path") + { + WHEN("Parsing a class with class-level annotation MyClassAnnotation(6)") + { + const symbol_tablet &new_symbol_table = load_java_class( + "ClassWithClassAnnotation", + "./java_bytecode/java_bytecode_convert_class"); + + THEN("The annotation should have the correct structure") + { + const symbolt &class_symbol = + *new_symbol_table.lookup("java::ClassWithClassAnnotation"); + const std::vector &java_annotations = + to_annotated_type(class_symbol.type).get_annotations(); + java_bytecode_parse_treet::annotationst annotations; + convert_java_annotations(java_annotations, annotations); + REQUIRE(annotations.size() == 1); + const auto &annotation = annotations.front(); + const auto &identifier = + to_symbol_type(annotation.type.subtype()).get_identifier(); + REQUIRE(id2string(identifier) == "java::MyClassAnnotation"); + const auto &element_value_pair = annotation.element_value_pairs.front(); + const auto &element_name = element_value_pair.element_name; + REQUIRE(id2string(element_name) == "value"); + const auto &expr = element_value_pair.value; + const auto comp_expr = from_integer(6, java_int_type()); + REQUIRE(expr == comp_expr); + } + } + WHEN("Parsing a class with method-level annotation MyMethodAnnotation(11)") + { + const symbol_tablet &new_symbol_table = load_java_class( + "ClassWithMethodAnnotation", + "./java_bytecode/java_bytecode_convert_class"); + + THEN("The annotation should have the correct structure") + { + const symbolt &method_symbol = *new_symbol_table.lookup( + "java::ClassWithMethodAnnotation.myMethod:()V"); + const std::vector &java_annotations = + to_annotated_type(method_symbol.type).get_annotations(); + java_bytecode_parse_treet::annotationst annotations; + convert_java_annotations(java_annotations, annotations); + REQUIRE(annotations.size() == 1); + const auto &annotation = annotations.front(); + const auto &identifier = + to_symbol_type(annotation.type.subtype()).get_identifier(); + REQUIRE(id2string(identifier) == "java::MyMethodAnnotation"); + const auto &element_value_pair = annotation.element_value_pairs.front(); + const auto &element_name = element_value_pair.element_name; + REQUIRE(id2string(element_name) == "methodValue"); + const auto &expr = element_value_pair.value; + const auto &comp_expr = from_integer(11, java_int_type()); + REQUIRE(expr == comp_expr); + } + } + } +} From 1fa0b97324097f025d929b2f1b9666c9ac964388 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Fri, 25 May 2018 13:58:11 +0100 Subject: [PATCH 3/4] Generalize and rename does_annotation_exist Making the function return an optionalt instead of a boolean provides some additional functionality without adding much complexity to the existing code that calls it. --- .../java_bytecode_convert_class.cpp | 5 +-- .../java_bytecode_parse_tree.cpp | 35 +++++++++++-------- .../java_bytecode/java_bytecode_parse_tree.h | 2 +- jbmc/src/java_bytecode/java_class_loader.cpp | 5 +-- 4 files changed, 28 insertions(+), 19 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 13533e7933b..706b61a0ecc 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -875,8 +875,9 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) bool java_bytecode_convert_classt::is_overlay_method(const methodt &method) { - return java_bytecode_parse_treet::does_annotation_exist( - method.annotations, ID_overlay_method); + return java_bytecode_parse_treet::find_annotation( + method.annotations, ID_overlay_method) + .has_value(); } bool java_bytecode_convert_class( diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp index 673ed6d22d2..bbd985182fc 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -99,23 +99,30 @@ void java_bytecode_parse_treet::annotationt::element_value_pairt::output( out << expr2java(value, ns); } -bool java_bytecode_parse_treet::does_annotation_exist( +/// Find an annotation given its name +/// \param annotations: A vector of annotationt +/// \param annotation_type_name: An irep_idt representing the name of the +/// annotation class, e.g. java::java.lang.SuppressWarnings +/// \return The first annotation with the given name in annotations if one +/// exists, an empty optionalt otherwise. +optionalt +java_bytecode_parse_treet::find_annotation( const annotationst &annotations, const irep_idt &annotation_type_name) { - return - std::find_if( - annotations.begin(), - annotations.end(), - [&annotation_type_name](const annotationt &annotation) - { - if(annotation.type.id() != ID_pointer) - return false; - typet type = annotation.type.subtype(); - return - type.id() == ID_symbol - && to_symbol_type(type).get_identifier() == annotation_type_name; - }) != annotations.end(); + const auto annotation_it = std::find_if( + annotations.begin(), + annotations.end(), + [&annotation_type_name](const annotationt &annotation) { + if(annotation.type.id() != ID_pointer) + return false; + const typet &type = annotation.type.subtype(); + return type.id() == ID_symbol && + to_symbol_type(type).get_identifier() == annotation_type_name; + }); + if(annotation_it == annotations.end()) + return {}; + return *annotation_it; } void java_bytecode_parse_treet::methodt::output(std::ostream &out) const diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 7d5adcff2d0..4baa6fd1dba 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -54,7 +54,7 @@ class java_bytecode_parse_treet typedef std::vector annotationst; - static bool does_annotation_exist( + static optionalt find_annotation( const annotationst &annotations, const irep_idt &annotation_type_name); diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 2541e4eeb76..3104c52e084 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -103,8 +103,9 @@ optionalt java_class_loadert::get_class_from_jar( static bool is_overlay_class(const java_bytecode_parse_treet::classt &c) { - return java_bytecode_parse_treet::does_annotation_exist( - c.annotations, ID_overlay_class); + return java_bytecode_parse_treet::find_annotation( + c.annotations, ID_overlay_class) + .has_value(); } /// Check through all the places class parse trees can appear and returns the From 3a7135aad06687c5d972705c2a9a2f70c59f98e4 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Wed, 30 May 2018 11:17:46 +0100 Subject: [PATCH 4/4] Add module_dependencies.txt in test folder This is required for a new check in cpplint. --- .../java_bytecode_convert_class/module_dependencies.txt | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_class/module_dependencies.txt diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/module_dependencies.txt b/jbmc/unit/java_bytecode/java_bytecode_convert_class/module_dependencies.txt new file mode 100644 index 00000000000..87cf9849bbf --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/module_dependencies.txt @@ -0,0 +1,3 @@ +java-testing-utils +testing-utils +java_bytecode