Provide the ability to "promise" alignment under miri-symbolic-alignment

[joshlf]

Symbolic alignment checking is very useful, but subject to false positives such as this one. It'd be great if there were a way to be able to run Miri with symbolic alignment enabled in order to get its benefits in most of the code and just disable it in specific locations - ie, by "promising" that a particular address is known to always have a particular alignment. I'm not sure what this API would look like, but it'd be great if there were some way to express this.

[RalfJung]

Symbolic alignment checking is very useful,

That's great to know, I was wondering if this feature is even worth keeping! Looks like the answer is "yes", then.

It'd be great if there were a way to be able to run Miri with symbolic alignment enabled in order to get its benefits in most of the code and just disable it in specific locations - ie, by "promising" that a particular address is known to always have a particular alignment. I'm not sure what this API would look like, but it'd be great if there were some way to express this.

Miri supports magic extern fn that can be used to interact directly with the interpreter. So those could be used to do... something with symbolic alignment. However, I don't see how "this pointer is aligned" should work in general, as that can lead to general-purpose arithmetic reasoning: if base_addr is 2-aligned, and base_addr + 10 is aligned to 8, and now we see an access to base_addr + 14, then we'd have to be smart enough to know that this is 4-aligned...

[joshlf]

Ah, I was just thinking that you'd be able to make very limited statements like "I promise this pointer is aligned to alignment N", and then Miri would track that so that future uses of that pointer which require alignment N would succeed. It'd be fine if Miri didn't support all arithmetic reasoning that is in principle possible to deduce from that fact.

Another way I could imagine doing this would be: When you convert from something like NonNull<u8> to NonNull<T> (as we do in the example I linked to in my original comment), you could tell Miri "make the same alignment assumptions you'd make if I derived this NonNull<T> from a &T". In other words, it seems to me that Miri already supports keeping track of this kind of information - for example when the symbolic alignment check allows you to go from &T to NonNull<T> and not "forget" that it's aligned - and so we could just reuse that machinery here.

[RalfJung]

The current symbolic check isn't really helpful here. It works as follows: for each allocation, we remember the alignment that was requested for it. (We anyway need to remember this to ensure that the same alignment is given on deallocation.) When a memory access occurs, we anyway need to determine which allocation it affects and at which relative offset. Then we check:

• Is the allocation alignment at least as large as the requested access alignment?
• Is the relative offset divisible by the requested access alignment?

If both of these pass, we know that the access is aligned independent of the concrete absolute base address that was picked for this allocation.

However, when you have some arbitrary pointer at arbitrary offset into some allocation and tell us "consider this to be 4-aligned", that doesn't really help.

I think we would have to store, for each allocation, information of the form "the base, when divided by X, has remainder Y". The current situation corresponds to Y always being 0. Then we could check:

• Is X at least as large as the requested access alignment?
• Is (Y + the relative offset) divisible by the requested access alignment?

When a pointer is "promised", we need to compute suitable values for X and Y.

[joshlf]

Symbolic alignment checking is very useful,

That's great to know, I was wondering if this feature is even worth keeping! Looks like the answer is "yes", then.

Bad news, we ended up deciding it was more complexity and CI execution time than it's worth to keep using symbolic alignment checking 🙁 While we try to take an approach of throwing the kitchen sink at zerocopy (in terms of testing correctness and soundness), there's not a great argument for symbolic alignment checking in particular because most of our code either performs a &T -> &[u8] conversion or a runtime-checked &[u8] -> &T conversion. Our only &T -> &U conversion is transmute_ref!, and it has UI tests that ensure compilation fails in cases where Miri's symbolic alignment check would fire.

We're specifically disabling it in this PR.

[RalfJung]

That's fine, thanks for the update! This is still an interesting idea I think, specifically for align_to. If we can have the symbolic alignment check "learn" about alignment detected by align_to, then we would not have to make align_to return "impossible" results.

[joshlf]

Yeah we'd definitely re-enable symbolic alignment checking if it were feasible! But I also don't want to signal that it's super important for us if that's going to affect your prioritization of various work on Miri.