Where is path condition and solution result stored in?

[QRXqrx]

Hi there, I'm new here and I have just investigated JDart about half a month. My requirement now is to extract the path condition of a pair of specific test input, and I just do not know how solve it. I have read paper about JDart and I found similar problem at issue#27. I followed the discussion there and implement a function to parse Node root in InternalConstraintTree but I doesn't work for me (maybe my implementation is not right).

I think I'm now still very confused about how JDart works. I looks like JDart will maintain a symbolic tree during execution and will dynamically update this tree when solved. Thus I want to know is there possible to extract the symbolic tree or maybe there are some more simplistic way to extract path condition for a specific test input? Such as instrument some codes and then execute to obtain path constraints? Anything relevant is welcome, I would very appreciate it if you could help me! Thx!

[fhowar]

You could set jdart.tree.json.print to otain a json representation of the tree.

The call to ca.getConstraintsTree().getAllPaths() in JDart.java (line 268) actually retuns all paths with constraints. You could work with these.

Also, please check out current development version: https://github.com/tudo-aqua/jdart

We have rewritten the constraints tree last year: https://github.com/tudo-aqua/jdart/tree/sv-comp-2021/src/main/gov/nasa/jpf/jdart/constraints/tree

We are happy to provide support for the current version. Please ask a question here: https://github.com/tudo-aqua/jdart/issues

[QRXqrx]

You could set jdart.tree.json.print to otain a json representation of the tree.

The call to ca.getConstraintsTree().getAllPaths() in JDart.java (line 268) actually retuns all paths with constraints. You could work with these.

Also, please check out current development version: https://github.com/tudo-aqua/jdart

We have rewritten the constraints tree last year: https://github.com/tudo-aqua/jdart/tree/sv-comp-2021/src/main/gov/nasa/jpf/jdart/constraints/tree

We are happy to provide support for the current version. Please ask a question here: https://github.com/tudo-aqua/jdart/issues

Hey! Thank u for replying! Your advice is really helpful yet unfortunately cannot fully cater my needs. I guess it is because I didn't describe my requirements so clearly. In particular, I do obtain json output of the constraint tree following the configuration you gave, though I all I need is a constraint of a path with respect to a certain set of test inputs. Suppose I have a simple program under test like below :

public class Main1 {

    int foo(int x) {
        if (x > 10) {
            if (x < 100) {
                System.out.println("[Main1] (x > 10) && (x < 100)");
                return 100;
            }

            else {
                System.out.println("[Main1] (x >= 100)");
                return 1000;
            }

        }
        else {
            if( x > 1 )
                System.out.println("[Main1] x > 1 && x <= 10");
            else if (x > 3)
                System.out.println("[Main1] x > 3 && x <= 10");
            else
                System.out.println("[Main1] x <= 1");
            return 0;
        }

    }

    public static void main(String[] args) {
        int val = new Main1().foo(5);
    }

}

Now I want to extract constraint of the path corresponding to the execution of x = 5, which should be x > 3 && x <= 10 in my example. To achieve this, what I'm doing currently is to put a constraint of x == 5 within my jpf config, like follows:

@include=../global/config.jpf

## Must tagged as concolic otherwise the testing process will be executed concretely.
concolic.method.foo=simple.Main1.foo(i:int)
concolic.method.foo.config=foo

########################## Main part

target=simple.Main1

concolic.method=foo

jdart.configs.foo.constraints=(i==5)

However, the execution result didn't as my expectation. It turns out that I can only got a constraint tree of one single branch, which usually looks like true OK: [ ]. I wander is it possible for JDart to realize the functionality I have mentioned directly or through some modification? I haven't read your project carefully. Maybe your modified version is able to finish this? Please let me know If you have any advice, thx : -) !

[fhowar]

Yeah, I don't know an easy fix for this in the current version of the code. The Constraint Tree will aggregate constraints in this way. You could explore the complete tree and then test on the paths, which paths are satisfiable for the assumption i==5 externally. But that would, of course, be a lot of unnecessary effort.

Are you interested in individual paths for concrete input values or in bigger slices?

[QRXqrx]

Yeah, in fact I'm interested in an individual path with respect to a certain group of inputs. I implemented my single path extraction by making concolic execution stopped right after initValuation. I do this modification because I found that JDart is always started its search for valuations with the values I give it. It works for me at present, but if there exists any problems in my implementation or there are another better choices, please let me know.