Regarding Objects

[Rohan Garg]

I have tried Symbolic Execution for v6,updated-spf and default repositories in Eclipse but unfortunately they did not work for "int". The revision no 4cd8ac11abee works well for "int" but I am unable to make it work for "Object". It would be great if someone could provide an example for Symbolic Execution to work with Objects. i.e the Java file and the JPF file.

Thanks and regards,

Rohan

[Quoc-Sang Phan]

v7 is released 4 yeas ago, why do you still want to try v6? Anyway, symbolic integer has long been supported, so pls clarify what doesn't work.

In order to use symbolic execution with object, you need to enable lazy initialization (symbolic.lazy=true). 

However, SPF can handle neither symbolic input file nor symbolic standard input, if this is what you are asking.

Sang

[Rohan Garg]

Hello Sang,

With the revision no. 621 i.e updated-spf I get the following output on Eclipse:

symbolic.min_int=-2147483648

symbolic.min_long=-9223372036854775808

symbolic.min_short=-32768

symbolic.min_byte=-128

symbolic.min_char=0

symbolic.max_int=2147483647

symbolic.max_long=9223372036854775807

symbolic.max_short=32767

symbolic.max_byte=127

symbolic.max_char=65535

symbolic.min_double=4.9E-324

symbolic.max_double=1.7976931348623157E308

JavaPathfinder core system v8.0 (rev 32+) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test

examples.Example.main()

====================================================== search started: 2/2/18 9:43 AM

First

Second

====================================================== Method Summaries

Inputs: x_1_SYMINT,y_2_SYMINT

No path conditions for examples.Example.foo(2,1)

====================================================== Method Summaries (HTML)

<h1>Test Cases Generated by Symbolic JavaPath Finder for examples.Example.foo (Path Coverage) </h1>

No path conditions for examples.Example.foo(2,1)

====================================================== results

no errors detected

====================================================== statistics

elapsed time:       00:00:00

states:             new=3,visited=0,backtracked=3,end=2

search:             maxDepth=2,constraints=0

choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=1

heap:               new=351,released=22,maxLive=345,gcCycles=3

instructions:       3136

max memory:         61MB

loaded code:        classes=60,methods=1279

====================================================== search finished: 2/2/18 9:43 AM

I am hereby attaching the files I have made taking the reference of the ppt at  http://selab.fbk.eu/issta2010/download/slides/JPF-Tutorial-ISSTA2010.pdf Slide No 61 and 62. This is where I find that symbolic integer does not work. 

Thanks,

Rohan

[Quoc-Sang Phan]

Hi Rohan,

The core symbolic execution engine does work correctly. That's why you get two outputs: "First" and "Second".
if you add Debug.printPC(""); at the end of method main, you can see two path conditions: x > y and x <= y

What does not work is the SymbolicListener, which generates test cases from path conditions.

If you are not generating test cases, it is safe to remove the listener.

Sang

[Rohan Garg]

Hello Sang,

Running the same files in revision no 610 generates the test cases. My goal is to generate the test cases for Objects like ArrayLists etc. However as the updated-spf does not generate test cases even for "int" , my question stands to how can I generate test cases for Objects?

Thanks,

Rohan

[Quoc-Sang Phan]

Hi Rohan,

The test cases are generated by different listeners. The symbolic listener only generate test cases for numeric inputs.

For symbolic array (with symbolic length), it is SymbolicSequenceListener. These listeners are independent to each other, so the fact that there is a bug in SymbolicListener doesn't mean other listeners do not work.

For reference type, you need to use lazy initialization. I'm looking at your other question about list.

Sang

[Rohan Garg]

Hello Sang,

I have tried keeping the lazy initialization on. Here is the output I get :

Running Symbolic PathFinder ...

symbolic.dp=choco

symbolic.string_dp_timeout_ms=0

symbolic.string_dp=none

symbolic.choco_time_bound=30000

symbolic.max_pc_length=2147483647

symbolic.max_pc_msec=0

symbolic.min_int=-1000000

symbolic.max_int=1000000

symbolic.min_double=-8.0

symbolic.max_double=7.0

---->Heap Listener

JavaPathfinder core system v8.0 (rev 32+) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test

myList.main()

====================================================== search started: 2/2/18 12:21 PM

[SEVERE] JPF exception, terminating: exception during instructionExecuted() notification

java.lang.NullPointerException

at gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction.getArgumentValues(JVMInvokeInstruction.java:168)

at gov.nasa.jpf.symbc.heap.HeapSymbolicListener.instructionExecuted(HeapSymbolicListener.java:429)

