Loops sharing the same head in Kani-compiled GOTO

[qinheping]

I tried this code:

fn binary_search(arr: &[i32], target: i32) -> Option<usize> {
    let mut left = 0;
    let mut right = arr.len() - 1;

    while left <= right {
        let mid = (left + right) / 2;
        if arr[mid] == target {
            return Some(mid);
        } else if arr[mid] < target {
            left = mid + 1;
        } else {
            right = mid - 1;
        }
    }
    None
}

#[kani::proof]
fn check() {
    let items = [kani::any(); i32::MAX as usize];
    assert_eq!(Some(1), binary_search(&items, 3));
}

using the following command line invocation:

kani test1.rs --keep-temps 
cbmc --show-loops test1.out

with Kani version: 0.24.0

I expected to see this happen: Only one loop in the function binary_search

Instead, this happened: There are two loops:

Loop _RNvCslgPNofJzcIt_5test113binary_search.0:
  file /Users/qinhh/Repos/kani/qinheping/tests/kani/NondetSlices/test1.rs line 9 column 16 function binary_search

Loop _RNvCslgPNofJzcIt_5test113binary_search.1:
  file /Users/qinhh/Repos/kani/qinheping/tests/kani/NondetSlices/test1.rs line 9 column 16 function binary_search

It is because that both else nodes jump directly to the loop head.
When I and @remi-delmas-3000 discussed about the normal form of loops, we agreed that we should apply loop contracts only on loops not sharing the same head.
So I think, when compile such loops into GOTO, we should add a latch node that jumps to the loop head and let all jumps-to-head jump to the latch node instead.

[tautschnig]

I believe you are looking at the goto binary before transformations are applied: if you do cbmc --show-loops test1.for-check.out you'll find that there is only one loop left. This is the effect of running goto-instrument --ensure-one-backedge-per-target (which does, I think, exactly what you are asking for), see kani-driver/src/call_goto_instrument.rs.