From c761c562cc65d28c73c135433e477bfb32d651c7 Mon Sep 17 00:00:00 2001 From: Darshan R Date: Tue, 11 Aug 2026 12:00:45 +0000 Subject: [PATCH 1/2] fix: correct record equals/toString/hashCode for reference and array components (#628) Three bugs fixed in executeRecord() on call-site-generation branch: 1. equals() for array components: was doing deep element comparison, now uses reference identity (JEP 395: Objects.equals() on arrays delegates to Object.equals() = reference identity). 2. toString() for String/boxed/reference components: was printing JPF heap addresses (e.g. java.lang.String@209). Now: - String: ei.asString() for actual content - Boxed JDK types: wrapped value via 'value' field - Arrays: [I@hexHash format (Object.toString() semantics) - Other references: ClassName@hexHash 3. equals() for boxed types (Integer, Long, etc.): was using reference identity, now compares by wrapped value using a safe whitelist of known JDK boxed types. User classes with a 'value' field but identity-based equals() are NOT affected. 4. hashCode() made consistent with equals(): - String: content hash - Boxed JDK types: wrapped value hash - Arrays: objectRef (identity, consistent with array equals) - Nested records: recursive hash - Other refs: objectRef (identity) Added RecordReferenceComponentTest with 15 regression tests covering arrays, strings, boxed types, identity classes, null components, nested records, and hashCode consistency. Verified: all 15 new tests pass, full suite BUILD SUCCESSFUL. --- .../nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java | 106 ++++++++++-- .../records/RecordReferenceComponentTest.java | 160 ++++++++++++++++++ 2 files changed, 250 insertions(+), 16 deletions(-) create mode 100644 src/tests/java17/records/RecordReferenceComponentTest.java diff --git a/src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java b/src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java index 896151e8..69a7e21c 100644 --- a/src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java +++ b/src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java @@ -50,6 +50,14 @@ */ public class INVOKEDYNAMIC extends Instruction { + private static final java.util.Set BOXED_TYPES = new java.util.HashSet<>( + java.util.Arrays.asList( + "java.lang.Integer", "java.lang.Long", "java.lang.Short", + "java.lang.Byte", "java.lang.Character", "java.lang.Boolean", + "java.lang.Float", "java.lang.Double" + ) + ); + // ==================== FIELDS ==================== int bootstrapMethodIndex; @@ -409,12 +417,43 @@ private int computeRecordHashCode(ThreadInfo ti, ClassInfo ci) { String[] components = bmi.getBmArg().split(";"); for (String compName : components) { + FieldInfo fi = ci.getDeclaredInstanceField(compName); Object value = ei.getFieldValueObject(compName); - hash = 31 * hash + (value != null ? value.hashCode() : 0); + hash = 31 * hash + componentHashCode(ti, value, fi != null ? fi.getSignature() : "Ljava/lang/Object;"); } return hash; } + private int componentHashCode(ThreadInfo ti, Object value, String sig) { + if (value == null) return 0; + char typeChar = sig.charAt(0); + if (isPrimitiveType(typeChar)) return value.hashCode(); + if (typeChar == '[') { + ElementInfo arrayEi = (value instanceof ElementInfo) ? (ElementInfo) value + : ti.getHeap().get((Integer) value); + return arrayEi != null ? arrayEi.getObjectRef() : 0; + } + if (value instanceof ElementInfo) { + ElementInfo valEi = (ElementInfo) value; + ClassInfo valCi = valEi.getClassInfo(); + if ("java.lang.String".equals(valCi.getName())) return valEi.asString().hashCode(); + if (valCi.isRecord()) { + StackFrame f = ti.getModifiableTopFrame(); + int orig = f.getThis(); + f.setThis(valEi.getObjectRef()); + int h = computeRecordHashCode(ti, valCi); + f.setThis(orig); + return h; + } + if (BOXED_TYPES.contains(valCi.getName())) { + Object fv = valEi.getFieldValueObject("value"); + return fv != null ? fv.hashCode() : 0; + } + return valEi.getObjectRef(); + } + return value.hashCode(); + } + private int computeRecordToString(ThreadInfo ti, ClassInfo ci) { ElementInfo ei = ti.getThisElementInfo(); String fullName = ci.getName(); @@ -453,6 +492,38 @@ private String formatRecordComponent(ThreadInfo ti, Object value) { currentFrame.setThis(originalThis); return result; } + if (value instanceof ElementInfo) { + ElementInfo valueEi = (ElementInfo) value; + ClassInfo valueCi = valueEi.getClassInfo(); + // String: extract actual content + if ("java.lang.String".equals(valueCi.getName())) { + return valueEi.asString(); + } + // Nested record: recurse + if (valueCi.isRecord()) { + StackFrame currentFrame = ti.getModifiableTopFrame(); + int originalThis = currentFrame.getThis(); + currentFrame.setThis(valueEi.getObjectRef()); + int stringRef = computeRecordToString(ti, valueCi); + String result = ti.getHeap().get(stringRef).asString(); + currentFrame.setThis(originalThis); + return result; + } + // Arrays: Object.toString() format — "[I@hexHash" — NOT deep printing. + // Java record toString() calls component.toString(), and arrays inherit + // Object.toString() which gives the type descriptor + identity hash. + if (valueEi.isArray()) { + String typeSig = valueCi.getSignature(); + return typeSig + "@" + Integer.toHexString(valueEi.getObjectRef()); + } + // Known JDK boxed types: show the wrapped value + if (BOXED_TYPES.contains(valueCi.getName())) { + Object fieldVal = valueEi.getFieldValueObject("value"); + return String.valueOf(fieldVal); + } + // All other reference types: Object.toString() = "ClassName@hexHash" + return valueCi.getName() + "@" + Integer.toHexString(valueEi.getObjectRef()); + } return String.valueOf(value); } @@ -472,21 +543,13 @@ private boolean deepEquals(ThreadInfo ti, Object val1, Object val2, String sig) } private boolean compareArrays(ThreadInfo ti, Object val1, Object val2, String sig) { - ElementInfo ei1 = ti.getHeap().get((Integer) val1); - ElementInfo ei2 = ti.getHeap().get((Integer) val2); - - if (ei1 == null || ei2 == null || !ei1.isArray() || !ei2.isArray()) return false; - if (ei1.arrayLength() != ei2.arrayLength()) return false; - - String componentSig = sig.substring(1); - char compType = componentSig.charAt(0); - - for (int i = 0; i < ei1.arrayLength(); i++) { - Object elem1 = getArrayElement(ei1, i, compType); - Object elem2 = getArrayElement(ei2, i, compType); - if (!deepEquals(ti, elem1, elem2, componentSig)) return false; - } - return true; + // Per JEP 395: record equals() uses Objects.equals() per component. + // For arrays, Objects.equals(a, b) calls a.equals(b) = Object.equals() = reference identity. + ElementInfo ei1 = (val1 instanceof ElementInfo) ? (ElementInfo) val1 + : ti.getHeap().get((Integer) val1); + ElementInfo ei2 = (val2 instanceof ElementInfo) ? (ElementInfo) val2 + : ti.getHeap().get((Integer) val2); + return ei1 == ei2; } private boolean comparePrimitives(Object val1, Object val2, char typeChar) { @@ -516,6 +579,17 @@ private boolean compareReferenceTypes(ThreadInfo ti, Object val1, Object val2, S return compareRecords(ti, ei1, ei2, ci); } + // For boxed types (Integer, Long, etc.) and other types with a "value" field, + // compare by value rather than by identity + // Use value-field comparison ONLY for known JDK boxed types (whitelist). + // User classes with a "value" field but identity equals() must NOT be affected. + if (BOXED_TYPES.contains(ci.getName())) { + Object v1 = ei1.getFieldValueObject("value"); + Object v2 = ei2.getFieldValueObject("value"); + if (v1 == v2) return true; + if (v1 == null || v2 == null) return false; + return v1.equals(v2); + } return ei1 == ei2; } diff --git a/src/tests/java17/records/RecordReferenceComponentTest.java b/src/tests/java17/records/RecordReferenceComponentTest.java new file mode 100644 index 00000000..0e3a1fb4 --- /dev/null +++ b/src/tests/java17/records/RecordReferenceComponentTest.java @@ -0,0 +1,160 @@ +package java17.records; + +import gov.nasa.jpf.util.test.TestJPF; +import org.junit.Test; +import static org.junit.Assert.*; + +/** + * Regression tests for GitHub issue #628: + * Record equals/toString/hashCode with reference and array components. + */ +public class RecordReferenceComponentTest extends TestJPF { + + record ArrayRecord(int[] data) {} + record StringRecord(String name, int age) {} + record BoxedRecord(Integer val) {} + record NullableRecord(String s, Integer i) {} + record NestedRecord(StringRecord inner, int x) {} + + static class IdentityClass { + int value; + IdentityClass(int v) { this.value = v; } + } + record IdentityRecord(IdentityClass obj) {} + + @Test + public void testArraySameReference() { + if (verifyNoPropertyViolation()) { + int[] arr = {1, 2, 3}; + ArrayRecord r1 = new ArrayRecord(arr); + ArrayRecord r2 = new ArrayRecord(arr); + assertTrue(r1.equals(r2)); + } + } + + @Test + public void testArrayDifferentReference() { + if (verifyNoPropertyViolation()) { + ArrayRecord r1 = new ArrayRecord(new int[]{1, 2, 3}); + ArrayRecord r2 = new ArrayRecord(new int[]{1, 2, 3}); + assertFalse(r1.equals(r2)); + } + } + + @Test + public void testArrayToStringFormat() { + if (verifyNoPropertyViolation()) { + ArrayRecord r = new ArrayRecord(new int[]{1, 2, 3}); + String s = r.toString(); + assertTrue("should contain [I@", s.contains("[I@")); + } + } + + @Test + public void testStringToString() { + if (verifyNoPropertyViolation()) { + StringRecord p = new StringRecord("alice", 30); + assertEquals("StringRecord[name=alice, age=30]", p.toString()); + } + } + + @Test + public void testStringEquals() { + if (verifyNoPropertyViolation()) { + StringRecord p1 = new StringRecord("alice", 30); + StringRecord p2 = new StringRecord("alice", 30); + assertTrue(p1.equals(p2)); + } + } + + @Test + public void testBoxedIntegerEquals() { + if (verifyNoPropertyViolation()) { + BoxedRecord r1 = new BoxedRecord(Integer.valueOf(1000)); + BoxedRecord r2 = new BoxedRecord(Integer.valueOf(1000)); + assertTrue(r1.equals(r2)); + } + } + + @Test + public void testBoxedIntegerToString() { + if (verifyNoPropertyViolation()) { + BoxedRecord r = new BoxedRecord(42); + assertEquals("BoxedRecord[val=42]", r.toString()); + } + } + + @Test + public void testIdentityClassEquality() { + if (verifyNoPropertyViolation()) { + IdentityClass a = new IdentityClass(99); + IdentityClass b = new IdentityClass(99); + IdentityRecord r1 = new IdentityRecord(a); + IdentityRecord r2 = new IdentityRecord(b); + assertFalse(r1.equals(r2)); + assertTrue(new IdentityRecord(a).equals(new IdentityRecord(a))); + } + } + + @Test + public void testNullComponents() { + if (verifyNoPropertyViolation()) { + NullableRecord r1 = new NullableRecord(null, null); + NullableRecord r2 = new NullableRecord(null, null); + assertTrue(r1.equals(r2)); + } + } + + @Test + public void testNullToString() { + if (verifyNoPropertyViolation()) { + NullableRecord r = new NullableRecord(null, null); + assertEquals("NullableRecord[s=null, i=null]", r.toString()); + } + } + + @Test + public void testNestedRecordEquals() { + if (verifyNoPropertyViolation()) { + NestedRecord r1 = new NestedRecord(new StringRecord("alice", 30), 1); + NestedRecord r2 = new NestedRecord(new StringRecord("alice", 30), 1); + assertTrue(r1.equals(r2)); + } + } + + @Test + public void testNestedRecordToString() { + if (verifyNoPropertyViolation()) { + NestedRecord r = new NestedRecord(new StringRecord("alice", 30), 1); + assertEquals("NestedRecord[inner=StringRecord[name=alice, age=30], x=1]", r.toString()); + } + } + + @Test + public void testHashCodeConsistencyString() { + if (verifyNoPropertyViolation()) { + StringRecord r1 = new StringRecord("alice", 30); + StringRecord r2 = new StringRecord("alice", 30); + assertEquals(r1.hashCode(), r2.hashCode()); + } + } + + @Test + public void testHashCodeConsistencyBoxed() { + if (verifyNoPropertyViolation()) { + BoxedRecord r1 = new BoxedRecord(Integer.valueOf(1000)); + BoxedRecord r2 = new BoxedRecord(Integer.valueOf(1000)); + assertEquals(r1.hashCode(), r2.hashCode()); + } + } + + @Test + public void testHashCodeConsistencyArray() { + if (verifyNoPropertyViolation()) { + int[] arr = {1, 2, 3}; + ArrayRecord r1 = new ArrayRecord(arr); + ArrayRecord r2 = new ArrayRecord(arr); + assertEquals(r1.hashCode(), r2.hashCode()); + } + } +} From 2b80554f50ac886b1e1f95f2d83f9bd5f87555dc Mon Sep 17 00:00:00 2001 From: Darshan R Date: Thu, 13 Aug 2026 02:57:35 +0000 Subject: [PATCH 2/2] fix: hash multidimensional record arrays correctly --- .../nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java | 56 +++++++++++++++++-- .../records/RecordReferenceComponentTest.java | 33 +++++++++++ 2 files changed, 83 insertions(+), 6 deletions(-) diff --git a/src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java b/src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java index 69a7e21c..2c99491e 100644 --- a/src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java +++ b/src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java @@ -426,34 +426,78 @@ private int computeRecordHashCode(ThreadInfo ti, ClassInfo ci) { private int componentHashCode(ThreadInfo ti, Object value, String sig) { if (value == null) return 0; + char typeChar = sig.charAt(0); if (isPrimitiveType(typeChar)) return value.hashCode(); + if (typeChar == '[') { ElementInfo arrayEi = (value instanceof ElementInfo) ? (ElementInfo) value : ti.getHeap().get((Integer) value); - return arrayEi != null ? arrayEi.getObjectRef() : 0; + return arrayHashCode(ti, arrayEi); } + if (value instanceof ElementInfo) { ElementInfo valEi = (ElementInfo) value; ClassInfo valCi = valEi.getClassInfo(); - if ("java.lang.String".equals(valCi.getName())) return valEi.asString().hashCode(); + + if ("java.lang.String".equals(valCi.getName())) { + return valEi.asString().hashCode(); + } + if (valCi.isRecord()) { StackFrame f = ti.getModifiableTopFrame(); int orig = f.getThis(); - f.setThis(valEi.getObjectRef()); - int h = computeRecordHashCode(ti, valCi); - f.setThis(orig); - return h; + try { + f.setThis(valEi.getObjectRef()); + return computeRecordHashCode(ti, valCi); + } finally { + f.setThis(orig); + } } + if (BOXED_TYPES.contains(valCi.getName())) { Object fv = valEi.getFieldValueObject("value"); return fv != null ? fv.hashCode() : 0; } + return valEi.getObjectRef(); } + return value.hashCode(); } + private int arrayHashCode(ThreadInfo ti, ElementInfo arrayEi) { + if (arrayEi == null) return 0; + + String arraySig = arrayEi.getClassInfo().getSignature(); + String componentSig = arraySig.substring(1); + char componentType = componentSig.charAt(0); + + int hash = 1; + + for (int i = 0; i < arrayEi.arrayLength(); i++) { + Object element = getArrayElement(arrayEi, i, componentType); + + int elementHash; + if (element == null) { + elementHash = 0; + } else if (componentType == '[') { + ElementInfo nestedArray = (element instanceof ElementInfo) + ? (ElementInfo) element + : ti.getHeap().get((Integer) element); + elementHash = arrayHashCode(ti, nestedArray); + } else if (isPrimitiveType(componentType)) { + elementHash = element.hashCode(); + } else { + elementHash = componentHashCode(ti, element, componentSig); + } + + hash = 31 * hash + elementHash; + } + + return hash; + } + private int computeRecordToString(ThreadInfo ti, ClassInfo ci) { ElementInfo ei = ti.getThisElementInfo(); String fullName = ci.getName(); diff --git a/src/tests/java17/records/RecordReferenceComponentTest.java b/src/tests/java17/records/RecordReferenceComponentTest.java index 0e3a1fb4..98a87ebd 100644 --- a/src/tests/java17/records/RecordReferenceComponentTest.java +++ b/src/tests/java17/records/RecordReferenceComponentTest.java @@ -15,6 +15,7 @@ record StringRecord(String name, int age) {} record BoxedRecord(Integer val) {} record NullableRecord(String s, Integer i) {} record NestedRecord(StringRecord inner, int x) {} + record LongArrayRecord(long[][] data) {} static class IdentityClass { int value; @@ -157,4 +158,36 @@ public void testHashCodeConsistencyArray() { assertEquals(r1.hashCode(), r2.hashCode()); } } + + @Test + public void testHashCodeDifferentLengthArrays() { + if (verifyNoPropertyViolation()) { + int[] arr2a = {1, 2}; + int[] arr2b = {1, 2}; + int[] arr3 = {1, 2, 3}; + + ArrayRecord r2a = new ArrayRecord(arr2a); + ArrayRecord r2b = new ArrayRecord(arr2b); + ArrayRecord r3 = new ArrayRecord(arr3); + + assertEquals(r2a.hashCode(), r2b.hashCode()); + assertTrue(r2a.hashCode() != r3.hashCode()); + } + } + + @Test + public void testHashCodeHigherDimensionalArray() { + if (verifyNoPropertyViolation()) { + long[][] arr1 = {{1L, 2L}, {3L, 4L}}; + long[][] arr2 = {{1L, 2L}, {3L, 4L}}; + + LongArrayRecord r1 = new LongArrayRecord(arr1); + LongArrayRecord r2 = new LongArrayRecord(arr2); + + assertEquals(r1.hashCode(), r2.hashCode()); + + LongArrayRecord r3 = new LongArrayRecord(arr1); + assertEquals(r1.hashCode(), r3.hashCode()); + } + } }