From 52fcc46d862ed68cf6e90b469ac1fd7da5b951b7 Mon Sep 17 00:00:00 2001 From: eklaDFF Date: Fri, 4 Oct 2024 13:41:37 +0530 Subject: [PATCH 1/2] add Tests to test record feature of jpf --- src/tests/java17/RecordFeatureTest.java | 53 +++++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 src/tests/java17/RecordFeatureTest.java diff --git a/src/tests/java17/RecordFeatureTest.java b/src/tests/java17/RecordFeatureTest.java new file mode 100644 index 00000000..e6a69328 --- /dev/null +++ b/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()); + } + } +} From 62a1a11788f3c126aa542591d55f1c147a2e2799 Mon Sep 17 00:00:00 2001 From: eklaDFF Date: Fri, 4 Oct 2024 13:43:29 +0530 Subject: [PATCH 2/2] modify the setBootstrapMethod(...) to adapt Java-17 requirement --- src/main/gov/nasa/jpf/jvm/JVMClassInfo.java | 61 ++++++--------------- 1 file changed, 18 insertions(+), 43 deletions(-) diff --git a/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java b/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java index 969f4ca3..2c641912 100644 --- a/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java +++ b/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 {