Symbolic Path Finder - test generation for objects

580 views
Skip to first unread message

grze...@gmail.com

unread,
Dec 10, 2014, 9:23:18 AM12/10/14
to java-pa...@googlegroups.com
Hi all


I just started playing with Symbolic Path Finder. I haven't examine all examples, but I have some question which came to my mind:

1. Is it always need to write driver to class usage ? By "class driver" I mean "main" method which is entry point for a program. 
2. If some method are not accessible from entry point, it means that it wouldn't be analyzed ?
3. I see that supported are primitives value constraints solver, I also checked that there were work for String constraint solver. It this work finished, could I check status of work somewhere ?
4. What about object (types) analysis ? I want to get test which covers bank.isRich() execution for 100% coverage in this simple example :

For example :

driver :
public class SPFDriver
{
    public static void main(String[] args)
    {
        Customer poor = new Customer(Status.POOR);
        Customer rich = new Customer(Status.RICH);
        Bank bank = Bank.getInstance();
        boolean rich1 = bank(poor);
    }
}


public class Bank
{
    public boolean isRich(Customer poor)
    {
        return poor.getStatus().equals(Status.RICH);
    }
    static Bank getInstance()
    {
        return new Bank();
    }
}

public class Customer
{
    private final Status _status;

    public Customer(Status status)
    {
        _status = status;
    }

    public Status getStatus()
    {
        return _status;
    }
}

class Status
{
    static Status RICH = new Status();
    static Status POOR = new Status();
}


my settings : 

target=bank.SPFDriver
classpath = /media/data/dev/workspaces/intleij/research/spf-objects/target/SPF-Objects.jar
sourcepath = /media/data/dev/workspaces/intleij/research/spf-objects/src/main/java
symbolic.method= bank.Bank.isRich(sym)

search.depth_limit = 10
symbolic.min_int=-1000000
symbolic.max_int=1000000
symbolic.undefined=-1000
symbolic.min_double=-100000.0
symbolic.max_double=100000.0
coverage.include=bank.*
coverage.show_methods=true
coverage.show_bodies=true
listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener,gov.nasa.jpf.listener.CoverageAnalyzer,gov.nasa.jpf.symbc.SymbolicListener
vm.storage.class=nil
search.multiple_errors=true
symbolic.debug=on 



My output: 
I don't see difference between debug on/off. I don't know what some values means in "statistics" section. I also miss comprehensive guide for configuration, is any on web ? I search on several pages, this forum and examples, and know something from each part, but I miss guide with explanations and examples. 

Running Symbolic PathFinder ...
symbolic.dp=choco
symbolic.string_dp_timeout_ms=0

symbolic.string_dp=none   <------ should be none ??

symbolic.choco_time_bound=30000
symbolic.min_int=-1000000
symbolic.max_int=1000000
symbolic.min_double=-100000.0
symbolic.max_double=100000.0

JavaPathfinder v6.0 (rev 1052) - (C) RIACS/NASA Ames Research Center <---- I compiled version from v7-dev branch, so it should be 7 ??

====================================================== system under test
bank.SPFDriver.main()   <---- this is ok 

====================================================== search started: 10.12.14 15:14

====================================================== Method Sequences <---- should be empty ?

====================================================== JUnit 4.0 test class
import static org.junit.Assert.*;
import org.junit.Before;
import org.junit.Test;

public class bank_BankTest {

        private bank.Bank bank_bank;

        @Before
        public void setUp() throws Exception {
                bank_bank = new bank.Bank();
        }
}

====================================================== coverage statistics <--- I skip most info, but this part looks ok
------------------------------------------------------------------------------------------------------------
0,94 (50/53)        0,94 (15/16)        0,91 (20/22)         -                  0,89 (8/9)          1,00 (4/4)         total

====================================================== Method Summaries
Inputs: poor_2_SYMREF
No path conditions for isRich(bank.Customer@15b)

