search

z3str / Z3-str

A Z3-Based String Constraint Solver
Other
87 stars 13 forks source link

String value generation algorithm #7

Closed yannicnoller closed 8 years ago

yannicnoller commented 8 years ago

I read your paper Z3-str: a z3-based string solver for web application analysis and I have a question how you generate the values for a model in case you find that the formula is satisfiable. The paper says "Besides, the satisfying values of string variables x, y and m can be retrieved from their equivalence classes.". How does that work in detail? What algorithm is used and there can I find that in the source code?

Btw is this the right place to ask such a question or do you have an user mailing list?

Thanks, Yannic

z3str commented 8 years ago

Hi Yannic,

Thanks for the question.

In short, this is implemented in function get_eqc_value(). And we keep querying whether a variable could be simplified. If yes, we use its equivalent concrete value and proceed (you could check the call sites of get_eqc_value)

This is related to how equivalent items are maintained in Z3. If the Z3 core thinks two items are equal, they are put in a circular link list. In addition, we know whether an item in the list is constant or not by calling isConstStr(). If yes, get_eqc_value return the concrete value.

Please let me know if I could help further. And, we don't have an email list. You could either post your question here or send me an email (zheng16.ad@gmail.com).

Thanks! -Yunhui

yannicnoller commented 8 years ago

Hi Yunhui,

I think my questions or not longer an "issue" of the code, it's more about how the algorithm works, so I'll mail you directly and close the issue.

Thanks a lot, Yannic