Skip to content

Commit

Permalink
Record Feature Progress (#499)
Browse files Browse the repository at this point in the history 
* add Tests to test record feature of jpf

* modify the setBootstrapMethod(...) to check the type of bootstrap method more precisely to handle each type with the correct scheme
  • Loading branch information
@eklaDFF
eklaDFF authored Oct 4, 2024
1 parent 50557c9 commit 4ffa7e9
Show file tree
Hide file tree
Showing 2 changed files with 71 additions and 43 deletions.
61 changes: 18 additions & 43 deletions src/main/gov/nasa/jpf/jvm/JVMClassInfo.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
*/
Expand Down Expand Up @@ -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('/', '.');
Expand Down Expand Up @@ -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 {
Expand Down
53 changes: 53 additions & 0 deletions src/tests/java17/RecordFeatureTest.java
View file
Original file line number Diff line number Diff line change
@@ -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());
}
}
}

0 comments on commit 4ffa7e9

Please sign in to comment.