Extend SMT backend to use string theory

[peterschrammel]

start with CVC4, Z3

links with front end via #45 and #46

[agriggio]

I've pushed a first attempt at this. I did not go through the Java front-end though, but by using some sort uninterpreted functions in the C front-end. This was because I wasn't able to get the Java part working (after discussing also with @martin-cs). I'm attaching a simple example of how the thing works so far. You can run it (from my fork) like this:

$ ./cbmc/cbmc --smt2 --outfile /tmp/out.smt2 --cvc4 /path/to/test.c

Then you can run cvc4 on the output, and it gives the expected result (unsat):

$ ./cvc4 /tmp/out.smt2

A lot needs to be done of course, and I've only tested a subset of the functions mentioned in cprover-string-hack.h. However, I hope this is enough for you to tell me if I'm going in the right direction.

[agriggio]

test.zip

[agriggio]

I've continued along the lines discussed with martin. I've added support for
an alternative string backend, using arrays with length and quantified
axioms. This is enabled if you use --z3. I've also updated the example and
put it in the repo (under regressions/strings).

Note I'm now working on a smt-strings branch instead of master

As usual, everything is very unstable and likely to crash in many different
ways... there's one example that works though :-)

[agriggio]

I pushed a couple more tests for strings. They are still tiny, but already
enough to show that current solvers aren't very good at handling this kind of
problems. Running regressions/strings/test3/test.c with the Z3 backend
results in an unkonwn answer, whereas CVC4 just seems to take forever.

[agriggio]

I also tried Z3 with built-in string support (i.e. running it on the .smt2 file generated with --cvc4 --smt2 --outfile), but it is as slow as CVC4

[agriggio]

Indeed, as discussed the INT<->BV conversion that is needed for integrating
with CBMC is a major source of difficulty for the solvers. I just committed
two versions of a hand-written SMT2 encoding of test3, one using Ints
directly, and one going through and Int<->BV conversion layer. The former is
solved almost immediately by CVC4, whereas the latter takes forever. I tried
also some other variants of Int<->BV conversion, but with no luck.

Suggestions welcome. In particular, is there a way to use unbounded integers
in CBMC? An alternative could be to check with the CVC4 people how feasible it
is to hack the string theory solver to work on BV directly (if possible by
perserving soundness...)

[agriggio]

quick update. I'm now experimenting with the PASS quantifier instantiation
strategy for solving string constraints as quantified arrays with length. I've
built a simple prototype to start playing with the technique. You can find it
at: https://github.com/agriggio/diffblue-experiments
(see the comment at the beginning of pass.py for instructions)

[agriggio]

Extending Z3str2 with bit-vector constraints:
https://uwspace.uwaterloo.ca/handle/10012/10022

There is a paper at the upcoming SMT'16 about this. Unfortunately, I haven't been able to find the solver and/or the benchmarks online. I'm reading the thesis now

[agriggio]

I have made some progress with my PASS-like prototype (at
https://github.com/agriggio/diffblue-experiments). Now the solver can also say
"sat" in some cases, and not just "unsat". Thanks also to a bug fix in the
encoding, now all the small examples in the regression/strings directory of
(my fork of) cbmc can be solved. This is remarkable because neither Z3 nor
CVC4 can solve all these problems, despite their (apparent?) simplicity.

[agriggio]

Added a bunch of small benchmarks from Z3str2-bv, whose source code in now on bitbucket:
https://bitbucket.org/sanues/z3-str2-bv

Unfortunately, the solver seems to crash quite often for me

[TGWDB]

Closing this as now a sub-goal of #6134.