Add annotations to java_class_typet, its methods and fields

Add the annotations parsed from the byte code to classes/fields/methods and static fields (globals) in the symbol table

Author: NathanJPhillips

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -68,6 +68,7 @@ class java_bytecode_convert_classt:public messaget
 
   typedef java_bytecode_parse_treet::classt classt;
   typedef java_bytecode_parse_treet::fieldt fieldt;
+  typedef java_bytecode_parse_treet::annotationt annotationt;
 
 protected:
   symbol_tablet &symbol_table;
@@ -306,6 +307,10 @@ void java_bytecode_convert_classt::convert(const classt &c)
     }
   }
 
+  // Load annotations
+  if(!c.annotations.empty())
+    convert_annotations(c.annotations, class_type.get_annotations());
+
   // produce class symbol
   symbolt new_symbol;
   new_symbol.base_name=c.name;
@@ -441,6 +446,14 @@ void java_bytecode_convert_classt::convert(
         ns,
         get_message_handler());
 
+    // Load annotations
+    if(!f.annotations.empty())
+    {
+      convert_annotations(
+        f.annotations,
+        static_cast<annotated_typet &>(new_symbol.type).get_annotations());
+    }
+
     // Do we have the static field symbol already?
     const auto s_it=symbol_table.symbols.find(new_symbol.name);
     if(s_it!=symbol_table.symbols.end())
@@ -453,7 +466,7 @@ void java_bytecode_convert_classt::convert(
   {
     class_typet &class_type=to_class_type(class_symbol.type);
 
-    class_type.components().push_back(class_typet::componentt());
+    class_type.components().emplace_back();
     class_typet::componentt &component=class_type.components().back();
 
     component.set_name(f.name);
@@ -469,6 +482,14 @@ void java_bytecode_convert_classt::convert(
       component.set_access(ID_public);
     else
       component.set_access(ID_default);
+
+    // Load annotations
+    if(!f.annotations.empty())
+    {
+      convert_annotations(
+        f.annotations,
+        static_cast<annotated_typet &>(component.type()).get_annotations());
+    }
   }
 }
 
@@ -774,6 +795,29 @@ static void find_and_replace_parameters(
   }
 }
 
+/// Convert parsed annotations into the symbol table
+/// \param parsed_annotations: The parsed annotations to convert
+/// \param annotations: The java_annotationt collection to populate
+void convert_annotations(
+  const java_bytecode_parse_treet::annotationst &parsed_annotations,
+  std::vector<java_annotationt> &annotations)
+{
+  for(const auto &annotation : parsed_annotations)
+  {
+    annotations.emplace_back(annotation.type);
+    std::vector<java_annotationt::valuet> &values =
+      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)
+      {
+        return java_annotationt::valuet(value.element_name, value.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

src/java_bytecode/java_bytecode_convert_class.h

@@ -27,6 +27,10 @@ bool java_bytecode_convert_class(
   method_bytecodet &,
   java_string_library_preprocesst &string_preprocess);
 
+void convert_annotations(
+  const java_bytecode_parse_treet::annotationst &parsed_annotations,
+  std::vector<java_annotationt> &annotations);
+
 void mark_java_implicitly_generic_class_type(
   const irep_idt &class_name,
   symbol_tablet &symbol_table);

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -366,6 +366,15 @@ void java_bytecode_convert_method_lazy(
     parameters.insert(parameters.begin(), this_p);
   }
 
+  // Load annotations
+  if(!m.annotations.empty())
+  {
+    convert_annotations(
+      m.annotations,
+      static_cast<annotated_typet &>(static_cast<typet &>(member_type))
+        .get_annotations());
+  }
+
   method_symbol.type=member_type;
   symbol_table.add(method_symbol);
 }

src/java_bytecode/java_types.h

@@ -18,6 +18,69 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/optional.h>
 
+class java_annotationt : public irept
+{
+public:
+  class valuet : public irept
+  {
+  public:
+    valuet(irep_idt name, const exprt &value) : irept(name)
+    {
+      get_sub().push_back(value);
+    }
+
+    const irep_idt &get_name() const
+    {
+      return id();
+    }
+
+    const exprt &get_value() const
+    {
+      return static_cast<const exprt &>(get_sub().front());
+    }
+  };
+
+  explicit java_annotationt(const typet &type)
+  {
+    set(ID_type, type);
+  }
+
+  const typet &get_type() const
+  {
+    return static_cast<const typet &>(find(ID_type));
+  }
+
+  const std::vector<valuet> &get_values() const
+  {
+    // This cast should be safe as valuet doesn't add data to irept
+    return reinterpret_cast<const std::vector<valuet> &>(get_sub());
+  }
+
+  std::vector<valuet> &get_values()
+  {
+    // This cast should be safe as valuet doesn't add data to irept
+    return reinterpret_cast<std::vector<valuet> &>(get_sub());
+  }
+};
+
+class annotated_typet : public typet
+{
+public:
+  const std::vector<java_annotationt> &get_annotations() const
+  {
+    // This cast should be safe as java_annotationt doesn't add data to irept
+    return reinterpret_cast<const std::vector<java_annotationt> &>(
+      find(ID_annotations).get_sub());
+  }
+
+  std::vector<java_annotationt> &get_annotations()
+  {
+    // This cast should be safe as java_annotationt doesn't add data to irept
+    return reinterpret_cast<std::vector<java_annotationt> &>(
+      add(ID_annotations).get_sub());
+  }
+};
+
 class java_class_typet:public class_typet
 {
  public:
@@ -30,6 +93,18 @@ class java_class_typet:public class_typet
   {
     return set(ID_access, access);
   }
+
+  const std::vector<java_annotationt> &get_annotations() const
+  {
+    return static_cast<const annotated_typet &>(
+      static_cast<const typet &>(*this)).get_annotations();
+  }
+
+  std::vector<java_annotationt> &get_annotations()
+  {
+    return static_cast<annotated_typet &>(
+      static_cast<typet &>(*this)).get_annotations();
+  }
 };
 
 inline const java_class_typet &to_java_class_type(const typet &type)

src/util/irep_ids.def

@@ -839,6 +839,7 @@ IREP_ID_TWO(type_variables, #type_variables)
 IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
+IREP_ID_ONE(annotations)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO