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.

Author: antlechner

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.class

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

jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.java

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

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.class

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

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.java

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

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.class

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

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.java

@@ -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());
+      }
+    }
+  }
+}