Improves annotation support (#161)
authorjtoman <jtoman@users.noreply.github.com>
Fri, 7 Sep 2018 19:34:36 +0000 (12:34 -0700)
committercyrille-artho <cyrille-artho@users.noreply.github.com>
Fri, 7 Sep 2018 19:34:36 +0000 (21:34 +0200)
* 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

18 files changed:
src/classes/gov/nasa/jpf/AnnotationProxyBase.java
src/classes/java/lang/reflect/Method.java
src/main/gov/nasa/jpf/jvm/ClassFile.java
src/main/gov/nasa/jpf/jvm/ClassFilePrinter.java
src/main/gov/nasa/jpf/jvm/ClassFileReader.java
src/main/gov/nasa/jpf/jvm/ClassFileReaderAdapter.java
src/main/gov/nasa/jpf/jvm/JVMAnnotationParser.java
src/main/gov/nasa/jpf/jvm/JVMClassInfo.java
src/main/gov/nasa/jpf/jvm/SkipAnnotation.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/MJIEnv.java
src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_AnnotationProxyBase.java
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java
src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java
src/tests/gov/nasa/jpf/test/vm/basic/AnnotationDefaultValueReflectionTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/AnnotationHashCodeEqualsTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/AnnotationToStringTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/MissingAnnotationClassTest.java [new file with mode: 0644]

index 43d84e4..72ac986 100644 (file)
@@ -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();
index e782d44..40b1888 100644 (file)
@@ -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);
index d3dbdb5..4bac2b2 100644 (file)
 
 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){
index d41cdd9..8b68eb9 100644 (file)
 
 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) {
+    
+  }
 }
index 6017fad..203537b 100644 (file)
@@ -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);
 
index 76fe464..4a3c19d 100644 (file)
@@ -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) {}
 }
index 8acef37..86d93a0 100644 (file)
@@ -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<AnnotationInfo> annotationStack;
+  protected AnnotationInfo curAi;
+  protected LinkedList<Object[]> 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;
     }
   }
index 3cd1214..7f3309f 100644 (file)
 
 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<AnnotationInfo> annotationStack;
+    protected LinkedList<Object[]> 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 (file)
index 0000000..5cf4686
--- /dev/null
@@ -0,0 +1,5 @@
+package gov.nasa.jpf.jvm;
+
+public class SkipAnnotation extends RuntimeException {
+
+}
index a37a941..1558f27 100644 (file)
  */
 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<Integer> 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<Integer> 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<a.length; i++){
           setDoubleArrayElement(aref,i,((Number)a[i]).doubleValue());
         }
