Running Symbolic Pathfinder from another Symbolic Pathfinder execution

[Juan Manuel Copia]

Hello,

I'm trying to launch a second symbolic execution from an already ongoing symbolic execution, but this second execution breaks the original one.

That is, I'm performing symbolic execution of a program "X", and during the execution of the method "execute" from the bytecode instruction: gov.nasa.jpf.symbc.bytecode.GETFIELD, I'm launching a second symbolic execution, which is executed correctly, but ends up breaking the symbolic execution of program "X".

This is the code inside "execute" from gov.nasa.jpf.symbc.bytecode.GETFIELD that launches the second symbolic execution:

try {

    String[] args = new String[10];

    Config conf = JPF.createConfig(args);

    conf.setProperty("target", "myexample.Example2");

    JPF jpf = new JPF(conf);

    jpf.run();

} catch (JPFConfigException cx) {

    System.out.println(cx.getMessage());

} catch (JPFException jx) {

    System.out.println(jx.getMessage());

}

The program that gets executed in this second execution is the following:

package myexample;

public class Example2 {

    public static void main(String[] args) {

        Object a = new Object();

        System.out.println("\nExecuted!!!");

    }

}

The execution terminates successfully, this is the output:

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 - (C) 2005-2014 United States Government. All rights reserved.

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

myexample.Example2.main()

====================================================== search started: 12/15/22 3:41 PM

Executed!!!

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

no errors detected

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

elapsed time: 00:00:00

states: new=1,visited=0,backtracked=1,end=1

search: maxDepth=1,constraints=0

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

heap: new=354,released=12,maxLive=0,gcCycles=1

instructions: 3225

max memory: 3925MB

loaded code: classes=60,methods=1294

====================================================== search finished: 12/15/22 3:41 PM

But soon after, the first symbolic execution breaks with the following exception:

Exception in thread "main" lissa.SPFLISSAException: jpf-core threw exception

at lissa.LISSAShell.runJPF(LISSAShell.java:48)

at lissa.LISSAShell.start(LISSAShell.java:41)

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

Caused by: gov.nasa.jpf.JPFException: object is not of type java.lang.String

at gov.nasa.jpf.vm.DynamicElementInfo.getStringChars(DynamicElementInfo.java:111)

at gov.nasa.jpf.vm.DynamicElementInfo.asString(DynamicElementInfo.java:99)

at gov.nasa.jpf.vm.ElementInfo.getStringField(ElementInfo.java:1521)

at gov.nasa.jpf.vm.UncaughtException.<init>(UncaughtException.java:51)

at gov.nasa.jpf.vm.ThreadInfo.throwException(ThreadInfo.java:2859)

at gov.nasa.jpf.vm.ThreadInfo.createAndThrowException(ThreadInfo.java:1789)

at gov.nasa.jpf.vm.ThreadInfo.createAndThrowException(ThreadInfo.java:1813)

at gov.nasa.jpf.symbc.bytecode.INVOKEVIRTUAL.execute(INVOKEVIRTUAL.java:48)

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

at lissa.LISSAShell.runJPF(LISSAShell.java:46)

... 2 more

Some times the error changes depending on the program that is executed. Apparently running JPF from inside an already ongoing execution breaks things.

Do you know why this happens and how can launch other symbolic executions from an ongoing one without breaking things?

Thank you!

Juan Manuel Copia