Feature request: Translate the bodies of all std functions.

[Nadrieril]

Offshoot of https://github.com/AeneasVerif/charon/issues/545. As noted there, we have the following issue: charon translates information from other crates by using the .rlib file that cargo provides us for each crates. For the crates we build ourselves we pass -Zalways-encode-mir to make sure that the rlib file includes the MIR of all functions. The stdlib rlib file is however pre-built so we can't pass this flag, so some non-generic non-inlineable functions may have no MIR.

Miri is faced with the exact same limitation, and they've solved it for us: running cargo miri setup -v --print-sysroot will build all the built-in crates with full MIR information. We can then pass it to charon by adding --sysroot=the/path/miri/gave/us to rustc_args.

I would like charon to do this automatically. The difficulty here is to do it in a way that's cross-platform and works both inside and outside of Nix. This issue requires some knowledge of Nix. There are three build setups we support:

• Fully without nix, using rustup; that one is easiest;
• Fully within nix, when building the default package and emitting an all-included charon binary; for that my preference would be for the sysroot to be already built as part of the nix build so that charon can just reference it (that's the tricky part);
• Nix-based development within a nix shell; we can usually do the same as above, just have to make sure to add the right env vars to the nix shell. For the non-nix case we should also gracefully fallback to the default sysroot if for some reason miri failed to build its own or if miri isn't installed.

To test if the sysroot is correctly set up, you can run

echo "fn main() {}" > file.rs
cargo build && ./target/debug/charon rustc --start-from=std::process::abort --include=std --print-llbc -- file.rs

If the sysroot is good, the translated abort function will have a body; otherwise not (that's a good test to add to the ui test suite actually).

[N1ark]

One possible flaw of this approach is that cargo miri setup --print-sysroot builds with --cfg miri, meaning the sysroot gets compiled with a bunch of checks we might not necessarily want, or that may use some Miri-only intrinsics; e.g. https://doc.rust-lang.org/src/core/ptr/const_ptr.rs.html#1357-1361. Maybe Charon should to the build itself (?)

[Nadrieril]

Oh wild, I didn't know! Having the same MIR as Miri sounds good though, since this is what ppl use to ensure lack of UB in their projects.

[N1ark]

yep, though im not very fond of the way they just hard-code cfg(miri) into the stdlib, rather than using the pre-existing UB checks nullop/intrinsic which is meant exactly for that i believe :'/

[Nadrieril]

Looking through std, the cfg(miri) I see are for intrinsics::miri_promise_symbolic_alignment, tests, and hiding away os details or inline assembly we don't want to see either. As far as I can tell there are no miri-only checks introduced in this way (maybe there used to be idk).

[N1ark]

There's also this stuff, but yeah tbh i guess it's alright https://github.com/rust-lang/rust/blob/35ebdf9ba1414456dfe1cb6a6b13ebae80e99734/library/core/src/mem/mod.rs#L715-L719