[JPF] Help about example listener

[Pham Quang Thap]

Dear all

I'm new familly with fpf. I also read much documentations on wiki jpf,
now I want to write a my own listener that implement ListenerPropertyAdapter to verify the program (check a class run with inputs arranges for exam)
in which inputs (properties in class) will be generated with me in IntructionExecuted ...

My problem is that I want to check a result ( get a value of property of class for example) for each path to check (complete path) ??
I have not understood much ListenerPropertyAdapter yet.

Help me, please,

Thanks alot.

Pham Quang Thap
Tel: 0983.220.597
other mail: thappq...@coltech.vnu.vn

[Ivan Mushketik]

Hello.
As I understand you want to know how to get a value of a specific
field of the object is a listener.

Here is a code sample:
// Overrided method from PropertyListenerAdapter
public void executeInstruction(JVM jvm) {
if (logExecuteInstruction) {
Instruction instr = jvm.getLastInstruction();
log("Execute instruction ");

ElementInfo ei = JVM.getVM().getLastElementInfo();
int numberOfFields = ei.getNumberOfFields();

for (int i = 0; i < numberOfFields; i++) {
FieldInfo fi = ei.getFieldInfo(i);
String fieldName = fi.getName();
log("\t" + fieldName);

if (fieldName.equals("isPrimitive")) {
log("\t\t isPrimitive ==" +
ei.getFields().getBooleanValue(i));
}
}

}
}

I receive a lot of output when I add this listener here is it part:
[MYLISTENER] Execute instruction
[MYLISTENER] name
[MYLISTENER] cref
[MYLISTENER] isPrimitive
[MYLISTENER] isPrimitive ==false
[MYLISTENER] enumConstantDirectory

I hope this will help you.

[Pham Quang Thap]

Hello
Thanks for your reply so much,
but, i want differently
for example, there are some intructions in class A as following

{
...
x = I will give arrange for x, y through choicegenerator
y =

some code to calculte x, y ..

x = x+ y;
...
}

Now, i want to get last value of x for each completed path (after run all code for each path)

I hope you could help me

Pham Quang Thap
Tel: 0983.220.597
other mail: thappq...@coltech.vnu.vn

[Peter Mehlitz]

there are three aspects involved:

(1) noticing when the relevant variables are changed. This you do with a normal instructionExecuted() listener either on PUTFIELD/STATIC (if x,y are fields) or xSTORE instruction (if x,y are local vars, which is a little harder because you have to get the name of the local variable from the StackFrame this is executed in).

(2) store these variable/value tuples as a state extension, and restore it upon backtracking. There is some support for this with gov.nasa.jpf.util.StateExtensionListener/Client, but the only jpf-core example (SrciptEnvironment) is actually more complicated than your example.

(3) recognizing end states and processing your stored variables/values - that is a simple stateAdvanced() listener that checks for Search.isEndState()

(1) and (3) can be combined within the same listener, which should also be a StateExtensionClient. For (2) you use the StateExtensionListener as is.

-- Peter

[Pham Quang Thap]

I've done follow (1) (3), but from end state i can not get value of x (assume x is public property of class A), something wrongs with me?
help me, please!

Thanks!

Pham Quang Thap
Tel: 0983.220.597
other mail: thappq...@coltech.vnu.vn

[Pham Quang Thap]

Dear all,

I try to get last value of a field after all changes in my listener, but i can not, any one help me? please

example: assume x is a field of my class, and some instructions change value of x, and i want to get last value of x in my listener

Thanks.

Pham Quang Thap
Tel: 0983.220.597
other mail: thappq...@coltech.vnu.vn

On Sat, Mar 12, 2011 at 10:32, Peter Mehlitz <pcme...@gmail.com> wrote:

[Ivan Mushketik]

Hello.
In listener on instructionExecuted or executeInstruction you can check
value of your variable. Only PUTFIELD and PUTSTATIC instructions
change values of fields (check out array instructions in JVM
specification if you need to monitor changes of array).
Every time one of those instruction is executed you can save new value
in your listener. I've already wrote in this theme a code sample how
you can get a value of a field.

Is that a solution to your problem?
Or you have some code that should do this but it doesn't work?

[Pham Quang Thap]

Yes, Thank a lot for your guide

