Merge pull request #4870 from romainbrenguier/bugfix/aload

Fix type of data_ptr in convert_aload/astore and useless typecasts

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1328,7 +1328,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     }
     else if(bytecode == patternt("?astore"))
     {
-      assert(op.size()==3 && results.empty());
+      PRECONDITION(results.empty());
       c = convert_astore(statement, op, i_it->source_location);
     }
     else if(bytecode == patternt("?store") || bytecode == patternt("?store_?"))
@@ -1340,7 +1340,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     }
     else if(bytecode == patternt("?aload"))
     {
-      PRECONDITION(op.size() == 2 && results.size() == 1);
+      PRECONDITION(results.size() == 1);
       results[0] = convert_aload(statement, op);
     }
     else if(bytecode == patternt("?load") || bytecode == patternt("?load_?"))
@@ -2851,16 +2851,37 @@ code_blockt java_bytecode_convert_methodt::convert_ret(
   return c;
 }
 
+/// Add typecast if necessary to \p expr to make it compatible with array type
+/// corresponding to \p type_char (see \ref java_array_type(const char)).
+/// Character 'b' is used both for `byte` and `boolean` arrays, so if \p expr
+/// is a boolean array and we are using a `b` operation we can skip the
+/// typecast.
+static exprt conditional_array_cast(const exprt &expr, char type_char)
+{
+  const auto ref_type =
+    type_try_dynamic_cast<java_reference_typet>(expr.type());
+  const bool typecast_not_needed =
+    ref_type && ((type_char == 'b' && ref_type->subtype().get_identifier() ==
+                                        "java::array[boolean]") ||
+                 *ref_type == java_array_type(type_char));
+  return typecast_not_needed ? expr
+                             : typecast_exprt(expr, java_array_type(type_char));
+}
+
 exprt java_bytecode_convert_methodt::convert_aload(
   const irep_idt &statement,
-  const exprt::operandst &op) const
+  const exprt::operandst &op)
 {
+  PRECONDITION(op.size() == 2);
   const char type_char = statement[0];
-  dereference_exprt deref{typecast_exprt{op[0], java_array_type(type_char)}};
+  const exprt op_with_right_type = conditional_array_cast(op[0], type_char);
+  dereference_exprt deref{op_with_right_type};
   deref.set(ID_java_member_access, true);
 
-  member_exprt data_ptr(
-    deref, "data", pointer_type(java_type_from_char(type_char)));
+  auto java_array_type = type_try_dynamic_cast<struct_tag_typet>(deref.type());
+  INVARIANT(java_array_type, "Java array type should be a struct_tag_typet");
+  member_exprt data_ptr{
+    deref, "data", pointer_type(java_array_element_type(*java_array_type))};
   plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
   // tag it so it's easy to identify during instrumentation
   data_plus_offset.set(ID_java_array_access, true);
@@ -2899,12 +2920,16 @@ code_blockt java_bytecode_convert_methodt::convert_astore(
   const exprt::operandst &op,
   const source_locationt &location)
 {
+  PRECONDITION(op.size() == 3);
   const char type_char = statement[0];
-  dereference_exprt deref{typecast_exprt{op[0], java_array_type(type_char)}};
+  const exprt op_with_right_type = conditional_array_cast(op[0], type_char);
+  dereference_exprt deref{op_with_right_type};
   deref.set(ID_java_member_access, true);
 
-  member_exprt data_ptr(
-    deref, "data", pointer_type(java_type_from_char(type_char)));
+  auto java_array_type = type_try_dynamic_cast<struct_tag_typet>(deref.type());
+  INVARIANT(java_array_type, "Java array type should be a struct_tag_typet");
+  member_exprt data_ptr{
+    deref, "data", pointer_type(java_array_element_type(*java_array_type))};
   plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
   // tag it so it's easy to identify during instrumentation
   data_plus_offset.set(ID_java_array_access, true);

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -366,8 +366,8 @@ class java_bytecode_convert_methodt:public messaget
     const method_offsett address,
     const source_locationt &location);
 
-  exprt
-  convert_aload(const irep_idt &statement, const exprt::operandst &op) const;
+  static exprt
+  convert_aload(const irep_idt &statement, const exprt::operandst &op);
 
   code_blockt convert_ret(
     const std::vector<method_offsett> &jsr_ret_targets,
@@ -504,5 +504,7 @@ class java_bytecode_convert_methodt:public messaget
     const source_locationt &location);
 
   codet convert_pop(const irep_idt &statement, const exprt::operandst &op);
+
+  friend class java_bytecode_convert_method_unit_testt;
 };
 #endif

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp

