minirust
minirust copied to clipboard
RalfJung
A precise specification for "Rust lite / MIR plus"
See [this Zulip thread](https://rust-lang.zulipchat.com/#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/SB.20UnsafeCell.20.2B.20exhaustiveness.20check.20.2B.20layout.20opts) for a bunch of discussion. The short summary is that currently one can write non-UB code which enters a `x & Some(_)` arm where in that...
Rust intrinsics are basically primitive operations of the language. So I think it makes most sense to add them as (unary or binary) operators to MiniRust, or possibly as statements...
We don't support encoding or decoding enums yet. Some interesting questions will arise when adding them. Relevant material: - https://github.com/camelid/type-layout by @camelid - [a very WIP writeup](https://hackmd.io/@2S4Crel_Q9OwC_vamlwXmw/By4FoVud9) by @JakobDegen suggesting...
So far we only support pairs, not tuples with an arbitrary number of fields. That's just laziness though, and should not be hard to fix.
So far we only support 16-bit integers. That's just laziness, I wanted to ensure that we handle endianess but not write the code for arbitrary-width handling.
One of the things I am least sure about is how to best add support for unsized types to MiniRust. Clearly `Pointer` should optionally carry some `metadata`, but what do...
This PR implements part of #1. It adds optional metadata in the pointer value and the place representation. Slices' subslice is not supported yet. In MIRI, it seems to be...
We need some maths to make the non-determinism used by MiniRust fully precise -- it's the one thing code cannot describe. Or maybe it can but then we need some...
Currently WF-check just returns "no" when it fails, which is not very friendly. It should say what went wrong, and ideally also where.