Confusion about the LLBC produced for a closure

[msprotz]

jonathan@verveine:~/Code/eurydice (protz_trait_clauses) $ \cat test/closure/src/main.rs
fn f() -> [u8; 1] {
    let s = [0; 1];
    let a: [u8; 1] = core::array::from_fn(|_| s[0]);
    a
}

fn main() {
    let actual = f()[0];
    let expected = 0;
    assert_eq!(actual, expected);
}

if I run eurydice on this, and I pass --log '*', I get a dump of the LLBC:

  fn closure::f::closure<0, 1>(state^1 : &0 mut ((&1 (@Array<u8, 1: usize>))), v@2 : (usize)) -> u8
{
    v@0 : u8;
    state^1 : &0 mut ((&1 (@Array<u8, 1: usize>)));
    v@2 : usize;
    v@3 : usize;
    v@4 : &'_ (@Array<u8, 1: usize>);
    v@5 : &'_ (u8);

    v@3 := (0: usize : usize);
    v@4 := &*((*(state^1)).0);
    v@5 := move @ArrayIndexShared<'_, u8, 1: usize>(move v@4, copy v@3);
    v@0 := copy *(v@5);
    drop v@3;
    return
  }

Now here's the snippet of Eurydice that we care for:

        match decl with
        | None -> None
        | Some decl ->
            let { C.def_id; name; signature; body; is_global_decl_body; item_meta; _ } = decl in
            let env = { env with generic_params = signature.generics } in
            L.log "AstOfLlbc" "Visiting %sfunction: %s\n%s"
              (if body = None then "opaque " else "")
              (string_of_name env name)
              (Charon.PrintLlbcAst.Ast.fun_decl_to_string env.format_env "  " "  " decl);

            assert (def_id = id);
            let name = lid_of_name env name in
            match body with
            | None ->
                ... (* irrelevant *)

            | Some { arg_count; locals; body; _ } ->
                if is_global_decl_body then
                  None
                else
                  let env = push_cg_binders env signature.C.generics.const_generics in
                  let env = push_type_binders env signature.C.generics.types in

                  L.log "AstOfLlbc" "ty of locals: %s"
                    (String.concat " ++ " (List.map (fun (local: C.var) ->
                      Charon.PrintTypes.ty_to_string env.format_env local.var_ty) locals));
                  L.log "AstOfLlbc" "ty of inputs: %s"
                    (String.concat " ++ " (List.map (fun t ->
                      Charon.PrintTypes.ty_to_string env.format_env t) signature.C.inputs));

Here's the fun bit: the types in the signature don't agree with the types of the locals.

ty of locals: u8 ++ &'0_0 mut ((&'0_1 (@Array<u8, 1: usize>))) ++ usize ++ usize ++ &'_ (@Array<u8, 1: usize>) ++ &'_ (u8)
ty of inputs: &'0_0 mut ((&'0_1 (@Array<u8, 1: usize>))) ++ (usize)

notably, one has a tuple of size one for the usize, while the other doesn't!

Please help me understand if I'm missing something or if this is a bug somewhere. Thanks!

[Nadrieril]

That really seems like a bug. See also #194 for our plans for closures

[msprotz]

Ok I worked around it by normalizing (t) to t everywhere.

[sonmarcho]

This is strange. ~~I wonder where the tuple is introduced: is it Rustc's fault or our fault?~~ I think this is the culprit (we should check if the length is 1): https://github.com/AeneasVerif/charon/blob/793680f108a4e1a56c9550b62aee751543aa242a/charon/src/transform/update_closure_signatures.rs#L82 (and if not the problem is probably in this file)

[Nadrieril]

I would guess the tuple comes from the Fn trait: a closure like |x, y, z| ... implements Fn<(X, Y, Z)>. Do we special-case the case of single arguments anywhere?

[sonmarcho]

I do some transformations above to, among other things, make the closure state more explicit (this is the update_closure_signatures file I refer to above). The error likely comes from there, and especially this line where I do not special case on single arguments (I didn't have much time to recheck the code, but it is possible Rust does it on its side).

[Nadrieril]

I fixed this in https://github.com/AeneasVerif/charon/pull/494. Now the closure signature matches the locals.