Use appropriate alignment constraints in LLVM memory model

[brianhuffman]

Changeset c8c1a54 adapts saw-script to a newer crucible-llvm version that has a new Alignment argument on various memory model operations (see GaloisInc/crucible#117). Currently this argument is set to 0 everywhere (byte-alignment, the minimum) but it would be better to use more alignment whenever possible.

(See also GaloisInc/macaw#20.)

[robdockins]

I needed to increase the alignment of newly-allocated regions so that subsequent loads/stores would not fail. In the doAlloc and doAllocConst functions, we're currently using maxAlignment to make sure that the alignment is sufficient for any primitive type.

It's not 100% clear that this is the right thing to do, as we don't explicitly check the alignment of arguments at call sites, etc. To be really precise about this probably requires adding alignment information to the SAWScript specifications. :-/

In the meantime, perhaps a more reasonable default is to use the alignment value computed for the type of memory object being allocated?

[brianhuffman]

After a series of PRs I think we're now using appropriate LLVM alignment values throughout saw-script: #528, #637, #648, #750, and possibly others.

[brianhuffman]

On further investigation, it appears that there are a couple of FIXMEs related to alignment remaining in the code.

saw-script/src/SAWScript/Crucible/LLVM/Override.hs

Line 1331 in 6789b1a

let alignment = Crucible.noAlignment -- default to byte alignment (FIXME)

saw-script/src/SAWScript/Crucible/LLVM/Override.hs

Line 1677 in 6789b1a

let alignment = Crucible.noAlignment -- default to byte alignment (FIXME)

saw-script/src/SAWScript/Crucible/LLVM/Override.hs

Line 1569 in 1c6470d

let alignment = Crucible.noAlignment -- default to byte alignment (FIXME, see #338)

saw-script/src/SAWScript/Crucible/LLVM/Override.hs

Line 2127 in 1c6470d

let alignment = Crucible.noAlignment -- default to byte alignment (FIXME, see #338)

saw-script/src/SAWScript/X86Spec.hs

Line 518 in 6789b1a

let alignment = noAlignment -- default to byte-aligned (FIXME)

saw-script/src/SAWScript/X86Spec.hs

Line 873 in 6789b1a

let alignment = noAlignment -- default to byte-aligned (FIXME)

saw-script/src/SAWScript/X86Spec.hs

Line 917 in 6789b1a

let alignment = noAlignment -- default to byte-aligned (FIXME)

saw-script/src/SAWScript/X86Spec.hs

Line 944 in 6789b1a

let alignment = noAlignment -- default to byte-aligned (FIXME)

saw-script/src/SAWScript/X86Spec.hs

Line 1050 in 6789b1a

let alignment = noAlignment -- default to byte-aligned (FIXME)

saw-script/src/SAWScript/X86Spec.hs

Line 1126 in 6789b1a

let alignment = noAlignment -- default to byte-aligned (FIXME)

We should probably leave this ticket open until we take care of each of those.

[RyanGlScott]

#1539 will add a couple more uses of noAlignment. I'll edit #338 (comment) once #1539 has landed to include them. I'll also update #1539 so that the comments in saw-script refer back to this issue.