Add support for closures

[zhassan-aws]

Filing this tracking issue for closure support.

Example program:

fn main() {
  let r: Result<i32, i32> = Ok(3);
  let _: Result<i32, i32> = r.map_err(|_| 4);
}

$ charon
   Compiling clos v0.1.0 (/home/ubuntu/examples/aeneas/clos)
[ INFO charon_driver::export:106] [gexport]: Generated the file: /home/ubuntu/examples/aeneas/clos/clos.llbc
    Finished release [optimized] target(s) in 0.16s
$ aeneas -backend lean clos.llbc 
[Info ] Imported: clos.llbc
Uncaught exception:

  (Failure "Closures are not supported yet")

Raised at Aeneas__InterpreterExpressions.eval_rvalue_aggregate.compute in file "InterpreterExpressions.ml", line 796, characters 29-77
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterStatements.eval_statement.cf_eval_st.cf_assign in file "InterpreterStatements.ml", line 955, characters 29-70
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterStatements.eval_statement.cf_eval_st.cf_assign in file "InterpreterStatements.ml", line 955, characters 29-70
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__Interpreter.evaluate_function_symbolic in file "Interpreter.ml", line 589, characters 4-71
Called from Aeneas__Translate.translate_function_to_symbolics in file "Translate.ml", line 35, characters 25-77
Called from Aeneas__Translate.translate_function_to_pure in file "Translate.ml", line 55, characters 23-69
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 298, characters 4-127
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 992, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 279, characters 6-58

[sonmarcho]

Thanks for the report: I should have opened an issue for this myself actually. We did a lot of work in Charon to properly extract closure information, and make this information higher-level than what the MIR gives us. There still remains a bit of work to add support for closures in Aeneas, though this is not fundamentally complicated. I'll see when I can add this (I'm trying to prioritize).