Record support (#520)

* Implemented parsing for the record

* Added support for printing record components

* Implemented RecordComponentInfo class to hold record metadata

* Updated ClassInfo.java to support record functionality

* Added support for parsing record components like name,descriptor and annotation attributes

Author: Mahmoud-Khawaja

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

@@ -178,6 +178,7 @@ public String getRequestedTypeName(){
   public static final String RUNTIME_INVISIBLE_ANNOTATIONS_ATTR = "RuntimeInvisibleAnnotations";
   public static final String RUNTIME_VISIBLE_ANNOTATIONS_ATTR = "RuntimeVisibleAnnotations";
   public static final String RUNTIME_VISIBLE_TYPE_ANNOTATIONS_ATTR = "RuntimeVisibleTypeAnnotations";
+  public static final String RUNTIME_INVISIBLE_TYPE_ANNOTATIONS_ATTR = "RuntimeInvisibleTypeAnnotations";
 
   //--- standard field attributes
   public static final String CONST_VALUE_ATTR = "ConstantValue";
@@ -216,11 +217,19 @@ public String getRequestedTypeName(){
   public static final String  INNER_CLASSES_ATTR = "InnerClasses";
   public static final String  ENCLOSING_METHOD_ATTR = "EnclosingMethod";
   public static final String  BOOTSTRAP_METHOD_ATTR = "BootstrapMethods";
-  
+  public static final String  RECORD_ATTR = "Record";
+
   protected final static String[] stdClassAttrs = {
     SOURCE_FILE_ATTR, DEPRECATED_ATTR, INNER_CLASSES_ATTR, DEPRECATED_ATTR, SIGNATURE_ATTR,
     RUNTIME_INVISIBLE_ANNOTATIONS_ATTR, RUNTIME_VISIBLE_ANNOTATIONS_ATTR, RUNTIME_VISIBLE_TYPE_ANNOTATIONS_ATTR,
-    ENCLOSING_METHOD_ATTR, BOOTSTRAP_METHOD_ATTR };
+    ENCLOSING_METHOD_ATTR, BOOTSTRAP_METHOD_ATTR, RECORD_ATTR};
+
+  //--- standard Record attributes
+  public static final String[] stdRecordComponentAttrs = {
+          SIGNATURE_ATTR,
+          RUNTIME_INVISIBLE_ANNOTATIONS_ATTR, RUNTIME_VISIBLE_ANNOTATIONS_ATTR,
+          RUNTIME_INVISIBLE_TYPE_ANNOTATIONS_ATTR, RUNTIME_VISIBLE_TYPE_ANNOTATIONS_ATTR
+  };
 
 
   protected String internStdAttrName(int cpIdx, String name, String[] stdNames){
@@ -1530,6 +1539,75 @@ public void parseBootstrapMethodAttr (ClassFileReader reader, Object tag){
 
     setBootstrapMethodsDone( reader, tag);
   }
+
+  //-- record parsing
+  /*
+  Record_attribute {
+    u2 attribute_name_index;
+    u4 attribute_length;
+    u2 components_count;
+    {
+        u2 name_index;
+        u2 descriptor_index;
+        u2 attributes_count;
+        attribute_info attributes[attributes_count];
+    } components[components_count];
+    }
+   */
+  private void setRecordComponentCount(ClassFileReader reader, Object tag, int count) {
+    int p = pos;
+    reader.setRecordComponentCount(this, tag, count);
+    pos = p;
+  }
+
+  private void setRecordComponent(ClassFileReader reader, Object tag, int index, String name, String descriptor, int attributesCount) {
+    int p = pos;
+    reader.setRecordComponent(this, tag, index, name, descriptor, attributesCount);
+    pos = p;
+  }
+
+  private void setRecordComponentAttribute(ClassFileReader reader, Object tag, int componentIndex, int attrIndex, String attrName, int attrLength) {
+    int p = pos + attrLength;
+    reader.setRecordComponentAttribute(this, tag, componentIndex, attrIndex, attrName, attrLength);
+    pos = p;
+  }
+
+  private void setRecordComponentsDone(ClassFileReader reader, Object tag) {
+    int p = pos;
+    reader.setRecordComponentsDone(this, tag);
+    pos = p;
+  }
+
+  public void parseRecordAttribute(ClassFileReader reader, Object tag) {
+    int componentsCount = readU2();
+    setRecordComponentCount(reader, tag, componentsCount);
+
+    for (int i = 0; i < componentsCount; i++) {
+      int nameIndex = readU2();
+      String name = utf8At(nameIndex);
+
+      int descriptorIndex = readU2();
+      String descriptor = utf8At(descriptorIndex);
+
+      int attributesCount = readU2();
+
+      // Create and set the record component
+      setRecordComponent(reader, tag, i, name, descriptor, attributesCount);
+
+      // Parse the component attributes
+      for (int j = 0; j < attributesCount; j++) {
+        int attrNameIndex = readU2();
+        String attrName = utf8At(attrNameIndex);
+
+        attrName = internStdAttrName(attrNameIndex, attrName, stdRecordComponentAttrs);
+
+        int attrLength = readI4();
+        setRecordComponentAttribute(reader, tag, i, j, attrName, attrLength);
+      }
+    }
+
+    setRecordComponentsDone(reader, tag);
+  }
 
   String nameAt(int nameTypeInfoIdx) {
     return utf8At(u2(cpPos[nameTypeInfoIdx] + 1));

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

@@ -188,6 +188,47 @@ public void setMethodAttribute(ClassFile cf, int methodIndex, int attrIndex, Str
     }
   }
 
+  //--- records
+  @Override
+  public void setRecordComponentCount(ClassFile cf, Object tag, int count) {
+    printSectionHeader("record components");
+    pw.printf("%srecord component count=%d\n", indent, count);
+    incIndent();
+  }
+
+  @Override
+  public void setRecordComponent(ClassFile cf, Object tag, int index, String name, String descriptor, int attributesCount) {
+    pw.printf("%s[%d]: %s, type=%s", indent, index, name, descriptor);
+  }
+
+  @Override
+  public void setRecordComponentAttribute(ClassFile cf, Object tag, int componentIndex, int attrIndex, String attrName, int attrLength) {
+    pw.printf(", attribute[%d]: %s", attrIndex, attrName);
+
+    if (attrName == ClassFile.SIGNATURE_ATTR) {
+      cf.parseSignatureAttr(this, tag);
+    } else if (attrName == ClassFile.RUNTIME_VISIBLE_ANNOTATIONS_ATTR) {
+      cf.parseAnnotationsAttr(this, tag);
+    } else if (attrName == ClassFile.RUNTIME_INVISIBLE_ANNOTATIONS_ATTR) {
+      cf.parseAnnotationsAttr(this, tag);
+    } else if (attrName == ClassFile.RUNTIME_VISIBLE_TYPE_ANNOTATIONS_ATTR) {
+      cf.parseTypeAnnotationsAttr(this, tag);
+    } else if (attrName == ClassFile.RUNTIME_INVISIBLE_TYPE_ANNOTATIONS_ATTR) {
+      cf.parseTypeAnnotationsAttr(this, tag);
+    } else {
+      pw.printf(" ,length=%d,data=[", attrLength);
+      printRawData(pw, cf, attrLength, 10);
+      pw.println(']');
+    }
+
+    pw.println();
+  }
+
+  @Override
+  public void setRecordComponentsDone(ClassFile cf, Object tag) {
+    decIndent();
+  }
+
   @Override
   public void setMethodAttributesDone(ClassFile cf, int methodIndex){
     decIndent();

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

@@ -195,4 +195,13 @@ void setEnumAnnotationValue(ClassFile cf, Object tag, int annotationIndex, int v
 
 
   void setSignature(ClassFile cf, Object tag, String signature);
+
+  //--- records
+  void setRecordComponentCount(ClassFile cf, Object tag, int count);
+
+  void setRecordComponent(ClassFile cf, Object tag, int index, String name, String descriptor, int attributesCount);
+
+  void setRecordComponentAttribute(ClassFile cf, Object tag, int componentIndex, int attrIndex, String attrName, int attrLength);
+
+  void setRecordComponentsDone(ClassFile cf, Object tag);
 }

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

@@ -249,4 +249,16 @@ public void setSignature(ClassFile cf, Object tag, String signature) {}
 
   @Override
   public void setAnnotationFieldValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex) {}
+
+  @Override
+  public void setRecordComponentCount(ClassFile cf, Object tag, int count) {}
+
+  @Override
+  public void setRecordComponent(ClassFile cf, Object tag, int index, String name, String descriptor, int attributesCount) {}
+
+  @Override
+  public void setRecordComponentAttribute(ClassFile cf, Object tag, int componentIndex, int attrIndex, String attrName, int attrLength) {}
+
+  @Override
+  public void setRecordComponentsDone(ClassFile cf, Object tag) {}
 }

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

@@ -84,6 +84,9 @@ public void setClassAttribute (ClassFile cf, int attrIndex, String name, int att
       } else if (name == ClassFile.BOOTSTRAP_METHOD_ATTR) {
         cf.parseBootstrapMethodAttr(this, JVMClassInfo.this);
 
+      } else if (name == ClassFile.RECORD_ATTR){
+        cf.parseRecordAttribute(this,JVMClassInfo.this);
+
       }
     }
 
@@ -189,6 +192,65 @@ public void setBootstrapMethodInfo(ClassInfo enclosingCls, String mthName, Strin
       }
     }
 
