Enable parsing of annotations on parameters

Author: NathanJPhillips

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -98,6 +98,8 @@ struct java_bytecode_parse_treet
       return instructions.back();
     }
 
+    std::vector<annotationst> parameter_annotations;
+
     struct exceptiont
     {
       exceptiont()

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1243,6 +1243,16 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
   {
     rRuntimeAnnotation_attribute(method.annotations);
   }
+  else if(
+    attribute_name == "RuntimeInvisibleParameterAnnotations" ||
+    attribute_name == "RuntimeVisibleParameterAnnotations")
+  {
+    u1 parameter_count = read_u1();
+    if(method.parameter_annotations.size() < parameter_count)
+      method.parameter_annotations.resize(parameter_count);
+    for(u2 param_no = 0; param_no < parameter_count; ++param_no)
+      rRuntimeAnnotation_attribute(method.parameter_annotations[param_no]);
+  }
   else if(attribute_name == "Exceptions")
   {
     method.throws_exception_table = rexceptions_attribute();

jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationsEverywhere.class

@@ -0,0 +1,22 @@
+@interface ClassAnnotation {
+}
+
+@interface FieldAnnotation {
+}
+
+@interface MethodAnnotation {
+}
+
+@interface ParameterAnnotation {
+}
+
+@ClassAnnotation
+public class AnnotationsEverywhere {
+    @FieldAnnotation
+    public int x;
+
+    @MethodAnnotation
+    public void foo(@ParameterAnnotation int p)
+    {
+    }
+}

jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationsEverywhere.java

@@ -11,6 +11,30 @@
 #include <java_bytecode/java_bytecode_parse_tree.h>
 #include <java_bytecode/java_types.h>
 #include <testing-utils/catch.hpp>
+#include <testing-utils/free_form_cmdline.h>
+#include <testing-utils/message.h>
+
+class test_java_bytecode_languaget : public java_bytecode_languaget
+{
+public:
+  std::vector<irep_idt> get_parsed_class_names()
+  {
+    std::vector<irep_idt> parsed_class_names;
+    for(const auto &named_class
+      : java_class_loader.get_class_with_overlays_map())
+    {
+      parsed_class_names.push_back(named_class.first);
+    }
+    return parsed_class_names;
+  }
+
+  java_class_loadert::parse_tree_with_overlayst &get_parse_trees_for_class(
+    const irep_idt &class_name)
+  {
+    //return java_class_loader(class_name);
+    return java_class_loader.get_class_with_overlays_map().at(class_name);
+  }
+};
 
 // See
 // https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1
@@ -91,5 +115,92 @@ SCENARIO(
         REQUIRE(java_type == void_type());
       }
     }
+    WHEN("Parsing a class with annotations everywhere")
+    {
+      free_form_cmdlinet command_line;
+      command_line.add_flag("no-lazy-methods");
+      command_line.add_flag("no-refine-strings");
+      test_java_bytecode_languaget language;
+      language.set_message_handler(null_message_handler);
+      language.get_language_options(command_line);
+
+      std::istringstream java_code_stream("ignored");
+      language.parse(java_code_stream, "AnnotationsEverywhere.class");
+      const java_class_loadert::parse_tree_with_overlayst &parse_trees =
+        language.get_parse_trees_for_class("AnnotationsEverywhere");
+      REQUIRE(parse_trees.size() == 1);
+      const java_bytecode_parse_treet::classt &parsed_class =
+        parse_trees.front().parsed_class;
+      auto method_it = std::find_if(
+        parsed_class.methods.begin(),
+        parsed_class.methods.end(),
+        [](const java_bytecode_parse_treet::methodt &method)
+        {
+          return method.name == "foo";
+        });
+      REQUIRE(method_it != parsed_class.methods.end());
+      const java_bytecode_parse_treet::methodt &method = *method_it;
+
+      THEN("Only the correct annotation should be on the class")
+      {
+        const java_bytecode_parse_treet::annotationst &annotations =
+          parsed_class.annotations;
+        REQUIRE(annotations.size() == 1);
+        const java_bytecode_parse_treet::annotationt &annotation =
+          annotations.front();
+        INVARIANT(
+          annotation.type.id() == ID_pointer,
+          "Annotation type should be pointer.");
+        REQUIRE(
+          annotation.type.subtype().get(ID_C_base_name) == "ClassAnnotation");
+      }
+
+      THEN("Only the correct annotation should be on the field")
+      {
+        REQUIRE(parsed_class.fields.size() == 1);
+        const java_bytecode_parse_treet::fieldt &field =
+          parsed_class.fields.front();
+        const java_bytecode_parse_treet::annotationst &annotations =
+          field.annotations;
+        REQUIRE(annotations.size() == 1);
+        const java_bytecode_parse_treet::annotationt &annotation =
+          annotations.front();
+        INVARIANT(
+          annotation.type.id() == ID_pointer,
+          "Annotation type should be pointer.");
+        REQUIRE(
+          annotation.type.subtype().get(ID_C_base_name) == "FieldAnnotation");
+      }
+
+      THEN("Only the correct annotation should be on the method")
+      {
+        const java_bytecode_parse_treet::annotationst &annotations =
+          method.annotations;
+        REQUIRE(annotations.size() == 1);
+        const java_bytecode_parse_treet::annotationt &annotation =
+          annotations.front();
+        INVARIANT(
+          annotation.type.id() == ID_pointer,
+          "Annotation type should be pointer.");
+        REQUIRE(
+          annotation.type.subtype().get(ID_C_base_name) == "MethodAnnotation");
+      }
+
+      THEN("Only the correct annotation should be on the parameter")
+      {
+        REQUIRE(method.parameter_annotations.size() == 1);
+        const java_bytecode_parse_treet::annotationst &annotations =
+          method.parameter_annotations.front();
+        REQUIRE(annotations.size() == 1);
+        const java_bytecode_parse_treet::annotationt &annotation =
+          annotations.front();
+        INVARIANT(
+          annotation.type.id() == ID_pointer,
+          "Annotation type should be pointer.");
+        REQUIRE(
+          annotation.type.subtype().get(ID_C_base_name) ==
+            "ParameterAnnotation");
+      }
+    }
   }
 }