This is my code in instructionExecuted method

public void instructionExecuted(JVM vm) {
        Instruction insn = vm.getLastInstruction();
        ElementInfo ei = vm.getLastElementInfo();
        SystemState ss = vm.getSystemState();
        ThreadInfo ti = vm.getLastThreadInfo();       
       
        if (insn instanceof EXECUTENATIVE) { // break on method call
            EXECUTENATIVE exec = (EXECUTENATIVE) insn;

            if (exec.getExecutedMethodName().equals("getInt")){ // Verify.getInt(..) - this insn did create a CG on its own
              if (!ti.isFirstStepInsn()){ // top half - first execution
                IntIntervalGenerator cg = new IntIntervalGenerator("instrumentVerifyGetInt", 1,10);
                ss.setNextChoiceGenerator(cg);
//                ...

              } else { // bottom half - reexecution at the beginning of the next transition
                IntIntervalGenerator cg = ss.getCurrentChoiceGenerator("instrumentVerifyGetInt", IntIntervalGenerator.class);
                assert cg != null : "no 'instrumentVerifyGetInt' IntIntervalGenerator found";
                int myChoice = cg.getNextChoice();
//                ... // process choice
              }
            }
          }       
       
        if (insn instanceof PUTFIELD){
            PUTFIELD getInsn = (PUTFIELD) insn;
            FieldInfo fi = getInsn.getFieldInfo();           
            if (fi.getName().equals("x")){
                storePUTFIELD = ei.getIntField(fi);               
            }
        }      
      
    }


but when it run, I see error:

[SEVERE] JPF exception, terminating: exception during instructionExecuted() notification
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFException: not an int[]
    at gov.nasa.jpf.jvm.ArrayFields.getIntValue(ArrayFields.java:67)
    at gov.nasa.jpf.jvm.ElementInfo.getIntField(ElementInfo.java:972)
    at gov.nasa.jpf.vs.ScenarioListener.instructionExecuted(ScenarioListener.java:119)
    at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:692)
    at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1989)
    at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:1941)
    at gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:652)
    at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1717)
    at gov.nasa.jpf.search.Search.forward(Search.java:500)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
    at gov.nasa.jpf.JPF.run(JPF.java:534)
    at gov.nasa.jpf.JPF.start(JPF.java:166)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
    at java.lang.reflect.Method.invoke(Unknown Source)
    at gov.nasa.jpf.tool.Run.call(Run.java:76)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:86)

Could you show me for my problem, please

Thanks

Pham Quang Thap
Tel: 0983.220.597
other mail: thappq...@coltech.vnu.vn

[Peter Mehlitz]

the error message is misleading (which I will fix), but the problem is that 'x' is an ArrayField, which you try to access as an 'int'. Maybe this is a different 'x' field in another class, your code also has to check the class this field belongs to.

You are also aware of that you are using a cascaded ChoiceGenerator? Verify.getInt() already registers a CG, which is not replaced by your 'instrumentVerifyGetInt'. If you want to replace the Verify.getInt() CG you have to either (a) remove it and then register yours, or (b) use a executeInstruction() notification and skip the Verify.getInt() call (in which case you have to clean up the callstack yourself)

-- Peter

[Peter Mehlitz]

correct first part of my last message (was looking at a wrong ElementInfo version) - your FieldInfo obviously is an IntegerFieldInfo, but the ElementInfo is for an array object. Either 'ei' is wrong, or something in your listener corrupted JPF. To tell, I need to see the whole listener code.

-- Peter

[Pham Quang Thap]

That is my simple example, Im only implement InstructionExecuted method for test
and this is my class for under test

import gov.nasa.jpf.jvm.Verify;

import java.util.logging.Level;
import java.util.logging.Logger;

public class MyScenario {
    int x;
    static Logger log = Logger.getLogger(MyScenario.class.getName());

    public MyScenario(){       
        x=Verify.getInt(1, 10);       
               
        System.out.println("Result x is " +x);
       
        x=x+1;
       
        System.out.println("Result after process is " +x);
    }
   
    public static void main(String[] args){           
        new MyScenario();
       
    }
}

I pay many time for it, but i do not understand why.

Pham Quang Thap
Tel: 0983.220.597
other mail: thappq...@coltech.vnu.vn