+      } else if(ftype.equals("char[]")) {
+        aref = newCharArray(a.length);
+        for (int i=0; i<a.length; i++){
+          setCharArrayElement(aref,i,((Character)a[i]).charValue());
+        }
+      } else if(ftype.equals("short[]")) {
+        aref = newShortArray(a.length);
+        for (int i=0; i<a.length; i++){
+          setShortArrayElement(aref,i,((Number)a[i]).shortValue());
+        }
+      } else if(ftype.equals("byte[]")) {
+        aref = newByteArray(a.length);
+        for (int i=0; i<a.length; i++){
+          setByteArrayElement(aref,i,((Number)a[i]).byteValue());
+        }
+      } else if(ftype.equals("float[]")) {
+        aref = newFloatArray(a.length);
+        for (int i=0; i<a.length; i++){
+          setFloatArrayElement(aref,i,((Number)a[i]).floatValue());
+        }
       } else if (ftype.equals("java.lang.Class[]")){
         aref = newObjectArray("java.lang.Class", a.length);
         for (int i=0; i<a.length; i++){
@@ -1685,19 +1702,82 @@ public class MJIEnv {
           int cref = cci.getClassObjectRef();
           setReferenceArrayElement(aref,i,cref);
         }
+      } else {
+        String typeName = ftype.substring(0, ftype.length() - 2);
+        ClassInfo elemType = ClassLoaderInfo.getCurrentResolvedClassInfo(typeName);
+        aref = newObjectArray(typeName, a.length);
+        if(elemType.isEnum()) {
+          for(int i = 0; i < a.length; i++) {
+            setReferenceArrayElement(aref, i, makeAnnotationEnumRef((EnumValue) a[i]));
+          }
+          
+        } else {
+          for(int i = 0; i < a.length; i++) {
+            setReferenceArrayElement(aref, i, makeAnnotationProxy((AnnotationInfo) a[i]));
+          }
+        }
       }
 
       if (aref != NULL){
-        setReferenceField(proxyRef, fname, aref);
+        return Optional.of(aref);
       } else {
-        throwException("AnnotationElement type not supported: " + ftype);
+        return Optional.empty();
       }
 
+    } else if(v instanceof AnnotationInfo) {
+      return Optional.of(makeAnnotationProxy((AnnotationInfo) v));
+    } else {
+      return Optional.empty();
+    }
+  }
+
+  void initAnnotationProxyField (int proxyRef, FieldInfo fi, Object v) throws ClinitRequired {
+    String fname = fi.getName();
+    String ftype = fi.getType();
+
+    if (v instanceof String){
+      setReferenceField(proxyRef, fname, 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());
+    } else if (v instanceof Long){
+      setLongField(proxyRef, fname, ((Long)v).longValue());
+    } else if (v instanceof Float){
+      setFloatField(proxyRef, fname, ((Float)v).floatValue());
+    } else if (v instanceof Short){
+      setShortField(proxyRef, fname, ((Short)v).shortValue());
+    } else if (v instanceof Character){
+      setCharField(proxyRef, fname, ((Character)v).charValue());
+    } else if (v instanceof Byte){
+      setByteField(proxyRef, fname, ((Byte)v).byteValue());
+    } else if (v instanceof Double){
+      setDoubleField(proxyRef, fname, ((Double)v).doubleValue());
     } else {
-      throwException("AnnotationElement type not supported: " + ftype);
+      Optional<Integer> 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<ai.length; i++){
-        ClassInfo aci = ClassLoaderInfo.getCurrentResolvedClassInfo(ai[i].getName());
-        ClassInfo aciProxy = aci.getAnnotationProxy();
-
-        int ar = newAnnotationProxy(aciProxy, ai[i]);
+        int ar = makeAnnotationProxy(ai[i]);
         setReferenceArrayElement(aref, i, ar);
       }
       return aref;
@@ -1738,6 +1814,14 @@ public class MJIEnv {
     }
   }
 
