Unexpected error

[sonmarcho]

Reported by @ Cemoixerestre. The following program triggers an "Unexpected" failure:

fn f(a: &mut i32, b: &mut i32, c: &mut i32, conds : &[bool]) {
    let mut y = &mut *a;
    let mut z = &mut *b;
    let mut i = 0;
    while i < conds.len() {
        if conds[i] {
            y = &mut *a;
            z = &mut *b;
        }
        else {
            y = &mut *b;
            z = &mut *c;
        }
        i += 1;
    }
    *y += 3;
    *a += 4;
    *z += 5;
}

[sonmarcho]

Slightly minimized:

fn f(a: &mut i32, b: &mut i32, cond : bool) {
    let mut y = &mut *a;
    let mut i = 0;
    while i < 32 {
        if cond {
            y = &mut *a;
        }
        else {
            y = &mut *b;
        }
        i += 1;
    }
}

[Cemoixerestre]

I minimized this example even further:

fn main() {
    let mut a = 0;
    let mut b = 1;
    let mut y = &mut a;
    let mut i = 0;
    while i < 32 {
        y = &mut b;
        i += 1;
    }
}

The error message is not exactly the same, is it a distinct issue?

[Info ] Imported: counter_example_aeneas.llbc
[Error] Internal error, please file an issue
Source: 'src/main.rs', lines 6:4-9:5

[sonmarcho]

Yes, it is probably a distinct issue... But I will clause this only once all the snippets above get accepted by the translation.

[sonmarcho]

I investigated the issue: it stems from the fact that the implementation does not properly handle joins of loan values. It is a known issue (the same problem appears in this test, which is marked as known-failure). I've been wanting to tackle it for a while, but first I have to slightly modify the way region abstractions are handled by the synthesis (this is an engineering problem, not a fundamental issue).

[sonmarcho]

https://github.com/AeneasVerif/aeneas/pull/600 solves all the issues but the very first example, because the loop fixed point is not precise enough yet to notice that it is possible to retrieve access to a without ending the borrow z (at the end of the function).