Add object stream support for JPF on Java 11

src/classes/modules/java.base/java/lang/Class.java

@@ -74,7 +74,9 @@ public final class Class<T> implements Serializable, GenericDeclaration, Type, A
    * to be set during <clinit> of the corresponding class
    */
   private boolean isPrimitive;
-
+
+  transient ClassValue.ClassValueMap classValueMap;
+
   private Class() {}
 
   public native boolean isArray ();
@@ -163,6 +165,15 @@ public Package getPackage() {
 
   }
 
+  public String getPackageName() {
+    int idx = name.lastIndexOf('.');
+    if (idx >= 0){
+      return name.substring(0,idx);
+    } else {
+      return "";
+    }
+  }
+
   //--- enum support ()
   // Java 1.5
   public native T[] getEnumConstants();

src/classes/modules/java.base/jdk/internal/misc/SharedSecrets.java

@@ -62,6 +62,7 @@ public class SharedSecrets {
   private static JavaAWTAccess javaAWTAccess;
   private static JavaObjectInputStreamAccess javaObjectInputStreamAccess;
   private static JavaObjectInputFilterAccess javaObjectInputFilterAccess;
+  private static JavaObjectInputStreamReadString javaObjectInputStreamReadString;
 
   // (required for EnumSet ops)
   public static JavaLangAccess getJavaLangAccess() {
@@ -196,4 +197,14 @@ public static JavaAWTAccess getJavaAWTAccess(){
     return javaAWTAccess;
   }
 
+  public static JavaObjectInputStreamReadString getJavaObjectInputStreamReadString() {
+    if (javaObjectInputStreamReadString == null) {
+        unsafe.ensureClassInitialized(ObjectInputStream.class);
+    }
+    return javaObjectInputStreamReadString;
+  }
+
+  public static void setJavaObjectInputStreamReadString(JavaObjectInputStreamReadString access) {
+    javaObjectInputStreamReadString = access;
+  }
 }

src/main/gov/nasa/jpf/jvm/JVMClassFileContainer.java

@@ -117,6 +117,20 @@ static String getModuleName(String typeName) {
       return typeName.split("\\$&\\$")[0];
     }
     try {
+      // In support of jdk.internal.reflect.ReflectionFactory,
+      // we use a model class java.lang.reflect.Constructor (which is non-final
+      // in our implementation but is final in OpenJDK's implementation)
+      // and define gov.nasa.jpf.SerializationConstructor as a subclass of it.
+      //
+      // Here we try to load the class on the underlying JVM (OpenJDK) to
+      // query its module name. But for gov.nasa.jpf.SerializationConstructor,
+      // OpenJDK will see it inheriting a final class (j.l.r.Constructor) and throw
+      // java.lang.VerifyError. Since we know it doesn't have module name, we can
+      // directly return null instead of loading it on the underlying OpenJDK
+      // and doing the query.
+      if (typeName.equals("gov.nasa.jpf.SerializationConstructor")) {
+        return null;
+      }
       return Class.forName(typeName.split("\\$")[0]).getModule().getName();
     } catch (ClassNotFoundException e) {
       return null;

src/peers/gov/nasa/jpf/vm/JPF_java_lang_System.java

@@ -177,6 +177,7 @@ int getSelectedSysPropsFromHost (MJIEnv env){
         "file.separator",
         "user.name",
         "user.dir",
+        "user.home",
         "user.timezone",
         "user.country",
         "java.home",

src/peers/gov/nasa/jpf/vm/JPF_jdk_internal_misc_VM.java

@@ -30,4 +30,12 @@ public class JPF_jdk_internal_misc_VM extends NativePeer {
   public void initialize____V (MJIEnv env, int clsObjRef){
     // nothing here yet
   }
+
+  @MJI
+  public void initializeFromArchive(MJIEnv env,
+                                    int clsObjRef,
+                                    int cRef) {
+    // We don't support CDS so we don't need to implement it,
+    // which doesn't affect our correctness.
+  }
 }

src/peers/gov/nasa/jpf/vm/JPF_jdk_internal_reflect_ReflectionFactory.java

@@ -0,0 +1,42 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ *        http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+package gov.nasa.jpf.vm;
+
+import gov.nasa.jpf.annotation.MJI;
+
+// Similar to JPF_sun_reflect_ReflectionFactory
+public class JPF_jdk_internal_reflect_ReflectionFactory extends NativePeer {
+
+  @MJI
+  public int generateConstructor__Ljava_lang_Class_2Ljava_lang_reflect_Constructor_2__Ljava_lang_reflect_Constructor_2(MJIEnv env,
+                                                                                                                       int objRef,
+                                                                                                                       int clsRef,
+                                                                                                                       int ctorRef) {
+    // This creates an artificial ctor for the concrete type
+    // that explicitly calls the default ctor of the first
+    // non-serializable superclass.
+    ClassInfo ci = ClassInfo.getInitializedClassInfo("gov.nasa.jpf.SerializationConstructor", env.getThreadInfo());
+    int sCtorRef = env.newObject(ci);
+
+    env.setReferenceField(sCtorRef, "mdc", clsRef);
+    env.setReferenceField(sCtorRef, "firstNonSerializableCtor", ctorRef);
+
+    return sCtorRef;
+  }
+}

src/tests/gov/nasa/jpf/test/java/io/ObjectStreamTest.java

@@ -39,7 +39,7 @@ static class X implements Serializable {
     Y a = new Y(-42);
 
     @Override
-	public String toString() {
+    public String toString() {
       return "X{q=\""+q+"\",a="+a+'}';
     }
   }
@@ -61,7 +61,7 @@ static class Y implements Serializable {
     }
 
     @Override
-	public String toString() {
+    public String toString() {
       return "Y{z="+z+",b="+b+",c="+c+",s="+s+",i="+i+",l="+l+",f="+f+",d="+d+ '}';
     }
   }
@@ -95,7 +95,7 @@ public void testSimpleReadbackOk () {
         X x = (X) o;
         assert x.a.i == -42;
       } catch (Throwable t){
-        //t.printStackTrace();
+        t.printStackTrace();
         fail("serialization readback failed: " + t);
       }