@@ -6,6 +6,7 @@ Author: Diffblue Limited.
 
 \*******************************************************************/
 
+#include <testing-utils/expr_query.h>
 #include <testing-utils/use_catch.h>
 
 #include <util/irep.h>
@@ -14,7 +15,9 @@ Author: Diffblue Limited.
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
 
+#include <java_bytecode/java_bytecode_convert_method_class.h>
 #include <java_bytecode/java_utils.h>
+#include <testing-utils/message.h>
 
 SCENARIO(
   "java_bytecode_convert_bridge_method",
@@ -286,3 +289,232 @@ SCENARIO(
     }
   }
 }
+
+/// Allow access to private methods so that they can be unit tested
+class java_bytecode_convert_method_unit_testt
+{
+public:
+  static exprt
+  convert_aload(const irep_idt &statement, const exprt::operandst &op)
+  {
+    return java_bytecode_convert_methodt::convert_aload(statement, op);
+  }
+
+  static code_blockt convert_astore(
+    java_bytecode_convert_methodt &converter,
+    const irep_idt &statement,
+    const exprt::operandst &op,
+    const source_locationt &location)
+  {
+    return converter.convert_astore(statement, op, location);
+  }
+};
+
+SCENARIO(
+  "baload byte array",
+  "[core][java_bytecode][java_bytecode_convert_method][convert_aload]")
+{
+  GIVEN("A byte array")
+  {
+    const typet byte_array_type = java_array_type('b');
+    const symbol_exprt byte_array{"byte_array", byte_array_type};
+    const exprt offset = from_integer(1, java_int_type());
+    WHEN("baload is called on the byte array")
+    {
+      const exprt result =
+        java_bytecode_convert_method_unit_testt::convert_aload(
+          "baload", {byte_array, offset});
+      THEN("The Result is of the form `(int)(*(byte_array->data + offset))`")
+      // See \ref java_bytecode_promotion on why we need a typecast to int.
+      {
+        const auto query = make_query(result)
+                             .as<typecast_exprt>()[0]
+                             .as<dereference_exprt>()[0]
+                             .as<plus_exprt>();
+        REQUIRE(query[1].get() == offset);
+        auto member = query[0].as<member_exprt>();
+        REQUIRE(member.get().get_component_name() == "data");
+        REQUIRE(member[0].as<dereference_exprt>()[0].get() == byte_array);
+        REQUIRE(result.type() == java_int_type());
+        // byte_array->data has type *byte
+        REQUIRE(member.get().type() == pointer_type(java_byte_type()));
+      }
+    }
+  }
+}
+
+SCENARIO(
+  "baload boolean array",
+  "[core][java_bytecode][java_bytecode_convert_method][convert_aload]")
+{
+  GIVEN("A boolean array")
+  {
+    const typet boolean_array_type = java_array_type('z');
+    const symbol_exprt boolean_array{"boolean_array", boolean_array_type};
+    const exprt offset = from_integer(2, java_int_type());
+    WHEN("baload is called on the byte array")
+    {
+      const exprt result =
+        java_bytecode_convert_method_unit_testt::convert_aload(
+          "baload", {boolean_array, offset});
+      THEN("The result is of the form `(int)(*(boolean_array->data + offset))`")
+      // See \ref java_bytecode_promotion on why we need a typecast to int.
+      {
+        const auto query = make_query(result)
+                             .as<typecast_exprt>()[0]
+                             .as<dereference_exprt>()[0]
+                             .as<plus_exprt>();
+        REQUIRE(query[1].get() == offset);
+        REQUIRE(
+          query[0].as<member_exprt>()[0].as<dereference_exprt>()[0].get() ==
+          boolean_array);
+        // boolean_array->data has type *boolean
+        REQUIRE(
+          query[0].as<member_exprt>().get().type() ==
+          pointer_type(java_boolean_type()));
+      }
+    }
+  }
+}
+
+SCENARIO(
+  "iaload int array",
+  "[core][java_bytecode][java_bytecode_convert_method][convert_aload]")
+{
+  GIVEN("An int array")
+  {
+    const typet int_array_type = java_array_type('i');
+    const symbol_exprt int_array{"int_array", int_array_type};
+    const exprt offset = from_integer(2, java_int_type());
+    WHEN("iaload is called on the int array")
+    {
+      const exprt result =
+        java_bytecode_convert_method_unit_testt::convert_aload(
+          "iaload", {int_array, offset});
+      THEN("The result is of the form `*(int_array->data + offset)`")
+      {
+        const auto query =
+          make_query(result).as<dereference_exprt>()[0].as<plus_exprt>();
+        REQUIRE(query[1].get() == offset);
+        REQUIRE(
+          query[0].as<member_exprt>()[0].as<dereference_exprt>()[0].get() ==
+          int_array);
+        // int_array->data has type *int
+        REQUIRE(
+          query[0].as<member_exprt>().get().type() ==
+          pointer_type(java_int_type()));
+      }
+    }
+  }
+}
+
+SCENARIO(
+  "astore",
+  "[core][java_bytecode][java_bytecode_convert_method][convert_astore]")
+{
+  symbol_tablet symbol_table;
+  java_string_library_preprocesst string_preprocess;
+  const class_hierarchyt class_hierarchy;
+  java_bytecode_convert_methodt converter{symbol_table,
+                                          null_message_handler,
+                                          10,
+                                          true,
+                                          {},
+                                          string_preprocess,
+                                          class_hierarchy,
+                                          false};
+
+  GIVEN("An int array")
+  {
+    const source_locationt location;
+    const typet int_array_type = java_array_type('i');
+    const symbol_exprt int_array{"int_array", int_array_type};
+    const exprt offset = from_integer(3, java_int_type());
+    const exprt value = from_integer(4, java_int_type());
+    WHEN("iastore is called on the int array")
+    {
+      const code_blockt result =
+        java_bytecode_convert_method_unit_testt::convert_astore(
+          converter, "iastore", {int_array, offset, value}, location);
+      THEN(
+        "The result contains 1 statement of the form `*(int_array->data + 3) = "
+        "4`")
+      {
+        REQUIRE(result.statements().size() == 1);
+        auto query = make_query(result.statements()[0]).as<code_assignt>();
+        REQUIRE(query[1].get() == value);
+        auto plus = query[0].as<dereference_exprt>()[0].as<plus_exprt>();
+        REQUIRE(plus[1].get() == offset);
+        REQUIRE(
+          plus[0].as<member_exprt>().get().get_component_name() == "data");
+        REQUIRE(
+          plus[0].as<member_exprt>()[0].as<dereference_exprt>()[0].get() ==
+          int_array);
+        THEN("int_array->data has type *int")
+        {
+          REQUIRE(
+            plus[0].as<member_exprt>().get().type() ==
+            pointer_type(java_int_type()));
+        }
+      }
+    }
+  }
+
+  GIVEN("A boolean array")
+  {
+    const source_locationt location;
+    const typet boolean_array_type = java_array_type('z');
+    const symbol_exprt boolean_array{"boolean_array", boolean_array_type};
+    const exprt offset = from_integer(3, java_int_type());
+    const exprt value = from_integer(true, java_boolean_type());
+    WHEN("bastore is called on the boolean array")
+    {
+      const code_blockt result =
+        java_bytecode_convert_method_unit_testt::convert_astore(
+          converter, "bastore", {boolean_array, offset, value}, location);
+      THEN(
+        "The result contains 1 statement of the form "
+        "`*(boolean_array->data + 3) = true`")
+      {
+        REQUIRE(result.statements().size() == 1);
+        auto query = make_query(result.statements()[0]).as<code_assignt>();
+        REQUIRE(query[1].get() == value);
+        auto plus = query[0].as<dereference_exprt>()[0].as<plus_exprt>();
+        REQUIRE(plus[1].get() == offset);
+        REQUIRE(
+          plus[0].as<member_exprt>().get().get_component_name() == "data");
+        REQUIRE(
+          plus[0].as<member_exprt>()[0].as<dereference_exprt>()[0].get() ==
+          boolean_array);
+        THEN("boolean_array->data has type *boolean")
+        {
+          REQUIRE(
+            plus[0].as<member_exprt>().get().type() ==
+            pointer_type(java_boolean_type()));
+        }
+      }
+    }
+    WHEN("iastore is called on the boolean array")
+    {
+      const code_blockt result =
+        java_bytecode_convert_method_unit_testt::convert_astore(
+          converter, "iastore", {boolean_array, offset, value}, location);
+      THEN(
+        "The result contains 1 statement of the form "
+        "`*(((int[])boolean_array)->data + offset)`")
+      {
+        REQUIRE(result.statements().size() == 1);
+        REQUIRE(
+          make_query(result.statements()[0])
+            .as<code_assignt>()[0]
+            .as<dereference_exprt>()[0]
+            .as<plus_exprt>()[0]
+            .as<member_exprt>()[0]
+            .as<dereference_exprt>()[0]
+            .as<typecast_exprt>()
+            .get()
+            .type() == java_array_type('i'));
+      }
+    }
+  }
+}