From 2e83ec9d31b25bdd34e39003038cc0b67c87ae2a Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Thu, 7 Jun 2018 14:06:46 +0100
Subject: [PATCH] Zero-initialize Class literals before calling initializer
 function

This (a) sets the class-identifier to "java.lang.Class," which wasn't being done before,
and allows the class initializer to assume fields are nulled before entry, as for a normal
constructor.
---
 .../regression/jbmc/class-literals/Test.class | Bin 1263 -> 1646 bytes
 jbmc/regression/jbmc/class-literals/Test.java |  17 ++++++++++++++
 jbmc/src/java_bytecode/java_entry_point.cpp   |  21 ++++++++++++++++--
 3 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/jbmc/regression/jbmc/class-literals/Test.class b/jbmc/regression/jbmc/class-literals/Test.class
index ef7d26bc773c3f56d66c6ea0686d47653139b1ed..c6ca2351f0ddd9e81137e371e1bf82e94187ca4d 100644
GIT binary patch
literal 1646
zcmZ{lOHUI~6vzMfws5EI0PPe?kvF39eu+;Ic`FFGC^0G<hce<|J0&v%k&P>segdK!
z6XVuLQj8`VH!fWG30(RKT)Hrxi$xlGoyC7Tzd1dxdrs!-@An@83}Y#bW^{+ph#rAn
zfj)u$Fv`#^Fd#4}FeGqRU|8Usz<GfS0v81?30xK!2_uM6DOaS7Nx3RzT*`!oUJU~p
z1~utqQnD$5X@+>a>3Npx+d0RZwmow-W34f;yA0){wqyHa41tc$TMWUe+?vHuwO~8e
z(pGlWa+jqsy~vuj!%&g(&Gf@XbF+Z8(R8NZAe_o=xoK<Gmgb>l%k%p-%xzOg8&2wI
zK`TRS=8>7*%vckSlk-iP4TX|M{Tb6)@1M$0mJG=wGI5yojO*rHhG@aToa0;WeKSpw
zA_X+#Y-NuOQag_S!1C=h17Devl9DnfWnRjx6zU9Lp(eyv7LH=xT-~tJ{s=?$iURAH
z!K{vJQm#vxlQJ*m1{SDKvTz-Xpa9Y1P8oFDD=wazPT?cAS5#2B?ftEVa8Vh8{^`2r
z4ue>?{3SC>wO4m^7A2nYUE5iw#1m_lXS>$gzwXhY`CA@ZY37<~23a&I&x3viz~u3e
zw$oE1-5K4>y7s|dOGBI@EkA%9A)G!m4Wz*74fwM+;CqN0fzJr;A@TubclJ^KsX&F2
zYDyYX(y)?7lvG#J3MH*n(kdm5Drrnf4J8fa5m$64kLpsY<xx{gLwO`hX*iGCQW{ZG
zT}dmHv{Ff{lr*ZOF(ow=w8o(BB#pWk$EK&o5R#uL<<z01QD4fbM@gfhh|3Y?2P6FW
zVD2>}Xo!0d#v~%R4IK_Du!~CUp$e}M#TUfz9R_|P&NNiBCM4J}YS}!J>>ldaHtN|E
zG_dDrWbe?#zM+}@KnweYRvtwgrv>4o=;h1k;~DhxT@3K27{VFKqy<fhn*Uw3bU{PM
q;eye3LT(}uGaB<~+JgwbL@@9c{HUnIy_C+&!1Zyty`A*H(e(!_R$}%5

literal 1263
zcmZvb%Tg0T6o&uKg`Ok>BomUL7!*Y%phOh$0&-6j1YCr&R8~XM#KB}j%}gxW`xMz*
zZoO26Dy`C;3tzyEPvHYto*olIk(tFg-Cv*XKIi;BKmUID24Du8VWg1>VF=?K6JcD#
zb&km}g2-@W<@^T6l=L?_Zb?7Qaa;NsjyoK8Iqq@X=a}V~<9NU^FBcaSOen}InBrKJ
zV2NXyAwH_xwy+$dX4<QUt?yPuiGjUf=$SK2!<lFBk7b@R1XgM#!O*{9m}0A5-4)ih
z45o#uZkP<c1xGKw+SCtPSeYwUS_gy+wYpUlc|(SWwuS9X?(4606&Em~Vi@NcV!1bZ
z^`Ih_Ota?bG8>K+6|2ZG49ehaMK{aYrFO14%c@xn(bl##(-GF5UKA?wa!aJeb7sA&
z;-N(C(88hVycCX6RPji1-wxfg_J356(=}<<rO8XPDh;(GzO&KE<H_#6C_1wY13MmA
z#X25SV`QZ&Hr(4!@1;(5&`O0wU{DRaQ@`7Hx;J9j$JLQ2hAnGy@o^;#oOW84en_LT
zaJKZSpwz}PCo(QLmSL7D<77$Lh9yeJtt8!?x{VQfaA|sgEIKG9p^+a<Dn#}o&C=u<
z`QZ2w*hd+NOJsXo=tBsj?NIg$K3V}Qe}b=pxaMyn&_LuXg3pi8^SwoR6G}G?H4*Nn
zktWn`+S^25H|_VNQBNB4q?#v<d(r_<n((Aa51NqONoj-cPW30DQGZg}nQl%UN@-_L
za4Ck*6(f(BD@hWZesBfLB+D~IU_!-P^rC@2d_X^bAd24<`v)3R5NE?kvl$GtE&3Jr
zNXE-_iiT)1apFs*Qgq^#w#b-vg$H8VP!s1G;DPrD_&>wfNvHib<Z(gx)J6G%uDaQd
F{R3bH3sL|8

diff --git a/jbmc/regression/jbmc/class-literals/Test.java b/jbmc/regression/jbmc/class-literals/Test.java
index a9b09288e71..1da577b9e15 100644
--- a/jbmc/regression/jbmc/class-literals/Test.java
+++ b/jbmc/regression/jbmc/class-literals/Test.java
@@ -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";
 
   }
 
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index e6e08371a6e..7d250b92ec7 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -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,