Can DSE component of Evosuite extract symbolic execution path?

[QRXqrx]

Dear Evosuite community, I'm new here and I'm not very familiar with Evosuite source code. I have some requirements in symbolic execution, that is, I want to extract specific path condition with respect to a certain vector of test inputs. It looks like that Evosuite supports symbolic execution as well which is implemented by package org.evosuite.symbolic. I'd like to know is there any chance that Evosuite can just satisfy my requirement above? If so, how can I invoke the API provided in org.evosuite.symbolic independently to realize it? I would really appreciate it if someone could help me. Any advice is welcome (like implement this functionality in some other way.) Thx :-）！

[ilebrero]

Hey @QRXqrx,

Currently, the symbolic engine is capable of extracting the particular path condition of a particular test case, though this is integrated inside the symbolic module, requires the construction of the test case the way is modeled inside of Evosuite and is not independently usable through an API at the moment. Let me take a look at it over the weekend to analyze what changes would be needed to support it both programmatically as an API and directly as a configuration in the tool and I'll get back to you. Thanks :)

[QRXqrx]

Hey @ilebrero,

Thank u for you replying! That would be great if Evosuite could support the functionality I mentioned. I will wait patiently :-).

[ilebrero]

Hi @QRXqrx,

Apologies for the delay. I took a look at the codebase, I can do a few changes to add a configuration in the tool for retrieving the path condition from a method given a set of inputs. To keep the implementation simple for a first try, at a high level it would work by:

1. Saving the inputs in a .txt file in JSON format in the same way as Jackson uses them.
2. Running Evosuite using a new configuration
3. The path conditions would be saved in another .txt file/printed on screen.

There are a few things to consider:

• Only static methods would be supported.
• Only Integers, floats, Strings and 1-dimensional arrays would be supported, everything else would be filled with a null value. The symbolic engine doesn't support objects and multidimensional arrays at the time. There is an implementation in the way, but there is no ETC yet.
• There might be limitations on the symbolic execution itself in case some elements of the language are not modeled by the engine.
• The format of the path conditions would be as is collected and not very friendly to read so some post-processing of the results might be needed after you get the resulting txt file.
• There might be some other limitations that I'm not seeing at the moment and might come up later on.

Would this work for you?

[QRXqrx]

Hey @ilebrero,

Thank u for your replying! Your ideas appeal to me, but it sounds it should take time to further extended, such as reference and array modeling. I'm also trying to extend other symbolic tools to support my requirement these days. Please let me know if there are anything I could help. But I have to admit that I have just picked symbolic execution recently, so that it would be better giving me some materials for reference when there are any work for me.