Add unit test for references to arrays

This is a case for the json conversion which requires particular
attention.

Author: romainbrenguier

jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp

@@ -106,17 +106,16 @@ SCENARIO(
     code_blockt block;
     for(auto code_with_references : code.list)
       block.append(code_with_references->to_code(reference_substitution));
-    THEN("The instruction is the declaration of a symbol of TestClass* type")
+    THEN(
+      "The instruction is the declaration of a symbol of TestClass* type,"
+      "followed by its allocation")
     {
       const symbol_exprt declared_symbol =
         make_query(block)[0].as<code_declt>()[0].as<symbol_exprt>().get();
       REQUIRE(declared_symbol.type() == test_class_type);
-      THEN("The instruction allocates the symbol")
-      {
-        REQUIRE(
-          make_query(block)[1].as<code_assignt>()[0].as<symbol_exprt>().get() ==
-          declared_symbol);
-      }
+      REQUIRE(
+        make_query(block)[1].as<code_assignt>()[0].as<symbol_exprt>().get() ==
+        declared_symbol);
     }
     THEN("The instruction assigns the symbol to `symbol_to_assign`")
     {
@@ -427,4 +426,210 @@ SCENARIO(
                                      .get()) == 42);
     }
   }
+  GIVEN("An object with two fields referencing the same array")
+  {
+    const json_objectt json = [] {
+      json_objectt entry{};
+      entry["array_field_1"] = [] {
+        json_objectt json;
+        json["@ref"] = json_stringt{"id_of_array_2"};
+        return json;
+      }();
+      entry["array_field_2"] = [] {
+        json_objectt int_json;
+        int_json["@items"] = json_arrayt{json_numbert{"42"}};
+        int_json["@type"] = json_stringt{"[I"};
+        int_json["@id"] = json_stringt{"id_of_array_2"};
+        return int_json;
+      }();
+      entry["@type"] = json_stringt{"TestClass"};
+      return entry;
+    }();
+    class_to_declared_symbols.emplace("java::TestClass", [] {
+      symbolt field_symbol;
+      field_symbol.base_name = "array_field_1";
+      field_symbol.name = "field_name_1_for_codet";
+      field_symbol.type = java_int_type();
+      field_symbol.is_static_lifetime = true;
+      return field_symbol;
+    }());
+    class_to_declared_symbols.emplace("java::TestClass", [] {
+      symbolt field_symbol;
+      field_symbol.base_name = "array_field_2";
+      field_symbol.name = "field_name_2_for_codet";
+      field_symbol.type = java_int_type();
+      field_symbol.is_static_lifetime = true;
+      return field_symbol;
+    }());
+    const irep_idt clinit_name = add_clinit(symbol_table, "TestClass");
+    add_class_with_components(
+      symbol_table,
+      "TestClass",
+      {std::pair<std::string, typet>("@class_identifier", string_typet{}),
+       std::pair<std::string, typet>("array_field_1", java_array_type('i')),
+       std::pair<std::string, typet>("array_field_2", java_array_type('i'))});
+    // For array[int]
+    add_java_array_types(symbol_table);
+
+    const reference_typet test_class_type =
+      reference_type(struct_tag_typet{"java::TestClass"});
+    optionalt<ci_lazy_methods_neededt> option{};
+    const code_with_references_listt code = assign_from_json(
+      symbol_exprt{"symbol_to_assign", test_class_type},
+      json,
+      clinit_name,
+      symbol_table,
+      option,
+      max_user_array_length,
+      references);
+
+    code_with_referencest::reference_substitutiont reference_substitution =
+      [&](const std::string &reference_id) -> object_creation_referencet & {
+      REQUIRE(reference_id == "id_of_array_2");
+      auto it = references.find(reference_id);
+      REQUIRE(it != references.end());
+      return it->second;
+    };
+    code_blockt block;
+    for(auto code_with_references : code.list)
+      block.append(code_with_references->to_code(reference_substitution));
+
+    THEN(
+      "The instruction declares a symbol of TestClass* type: "
+      "TestClass* malloc_site;")
+    {
+      const symbol_exprt allocation_symbol =
+        make_query(block)[0].as<code_declt>()[0].as<symbol_exprt>().get();
+      REQUIRE(allocation_symbol.type() == test_class_type);
+    }
+    THEN(
+      "declares the array data: "
+      "int[] user_specified_array_ref;")
+    {
+      REQUIRE(
+        make_query(block)[1]
+          .as<code_declt>()[0]
+          .as<symbol_exprt>()
+          .get()
+          .type() == java_array_type('i'));
+    }
+    THEN(
+      "declares the length: "
+      "int user_specified_array_length;")
+    {
+      REQUIRE(
+        make_query(block)[2]
+          .as<code_declt>()[0]
+          .as<symbol_exprt>()
+          .get()
+          .type() == java_int_type());
+    }
+    THEN(
+      "declares the data:"
+      "int* user_specified_array_data_init;")
+    {
+      REQUIRE(
+        make_query(block)[3]
+          .as<code_declt>()[0]
+          .as<symbol_exprt>()
+          .get()
+          .type() == java_reference_type(java_int_type()));
+    }
+    THEN(
+      "allocates the object:"
+      "malloc_site = new TestClass();")
+    {
+      REQUIRE(
+        make_query(block)[4]
+          .as<code_assignt>()[0]
+          .as<symbol_exprt>()
+          .get()
+          .type() == test_class_type);
+      REQUIRE(
+        make_query(block)[4]
+          .as<code_assignt>()[1]
+          .as<side_effect_exprt>()
+          .get()
+          .get_statement() == ID_allocate);
+    }
+
+    THEN(
+      "assigns the allocated object:"
+      "symbol_to_assign = malloc_site;")
+    {
+      REQUIRE(
+        make_query(block)[5]
+          .as<code_assignt>()[0]
+          .as<symbol_exprt>()
+          .get()
+          .get_identifier() == "symbol_to_assign");
+    }
+    THEN(
+      "zero-initialize the object:"
+      "*malloc_site = {\"java::\", NULL, NULL};")
+    {
+      REQUIRE(
+        make_query(block)[6]
+          .as<code_assignt>()[0]
+          .as<dereference_exprt>()[0]
+          .get()
+          .type() == test_class_type);
+    }
+    THEN(
+      "allocate the array :"
+      "user_specified_array_ref = new int[1];")
+    {
+      REQUIRE(
+        make_query(block)[7].as<code_assignt>()[0].get().type() ==
+        java_array_type('i'));
+      const auto side_effect_expr = make_query(block)[7]
+                                      .as<code_assignt>()[1]
+                                      .as<side_effect_exprt>()
+                                      .get();
+      REQUIRE(side_effect_expr.get_statement() == ID_java_new_array);
+      REQUIRE(
+        numeric_cast_v<mp_integer>(
+          make_query(side_effect_expr)[0].as<constant_exprt>().get()) == 1);
+    }
+    THEN(
+      "assign array_field_1 :"
+      "malloc_site->array_field_1 = user_specified_array_ref;")
+    {
+      REQUIRE(
+        make_query(block)[8]
+          .as<code_assignt>()[0]
+          .as<member_exprt>()
+          .get()
+          .get_component_name() == "array_field_1");
+    }
+    THEN(
+      "assign pointer to the data for initializing it:"
+      "user_specified_array_data_init = user_specified_array_ref->data;")
+    {
+      REQUIRE(
+        make_query(block)[9].as<code_assignt>()[0].get().type() ==
+        java_reference_type(java_int_type()));
+    }
+    THEN(
+      "assign the array cell value :"
+      "user_specified_array_data_init[0] = 42;")
+    {
+      REQUIRE(
+        numeric_cast_v<mp_integer>(make_query(block)[10]
+                                     .as<code_assignt>()[1]
+                                     .as<constant_exprt>()
+                                     .get()) == 42);
+    }
+    THEN(
+      "assign array_field_2 :"
+      "malloc_site->array_field_2 = user_specified_array_ref;")
+    {
+      REQUIRE(
+        make_query(block)[11]
+          .as<code_assignt>()[0]
+          .as<member_exprt>()
+          .get()
+          .get_component_name() == "array_field_2");
+    }
+  }
 }