at gov.nasa.jpf.vm.VM.notifyInstructionExecuted(VM.java:808)

at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1922)

at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)

at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)

at gov.nasa.jpf.vm.VM.forward(VM.java:1722)

at gov.nasa.jpf.search.Search.forward(Search.java:579)

at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)

at gov.nasa.jpf.JPF.run(JPF.java:613)

at gov.nasa.jpf.JPF.start(JPF.java:189)

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:80)

at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

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

gov.nasa.jpf.JPFListenerException: exception during instructionExecuted() notification

at gov.nasa.jpf.vm.VM.notifyInstructionExecuted(VM.java:815)

at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1922)

at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)

at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)

at gov.nasa.jpf.vm.VM.forward(VM.java:1722)

at gov.nasa.jpf.search.Search.forward(Search.java:579)

at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)

at gov.nasa.jpf.JPF.run(JPF.java:613)

at gov.nasa.jpf.JPF.start(JPF.java:189)

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:80)

at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

Caused by: java.lang.NullPointerException

at gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction.getArgumentValues(JVMInvokeInstruction.java:168)

at gov.nasa.jpf.symbc.heap.HeapSymbolicListener.instructionExecuted(HeapSymbolicListener.java:429)

at gov.nasa.jpf.vm.VM.notifyInstructionExecuted(VM.java:808)

... 14 more

What I need here is to generate test cases for any object say eg. ArrayList

PFA the .java and .jpf files for your reference.

[Rohan Garg]

Hello Sang,

An update on the previous post. Running the same myList.jpf and myList.java for the updated-spf gives the following output

Running Symbolic PathFinder ...

symbolic.dp=choco

symbolic.string_dp_timeout_ms=0

symbolic.string_dp=none

symbolic.choco_time_bound=30000

symbolic.max_pc_length=2147483647

symbolic.max_pc_msec=0

symbolic.bvlength=32

symbolic.min_int=-2147483648

symbolic.min_long=-9223372036854775808

symbolic.min_short=-32768

symbolic.min_byte=-128

symbolic.min_char=0

symbolic.max_int=2147483647

symbolic.max_long=9223372036854775807

symbolic.max_short=32767

symbolic.max_byte=127

symbolic.max_char=65535

symbolic.min_double=4.9E-324

symbolic.max_double=1.7976931348623157E308

JavaPathfinder core system v8.0 (rev 32+) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test

myList.main()

====================================================== search started: 2/5/18 9:16 AM

New sym int al_1_SYMREF min=-2147483648, max=2147483647

ALOAD pcHeap: constraint # = 1

al_1_SYMREF = CONST_-1

====================================================== error 1

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty

java.lang.NoSuchMethodError: ?UNKNOWN?.get(I)Ljava/lang/Object;

at myList.compareList(myList.java:37)

at myList.main(myList.java:18)

====================================================== snapshot #1

thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}

  call stack:

at myList.compareList(myList.java:37)

at myList.main(myList.java:18)

New sym int al_1_SYMREF min=-2147483648, max=2147483647

New sym int al_1_SYMREF.modCount min=-2147483648, max=2147483647

New sym int al_1_SYMREF.elementData min=-2147483648, max=2147483647

New sym int al_1_SYMREF.size min=-2147483648, max=2147483647

New sym int java.util.ArrayList.serialVersionUID min=-2147483648, max=2147483647

New sym int java.util.ArrayList.DEFAULT_CAPACITY min=-2147483648, max=2147483647

New sym int java.util.ArrayList.EMPTY_ELEMENTDATA min=-2147483648, max=2147483647

New sym int java.util.ArrayList.DEFAULTCAPACITY_EMPTY_ELEMENTDATA min=-2147483648, max=2147483647

New sym int java.util.ArrayList.MAX_ARRAY_SIZE min=-2147483648, max=2147483647

New sym int java.util.AbstractCollection.MAX_ARRAY_SIZE min=-2147483648, max=2147483647

ALOAD pcHeap: constraint # = 2

al_1_SYMREF = CONST_0 &&

al_1_SYMREF != CONST_-1

numeric PC: constraint # = 1

CONST_0 < al_1_SYMREF.size -> true

### PCs: total:1 sat:1 unsat:0

string analysis: SPC # = 0

NPC constraint # = 1

CONST_0 < al_1_SYMREF.size

numeric PC: constraint # = 1

CONST_0 >= al_1_SYMREF.size -> true

### PCs: total:2 sat:2 unsat:0

string analysis: SPC # = 0

NPC constraint # = 1

CONST_0 >= al_1_SYMREF.size

