Unsound: Env::var_type rebuilds an enum's type arguments from its first field, so a nested refinement that held for that field's original value is assumed for a field overwritten through &mut — panicking programs verify as safe #338

Summary

When a generic enum value is expanded into per-field flow variables, Env::var_type rebuilds the enum's type arguments with rty::unify_tys_params. That function takes the substitution for T from the first field that mentions T. If that field was not expanded further (because of THRUST_ENUM_EXPANSION_DEPTH_LIMIT), its type still carries the nested refinement template from the binding's entry type, for example Option<{ int | p7 }>.

That refinement is then applied to every T position, including a field that has since been overwritten through a &mut. Thrust assumes the stale refinement for the new value. The solver can pick p7 so that the assumptions contradict each other, and everything after that point verifies vacuously.

Reproduction

enum Pair<T> { P(Option<T>, T) }
impl<T: thrust_models::Model> thrust_models::Model for Pair<T> { type Ty = Pair<T::Ty>; }

fn set_second(m: &mut Pair<Option<i32>>) -> Option<i32> {
    let Pair::P(_, second) = m;
    *second = Some(100);
    let Pair::P(_, now) = *m;
    let mut out = now;
    let _keep = &mut out;
    out
}

fn main() {
    let mut p = Pair::P(None, Some(5));
    let r = set_second(&mut p);
    let k = match r { Some(k) => k, None => 0 };
    assert!(k == 5);
}

$ thrust-rustc -Adead_code -C debug-assertions=false repro.rs && echo safe
safe

At runtime set_second returns Some(100) and assert!(k == 5) panics. Thrust also reports safe when the assertion is k == 100, which shows the result is vacuous.

Thrust gives the correct Unsat in each of these cases:

• with THRUST_ENUM_EXPANSION_DEPTH_LIMIT=4, and the k == 100 version then verifies;
• without the write *second = Some(100);
• when the written value agrees with the original, i.e. Some(5);
• without let _keep = &mut out;, so out is not rebound as a mutable local.

A smaller variant with assert!(false) placed right after the re-read also verifies as safe:

fn f(m: &mut Pair<Option<i32>>) {
    let Pair::P(_, o) = m;
    *o = Some(100);
    let Pair::P(_, x) = *m;
    let mut v = x;
    let _r = &mut v;
    assert!(false);
}

Root cause (src/refine/env.rs)

1. A truncated field keeps its refinement. bind_impl stops expanding at the depth limit (2 by default). For Pair<Option<i32>>, the field P.0: Option<T> is the second enum level, so its Some payload of type T = Option<i32> is bound as one variable with its full type Option<{ int | p7 }>. Here p7 is the nested template from the parameter's entry type. Fields that are expanded further end in plain leaves; their refinements live in the assumptions, not in the type.
2. var_type takes T from that field. In the FlowBinding::Enum case, var_type calls rty::unify_tys_params(expected_tys, got_tys). This picks T := Option<{ int | p7 }> from P.0's payload. Meanwhile P.1 has been rebound to the borrow's prophecy, whose value is Some(100). The rebuilt type Pair<Option<{ int | p7 }>> therefore claims p7 for the new value.
3. The stale refinement becomes an assumption. Reading (*m as P).1 goes through PlaceType::downcast, which instantiates the field type with the rebuilt arguments. Binding the result to a mutable local goes through bind_enum, which assumes the field types instantiated with ty.args. That is p7(100), while only the caller's Some(5) constrains p7.

This differs from #253, which is about the depth limit causing panics, and from the partial-move double resolutions in #121, #122 and #207.

Fix direction

When var_type rebuilds an enum's type arguments from its fields, do not carry over refinements found in a field's type, for example by stripping them before unification. Alternatively, derive the arguments from the binding's declared type rather than from whichever field mentions T first.

Environment

• thrust @ 187a1e9
• Z3 5.0.0