Record Feature Progress

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

@@ -18,43 +18,16 @@
 
 package gov.nasa.jpf.jvm;
 
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.util.Misc;
+import gov.nasa.jpf.util.StringSetMatcher;
+import gov.nasa.jpf.vm.*;
+
 import java.lang.reflect.Modifier;
 import java.util.HashMap;
 import java.util.LinkedHashMap;
 import java.util.LinkedList;
 
-import gov.nasa.jpf.Config;
-import gov.nasa.jpf.util.Misc;
-import gov.nasa.jpf.util.StringSetMatcher;
-import gov.nasa.jpf.vm.AbstractTypeAnnotationInfo;
-import gov.nasa.jpf.vm.AnnotationInfo;
-import gov.nasa.jpf.vm.BootstrapMethodInfo;
-import gov.nasa.jpf.vm.BytecodeAnnotationInfo;
-import gov.nasa.jpf.vm.BytecodeTypeParameterAnnotationInfo;
-import gov.nasa.jpf.vm.ClassInfo;
-import gov.nasa.jpf.vm.ClassInfoException;
-import gov.nasa.jpf.vm.ClassLoaderInfo;
-import gov.nasa.jpf.vm.ClassParseException;
-import gov.nasa.jpf.vm.DirectCallStackFrame;
-import gov.nasa.jpf.vm.ExceptionHandler;
-import gov.nasa.jpf.vm.ExceptionParameterAnnotationInfo;
-import gov.nasa.jpf.vm.FieldInfo;
-import gov.nasa.jpf.vm.FormalParameterAnnotationInfo;
-import gov.nasa.jpf.vm.GenericSignatureHolder;
-import gov.nasa.jpf.vm.InfoObject;
-import gov.nasa.jpf.vm.LocalVarInfo;
-import gov.nasa.jpf.vm.MethodInfo;
-import gov.nasa.jpf.vm.NativeMethodInfo;
-import gov.nasa.jpf.vm.StackFrame;
-import gov.nasa.jpf.vm.SuperTypeAnnotationInfo;
-import gov.nasa.jpf.vm.ThreadInfo;
-import gov.nasa.jpf.vm.ThrowsAnnotationInfo;
-import gov.nasa.jpf.vm.TypeAnnotationInfo;
-import gov.nasa.jpf.vm.TypeParameterAnnotationInfo;
-import gov.nasa.jpf.vm.TypeParameterBoundAnnotationInfo;
-import gov.nasa.jpf.vm.Types;
-import gov.nasa.jpf.vm.VariableAnnotationInfo;
-
 /**
  * a ClassInfo that was created from a Java classfile
  */
@@ -118,14 +91,15 @@ public void setClassAttribute (ClassFile cf, int attrIndex, String name, int att
     public void setBootstrapMethodCount (ClassFile cf, Object tag, int count) {
       bootstrapMethods = new BootstrapMethodInfo[count];
     }
-    
+
     @Override
     public void setBootstrapMethod (ClassFile cf, Object tag, int idx, int refKind, String cls, String mth,
                                      String parameters, String descriptor, int[] cpArgs) {
       String clsName = null;
       ClassInfo enclosingLambdaCls;
-
-      if (cpArgs.length > 1) {
+
+      if (cls.equals("java/lang/invoke/LambdaMetafactory") && (mth.equals("metafactory") || mth.equals("altMetafactory"))) {
+        assert(cpArgs.length>1);
         // For Lambdas
       	int mrefIdx = cf.mhMethodRefIndexAt(cpArgs[1]);
         clsName = cf.methodClassNameAt(mrefIdx).replace('/', '.');
@@ -164,16 +138,17 @@ public void setBootstrapMethod (ClassFile cf, Object tag, int idx, int refKind,
       	int lambdaRefKind = cf.mhRefTypeAt(cpArgs[1]);
       	String mthName = cf.methodNameAt(mrefIdx);
         String signature = cf.methodDescriptorAt(mrefIdx);
-        String samDescriptor = cf.methodTypeDescriptorAt(cpArgs[2]); 
-        
+        String samDescriptor = cf.methodTypeDescriptorAt(cpArgs[2]);
+
         setBootstrapMethodInfo(enclosingLambdaCls, mthName, signature, idx, lambdaRefKind, samDescriptor, null,
-                               isSerializable ? BootstrapMethodInfo.BMType.SERIALIZABLE_LAMBDA_EXPRESSION
-                                              : BootstrapMethodInfo.BMType.LAMBDA_EXPRESSION);
-      }
-      else {
+                isSerializable ? BootstrapMethodInfo.BMType.SERIALIZABLE_LAMBDA_EXPRESSION
+                        : BootstrapMethodInfo.BMType.LAMBDA_EXPRESSION);
+      } else if (cls.equals("java/lang/runtime/ObjectMethods") && mth.equals("bootstrap")) {
+        // -----
+      } else {
         // For String Concatenation
-        clsName = cls; 
-          
+        clsName = cls;
+        assert(mth.startsWith("makeConcat"));
         if(!clsName.equals(JVMClassInfo.this.getName())) {
         enclosingLambdaCls = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
         } else {

src/tests/java17/RecordFeatureTest.java

@@ -0,0 +1,53 @@
+package java17;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+
+public class RecordFeatureTest extends TestJPF {
+    record Point(int x, int y){}
+    // Official documents suggest that fields of "record" are "private" and "final".
+    // So we are testing by direct access. It should fail here at compile time, but do not know why it works.
+    @Test
+    public void testRecordFieldsDirectly(){
+        if (verifyNoPropertyViolation()){
+            Point point = new Point(4, 5);
+            assertEquals("",4,point.x);
+            assertEquals("",5,point.y);
+        }
+    }
+    @Test
+    public void testRecordFields(){
+        if (verifyNoPropertyViolation()){
+            Point point = new Point(4, 5);
+            assertEquals("",4,point.x());
+            assertEquals("",5,point.y());
+        }
+    }
+    @Test
+    public void testRecordEquality(){
+        if (verifyNoPropertyViolation()){
+            Point point1 = new Point(4,5);
+            Point point2 = new Point(4,5);
+            Point point3 = new Point(3,5);
+            assertEquals("",point1, point2);
+            assertNotEquals("",point1, point3);
+        }
+    }
+    @Test
+    public void testRecordHashCode() {
+        if (verifyNoPropertyViolation()){
+            Point point1 = new Point(4, 5);
+            Point point2 = new Point(4, 5);
+            Point point3 = new Point(3,5);
+            assertEquals("", point1.hashCode(), point2.hashCode());
+            assertNotEquals("",point1.hashCode(),point3.hashCode());
+        }
+    }
+    @Test
+    public void testRecordToString() {
+        if (verifyNoPropertyViolation()){
+            Point point = new Point(4, 5);
+            assertEquals("Point[x=4, y=5]", point.toString());
+        }
+    }
+}