Remove use of uninterpreted functions from memory model in favor of explicit assertions

[danmatichuk]

Bitvector operations in the memory model potentially have undefined results when mixing pointers from different regions. Currently this is handled by emitting uninterpreted functions when the result of an operation is not statically known to be defined. The advantage of this approach is that we can handle the case where two pointers are potentially undefined, but we can still prove that they are equal (i.e. we can prove that even if undefined, it will have the same undefined value in both programs).

A significant limitation with this approach is that we are unable to propagate concrete information about pointers in the case where they may potentially resolve to an undefined value. For example, we may have a pointer 3+0x02 and add an offset A+0x03 where Ais a free variable representing a symbolic region. If we add these pointers together, the resulting expression is as follows:if (A == 3 || A == 0) then 3+0x05 else uf_addInt(3,A)+uf_addBV(0x02,0x03)`.

Since the resulting pointer is not necessarily in region 3 (in the case where A is not 0 or 3), we lose precision in our analysis.
Recognizing that these undefined values almost certainly represent infeasible program paths, it is much more preferable to continue our analysis under the assumption that they don't actually appear, and defer this proof (either to be solved later or admitted as a top-level assumption).

[thebendavis]

completed