Add support for Java annotations with Class value

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;
 

jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.java

@@ -0,0 +1,3 @@
+public @interface AnnotationWithClassType {
+    Class<?> value();
+}

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.java

@@ -0,0 +1,3 @@
+@AnnotationWithClassType(java.lang.String.class)
+public class ClassWithClassTypeAnnotation {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.java

@@ -0,0 +1,3 @@
+@AnnotationWithClassType(byte.class)
+public class ClassWithPrimitiveTypeAnnotation {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithVoidTypeAnnotation.java

@@ -0,0 +1,3 @@
+@AnnotationWithClassType(void.class)
+public class ClassWithVoidTypeAnnotation {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/module_dependencies.txt

@@ -0,0 +1,3 @@
+java-testing-utils
+testing-utils
+java_bytecode

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 <java-testing-utils/load_java_class.h>
+#include <java_bytecode/java_bytecode_convert_class.h>
+#include <java_bytecode/java_bytecode_parse_tree.h>
+#include <java_bytecode/java_types.h>
+#include <testing-utils/catch.hpp>
+
+// 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_annotationt> &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_annotationt> &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_annotationt> &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());
+      }
+    }
+  }
+}