Comments (12)
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:
miri/tests/pass-dep/shims/mmap.rs
Lines 31 to 34 in 0970421
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.
Related Issues (20)
- NaN non-determinism for platform intrinsics
- Test that we can build a sysroot for at least all tier 2 targets? HOT 9
- macOS CI often fails with SIGABRT HOT 1
- Detecting races when releasing Tree Borrows protectors? HOT 3
- How to support or disable SIMD instructions? HOT 7
- Running any program on freebsd needs __cxa_thread_atexit_impl HOT 1
- When reads/writes from the borrow model cause data races, the errors are confusing HOT 3
- ICE due to missing struct tail normalization HOT 2
- ICE: InterErrorInfo / Unsupported with `-Zmiri-symbolic-alignment-check`
- Stop recommending cargo clean? HOT 1
- "./miri test" is very slow on repeated executions HOT 7
- CI: Linux test often takes >1h HOT 3
- convert intrinsic shims to intrinsics with fallback bodies HOT 1
- Add direct tests for the Windows RNG functions HOT 2
- Miri does not work with a sysroot built without cfg(miri) HOT 12
- Broken sysroot when custom "release" profile sets `panic="abort"` HOT 7
- miri fmt failing on Windows HOT 7
- Ship Miri on stable toolchains HOT 2
- Execution Traces HOT 3
- miri clippy failing on Windows HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from miri.