Unix: `munmap` emits "warning: integer-to-pointer cast" about miri HOT 12 CLOSED

Every munmap is an implicit integer-to-pointer cast in the way we have modeled it -- the provenance of the pointer does not matter, only the address does. Making the provenance matter would probably fail some theoretically legal code, though I don't know if that's code anyone would actually write...

Cc @saethlin

from miri.

Yeah this is deliberate and is not well-explained in the code.

I think ideally the thing to do here is to try the munmap with the provenance that's passed in, and if that fails we do from_exposed(ptr.addr()). I think I didn't implement this because we'd need to modify the interpreter to make this particular failure mode possible to recognize directly, or we could just try unexposing on any UB error but that seems dubious.

from miri.

We could also say that if the pointer has some provenance then we enforce it, but if it's a ptr::invalid pointer then we do an int2ptr cast.

What is the usecase for not requiring provenance?

from miri.

If we require provenance then you can't do things like munmap pages returned by multiple mmap calls at once. For example, a memory allocator may grow an allocation by mapping additional pages at the end of said allocation, then munmap the entire page range for that allocation at once when it is deallocated. The man pages strongly indicate that such use is valid, so it would be odd for us to report UB.

from miri.

We don't even support putting new pages at the end of an existing allocation (you cannot map a ta fixed address), so currently this case cannot really occur.

from miri.

Yes, I punted on implementing MAP_FIXED specifically because I thought the tools I'd need to make it happen would land with some of the MMIO work that seemed to be coming.

from miri.

The man pages strongly indicate that such use is valid, so it would be odd for us to report UB.

FWIW this is related to rust-lang/unsafe-code-guidelines#430 -- as of now it doesn't seem entirely clear that Rust allows such in-place growing of allocations.

Yes, I punted on implementing MAP_FIXED specifically because I thought the tools I'd need to make it happen would land with some of the MMIO work that seemed to be coming.

But that means that the code you are worried about wouldn't report UB even if we were to make provenance matter for munmap. It would already fail earlier saying that mmap at a fixed address is unsupported.

So, that's not an argument against making provenance matter.

from miri.

My argument (you originally asked for a use case) is that Miri shouldn't have shims that report UB when the man pages for the shims indicate that such use is valid.

The munmap() system call deletes the mappings for the specified address range

Which I think means that this program is intended to be well-defined and map then unmap an address range:

let ptr = mmap(0, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0);
munmap(ptr.addr(), 4096);

And we have a test for this:

from miri.

As the reporter, is there some way to suppress this single warning, without suppressing all strict provenance warnings?

from miri.

Miri shouldn't have shims that report UB when the man pages for the shims indicate that such use is valid.

I am not at all convinced that the manpage allows your testcase. It is just not written precisely enough to infer much about provenance. If a mapping was created at a fixed address, then I could see the argument that one can munmap it via ptr::invalid(that_fixed_addr) (though honestly requiring that_fixed_addr as *const _ does not seem unreasonable either). But for mappings at dynamically chosen addresses, I don't see a clear license to transmute those addresses through integers and back.

Your testcase would also still pass with the semantics I proposed above. Those semantics do violate provenance monotonicity, but this is all just an approximate model anyway so I'm not too bothered by that.

As the reporter, is there some way to suppress this single warning, without suppressing all strict provenance warnings?

No, unfortunately not. @saethlin is basically arguing that mmap is fundamentally not a strict provenance compatible operation, and that's what Miri currently reflects.

from miri.

Given LLVM behavior such as this and this, I'm less and less convinced that the usage patterns you are describing, @saethlin, are actually permitted in any language that compiles to LLVM. It's true that we don't have any docs that call out the UB, but if the compiler de-facto makes it UB and that's a hard-to-change deep-rooted LLVM assumption, I'd rather have Miri flag such code than risk misbehavior.

So I think we should do full provenance enforcement on the mmap APIs when the addr is not fixed by the caller, and treat them like regular (de)allocation.

from miri.

I agree, though I don't have time in the next 2 weeks or so to make this change.

from miri.