Track and check alignment for memory regions in llvm overrides

[brianhuffman]

This contains a fix for #635. I'm making a PR now for the automated tests, but I want to also implement a fix for #633 on this branch before it's ready to merge.

[andreistefanescu]

thank you for splitting this in multiple commits, it was easy to review :-)

[andreistefanescu]

maybe show both memTy and memTyAlign

[brianhuffman]

good idea

[brianhuffman]

See revision 950f106

[andreistefanescu]

let's add the test from https://github.com/GaloisInc/saw-script/tree/issue633

[andreistefanescu]

looks good, thank you!

[brianhuffman]

It's not quite ready, as it appears there is a bug in crucible-llvm's isAligned function, where it ignores the alignment of the memory region of the pointer and only checks that the offset part is a multiple of the alignment. Crucible still correctly catches memory writes with insufficient alignment, but it produces the wrong error message, reporting that the "region wasn't allocated, or wasn't mutable" instead of complaining about insufficient alignment.

[robdockins]

Yeah, the check is broken into two phases. The isAllocated check ensures that the base pointer is currently allocated with at least as much alignment as required, while the isAligned function just checks the offset. Aside from the issue with error reporting (which we should fix), I would be surprised if overrides don't check the precondition that pointers are allocated. Is the alignment information not being passed in there?

[brianhuffman]

It turns out that saw-script is not calling isAllocated at all to check that the precondition that input memory regions are all valid. I can very nearly write an unsound "proof" exploiting that, by proving an override for a function that takes a pointer to a scratch buffer: When we use the override, saw-script doesn't bother to check that the pointer to the scratch buffer is valid; however, the invalidateMutableAllocs pass that we do as part of executing overrides will fail when it tries to invalidate a memory region that is not the right size or doesn't exist.

[langston-barrett]

It's unfortunate that we can't have a more specific diagnosis here. The tradeoff for a better API on the Crucible side seems to be that we and more predicates together, losing some granularity in the assertions.