Include annotations in Java class loading [TG-3831]

jbmc/regression/jbmc/class-loading-annotations/AnnotationWithArrayValue.java

@@ -0,0 +1,5 @@
+public @interface AnnotationWithArrayValue {
+
+  Class<?>[] value();
+
+}

jbmc/regression/jbmc/class-loading-annotations/AnnotationWithClassValue.java

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

jbmc/regression/jbmc/class-loading-annotations/ArrayValueAnnotationOnClass.java

@@ -0,0 +1,3 @@
+@AnnotationWithArrayValue({MyClassA.class, MyClassB.class})
+public class ArrayValueAnnotationOnClass {
+}

jbmc/regression/jbmc/class-loading-annotations/ArrayValueAnnotationOnField.java

@@ -0,0 +1,4 @@
+public class ArrayValueAnnotationOnField {
+  @AnnotationWithArrayValue({MyClassA.class, MyClassB.class})
+  int arrayValueAnnotatedField;
+}

jbmc/regression/jbmc/class-loading-annotations/ArrayValueAnnotationOnMethod.java

@@ -0,0 +1,4 @@
+public class ArrayValueAnnotationOnMethod {
+  @AnnotationWithArrayValue({MyClassA.class, MyClassB.class})
+  public void arrayValueAnnotatedMethod() {}
+}

jbmc/regression/jbmc/class-loading-annotations/ArrayValueAnnotationOnParameter.java

@@ -0,0 +1,4 @@
+public class ArrayValueAnnotationOnParameter {
+  public void classValueAnnotatedParameter(
+      @AnnotationWithArrayValue({MyClassA.class, MyClassB.class}) int param) {}
+}

jbmc/regression/jbmc/class-loading-annotations/ClassValueAnnotationOnClass.java

@@ -0,0 +1,3 @@
+@AnnotationWithClassValue(MyClassA.class)
+public class ClassValueAnnotationOnClass {
+}

jbmc/regression/jbmc/class-loading-annotations/ClassValueAnnotationOnField.java

@@ -0,0 +1,4 @@
+public class ClassValueAnnotationOnField {
+  @AnnotationWithClassValue(MyClassA.class)
+  int classValueAnnotatedField;
+}

jbmc/regression/jbmc/class-loading-annotations/ClassValueAnnotationOnMethod.java

@@ -0,0 +1,4 @@
+public class ClassValueAnnotationOnMethod {
+  @AnnotationWithClassValue(MyClassA.class)
+  public void classValueAnnotatedMethod() {}
+}

jbmc/regression/jbmc/class-loading-annotations/ClassValueAnnotationOnParameter.java

@@ -0,0 +1,4 @@
+public class ClassValueAnnotationOnParameter {
+  public void classValueAnnotatedParameter(
+    @AnnotationWithClassValue(MyClassA.class) int param) {}
+}

jbmc/regression/jbmc/class-loading-annotations/MyClassA.java

@@ -0,0 +1 @@
+public class MyClassA {}

jbmc/regression/jbmc/class-loading-annotations/MyClassB.java

@@ -0,0 +1 @@
+public class MyClassB {}

jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-class.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayValueAnnotationOnClass.class
+--verbosity 10
+Getting class `MyClassA' from file \.[\\/]MyClassA\.class
+Getting class `MyClassB' from file \.[\\/]MyClassB\.class
+--
+--
+This test checks that element classes of arrays that are given as values of a class-level annotation
+are loaded by java_class_loadert.

jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-field.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayValueAnnotationOnField.class
+--verbosity 10
+Getting class `MyClassA' from file \.[\\/]MyClassA\.class
+Getting class `MyClassB' from file \.[\\/]MyClassB\.class
+--
+--
+This test checks that element classes of arrays that are given as values of a field-level annotation
+are loaded by java_class_loadert.

jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-method.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayValueAnnotationOnMethod.class
+--verbosity 10
+Getting class `MyClassA' from file \.[\\/]MyClassA\.class
+Getting class `MyClassB' from file \.[\\/]MyClassB\.class
+--
+--
+This test checks that element classes of arrays that are given as values of a method-level
+annotation are loaded by java_class_loadert.

jbmc/regression/jbmc/class-loading-annotations/test-array-value-annotation-on-parameter.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayValueAnnotationOnParameter.class
+--verbosity 10
+Getting class `MyClassA' from file \.[\\/]MyClassA\.class
+Getting class `MyClassB' from file \.[\\/]MyClassB\.class
+--
+--
+This test checks that element classes of arrays that are given as values of an annotation at method
+parameter level are loaded by java_class_loadert.

jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-class.desc

