Merge pull request #5060 from smowton/smowton/feature/model-create-array-with-type

 Model CProver.createArrayWithType function

Author: smowton

jbmc/regression/jbmc/create-array-with-type-1/Test.class

@@ -0,0 +1,16 @@
+import org.cprover.CProver;
+
+public class Test {
+
+  public static void test() {
+
+    String[] strings = new String[5];
+
+    Object[] clone = CProver.createArrayWithType(1, strings);
+    assert clone instanceof String[];
+    assert clone.length == 1;
+    assert clone[0] == null;
+    assert clone instanceof Object[];
+    assert clone instanceof Integer[]; // Should fail
+  }
+}

jbmc/regression/jbmc/create-array-with-type-1/Test.java

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.test:\(\)V\.assertion\.1\] line 10 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.2\] line 11 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.3\] line 12 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.4\] line 13 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.5\] line 14 assertion.*: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/create-array-with-type-1/test.desc

@@ -0,0 +1,16 @@
+import org.cprover.CProver;
+
+public class Test {
+
+  public static void test() {
+
+    String[] strings = new String[0];
+
+    Object[] clone = CProver.createArrayWithType(1, strings);
+    assert clone instanceof String[];
+    assert clone.length == 1;
+    assert clone[0] == null;
+    assert clone instanceof Object[];
+    assert clone instanceof Integer[]; // Should fail
+  }
+}

jbmc/regression/jbmc/create-array-with-type-2/Test.class

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.test:\(\)V\.assertion\.1\] line 10 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.2\] line 11 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.3\] line 12 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.4\] line 13 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.5\] line 14 assertion.*: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/create-array-with-type-2/Test.java

@@ -0,0 +1,16 @@
+import org.cprover.CProver;
+
+public class Test {
+
+  public static void test() {
+
+    String[][] stringArrays = new String[1][1];
+
+    Object[] clone = CProver.createArrayWithType(1, stringArrays);
+    assert clone instanceof String[][];
+    assert clone.length == 1;
+    assert clone[0] == null;
+    assert clone instanceof Object[];
+    assert clone instanceof String[]; // Should fail
+  }
+}

jbmc/regression/jbmc/create-array-with-type-2/test.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.test:\(\)V\.assertion\.1\] line 10 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.2\] line 11 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.3\] line 12 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.4\] line 13 assertion.*: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.5\] line 14 assertion.*: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/create-array-with-type-3/Test.class

@@ -4,6 +4,7 @@ SRC = assignments_from_json.cpp \
       ci_lazy_methods.cpp \
       ci_lazy_methods_needed.cpp \
       convert_java_nondet.cpp \
+      create_array_with_type_intrinsic.cpp \
       expr2java.cpp \
       generic_parameter_specialization_map.cpp \
       generic_parameter_specialization_map_keys.cpp \

jbmc/regression/jbmc/create-array-with-type-3/Test.java

