Merge pull request #1152 from thk123/feature/java-array-checker

Added check for a type being a valid formed Java array

Author: thk123

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -292,6 +292,11 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     comp2.set_base_name("data");
     struct_type.components().push_back(comp2);
 
+    INVARIANT(
+      is_valid_java_array(struct_type),
+      "Constructed a new type representing a Java Array "
+      "object that doesn't match expectations");
+
     symbolt symbol;
     symbol.name=symbol_type.get_identifier();
     symbol.base_name=symbol_type.get(ID_C_base_name);

src/java_bytecode/java_object_factory.cpp

@@ -1059,6 +1059,10 @@ void java_object_factoryt::gen_nondet_array_init(
   // Otherwise we're updating the array in place, and use the
   // existing array allocation and length.
 
+  INVARIANT(
+    is_valid_java_array(struct_type),
+    "Java struct array does not conform to expectations");
+
   dereference_exprt deref_expr(expr, expr.type().subtype());
   const auto &comps=struct_type.components();
   exprt length_expr=member_exprt(deref_expr, "length", comps[1].type());

src/java_bytecode/java_types.cpp

@@ -314,3 +314,47 @@ symbol_typet java_classname(const std::string &id)
 
   return symbol_type;
 }
+
+/// Programmatic documentation of the structure of a Java array (of either
+/// primitives or references) type.
+/// A Java array is represented in GOTO in the following way:
+/// A struct component with a tag like java::array[type] where type is either
+/// a primitive like int, or reference.
+/// The struct has precisely three components:
+/// 1. \@java.lang.Object: of type struct {java.lang.Object} containing the base
+///   class data
+/// 2. length: of type Java integer - the length of the array
+/// 3. data: of type pointer to either pointer to a primitive type, or pointer
+///   to pointer to empty (i.e. a void**) pointing to the contents of the array
+/// \param type: A type that might represent a Java array
+/// \return True if it is a Java array type, false otherwise
+bool is_valid_java_array(const struct_typet &type)
+{
+  bool correct_num_components=type.components().size()==3;
+  if(!correct_num_components)
+    return false;
+
+  // First component, the base class (Object) data
+  const struct_union_typet::componentt base_class_component=
+    type.components()[0];
+
+  bool base_component_valid=true;
+  base_component_valid&=base_class_component.get_name()=="@java.lang.Object";
+
+  bool length_component_valid=true;
+  const struct_union_typet::componentt length_component=
+    type.components()[1];
+  length_component_valid&=length_component.get_name()=="length";
+  length_component_valid&=length_component.type()==java_int_type();
+
+  bool data_component_valid=true;
+  const struct_union_typet::componentt data_component=
+    type.components()[2];
+  data_component_valid&=data_component.get_name()=="data";
+  data_component_valid&=data_component.type().id()==ID_pointer;
+
+  return correct_num_components &&
+    base_component_valid &&
+    length_component_valid &&
+    data_component_valid;
+}

src/java_bytecode/java_types.h

@@ -74,4 +74,6 @@ exprt java_bytecode_promotion(const exprt &);
 
 bool is_java_array_tag(const irep_idt& tag);
 
+bool is_valid_java_array(const struct_typet &type);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H