numeric PC: constraint # = 1

CONST_0 >= al_1_SYMREF.size -> true

string analysis: SPC # = 0

NPC constraint # = 1

CONST_0 >= al_1_SYMREF.size[-2147483648]

Property Violated: PC is constraint # = 1

CONST_0 >= al_1_SYMREF.size[-2147483648]

Property Violated: result is  "java.lang.IndexOutOfBoundsException: Index: 0, Size: 0..."

****************************

====================================================== error 2

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty

java.lang.IndexOutOfBoundsException: Index: 0, Size: 0

at java.util.ArrayList.rangeCheck

at java.util.ArrayList.get

at myList.compareList(myList.java:37)

at myList.main(myList.java:18)

====================================================== snapshot #2

thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}

  call stack:

at java.util.ArrayList.rangeCheck(pc 20)

at java.util.ArrayList.get(pc 2)

at myList.compareList(myList.java:37)

at myList.main(myList.java:18)

lazy initialization

# heap cg registered: gov.nasa.jpf.symbc.heap.HeapChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=-1]

lazy initialization

GETFIELD pcHeap: constraint # = 3

al_1_SYMREF.elementData = CONST_-1 &&

al_1_SYMREF = CONST_0 &&

al_1_SYMREF != CONST_-1

numeric PC: constraint # = 1

CONST_0 < al_1_SYMREF.size -> true

string analysis: SPC # = 0

NPC constraint # = 1

CONST_0 < al_1_SYMREF.size[2147483647]

Property Violated: PC is constraint # = 1

CONST_0 < al_1_SYMREF.size[2147483647]

Property Violated: result is  "java.lang.NullPointerException..."

****************************

====================================================== error 3

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty

java.lang.NullPointerException

at java.util.ArrayList.elementData

at java.util.ArrayList.get

at myList.compareList(myList.java:37)

at myList.main(myList.java:18)

====================================================== snapshot #3

thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}

  call stack:

at java.util.ArrayList.elementData(pc 5)

at java.util.ArrayList.get(pc 7)

at myList.compareList(myList.java:37)

at myList.main(myList.java:18)

lazy initialization

New sym int al_1_SYMREF.elementData min=-2147483648, max=2147483647

New sym int [Ljava.lang.Object;@2b7_length min=-2147483648, max=2147483647

GETFIELD pcHeap: constraint # = 4

al_1_SYMREF.elementData = CONST_0 &&

al_1_SYMREF.elementData != CONST_-1 &&

al_1_SYMREF = CONST_0 &&

al_1_SYMREF != CONST_-1

[SEVERE] JPF exception, terminating: object is not an array: [Ljava.lang.Object;@2b7

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

gov.nasa.jpf.JPFException: object is not an array: [Ljava.lang.Object;@2b7

at gov.nasa.jpf.vm.ElementInfo.checkArrayBounds(ElementInfo.java:1644)

at gov.nasa.jpf.jvm.bytecode.AALOAD.push(AALOAD.java:37)

at gov.nasa.jpf.jvm.bytecode.ArrayLoadInstruction.execute(ArrayLoadInstruction.java:61)

at gov.nasa.jpf.symbc.bytecode.AALOAD.execute(AALOAD.java:46)

at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)

at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)

at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)

at gov.nasa.jpf.vm.VM.forward(VM.java:1722)

at gov.nasa.jpf.search.Search.forward(Search.java:579)

at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)

at gov.nasa.jpf.JPF.run(JPF.java:613)

at gov.nasa.jpf.JPF.start(JPF.java:189)

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:80)

at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

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

gov.nasa.jpf.JPFException: object is not an array: [Ljava.lang.Object;@2b7

at gov.nasa.jpf.vm.ElementInfo.checkArrayBounds(ElementInfo.java:1644)

at gov.nasa.jpf.jvm.bytecode.AALOAD.push(AALOAD.java:37)

at gov.nasa.jpf.jvm.bytecode.ArrayLoadInstruction.execute(ArrayLoadInstruction.java:61)

at gov.nasa.jpf.symbc.bytecode.AALOAD.execute(AALOAD.java:46)

at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)

at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)

at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)

at gov.nasa.jpf.vm.VM.forward(VM.java:1722)

at gov.nasa.jpf.search.Search.forward(Search.java:579)

at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)

at gov.nasa.jpf.JPF.run(JPF.java:613)

at gov.nasa.jpf.JPF.start(JPF.java:189)

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:80)

at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

Again here the purpose to get the test cases for reference types is not getting fulfilled  also another unknown object is being created.

PFA the codes for your reference.

Regards,

Rohan