Add hooks to memory reads about memory offsets

[fortunac]

Related to #93. We initially expressed memory offsets as quantifiers added to the hypothesis, but this created a slowdown with Z3.

Instead, we should be adding hooks to memory reads (currently unsure if we need writes) for both the stack and heap in the form of the constraints:

Heap(x) => init_mem_orig[x] == init_mem_mod[x + d]

and

Stack(x) => init_mem_orig[x] == init_mem_mod[x]

where d is some offset that can be inputted as a parameter.

init_mem_orig and init_mem_mod are fresh variables generated prior to running wp, and init_mem_orig == mem_orig and init_mem_mod == mem_mod should be added to the hypothesis. The user should also be able to use #101 to express precondition about the initial memory.

We still need to assert that Stack(SP) is pointing to a valid location on the stack. It is unclear whether we should say that SP is at the top of the stack, in the top region of the stack, or any other notion of it being valid.

[fortunac]

Handled in #107