From 98de899d267390fe285be83b07cc9cf8d0862411 Mon Sep 17 00:00:00 2001
From: Chris Ryder <chris.ryder@diffblue.com>
Date: Tue, 31 Oct 2017 15:49:55 +0000
Subject: [PATCH] Add a unit test for specialising Java generic types with
 array types

---
 .../generate_java_generic_type.cpp            |  64 +++++++++++++++++-
 ...ic_field_array_instantiation$generic.class | Bin 0 -> 550 bytes
 .../generic_field_array_instantiation.class   | Bin 0 -> 506 bytes
 .../generic_field_array_instantiation.java    |  11 +++
 4 files changed, 74 insertions(+), 1 deletion(-)
 create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class
 create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class
 create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java

diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp
index 7ea813cc4d9..b4c1a7ea07a 100644
--- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp
+++ b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp
@@ -13,7 +13,8 @@
 #include <util/symbol_table.h>
 
 #include <java_bytecode/generate_java_generic_type.h>
-
+#include <testing-utils/require_type.h>
+#include <util/ui_message.h>
 
 SCENARIO(
   "generate_java_generic_type_from_file",
@@ -160,3 +161,64 @@ SCENARIO(
             "java::java.lang.Integer");
   }
 }
+
+SCENARIO(
+  "generate_java_generic_type_with_array_concrete_type",
+  "[core][java_bytecode][generate_java_generic_type]")
+{
+  // We have a 'harness' class who's only purpose is to contain a reference
+  // to the generic class so that we can test the specialization of that generic
+  // class
+  const irep_idt harness_class=
+    "java::generic_field_array_instantiation";
+
+  // We want to test that the specialized/instantiated class has it's field
+  // type updated, so find the specialized class, not the generic class.
+  const irep_idt test_class=
+    "java::generic_field_array_instantiation$generic<java::array[reference]>";
+
+  GIVEN("A generic type instantiated with an array type")
+  {
+    symbol_tablet new_symbol_table=
+      load_java_class(
+        "generic_field_array_instantiation",
+        "./java_bytecode/generate_concrete_generic_type");
+
+    // Ensure the class has been specialized
+    REQUIRE(new_symbol_table.has_symbol(harness_class));
+    const symbolt &harness_symbol=
+      new_symbol_table.lookup_ref(harness_class);
+
+    const struct_typet::componentt &harness_component=
+      require_type::require_component(
+        to_struct_type(harness_symbol.type),
+        "f");
+
+    ui_message_handlert message_handler;
+    generate_java_generic_typet instantiate_generic_type(message_handler);
+    instantiate_generic_type(
+      to_java_generic_type(harness_component.type()), new_symbol_table);
+
+    // Test the specialized class
+    REQUIRE(new_symbol_table.has_symbol(test_class));
+    const symbolt test_class_symbol=
+      new_symbol_table.lookup_ref(test_class);
+
+    REQUIRE(test_class_symbol.type.id()==ID_struct);
+    const struct_typet::componentt &field_component=
+      require_type::require_component(
+        to_struct_type(test_class_symbol.type),
+        "gf");
+    const typet &test_field_type=field_component.type();
+
+    REQUIRE(test_field_type.id()==ID_pointer);
+    REQUIRE(test_field_type.subtype().id()==ID_symbol);
+    const symbol_typet test_field_array=
+      to_symbol_type(test_field_type.subtype());
+    REQUIRE(test_field_array.get_identifier()=="java::array[reference]");
+    const pointer_typet &element_type=
+      require_type::require_pointer(
+        java_array_element_type(test_field_array),
+        symbol_typet("java::java.lang.Float"));
+  }
+}
diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class
new file mode 100644
index 0000000000000000000000000000000000000000..b7056a5e522af6c9b024a55648bbb36504d3e855
GIT binary patch
literal 550
zcma)3%TB^T6g|^cYD<-hZ{7GH1TYa7u9UDLF)<;!pm9qE80wHZB<<A1&vIc*T=)Tg
zl<^KBE@Xj=JNGf?+~?Q#$0vYG9D1-(_TgaD#kPw*1}h#jl)DrD%$o^Uar1sK5kq~=
z;PqszxXx3-U`G)}3i?rIl?#T`ZY-2Y<*+}NA{q60n(~*vRGH>VORnWq8F))7soM<I
z+CT912L`7z9Z|JXS1NIrKMh10@j*h7S}VF*?6JKVV(@#@JROP~X?WG8eV&`i19<QQ
z6tVB(fT6yWRhc6g++QoWRkV{%!m~_d4B_9E(iUrG$m6BiaYScw=wcSh3JRbyGjBBv
zO{Zitk|F}qYh;}e(qR3@*&A5n9oFj%vreyJgYwz)93_P0TiC!ZX`g;=Y+(oZ0UzIt
AQ2+n{

literal 0
HcmV?d00001

diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class
new file mode 100644
index 0000000000000000000000000000000000000000..67141fda96ad3efeb8fc30b66662b11e256317a7
GIT binary patch
literal 506
zcma)3%SyvQ6g@Y6L}RqIzE&;@B38j}+_lt2p&$fZRNS}-lXM!U#0g9$f}iC|aN!5|
zQQ}RgxNs3SXXc#ym^1f&e!YJHxWbW#2KHR+yEt%hNN^LWrBN}#ztMb~rXtT}PM{^>
zB3MVmrIP6)6vl{`Q0d$XZI!Sp(<keU5n*$#5-n_DB;or1mE*@?C7#7F6*?Kt(oERV
zgu6L{4fOuT2<@@b%1#K4v%v$QIn5UQVkb~q-WE@hH1{G(S@GssVPZK`B{{AA$z|!n
z$2N8d{n~6o_t*7Zw34wU3~I}M#)Uo{-UJu{7aQR5Rm@}Dg3rh+D9tc-m>pLfXq~@-
aUaN4IvCVRs>R^{o2R&8*kCi5~7Vr(|Glnk!

literal 0
HcmV?d00001

diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java
new file mode 100644
index 00000000000..c5266feeedb
--- /dev/null
+++ b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java
@@ -0,0 +1,11 @@
+public class generic_field_array_instantiation {
+
+    class generic<T> {
+        T gf;
+    }
+
+    generic<Float []> f;
+    Float [] af;
+}
+
+