Zero-initialize object factory structs

Previously these were incrementally populated (assigning each field in turn); the zero init
was skipped because it is technically redundant. However, this prevents symex (and perhaps other
analyses) from propagating useful information, as the first write appears to be a partial update
on top of uninitialised data, and each subsequent write is based on its predecessor. Hence objects
produced by the factory end up represented as a stack of WITH operations, ultimately based on an
undefined symbol (e.g. dynamic_object1#0).

With this change symex becomes able to constant propagate the initial object, reducing equation
complexity, and objects that don't have any fields to nondet initialise can potentially be constant-
propagated throughout their lifetime.

Author: smowton

src/java_bytecode/java_object_factory.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
+#include <util/message.h>
 #include <util/namespace.h>
 #include <util/nondet_bool.h>
 #include <util/nondet_ifthenelse.h>
@@ -25,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <linking/zero_initializer.h>
 
+#include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_functions.h>
 
 #include <java_bytecode/select_pointer_type.h>
@@ -1046,8 +1048,26 @@ void java_object_factoryt::gen_nondet_struct_init(
   const componentst &components=struct_type.components();
 
   if(!is_sub)
+  {
     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.
+
+    // This code mirrors `goto_convertt::do_java_new`:
+    null_message_handlert nullout;
+     exprt zero_object=
+       zero_initializer(
+         struct_type, source_locationt(), ns, nullout);
+     irep_idt qualified_clsid = "java::" + id2string(class_identifier);
+     set_class_identifier(
+       to_struct_expr(zero_object), ns, symbol_typet(qualified_clsid));
+
+     assignments.copy_to_operands(
+       code_assignt(expr, zero_object));
+  }
+
   for(const auto &component : components)
   {
     const typet &component_type=component.type();
@@ -1057,25 +1077,11 @@ void java_object_factoryt::gen_nondet_struct_init(
 
     if(name=="@class_identifier")
     {
-      if(update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE)
-        continue;
-
-      if(skip_classid)
-        continue;
-
-      irep_idt qualified_clsid = "java::" + id2string(class_identifier);
-      constant_exprt ci(qualified_clsid, string_typet());
-      code_assignt code(me, ci);
-      code.add_source_location()=loc;
-      assignments.copy_to_operands(code);
+      continue;
     }
     else if(name=="@lock")
     {
-      if(update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE)
-        continue;
-      code_assignt code(me, from_integer(0, me.type()));
-      code.add_source_location()=loc;
-      assignments.copy_to_operands(code);
+      continue;
     }
     else
     {