+  private int makeAnnotationProxy(AnnotationInfo annotationInfo) {
+    ClassInfo aci = ClassLoaderInfo.getCurrentResolvedClassInfo(annotationInfo.getName());
+    ClassInfo aciProxy = aci.getAnnotationProxy();
+
+    int ar = newAnnotationProxy(aciProxy, annotationInfo);
+    return ar;
+  }
+
   public void handleClinitRequest (ClassInfo ci) {
     ThreadInfo ti = getThreadInfo();
 
index fdaaa85..70def1b 100644 (file)
 
 package gov.nasa.jpf.vm;
 
+import java.util.Arrays;
+import java.util.Objects;
+import java.util.function.IntFunction;
+
 import gov.nasa.jpf.annotation.MJI;
 
 /**
@@ -38,10 +42,255 @@ public class JPF_gov_nasa_jpf_AnnotationProxyBase extends NativePeer {
     return ci.getClassObjectRef();
   }
   
+  @MJI
+  public boolean equals__Ljava_lang_Object_2__Z(MJIEnv env, int objRef, int otherObj) {
+    if(otherObj == MJIEnv.NULL) {
+      return false;
+    }
+    ClassInfo thisProxy = env.getClassInfo(objRef);
+    ClassInfo otherProxy = env.getClassInfo(otherObj);
+    if(!thisProxy.equals(otherProxy)) {
+      if(!otherProxy.getAllInterfaceClassInfos().containsAll(thisProxy.getAllInterfaces())) {
+        return false;
+      }
+      // oof, someone implemented an annotation in user code. Delegate to their equals and let them deal with it
+      MethodInfo mi = otherProxy.getMethod("equals(Ljava/lang/Object;)Z", true);
+      assert mi != null;
+      ThreadInfo ti = env.getThreadInfo();
+      DirectCallStackFrame frame = ti.getReturnedDirectCall();
+      if(frame == null) {
+        frame = mi.createDirectCallStackFrame(ti, 0);
+        frame.setReferenceArgument(0, otherObj, env.getObjectAttr(otherObj));
+        frame.setReferenceArgument(1, objRef, env.getObjectAttr(objRef));
+        ti.pushFrame(frame);
+        return false;
+      } else {
+        Object attr = frame.getResultAttr();
+        int ret = frame.getResult();
+        env.setReturnAttribute(attr);
+        return ret == 1;
+      }
+    }
+    return annotationsEqual(env, objRef, otherObj);
+  }
+  
+  public static boolean annotationsEqual(MJIEnv env, int aObj, int bObj) {
+    if((aObj == MJIEnv.NULL) != (bObj == MJIEnv.NULL)) {
+      return false;
+    }
+    ClassInfo thisProxy = env.getClassInfo(aObj);
+    ClassInfo otherProxy = env.getClassInfo(bObj);
+    if(!thisProxy.equals(otherProxy)) {
+      return false;
+    }
+    FieldInfo[] fields = thisProxy.getDeclaredInstanceFields();
+    ElementInfo aE = env.getElementInfo(aObj);
+    ElementInfo bE = env.getElementInfo(bObj);
+    for (int i=0; i<fields.length; i++){
+      FieldInfo fi = fields[i];
+      String fn = fi.getName();
+      String ft = fi.getType();
+      if(!fi.isReference()) {
+        if(fi.is1SlotField()) {
+          if(aE.get1SlotField(fi) != bE.get1SlotField(fi)) {
+            return false;
+          }
+        } else {
+          if(aE.get2SlotField(fi) != bE.get2SlotField(fi)) {
+            return false;
+          }
+        }
+      } else if(ft.equals("java.lang.Class")) {
+        if(env.getReferenceField(aObj, fi) != env.getReferenceField(bObj, fi)) {
+          return false;
+        }
+      } else if(ft.equals("java.lang.String")) {
+        String aStr = env.getStringField(aObj, fn);
+        String bStr = env.getStringField(bObj, fn);
+        if(!Objects.equals(aStr, bStr)) {
+          return false;
+        }
+      } else if(ft.endsWith("[]")) {
+        String elemType = Types.getTypeName(Types.getArrayElementType(fi.getSignature()));
+        int aArrayRef = env.getReferenceField(aObj, fi);
+        int bArrayRef = env.getReferenceField(bObj, fi);
+        if((aArrayRef == MJIEnv.NULL) != (bArrayRef == MJIEnv.NULL)) {
+          return false;
+        }
+        ElementInfo aArrayContents = env.getElementInfo(aArrayRef);
+        ElementInfo bArrayContents = env.getElementInfo(bArrayRef);
+        assert aArrayContents.isArray() && bArrayContents.isArray();
+        if(Types.isBasicType(elemType) || elemType.equals("java.lang.Class")) {
+          Object rawArray1 = aArrayContents.getArrayFields().getValues();
+          Object rawArray2 = bArrayContents.getArrayFields().getValues();
+          if(!Objects.deepEquals(rawArray1, rawArray2)) {
+            return false;
+          }
+        // string array
+        } else if(elemType.equals("java.lang.String")) {
+          if(!Arrays.equals(env.getStringArrayObject(aArrayRef), env.getStringArrayObject(bArrayRef))) {
+            return false;
+          }
+        // either annotation or enum
+        } else {
+          int arrayLength1 = env.getArrayLength(aArrayRef);
+          int arrayLength2 = env.getArrayLength(bArrayRef);
+          if(arrayLength2 != arrayLength1) {
+            return false;
+          }
+          for(int j = 0; j < arrayLength1; j++) {
+            int elem1Ref = env.getReferenceArrayElement(aArrayRef, j);
+            int elem2Ref = env.getReferenceArrayElement(bArrayRef, j);
+            assert elem1Ref != MJIEnv.NULL && elem2Ref != MJIEnv.NULL;
+            if(!referenceTypesEqual(env, elem1Ref, elem2Ref)) {
+              return false;
+            }
+          }
+        }
+      } else {
+        if(!referenceTypesEqual(env, env.getReferenceField(aObj, fi), env.getReferenceField(bObj, fi))) {
+          return false;
+        }
+      }
+    }
+    return true;
+  }
+  
+  private static boolean referenceTypesEqual(MJIEnv env, int elem1Ref, int elem2Ref) {
+    ClassInfo aci = env.getClassInfo(elem1Ref);
+    ClassInfo bci = env.getClassInfo(elem2Ref);
+    assert aci != null && bci != null;
+    if(!aci.equals(bci)) {
+      return false;
+    }
+    if(aci.isEnum()) {
+      return elem1Ref == elem2Ref;
+    } else {
+      return annotationsEqual(env, elem1Ref, elem2Ref);
+    }
+  }
+
   @MJI
   public int toString____Ljava_lang_String_2 (MJIEnv env, int objref){
-    StringBuffer sb = new StringBuffer();
-    
+    StringBuilder sb = new StringBuilder();
+    annotationReferenceToString(env, objref, sb);
+    return env.newString(sb.toString());
+  }
+  
+  private int annotationHashCode(MJIEnv env, int objRef) {
+    ClassInfo thisProxy = env.getClassInfo(objRef);
+    FieldInfo[] fields = thisProxy.getDeclaredInstanceFields();
+    int hashCode = 0;
+    for (int i=0; i<fields.length; i++){
+      FieldInfo fi = fields[i];
+      int fieldHash = computeFieldHash(env, objRef, fi);
+      hashCode += (127 * getStringHash(env, env.newString(fi.getName()))) ^ fieldHash;
+    }
+    return hashCode;
+  }
+
+  private int computeFieldHash(MJIEnv env, int objRef, FieldInfo fi) {
+    String fn = fi.getName();
+    String ft = fi.getType();
+    if(!fi.isReference()) {
+      switch(ft) {
+      case "byte":
+        return Byte.valueOf(env.getByteField(objRef, fn)).hashCode();
+      case "boolean":
+        return Boolean.valueOf(env.getBooleanField(objRef, fn)).hashCode();
+      case "char":
+        return Character.valueOf(env.getCharField(objRef, fn)).hashCode();
+      case "short":
+        return Short.valueOf(env.getShortField(objRef, fn)).hashCode();
+      case "int":
+        return Integer.valueOf(env.getIntField(objRef, fn)).hashCode();
+      case "long":
+        return Long.valueOf(env.getLongField(objRef, fn)).hashCode();
+      case "float":
+        return Float.valueOf(env.getFloatField(objRef, fn)).hashCode();
+      case "double":
+        return Double.valueOf(env.getDoubleField(objRef, fn)).hashCode();
+      default:
+        throw new UnsupportedOperationException();
+      }
+    } else if(ft.equals("java.lang.Class")) {
+      return getObjectHash(env.getReferenceField(objRef, fi));
+    } else if(ft.equals("java.lang.String")) {
+      return getStringHash(env, env.getReferenceField(objRef, fi));
+    } else if(ft.endsWith("[]")) {
+      int aArrayRef = env.getReferenceField(objRef, fi);
+      ElementInfo aArrayContents = env.getElementInfo(aArrayRef);
+      String elemType = Types.getTypeName(Types.getArrayElementType(fi.getSignature()));
+      if(Types.isBasicType(elemType)) {
+        Object rawArray1 = aArrayContents.getArrayFields().getValues();
+        if(rawArray1 instanceof boolean[]) {
+          return Arrays.hashCode((boolean[])rawArray1);
+        } else if(rawArray1 instanceof byte[]) {
+          return Arrays.hashCode((byte[])rawArray1);
+        } else if(rawArray1 instanceof char[]) {
+          return Arrays.hashCode((char[])rawArray1);
+        } else if(rawArray1 instanceof short[]) {
+          return Arrays.hashCode((short[])rawArray1);
+        } else if(rawArray1 instanceof int[]) {
+          return Arrays.hashCode((int[])rawArray1);
+        } else if(rawArray1 instanceof long[]) {
+          return Arrays.hashCode((long[])rawArray1);
+        } else if(rawArray1 instanceof float[]) {
+          return Arrays.hashCode((float[])rawArray1);
+        } else if(rawArray1 instanceof double[]) {
+          return Arrays.hashCode((double[])rawArray1);
+        } else {
+          throw new RuntimeException();
+        }
+      } else if(elemType.equals("java.lang.Class")) {
+        return computeObjectArrayHash(env, aArrayRef, this::getObjectHash);
+      // string array
+      } else if(elemType.equals("java.lang.String")) {
+        return computeObjectArrayHash(env, aArrayRef, (ref) -> 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<Integer> 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; j<n; j++){
               if (j>0) 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; j<n; j++){
               if (j>0) sb.append(',');
-              sb.append(env.getIntArrayElement(ar,j));
+              sb.append(env.getByteArrayElement(ar,j));
+            }
+
+          } else if(ft.equals("boolean[]")) {
+            for (int j=0; j<n; j++){
+              if (j>0) sb.append(',');
+              sb.append(env.getBooleanArrayElement(ar,j));
+            }
+
+          } else if(ft.equals("short[]")) {
+            for (int j=0; j<n; j++){
+              if (j>0) sb.append(',');
+              sb.append(env.getShortArrayElement(ar,j));
+            }
+
+          } else if(ft.equals("char[]")) {
+            for (int j=0; j<n; j++){
+              if (j>0) sb.append(',');
+              sb.append(env.getCharArrayElement(ar,j));
+            }
+
+          } else if(ft.equals("float[]")) {
+            for (int j=0; j<n; j++){
+              if (j>0) sb.append(',');
+              sb.append(env.getFloatArrayElement(ar,j));
             }
 
-          } else if (ft.equals("long[]")){
+          } else if(ft.equals("long[]")) {
             for (int j=0; j<n; j++){
               if (j>0) sb.append(',');
               sb.append(env.getLongArrayElement(ar,j));
             }
-            
-          } else if (ft.equals("double[]")){
+
+          } else if(ft.equals("double[]")) {
             for (int j=0; j<n; j++){
               if (j>0) sb.append(',');
               sb.append(env.getDoubleArrayElement(ar,j));
             }
-            
-          } else if (ft.equals("boolean[]")){
+
+          } else if(ft.equals("java.lang.String[]")) {
             for (int j=0; j<n; j++){
               if (j>0) 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; j<n; j++){
               if (j>0) 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);
+    }
   }
 }
index 90a5dcf..c76ecb8 100644 (file)
  */
 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
index ba84851..34a2579 100644 (file)
@@ -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");
 
index 66b564e..8d13a0c 100644 (file)
@@ -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 (file)
index 0000000..eec9e89
--- /dev/null
@@ -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 (file)
index 0000000..484ddb0
--- /dev/null
@@ -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 (file)
index 0000000..2dbec23
--- /dev/null
@@ -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 (file)
index 0000000..170a62c
--- /dev/null
@@ -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);
+    }
+  }
+}