Fix the semantics of strlen on symbolic strings.

[robdockins]

Previously, strlen would recurse down a string until it
ran into a concrete zero. This is fine, except that it would
assert that each load along the way would succeed, without taking
into account the previous zero tests that had to fail. To correct
this we need to emulate a path condition such that to load
at position n each of the n-1 previous locations must have
been non-zero, and the loads are only required to succeed under
that condition. This allows one, for example, to assume that
some value in a string is 0 (but not specify which one). Previously,
strlen would index off the end of the allocation of such a string
and fail. Now it will succeed because the path condition required
to index out-of-bounds is inconsistent.

Fixes #468

[weaversa]

This allows one, for example, to assume that some value in a string is 0 (but not specify which one).

Oh I like that!

I hate to ask, but is strlen the only function that has this kind of problem?

[robdockins]

I hate to ask, but is strlen the only function that has this kind of problem?

I think so. memcpy, memmove and memset are all memory model primitives, so they don't have this issue. All the other functions that deal with strings require the bytes to be fully concrete

If we want to support more of "string.h" we'd arguably be better off providing a library of naive C implementations to avoid running into this issue again.