From ac6c7d4ed926522b15ef9792c99ee2d493cb87ca Mon Sep 17 00:00:00 2001
From: johndumbell <john.dumbell@diffblue.com>
Date: Tue, 24 Jul 2018 15:29:14 +0100
Subject: [PATCH] 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.
---
 .../java_bytecode/java_bytecode_parser.cpp    |  33 ++++++++----------
 .../AnnotationWithStringArray.class           | Bin 0 -> 239 bytes
 .../AnnotationWithStringArray.java            |   3 ++
 .../ClassWithArrayAnnotation.class            | Bin 0 -> 410 bytes
 .../ClassWithArrayAnnotation.java             |   3 ++
 .../parse_java_annotations.cpp                |  25 +++++++++++++
 6 files changed, 46 insertions(+), 18 deletions(-)
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.java
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithArrayAnnotation.class
 create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithArrayAnnotation.java

diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index 57301eff756..45e8f51e76a 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -126,7 +126,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);
@@ -1511,16 +1511,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();
 
@@ -1531,50 +1532,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;
   }
 }
 
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.class b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.class
new file mode 100644
index 0000000000000000000000000000000000000000..95e187131c26168fb07b40f7807da6c6094e96fe
GIT binary patch
literal 239
zcmX^0Z`VEs1_l!b9(D#!b_OnX25v?M*0RK$(o{wUQ4P&#pRB~PME#t^ymbBGlA_GK
zbZbTiLC3tj{F20y%=|o;)U?FXoDxO`uHgLAqU2P!%p9ObIfR1n%#sX<M#rL}#7aGo
zaf}R-I2AB52q0|qPs&P71{yAp5K4qwt&cE6jgf(ofeDD2fqr3RVPs%oU<LBnfIQ}C
NkPrhqkYr-u007ZpL5~0c

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.java b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.java
new file mode 100644
index 00000000000..ae5bad91919
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.java
@@ -0,0 +1,3 @@
+public @interface AnnotationWithStringArray {
+    String[] value() default {};
+}
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithArrayAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithArrayAnnotation.class
new file mode 100644
index 0000000000000000000000000000000000000000..7cd4048903f6a52849d4f7177f8cf0d40702f884
GIT binary patch
literal 410
zcmZ`#O-sZu5Pj+PLu++ER1g<IZ|cEbyeUFi5rm@P%6jmW*09aeO(9JS{wz;|2Y-M+
zN}Lp7Pn(c8^WG%$hWz|~eFM0}euy4M0d@oIG5FU~Npr){J3X5*xRdHlF!WQY#6z>p
zgns5(Ny;d#a$e53mX`mEt|?^AaF|X?Ue_<u6p7aSJyEJM+{j8@F@)2q(Yd&jw#(7F
zix&&ta)$9!ql{dNd)3NXlF_Oa`Ha&QwPsVJrJ8q^WaPEHY{<jC<t>FMp&<&Pk1dVh
z!ecmCXU{OO1H>g)^Y}4ah}_@=4t<nej5fU|^ohkC2fXu7un!U(1cW}xHs2tOy4=Gi
Y!cN=jFv2#)A=P&1^k3oB7}Oa40jD5h-2eap

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithArrayAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithArrayAnnotation.java
new file mode 100644
index 00000000000..ee865d5f287
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithArrayAnnotation.java
@@ -0,0 +1,3 @@
+@AnnotationWithStringArray({"Dave", "Another Dave"})
+public class ClassWithArrayAnnotation {
+}
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
index 5eeaa2dd097..aaac5ca4ac8 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
@@ -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");
+      }
+    }
   }
 }