@@ -0,0 +1,9 @@
+CORE
+ClassValueAnnotationOnClass.class
+--verbosity 10
+Getting class `MyClassA' from file \.[\\/]MyClassA\.class
+--
+MyClassB
+--
+This test checks that classes that are given as values of a class-level annotation are loaded by
+java_class_loadert.

jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-field.desc

@@ -0,0 +1,9 @@
+CORE
+ClassValueAnnotationOnField.class
+--verbosity 10
+Getting class `MyClassA' from file \.[\\/]MyClassA\.class
+--
+MyClassB
+--
+This test checks that classes that are given as values of a field-level annotation are loaded by
+java_class_loadert.

jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-method.desc

@@ -0,0 +1,9 @@
+CORE
+ClassValueAnnotationOnMethod.class
+--verbosity 10
+Getting class `MyClassA' from file \.[\\/]MyClassA\.class
+--
+MyClassB
+--
+This test checks that classes that are given as values of a method-level annotation are loaded by
+java_class_loadert.

jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-parameter.desc

@@ -0,0 +1,9 @@
+CORE
+ClassValueAnnotationOnParameter.class
+--verbosity 10
+Getting class `MyClassA' from file \.[\\/]MyClassA\.class
+--
+MyClassB
+--
+This test checks that classes that are given as values of an annotation at method parameter level
+are loaded by java_class_loadert.

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -134,6 +134,9 @@ class java_bytecode_parsert:public parsert
   void rbytecode(methodt::instructionst &);
   void get_class_refs();
   void get_class_refs_rec(const typet &);
+  void get_annotation_class_refs(
+    const java_bytecode_parse_treet::annotationst &annotations);
+  void get_annotation_value_class_refs(const exprt &value);
   void parse_local_variable_type_table(methodt &method);
   optionalt<lambda_method_handlet>
   parse_method_handle(const class method_handle_infot &entry);
@@ -525,11 +528,9 @@ void java_bytecode_parsert::rClassFile()
   parse_tree.loading_successful=true;
 }
 
+/// Get the class references for the benefit of a dependency analysis.
 void java_bytecode_parsert::get_class_refs()
 {
-  // Get the class references for the benefit of a dependency
-  // analysis.
-
   for(const auto &c : constant_pool)
   {
     switch(c.tag)
@@ -549,8 +550,11 @@ void java_bytecode_parsert::get_class_refs()
     }
   }
 
+  get_annotation_class_refs(parse_tree.parsed_class.annotations);
+
   for(const auto &field : parse_tree.parsed_class.fields)
   {
+    get_annotation_class_refs(field.annotations);
     typet field_type;
     if(field.signature.has_value())
     {
@@ -572,6 +576,9 @@ void java_bytecode_parsert::get_class_refs()
 
   for(const auto &method : parse_tree.parsed_class.methods)
   {
+    get_annotation_class_refs(method.annotations);
+    for(const auto &parameter_annotations : method.parameter_annotations)
+      get_annotation_class_refs(parameter_annotations);
     typet method_type;
     if(method.signature.has_value())
     {
@@ -637,6 +644,41 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)
     get_class_refs_rec(src.subtype());
 }
 
+/// For each of the given annotations, get a reference to its class and
+/// recursively get class references of the values it stores.
+void java_bytecode_parsert::get_annotation_class_refs(
+  const java_bytecode_parse_treet::annotationst &annotations)
+{
+  for(const auto &annotation : annotations)
+  {
+    get_class_refs_rec(annotation.type);
+    for(const auto &element_value_pair : annotation.element_value_pairs)
+      get_annotation_value_class_refs(element_value_pair.value);
+  }
+}
+
+/// See \ref java_bytecode_parsert::get_annotation_class_refs.
+/// For the different cases of `exprt`, see \ref
+/// java_bytecode_parsert::get_relement_value.
+void java_bytecode_parsert::get_annotation_value_class_refs(const exprt &value)
+{
+  if(const auto &symbol_expr = expr_try_dynamic_cast<symbol_exprt>(value))
+  {
+    const irep_idt &value_id = symbol_expr->get_identifier();
+    const typet value_type = java_type_from_string(id2string(value_id));
+    get_class_refs_rec(value_type);
+  }
+  else if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(value))
+  {
+    for(const exprt &operand : array_expr->operands())
+      get_annotation_value_class_refs(operand);
+  }
+  // TODO: enum and nested annotation cases (once these are correctly parsed by
+  // get_relement_value).
+  // Note that in the cases where expr is a string or primitive type, no
+  // additional class references are needed.
+}
+
 void java_bytecode_parsert::rconstant_pool()
 {
   u2 constant_pool_count=read_u2();