crux-mir: use layout info for tuple aggregates

[spernsteiner]

Currently, TyTuple use MirAggregateRepr (as do the related types TyClosure and TyCoroutineClosure), but fields are laid out sequentially, with each MirAggregateEntry having size 1. This branch changes tuple handling to use real layout information emitted by mir-json. Each field of the tuple is written to the MirAggregate using the actual size and alignment computed by rustc.

Using real offsets introduces a problem related to ZSTs: a zero-sized field can have the same offset as another field. For example, in the type ((), i32), both fields have offset 0. Since MirAggregate can only hold at most one entry for a given offset, writing both fields to offset zero will overwrite one with the other, causing a conflict (this usually appears as a type or size mismatch in mirAggregate_insert). The approach taken here is to omit zero-sized fields from the MirAggregate. For example, ((), i32) is represented by a MirAggregate with only one entry, a BVRepr 32 at offset 0. ZSTs carry no data, so it's always possible to reconstitute them on the fly when read from memory. However, often this is not even needed, since rustc omits loads and stores of zero-sized values.

---

This builds upon #1704 (that PR removed most of the hardcoded size=1 assumptions; this one removes the rest). I also plan to hold off merging this until I have a matching saw-script PR ready to go.

[RyanGlScott]

Looking good!

The mir-json submodule bump brings in the changes from GaloisInc/mir-json#218, right? If so, it would be worth saying as much in the commit message, if only so that it's easier to find this when doing git archaeology later.

In GaloisInc/mir-json#218 (comment), you give an example of a program that accesses uninitialized memory due to certain operations preserving padding bytes. Have you verified that crux-mir does the same? If so, would it be worth adding this as a test case?

Also, you say:

Using real offsets introduces a problem related to ZSTs: a zero-sized field can have the same offset as another field. For example, in the type ((), i32), both fields have offset 0. Since MirAggregate can only hold at most one entry for a given offset, writing both fields to offset zero will overwrite one with the other, causing a conflict (this usually appears as a type or size mismatch in mirAggregate_insert). The approach taken here is to omit zero-sized fields from the MirAggregate. For example, ((), i32) is represented by a MirAggregate with only one entry, a BVRepr 32 at offset 0. ZSTs carry no data, so it's always possible to reconstitute them on the fly when read from memory. However, often this is not even needed, since rustc omits loads and stores of zero-sized values.

This information was not at all obvious to me from reading the patch, and I wonder if this should be documented somewhere, perhaps in the Haddocks for MirAggregate.

[samcowger]

Is it worth panicking if off somehow exceeds the size of the aggregate?

[spernsteiner]

I think it's reasonable for this code to assume that the RegValue is valid for the type. Ideally we would do validity checks much earlier (such as at the point of assignment), like MIRI does.