Merge pull request #2247 from antlechner/antonia/annotation-conversion

Additional functions for processing Java annotations

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -875,8 +875,9 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
 bool java_bytecode_convert_classt::is_overlay_method(const methodt &method)
 {
-  return java_bytecode_parse_treet::does_annotation_exist(
-    method.annotations, ID_overlay_method);
+  return java_bytecode_parse_treet::find_annotation(
+           method.annotations, ID_overlay_method)
+    .has_value();
 }
 
 bool java_bytecode_convert_class(
@@ -1015,24 +1016,48 @@ static void find_and_replace_parameters(
 /// \param annotations: The java_annotationt collection to populate
 void convert_annotations(
   const java_bytecode_parse_treet::annotationst &parsed_annotations,
-  std::vector<java_annotationt> &annotations)
+  std::vector<java_annotationt> &java_annotations)
 {
   for(const auto &annotation : parsed_annotations)
   {
-    annotations.emplace_back(annotation.type);
+    java_annotations.emplace_back(annotation.type);
     std::vector<java_annotationt::valuet> &values =
-      annotations.back().get_values();
+      java_annotations.back().get_values();
     std::transform(
       annotation.element_value_pairs.begin(),
       annotation.element_value_pairs.end(),
       std::back_inserter(values),
-      [](const decltype(annotation.element_value_pairs)::value_type &value)
-      {
+      [](const decltype(annotation.element_value_pairs)::value_type &value) {
         return java_annotationt::valuet(value.element_name, value.value);
       });
   }
 }
 
+/// 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/src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -99,23 +99,30 @@ void java_bytecode_parse_treet::annotationt::element_value_pairt::output(
   out << expr2java(value, ns);
 }
 
-bool java_bytecode_parse_treet::does_annotation_exist(
+/// Find an annotation given its name
+/// \param annotations: A vector of annotationt
+/// \param annotation_type_name: An irep_idt representing the name of the
+///   annotation class, e.g. java::java.lang.SuppressWarnings
+/// \return The first annotation with the given name in annotations if one
+///    exists, an empty optionalt otherwise.
+optionalt<java_bytecode_parse_treet::annotationt>
+java_bytecode_parse_treet::find_annotation(
   const annotationst &annotations,
   const irep_idt &annotation_type_name)
 {
-  return
-    std::find_if(
-      annotations.begin(),
-      annotations.end(),
-      [&annotation_type_name](const annotationt &annotation)
-      {
-        if(annotation.type.id() != ID_pointer)
-          return false;
-        typet type = annotation.type.subtype();
-        return
-          type.id() == ID_symbol
-          && to_symbol_type(type).get_identifier() == annotation_type_name;
-      }) != annotations.end();
+  const auto annotation_it = std::find_if(
+    annotations.begin(),
+    annotations.end(),
+    [&annotation_type_name](const annotationt &annotation) {
+      if(annotation.type.id() != ID_pointer)
+        return false;
+      const typet &type = annotation.type.subtype();
+      return type.id() == ID_symbol &&
+             to_symbol_type(type).get_identifier() == annotation_type_name;
+    });
+  if(annotation_it == annotations.end())
+    return {};
+  return *annotation_it;
 }
 
 void java_bytecode_parse_treet::methodt::output(std::ostream &out) const

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -54,7 +54,7 @@ class java_bytecode_parse_treet
 
   typedef std::vector<annotationt> annotationst;
 
-  static bool does_annotation_exist(
+  static optionalt<annotationt> find_annotation(
     const annotationst &annotations,
     const irep_idt &annotation_type_name);
 

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -103,8 +103,9 @@ optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
 
 static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
 {
-  return java_bytecode_parse_treet::does_annotation_exist(
-    c.annotations, ID_overlay_class);
+  return java_bytecode_parse_treet::find_annotation(
+           c.annotations, ID_overlay_class)
+    .has_value();
 }
 
 /// Check through all the places class parse trees can appear and returns the

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