Problem with reflection/annotations

[Cyrille Artho]

I found a bug that prevents JPF from executing any programs using character annotations (and probably some other types as well).
The problem is that characters are internally integers, so initAnnotationProxyField uses the wrong type when checking for the type of v (the value object):

  void initAnnotationProxyField (int proxyRef, FieldInfo fi, Object v) throws ClinitRequired {
    String fname = fi.getName();
    String ftype = fi.getType();
System.err.println(ftype + ", " + v.getClass().getName());

    if (v instanceof String){
      setReferenceField(proxyRef, fname, newString((String)v));
    } else if (v instanceof Boolean){
      setBooleanField(proxyRef, fname, ((Boolean)v).booleanValue());
   ...

The "println" I inserted shows that "ftype" is a String with contents "char" (which is correct), but v is of type Integer, which results in a type error later:

char, java.lang.Integer
[SEVERE] JPF exception, terminating: exception in native method java.lang.reflect.Field.getAnnotation
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFException: not an int field: value
    at gov.nasa.jpf.vm.ElementInfo.setIntField(ElementInfo.java:881)
    at gov.nasa.jpf.vm.ElementInfo.setIntField(ElementInfo.java:786)
    at gov.nasa.jpf.vm.MJIEnv.setIntField(MJIEnv.java:443)
    at gov.nasa.jpf.vm.MJIEnv.initAnnotationProxyField(MJIEnv.java:1580)
...

I wonder what's the best way to fix this? Shouldn't the field information be based on constants (at least for primitive types) to allow a "switch" statement here covering all primitive types? A quick fix without that is a cascade of "if" statements on ftype:

  if (ftype.equals("char")) {
    setCharField(proxyRef, fname, ((Character)v).charValue());
  } else if (ftype.equals(...)) {
     ...
  } else if (v instanceOf String) { // non-primitive type: use existing if cascade covering other cases
    ...
  } else if (v instanceof AnnotationInfo.EnumValue) {
    ...
  } ...

My test case:

-- Test.jpf: --

classpath=.
target = Test


-- Test.java: --

public class Test {
  @charAnnotation('x') int n;

  public static void main(String[] args) throws Exception {
    java.lang.reflect.Field f = Test.class.getDeclaredField("n");
    java.lang.annotation.Annotation ann = f.getAnnotation(charAnnotation.class);
    System.out.println(ann);
  }
}

-- charAnnotation.java: --

import java.lang.annotation.ElementType;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Retention;
import java.lang.annotation.Target;

@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.FIELD)

public @interface charAnnotation {
  char value();
}

[Peter Mehlitz]

ClassFile.parseAnnotationValue() has to be fixed. Will do

-- Peter

> --
>
> ---
> You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[Cyrille Artho]

Thanks, I can confirm that it works for me now.

[Cyrille Artho]

Unfortunately, on the real system, I found another problem soon after. It does not seem to be related to MJIEnv anymore, though. It also works on small examples but not on the real system so I currently don't have a test case.

The issue is a private field inside a public class, which is accessed (set) by another class using reflection (Field.setInt). The type is correct this time but the "frozen" information is incorrect (the field is not final). The field is declared as "private int ..." in a public class.

[SEVERE] JPF exception, terminating: exception in native method java.lang.reflect.Field.setInt

---------------------- JPF error stack trace ---------------------

gov.nasa.jpf.JPFException: attempt to modify frozen object: ...
    at gov.nasa.jpf.vm.ElementInfo.checkIsModifiable(ElementInfo.java:2100)
    at gov.nasa.jpf.vm.ElementInfo.setIntField(ElementInfo.java:876)
    at gov.nasa.jpf.vm.JPF_java_lang_reflect_Field.setInt__Ljava_lang_Object_2I__V(JPF_java_lang_reflect_Field.java:291)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
    at java.lang.reflect.Method.invoke(Method.java:597)
    at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:121)
    at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:71)
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1894)
    at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1845)
    at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:748)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1638)
    at gov.nasa.jpf.search.Search.forward(Search.java:533)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:190)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
    at java.lang.reflect.Method.invoke(Method.java:597)
    at gov.nasa.jpf.tool.Run.call(Run.java:76)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:117)

---------------------- JPF error stack trace ---------------------

gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.reflect.Field.setInt
    at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:179)
    at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:71)
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1894)
    at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1845)
    at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:748)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1638)
    at gov.nasa.jpf.search.Search.forward(Search.java:533)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:190)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
    at java.lang.reflect.Method.invoke(Method.java:597)
    at gov.nasa.jpf.tool.Run.call(Run.java:76)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:117)
Caused by: gov.nasa.jpf.JPFException: attempt to modify frozen object: ...
    at gov.nasa.jpf.vm.ElementInfo.checkIsModifiable(ElementInfo.java:2100)
    at gov.nasa.jpf.vm.ElementInfo.setIntField(ElementInfo.java:876)
    at gov.nasa.jpf.vm.JPF_java_lang_reflect_Field.setInt__Ljava_lang_Object_2I__V(JPF_java_lang_reflect_Field.java:291)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
    at java.lang.reflect.Method.invoke(Method.java:597)
    at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:121)
    ... 15 more

[Cyrille Artho]

To update on the message below: I was able to rewrite the code such that the type of field access in question (java.lang.reflect.Field.set... family) can be avoided. So the bug in jpf-core still persists, but no longer affects my case study. A fix is therefore not so urgent (but of course still welcome).

[Peter Mehlitz]

it's just that Field.getCheckedElementInfo() doesn't do a getModifiableElementInfo() since it is also called from all the getters (which don't need it). Will fix.

In general - this exception means there is an attempt to modify program state that was already stored, which means getModifiable..() should have been used to obtain ElementInfo/StackFrame. I fully expect that we will still encounter these for a while since it was one of the major changes in v7. Again, the major reason for differentiating between get..() and getModifiable..() was to avoid the common v6 pitfall of storing/using references that were silently changed by its container (such as the top frame of ThreadInfos).

-- Peter

On Jul 3, 2013, at 12:34 AM, Cyrille Artho <cyrill...@gmail.com> wrote:

> To update on the message below: I was able to rewrite the code such that the type of field access in question (java.lang.reflect.Field.set... family) can be avoided. So the bug in jpf-core still persists, but no longer affects my case study. A fix is therefore not so urgent (but of course still welcome).
>