Correct use of symbolic execution for java pathfinder or false positive?

[as...@itu.dk]

Hi,

I am trying to use JPF to verify a simple Java program, and it seems that I have encountered a weird situation/false positive where JPF reports a NullPointerException where there should not be any.

Specifically my example is

public class MinimalExample {
    public boolean testFoo(Foo foo) {
        if (foo != null) foo.runIt();
        return true;
    }

    public static void main(String[] args) {
        Foo foo = new Bar();
        MinimalExample minex = new MinimalExample();
        assert minex.testFoo(foo);
    }
}

interface Foo { void runIt(); }
class Bar implements Foo  { @Override public void runIt() { /* skip */ } }

When I run the above example, I get a NullPointerException at the foo.runIt() line in testFoo, even though I explicitly test that foo is not null before calling the method.

I am unsure on whether this is because I have called JPF in a wrong way, or that it is somehow a false positive. My JPF configuration is as follows:

target=examples.MinimalExample

# here write your own classpath and un-comment
classpath=/Users/asal/Documents/SourceControl/JavaRefactoring/build/classes/main

symbolic.lazy=true
symbolic.method=examples.MinimalExample.testFoo(sym)

# listener to print information (PCs, test cases) about symbolic run

listener = gov.nasa.jpf.symbc.SymbolicListener

# The following JPF options are usually used for SPF as well:

# no state matching

vm.storage.class=nil

# instruct jpf not to stop at first error

search.multiple_errors=true

and I run the command as follows:

> jpf src/main/resources/MinimalExample.jpf
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
JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.




====================================================== system under test
examples.MinimalExample.main()


====================================================== search started: 14-12-15 10:56


====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: Calling 'runIt()V' on null object
        at examples.MinimalExample.testFoo(MinimalExample.java:37)
        at examples.MinimalExample.main(MinimalExample.java:44)




====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
        at examples.MinimalExample.testFoo(MinimalExample.java:37)
        at examples.MinimalExample.main(MinimalExample.java:44)




====================================================== Method Summaries
Inputs: foo_1_SYMREF
No path conditions for examples.MinimalExample.testFoo(examples.Bar@161)


====================================================== Method Summaries (HTML)
<h1>Test Cases Generated by Symbolic JavaPath Finder for examples.MinimalExample.testFoo (Path Coverage) </h1>
No path conditions for examples.MinimalExample.testFoo(examples.Bar@161)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException: Calling 'runIt()V'..."


====================================================== statistics
elapsed time:       00:00:00
states:             new=2,visited=0,backtracked=2,end=0
search:             maxDepth=2,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=1
heap:               new=370,released=2,maxLive=0,gcCycles=1
instructions:       3134
max memory:         123MB
loaded code:        classes=66,methods=1309


====================================================== search finished: 14-12-15 10:56

Does anyone have any idea of why this is happening?

Thank you and Kind Regards,

Ahmad Salim

[Kasper Søe Luckow]

Hej Ahmad,

I think lazy loading needs to be fixed. SPF seems to incorrectly insert a heap choice at the invocation to runIt(), in turn incorrectly setting the reference to null. I can try looking into it.

Are you ultimately trying to analyze unbounded data structures or just a symbolic reference type as in this example?

Kasper

[Ahmad Salim Al-Sibahi]

Hej Kasper,

Thank you for the answer.

Ultimately, I am trying to analyze an unbounded data structure in the context of a program that uses the visitor pattern.

SPF seemed to get stuck on that particular implementation (I gave up around after 1 hour), but I got a similar NullPointerException as one branch where it should not happen before it got stuck and I tried to reproduce that error with this minimal example. This is primarily why I had send this mail, to check whether this was perhaps due to me configuring JPF wrongly or it was indeed a true bug in the lazy initialization procedure.

Kind Regards/Med Venlig Hilsen

Ahmad Salim Al-Sibahi

--

---
You received this message because you are subscribed to a topic in the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/java-pathfinder/lPvcZkZ8nkE/unsubscribe.
To unsubscribe from this group and all its topics, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.