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.

Author: antlechner

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_annotationt> &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

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<java_annotationt> &annotations);
 
+void convert_java_annotations(
+  const std::vector<java_annotationt> &java_annotations,
+  java_bytecode_parse_treet::annotationst &annotations);
+
 void mark_java_implicitly_generic_class_type(
   const irep_idt &class_name,
   symbol_tablet &symbol_table);

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 \

jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.class

@@ -0,0 +1,3 @@
+@MyClassAnnotation(6)
+public class ClassWithClassAnnotation {
+}

jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.java

@@ -0,0 +1,7 @@
+public class ClassWithMethodAnnotation {
+
+    @MyMethodAnnotation(methodValue = 11)
+    public void myMethod() {
+    }
+
+}

jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.class

@@ -0,0 +1,3 @@
+public @interface MyClassAnnotation {
+    int value();
+}

jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.java

@@ -0,0 +1,3 @@
+public @interface MyMethodAnnotation {
+    int methodValue();
+}

jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.class

@@ -0,0 +1,76 @@
+/*******************************************************************\
+
+ 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>
+
+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_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 &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_annotationt> &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);
+      }
+    }
+  }
+}