crucible_llvm_verify produces too-complicated proof goals for isAllocated tests

[brianhuffman]

Specifically, this refers to goals with names/descriptions that include "the region wasn't allocated". These goals contain terms which are essentially the saw-core translation of a cryptol expression like this:

(((4 * i <= 4 + 4 * i) /\ (4 <= 4 + 4 * i)) \/ (0 == 4 + 4 * i)) /\ (4 + 4 * i <= 400)

Here 400 is the size of the allocation, 4 is the size of the memory load or store, and 4 * i is the offset of the pointer. The formula is supposed to state that the sequence of addresses [4*i .. 4+4*i) lies entirely within the range [0 .. 400).

This is way too complicated. We should generate a much simpler formula instead.

[brianhuffman]

I think it would suffice to check two properties:

• The size of the load/store is no larger than the allocation size: size <= alloc_size
• The offset of the pointer at least size bytes below the top of the allocation: offset <= alloc_size - size. Note that the first property ensures that the subtraction will not underflow.

So in the case of size = 4, alloc_size = 400, and offset = 4*i, we would have a proof obligation of

  (4 <= 400) /\ (4 * i <= 396)

which is a bit simpler than the one above. Furthermore, the first conjunct is usually a comparison of two concrete values and will simplify away.