From 28c066f86c2cd268b8c9b9959161e3d07c6146c6 Mon Sep 17 00:00:00 2001 From: jtoman Date: Fri, 7 Sep 2018 12:34:36 -0700 Subject: [PATCH] Improves annotation support (#161) * Improves annotation support Closes #150. Improves toString to cover all primitive types and annotation attributes. Also adds support for: * Default value reflection * hashCode/equals on annotations * nested annotations * Ignoring missing annotations (which is what the JVM does) * Reverts unrelated format change --- .../gov/nasa/jpf/AnnotationProxyBase.java | 6 + src/classes/java/lang/reflect/Method.java | 4 +- src/main/gov/nasa/jpf/jvm/ClassFile.java | 103 ++- .../gov/nasa/jpf/jvm/ClassFilePrinter.java | 9 +- .../gov/nasa/jpf/jvm/ClassFileReader.java | 2 + .../nasa/jpf/jvm/ClassFileReaderAdapter.java | 3 + .../gov/nasa/jpf/jvm/JVMAnnotationParser.java | 52 +- src/main/gov/nasa/jpf/jvm/JVMClassInfo.java | 116 +++- src/main/gov/nasa/jpf/jvm/SkipAnnotation.java | 5 + src/main/gov/nasa/jpf/vm/MJIEnv.java | 172 +++-- .../JPF_gov_nasa_jpf_AnnotationProxyBase.java | 387 +++++++++-- .../gov/nasa/jpf/vm/JPF_java_lang_Class.java | 6 +- .../gov/nasa/jpf/vm/JPF_java_lang_String.java | 4 + .../jpf/vm/JPF_java_lang_reflect_Method.java | 21 + .../AnnotationDefaultValueReflectionTest.java | 492 ++++++++++++++ .../basic/AnnotationHashCodeEqualsTest.java | 626 ++++++++++++++++++ .../test/vm/basic/AnnotationToStringTest.java | 526 +++++++++++++++ .../vm/basic/MissingAnnotationClassTest.java | 49 ++ 18 files changed, 2456 insertions(+), 127 deletions(-) create mode 100644 src/main/gov/nasa/jpf/jvm/SkipAnnotation.java create mode 100644 src/tests/gov/nasa/jpf/test/vm/basic/AnnotationDefaultValueReflectionTest.java create mode 100644 src/tests/gov/nasa/jpf/test/vm/basic/AnnotationHashCodeEqualsTest.java create mode 100644 src/tests/gov/nasa/jpf/test/vm/basic/AnnotationToStringTest.java create mode 100644 src/tests/gov/nasa/jpf/test/vm/basic/MissingAnnotationClassTest.java diff --git a/src/classes/gov/nasa/jpf/AnnotationProxyBase.java b/src/classes/gov/nasa/jpf/AnnotationProxyBase.java index 43d84e4..72ac986 100644 --- a/src/classes/gov/nasa/jpf/AnnotationProxyBase.java +++ b/src/classes/gov/nasa/jpf/AnnotationProxyBase.java @@ -30,6 +30,12 @@ public class AnnotationProxyBase { @Override public native String toString(); + @Override + public native boolean equals(Object o); + + @Override + public native int hashCode(); + /*** public String toString() { StringBuilder sb = new StringBuilder(); diff --git a/src/classes/java/lang/reflect/Method.java b/src/classes/java/lang/reflect/Method.java index e782d44..40b1888 100644 --- a/src/classes/java/lang/reflect/Method.java +++ b/src/classes/java/lang/reflect/Method.java @@ -65,9 +65,7 @@ public final class Method extends AccessibleObject implements Member { // for Annotations - return the default value of the annotation member // represented by this method - public Object getDefaultValue() { - throw new UnsupportedOperationException("Method.getDefaultValue() not supported yet"); - } + public native Object getDefaultValue(); @Override public native boolean equals (Object obj); diff --git a/src/main/gov/nasa/jpf/jvm/ClassFile.java b/src/main/gov/nasa/jpf/jvm/ClassFile.java index d3dbdb5..4bac2b2 100644 --- a/src/main/gov/nasa/jpf/jvm/ClassFile.java +++ b/src/main/gov/nasa/jpf/jvm/ClassFile.java @@ -18,13 +18,12 @@ package gov.nasa.jpf.jvm; -import gov.nasa.jpf.jvm.JVMByteCodeReader; -import gov.nasa.jpf.vm.ClassParseException; +import java.io.File; + import gov.nasa.jpf.JPFException; import gov.nasa.jpf.util.BailOut; import gov.nasa.jpf.util.BinaryClassSource; - -import java.io.File; +import gov.nasa.jpf.vm.ClassParseException; /** * class to read and dissect Java classfile contents (as specified by the Java VM @@ -692,11 +691,67 @@ public class ClassFile extends BinaryClassSource { reader.setAnnotationCount( this, tag, annotationCount); pos = p; } - private void setAnnotation(ClassFileReader reader, Object tag, int annotationIndex, String annotationType){ + private boolean setAnnotation(ClassFileReader reader, Object tag, int annotationIndex, String annotationType){ int p = pos; - reader.setAnnotation( this, tag, annotationIndex, annotationType); - pos = p; + try { + reader.setAnnotation( this, tag, annotationIndex, annotationType); + pos = p; + return true; + } catch (SkipAnnotation sa) { + this.skipAnnotation(false); + return false; + } + } + + /* + * This is largely lifted from AnnotationParser.java + * annotation { + * u2 type_index; + * u2 num_element_value_pairs; + * { + * u2 element_name_index; + * element_value value; + * } element_value_pairs[num_element_value_pairs] + * } + */ + private void skipAnnotation(boolean skipTypeIndex) { + if(skipTypeIndex) { // we may want to skip after reading the type name + readU2(); + } + int numKV = readU2(); + for(int i = 0; i < numKV; i++) { + readU2(); // skip name + skipMemberValue(); + } + } + + /* + * Skips an element_value + */ + private void skipMemberValue() { + int tag = readUByte(); + switch(tag) { + case 'e': // Enum value + pos += 4; // an enum value is a struct of two shorts, for 4 bytes total + break; + case '@': + skipAnnotation(true); + break; + case '[': + skipArray(); + break; + default: + pos += 2; // either two bye const val index or two byte class info index + } } + + private void skipArray() { + int len = readU2(); + for(int i = 0; i < len; i++) { + skipMemberValue(); + } + } + private void setAnnotationsDone(ClassFileReader reader, Object tag){ int p = pos; reader.setAnnotationsDone(this, tag); @@ -738,6 +793,13 @@ public class ClassFile extends BinaryClassSource { reader.setClassAnnotationValue( this, tag, annotationIndex, valueIndex, elementName, arrayIndex, typeName); pos = p; } + + private void setAnnotationFieldValue(ClassFileReader reader, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex) { + int p = pos; + reader.setAnnotationFieldValue( this, tag, annotationIndex, valueIndex, elementName, arrayIndex); + pos = p; + } + private void setEnumAnnotationValue(ClassFileReader reader, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex, String enumType, String enumValue){ int p = pos; @@ -774,10 +836,17 @@ public class ClassFile extends BinaryClassSource { reader.setParameterAnnotationCount(this, tag, paramIndex, annotationCount); pos = p; } - private void setParameterAnnotation(ClassFileReader reader, Object tag, int annotationIndex, String annotationType){ + + private boolean setParameterAnnotation(ClassFileReader reader, Object tag, int annotationIndex, String annotationType){ int p = pos; - reader.setParameterAnnotation( this, tag, annotationIndex, annotationType); - pos = p; + try { + reader.setParameterAnnotation( this, tag, annotationIndex, annotationType); + pos = p; + return true; + } catch(SkipAnnotation s) { + this.skipAnnotation(false); + return false; + } } private void setParameterAnnotationsDone(ClassFileReader reader, Object tag, int paramIndex){ int p = pos; @@ -1515,7 +1584,8 @@ public class ClassFile extends BinaryClassSource { break; case '@': - parseAnnotation(reader, tag, 0, false); // getting recursive here + parseAnnotation(reader, tag, -1, false); // getting recursive here + setAnnotationFieldValue(reader, tag, annotationIndex, valueIndex, elementName, arrayIndex); break; case '[': @@ -1542,14 +1612,15 @@ public class ClassFile extends BinaryClassSource { void parseAnnotation (ClassFileReader reader, Object tag, int annotationIndex, boolean isParameterAnnotation){ int cpIdx = readU2(); String annotationType = (String)cpValue[cpIdx]; - + boolean parseValues; if (isParameterAnnotation){ - setParameterAnnotation(reader, tag, annotationIndex, annotationType); + parseValues = setParameterAnnotation(reader, tag, annotationIndex, annotationType); } else { - setAnnotation(reader, tag, annotationIndex, annotationType); + parseValues = setAnnotation(reader, tag, annotationIndex, annotationType); + } + if(parseValues) { + parseAnnotationValues(reader, tag, annotationIndex); } - - parseAnnotationValues(reader, tag, annotationIndex); } void parseAnnotationValues (ClassFileReader reader, Object tag, int annotationIndex){ diff --git a/src/main/gov/nasa/jpf/jvm/ClassFilePrinter.java b/src/main/gov/nasa/jpf/jvm/ClassFilePrinter.java index d41cdd9..8b68eb9 100644 --- a/src/main/gov/nasa/jpf/jvm/ClassFilePrinter.java +++ b/src/main/gov/nasa/jpf/jvm/ClassFilePrinter.java @@ -18,10 +18,10 @@ package gov.nasa.jpf.jvm; -import gov.nasa.jpf.jvm.JVMByteCodePrinter; +import java.io.PrintWriter; + import gov.nasa.jpf.util.StructuredPrinter; import gov.nasa.jpf.vm.ClassParseException; -import java.io.PrintWriter; /** * simple tool to print contents of a classfile @@ -777,4 +777,9 @@ public class ClassFilePrinter extends StructuredPrinter implements ClassFileRead pw.print(".."); } } + + @Override + public void setAnnotationFieldValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex) { + + } } diff --git a/src/main/gov/nasa/jpf/jvm/ClassFileReader.java b/src/main/gov/nasa/jpf/jvm/ClassFileReader.java index 6017fad..203537b 100644 --- a/src/main/gov/nasa/jpf/jvm/ClassFileReader.java +++ b/src/main/gov/nasa/jpf/jvm/ClassFileReader.java @@ -167,6 +167,8 @@ public interface ClassFileReader { void setAnnotationValueCount(ClassFile cf, Object tag, int annotationIndex, int nValuePairs); void setPrimitiveAnnotationValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex, Object val); + + void setAnnotationFieldValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex); void setStringAnnotationValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex, String s); diff --git a/src/main/gov/nasa/jpf/jvm/ClassFileReaderAdapter.java b/src/main/gov/nasa/jpf/jvm/ClassFileReaderAdapter.java index 76fe464..4a3c19d 100644 --- a/src/main/gov/nasa/jpf/jvm/ClassFileReaderAdapter.java +++ b/src/main/gov/nasa/jpf/jvm/ClassFileReaderAdapter.java @@ -246,4 +246,7 @@ public class ClassFileReaderAdapter implements ClassFileReader { @Override 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) {} } diff --git a/src/main/gov/nasa/jpf/jvm/JVMAnnotationParser.java b/src/main/gov/nasa/jpf/jvm/JVMAnnotationParser.java index 8acef37..86d93a0 100644 --- a/src/main/gov/nasa/jpf/jvm/JVMAnnotationParser.java +++ b/src/main/gov/nasa/jpf/jvm/JVMAnnotationParser.java @@ -17,6 +17,8 @@ */ package gov.nasa.jpf.jvm; +import java.util.LinkedList; + import gov.nasa.jpf.JPFException; import gov.nasa.jpf.vm.AnnotationInfo; import gov.nasa.jpf.vm.AnnotationParser; @@ -47,6 +49,10 @@ public class JVMAnnotationParser extends ClassFileReaderAdapter implements Annot String annotationName; AnnotationInfo.Entry[] entries; + protected LinkedList annotationStack; + protected AnnotationInfo curAi; + protected LinkedList valuesStack; + public JVMAnnotationParser (ClassFile cf) { this.cf = cf; } @@ -113,28 +119,60 @@ public class JVMAnnotationParser extends ClassFileReaderAdapter implements Annot @Override public void setAnnotation (ClassFile cf, Object tag, int annotationIndex, String annotationType) { - if (annotationType.equals("Ljava/lang/annotation/Inherited;")) { + if (key == null && annotationType.equals("Ljava/lang/annotation/Inherited;")) { ai.setInherited( true); } + if(key != null && annotationIndex == -1) { + if(annotationStack == null) { + assert valuesStack == null; + annotationStack = new LinkedList<>(); + valuesStack = new LinkedList<>(); + } + annotationStack.addFirst(curAi); + valuesStack.addFirst(valElements); + valElements = null; + curAi = ai.getClassLoaderInfo().getResolvedAnnotationInfo(Types.getClassNameFromTypeName(annotationType)); + } } - + + @Override + public void setAnnotationFieldValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex) { + assert annotationStack.size() > 0; + AnnotationInfo ai = curAi; + valElements = valuesStack.pop(); + curAi = annotationStack.pop(); + if(arrayIndex >= 0) { + valElements[arrayIndex] = ai; + } else { + if(curAi != null) { + curAi.setClonedEntryValue(elementName, ai); + } else { + value = ai; + } + } + } + @Override public void setPrimitiveAnnotationValue (ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex, Object val) { if (arrayIndex >= 0) { valElements[arrayIndex] = val; + } else if(curAi != null) { + curAi.setClonedEntryValue(elementName, val); } else { if (key != null){ value = val; } } } - + @Override public void setStringAnnotationValue (ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex, String val) { if (arrayIndex >= 0) { valElements[arrayIndex] = val; + } else if(curAi != null) { + curAi.setClonedEntryValue(elementName, val); } else { if (key != null){ value = val; @@ -148,6 +186,8 @@ public class JVMAnnotationParser extends ClassFileReaderAdapter implements Annot Object val = AnnotationInfo.getClassValue(typeName); if (arrayIndex >= 0) { valElements[arrayIndex] = val; + } else if(curAi != null) { + curAi.setClonedEntryValue(elementName, val); } else { if (key != null){ value = val; @@ -161,6 +201,8 @@ public class JVMAnnotationParser extends ClassFileReaderAdapter implements Annot Object val = AnnotationInfo.getEnumValue(enumType, enumValue); if (arrayIndex >= 0) { valElements[arrayIndex] = val; + } else if(curAi != null) { + curAi.setClonedEntryValue(elementName, val); } else { if (key != null){ value = val; @@ -177,7 +219,9 @@ public class JVMAnnotationParser extends ClassFileReaderAdapter implements Annot @Override public void setAnnotationValueElementsDone (ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName) { - if (key != null) { + if(curAi != null) { + curAi.setClonedEntryValue(elementName, valElements); + } else if (key != null) { value = valElements; } } diff --git a/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java b/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java index 3cd1214..7f3309f 100644 --- a/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java +++ b/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java @@ -18,14 +18,42 @@ 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 @@ -388,8 +416,12 @@ public class JVMClassInfo extends ClassInfo { //--- annotations protected AnnotationInfo[] annotations; protected AnnotationInfo curAi; + protected LinkedList annotationStack; + protected LinkedList valuesStack; protected AnnotationInfo[][] parameterAnnotations; protected Object[] values; + // true if we need to filter null annotations + private boolean compactAnnotationArray = false; //--- declaration annotations @@ -401,16 +433,57 @@ public class JVMClassInfo extends ClassInfo { @Override public void setAnnotation (ClassFile cf, Object tag, int annotationIndex, String annotationType) { if (tag instanceof InfoObject) { - curAi = getResolvedAnnotationInfo(Types.getClassNameFromTypeName(annotationType)); - annotations[annotationIndex] = curAi; + if(annotationIndex == -1) { + if(annotationStack == null) { + assert valuesStack == null; + valuesStack = new LinkedList<>(); + annotationStack = new LinkedList<>(); + } + annotationStack.addFirst(curAi); + valuesStack.addFirst(values); + } + try { + curAi = getResolvedAnnotationInfo(Types.getClassNameFromTypeName(annotationType)); + if(annotationIndex != -1) { + annotations[annotationIndex] = curAi; + } + } catch(ClassInfoException cie) { + // if we can't parse a field, we're sunk, throw and tank the reflective call + if(annotationIndex == -1) { + throw cie; + } + compactAnnotationArray = true; + annotations[annotationIndex] = null; + // skip this annotation + throw new SkipAnnotation(); + } } } @Override public void setAnnotationsDone (ClassFile cf, Object tag) { if (tag instanceof InfoObject) { - ((InfoObject) tag).addAnnotations(annotations); + AnnotationInfo[] toSet; + if(compactAnnotationArray) { + int nAnnot = 0; + for(AnnotationInfo ai : annotations) { + if(ai != null) { + nAnnot++; + } + } + toSet = new AnnotationInfo[nAnnot]; + int idx = 0; + for(AnnotationInfo ai : annotations) { + if(ai != null) { + toSet[idx++] = ai; + } + } + } else { + toSet = annotations; + } + ((InfoObject) tag).addAnnotations(toSet); } + compactAnnotationArray = false; } @Override @@ -426,8 +499,14 @@ public class JVMClassInfo extends ClassInfo { @Override public void setParameterAnnotation (ClassFile cf, Object tag, int annotationIndex, String annotationType) { - curAi = getResolvedAnnotationInfo(Types.getClassNameFromTypeName(annotationType)); - annotations[annotationIndex] = curAi; + try { + curAi = getResolvedAnnotationInfo(Types.getClassNameFromTypeName(annotationType)); + annotations[annotationIndex] = curAi; + } catch(ClassInfoException cie) { + compactAnnotationArray = true; + annotations[annotationIndex] = null; + throw new SkipAnnotation(); + } } @Override @@ -533,7 +612,9 @@ public class JVMClassInfo extends ClassInfo { public void setAnnotationValueCount (ClassFile cf, Object tag, int annotationIndex, int nValuePairs) { // if we have values, we need to clone the defined annotation so that we can overwrite entries curAi = curAi.cloneForOverriddenValues(); - annotations[annotationIndex] = curAi; + if(annotationIndex != -1) { + annotations[annotationIndex] = curAi; + } } @Override @@ -545,6 +626,19 @@ public class JVMClassInfo extends ClassInfo { curAi.setClonedEntryValue(elementName, val); } } + + @Override + public void setAnnotationFieldValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex) { + assert annotationStack.size() > 0; + AnnotationInfo ai = curAi; + values = valuesStack.pop(); + curAi = annotationStack.pop(); + if(arrayIndex >= 0) { + values[arrayIndex] = ai; + } else { + curAi.setClonedEntryValue(elementName, ai); + } + } @Override public void setStringAnnotationValue (ClassFile cf, Object tag, int annotationIndex, int valueIndex, diff --git a/src/main/gov/nasa/jpf/jvm/SkipAnnotation.java b/src/main/gov/nasa/jpf/jvm/SkipAnnotation.java new file mode 100644 index 0000000..5cf4686 --- /dev/null +++ b/src/main/gov/nasa/jpf/jvm/SkipAnnotation.java @@ -0,0 +1,5 @@ +package gov.nasa.jpf.jvm; + +public class SkipAnnotation extends RuntimeException { + +} diff --git a/src/main/gov/nasa/jpf/vm/MJIEnv.java b/src/main/gov/nasa/jpf/vm/MJIEnv.java index a37a941..1558f27 100644 --- a/src/main/gov/nasa/jpf/vm/MJIEnv.java +++ b/src/main/gov/nasa/jpf/vm/MJIEnv.java @@ -17,17 +17,17 @@ */ package gov.nasa.jpf.vm; -import com.sun.org.apache.bcel.internal.generic.InstructionConstants; +import java.util.Date; +import java.util.Locale; +import java.util.Optional; + import gov.nasa.jpf.Config; import gov.nasa.jpf.JPF; import gov.nasa.jpf.JPFException; import gov.nasa.jpf.JPFListener; +import gov.nasa.jpf.vm.AnnotationInfo.EnumValue; import gov.nasa.jpf.vm.serialize.UnknownJPFClass; -import java.util.Date; -import java.util.Locale; - - /** * MJIEnv is the call environment for "native" methods, i.e. code that * is executed by the VM, not by JPF. @@ -1153,7 +1153,6 @@ public class MJIEnv { } } } - return String.format(format,arg); } @@ -1353,7 +1352,7 @@ public class MJIEnv { public void throwException (String clsName) { ClassInfo ciX = ClassInfo.getInitializedClassInfo(clsName, ti); - assert ciX.isInstanceOf("java.lang.Throwable"); + assert ciX.isInstanceOf("java.lang.Throwable") : ciX; exceptionRef = ti.createException(ciX, null, NULL); } @@ -1595,43 +1594,41 @@ public class MJIEnv { ElementInfo ei = getModifiableElementInfo(objref); ei.lockNotified(ti); } - - void initAnnotationProxyField (int proxyRef, FieldInfo fi, Object v) throws ClinitRequired { - String fname = fi.getName(); - String ftype = fi.getType(); - + + public int liftNativeAnnotationValue(String ftype, Object v) { if (v instanceof String){ - setReferenceField(proxyRef, fname, newString((String)v)); + return newString((String)v); } else if (v instanceof Boolean){ - setBooleanField(proxyRef, fname, ((Boolean)v).booleanValue()); - } else if (v instanceof Integer){ - setIntField(proxyRef, fname, ((Integer)v).intValue()); + return valueOfBoolean((Boolean)v); + } else if (v instanceof Integer) { + return valueOfInteger((Integer)v); } else if (v instanceof Long){ - setLongField(proxyRef, fname, ((Long)v).longValue()); + return valueOfLong((Long)v); } else if (v instanceof Float){ - setFloatField(proxyRef, fname, ((Float)v).floatValue()); + return newFloat((Float) v); } else if (v instanceof Short){ - setShortField(proxyRef, fname, ((Short)v).shortValue()); + return valueOfShort((Short)v); } else if (v instanceof Character){ - setCharField(proxyRef, fname, ((Character)v).charValue()); + return valueOfCharacter((Character)v); } else if (v instanceof Byte){ - setByteField(proxyRef, fname, ((Byte)v).byteValue()); + return valueOfByte((Byte)v); } else if (v instanceof Double){ - setDoubleField(proxyRef, fname, ((Double)v).doubleValue()); - - } else if (v instanceof AnnotationInfo.EnumValue){ // an enum constant - AnnotationInfo.EnumValue ev = (AnnotationInfo.EnumValue)v; - String eCls = ev.getEnumClassName(); - String eConst = ev.getEnumConstName(); - - ClassInfo eci = ClassLoaderInfo.getCurrentResolvedClassInfo(eCls); - if (!eci.isInitialized()){ - throw new ClinitRequired(eci); + return newDouble((Double)v); + } else { + Optional ref = liftAnnotationReferenceValue(v, ftype); + if(ref.isPresent()) { + return ref.get(); + } else { + throwException("java.lang.InternalError", "AnnotationElement type not supported: " + ftype); + return -1; } - - StaticElementInfo sei = eci.getStaticElementInfo(); - int eref = sei.getReferenceField(eConst); - setReferenceField(proxyRef, fname, eref); + } + } + + Optional liftAnnotationReferenceValue(Object v, String ftype) { + if (v instanceof AnnotationInfo.EnumValue){ // an enum constant + int eref = makeAnnotationEnumRef((EnumValue) v); + return Optional.of(eref); } else if (v instanceof AnnotationInfo.ClassValue){ // a class String clsName = v.toString(); @@ -1643,7 +1640,7 @@ public class MJIEnv { } int cref = cci.getClassObjectRef(); - setReferenceField(proxyRef, fname, cref); + return Optional.of(cref); } else if (v.getClass().isArray()){ // ..or arrays thereof Object[] a = (Object[])v; @@ -1674,6 +1671,26 @@ public class MJIEnv { for (int i=0; i ref = liftAnnotationReferenceValue(v, ftype); + if(ref.isPresent()) { + setReferenceField(proxyRef, fname, ref.get()); + } else { + throwException("java.lang.InternalError", "AnnotationElement type not supported: " + ftype); + } } } + private int makeAnnotationEnumRef(AnnotationInfo.EnumValue v) { + AnnotationInfo.EnumValue ev = (AnnotationInfo.EnumValue)v; + String eCls = ev.getEnumClassName(); + String eConst = ev.getEnumConstName(); + + ClassInfo eci = ClassLoaderInfo.getCurrentResolvedClassInfo(eCls); + if (!eci.isInitialized()){ + throw new ClinitRequired(eci); + } + + StaticElementInfo sei = eci.getStaticElementInfo(); + int eref = sei.getReferenceField(eConst); + return eref; + } + int newAnnotationProxy (ClassInfo aciProxy, AnnotationInfo ai) throws ClinitRequired { int proxyRef = newObject(aciProxy); @@ -1707,7 +1787,6 @@ public class MJIEnv { Object v = e.getValue(); String fname = e.getKey(); FieldInfo fi = aciProxy.getInstanceField(fname); - initAnnotationProxyField(proxyRef, fi, v); } @@ -1719,10 +1798,7 @@ public class MJIEnv { if ((ai != null) && (ai.length > 0)){ int aref = newObjectArray("Ljava/lang/annotation/Annotation;", ai.length); for (int i=0; i getStringHash(env, ref)); + } else { + return computeObjectArrayHash(env, aArrayRef, (ref) -> hashReferenceValue(env, ref)); + } + } else { + return hashReferenceValue(env, env.getReferenceField(objRef, fi)); + } + } + + /* + * THIS WILL BREAK if the JDK uses a different hashcode from the one here + */ + private int computeObjectArrayHash(MJIEnv env, int arrayRef, IntFunction refHasher) { + int arrayLength1 = env.getArrayLength(arrayRef); + int hash = 1; + for(int j = 0; j < arrayLength1; j++) { + int elem1Ref = env.getReferenceArrayElement(arrayRef, j); + hash = 31 * hash + refHasher.apply(elem1Ref); + } + return hash; + } + + private int getStringHash(MJIEnv env, int strObjRef) { + return JPF_java_lang_String.computeStringHashCode(env, strObjRef); + } + + private int getObjectHash(int ref) { + return ref ^ 0xABCD; + } + + private int hashReferenceValue(MJIEnv env, int elem1Ref) { + ClassInfo aci = env.getClassInfo(elem1Ref); + if(aci.isEnum()) { + return getObjectHash(elem1Ref); + } else { + return annotationHashCode(env, elem1Ref); + } + } + + @MJI + public int hashCode____I(MJIEnv env, int objRef) { + return annotationHashCode(env, objRef); + } + + private void annotationReferenceToString(MJIEnv env, int objref, StringBuilder sb) { ClassInfo ci = env.getClassInfo(objref); String cname = ci.getName(); int idx = cname.lastIndexOf('$'); @@ -62,22 +311,34 @@ public class JPF_gov_nasa_jpf_AnnotationProxyBase extends NativePeer { sb.append(fn); sb.append('='); - if (ft.equals("int")){ + if(ft.equals("int")) { sb.append(env.getIntField(objref,fn)); - } else if (ft.equals("long")){ - sb.append(env.getLongField(objref,fn)); - - } else if (ft.equals("double")){ - sb.append(env.getDoubleField(objref,fn)); + } else if(ft.equals("byte")) { + sb.append(env.getByteField(objref,fn)); - } else if (ft.equals("boolean")){ + } else if(ft.equals("boolean")) { sb.append(env.getBooleanField(objref,fn)); - - } else if (ft.equals("java.lang.String")){ + + } else if(ft.equals("short")) { + sb.append(env.getShortField(objref, fn)); + + } else if(ft.equals("char")) { + sb.append(env.getCharField(objref, fn)); + + } else if(ft.equals("float")) { + sb.append(env.getFloatField(objref, fn)); + + } else if(ft.equals("long")) { + sb.append(env.getLongField(objref, fn)); + + } else if(ft.equals("double")) { + sb.append(env.getDoubleField(objref,fn)); + + } else if(ft.equals("java.lang.String")) { sb.append(env.getStringObject(env.getReferenceField(objref, fn))); - - } else if (ft.equals("java.lang.Class")){ + + } else if(ft.equals("java.lang.Class")) { int cref = env.getReferenceField(objref, fn); if (cref != MJIEnv.NULL){ int nref = env.getReferenceField(cref, "name"); @@ -88,43 +349,68 @@ public class JPF_gov_nasa_jpf_AnnotationProxyBase extends NativePeer { } else { sb.append("class ?"); } - - } else if (ft.endsWith("[]")){ + + } else if(ft.endsWith("[]")) { int ar = env.getReferenceField(objref, fn); int n = env.getArrayLength((ar)); sb.append('['); - - if (ft.equals("java.lang.String[]")){ + + if(ft.equals("int[]")) { for (int j=0; j0) sb.append(','); - sb.append(env.getStringObject(env.getReferenceArrayElement(ar,j))); + sb.append(env.getIntArrayElement(ar,j)); } - - } else if (ft.equals("int[]")){ + + } else if(ft.equals("byte[]")) { for (int j=0; j0) sb.append(','); - sb.append(env.getIntArrayElement(ar,j)); + sb.append(env.getByteArrayElement(ar,j)); + } + + } else if(ft.equals("boolean[]")) { + for (int j=0; j0) sb.append(','); + sb.append(env.getBooleanArrayElement(ar,j)); + } + + } else if(ft.equals("short[]")) { + for (int j=0; j0) sb.append(','); + sb.append(env.getShortArrayElement(ar,j)); + } + + } else if(ft.equals("char[]")) { + for (int j=0; j0) sb.append(','); + sb.append(env.getCharArrayElement(ar,j)); + } + + } else if(ft.equals("float[]")) { + for (int j=0; j0) sb.append(','); + sb.append(env.getFloatArrayElement(ar,j)); } - } else if (ft.equals("long[]")){ + } else if(ft.equals("long[]")) { for (int j=0; j0) sb.append(','); sb.append(env.getLongArrayElement(ar,j)); } - - } else if (ft.equals("double[]")){ + + } else if(ft.equals("double[]")) { for (int j=0; j0) sb.append(','); sb.append(env.getDoubleArrayElement(ar,j)); } - - } else if (ft.equals("boolean[]")){ + + } else if(ft.equals("java.lang.String[]")) { for (int j=0; j0) sb.append(','); - sb.append(env.getBooleanArrayElement(ar,j)); + sb.append(env.getStringObject(env.getReferenceArrayElement(ar,j))); } - } else if (ft.equals("java.lang.Class[]")){ + + } else if(ft.equals("java.lang.Class[]")) { for (int j=0; j0) sb.append(','); @@ -139,30 +425,43 @@ public class JPF_gov_nasa_jpf_AnnotationProxyBase extends NativePeer { sb.append("class ?"); } - } + } + } else { + for(int j=0; j < n; j++) { + if (j>0) sb.append(','); + + int cref = env.getReferenceArrayElement(ar,j); + if (cref != MJIEnv.NULL){ + referenceToString(env, sb, cref); + } else { + sb.append("null"); + } + } } - sb.append(']'); - - } else { // arbitrary type name, must be a reference + sb.append("]"); + } else { int eref = env.getReferenceField(objref, fn); if (eref != MJIEnv.NULL){ - ClassInfo eci = env.getClassInfo(eref); - if (eci.isEnum()){ - int nref = env.getReferenceField(eref, "name"); - String en = env.getStringObject(nref); - - sb.append(eci.getName()); - sb.append('.'); - sb.append(en); - } + referenceToString(env, sb, eref); } } } sb.append(')'); } - - - return env.newString(sb.toString()); + } + + private void referenceToString(MJIEnv env, StringBuilder sb, int eref) { + ClassInfo eci = env.getClassInfo(eref); + if (eci.isEnum()){ + int nref = env.getReferenceField(eref, "name"); + String en = env.getStringObject(nref); + + sb.append(eci.getName()); + sb.append('.'); + sb.append(en); + } else { + annotationReferenceToString(env, eref, sb); + } } } diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java index 90a5dcf..c76ecb8 100644 --- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java +++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java @@ -17,15 +17,15 @@ */ package gov.nasa.jpf.vm; -import gov.nasa.jpf.Config; -import gov.nasa.jpf.annotation.MJI; - import java.io.IOException; import java.io.InputStream; import java.util.ArrayList; import java.util.HashMap; import java.util.Set; +import gov.nasa.jpf.Config; +import gov.nasa.jpf.annotation.MJI; + /** * MJI NativePeer class for java.lang.Class library abstraction diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java index ba84851..34a2579 100644 --- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java +++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java @@ -272,6 +272,10 @@ public class JPF_java_lang_String extends NativePeer { @MJI public int hashCode____I (MJIEnv env, int objref) { + return computeStringHashCode(env, objref); + } + + public static int computeStringHashCode(MJIEnv env, int objref) { ElementInfo ei = env.getElementInfo(objref); int h = ei.getIntField("hash"); diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java index 66b564e..8d13a0c 100644 --- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java +++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java @@ -146,6 +146,27 @@ public class JPF_java_lang_reflect_Method extends NativePeer { return getExceptionTypes(env, getMethodInfo(env, objRef)); } + @MJI + public int getDefaultValue____Ljava_lang_Object_2(MJIEnv env, int objRef) { + MethodInfo mi = getMethodInfo(env, objRef); + ClassInfo ci = mi.getClassInfo(); + if(!ci.isInterface() || ci.getDirectInterfaceNames() == null || ci.getDirectInterfaceNames().length != 1 || !ci.getDirectInterfaceNames()[0].equals("java.lang.annotation.Annotation")) { + return MJIEnv.NULL; + } + String annotationName = ci.getName(); + AnnotationInfo ai = ci.getClassLoaderInfo().getResolvedAnnotationInfo(annotationName); + Object o = ai.getValue(mi.getName()); + if(o == null) { + return MJIEnv.NULL; + } + try { + return env.liftNativeAnnotationValue(Types.getTypeName(mi.getReturnType()), o); + } catch(ClinitRequired e) { + env.handleClinitRequest(e.getRequiredClassInfo()); + return -1; + } + } + @MJI public int getReturnType____Ljava_lang_Class_2 (MJIEnv env, int objRef){ MethodInfo mi = getMethodInfo(env, objRef); diff --git a/src/tests/gov/nasa/jpf/test/vm/basic/AnnotationDefaultValueReflectionTest.java b/src/tests/gov/nasa/jpf/test/vm/basic/AnnotationDefaultValueReflectionTest.java new file mode 100644 index 0000000..eec9e89 --- /dev/null +++ b/src/tests/gov/nasa/jpf/test/vm/basic/AnnotationDefaultValueReflectionTest.java @@ -0,0 +1,492 @@ +package gov.nasa.jpf.test.vm.basic; + +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.reflect.Method; +import java.util.Arrays; +import java.util.Objects; + +import org.junit.Test; + +import gov.nasa.jpf.test.vm.basic.AnnotationToStringTest.EnumConsts; +import gov.nasa.jpf.util.test.TestJPF; + +public class AnnotationDefaultValueReflectionTest extends TestJPF { + public class NotAnAnnotation { + public void method() { + + } + } + + @Test + public void testNoDefaultValue() throws NoSuchMethodException, SecurityException { + Method m = NotAnAnnotation.class.getDeclaredMethod("method"); + assertNull(m.getDefaultValue()); + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A0 { + boolean f1() default true; + + boolean f2(); + } + + @Test + public void testBooleanAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A0.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + boolean expected = true; + Object defaultValue = f1.getDefaultValue(); + assertTrue(expected == (boolean) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A1 { + boolean[] f1() default { true, false }; + + boolean[] f2(); + } + + @Test + public void testBooleanArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A1.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + boolean[] expected = { true, false }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (boolean[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A2 { + byte f1() default 2; + + byte f2(); + } + + @Test + public void testByteAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A2.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + byte expected = 2; + Object defaultValue = f1.getDefaultValue(); + assertTrue(expected == (byte) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A3 { + byte[] f1() default { 2, 3 }; + + byte[] f2(); + } + + @Test + public void testByteArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A3.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + byte[] expected = { 2, 3 }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (byte[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A4 { + char f1() default 'a'; + + char f2(); + } + + @Test + public void testCharAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A4.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + char expected = 'a'; + Object defaultValue = f1.getDefaultValue(); + assertTrue(expected == (char) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A5 { + char[] f1() default { 'a', 'b' }; + + char[] f2(); + } + + @Test + public void testCharArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A5.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + char[] expected = { 'a', 'b' }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (char[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A6 { + short f1() default 0; + + short f2(); + } + + @Test + public void testShortAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A6.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + short expected = 0; + Object defaultValue = f1.getDefaultValue(); + assertTrue(expected == (short) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A7 { + short[] f1() default { 0, 1 }; + + short[] f2(); + } + + @Test + public void testShortArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A7.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + short[] expected = { 0, 1 }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (short[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A8 { + int f1() default 4; + + int f2(); + } + + @Test + public void testIntAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A8.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + int expected = 4; + Object defaultValue = f1.getDefaultValue(); + assertTrue(expected == (int) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A9 { + int[] f1() default { 4, 5 }; + + int[] f2(); + } + + @Test + public void testIntArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A9.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + int[] expected = { 4, 5 }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (int[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A10 { + long f1() default 9L; + + long f2(); + } + + @Test + public void testLongAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A10.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + long expected = 9L; + Object defaultValue = f1.getDefaultValue(); + assertTrue(expected == (long) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A11 { + long[] f1() default { 9L, 10L }; + + long[] f2(); + } + + @Test + public void testLongArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A11.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + long[] expected = { 9L, 10L }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (long[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A12 { + float f1() default 0.5f; + + float f2(); + } + + @Test + public void testFloatAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A12.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + float expected = 0.5f; + Object defaultValue = f1.getDefaultValue(); + assertTrue(expected == (float) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A13 { + float[] f1() default { 0.5f, 2.0f }; + + float[] f2(); + } + + @Test + public void testFloatArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A13.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + float[] expected = { 0.5f, 2.0f }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (float[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A14 { + double f1() default 2.0; + + double f2(); + } + + @Test + public void testDoubleAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A14.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + double expected = 2.0; + Object defaultValue = f1.getDefaultValue(); + assertTrue(expected == (double) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A15 { + double[] f1() default { 2.0, 3.5 }; + + double[] f2(); + } + + @Test + public void testDoubleArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A15.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + double[] expected = { 2.0, 3.5 }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (double[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A16 { + String f1() default "Hello"; + + String f2(); + } + + @Test + public void testStringAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A16.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + String expected = "Hello"; + Object defaultValue = f1.getDefaultValue(); + assertEquals(expected, (String) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A17 { + String[] f1() default { "Hello", "World" }; + + String[] f2(); + } + + @Test + public void testStringArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A17.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + String[] expected = { "Hello", "World" }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (String[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A18 { + Class f1() default String.class; + + Class f2(); + } + + @Test + public void testClassAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A18.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + Class expected = String.class; + Object defaultValue = f1.getDefaultValue(); + assertEquals(expected, (Class) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A19 { + Class[] f1() default { String.class, Integer.class }; + + Class[] f2(); + } + + @Test + public void testClassArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A19.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + Class[] expected = { String.class, Integer.class }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (Class[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A20 { + EnumConsts f1() default EnumConsts.FIRST; + + EnumConsts f2(); + } + + @Test + public void testEnumConstsAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A20.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + EnumConsts expected = EnumConsts.FIRST; + Object defaultValue = f1.getDefaultValue(); + assertEquals(expected, (EnumConsts) defaultValue); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A21 { + EnumConsts[] f1() default { EnumConsts.FIRST, EnumConsts.SECOND }; + + EnumConsts[] f2(); + } + + @Test + public void testEnumConstsArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A21.class; + Method f1 = klass.getDeclaredMethod("f1"); + Method f2 = klass.getDeclaredMethod("f2"); + assertNull(f2.getDefaultValue()); + EnumConsts[] expected = { EnumConsts.FIRST, EnumConsts.SECOND }; + Object defaultValue = f1.getDefaultValue(); + assertTrue(Arrays.equals(expected, (EnumConsts[]) defaultValue)); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface Nested { + A0 f1() default @A0(f2 = true); + A16 f2(); + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A22 { + Nested f1() default @Nested(f2 = @A16(f1 = "Hello", f2 = "World")); + } + + @Nested(f2 = @A16(f1 = "Hello", f2 = "World")) + public static class Holder { + } + + @Test + public void testAnnotationAttributeDefaultValue() throws NoSuchMethodException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = A22.class; + Method f1 = klass.getDeclaredMethod("f1"); + Nested expected = Holder.class.getAnnotation(Nested.class); + Object defaultValue = f1.getDefaultValue(); + assertEquals(expected, defaultValue); + } + } +} diff --git a/src/tests/gov/nasa/jpf/test/vm/basic/AnnotationHashCodeEqualsTest.java b/src/tests/gov/nasa/jpf/test/vm/basic/AnnotationHashCodeEqualsTest.java new file mode 100644 index 0000000..484ddb0 --- /dev/null +++ b/src/tests/gov/nasa/jpf/test/vm/basic/AnnotationHashCodeEqualsTest.java @@ -0,0 +1,626 @@ +package gov.nasa.jpf.test.vm.basic; + +import org.junit.Test; + +import gov.nasa.jpf.test.vm.basic.AnnotationToStringTest.*; +import gov.nasa.jpf.util.test.TestJPF; + +public class AnnotationHashCodeEqualsTest extends TestJPF { + public class C0 { + @A0(f1 = true, f2 = false) + public int f1; + + @A0(f1 = true, f2 = false) + public int f2; + + @A0(f1 = false, f2 = true) + public int f3; + } + + @Test + public void testBooleanAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C0.class; + A0 a = klass.getDeclaredField("f1").getAnnotation(A0.class); + A0 b = klass.getDeclaredField("f2").getAnnotation(A0.class); + A0 c = klass.getDeclaredField("f3").getAnnotation(A0.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C1 { + @A1(f1 = { true, false }, f2 = { false, true }) + public int f1; + + @A1(f1 = { true, false }, f2 = { false, true }) + public int f2; + + @A1(f1 = { false, true }, f2 = { true, false }) + public int f3; + } + + @Test + public void testBooleanArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C1.class; + A1 a = klass.getDeclaredField("f1").getAnnotation(A1.class); + A1 b = klass.getDeclaredField("f2").getAnnotation(A1.class); + A1 c = klass.getDeclaredField("f3").getAnnotation(A1.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C2 { + @A2(f1 = 2, f2 = 3) + public int f1; + + @A2(f1 = 2, f2 = 3) + public int f2; + + @A2(f1 = 3, f2 = 2) + public int f3; + } + + @Test + public void testByteAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C2.class; + A2 a = klass.getDeclaredField("f1").getAnnotation(A2.class); + A2 b = klass.getDeclaredField("f2").getAnnotation(A2.class); + A2 c = klass.getDeclaredField("f3").getAnnotation(A2.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C3 { + @A3(f1 = { 2, 3 }, f2 = { 3, 2 }) + public int f1; + + @A3(f1 = { 2, 3 }, f2 = { 3, 2 }) + public int f2; + + @A3(f1 = { 3, 2 }, f2 = { 2, 3 }) + public int f3; + } + + @Test + public void testByteArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C3.class; + A3 a = klass.getDeclaredField("f1").getAnnotation(A3.class); + A3 b = klass.getDeclaredField("f2").getAnnotation(A3.class); + A3 c = klass.getDeclaredField("f3").getAnnotation(A3.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C4 { + @A4(f1 = 'a', f2 = 'b') + public int f1; + + @A4(f1 = 'a', f2 = 'b') + public int f2; + + @A4(f1 = 'b', f2 = 'a') + public int f3; + } + + @Test + public void testCharAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C4.class; + A4 a = klass.getDeclaredField("f1").getAnnotation(A4.class); + A4 b = klass.getDeclaredField("f2").getAnnotation(A4.class); + A4 c = klass.getDeclaredField("f3").getAnnotation(A4.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C5 { + @A5(f1 = { 'a', 'b' }, f2 = { 'b', 'a' }) + public int f1; + + @A5(f1 = { 'a', 'b' }, f2 = { 'b', 'a' }) + public int f2; + + @A5(f1 = { 'b', 'a' }, f2 = { 'a', 'b' }) + public int f3; + } + + @Test + public void testCharArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C5.class; + A5 a = klass.getDeclaredField("f1").getAnnotation(A5.class); + A5 b = klass.getDeclaredField("f2").getAnnotation(A5.class); + A5 c = klass.getDeclaredField("f3").getAnnotation(A5.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C6 { + @A6(f1 = 0, f2 = 1) + public int f1; + + @A6(f1 = 0, f2 = 1) + public int f2; + + @A6(f1 = 1, f2 = 0) + public int f3; + } + + @Test + public void testShortAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C6.class; + A6 a = klass.getDeclaredField("f1").getAnnotation(A6.class); + A6 b = klass.getDeclaredField("f2").getAnnotation(A6.class); + A6 c = klass.getDeclaredField("f3").getAnnotation(A6.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C7 { + @A7(f1 = { 0, 1 }, f2 = { 1, 0 }) + public int f1; + + @A7(f1 = { 0, 1 }, f2 = { 1, 0 }) + public int f2; + + @A7(f1 = { 1, 0 }, f2 = { 0, 1 }) + public int f3; + } + + @Test + public void testShortArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C7.class; + A7 a = klass.getDeclaredField("f1").getAnnotation(A7.class); + A7 b = klass.getDeclaredField("f2").getAnnotation(A7.class); + A7 c = klass.getDeclaredField("f3").getAnnotation(A7.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C8 { + @A8(f1 = 4, f2 = 5) + public int f1; + + @A8(f1 = 4, f2 = 5) + public int f2; + + @A8(f1 = 5, f2 = 4) + public int f3; + } + + @Test + public void testIntAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C8.class; + A8 a = klass.getDeclaredField("f1").getAnnotation(A8.class); + A8 b = klass.getDeclaredField("f2").getAnnotation(A8.class); + A8 c = klass.getDeclaredField("f3").getAnnotation(A8.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C9 { + @A9(f1 = { 4, 5 }, f2 = { 5, 4 }) + public int f1; + + @A9(f1 = { 4, 5 }, f2 = { 5, 4 }) + public int f2; + + @A9(f1 = { 5, 4 }, f2 = { 4, 5 }) + public int f3; + } + + @Test + public void testIntArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C9.class; + A9 a = klass.getDeclaredField("f1").getAnnotation(A9.class); + A9 b = klass.getDeclaredField("f2").getAnnotation(A9.class); + A9 c = klass.getDeclaredField("f3").getAnnotation(A9.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C10 { + @A10(f1 = 9L, f2 = 10L) + public int f1; + + @A10(f1 = 9L, f2 = 10L) + public int f2; + + @A10(f1 = 10L, f2 = 9L) + public int f3; + } + + @Test + public void testLongAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C10.class; + A10 a = klass.getDeclaredField("f1").getAnnotation(A10.class); + A10 b = klass.getDeclaredField("f2").getAnnotation(A10.class); + A10 c = klass.getDeclaredField("f3").getAnnotation(A10.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C11 { + @A11(f1 = { 9L, 10L }, f2 = { 10L, 9L }) + public int f1; + + @A11(f1 = { 9L, 10L }, f2 = { 10L, 9L }) + public int f2; + + @A11(f1 = { 10L, 9L }, f2 = { 9L, 10L }) + public int f3; + } + + @Test + public void testLongArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C11.class; + A11 a = klass.getDeclaredField("f1").getAnnotation(A11.class); + A11 b = klass.getDeclaredField("f2").getAnnotation(A11.class); + A11 c = klass.getDeclaredField("f3").getAnnotation(A11.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C12 { + @A12(f1 = 0.5f, f2 = 2.0f) + public int f1; + + @A12(f1 = 0.5f, f2 = 2.0f) + public int f2; + + @A12(f1 = 2.0f, f2 = 0.5f) + public int f3; + } + + @Test + public void testFloatAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C12.class; + A12 a = klass.getDeclaredField("f1").getAnnotation(A12.class); + A12 b = klass.getDeclaredField("f2").getAnnotation(A12.class); + A12 c = klass.getDeclaredField("f3").getAnnotation(A12.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C13 { + @A13(f1 = { 0.5f, 2.0f }, f2 = { 2.0f, 0.5f }) + public int f1; + + @A13(f1 = { 0.5f, 2.0f }, f2 = { 2.0f, 0.5f }) + public int f2; + + @A13(f1 = { 2.0f, 0.5f }, f2 = { 0.5f, 2.0f }) + public int f3; + } + + @Test + public void testFloatArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C13.class; + A13 a = klass.getDeclaredField("f1").getAnnotation(A13.class); + A13 b = klass.getDeclaredField("f2").getAnnotation(A13.class); + A13 c = klass.getDeclaredField("f3").getAnnotation(A13.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C14 { + @A14(f1 = 2.0, f2 = 3.5) + public int f1; + + @A14(f1 = 2.0, f2 = 3.5) + public int f2; + + @A14(f1 = 3.5, f2 = 2.0) + public int f3; + } + + @Test + public void testDoubleAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C14.class; + A14 a = klass.getDeclaredField("f1").getAnnotation(A14.class); + A14 b = klass.getDeclaredField("f2").getAnnotation(A14.class); + A14 c = klass.getDeclaredField("f3").getAnnotation(A14.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C15 { + @A15(f1 = { 2.0, 3.5 }, f2 = { 3.5, 2.0 }) + public int f1; + + @A15(f1 = { 2.0, 3.5 }, f2 = { 3.5, 2.0 }) + public int f2; + + @A15(f1 = { 3.5, 2.0 }, f2 = { 2.0, 3.5 }) + public int f3; + } + + @Test + public void testDoubleArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C15.class; + A15 a = klass.getDeclaredField("f1").getAnnotation(A15.class); + A15 b = klass.getDeclaredField("f2").getAnnotation(A15.class); + A15 c = klass.getDeclaredField("f3").getAnnotation(A15.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C16 { + @A16(f1 = "Hello", f2 = "World") + public int f1; + + @A16(f1 = "Hello", f2 = "World") + public int f2; + + @A16(f1 = "World", f2 = "Hello") + public int f3; + } + + @Test + public void testStringAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C16.class; + A16 a = klass.getDeclaredField("f1").getAnnotation(A16.class); + A16 b = klass.getDeclaredField("f2").getAnnotation(A16.class); + A16 c = klass.getDeclaredField("f3").getAnnotation(A16.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C17 { + @A17(f1 = { "Hello", "World" }, f2 = { "World", "Hello" }) + public int f1; + + @A17(f1 = { "Hello", "World" }, f2 = { "World", "Hello" }) + public int f2; + + @A17(f1 = { "World", "Hello" }, f2 = { "Hello", "World" }) + public int f3; + } + + @Test + public void testStringArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C17.class; + A17 a = klass.getDeclaredField("f1").getAnnotation(A17.class); + A17 b = klass.getDeclaredField("f2").getAnnotation(A17.class); + A17 c = klass.getDeclaredField("f3").getAnnotation(A17.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C18 { + @A18(f1 = String.class, f2 = Integer.class) + public int f1; + + @A18(f1 = String.class, f2 = Integer.class) + public int f2; + + @A18(f1 = Integer.class, f2 = String.class) + public int f3; + } + + @Test + public void testClassAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C18.class; + A18 a = klass.getDeclaredField("f1").getAnnotation(A18.class); + A18 b = klass.getDeclaredField("f2").getAnnotation(A18.class); + A18 c = klass.getDeclaredField("f3").getAnnotation(A18.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C19 { + @A19(f1 = { String.class, Integer.class }, f2 = { Integer.class, String.class }) + public int f1; + + @A19(f1 = { String.class, Integer.class }, f2 = { Integer.class, String.class }) + public int f2; + + @A19(f1 = { Integer.class, String.class }, f2 = { String.class, Integer.class }) + public int f3; + } + + @Test + public void testClassArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C19.class; + A19 a = klass.getDeclaredField("f1").getAnnotation(A19.class); + A19 b = klass.getDeclaredField("f2").getAnnotation(A19.class); + A19 c = klass.getDeclaredField("f3").getAnnotation(A19.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C20 { + @A20(f1 = EnumConsts.FIRST, f2 = EnumConsts.SECOND) + public int f1; + + @A20(f1 = EnumConsts.FIRST, f2 = EnumConsts.SECOND) + public int f2; + + @A20(f1 = EnumConsts.SECOND, f2 = EnumConsts.FIRST) + public int f3; + } + + @Test + public void testEnumConstsAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C20.class; + A20 a = klass.getDeclaredField("f1").getAnnotation(A20.class); + A20 b = klass.getDeclaredField("f2").getAnnotation(A20.class); + A20 c = klass.getDeclaredField("f3").getAnnotation(A20.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C21 { + @A21(f1 = { EnumConsts.FIRST, EnumConsts.SECOND }, f2 = { EnumConsts.SECOND, EnumConsts.FIRST }) + public int f1; + + @A21(f1 = { EnumConsts.FIRST, EnumConsts.SECOND }, f2 = { EnumConsts.SECOND, EnumConsts.FIRST }) + public int f2; + + @A21(f1 = { EnumConsts.SECOND, EnumConsts.FIRST }, f2 = { EnumConsts.FIRST, EnumConsts.SECOND }) + public int f3; + } + + @Test + public void testEnumConstsArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C21.class; + A21 a = klass.getDeclaredField("f1").getAnnotation(A21.class); + A21 b = klass.getDeclaredField("f2").getAnnotation(A21.class); + A21 c = klass.getDeclaredField("f3").getAnnotation(A21.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C22 { + @A22(f1 = @Nested1(fields = @A16(f1 = "Hello", f2 = "World")), f2 = @Nested2(fields = @A1(f1 = false, f2 = false))) + public int f1; + + @A22(f1 = @Nested1(fields = @A16(f1 = "Hello", f2 = "World")), f2 = @Nested2(fields = @A1(f1 = false, f2 = false))) + public int f2; + + @A22(f1 = @Nested1(fields = @A16(f1 = "Hola", f2 = "Mundo")), f2 = @Nested2(fields = @A1(f1 = true, f2 = true))) + public int f3; + } + + @Test + public void testAnnotationAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C22.class; + A22 a = klass.getDeclaredField("f1").getAnnotation(A22.class); + A22 b = klass.getDeclaredField("f2").getAnnotation(A22.class); + A22 c = klass.getDeclaredField("f3").getAnnotation(A22.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + + public class C23 { + @A23(f1 = { + @Nested1(fields = @A16(f1 = "Hello", f2 = "World")), + @Nested1(fields = @A16(f1 = "Bonjour", f2 = "Monde")) + }, f2 = { + @Nested2(fields = @A1(f1 = false, f2 = false)), + @Nested2(fields = @A1(f1 = true, f2 = true)) + }) + public int f1; + + @A23(f1 = { + @Nested1(fields = @A16(f1 = "Hello", f2 = "World")), + @Nested1(fields = @A16(f1 = "Bonjour", f2 = "Monde")) + }, f2 = { + @Nested2(fields = @A1(f1 = false, f2 = false)), + @Nested2(fields = @A1(f1 = true, f2 = true)) + }) + public int f2; + + @A23(f1 = { + @Nested1(fields = @A16(f1 = "Hola", f2 = "Mundo")), + @Nested1(fields = @A16(f1 = "Bonjour", f2 = "Monde")) + }, f2 = { + @Nested2(fields = @A1(f1 = false, f2 = true)), + @Nested2(fields = @A1(f1 = true, f2 = false)) + }) public int f3; + } + + @Test + public void testAnnotationArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException { + if(verifyNoPropertyViolation()) { + Class klass = C23.class; + A23 a = klass.getDeclaredField("f1").getAnnotation(A23.class); + A23 b = klass.getDeclaredField("f2").getAnnotation(A23.class); + A23 c = klass.getDeclaredField("f3").getAnnotation(A23.class); + assertEquals(a, b); + assertEquals(a.hashCode(), b.hashCode()); + assertFalse(c.equals(b)); + assertFalse(c.equals(a)); + } + } + +} diff --git a/src/tests/gov/nasa/jpf/test/vm/basic/AnnotationToStringTest.java b/src/tests/gov/nasa/jpf/test/vm/basic/AnnotationToStringTest.java new file mode 100644 index 0000000..2dbec23 --- /dev/null +++ b/src/tests/gov/nasa/jpf/test/vm/basic/AnnotationToStringTest.java @@ -0,0 +1,526 @@ +package gov.nasa.jpf.test.vm.basic; + +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; + +import org.junit.Test; + +import gov.nasa.jpf.util.test.TestJPF; + +public class AnnotationToStringTest extends TestJPF { + private static final String TTFF_NESTED = "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$Nested2(" + + "fields=@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A1(f1=[false,false],f2=[true,true]))"; + private static final String HELLO_WORLD_NESTED = "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$Nested1(" + + "fields=@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A16(f1=Hello,f2=World))"; + + + public static enum EnumConsts { + FIRST, SECOND + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A0 { + boolean f1(); + + boolean f2(); + } + + @A0(f1 = true, f2 = false) + public class C0 { + } + + @Test + public void testBooleanAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C0.class; + A0 a = klass.getAnnotation(A0.class); + System.out.println(a.toString()); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A0(f1=true,f2=false)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A1 { + boolean[] f1(); + + boolean[] f2(); + } + + @A1(f1 = { true, false }, f2 = { false, true }) + public class C1 { + } + + @Test + public void testBooleanArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C1.class; + A1 a = klass.getAnnotation(A1.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A1(f1=[true,false],f2=[false,true])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A2 { + byte f1(); + + byte f2(); + } + + @A2(f1 = 0, f2 = 1) + public class C2 { + } + + @Test + public void testByteAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C2.class; + A2 a = klass.getAnnotation(A2.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A2(f1=0,f2=1)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A3 { + byte[] f1(); + + byte[] f2(); + } + + @A3(f1 = { 0, 1 }, f2 = { 1, 0 }) + public class C3 { + } + + @Test + public void testByteArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C3.class; + A3 a = klass.getAnnotation(A3.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A3(f1=[0,1],f2=[1,0])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A4 { + char f1(); + + char f2(); + } + + @A4(f1 = 'a', f2 = 'b') + public class C4 { + } + + @Test + public void testCharAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C4.class; + A4 a = klass.getAnnotation(A4.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A4(f1=a,f2=b)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A5 { + char[] f1(); + + char[] f2(); + } + + @A5(f1 = { 'a', 'b' }, f2 = { 'b', 'a' }) + public class C5 { + } + + @Test + public void testCharArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C5.class; + A5 a = klass.getAnnotation(A5.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A5(f1=[a,b],f2=[b,a])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A6 { + short f1(); + + short f2(); + } + + @A6(f1 = 0, f2 = 1) + public class C6 { + } + + @Test + public void testShortAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C6.class; + A6 a = klass.getAnnotation(A6.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A6(f1=0,f2=1)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A7 { + short[] f1(); + + short[] f2(); + } + + @A7(f1 = { 0, 1 }, f2 = { 1, 0 }) + public class C7 { + } + + @Test + public void testShortArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C7.class; + A7 a = klass.getAnnotation(A7.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A7(f1=[0,1],f2=[1,0])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A8 { + int f1(); + + int f2(); + } + + @A8(f1 = 0, f2 = 1) + public class C8 { + } + + @Test + public void testIntAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C8.class; + A8 a = klass.getAnnotation(A8.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A8(f1=0,f2=1)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A9 { + int[] f1(); + + int[] f2(); + } + + @A9(f1 = { 0, 1 }, f2 = { 1, 0 }) + public class C9 { + } + + @Test + public void testIntArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C9.class; + A9 a = klass.getAnnotation(A9.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A9(f1=[0,1],f2=[1,0])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A10 { + long f1(); + + long f2(); + } + + @A10(f1 = 1L, f2 = 10L) + public class C10 { + } + + @Test + public void testLongAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C10.class; + A10 a = klass.getAnnotation(A10.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A10(f1=1,f2=10)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A11 { + long[] f1(); + + long[] f2(); + } + + @A11(f1 = { 1L, 10L }, f2 = { 10L, 1L }) + public class C11 { + } + + @Test + public void testLongArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C11.class; + A11 a = klass.getAnnotation(A11.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A11(f1=[1,10],f2=[10,1])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A12 { + float f1(); + + float f2(); + } + + @A12(f1 = 0.5f, f2 = 2.0f) + public class C12 { + } + + @Test + public void testFloatAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C12.class; + A12 a = klass.getAnnotation(A12.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A12(f1=0.5,f2=2.0)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A13 { + float[] f1(); + + float[] f2(); + } + + @A13(f1 = { 0.5f, 2.0f }, f2 = { 2.0f, 0.5f }) + public class C13 { + } + + @Test + public void testFloatArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C13.class; + A13 a = klass.getAnnotation(A13.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A13(f1=[0.5,2.0],f2=[2.0,0.5])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A14 { + double f1(); + + double f2(); + } + + @A14(f1 = 2.0, f2 = 3.5) + public class C14 { + } + + @Test + public void testDoubleAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C14.class; + A14 a = klass.getAnnotation(A14.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A14(f1=2.0,f2=3.5)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A15 { + double[] f1(); + + double[] f2(); + } + + @A15(f1 = { 2.0, 3.5 }, f2 = { 3.5, 2.0 }) + public class C15 { + } + + @Test + public void testDoubleArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C15.class; + A15 a = klass.getAnnotation(A15.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A15(f1=[2.0,3.5],f2=[3.5,2.0])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A16 { + String f1(); + + String f2(); + } + + @A16(f1 = "Hello", f2 = "World") + public class C16 { + } + + @Test + public void testStringAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C16.class; + A16 a = klass.getAnnotation(A16.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A16(f1=Hello,f2=World)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A17 { + String[] f1(); + + String[] f2(); + } + + @A17(f1 = { "Hello", "World" }, f2 = { "World", "Hello" }) + public class C17 { + } + + @Test + public void testStringArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C17.class; + A17 a = klass.getAnnotation(A17.class); + System.out.println(a.toString()); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A17(f1=[Hello,World],f2=[World,Hello])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A18 { + Class f1(); + + Class f2(); + } + + @A18(f1 = String.class, f2 = Integer.class) + public class C18 { + } + + @Test + public void testClassAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C18.class; + A18 a = klass.getAnnotation(A18.class); + System.out.println(a.toString()); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A18(f1=class java.lang.String,f2=class java.lang.Integer)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A19 { + Class[] f1(); + + Class[] f2(); + } + + @A19(f1 = { String.class, Integer.class }, f2 = { Integer.class, String.class }) + public class C19 { + } + + @Test + public void testClassArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C19.class; + A19 a = klass.getAnnotation(A19.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A19(f1=[class java.lang.String,class java.lang.Integer]," + + "f2=[class java.lang.Integer,class java.lang.String])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A20 { + EnumConsts f1(); + + EnumConsts f2(); + } + + @A20(f1 = EnumConsts.FIRST, f2 = EnumConsts.SECOND) + public class C20 { + } + + @Test + public void testEnumConstsAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C20.class; + A20 a = klass.getAnnotation(A20.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A20(f1=gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.FIRST," + + "f2=gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.SECOND)"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A21 { + EnumConsts[] f1(); + + EnumConsts[] f2(); + } + + @A21(f1 = { EnumConsts.FIRST, EnumConsts.SECOND }, f2 = { EnumConsts.SECOND, EnumConsts.FIRST }) + public class C21 { + } + + @Test + public void testEnumConstsArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C21.class; + A21 a = klass.getAnnotation(A21.class); + assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A21(" + + "f1=[gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.FIRST,gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.SECOND]," + + "f2=[gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.SECOND,gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.FIRST])"); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface Nested1 { + A16 fields(); + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface Nested2 { + A1 fields(); + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A22 { + Nested1 f1(); + Nested2 f2(); + } + + @A22(f1 = @Nested1(fields = @A16(f1 = "Hello", f2 = "World")), f2 = @Nested2(fields = @A1(f1 = {false, false}, f2 = {true, true}))) + public class C22 { + + } + + @Test + public void testAnnotationAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C22.class; + A22 a = klass.getAnnotation(A22.class); + String toString = "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A22(f1=" + HELLO_WORLD_NESTED + ",f2=" + TTFF_NESTED + ")"; + assertEquals(a.toString(), a.toString(), toString); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface A23 { + Nested1[] f1(); + Nested2[] f2(); + } + + @A23(f1 = { + @Nested1(fields = @A16(f1 = "Hello", f2 = "World")), @Nested1(fields = @A16(f1 = "Hola", f2 = "Mundo")) + }, f2 = { + @Nested2(fields = @A1(f1 = {false, false}, f2 = {true, true})), @Nested2(fields = @A1(f1 = {true,true}, f2 = {false,false})) + }) + public class C23 { + + } + + @Test + public void testAnnotationArrayAttributeToString() { + if(verifyNoPropertyViolation()) { + Class klass = C23.class; + A23 a = klass.getAnnotation(A23.class); + String holaMundo = HELLO_WORLD_NESTED.replace("Hello", "Hola").replace("World", "Mundo"); + String trueTrueString = TTFF_NESTED.replaceAll("false", "TMP").replaceAll("true", "false").replaceAll("TMP", "true"); + String toString = "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A23(f1=[" + HELLO_WORLD_NESTED + "," + holaMundo + "]," + + "f2=[" + TTFF_NESTED + "," + trueTrueString + "])"; + assertEquals(a.toString(), toString); + } + } +} diff --git a/src/tests/gov/nasa/jpf/test/vm/basic/MissingAnnotationClassTest.java b/src/tests/gov/nasa/jpf/test/vm/basic/MissingAnnotationClassTest.java new file mode 100644 index 0000000..170a62c --- /dev/null +++ b/src/tests/gov/nasa/jpf/test/vm/basic/MissingAnnotationClassTest.java @@ -0,0 +1,49 @@ +package gov.nasa.jpf.test.vm.basic; + +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; + +import org.junit.Test; + +import gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo; +import gov.nasa.jpf.util.test.TestJPF; +import gov.nasa.jpf.vm.AnnotationInfo; +import gov.nasa.jpf.vm.ClassInfoException; +import gov.nasa.jpf.vm.VM; + +public class MissingAnnotationClassTest extends TestJPF { + public static class SkippingSystemClassLoader extends JVMSystemClassLoaderInfo { + public SkippingSystemClassLoader(VM vm, int appId) { + super(vm, appId); + } + + @Override + public AnnotationInfo getResolvedAnnotationInfo(String typeName) throws ClassInfoException { + if(typeName.equals("gov.nasa.jpf.test.vm.basic.MissingAnnotationClassTest$Nullable")) { + throw new ClassInfoException("class not found: " + typeName, this, "java.lang.ClassNotFoundException", typeName); + } + return super.getResolvedAnnotationInfo(typeName); + } + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface Nullable { + } + + @Retention(RetentionPolicy.RUNTIME) + public @interface Present { + } + + @Present + @Nullable + public static class AnnotatedClass { + + } + + @Test + public void testMissingAnnotationOk() { + if(verifyNoPropertyViolation("+vm.classloader.class=gov.nasa.jpf.test.vm.basic.MissingAnnotationClassTest$SkippingSystemClassLoader")) { + assertEquals(1, AnnotatedClass.class.getAnnotations().length); + } + } +} -- 2.34.1