Bug: Closures with drop glue translated

[ssyram]

To be reported after the current main branch is merged into main of Charon official, when vtable for closures is supported.

Now, if one has a simple function:

fn dummy() {
    let b = Box::new(10);
    let x: &dyn FnOnce(i32) -> i32 = &move |x| x + *b + 1;
}

This generates LLBC of the following form:

struct test_crate::dummy::closure {
  alloc::boxed::Box<i32>[MetaSized<i32>, Sized<Global>],
}

// Full name: test_crate::dummy::{impl FnOnce<(i32)> for test_crate::dummy::closure}::call_once
fn {impl FnOnce<(i32)> for test_crate::dummy::closure}::call_once(@1: test_crate::dummy::closure, @2: (i32)) -> i32
{
    let @0: i32; // return
    let @1: test_crate::dummy::closure; // arg #1
    let tupled_args@2: (i32); // arg #2
    let x@3: i32; // local
    let @4: i32; // anonymous local
    let @5: i32; // anonymous local
    let @6: i32; // anonymous local
    let @7: i32; // anonymous local
    let @8: i32; // anonymous local

    storage_live(x@3)
    storage_live(@7)
    storage_live(@8)
    x@3 := move ((tupled_args@2).0)
    storage_live(@4)
    storage_live(@5)
    @5 := copy (x@3)
    storage_live(@6)
    @6 := copy (*((@1).0))
    @7 := copy (@5) panic.+ copy (@6)
    @4 := move (@7)
    storage_dead(@6)
    storage_dead(@5)
    @8 := copy (@4) panic.+ const (1 : i32)
    @0 := move (@8)
    storage_dead(@4)
    drop[Drop<test_crate::dummy::closure>] @1
    return
}
...
// Full name: test_crate::dummy
fn dummy()
{
    let @0: (); // return
    let b@1: alloc::boxed::Box<i32>[MetaSized<i32>, Sized<Global>]; // local
    let x@2: &'_ ((dyn exists<_dyn> [@TraitClause0]: FnOnce<_dyn, (i32)> + _dyn : '_ + @TraitClause1_0::Output = i32)); // local
    let @3: &'_ (test_crate::dummy::closure); // anonymous local
    let @4: &'_ (test_crate::dummy::closure); // anonymous local
    let @5: test_crate::dummy::closure; // anonymous local

    storage_live(b@1)
    b@1 := @BoxNew<i32>[Sized<i32>](const (10 : i32))
    storage_live(x@2)
    storage_live(@3)
    storage_live(@4)
    storage_live(@5)
    @5 := test_crate::dummy::closure { 0: move (b@1) }
    @4 := &@5
    @3 := &*(@4)
    x@2 := unsize_cast<&'_ (test_crate::dummy::closure), &'_ ((dyn exists<_dyn> [@TraitClause0]: FnOnce<_dyn, (i32)> + _dyn : '_ + @TraitClause1_0::Output = i32)), {impl FnOnce<(i32)> for test_crate::dummy::closure}>(move (@3))
    storage_dead(@3)
    storage_dead(@4)
    @0 := ()
    drop[Drop<test_crate::dummy::closure>] @5
    storage_dead(@5)
    storage_dead(x@2)
    drop[{impl Drop for alloc::boxed::Box<T>[@TraitClause0, @TraitClause1]}<i32, Global>[MetaSized<i32>, Sized<Global>]] b@1
    storage_dead(b@1)
    @0 := ()
    return
}

This results in the LLBC with several bugs:

1. Obviously, the closure inside is with Box by the move, this is correctly reflected in the fields of the closure ADT, but no drop impl for this closure is implemented. As the drop_glue is not reflected, this should be a Hax bug.
2. After the move of the Box<i32> to @5, finally there is a drop on b1, besides the drop on @5. This is a double drop problem.

[Nadrieril]

You opened this on your own repo, did you mean to open it on the main charon repo?

[ssyram]

Thanks for reminding, I remember this stemmed from the dyn Trait support PR (AeneasVerif#762) , as it uses &dyn FnOnce, which should be unsupported by the main branch of Charon yet? I planned to report after the dyn Trait branch is supported. But if you find it suitable, I'm happy also to report now.

[Nadrieril]

Do as you wish, but this is an interesting bug.