====================================================== Method Summaries (HTML)
<h1>Test Cases Generated by Symbolic JavaPath Finder for isRich (Path Coverage) </h1>
No path conditions for isRich(bank.Customer@15b)

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=2, visited=0, backtracked=2, end=1
search:             maxDepth=2, constraints hit=0
choice generators:  thread=1 (signal=0, lock=1, shared ref=0), data=1
heap:               new=357, released=14, max live=0, gc-cycles=2
instructions:       3224
max memory:         180MB
loaded code:        classes=59, methods=1093




Quoc-Sang Phan

unread,
Dec 10, 2014, 7:01:16 PM12/10/14
to java-pa...@googlegroups.com
Hi,

1. Yes.
2. No, it wouldn't.
3. Take a look at the examples in "jpf-symbc/src/examples/strings" to have an idea about what you can do with strings and settings for decision procedures etc.
4. Your example illustrates your question 2. isRich is not reachable from "main", that's why SPF says:
    "No path conditions for isRich(bank.Customer@15b)"

Hope this helps.

Sang

grze...@gmail.com

unread,
Dec 11, 2014, 3:11:53 AM12/11/14
to java-pa...@googlegroups.com
W dniu czwartek, 11 grudnia 2014 01:01:16 UTC+1 użytkownik Quoc-Sang Phan napisał:
Hi,

1. Yes.
2. No, it wouldn't.
3. Take a look at the examples in "jpf-symbc/src/examples/strings" to have an idea about what you can do with strings and settings for decision procedures etc.
4. Your example illustrates your question 2. isRich is not reachable from "main", that's why SPF says:
    "No path conditions for isRich(bank.Customer@15b)"

I made mistake when composing message and copy-pasting, in this line is exactly
boolean rich1 = bank.isRich(poor);

so whole method looks :
    public static void main(String[] args)
    {
        Customer poor = new Customer(Status.POOR);
        Customer rich = new Customer(Status.RICH);
        Bank bank = Bank.getInstance();
        boolean rich1 = bank.isRich(poor);
    }
so it is reachable.
 
Hope this helps.

Sang


Thanks ! 


P.S.
Is debug mode does anything ? I was trying to get some intel about what is happening and how this looks from inside to shine my driver in order to get it working.

grze...@gmail.com

unread,
Dec 11, 2014, 4:41:58 AM12/11/14
to java-pa...@googlegroups.com
For clarification :
it seems that it can correctly detect coverage :
-------------------------------------------- class coverage ------------------------------------------------
bytecode            line                basic-block         branch              methods             location
------------------------------------------------------------------------------------------------------------
1,00 (12/12)        1,00 (3/3)          1,00 (7/7)           -                  1,00 (3/3)          bank.Bank
  1,00 (3/3)          1,00 (1/1)          1,00 (2/2)           -                   -                  <init>()
  1,00 (4/4)          1,00 (1/1)          1,00 (2/2)           -                   -                  getInstance()
  1,00 (5/5)          1,00 (1/1)          1,00 (3/3)           -                   -                  isRich(Customer)

after switch to default branch version (previous was done on v7)
I see :
====================================================== Method Summaries
Inputs: poor_CONCRETE,
No path conditions for bank.Bank.isRich(bank.Customer@15e)

So instead symbolic Inputs: poor_2_SYMREF I see Inputs: poor_CONCRETE, but I have used same config with :
symbolic.method= bank.Bank.isRich(sym)

Quoc-Sang Phan

unread,
Dec 11, 2014, 11:44:03 AM12/11/14
to java-pa...@googlegroups.com
Did you turn on lazy initialization (symbolic.lazy) ?
If you use SymbolicListener in debug mode, it will print the path conditions and symbolic expression of the return value.

Sang

grze...@gmail.com

unread,
Dec 18, 2014, 4:56:32 AM12/18/14
to java-pa...@googlegroups.com


