z3 string support update

[natsteven]

• Added support for StringBuilder methods: delete, insert, and reverse.

• Fixed translation semantics for replacement. Where Java defaults to replaceAll the smt-lib 'str.replace' operator is a replaceFirst operation.

• Changed isEmpty translation to '(= 0 (str.len' as 'empty' is not an smt-lib supported predicate

• Added smt-lib case conversion support for z3 satisfiability checks as recursive functions. This was implemented before seeing the current handling of case conversion by SPF and I am not sure that it would be preferable.

[sohah]

Thank you @natsteven for your pull request. But can you please add test cases under the examples folder, together with its corresponding .jpf configuration file that shows the effect of the changes of this PR?
Also, can you please also clarify which recursive function are you talking about in the 4th point of the list of changes? Can you be more specific about it.

Thank you

[natsteven]

Hi @sohah, yes I will include the simple test cases I was using for the additional method support I added. I might not be able to get to it for several days though.

On the point of the case-conversion. I set up translation of toLowerCase() and toUpperCase() operations directly to smt-lib. That is, in Z3Translator.java I define recursive functions in smt-lib that model the above operations and add them to the smt query. This worked for the tests that I ran that included those string methods and called z3tr3.

However, it looks like in the sv-comp branch there has been some additional work done on handling the case conversion operations as part of the path constraint handling in SymbolicStringHandler.java. It seems to me that the route I took is fundamentally different from the implementation that is currently present using, for example, the handleToLowerCase() method. I have not had the chance to test that alternative implementation so I am not sure which one would be preferable either performatively or design-wise. I only know that my implementation works as expected for handling those methods and do not know whether the current handling works or how it effects the semantics of the query. Hopefully that makes things a bit clearer.

Thanks!