charon icon indicating copy to clipboard operation
charon copied to clipboard

Bug: Properly `drop`ping

Open ssyram opened this issue 8 months ago • 1 comments

Currently, the drop statements in the translated LLBC are not working properly. Particularly:

  1. It is often called for types like unit, i32 or so, which is dummy;
  2. The calling positions are messy and not predictable -- often, it is absent in places it should happen, but appears in places it should not;
  3. Multiple drop for the same variable also happens. To sum up, I think the drops in LLBC are not informative.

On the other hand, I think MIR has already provided pretty good drop support -- take the following as an example:

fn test_move() {
    let d = gen_some_movable_and_droppable();
    if complex_compute() {
        use_move(d);
    }
}

So the MIR will generate a variable to track whether d is moved -- if it is, there will be no drop calling for d, otherwise, d is dropped. Interestingly, if the type of d does not implement Drop, there will be no variable to track this. I think this is already a pretty good support for dropping. I tested this in https://play.rust-lang.org .

But I did not see anything in LLBC trying to replicate these efforts. I guess this is especially important for Eurydice to properly translate heap object releasing and file-related operations, right?

ssyram avatar Apr 09 '25 08:04 ssyram

Hi! Yep, this is an artefact of us using an early version of MIR. We absolutely would like correct drops, see #152. We're working on it, it's a current priority.

Nadrieril avatar Apr 09 '25 09:04 Nadrieril

Has this issue been resolved? I found the current version with --mir elaborated seems to work properly.

ssyram avatar May 21 '25 12:05 ssyram

It's indeed pretty much resolved by --mir elaborated, but I'd like to make that the default before closing the issue

Nadrieril avatar May 21 '25 13:05 Nadrieril

I'm glad --mir elaborated is working well for you!

Nadrieril avatar May 21 '25 13:05 Nadrieril

Thanks! This really helps! Btw, is there still some known issue with this functionality? E.g., potential limitation or bugs? I guess, stemming from its technical origin, the drop here should be pretty much the same as how Rustc is actually doing (if not exactly?)?

ssyram avatar May 21 '25 14:05 ssyram

It's be exactly the same drops as rustc, since it's rustc who gives them to us. One limitation is #684 which is tracked separately. I'm not aware of any bugs with the feature.

Nadrieril avatar May 21 '25 14:05 Nadrieril

Thanks so much! So we can definitely trust the information provided!

ssyram avatar May 21 '25 14:05 ssyram