From 8a59f6f6716e35b25ad78a5a1a133f2c1d09171e Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 18 May 2018 17:06:10 +0100
Subject: [PATCH] Object factory: permit null pointers within java.lang.Class

This is in fact required by the Deeptest models library, and is generally sensible if we don't
know whether or not a particular implementation of java.lang.Class should or should not be able
to store null in any particular field. If you're running an implementation that requires them
not null, add a cproverNondetInitialize function to that effect.

This was blocking using implementations that expect a null value from passing initialization.
---
 jbmc/regression/jbmc/class-fields/Test.class      | Bin 0 -> 598 bytes
 jbmc/regression/jbmc/class-fields/Test.java       |  10 ++++++++++
 .../jbmc/class-fields/java/lang/Class.class       | Bin 0 -> 488 bytes
 .../jbmc/class-fields/java/lang/Class.java        |  11 +++++++++++
 jbmc/regression/jbmc/class-fields/test.desc       |   9 +++++++++
 jbmc/src/java_bytecode/java_entry_point.cpp       |   5 -----
 jbmc/src/java_bytecode/java_object_factory.cpp    |   6 +-----
 7 files changed, 31 insertions(+), 10 deletions(-)
 create mode 100644 jbmc/regression/jbmc/class-fields/Test.class
 create mode 100644 jbmc/regression/jbmc/class-fields/Test.java
 create mode 100644 jbmc/regression/jbmc/class-fields/java/lang/Class.class
 create mode 100644 jbmc/regression/jbmc/class-fields/java/lang/Class.java
 create mode 100644 jbmc/regression/jbmc/class-fields/test.desc

diff --git a/jbmc/regression/jbmc/class-fields/Test.class b/jbmc/regression/jbmc/class-fields/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..a69b61691fefdb65fd7db0a768b8efa309591740
GIT binary patch
literal 598
zcmZXR%TC)+5QhJ;o%n*u#atSoHxLV8K{geeB1A>oO<j;6iqz~*oFh13Y-Bq;3@^aC
zAQcHD*z-&Xb&d<kq6^P`zL`0Ge7?O0uz@8HHs);1yD+d|<E;k^a~@{!&c=Jf)UwEP
znH4Hc@~<iv{a6kN)FV_kRicV5g1NHVC0IM@KoaVqO62bFv@f%cE+zzF8i}|oGNt{O
zpj8~HoEc$9=EZ03J{2lqZbWE?$KqVHW04%TcVeE->B)maL?=JRS=nym1Hsvh;+F-y
zgLIfh^1IUGTuofp2p=9M7_9?79Jqwm82#n-tZ!MCW<EY*k<b|D_xi^&D)^vrsN9Ay
zJCM1`<X}YL<%%I+!w=EJBEO@}PfLxKp2?O8(wngK*=w^V)|Isz&~G*jOtP$&K|+mf
z|6c*>Xt3v^IcnbLYTX<J#*ZtQ7nrz%_3H+e2Td|dQjIm^Sys8z84*q91(@R8G=C20
r2~C^-vxC_Y|5Hf^nt|~L)eG3xB`otA=KqUoNCk$!t<QPGj)B%+oj7Ul

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/class-fields/Test.java b/jbmc/regression/jbmc/class-fields/Test.java
new file mode 100644
index 00000000000..5ee259eb337
--- /dev/null
+++ b/jbmc/regression/jbmc/class-fields/Test.java
@@ -0,0 +1,10 @@
+public class Test {
+
+  public static void main() {
+
+    java.lang.Class c = Test.class;
+    assert false;
+
+  }
+
+}
diff --git a/jbmc/regression/jbmc/class-fields/java/lang/Class.class b/jbmc/regression/jbmc/class-fields/java/lang/Class.class
new file mode 100644
index 0000000000000000000000000000000000000000..6af088fde911a64f7061730ed80b7eaa05c01e30
GIT binary patch
literal 488
zcmYjNOHaZ;5dOB^QYl3WsQ9{g0}l4)MPp1zOh^z-FdV!sWyQtPl2SPMhdi5@Xgqi|
z@kbeFn?}qglX>j-nEC$s_yll*LkAY>MR066*v5{HhK*eY>t4xl%uw%5#Y*_0h$enF
zO65c*rwoNN6{+-`!ECmM47?MMB}1jBBH3TgMl!h-qmVkaUL1&UC=#XXyvfrCwP2|J
zWA21vu^`??Fi+x@O!{#&mT8wXlnB)mF_j0Y2p+G*JSTAm@iGbIrP4A^hCkL$U2LG}
zq5#{*o{N1PkgxR$*+&L%-MJo3WsuUMaWe69dB1a$*`P(q*K$S@ym{9e;)w2K(cKt5
zlAz3>j1(z4RQcHiu-b26FWI<6u|RFWgiF!Qatmc_QpHjE19x+<*M5cZ1)D#Eo9{3+
ej|t7=kQ_)(W7b?=&gId}f>FBA?y6K6sQm(2j$AMR

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/class-fields/java/lang/Class.java b/jbmc/regression/jbmc/class-fields/java/lang/Class.java
new file mode 100644
index 00000000000..96b348b7594
--- /dev/null
+++ b/jbmc/regression/jbmc/class-fields/java/lang/Class.java
@@ -0,0 +1,11 @@
+package java.lang;
+
+public class Class {
+
+  public Integer field;
+
+  protected void cproverNondetInitialize() {
+    org.cprover.CProver.assume(field == null);
+  }
+
+}
diff --git a/jbmc/regression/jbmc/class-fields/test.desc b/jbmc/regression/jbmc/class-fields/test.desc
new file mode 100644
index 00000000000..abf3d4e911c
--- /dev/null
+++ b/jbmc/regression/jbmc/class-fields/test.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Test\.java line 6.*: FAILURE$
+--
+^warning: ignoring
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 2556ee4d7e9..62b18d3dcf7 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -94,11 +94,6 @@ static void java_static_lifetime_init(
         if(allow_null)
         {
           irep_idt nameid=sym.symbol_expr().get_identifier();
-          std::string namestr=id2string(nameid);
-          const std::string suffix="@class_model";
-          // Static '.class' fields are always non-null.
-          if(has_suffix(namestr, suffix))
-            allow_null=false;
           if(allow_null && is_java_string_literal_id(nameid))
             allow_null=false;
           if(allow_null && is_non_null_library_global(nameid))
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 6e9617cb109..b8ed2371242 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -874,10 +874,6 @@ void java_object_factoryt::gen_nondet_pointer_init(
 
   auto set_null_inst=get_null_assignment(expr, pointer_type);
 
-  // Determine whether the pointer can be null. In particular the pointers
-  // inside the java.lang.Class class shall not be null
-  const bool not_null = !allow_null || class_identifier == "java.lang.Class";
-
   // Alternatively, if this is a void* we *must* initialise with null:
   // (This can currently happen for some cases of #exception_value)
   bool must_be_null=
@@ -889,7 +885,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
     // <expr> = nullptr;
     new_object_assignments.add(set_null_inst);
   }
-  else if(not_null)
+  else if(!allow_null)
   {
     // Add the following code to assignments:
     // <expr> = <aoe>;