Heapster memblock prover improvements

[eddywestbrook]

Added a number of improvements to how the implication prover handles memblock permissions. Specifically:

• Changed implElimLLVMBlock to only perform one step of elimination for memblock permissions

• Added more comments to implElimLLVMBlock

• Added implElimAppendIthLLVMBlock, which calls implElimLLVMBlock and then appends its results to the conjunctive permission on top of the stack

• Added implIntroOrShapeMultiM to allow multiple nested or shapes to be all proved at once

• Changed proveVarLLVMBlocks to use the new implElimAppendIthLLVMBlock when it eliminates memblock permissions to allow it to call itself again rather than calling implElimPopIthLLVMBlock and then going all the way to the top of proveVarImpl

• Added the notion of a tagged union shape, which is a multi-way nested or shape of the form sh1 orsh ... orsh shn where each shi starts with an equality permission to a concrete bitvector value that represents a tag for that disjunct. Also added implication prover for recognizing when we are trying to prove a tagged union shape and already know which tag to choose, in which case we avoid doing the search across all n disjuncts and instead choose the right one from the beginning.

• Added debug output for type-checking return statements

[glguy]

It's not a new change, but while we're looking at this function, it would be nice if we weren't duplicating mbMatch $ fmap llvmBlockShape mb_bp so much. Each of these could be redoing the work of converting to pair representation.

This whole function could potentially benefit from doing a single [nuMP| mb_bp : mb_bps |] pattern and handling the cases under that.

[eddywestbrook]

Well, I started to look at how to implement this change, and it led to a fair bit of reorganizing proveVarLLVMBlocks. The main changes are that it is now organized into two separate stages, represented by two separate functions, where the second stage / function takes a MatchedMb for the shape as an explicit argument.

Another change is that these functions now take lists of multi-bindings instead of multi-bindings of lists. The justification is that those lists are always going to be converted to pair form and matched against anyway, so we might as well do that to begin with. Plus, there are a number of recursive calls that cons or prepend to those lists, and before they had to do this with fmap, which converts back to function form and then again to pair form, while now this conversion has been removed. Because one of the main concerns with this change is performance, I did in fact time running Heapster on the rust_data example before and after the change, and it seems to improve performance slightly, on the order of .1 - .2 seconds out of 17 seconds for the entire test. So I think that's a win?