Panic in assert_entry: a deferred-initialized local with drop glue (let tmp; if c { tmp = Box::new(..); .. }) is live at START_BLOCK through its drop-flag-guarded drop, and drop_bb_zst_params removes it as if it were a ZST #344

Summary

A local that is declared without an initializer and assigned on only some paths, and whose type has drop glue (Box, Vec, Option<Box<_>>, …), crashes the analyzer in local_def::Analyzer::assert_entry for the function that contains it. The same code with a type that has no drop glue verifies normally.

The common real-world form is the Rust idiom of initializing a value later so a reference to it outlives the if:

fn get(c: bool, d: &i64) -> i64 {
    let tmp;
    let r: &i64 = if c { tmp = Box::new(5i64); &*tmp } else { d };
    *r
}

fn main() {
    let d = 1i64;
    assert!(get(true, &d) == 5);
}

$ thrust-rustc --edition 2021 -Adead_code -C debug-assertions=false repro.rs
thread 'rustc' panicked at src/rty.rs:311:21:
refinement of the parameter being removed references its own value
  ...
  thrust::rty::FunctionType::remove_param
  thrust::analyze::local_def::Analyzer::drop_bb_zst_params
  thrust::analyze::local_def::Analyzer::assert_entry

The construct is otherwise supported. Changing tmp to a type without drop glue (tmp = (5i64, 6i64); &tmp.0) verifies as safe.

Variants

Root cause

rustc's drop elaboration guards the drop of a maybe-initialized local with a drop flag. Optimized MIR for the third variant:

bb0: { _6 = const false; _3 = const 0_i64; switchInt(copy _1) -> [0: bb3, otherwise: bb1]; }
bb1: { _4 = Box::<i64>::new(const 1_i64) -> [return: bb2, ...]; }
bb2: { _6 = const true; _2 = move _4; ...; goto -> bb3; }
bb3: { _0 = copy _3; switchInt(copy _6) -> [0: bb4, otherwise: bb5]; }
bb4: { _6 = const false; return; }
bb5: { drop(_2) -> [return: bb4, ...]; }

MaybeLiveLocals counts drop(_2) in bb5 as a use. The CFG has a path bb0 -> bb3 -> bb5 with no assignment to _2, and the dataflow cannot tell that _6 makes that path infeasible. So _2 is live at START_BLOCK, and refine_basic_blocks (src/analyze/local_def.rs:908) makes it a parameter of the entry block's type, so _2 appears in the entry precondition template.

assert_entry then calls drop_bb_zst_params (src/analyze/local_def.rs:1057-1084), which removes every non-argument parameter with FunctionType::remove_param. That function's comment and #72 assume the only non-argument locals live at entry are ZSTs. Their singleton sort keeps them out of the precondition, so removing them is harmless. #72 says so directly: "Non-ZST locals do not have this problem because their definition appears as a real MIR statement that kills liveness." The drop-flag path above breaks that assumption:

• When the function has arguments, the removed local is the last entry parameter, and the precondition template refers to it as ν. remove_param panics at src/rty.rs:311. If the removed local is not the last parameter, the template refers to it as $i and it panics at src/rty.rs:292 instead.
• When the function has no arguments, every parameter is removed. The fallback that re-adds a synthetic unit parameter copies over the precondition refinement, which still mentions ν. unit is a singleton sort, so with_value_var creates no value variable, and Instantiator::instantiate unwraps None. This is the same symptom ICE: elaborate_unused_args panics when ZST local appears in START block liveness #72 fixed for ZSTs.

Expected behavior

The local is uninitialized at entry and never read before it is assigned, so the entry obligation should hold for any value of it. The local should be treated as universally quantified in the clause expected(args) ⇒ P(args, tmp), not removed from the precondition it occurs in.

Possible fixes:

1. In assert_entry, keep non-argument entry parameters whose sort is not a singleton. Pad expected with matching unrefined parameters and move the precondition refinement onto the new last parameter, so relate_sub_param_types maps them as plain clause variables.
2. Exclude locals that are not maybe-initialized at START_BLOCK from the entry block's parameters (MaybeInitializedPlaces is already computed in reassign_local_mutabilities). The successors that do list them as parameters would then need an unconstrained binding on such paths.

Only drop_bb_zst_params actually crashes. This is related to, but distinct from, #250: both come from deriving per-block state from liveness alone while ignoring initializedness. #250 is about edge drops of a value that was conditionally moved. This issue is about entry parameters for a value that is conditionally initialized, and the fix suggested there (intersecting edge-drop sets with maybe-initialized places) does not touch this code path.

Environment

• thrust @ 187a1e9
• rustc nightly-2025-09-08 (per rust-toolchain.toml), default -C opt-level=0
• Z3 5.0.0, default solver configuration (the panic happens before solving)