Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Enable miri testing #45

Closed
wants to merge 3 commits into from
Closed

Enable miri testing #45

wants to merge 3 commits into from

Conversation

h33p
Copy link
Contributor

@h33p h33p commented Mar 28, 2023

This enables use of miri to check for correctness of the codebase at MIR level. miri allows you to be more sure of soundness of your unsafe blocks.

The first thing that had to be changed is use of libc::mmap for NockStack. I changed it to the system allocator. Now, I'm aware that there is some special care taken to prevent system allocations, but I don't think I know the full story, so I'm not so sure what the difference is between calling mmap directly or invoking alloc::alloc, but what I know is that libc::mmap (or any third party lib) is not usable under miri, so allocation code needs to be somewhat generic to work (if using libc::mmap is a must, it can be worked around with #[cfg(miri)]).

The second thing is pointer handling. If you were to run cargo +nightly miri test on the first two commits, you'd get errors about dangling pointers, which occur because pointers to the stack get built from integers without provenance data. Pointer provenance is a bit of a complicated subject, but it basically boils down to "keeping track of which allocation it came from", which I guess is always going to be the NockStack it resides in. If you don't track provenance, probably not much is going to happen today, but compilers, especially rustc, are likely to start to rely on pointer provenance to enable some tricky optimizations leading to very subtle miscompilations down the road. There is also an existing rustc experiment, which probably won't get anywhere in the next 5 years, but still worth mentioning: rust-lang/rust#95228.

The third commit restores provenance to the pointers. This could potentially work under -Zmiri-strict-provenance, but there are issues with noun tags:

running 27 tests
test jets::math::tests::test_add ... error: unsupported operation: integer-to-pointer casts and `ptr::from_exposed_addr` are not supported with `-Zmiri-strict-provenance`
   --> src/noun.rs:253:9
    |
253 |         (self.0 << 3) as *const u64
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^ integer-to-pointer casts and `ptr::from_exposed_addr` are not supported with `-Zmiri-strict-provenance`

To fix this we'd want to swap the tagging around to add bits to direct nouns rather than other way around, but that's another problem on its own.

The question is how useful is this? I'd say this will prevent subtle miscompilations many years down the road, plus any potential memory issues stemming from use of unsafe.

@eamsden
Copy link
Collaborator

eamsden commented Apr 11, 2023

I'm willing to look over this more but FFR I'm highly unlikely to merge such a large change unsolicited and without extended discussion. Feel free to message me on the network and we can set up some time to look it over.

@h33p h33p closed this Apr 22, 2023
@h33p h33p mentioned this pull request Apr 22, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants