Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field

Summary

Env::dropping_formula_for_term (src/refine/env.rs) recurses infinitely and overflows the stack when analyzing a recursive enum whose recursive Box<Self> (or &mut Self) is reached through a tuple/struct field instead of being a direct field of the variant. The recursive-ADT cutoff only recognizes a direct pointer field, so any indirection bypasses it.

This needs no mutable references — a purely-owned recursive data type triggers it — and the program being analyzed is trivially safe.

Reproduction (minimal)

enum L { Cons((i64, Box<L>)), Nil }   // recursive Box<L> nested in a tuple field
impl thrust_models::Model for L { type Ty = Self; }

#[thrust::callable]
fn check() {
    let l = L::Cons((1, Box::new(L::Nil)));
    assert!(matches!(l, L::Cons(_)));   // trivially true
}
fn main() {}

$ THRUST_SOLVER=z3 cargo run -q -- -Adead_code -C debug-assertions=false repro.rs
thread 'rustc' has overflowed its stack
fatal runtime error: stack overflow, aborting
(exit 134)

The direct form — where the recursive Box<L> is a direct field of the variant — verifies cleanly:

enum L { Cons(i64, Box<L>), Nil }     // direct recursive field
impl thrust_models::Model for L { type Ty = Self; }
#[thrust::callable]
fn check() {
    let l = L::Cons(1, Box::new(L::Nil));
    assert!(matches!(l, L::Cons(_, _)));   // verifies: exit 0
}
fn main() {}

So the only difference between "crashes" and "verifies" is whether the recursive pointer sits directly in the variant or inside a tuple field of the variant.

Mechanism

src/refine/env.rs, dropping_formula_for_term (~lines 1120-1166). The three relevant branches:

} else if ty.is_own() {                                   // (A) Box: recurse into pointee
    let inner = &ty.as_pointer().unwrap().elem.ty;
    self.dropping_formula_for_term(existentials, inner, term.box_current())
} else if let Some(tty) = ty.as_tuple() {                 // (B) tuple: recurse into each element
    ...
    self.dropping_formula_for_term(existentials, &elem.ty, term.clone().tuple_proj(i))
    ...
} else if let Some(ety) = ty.as_enum() {                  // (C) enum: recurse into each variant field
    ...
    for field_ty in enum_def.field_tys() {
        ...
        if let Some(p) = field_type.as_pointer() {
            if matches!(&p.elem.ty, rty::Type::Enum(e) if e.symbol == ety.symbol) {
                // TODO: we need recursively defined drop_pred for the recursive ADTs!
                tracing::warn!("skipping recursive variant");
                continue;                                  // <-- the ONLY cycle cutoff
            }
        }
        self.dropping_formula_for_term(existentials, &field_type, field_term);
    }
    ...
}

The cycle cutoff in branch (C) engages only when a variant field's type is itself a pointer to the same enum (field_type.as_pointer() → Enum(e) with the same symbol). For Cons((i64, Box<L>)) the field type is a tuple, so the as_pointer() check fails and the guard is skipped. The descent then goes:

enum L (C) → tuple (i64, Box<L>) (B) → Box<L> (A) → enum L (C) → tuple … (B) → Box<L> (A) → …   ∞

Neither the tuple branch (B) nor the owned-pointer branch (A) has any cycle guard of its own, so the recursion never terminates. The TODO on line 1151 already flags that the current cutoff is a stopgap ("we need recursively defined drop_pred for the recursive ADTs"); this report is a concrete case where the stopgap is bypassed entirely and turns into a hard crash rather than a skipped obligation.

Notes

