setField fails on private field even if "private" is disabled via reflection

[Cyrille Artho]

I'm trying to analyze code that uses JPF_java_lang_reflect_Field.setValue.
Unfortunately it looks like JPF assumes that private fields stay private forever, even though reflection can change that:

gov.nasa.jpf.JPFException: attempt to modify frozen object

Is there an easy way to turn this check off? It should not trigger an error if Field.setAccessible(true) was called before setValue.

Below is the stack trace, but there's nothing else to be found there: calling setValue on a private field produces that exception even though setAccessible(true) was called.

[SEVERE] JPF exception, terminating: exception in native method java.lang.reflect.Field.set
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFException: attempt to modify frozen object: ...
    at gov.nasa.jpf.vm.ElementInfo.checkIsModifiable(ElementInfo.java:2099)
    at gov.nasa.jpf.vm.ElementInfo.setFieldAttr(ElementInfo.java:638)
    at gov.nasa.jpf.vm.JPF_java_lang_reflect_Field.setValue(JPF_java_lang_reflect_Field.java:542)
    at gov.nasa.jpf.vm.JPF_java_lang_reflect_Field.set__Ljava_lang_Object_2Ljava_lang_Object_2__V(JPF_java_lang_reflect_Field.java:468)
    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.set
    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:2099)
    at gov.nasa.jpf.vm.ElementInfo.setFieldAttr(ElementInfo.java:638)
    at gov.nasa.jpf.vm.JPF_java_lang_reflect_Field.setValue(JPF_java_lang_reflect_Field.java:542)
    at gov.nasa.jpf.vm.JPF_java_lang_reflect_Field.set__Ljava_lang_Object_2Ljava_lang_Object_2__V(JPF_java_lang_reflect_Field.java:468)
    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

[PETER C MEHLITZ]

this is not the private modifier, it is attempting to modify an already state stored ElementInfo. Is this a static field?

-- 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]

No, it's a private instance field. The bytecode is generated from scalac so the field can't be made public.
I guess the framework could be written to call Scala's _$eq method instead of using setField. But the basic problem is that setField does not seem to work where it should.

[Peter Mehlitz]

'public' won't help, this was JPF state management - everytime you want to modify a ElementInfo, you have to obtain it via getModifiableElementInfo() so that JPF can do proper copy-on-first-write.

Should be fixed now

-- Peter