Implement simple string methods

[Rik-de-Kort]

This PR continues work on #39

[Rik-de-Kort]

Here's an example that produces the wrong result. It appears to work find with ASCII. Do we have to hold off on implementing this until we can get full unicode support in SmtStr/z3?

import z3
from crosshair.libimpl.builtinslib import SmtStr
from crosshair.statespace import SimpleStateSpace, StateSpaceContext
import crosshair.core_and_libs 

space = SimpleStateSpace()
with StateSpaceContext(space):
    s = SmtStr(z3.StringVal('Â'))
    print(s.join(['a', 'b', 'c']), 'Â'.join(['a', 'b', 'c']))

Output

a\u{ffffffc2}b\u{ffffffc2}c aÂbÂc

[pschanely]

My experience is that at least our version of z3 has issues with unicode, and have been working under the idea that (for the moment) SmtStr is only for ASCII. (well, technically a little larger - the codepoints 0-255)

You may have noticed that I'm using sequences of bitvectors in places to try and keep z3 from attempting to use other values.

In spite of this restriction, I think we should always consider it a bug if Crosshair produces a counterexample that doesn't reproduce.

[pschanely]

A heads-up (and apology). I'm trying to make the naming less confusing: 8f87df3 performs a large rename of Smt* to Symbolic*. So you'll have to rebase and resolve some conflicts - sorry!

[Rik-de-Kort]

A heads-up (and apology). I'm trying to make the naming less confusing: 8f87df3 performs a large rename of Smt* to Symbolic*. So you'll have to rebase and resolve some conflicts - sorry!

No problem, I think it's a great idea!

[Rik-de-Kort]

My experience is that at least our version of z3 has issues with unicode, and have been working under the idea that (for the moment) SmtStr is only for ASCII. (well, technically a little larger - the codepoints 0-255)

You may have noticed that I'm using sequences of bitvectors in places to try and keep z3 from attempting to use other values.

Based on a very brief excursion into the land of z3 and unicode, the issue appears whenever we try to materialize a string value (for instance, by printing it). I think for now not something I want to spend an inordinate amount of time on.

I'll continue on with the string methods and ping you when done.

[Rik-de-Kort]

@pschanely any idea why CrossHair can find the counterexample on 3.8 but not on 3.7?

[pschanely]

OK - apologies for the delays here!
I think the test_partition_ok and test_rpartition_ok issues are coming from a bug in the patching mechanism; they pass for me with a fix I just pushed in c7b658c.

test_rpartition_fail is more strange - I see an unknown satisfiability result from Z3 in the log, which happens where I'd expect to find the counterexample. I am less sure what to do here, but I'll continue to poke at it.

[pschanely]

Ah, silly me, test_rpartition_fail just needs a little more time. (string reasoning is expensive I suppose!) For now, you can do something like this:

self.assertEqual(*check_fail(f, AnalysisOptionSet(per_path_timeout=5)))

per_path_timeout controls the max seconds we'll spend on a single execution before giving up.
per_condition_timeout controls the max seconds we'll spend over all executions for checking one postcondition.

[Rik-de-Kort]

Thanks for the help! I don't think it's a good idea to add a flaky test and then rely on the timeout for it to pass (because that can still be ruined by poor computation speed), so I've taken it out for now. Maybe in some next PR we'll do some performance benchmarking, eh?

I think I'd like to call this ready for merging. Let me know if I need to do anything else about it. :)

[pschanely]

Amazing. This is a lot of stuff! A few minor comments.

Sounds good on the testing. Later this week, I'd like to forward you a potential new test pattern for how we might expand our coverage, reduce flakes, and improve test time. I'd be curious about your opinions on it!

[Rik-de-Kort]

Thanks for the review. Definitely up for having a look at the test pattern. :)