Merge pull request #2303 from smowton/smowton/fix/initialize-before-class-literal-init

Zero-initialize Class literals before calling initializer function

Author: smowton

jbmc/regression/jbmc/class-literals/Test.class

@@ -3,6 +3,22 @@ public class Test {
 
   public static void main() {
 
+    // First check that all `.class` literals are indeed java.lang.Class
+    // instances:
+    assert ExampleAnnotation.class instanceof Class;
+    assert ExampleInterface.class instanceof Class;
+    assert ExampleEnum.class instanceof Class;
+    assert ExampleSynthetic.class instanceof Class;
+    assert char[].class instanceof Class;
+    assert short[].class instanceof Class;
+    assert int[].class instanceof Class;
+    assert long[].class instanceof Class;
+    assert float[].class instanceof Class;
+    assert double[].class instanceof Class;
+    assert boolean[].class instanceof Class;
+    assert Object[].class instanceof Class;
+    assert Object[][].class instanceof Class;
+
     assert ExampleAnnotation.class.isAnnotation();
     assert ExampleInterface.class.isInterface();
     assert ExampleEnum.class.isEnum();
@@ -29,6 +45,7 @@ public static void main() {
     assert ExampleAnnotation.class.getName() == "ExampleAnnotation";
     assert ExampleInterface.class.getName() == "ExampleInterface";
     assert ExampleEnum.class.getName() == "ExampleEnum";
+    assert ExampleSynthetic.class.getName() == "ExampleSynthetic";
 
   }
 

jbmc/regression/jbmc/class-literals/Test.java

@@ -9,9 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_entry_point.h"
 
 #include <util/config.h>
+#include <util/expr_initializer.h>
 #include <util/string_constant.h>
 #include <util/suffix.h>
 
+#include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_functions.h>
 
 #include <linking/static_lifetime_init.h>
@@ -117,7 +119,8 @@ static void java_static_lifetime_init(
   bool assume_init_pointers_not_null,
   const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
-  bool string_refinement_enabled)
+  bool string_refinement_enabled,
+  message_handlert &message_handler)
 {
   symbolt &initialize_symbol=*symbol_table.get_writeable(INITIALIZE_FUNCTION);
   code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
@@ -188,6 +191,19 @@ static void java_static_lifetime_init(
         args.push_back(
           constant_bool(class_symbol.type.get_bool(ID_enumeration)));
 
+        // First initialize the object as prior to a constructor:
+        namespacet ns(symbol_table);
+
+        exprt zero_object =
+          zero_initializer(
+            sym.type, source_locationt(), ns, message_handler);
+        set_class_identifier(
+          to_struct_expr(zero_object), ns, to_symbol_type(sym.type));
+
+        code_block.copy_to_operands(
+          code_assignt(sym.symbol_expr(), zero_object));
+
+        // Then call the init function:
         code_block.move_to_operands(initializer_call);
       }
       else if(sym.value.is_nil() && sym.type!=empty_typet())
@@ -530,7 +546,8 @@ bool java_entry_point(
     assume_init_pointers_not_null,
     object_factory_parameters,
     pointer_type_selector,
-    string_refinement_enabled);
+    string_refinement_enabled,
+    message_handler);
 
   return generate_java_start_function(
     symbol,