Add support for SMT array backed pointers in writeMemWithAllocationCheck

[bboston7]

This pull request adds support for pointer values backed by SMT arrays in writeMemWithAllocationCheck, which would previously generate failing goals for this case.

[travitch]

How hard would it be to add a test?

It could just:

1. Malloc two blocks
2. Store the second pointer into the first block
3. Read the pointer back
4. Assert that the symbolic value read from the original pointer vs the read pointer produce an identical result

[bboston7]

It seems like it shouldn't be hard to add that test. I'll add it.

[bboston7]

@travitch The changes I just pushed up add the test you mentioned.

[travitch]

Thanks! I'll defer to @andreistefanescu for the review, but it looks good to me

[robdockins]

If I understand correctly, this will cause the SMT array to no longer be used for writes once a pointer is written into that block. I don't know if that is the behavior you want. Presumably, if you were OK with that, you wouldn't be using SMT arrays in the first place.

[travitch]

Yes, it isn't ideal for sure. Without this change, the memory model just asserts false, which is somewhat less helpful. There is currently nowhere to store the (symbolic) block ID in the memory model. I'm hoping to address that soon to avoid the need for this case.

[andreistefanescu]

👍