Fix strings not being recognized in the object factory

For a given struct, the object factory previously checked if it was a
string only in the case where skip_classid was set to false and the
update strategy was NO_UPDATE_IN_PLACE or MAY_UPDATE_IN_PLACE.
This missed some cases, for example the case where no model for String
is loaded and the Java method includes a call to a string constructor
that depends on a model. In this case the constructor is stubbed and
skip_classid is set to true in java_simple_method_stubst. Before this
fix, the object factory would go through the components of the string
expression as if it was a regular object expression, and hit an
invariant violation because the data component is stored as a pointer
to an unsignedbv, contradicting the assumption that all pointers point
to structs.

Author: Antonia Lechner

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -794,77 +794,69 @@ void java_object_factoryt::gen_nondet_struct_init(
   // * Not if the object has already been initialised by our caller, in which
   //   case they will set `skip_classid`
   // * Not if we're re-initializing an existing object (i.e. update_in_place)
-
-  bool skip_special_string_fields = false;
-
-  if(!is_sub &&
-     !skip_classid &&
-     update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE)
+  // * Always if it has a string type. Strings should not be partially updated,
+  //   and the `length` and `data` components of string types need to be
+  //   generated differently from object fields in the general case, see
+  //   \ref java_object_factoryt::initialize_nondet_string_fields.
+
+  const bool is_char_sequence =
+    java_string_library_preprocesst::implements_java_char_sequence(struct_type);
+  const bool has_length_and_data =
+    struct_type.has_component("length") && struct_type.has_component("data");
+  const bool skip_special_string_fields =
+    is_char_sequence && has_length_and_data;
+  const bool has_string_input_values =
+    !object_factory_parameters.string_input_values.empty();
+
+  if(skip_special_string_fields && has_string_input_values && !skip_classid)
+  { // We're dealing with a string and we should set fixed input values.
+    // We create a switch statement where each case is an assignment
+    // of one of the fixed input strings to the input variable in question
+    const alternate_casest cases = get_string_input_values_code(
+      expr, object_factory_parameters.string_input_values, symbol_table);
+    assignments.add(generate_nondet_switch(
+      id2string(object_factory_parameters.function_id),
+      cases,
+      java_int_type(),
+      ID_java,
+      location,
+      symbol_table));
+  }
+  else if(
+    (!is_sub && !skip_classid &&
+     update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) ||
+    skip_special_string_fields)
   {
-    class_identifier = struct_tag;
+    // Add an initial all-zero write. Most of the fields of this will be
+    // overwritten, but it helps to have a whole-structure write that analysis
+    // passes can easily recognise leaves no uninitialised state behind.
 
-    const bool is_char_sequence =
-      java_string_library_preprocesst
-        ::implements_java_char_sequence(struct_type);
-    const bool has_length_and_data =
-      struct_type.has_component("length") && struct_type.has_component("data");
-    const bool has_string_input_values =
-      !object_factory_parameters.string_input_values.empty();
-
-    if(is_char_sequence && has_length_and_data && has_string_input_values)
-    { // We're dealing with a string and we should set fixed input values.
-      skip_special_string_fields = true;
-
-      // We create a switch statement where each case is an assignment
-      // of one of the fixed input strings to the input variable in question
-
-      const alternate_casest cases =
-        get_string_input_values_code(
-          expr,
-          object_factory_parameters.string_input_values,
-          symbol_table);
-      assignments.add(generate_nondet_switch(
-        id2string(object_factory_parameters.function_id),
-        cases,
-        java_int_type(),
-        ID_java,
+    // This code mirrors the `remove_java_new` pass:
+    auto initial_object = zero_initializer(expr.type(), source_locationt(), ns);
+    CHECK_RETURN(initial_object.has_value());
+    class_identifier = struct_tag;
+    const irep_idt qualified_clsid = "java::" + id2string(class_identifier);
+    set_class_identifier(
+      to_struct_expr(*initial_object), ns, struct_tag_typet(qualified_clsid));
+
+    // If the initialised type is a special-cased String type (one with length
+    // and data fields introduced by string-library preprocessing), initialise
+    // those fields with nondet values
+    if(skip_special_string_fields)
+    { // We're dealing with a string
+      initialize_nondet_string_fields(
+        to_struct_expr(*initial_object),
+        assignments,
+        object_factory_parameters.min_nondet_string_length,
+        object_factory_parameters.max_nondet_string_length,
         location,
-        symbol_table));
-    }
-    else
-    {
-      // Add an initial all-zero write. Most of the fields of this will be
-      // overwritten, but it helps to have a whole-structure write that analysis
-      // passes can easily recognise leaves no uninitialised state behind.
-
-      // This code mirrors the `remove_java_new` pass:
-      auto initial_object =
-        zero_initializer(expr.type(), source_locationt(), ns);
-      CHECK_RETURN(initial_object.has_value());
-      const irep_idt qualified_clsid = "java::" + id2string(class_identifier);
-      set_class_identifier(
-        to_struct_expr(*initial_object), ns, struct_tag_typet(qualified_clsid));
-
-      // If the initialised type is a special-cased String type (one with length
-      // and data fields introduced by string-library preprocessing), initialise
-      // those fields with nondet values
-      if(is_char_sequence && has_length_and_data)
-      { // We're dealing with a string
-        skip_special_string_fields = true;
-        initialize_nondet_string_fields(
-          to_struct_expr(*initial_object),
-          assignments,
-          object_factory_parameters.min_nondet_string_length,
-          object_factory_parameters.max_nondet_string_length,
-          location,
-          object_factory_parameters.function_id,
-          symbol_table,
-          object_factory_parameters.string_printable,
-          allocate_objects);
-      }
-
-      assignments.add(code_assignt(expr, *initial_object));
+        object_factory_parameters.function_id,
+        symbol_table,
+        object_factory_parameters.string_printable,
+        allocate_objects);
     }
+
+    assignments.add(code_assignt(expr, *initial_object));
   }
 
   for(const auto &component : components)