Progress on Mr. Solver SHA512 example

[m-yac]

This PR contains initial progress on getting a SHA512 example working with Mr. Solver. Aside from adding this example to the Heapster examples directory, it contains the following changes.

• Add proper handling of vector literals to Mr. Solver. This mostly involved adding a case to smtNormPrims for genBVVecFromVec of a vector literal, which turns the term into a genBVVec of a large chain of ites. It also involved adding more general cases for atM and updateM to normComp.
• Add a case to askMRSolverH for a BVVec on one side but a Vec on the other. This involved adding a genFromBVVec function to the prelude, which is unfolded during the SMT step in smtNormPrims.
• (d166857) In getDetVarsClauses, determinedVars, etc, instead of keeping track of seen determined vars as a NameSet, keep track of them as a NameMap to the list of DetVarsClauses they determine. This fixes a bug where a variable was not getting considered determined because the variable which determines it was already seen, but in a context where it was not determined. By keeping track of the determined vars for each seen variable, it allows us to figure our first variable is determined in the former context.
• (6c3ab4d) Modify suitableAP such to check that either the borrows of the two permissions are equal or the range [off,len) is not fully borrowed, instead of just the latter. This fixes a bug where we were unable to prove x -o x for a fully borrowed array permission x.

Sorry this PR is so many changes lumped together! In the future I will try to keep PRs limited to single changes.

[eddywestbrook]

This all looks good, thanks Matt!