Unreachable List Loop

[Thanhson89]

use std::borrow::Borrow;

pub enum List<T> {
    Cons(T, Box<List<T>>),
    Nil,
}

fn foo(v: &List<List<u8>>) -> Option<List<u8>> {
    if let List::Cons(h, t) = v {
        let mut t = t.borrow();
        let mut last = h;
        while let List::Cons(ht, tt) = t
        {
            last = ht;
            t = tt.borrow();
        }
        None
    }
    else {
        None
    }
}

Trigger

$ aeneas -backend lean list_cons.llbc
[Info ] Imported: list_cons.llbc
[Info ] Generated the partial file (because of errors): ./ListCons.lean
[Error] Unreachable
Source: 'src/main.rs', lines 11:8-18:5

[sonmarcho]

Minimized further:

pub enum List<T> {
    Cons(T, Box<List<T>>),
    Nil,
}


fn foo(v: &List<List<u8>>) {
    if let List::Cons(_, t) = v {
        let mut t = &**t;
        while let List::Cons(_, tt) = t
        {
            t = &**tt;
        }
    }
}

When using the option -abort-on-error the log is:

[Info ] Imported: rust_tests.llbc
[Error] In file InterpreterLoopsFixedPoint.ml, line 531:
Unreachable
Source: 'src/lib.rs', lines 10:8-13:9

Uncaught exception:
  
  (Failure
    "In file InterpreterLoopsFixedPoint.ml, line 531:\
   \nIn file InterpreterLoopsFixedPoint.ml, line 531:\
   \nUnreachable\
   \nSource: 'src/lib.rs', lines 10:8-13:9\
   \nSource: 'src/lib.rs', lines 10:8-13:9")

Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 52, characters 4-76
Called from Stdlib__List.filter_map.aux in file "list.ml", line 258, characters 14-17
Called from Aeneas__InterpreterLoopsFixedPoint.compute_loop_entry_fixed_point.compute_fixed_ in file "InterpreterLoopsFixedPoint.ml", line 542, characters 26-68
Called from Aeneas__InterpreterLoopsFixedPoint.compute_loop_entry_fixed_point in file "InterpreterLoopsFixedPoint.ml", line 574, characters 11-60
Called from Aeneas__InterpreterLoops.eval_loop_symbolic in file "InterpreterLoops.ml", line 276, characters 4-73
Called from Aeneas__InterpreterLoops.eval_loop in file "InterpreterLoops.ml", line 416, characters 14-65
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 973, characters 8-545
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 973, characters 8-545
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 973, characters 8-545
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 973, characters 8-545
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Aeneas__InterpreterStatements.eval_switch in file "InterpreterStatements.ml", line 1193, characters 31-60
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__InterpreterStatements.eval_switch in file "InterpreterStatements.ml", line 1204, characters 14-77
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 968, characters 29-58
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 973, characters 8-545
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Aeneas__InterpreterStatements.eval_function_body in file "InterpreterStatements.ml", line 1572, characters 26-56
Called from Aeneas__Interpreter.evaluate_function_symbolic in file "Interpreter.ml", line 660, characters 8-65
Called from Aeneas__Translate.translate_function_to_symbolics in file "Translate.ml", line 37, characters 25-77
Called from Aeneas__Translate.translate_function_to_pure_aux in file "Translate.ml", line 57, characters 23-69
Called from Aeneas__Translate.translate_function_to_pure in file "Translate.ml", line 210, characters 6-79
Called from Stdlib__List.filter_map.aux in file "list.ml", line 258, characters 14-17
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 286, characters 4-134
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1033, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66