Valid, safe Rust: the reproducer compiles and runs fine under rustc; the assert! is always true.
Distinct from the recursive-ADT prophecy issues (Incompleteness: dropping a recursively-defined ADT does not resolve &mut prophecies stored in its recursive-position field, so safe programs are wrongly rejected #173 wrong-verdict for &mut in a recursive-position field; Incompleteness: a &mut stored in a Box has its prophecy resolved only at the Box's drop, so reading the referent before the box is dropped wrongly rejects safe programs #175 Box-held &mut prophecy timing): this reproducer contains no &mut at all, and the symptom is non-termination / stack overflow, not a wrong soundness/completeness verdict. It is triggered purely by the shape of the owned recursive type during drop-formula construction.
Any indirection through an aggregate should reproduce it (e.g. a struct field wrapping the Box<L>), since the guard is keyed on a direct pointer field.

Environment

thrust @ af7cd99 (current main)
rustc nightly-2025-09-08 (per rust-toolchain.toml)
z3 4.16.0

Two more triggers with the same root cause, including the usual `Option<Box<Self>>` shape

Re-checked on main @ 187a1e9 (Z3 5.0.0, -Adead_code -C debug-assertions=false). The tuple field in the report isn't the only way past the cutoff. The cutoff in dropping_formula_for_term only fires when a variant field is directly a pointer to an enum with the same symbol. So any recursive enum whose cycle goes through another enum also overflows the stack. That includes the most common way to write an optional child in Rust.

1. Recursion through `Option<Box<Self>>`

enum T { Node(i64, Option<Box<T>>) }
impl thrust_models::Model for T { type Ty = Self; }

fn main() {
    let t = T::Node(1, None);
    match t { T::Node(x, _) => assert!(x == 1) }
}

$ thrust-rustc -Adead_code -C debug-assertions=false a.rs
thread 'rustc' has overflowed its stack
fatal runtime error: stack overflow, aborting
(exit 134)

The field is Option<Box<T>>, which is not a pointer, so T's check doesn't fire. Inside Option, the field Box<T> is a pointer to T, but T isn't Option, so Option's check doesn't fire either. The descent is T → Option<Box<T>> → Box<T> → T → ….

2. Mutually recursive enums

enum A { Leaf(i64), Wrap(Box<B>) }
enum B { Back(Box<A>), Nil }
impl thrust_models::Model for A { type Ty = Self; }
impl thrust_models::Model for B { type Ty = Self; }

fn main() {
    let a = A::Leaf(1);
    match a { A::Leaf(x) => assert!(x == 1), _ => {} }
}

This overflows the same way: A → Box<B> → B → Box<A> → A → ….

In both cases gdb shows the overflowing frames alternating between the enum branch and the Box branch of Env::dropping_formula_for_term. That's the frame pair from this issue, with no tuple involved. Neither program has a &mut. Just dropping the value is enough.

Fix

#356 replaces the direct-pointer check with a guard on the sorts of the enums whose drop formula is currently being built. An enum is skipped when it's reached again inside its own drop formula, whatever path leads back to it. That covers the tuple case here, both shapes above, and the direct Box<Self> case, which keeps today's behavior. It also handles the non-recursive Option<&mut Option<_>> from #341, because a different instantiation has a different sort.

Generated by Claude Code

Navigation Menu

Repository navigation

Stack overflow (non-termination) in `dropping_formula_for_term` when a recursive ADT's self-pointer is nested inside a tuple/struct field #178

Summary

Reproduction (minimal)

Mechanism

Notes

Environment

Two more triggers with the same root cause, including the usual `Option<Box<Self>>` shape

1. Recursion through `Option<Box<Self>>`

2. Mutually recursive enums

Fix

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field #178

Description

Summary

Reproduction (minimal)

Mechanism

Notes

Environment

Activity

coord-e commented on Oct 27, 2026

Two more triggers with the same root cause, including the usual Option<Box<Self>> shape

1. Recursion through Option<Box<Self>>

2. Mutually recursive enums

Fix

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions

Stack overflow (non-termination) in `dropping_formula_for_term` when a recursive ADT's self-pointer is nested inside a tuple/struct field #178

Two more triggers with the same root cause, including the usual `Option<Box<Self>>` shape

1. Recursion through `Option<Box<Self>>`