Fix a bug in the LLVM memory model (with SMT array backed allocations)

[travitch]

Most of this commit is additional comments that try to clarify some of the
things that came up while diagnosing the bug. The actual fix is in
writeMemWithAllocationCheck.

The observed behavior was that a test case (in another repository) generated
formulas where reads and writes to SMT array-backed allocations did not refer to
the same byte offsets, when they should have. Specifically, the scenario was
that the test case has a single large allocation backed by an SMT array. The
function exhibiting the problem started with a pointer to the middle of that
allocation. Some of the reads and writes were properly in the middle of the
allocation (with a large offset appearing in SMT array select operations),
while others were using inappropriate low offsets (around zero).

The problem was a bug in the optimization in the memory model that coalesces
writes to SMT array backed allocations (which reduces the number of muxes
generated in many cases). The goal of this optimization (which is now
documented) is to turn sequential updates to an SMT array backed allocation into
a single entry in the write log by pretending that the small write actually
overwrites the entire SMT array with new values (which are the original contents
of the SMT array plus the new values just written, expressed as an SMT array
update).

To do this correctly, the updated array must overwrite the entire
allocation (i.e., starting at offset 0 within the block). The bug was that the
array was being written at the offset in the pointer to the start of the new
write. In the case outlined above, this meant that the new array was spliced
over the old one halfway through the allocation. This had a few consequences:

• The offsets of reads no longer matched the offsets of their corresponding
  writes (due to the intricacies of how read offsets are calculated in SMT array
  allocations)
• The expected optimized path for array reads was no longer taken, as writes
  looked like they spanned two different array allocations
• The ultimate SMT queries actually had no update operations in them at all
  because the reads looked independent of all of the writes (due to the
  misalignment)

[kquick]

The additional documentation really helps, thanks!

[robdockins]

Nice catch, that's a subtle bug! How hard would it be to add a test case for this situation?

[travitch]

I tried - the previous test I added attempted to trigger this (a simplified version of the real program), but some of the optimizations in the memory model ended up eliminating all of the actual memory options. Andrei said he thinks he can cook up a test case that will tickle it.

[andreistefanescu]

@travitch the problem was that asMemAllocationArrayStore did not check that the pointer offset is 0, thus incorrectly identifying an array store at an incorrect pointer as covering the entire allocation (yes, in this case, two wrongs make a right).