Fix `attempted to read from stolen value`

[W95Psp]

The frontend browses items of a crate in an order that causes this bug. Some data in the Rust compiler is kept in a Steal, which is basically a box whose content can be stolen, that is pulled out of the memory (rustc uses arenas)

Thus, the order in which we browse the crate to export every item matters: sometimes I inspect things that happens to be stolen before because of some previous inspections. This is particularly true for constants, it seems.

Status: mostly fixed

• @geonnave's bug (https://github.com/hacspec/hacspec-v2/issues/27#issuecomment-1568365024) is fixed
• @franziskuskiefer's bug (https://github.com/hacspec/hacspec-v2/issues/27#issuecomment-1586990315) is fixed

However, I tried Hax on core, and I get new stolen stuff. Thus, there exists some scenarios in which this still fails.

[geonnave]

For the record (context from #99):

• this issue also affects translation of the edhoc-rs crate into fstar.
• in #99 there is a How to reproduce section, that could be validated against once this issue is addressed.

[franziskuskiefer]

Another code snippet that panics

#[repr(u16)]
pub enum ProtocolVersion {
    Mls10 = 1,
}

impl ProtocolVersion {
    #[allow(non_upper_case_globals)]
    fn tls_deserialize(bytes: &[u8]) -> core::result::Result<(Self, &[u8]), tls_codec::Error> {
        const __TLS_CODEC_Mls10: u16 = ProtocolVersion::Mls10 as u16;
        let (discriminant, remainder) =
            <u16 as tls_codec::DeserializeBytes>::tls_deserialize(bytes)?;
        match discriminant {
            __TLS_CODEC_Mls10 => {
                let result = ProtocolVersion::Mls10 {};
                Ok((result, remainder))
            }
            _ => Err(tls_codec::Error::UnknownValue(discriminant.into())),
        }
    }
}

[W95Psp]

Another stealing bug (from issue #474):

https://github.com/hacspec/hax/blob/aa14fb139280e7fcd28acb45db27b01b53c9de93/tests/rust-ast/src/lib.rs#L14-L20

Originally posted by @franziskuskiefer in https://github.com/hacspec/hax/issues/474#issuecomment-1916302172

Open this code snippet in the playground

Status: works OK in 8ab62258df ✅

[franziskuskiefer]

It looks like the two examples here are not triggering the stealing bug anymore.

[Nadrieril]

My current understanding of stealing insofar as it affects us:

• THIR is stolen to construct the built MIR;
• the built MIR is stolen to construct the optimized or ctfe MIRs;
• optimized/ctfe MIR is required to evaluate constants, which happens if a constant shows up as a const generic argument, as a pattern, inside another evaluated constant, inside a MIR body that is being optimized, and likely other cases.

Hence even translating a type may steal a THIR/MIR body.

[W95Psp]

Yes, exactly, that's what is happening :( Thus it's not even clear we can come up with a visit order of items that would avoid stealing issues...

[Nadrieril]

If we could detect whether a value is already stolen, we could fallback to the optimized MIR/evaluated value for constants.

[Nadrieril]

Opened https://github.com/rust-lang/rust/pull/128815

[W95Psp]

reproducer for a stealing bug with cargo hax into -k mir-built: https://hax-playground.cryspen.com/#json+mir/a339b28377/gist=6630144c4732a2bd55ef8ded02b30ef6

(I haven't shown you the playground yet @Nadrieril, right? :smiley: 'right click > show MIR' on a rust subexpression might be interesting to you :D)

[Nadrieril]

You should now be able to fix all MIR stealing bugs by using the optimized_mir when tcx.mir_built().is_stolen(). For THIR bodies I don't think there's a good solution.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[franziskuskiefer]

I can't reproduce with any of the examples in here. Unless we have a reproducer, let's close this and open something new when we hit it again.

[W95Psp]

We were discussing that yesterday with @Nadrieril: he found a way to override queries, which basically means we can just reimplement the code that used to do the stealing! 🥳

But indeed, on the THIR side of things, same thing for me, no stealing for a long time! And it's worth noting that we had no stealing issue extracting top 10k crates.io.

[franziskuskiefer]

This is still an issue (see linked libcrux issue above).

[Nadrieril]

You could solve these issues for good by overriding queries to catch the THIR directly after it is built. See here an example in Creusot that reliably catches the mir_built in this way.

[karthikbhargavan]

This fix still needs to be upstreamed to hax from hax-evit, so maybe keep this open?

[Nadrieril]

Out of curiosity, how did you fix it?