@@ -0,0 +1,108 @@
+/*******************************************************************\
+
+Module: Implementation of CProver.createArrayWithType intrinsic
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+/// Implementation of CProver.createArrayWithType intrinsic
+
+#include "create_array_with_type_intrinsic.h"
+
+#include <goto-programs/class_identifier.h>
+#include <java_bytecode/java_types.h>
+#include <util/fresh_symbol.h>
+#include <util/namespace.h>
+#include <util/symbol_table_base.h>
+
+/// Returns the symbol name for `org.cprover.CProver.createArrayWithType`
+irep_idt get_create_array_with_type_name()
+{
+  static irep_idt create_array_with_type_name =
+    "java::org.cprover.CProver.createArrayWithType:"
+    "(I[Ljava/lang/Object;)[Ljava/lang/Object;";
+  return create_array_with_type_name;
+}
+
+/// Returns the internal implementation for
+/// `org.cprover.CProver.createArrayWithType`. Our implementation copies the
+/// internal type information maintained by jbmc that tracks the runtime type
+/// of an array object rather than using reflection to achieve similar type
+/// cloning.
+/// \param function_id: identifier of the function being produced. Currently
+///   always `get_create_array_with_type_name()`
+/// \param symbol_table: global symbol table
+/// \param message_handler: any GOTO program conversion errors are logged here
+/// \return new GOTO program body for `org.cprover.CProver.createArrayWithType`.
+codet create_array_with_type_body(
+  const irep_idt &function_id,
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler)
+{
+  // Replace CProver.createArrayWithType, which uses reflection to copy the
+  // type but not the content of a given array, with a java_new_array statement
+  // followed by overwriting its element type and dimension, similar to our
+  // implementation (in java_bytecode_convert_class.cpp) of the
+  // array[reference].clone() method.
+
+  PRECONDITION(function_id == get_create_array_with_type_name());
+
+  namespacet ns{symbol_table};
+
+  const symbolt &function_symbol =
+    symbol_table.lookup_ref(get_create_array_with_type_name());
+  const auto &function_type = to_code_type(function_symbol.type);
+  const auto &length_argument = function_type.parameters().at(0);
+  symbol_exprt length_argument_symbol_expr{length_argument.get_identifier(),
+                                           length_argument.type()};
+  const auto &existing_array_argument = function_type.parameters().at(1);
+  symbol_exprt existing_array_argument_symbol_expr{
+    existing_array_argument.get_identifier(), existing_array_argument.type()};
+
+  symbolt &new_array_symbol = get_fresh_aux_symbol(
+    function_type.parameters().at(1).type(),
+    id2string(get_create_array_with_type_name()),
+    "new_array",
+    source_locationt(),
+    ID_java,
+    symbol_table);
+  const auto new_array_symbol_expr = new_array_symbol.symbol_expr();
+
+  code_blockt code_block;
+
+  // Declare new_array temporary:
+  code_block.add(code_declt(new_array_symbol_expr));
+
+  // new_array = new Object[length];
+  side_effect_exprt new_array_expr{
+    ID_java_new_array, new_array_symbol.type, source_locationt{}};
+  new_array_expr.copy_to_operands(length_argument_symbol_expr);
+  code_block.add(code_assignt(new_array_symbol_expr, new_array_expr));
+
+  dereference_exprt existing_array(existing_array_argument_symbol_expr);
+  dereference_exprt new_array(new_array_symbol_expr);
+
+  // new_array.@array_dimensions = existing_array.@array_dimensions
+  // new_array.@element_class_identifier =
+  //   existing_array.@element_class_identifier
+  member_exprt old_array_dimension(
+    existing_array, JAVA_ARRAY_DIMENSION_FIELD_NAME, java_int_type());
+  member_exprt old_array_element_classid(
+    existing_array, JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME, string_typet());
+
+  member_exprt new_array_dimension(
+    new_array, JAVA_ARRAY_DIMENSION_FIELD_NAME, java_int_type());
+  member_exprt new_array_element_classid(
+    new_array, JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME, string_typet());
+
+  code_block.add(code_assignt(new_array_dimension, old_array_dimension));
+  code_block.add(
+    code_assignt(new_array_element_classid, old_array_element_classid));
+
+  // return new_array
+  code_block.add(code_returnt(new_array_symbol_expr));
+
+  return std::move(code_block);
+}

jbmc/regression/jbmc/create-array-with-type-3/test.desc

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: Implementation of CProver.createArrayWithType intrinsic
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+/// Implementation of CProver.createArrayWithType intrinsic
+
+#ifndef CPROVER_JAVA_BYTECODE_CREATE_ARRAY_WITH_TYPE_INTRINSIC_H
+#define CPROVER_JAVA_BYTECODE_CREATE_ARRAY_WITH_TYPE_INTRINSIC_H
+
+#include <util/message.h>
+#include <util/std_code.h>
+#include <util/symbol_table_base.h>
+
+irep_idt get_create_array_with_type_name();
+
+codet create_array_with_type_body(
+  const irep_idt &function_id,
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler);
+
+#endif

jbmc/src/java_bytecode/Makefile

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/class_hierarchy.h>
 
 #include "ci_lazy_methods.h"
+#include "create_array_with_type_intrinsic.h"
 #include "java_bytecode_concurrency_instrumentation.h"
 #include "java_bytecode_convert_class.h"
 #include "java_bytecode_convert_method.h"
@@ -740,6 +741,14 @@ bool java_bytecode_languaget::typecheck(
     }
   }
 
+  // Register synthetic method that replaces a real definition if one is
+  // available:
+  if(symbol_table.has_symbol(get_create_array_with_type_name()))
+  {
+    synthetic_methods[get_create_array_with_type_name()] =
+      synthetic_method_typet::CREATE_ARRAY_WITH_TYPE;
+  }
+
   // Now add synthetic classes for every invokedynamic instruction found (it
   // makes this easier that all interface types and their methods have been
   // created above):
@@ -1209,6 +1218,18 @@ bool java_bytecode_languaget::convert_single_method(
       writable_symbol.value = invokedynamic_synthetic_method(
         function_id, symbol_table, get_message_handler());
       break;
+    case synthetic_method_typet::CREATE_ARRAY_WITH_TYPE:
+    {
+      INVARIANT(
+        cmb,
+        "CProver.createArrayWithType should only be registered if "
+        "we have a real implementation available");
+      java_bytecode_initialize_parameter_names(
+        writable_symbol, cmb->get().method.local_variable_table, symbol_table);
+      writable_symbol.value = create_array_with_type_body(
+        function_id, symbol_table, get_message_handler());
+      break;
+    }
     }
     // Notify lazy methods of static calls made from the newly generated
     // function:

jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp

@@ -42,7 +42,10 @@ enum class synthetic_method_typet
   INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR,
   /// A generated method for a class capturing the parameters of an
   /// invokedynamic instruction
-  INVOKEDYNAMIC_METHOD
+  INVOKEDYNAMIC_METHOD,
+  /// Our internal implementation of CProver.createArrayWithType, which needs to
+  /// access internal type-id fields
+  CREATE_ARRAY_WITH_TYPE
 };
 
 /// Maps method names on to a synthetic method kind.