Does jdart support complex data structure?

[Marvinmw]

Does jdart support complex data structure?

[zvonimir]

The current implementation of JDart supports symbolic inputs of only primitive types (int, bool, etc.). One can of course manually write a harness (e.g., unit test) that generates inputs that are complex data structure by leveraging symbolic inputs of primitive types. However, such complex data structures would in that case be concrete, although potentially filled with symbolic primitive values. An interesting (and challenging) extension to JDart would be to add support for symbolic data structures.
Does that answer your question?

[Marvinmw]

thanks. It is my expected answer. BTW, does Symbolic Java-PathFinder (jpf-symbc) support complex data structure?

[zvonimir]

I am not sure about that, sorry. I think that at some point they published papers about this, but I don't know if the published techniques were implemented in the main branch of Symbolic Java PathFinder.

[Marvinmw]

thanks, does jdart support string and char type?

[zvonimir]

Not in the way that I would guess you are asking about - to have it use the theory of strings.
@fhowar maybe you could confirm this for sure?

[ilebrero]

Hi all,

@zvonimir @fhowar do you know if there's a tool that currently supports complex data structures (concolically or just symbolically)? Or if there's research about solving these constraints on SMT? E.g. modelled in such a way that the solver finds the new heap configuration of a list given a path condition like:

list!=null` && list.header != null && list.header.next ==null && list.header.value = 10 
&& list instanceof List && list.header instanceof Node`

[fhowar]

Hi, I am not aware that any of the current concolic / symbolic tools for Java can do this. Symbolic pathfinder had some work in the past on heap shape (search for lazy initialization). Cheers Falk

…

On 27. Jun 2020, at 19:35, Ignacio Lebrero ***@***.***> wrote: Hi all, @zvonimir @fhowar do you know if there's a tool that currently supports complex data structures (concolically or just symbolically)? Or if there's research about solving these constraints on SMT? E.g. modelled in such a way that the solver finds the new heap configuration of a list given a path condition like: list!=null` && list.header != null && list.header.next ==null && list.header.value = 10 && list instanceof List && list.header instanceof Node` — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.

[ilebrero]

I'll take a look at it.

Thanks for the quick response!