Open joboet opened 7 months ago
LLVM has plenty of bugs around with_exposed_provenance_mut
, see e.g. https://github.com/llvm/llvm-project/issues/33896. They don't have a clear enough semantics to even be able to evaluate what the fix should look like -- they first need to decide how provenance interacts with the iN
type, and how "exposed" works. Not sure if and how we should track that on our side.
Furthermore, if you run that program in Miri you already get a warning that you are outside the scope where Miri can reliably detect bugs (or you silenced that warning by passing -Zmiri-permissive-provenance
).
Adding something like a black_box to both expose_provenance and with_exposed_provenance that tells LLVM "this does something funky (but results in a pointer with the given address)"
Yes, IMO we should do that some time after strict provenance stabilization (also for as
casts between pointers and integers).
Per miri's (temporary) "wildcard"-provenance model, this code is considered sound (playground):
Also note that wildcard provenance is not a sound model. So Miri accepting unsound code is entirely expected. That's why Miri shows a warning when your program does an int2ptr cast. So the part about Miri not showing UB for this program is entirely not-a-bug works-as-intended. There are examples of programs Miri will accept that are unambiguously UB under Rust semantics. That's why strict provenance is a thing -- to let people write code that does messy pointer things while still enabling Miri to reliably find bugs.
Wildcard provenance is a Miri-specific concept and not part of the Rust specification in any way.
However, your program does not just pass Miri, it is actually sound under the intended actual model of with_exposed_provenance_mut
, the one sketched in that function's documentation. That's why this is concerning.
Rust adopting a different model for exposed provenance
Wildcard provenance is not Rust's model for exposed provenance. Rust's model for exposed provenance is describred in the with_exposed_provenance_mut
docs.
Per miri's (temporary) "wildcard"-provenance model, this code is considered sound (playground):
However, LLVM folds the
with_exposed_provenance_mut
call tonull
and thus creates undefined behaviour.Personally, I'd argue that this should be considered an LLVM bug: the LangRef states that:
though this contradicts with:
However, I'm filing this here, as it seems bad that miri doesn't report this and it seems unlikely to me that LLVM would fix this, as doing so would probably result in regressions for C code doing the equivalent of
map_addr
.I think this would be best fixed by:
with_exposed_provenance
be pure is a cool property)expose_provenance
andwith_exposed_provenance
black_box
to bothexpose_provenance
andwith_exposed_provenance
that tells LLVM "this does something funky (but results in a pointer with the given address)"