creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.
GNU Lesser General Public License v2.1
1.14k stars 50 forks source link

Weird span changes in RBT #631

Closed xldenis closed 1 year ago

xldenis commented 2 years ago

Unrelated changes to creusot-contracts can cause linenumbers of spans in Red Black Tree to change.. Investigating this would be highly worthwhile. @jhjourdan emitted the hypothesis that this could be due to serialization, since we've seen it before, and it would be a leading candidate. No idea where to start investigating.

xldenis commented 1 year ago

Ok I think i've identified the posdible cause / effect relation. My suspicion is that our metadata encoding is causing collisions with the spans of creusot-contracts and other crates. The reason we only see this for red_black_tree is that it is the only long enough test to have a meaningful overlap. This would explain why the diff of spans corresponds to the size of changes that occured in creusot-contracts.

Looking at the code for encoding and decoding spans, it also seems like a likely culprit:

The default implementation of Encodable for Span seems totally completely broken:

impl<E: Encoder> Encodable<E> for Span {
    default fn encode(&self, s: &mut E) {
        let span = self.data();
        span.lo.encode(s);
        span.hi.encode(s);
    }
}

A span is a pair of absolute indices into the concatenated bytestream of the files in a crate. This implementation provides no way to recover which file this is supposed to be a span into.

This is made evident by the fact that the 'real' implementations used by rustc in Encoder and Decoder take a much more complex route which in particular saves spans as relative positions into a specific file. While rustc is also trying to squeeze out every ounce of performance from metadata decoding/encoding, I think if we provide better implementations for spans that turn them into SourceFile, usize,usize that will fix the bug we encounter today.