[CYJ904]

This fixes #3596, an issue in the Autoharness milestone.

Priority: Critical (C3, stops a whole run; P3, 11 changed lines outside tests with tests that fail without the fix). Until this is fixed, users of kani autoharness cannot get any verdicts for a crate that contains a by-reference downcast into an enum like enum E { A(!) }: the compiler panics and the whole run aborts. It affects place codegen (the Downcast arm of codegen_projection) and fixes the crate-wide abort of #3596.

Root cause

rustc gives an enum whose variants are all uninhabited and contain only zero-sized fields (e.g. enum E { A(!) }) the Variants::Empty layout of !, so Kani generates a goto struct with no fields for it. MIR still projects Downcast(A) then Field(0). The Downcast arm treated Empty like Single and passed the expression through, so the Field projection called .member("0") on an empty struct and hit unreachable! in Expr::member (cprover_bindings/src/goto_program/expr.rs:914).

Codegen runs for the whole crate before any harness is checked, so under autoharness one such function aborts the entire run and every other function in the crate gets no result.

Fix

The Downcast arm now returns an UnimplementedData error for Variants::Empty. The existing flow turns it into an unsupported-construct check that only fails verification if it is reachable. No program that can fail is reported as successful.

Testing

1. tests/expected/uninhabited-enum-downcast: the issue's reproducer (let E::A(ref _a) = ...) and a match by-reference variant. Both now fail with the unsupported-construct check instead of crashing.
2. tests/script-based-pre/autoharness_uninhabited_enum_downcast: an autoharness run over a crate with the crashing function plus an ordinary ok_fn. ok_fn is verified and the run completes with a summary.
3. Both tests fail (compiler panic at expr.rs:914) with the compiler change reverted, and pass with it.
4. By-value forms (let E::A(a) = ..., match ... { E::A(a) => a }) never reached the Downcast, since rustc lowers them to unreachable, and behave as before.

Notes for reviewers

1. The unsupported message links to ICE: unable to find field 0 for type StructTag (never_type) #3596, which this PR closes. Happy to point it at a different issue if you prefer.
2. Reading through a reference to an uninhabited type is UB under Miri's current validity rules. A possible follow-up is to report it as a safety check (like transmute to an uninhabited type in intrinsic.rs) rather than as unsupported, but since the opsem question about reference validity is still open, this PR keeps to the conservative fix.
3. Fix projections after a subslice at mir-opt-level 2 #4973 and Ignore min_length of a constant index into an array #4974 also touch codegen_projection, in different arms (subslice and constant index). They are independent of this change.

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

[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

2 open issues

• The issue URL is hardcoded here, which makes the message brittle to future issue migrations/renames… · New
• The comment explains one motivating example, but it reads as if “only zero-sized fields” is… · New

What changed in this PR

This PR prevents kani autoharness runs from aborting when MIR performs a by-reference Downcast into an enum whose layout is Variants::Empty (e.g., enum E { A(!) }), by reporting it as an unsupported construct instead of crashing.

Changes:

• Handle Variants::Empty in codegen_projection’s Downcast arm by returning UnimplementedData (instead of passing through and later crashing on a missing field).
• Add regression tests covering both expected-test and script-based autoharness scenarios to ensure the run completes and reports a targeted failure.

File	Description
kani-compiler/​src/​codegen_cprover_gotoc/​codegen/​place.rs	Converts the Variants::Empty downcast case from a crash into a structured unsupported-construct error.
tests/​expected/​uninhabited-enum-downcast/​main.rs	Adds a reproducer exercising by-reference downcast via let and match.
tests/​expected/​uninhabited-enum-downcast/​expected	Locks in the expected “unsupported construct” failure message instead of a compiler panic.
tests/​script-based-pre/​autoharness_uninhabited_enum_downcast/​uninhabited_enum_downcast.rs	Adds an autoharness crate containing both a triggering function and a normal function to verify the run continues.
tests/​script-based-pre/​autoharness_uninhabited_enum_downcast/​run.sh	Runs autoharness over the reproducer crate to ensure the whole run doesn’t abort.
tests/​script-based-pre/​autoharness_uninhabited_enum_downcast/​expected	Asserts the run completes, with ok_fn verified and trigger failing.
tests/​script-based-pre/​autoharness_uninhabited_enum_downcast/​config.yml	Wires the new script-based test into the harness.

_{Review effort: Lite}

[feliperodri]

The fix is minimal and safe: an uninhabited downcast becomes an unsupported-construct check, which only fails when reachable. Both tests fail without the change, which is good evidence.

Before merge:

1. This is a crash fix, so please add [C] Bug and [F] Crash. We can discuss T-High Priority separately, since it stops whole autoharness runs.
2. The issue URL is hardcoded here. Please centralize it, as Copilot suggests.
3. The comment suggests only zero-sized fields trigger this. The arm matches Variants::Empty alone, so please reword it.
4. Six jobs are cancelled. Please re-run them.