W dniu czwartek, 11 grudnia 2014 17:44:03 UTC+1 użytkownik Quoc-Sang Phan napisał:
Did you turn on lazy initialization (symbolic.lazy) ?
If you use SymbolicListener in debug mode, it will print the path conditions and symbolic expression of the return value.

Sang


Sorry for late response.

Indeed I haven't this setting in my file.
When I put it on to my *.jpf file, I have :
====================================================== search started: 18.12.14 10:44
java.lang.AssertionError: expected HeapChoiceGenerator, got:gov.nasa.jpf.symbc.sequences.SequenceChoiceGenerator[id="?",isCascaded:false,0..0,delta=+1,cur=0]
        at gov.nasa.jpf.symbc.bytecode.ALOAD.execute(ALOAD.java:102)
        at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1890)
        at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1848)
        at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:733)
        at gov.nasa.jpf.vm.VM.forward(VM.java:1719)
        at gov.nasa.jpf.search.Search.forward(Search.java:580)
        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:62)
        at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
        at java.lang.reflect.Method.invoke(Method.java:483)
        at gov.nasa.jpf.tool.Run.call(Run.java:81)
        at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:117)

is there any option to configure used choice generator ?

grze...@gmail.com

unread,
Dec 18, 2014, 5:17:01 AM12/18/14
to java-pa...@googlegroups.com

Sorry for late response.

Indeed I haven't this setting in my file.
When I put it on to my *.jpf file, I have :
====================================================== search started: 18.12.14 10:44
java.lang.AssertionError: expected HeapChoiceGenerator, got:gov.nasa.jpf.symbc.sequences.SequenceChoiceGenerator[id="?",isCascaded:false,0..0,delta=+1,cur=0]
        at gov.nasa.jpf.symbc.bytecode.ALOAD.execute(ALOAD.java:102)
        at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1890)
        at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1848)
        at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:733)
        at gov.nasa.jpf.vm.VM.forward(VM.java:1719)
        at gov.nasa.jpf.search.Search.forward(Search.java:580)
        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:62)
        at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
        at java.lang.reflect.Method.invoke(Method.java:483)
        at gov.nasa.jpf.tool.Run.call(Run.java:81)
        at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:117)

is there any option to configure used choice generator ?


Does "snapshot"'s in JPF output info refers to possible flows of code ?? I still have no PC info.

When I comment out gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener, I got :

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=-100000.0
symbolic.max_double=100000.0
JavaPathfinder v7.0 (rev 1225) - (C) RIACS/NASA Ames Research Center


====================================================== system under test
bank.SPFDriver.main()

====================================================== search started: 18.12.14 11:07
ALOAD pcHeap: constraint # = 1
poor_1_SYMREF == CONST_-1

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: Calling 'getStatus()Lbank/Status;' on null object <--- correctly detects possible NPE
        at bank.Bank.isRich(Bank.java:20)
        at bank.SPFDriver.main(SPFDriver.java:23)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
        at bank.Bank.isRich(Bank.java:20)
        at bank.SPFDriver.main(SPFDriver.java:23)

ALOAD pcHeap: constraint # = 1
poor_1_SYMREF[377] != CONST_-1
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 # = 2
poor_1_SYMREF[377]._status == CONST_-1 &&
poor_1_SYMREF[377] != CONST_-1

====================================================== error 2
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty  <--- I don't understand this error, does JPF cannot resolve equals method ? 
java.lang.NoSuchMethodError: ?UNKNOWN?.equals(Ljava/lang/Object;)Z
        at bank.Bank.isRich(Bank.java:20)
        at bank.SPFDriver.main(SPFDriver.java:23)


====================================================== snapshot #2
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
        at bank.Bank.isRich(Bank.java:20)
        at bank.SPFDriver.main(SPFDriver.java:23)

