Heapster memblock prover improvements (#1406)

* bugfix: there was an infinite loop that kept copying a block permission before eliminating it and would then go right back to trying to eliminate that same permission again...

* added debug output for return statements, which is long overdue

* changed implElimLLVMBlock to always only eliminate one step of a memblock permission; changed proveVarLLVMBlocks to focus first on eliminating memblock permissions on the left that overlap with but are not contained in memblock permissions on the right

* unfold defined shapes on the left when their ranges match a shape we are trying to prove on the right

* whoops, do not try to eliminate LHS block perms when we are proving an empty block perm on the right

* added a case to proveVarLLVMBlocks to detect if the right-hand side is a tagged union type where we already know from something on the left what the tag is, in which case we can avoid searching for proofs of all the disjuncts other than the one that matches that known tag

* added another special case to proveVarLLVMBlocks, to eliminate a sequence shape sh;emptysh with the empty shape when necessary

* reorganized proveVarLLVMBlocks into two separate stages represented by two separate functions, all of which now take lists of multi-bindings instead of multi-bindings of lists

* whoops, forgot to change a shadowed variable...

* implemented a few more suggestions from Eric Mertens