[srivatsansamraj]

codegen_constant_index asserted length >= min_length for arrays, following the MIR documentation, which says min_length is the exact length for arrays. GVN does not keep that: it rewrites an Index with a known value into ConstantIndex { offset, min_length: offset + 1 } without comparing it with the array length. For C[10] on a 5-element array, the bounds check becomes assert(const false) and the unreachable access after it becomes C[10 of 11], so Kani aborted at compile time (#2732). rustc uses mir-opt-level 2 whenever opt-level is above 0, so a crate with opt-level = 1 in its dev profile reached this with plain cargo kani.

rustc's codegen ignores min_length (rustc_codegen_ssa/src/mir/place.rs), and so does Kani's slice arm. This ignores it for arrays too and removes the parameter that becomes unused.

The issue's program now reports the always-failing bounds check instead of aborting. Kani emits that check as assert then assume, so the access after it is unreachable; were such an access reached, CBMC's array_bounds check would fail. With --cbmc-args --no-assumptions, test.array_bounds.1 goes from SUCCESS to FAILURE.

The new test expected/issue-2732 (-Zmir-opt-level=2) calls the issue's function directly, expecting the bounds-check failure, and behind a branch that is never taken, expecting it unreachable. It panics on main.

Resolves #2732

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[srivatsansamraj]

@CYJ904 @Tianshu-Huang @wodex1nhaoIeng @acearyanarun for review. At the same optimisation level, rustc can rewrite an array index that is always out of bounds into a form that broke an assertion inside Kani, so the compiler aborted. Kani now ignores that field the way rustc's own codegen does, and the out-of-bounds check is reported as an ordinary failure. The standard-library runs never hit this, so their numbers don't change.

[Tianshu-Huang]

LGTM, just one comment update

[Copilot]

Warning

Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.

Copilot review overview

1 open issue

• length - offset will panic on underflow in debug builds if from_end is true and `offset >… · New

What changed in this PR

Fixes Kani codegen for MIR ConstantIndex on arrays by ignoring min_length (which can become inconsistent after GVN at -Zmir-opt-level=2), preventing compile-time aborts and ensuring out-of-bounds checks are reported as expected.

Changes:

• Update array ConstantIndex codegen to ignore min_length and drop the now-unused parameter.
• Add a regression test for issue #2732 and its expected output at -Zmir-opt-level=2.
• Keep slice handling consistent with rustc by not relying on min_length.

File	Description
tests/​expected/​issue-2732/​issue_2732.rs	Adds a regression test harness covering always-failing and unreachable out-of-bounds indexing.
tests/​expected/​issue-2732/​issue_2732.expected	Captures expected Kani results (FAILURE and UNREACHABLE) for the new regression test.
kani-compiler/​src/​codegen_cprover_gotoc/​codegen/​place.rs	Ignores min_length for array ConstantIndex and removes the parameter from codegen.

_{Review effort: Lite}

[srivatsansamraj]

Done in 3d531c8bd: the index uses wrapping_sub, so an out-of-bounds index reaches CBMC's bounds check instead of panicking.

[feliperodri]

Dropping the length >= min_length assert follows rustc's codegen, and the explanation of the always-failing bounds check is clear.

Before merge:

1. length - offset can panic in the compiler when from_end is set and offset > length, on a path behind an always-failing bounds check. Use checked_sub (or saturating_sub) and handle the unreachable case explicitly.
2. Nine jobs are cancelled. Please re-run them.