lazy initialization
GETFIELD pcHeap: constraint # = 2
poor_1_SYMREF[377]._status[394] != CONST_-1 &&
poor_1_SYMREF[377] != CONST_-1
lazy initialization
lazy initialization
GETSTATIC pcHeap: constraint # = 3
bank.Status.RICH == poor_1_SYMREF[377]._status[394] &&
poor_1_SYMREF[377]._status[394] != CONST_-1 &&
poor_1_SYMREF[377] != CONST_-1
lazy initialization
GETSTATIC pcHeap: constraint # = 3
bank.Status.RICH == CONST_-1 &&
poor_1_SYMREF[377]._status[394] != CONST_-1 &&
poor_1_SYMREF[377] != CONST_-1
lazy initialization
GETSTATIC pcHeap: constraint # = 4
bank.Status.RICH[395] != poor_1_SYMREF[377]._status[394] &&
bank.Status.RICH[395] != CONST_-1 &&
poor_1_SYMREF[377]._status[394] != CONST_-1 &&
poor_1_SYMREF[377] != CONST_-1



====================================================== coverage statistics

-------------------------------------------- class coverage ------------------------------------------------
bytecode            line                basic-block         branch              methods             location
------------------------------------------------------------------------------------------------------------
1,00 (12/12)        1,00 (3/3)          1,00 (7/7)           -                  1,00 (3/3)          bank.Bank
  1,00 (3/3)          1,00 (1/1)          1,00 (2/2)           -                   -                  <init>()
  1,00 (4/4)          1,00 (1/1)          1,00 (2/2)           -                   -                  getInstance()
  1,00 (5/5)          1,00 (1/1)          1,00 (3/3)           -                   -                  isRich(Customer)
1,00 (9/9)          1,00 (4/4)          1,00 (3/3)           -                  1,00 (2/2)          bank.Customer
  1,00 (6/6)          1,00 (3/3)          1,00 (2/2)           -                   -                  <init>(Status)
  1,00 (3/3)          1,00 (1/1)          1,00 (1/1)           -                   -                  getStatus()
0,85 (17/20)        0,83 (5/6)          0,71 (5/7)           -                  0,50 (1/2)          bank.SPFDriver
  0,00 (0/3)          0,00 (0/1)          0,00 (0/2)           -                   -                  <init>()
                                                                                    at bank.SPFDriver.<init>(SPFDriver.java:15) 
  1,00 (17/17)        1,00 (5/5)          1,00 (5/5)           -                   -                  main(String[])
1,00 (12/12)        1,00 (3/3)          1,00 (5/5)           -                  1,00 (2/2)          bank.Status
  1,00 (9/9)          1,00 (2/2)          1,00 (3/3)           -                   -                  <clinit>()
  1,00 (3/3)          1,00 (1/1)          1,00 (2/2)           -                   -                  <init>()

------------------------------------------------------------------------------------------------------------
0,94 (50/53)        0,94 (15/16)        0,91 (20/22)         -                  0,89 (8/9)          1,00 (4/4)         total

====================================================== Method Summaries
Inputs: poor_1_SYMREF
No path conditions for bank.Bank.isRich(bank.Customer@15e)

====================================================== Method Summaries (HTML)
<h1>Test Cases Generated by Symbolic JavaPath Finder for bank.Bank.isRich (Path Coverage) </h1>
No path conditions for bank.Bank.isRich(bank.Customer@15e)

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException: Calling 'getStatus..."
error #2: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodError: ?UNKNOWN?.equals(Ljav..."

====================================================== statistics
elapsed time:       00:00:00
states:             new=8,visited=0,backtracked=8,end=3
search:             maxDepth=4,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=3
heap:               new=398,released=41,maxLive=360,gcCycles=6
instructions:       3202
max memory:         180MB
loaded code:        classes=67,methods=1223

====================================================== search finished: 18.12.14 11:07

Corina Pasareanu

