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 00000000000..05ac7ad3e80 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.java b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.java new file mode 100644 index 00000000000..71fa13fd45a --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.java @@ -0,0 +1,3 @@ +public @interface AnnotationWithClassType { + Class 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 00000000000..0585c25fd0b Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.class differ 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 00000000000..ed940e51f09 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.class differ 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 00000000000..1cb2becfb7d Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithVoidTypeAnnotation.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithVoidTypeAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithVoidTypeAnnotation.java new file mode 100644 index 00000000000..5a8bf3ee2c6 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithVoidTypeAnnotation.java @@ -0,0 +1,3 @@ +@AnnotationWithClassType(void.class) +public class ClassWithVoidTypeAnnotation { +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/module_dependencies.txt b/jbmc/unit/java_bytecode/java_bytecode_parser/module_dependencies.txt new file mode 100644 index 00000000000..87cf9849bbf --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/module_dependencies.txt @@ -0,0 +1,3 @@ +java-testing-utils +testing-utils +java_bytecode diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp new file mode 100644 index 00000000000..5eeaa2dd097 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp @@ -0,0 +1,95 @@ +/*******************************************************************\ + + Module: Unit tests for converting annotations + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#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()); + } + } + } +}