From e0ad0697fe29d7db9565194dcf63f07d4173da20 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Wed, 30 May 2018 17:18:47 +0100 Subject: [PATCH] Add support for Java annotations with Class value Java annotations can store element-value pairs, where each value is of type String, Enum, Class, annotation, array or a primitive type. The Class case was among the cases that did not have support in the java bytecode parser before. For minimal support (without storing any reference to java.lang.Class), we can just store the name of the type as retrieved from the constant pool in a symbol_exprt. --- .../java_bytecode/java_bytecode_parser.cpp | 7 +- .../AnnotationWithClassType.class | Bin 0 -> 249 bytes .../AnnotationWithClassType.java | 3 + .../ClassWithClassTypeAnnotation.class | Bin 0 -> 334 bytes .../ClassWithClassTypeAnnotation.java | 3 + .../ClassWithPrimitiveTypeAnnotation.class | Bin 0 -> 325 bytes .../ClassWithPrimitiveTypeAnnotation.java | 3 + .../ClassWithVoidTypeAnnotation.class | Bin 0 -> 315 bytes .../ClassWithVoidTypeAnnotation.java | 3 + .../module_dependencies.txt | 3 + .../parse_java_annotations.cpp | 95 ++++++++++++++++++ 11 files changed, 115 insertions(+), 2 deletions(-) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithVoidTypeAnnotation.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithVoidTypeAnnotation.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/module_dependencies.txt create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 18fb937234a..5fdf0915e2f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1509,6 +1509,9 @@ void java_bytecode_parsert::relement_value_pairs( } } +/// Corresponds to the element_value structure +/// Described in Java 8 specification 4.7.16.1 +/// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1 void java_bytecode_parsert::relement_value_pair( annotationt::element_value_pairt &element_value_pair) { @@ -1526,8 +1529,8 @@ void java_bytecode_parsert::relement_value_pair( case 'c': { - UNUSED u2 class_info_index=read_u2(); - // todo: class + u2 class_info_index = read_u2(); + element_value_pair.value = symbol_exprt(pool_entry(class_info_index).s); } break; diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.class b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.class new file mode 100644 index 0000000000000000000000000000000000000000..05ac7ad3e808ab0f009d0da8c15d32e8663d33aa GIT binary patch literal 249 zcmX^0Z`VEs1_l!bUUmj9b_Q;C1|CKR*0RK$(o{wUVGT{6ti-ZJ{hY+SbbaTX#NuLW zMh4E{%=Em(lF}le3NcI-Hd=N-MO?x8rA5i9ZkahiRWgowdHE%YC7Jno;h7~FV1q&` z3sUt!hBGpV value(); +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.class new file mode 100644 index 0000000000000000000000000000000000000000..0585c25fd0b8bed06315b422744a2f882d0ad10d GIT binary patch literal 334 zcmaJ+K}*9>4F0mMt=8$LH&G9}sRwuQwjs!1AQS~R^!!>MGowqTeJ%L2JP98B0sg3A z+Dq|bLX!7=NxtxYwqM@>u5lQmi-Q1z07HU5Wnp(i=$>CZ5qh)i#S#V)i@h&5vCWqz zPL&B4S(ztx&NUd#Qd1Pq>|UG4^8L-;ie%0>&g5!sDnmGVEXDE0-buv;t42Ff5RRi3 z{?VBbyvn4dUO9?trEzLxHD0)!Wi{!e2aj<2-+jWc-Ft}FHgOoCqo1yg)Kx>Xujs77 ffOq)``e@pLW?yOON(Vbl-9@N%PuV*93HE;h8NE?= literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.java new file mode 100644 index 00000000000..d0ed0f3d14c --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.java @@ -0,0 +1,3 @@ +@AnnotationWithClassType(java.lang.String.class) +public class ClassWithClassTypeAnnotation { +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.class new file mode 100644 index 0000000000000000000000000000000000000000..ed940e51f09fb8f636e39c40b40cb214084c7dad GIT binary patch literal 325 zcmaivK}*9x5QX2gO;TgE?XifU2f_AWFWwYE3xz^yMT?#{acQR{8%Z_+f0ie~gFnC@ zCC=v3V;5$I_jdPt%I%vToob8Jw^jzpTQD!|}Mq3?QoTDMTx+5gVk?xB+ gtu^3{zCfS#bs*gr8}g-rc0CUe$~+X;RVT*LKZ!?9mH+?% literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.java new file mode 100644 index 00000000000..80c5d1ec270 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.java @@ -0,0 +1,3 @@ +@AnnotationWithClassType(byte.class) +public class ClassWithPrimitiveTypeAnnotation { +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithVoidTypeAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithVoidTypeAnnotation.class new file mode 100644 index 0000000000000000000000000000000000000000..1cb2becfb7dc75dfcd6fa0b86b9414cea111db76 GIT binary patch literal 315 zcmaKnK}*9x5QX2gO`@^2?NLO~n|iR9-dYM$C=^NyTH<+=E;=RMm1Yz0XL%Al_yhb= z(%D>kb75w9Z+E}P{QiCa02rblqlxnf-3UEGIA+6cLTKLJC4|=0ZZx60V567iF4g +#include +#include +#include +#include + +// See +// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1 +SCENARIO( + "java_bytecode_parse_annotations", + "[core][java_bytecode][java_bytecode_parser]") +{ + GIVEN("Some class files in the class path") + { + WHEN( + "Parsing an annotation with Class value specified to non-primitive " + "(java.lang.String)") + { + const symbol_tablet &new_symbol_table = load_java_class( + "ClassWithClassTypeAnnotation", "./java_bytecode/java_bytecode_parser"); + + THEN("The annotation should store the correct type (String)") + { + const symbolt &class_symbol = + *new_symbol_table.lookup("java::ClassWithClassTypeAnnotation"); + 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 &element_value_pair = annotation.element_value_pairs.front(); + const auto &id = + to_symbol_expr(element_value_pair.value).get_identifier(); + const auto &java_type = java_type_from_string(id2string(id)); + const std::string &class_name = + id2string(to_symbol_type(java_type.subtype()).get_identifier()); + REQUIRE(id2string(class_name) == "java::java.lang.String"); + } + } + WHEN("Parsing an annotation with Class value specified to primitive (byte)") + { + const symbol_tablet &new_symbol_table = load_java_class( + "ClassWithPrimitiveTypeAnnotation", + "./java_bytecode/java_bytecode_parser"); + + THEN("The annotation should store the correct type (byte)") + { + const symbolt &class_symbol = + *new_symbol_table.lookup("java::ClassWithPrimitiveTypeAnnotation"); + 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 &element_value_pair = annotation.element_value_pairs.front(); + const auto &id = + to_symbol_expr(element_value_pair.value).get_identifier(); + const auto &java_type = java_type_from_string(id2string(id)); + REQUIRE(java_type == java_byte_type()); + } + } + WHEN("Parsing an annotation with Class value specified to void") + { + const symbol_tablet &new_symbol_table = load_java_class( + "ClassWithVoidTypeAnnotation", "./java_bytecode/java_bytecode_parser"); + + THEN("The annotation should store the correct type (void)") + { + const symbolt &class_symbol = + *new_symbol_table.lookup("java::ClassWithVoidTypeAnnotation"); + 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 &element_value_pair = annotation.element_value_pairs.front(); + const auto &id = + to_symbol_expr(element_value_pair.value).get_identifier(); + const auto &java_type = java_type_from_string(id2string(id)); + REQUIRE(java_type == void_type()); + } + } + } +}