Support memory invalidation in LLVM memory model

[chameco]

Adds a new WriteSource called MemInvalidate. Reading from invalidated memory yields an error with a user-specified message.

This facilitates a saw-script change that should fix the compositional verification soundness bug described in GaloisInc/saw-script#30.

[atomb]

I haven't carefully examined the logic of readMemInvalidate, but I think these changes make sense. It's a simple addition that significantly improves our ability to do sound verification.

[langston-barrett]

This breaks macaw-symbolic, so can't yet be tested against S2N/SAWscript on Fryingpan: http://fryingpan.dev.galois.com/hydra/jobset/s2n/PR-explicit-invalid-write.submodules-ghc865#tabs-jobs

If you create a branch in macaw-symbolic with the same name ("explicit-invalid-write") and update it, the tests will automatically pick up on the changes you make there and build SAW+S2N against both those updates together.

[robdockins]

This looks pretty good to me, except that I think we'll need to expose more memory initialization options. We need to be able to allocate the globals that are mentioned in SAW function preconditions, in addition to "all" globals and just the constant ones.

So, we should probably rename initializeMemory' to just initializeMemory, and rename initializeMemory to initializeAllMemory or something, similar to how we have populateGobals, populateAllGlobals and populateConstantGlobals.

[atomb]

With the naming changes, the crux-llvm build is failing. It should be easy to fix, though: all the references initializeMemory in CruxLLVMMain should become initializeAllMemory. I'd make the change myself, except that the branch is in @chameco's fork of the repo.

Once that's fixed, are there any remaining objections to merging this?