Parse java arrays in annotations properly

Previously the value from the arrays was being parsed correctly but into an object which was then immediately thrown away, so the value was never really used.

Author: JohnDumbell

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -125,7 +125,7 @@ class java_bytecode_parsert:public parsert
   void rRuntimeAnnotation_attribute(annotationst &);
   void rRuntimeAnnotation(annotationt &);
   void relement_value_pairs(annotationt::element_value_pairst &);
-  void relement_value_pair(annotationt::element_value_pairt &);
+  exprt get_relement_value();
   void rmethod_attribute(methodt &method);
   void rfield_attribute(fieldt &);
   void rcode_attribute(methodt &method);
@@ -1507,16 +1507,17 @@ void java_bytecode_parsert::relement_value_pairs(
   {
     u2 element_name_index=read_u2();
     element_value_pair.element_name=pool_entry(element_name_index).s;
-
-    relement_value_pair(element_value_pair);
+    element_value_pair.value = get_relement_value();
   }
 }
 
 /// Corresponds to the element_value structure
 /// Described in Java 8 specification 4.7.16.1
 /// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1
-void java_bytecode_parsert::relement_value_pair(
-  annotationt::element_value_pairt &element_value_pair)
+/// \returns An exprt that represents the particular value of annotations field.
+///   This is usually one of: a byte, number of some sort, string, character,
+///   enum, Class type, array or another annotation.
+exprt java_bytecode_parsert::get_relement_value()
 {
   u1 tag=read_u1();
 
@@ -1527,50 +1528,46 @@ void java_bytecode_parsert::relement_value_pair(
       UNUSED_u2(type_name_index);
       UNUSED_u2(const_name_index);
       // todo: enum
+      return exprt();
     }
-    break;
 
   case 'c':
     {
       u2 class_info_index = read_u2();
-      element_value_pair.value = symbol_exprt(pool_entry(class_info_index).s);
+      return symbol_exprt(pool_entry(class_info_index).s);
     }
-    break;
 
   case '@':
     {
+      // TODO: return this wrapped in an exprt
       // another annotation, recursively
       annotationt annotation;
       rRuntimeAnnotation(annotation);
+      return exprt();
     }
-    break;
 
   case '[':
     {
+      array_exprt values;
       u2 num_values=read_u2();
       for(std::size_t i=0; i<num_values; i++)
       {
-        annotationt::element_value_pairt element_value;
-        relement_value_pair(element_value); // recursive call
+        values.operands().push_back(get_relement_value());
       }
+      return values;
     }
-    break;
 
   case 's':
     {
       u2 const_value_index=read_u2();
-      element_value_pair.value=string_constantt(
-        pool_entry(const_value_index).s);
+      return string_constantt(pool_entry(const_value_index).s);
     }
-    break;
 
   default:
     {
       u2 const_value_index=read_u2();
-      element_value_pair.value=constant(const_value_index);
+      return constant(const_value_index);
     }
-
-  break;
   }
 }
 

jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.class

@@ -0,0 +1,3 @@
+public @interface AnnotationWithStringArray {
+    String[] value() default {};
+}

jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.java

@@ -0,0 +1,3 @@
+@AnnotationWithStringArray({"Dave", "Another Dave"})
+public class ClassWithArrayAnnotation {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithArrayAnnotation.class

@@ -91,5 +91,30 @@ SCENARIO(
         REQUIRE(java_type == void_type());
       }
     }
+    WHEN("Parsing an annotation with an array field.")
+    {
+      const symbol_tablet &new_symbol_table = load_java_class(
+        "ClassWithArrayAnnotation", "./java_bytecode/java_bytecode_parser");
+
+      THEN("The annotation should store an array of type string.")
+      {
+        const symbolt &class_symbol =
+          *new_symbol_table.lookup("java::ClassWithArrayAnnotation");
+        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 &element_value_pair = annotation.element_value_pairs.front();
+        const auto &array = to_array_expr(element_value_pair.value);
+
+        REQUIRE(array.operands().size() == 2);
+        const auto &dave = array.op0().get(ID_value);
+        const auto &another_dave = array.op1().get(ID_value);
+        REQUIRE(id2string(dave) == "Dave");
+        REQUIRE(id2string(another_dave) == "Another Dave");
+      }
+    }
   }
 }