Unsound: a by-value parameter that is moved out and re-initialized is equated to its entry argument at every join point, so the function's postcondition becomes vacuous — even assert!(false) in the caller verifies as safe #334

Summary

bind_locals (src/analyze/basic_block.rs) adds the assumption "the parameter's entry value (OuterFnParam) equals the parameter local's current value" for every parameter whose local is non-flow:

// XXX: A user-supplied loop invariant replaces the inferred precondition, so
// it no longer carries the relationship between a function's entry argument
// (`OuterFnParam`) and its current local. ... As an ad-hoc workaround,
// equate them when the local is non-flow, since its representation cannot change.
let local = analyze::local_of_function_param(outer_idx);
if !param_ty.to_sort().is_singleton() && self.env.is_non_flow_local(local) {
    assumption.body.push_conj(
        chc::Term::var(PlaceTypeVar::Var(var))
            .equal_to(self.env.local_type(local).term),
    );
}

The premise "a non-flow local cannot change" is false for a parameter that is moved out and then re-initialized. reassign_local_mutabilities marks a local Mut only when it is assigned while it is (maybe-)initialized, so s = … after let t = s; leaves the parameter local immutable (non-flow). It is simply re-bound to the new value, and from then on its current value differs from the argument.

The code runs in bind_locals, i.e. at the entry of every block that has its own precondition (every join point and loop header), not only at headers with an invariant!. At the first join point after the re-initialization, the clause assumes entry == current while the incoming state has current == entry + 1. Every path through that point is infeasible, the function's inferred postcondition can be false, and the callers verify vacuously.

Reproduction

No annotations and no loop needed. The if only creates a join point:

struct S { a: i64 }
impl thrust_models::Model for S { type Ty = Self; }

fn id(x: i64) -> i64 { x }

fn f(mut s: S) -> i64 {
    let t = s;                 // move the parameter out
    s = S { a: id(t.a + 1) };  // re-initialize it in a later block
    if id(0) == 0 {}           // any join point
    s.a
}

fn main() {
    assert!(f(S { a: 0 }) == 0);   // false: f returns 1
}

$ rustc --edition 2021 plain.rs && ./plain      # same program without the Model impl
thread 'main' panicked at plain.rs:10:5:
assertion failed: f(S { a: 0 }) == 0
$ cargo run -q -- -Adead_code -C debug-assertions=false repro.rs && echo safe
safe

f verifies vacuously, so even this verifies:

fn main() {
    f(S { a: 0 });
    assert!(false);
}

$ cargo run -q -- -Adead_code -C debug-assertions=false repro_false.rs && echo safe
safe

Variants

All of these verify as safe on main @ 47e432e (Z3 5.0.0, default options). All are Unsat once the equation is skipped:

The re-initialization has to be in a different basic block from the move. Here that comes from the call id(..). If both are in one block, the assignment hits the "assignment to a defined local" path and panics in elaborate_place_for_borrow instead. That panic is not what this issue is about.

Root cause

The workaround is meant for invariant headers. Its guard, is_non_flow_local, does not ensure that the local still holds the argument. A non-flow parameter local can be bound twice: once at entry, and again by a definition after it has been moved out and dropped.

Suggested fix

Only add the equation when the body never assigns the parameter local. A parameter that is never assigned always holds its argument, so the equation is then valid at every block. A small mir::visit::Visitor using PlaceContext::is_place_assignment() is enough, like def_local in drop_point.rs. All tests/ui cases still pass with that change, the loop-invariant ones included. PR to follow.

Not a duplicate of

• Incompleteness: an explicit invariant! havocs live locals it doesn't mention, even when the loop never modifies them, wrongly rejecting safe programs #186 (an explicit invariant! havocs unmentioned locals): over-rejection, and only at invariant headers. Here the result is a wrong safe, at any join point, with no invariant.
• A loop bound that MIR folds into a debug-info constant cannot be named in invariant!: let n = 10; while i < n fatally errors with "not a live variable", and under shadowing the name silently binds to the wrong variable #257 (a debug-info constant cannot be named in invariant!, and shadowing binds the wrong name): about resolving names in the invariant formula. Here no formula is involved.
• Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121 / Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy #122 (partially-moved locals / aggregates dropped after a partial move): those are about resolving &mut prophecies on drop. Here there are no references.
• Unsound: at -C opt-level >= 1 GVN rewrites the Box deref temp from deref_copy to copy, so unelaborate_derefs misses it and every write through a nested Box lands on a copy — panicking programs verify as safe #244 / Unsound: at -C opt-level >= 1 a compound assignment through a &mut that sits behind a projection is reborrowed twice, the two prophecy resolutions contradict the write, and the function verifies vacuously — even assert!(false) is safe #248 / Unsound: unelaborate_derefs substitutes every deref_copy destination by its source place, but at opt-level 0 that destination can be a long-lived user reference or _0. Reads after the source is reassigned see the new value (panicking programs verify as safe), and a returned p.0 crashes #333 (deref_copy / GVN at -C opt-level >= 1): this reproduces at the default -C opt-level=0. At -C opt-level=1 the MIR changes and the program is correctly Unsat.