+    //--- Storing record while parsing
+    @Override
+    public void setRecordComponentCount(ClassFile cf, Object tag, int count) {
+      JVMClassInfo.this.isRecord = true; // marking this as a record
+      JVMClassInfo.this.recordComponents = new RecordComponentInfo[count]; // init array
+    }
+
+    @Override
+    public void setRecordComponent(ClassFile cf, Object tag, int index, String name, String descriptor, int attributesCount) {
+      // Create a basic RecordComponentInfo object. this can be the default
+      // TODO: attributes like signature/annotations will be added later
+      RecordComponentInfo rci = new RecordComponentInfo(name, descriptor, null, null, null);
+      JVMClassInfo.this.recordComponents[index] = rci;
+    }
+
+    @Override
+    public void setRecordComponentAttribute(ClassFile cf, Object tag, int componentIndex, int attrIndex, String attrName, int attrLength) {
+      RecordComponentInfo rci = JVMClassInfo.this.recordComponents[componentIndex];
+
+      String name = rci.getName();
+      String descriptor = rci.getDescriptor();
+      String signature = rci.getSignature();
+      AnnotationInfo[] annotations = rci.getAnnotations();
+      TypeAnnotationInfo[] typeAnnotations = rci.getTypeAnnotations();
+
+      if (attrName.equals(ClassFile.SIGNATURE_ATTR)) {
+        // Use the signature consumer pattern
+        cf.parseSignatureAttr(this, rci);
+        signature = rci.getSignature();
+      }
+      else if (attrName.equals(ClassFile.RUNTIME_VISIBLE_ANNOTATIONS_ATTR)) {
+        annotations = new AnnotationInfo[0]; // Initialize or preserve existing
+        cf.parseAnnotationsAttr(this, rci);
+        annotations = rci.getAnnotations();
+      }
+      else if (attrName.equals(ClassFile.RUNTIME_INVISIBLE_ANNOTATIONS_ATTR)) {
+        cf.parseAnnotationsAttr(this, rci);
+        // we might need to merge with existing annotations
+      }
+      else if (attrName.equals(ClassFile.RUNTIME_VISIBLE_TYPE_ANNOTATIONS_ATTR)) {
+        // Set up for type annotation parsing
+        typeAnnotations = new TypeAnnotationInfo[0];
+        cf.parseTypeAnnotationsAttr(this, rci);
+        typeAnnotations = rci.getTypeAnnotations();
+      }
+      else if (attrName.equals(ClassFile.RUNTIME_INVISIBLE_TYPE_ANNOTATIONS_ATTR)) {
+        cf.parseTypeAnnotationsAttr(this, rci);
+      }
+
+      // a new RecordComponentInfo with all updated attributes
+      JVMClassInfo.this.recordComponents[componentIndex] =
+              new RecordComponentInfo(name, descriptor, signature, annotations, typeAnnotations);
+    }
+
+    @Override
+    public void setRecordComponentsDone(ClassFile cf, Object tag) {
+      // TODO: finalize logic here if needed or whatever we can leave it for now
+    }
+
    //--- inner/enclosing classes 
     @Override
     public void setInnerClassCount (ClassFile cf, Object tag, int classCount) {

src/main/gov/nasa/jpf/vm/ClassInfo.java

@@ -144,6 +144,7 @@ public class ClassInfo extends InfoObject implements Iterable<MethodInfo>, Gener
   protected boolean      isReferenceArray = false;
   protected boolean      isAbstract = false;
   protected boolean      isBuiltin = false;
+  protected boolean      isRecord = false;
 
   // that's ultimately where we keep the attributes
   // <2do> this is currently quite redundant, but these are used in reflection
@@ -222,7 +223,10 @@ public class ClassInfo extends InfoObject implements Iterable<MethodInfo>, Gener
   /** from where the corresponding classfile was loaded (if this is not a builtin) */
   protected gov.nasa.jpf.vm.ClassFileContainer container;
 
-  
+  /** Array of Record components if this class is a record **/
+  protected RecordComponentInfo[] recordComponents;
+
+
   /**
    *  a search global numeric id that is only unique within this ClassLoader namespace. Ids are
    *  computed by the ClassLoaderInfo/Statics implementation during ClassInfo registration
@@ -866,6 +870,13 @@ public ClassInfo getClassInfo() {
     return this;
   }
 
+  /**
+   * Returns the array of record components if this class is a record, or null otherwise.
+   */
+  public RecordComponentInfo[] getRecordComponents() {
+    return recordComponents;
+  }
+
   protected void setAssertionStatus() {
     if(isInitialized()) {
       return;
@@ -928,6 +939,8 @@ public boolean isThreadClassInfo() {
     return isThreadClassInfo;
   }
 
+  public boolean isRecord() { return isRecord; }
+
   protected void checkNoClinitInitialization(){
     if (!isInitialized()){
       ThreadInfo ti = ThreadInfo.getCurrentThread();

src/main/gov/nasa/jpf/vm/RecordComponentInfo.java

@@ -0,0 +1,42 @@
+package gov.nasa.jpf.vm;
+
+/**
+ * Class representing a Record component in a Java 17+ record class
+ */
+
+public class RecordComponentInfo {
+    private final String name;
+    private final String descriptor;
+    private final String signature;
+    private final AnnotationInfo[] annotations;
+    private final TypeAnnotationInfo[] typeAnnotations;
+
+    public RecordComponentInfo(String name, String descriptor, String signature,
+                           AnnotationInfo[] annotations, TypeAnnotationInfo[] typeAnnotations) {
+        this.name = name;
+        this.descriptor = descriptor;
+        this.signature = signature;
+        this.annotations = annotations;
+        this.typeAnnotations = typeAnnotations;
+    }
+
+    public String getName() {
+        return name;
+    }
+
+    public String getDescriptor() {
+        return descriptor;
+    }
+
+    public String getSignature() {
+        return signature;
+    }
+
+    public AnnotationInfo[] getAnnotations() {
+        return annotations;
+    }
+
+    public TypeAnnotationInfo[] getTypeAnnotations() {
+        return typeAnnotations;
+    }
+}