unread,
Dec 18, 2014, 11:39:02 AM12/18/14
to java-pa...@googlegroups.com
you can put symbolic.debug=true in your config file to get some info.
what is the issue?
corina

--

---
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/d/optout.

grze...@gmail.com

unread,
Dec 19, 2014, 10:04:00 AM12/19/14
to java-pa...@googlegroups.com

Hi!


W dniu czwartek, 18 grudnia 2014 17:39:02 UTC+1 użytkownik Corina napisał:
you can put symbolic.debug=true in your config file to get some info.

I have symbolic.debug=on, when I add symbolic.debug=true I don't see any change.
 
what is the issue?
corina

I have issue with :
====================================================== Method Summaries
Inputs: poor_1_SYMREF
No path conditions for bank.Bank.isRich(bank.Customer@15e)

====================================================== Method Summaries (HTML)
<h1>Test Cases Generated by Symbolic JavaPath Finder for bank.Bank.isRich (Path Coverage) </h1>
No path conditions for bank.Bank.isRich(bank.Customer@15e)

I don't understand why :
1) It cannot generates tests
2) It prints : No path conditions for :bank.Bank.isRich(bank.Customer@15e).. but several lines above I could see :

====================================================== error 2
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodError: ?UNKNOWN?.equals(Ljava/lang/Object;)Z
        at bank.Bank.isRich(Bank.java:20)
        at bank.SPFDriver.main(SPFDriver.java:23)


so there is PC for bank.Bank.isRich.

Also I cannot understand why mean this error above : java.lang.NoSuchMethodError: ?UNKNOWN?.equals(Ljava/lang/Object;)Z


Could you help with my doubts ?

Thanks in advance,
Grzesiek

 

Quoc-Sang Phan

unread,
Dec 19, 2014, 10:29:34 AM12/19/14
to java-pa...@googlegroups.com
On Friday, 19 December 2014 07:04:00 UTC-8, grze...@gmail.com wrote:

Also I cannot understand why mean this error above : java.lang.NoSuchMethodError: ?UNKNOWN?.equals(Ljava/lang/Object;)Z


There is an error in your isRich method, the description is as above: the method "equals" had not been defined before being called.
You need to define the method "equals" for the class "Status".

--Sang

grze...@gmail.com

unread,
Dec 23, 2014, 5:10:27 PM12/23/14
to java-pa...@googlegroups.com
I see, but in this case "equals" is inherited from Object class, is this some kind of error detection (using default "equals" instead implementing own version) ?


Grzesiek

Corina Pasareanu

unread,
Jan 15, 2015, 2:31:46 PM1/15/15
to java-pa...@googlegroups.com
Hi
What do you use to print the test cases?
I think you want to use lazy initialization but then a test case can not be printed with the sequence generator.
I plan a proper release for SPF (similar to JPF core) that should be cleaned up a bit. However this takes a bit of time.
Thank you all in advance for your patience and for your interest in SPF,
Corina


--

grze...@gmail.com

unread,
Jan 25, 2015, 11:54:15 AM1/25/15
to java-pa...@googlegroups.com

W dniu czwartek, 15 stycznia 2015 20:31:46 UTC+1 użytkownik Corina napisał:
Hi
Hi, sorry for late respond,
 
What do you use to print the test cases?
I think you want to use lazy initialization but then a test case can not be printed with the sequence generator.
I plan a proper release for SPF (similar to JPF core) that should be cleaned up a bit. However this takes a bit of time.
Thank you all in advance for your patience and for your interest in SPF,
Corina


Yes, exactly I used lazy init along with sequence generator to print test cases,
So this is expected behaviour ?

Thanks,

Grzesiek

Wira Pakpahan

unread,
Jun 25, 2018, 3:40:23 AM6/25/18
to Java™ Pathfinder
Hello, i wanna ask some questions about SPF.
When i use a mutant program then i run SPF for generate test case, it stop running, Why??
Reply all
Reply to author
Forward
0 new messages