From 28acdfa015e393357d15cf79cf835ee40646fc21 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 16 Oct 2026 21:45:04 +0000 Subject: [PATCH] Skip only truly recursive fields when dropping an enum dropping_formula_for_term treated any pointer field whose pointee is an enum with the same datatype symbol as a recursive variant and skipped it. The symbol is shared by every instantiation of a generic enum, so a non-recursive nesting such as Option<&mut Option> or Option>> lost the drop of its inner value and the &mut inside was never resolved, havocking the borrowed owner. Compare the pointee's sort with the dropped enum's sort instead, which includes the type arguments. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XWq7RJmc4iTGM8H7fsjtAT --- src/refine/env.rs | 2 +- tests/ui/fail/enum_nested_same_enum_mut_drop.rs | 14 ++++++++++++++ tests/ui/pass/enum_nested_same_enum_mut_drop.rs | 14 ++++++++++++++ 3 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 tests/ui/fail/enum_nested_same_enum_mut_drop.rs create mode 100644 tests/ui/pass/enum_nested_same_enum_mut_drop.rs diff --git a/src/refine/env.rs b/src/refine/env.rs index 778bcfde..efb86089 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -1160,7 +1160,7 @@ where pred_args.push(field_term.clone()); if let Some(p) = field_type.as_pointer() { - if matches!(&p.elem.ty, rty::Type::Enum(e) if e.symbol == ety.symbol) { + if p.elem.ty.to_sort() == ty.to_sort() { // TODO: we need recursively defined drop_pred for the recursive ADTs! tracing::warn!("skipping recursive variant"); continue; diff --git a/tests/ui/fail/enum_nested_same_enum_mut_drop.rs b/tests/ui/fail/enum_nested_same_enum_mut_drop.rs new file mode 100644 index 00000000..e0ae7d60 --- /dev/null +++ b/tests/ui/fail/enum_nested_same_enum_mut_drop.rs @@ -0,0 +1,14 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut slot: Option = None; + let o: Option<&mut Option> = Some(&mut slot); + if let Some(s) = o { + *s = Some(3); + } + match slot { + Some(y) => assert!(y == 4), + None => assert!(false), + } +} diff --git a/tests/ui/pass/enum_nested_same_enum_mut_drop.rs b/tests/ui/pass/enum_nested_same_enum_mut_drop.rs new file mode 100644 index 00000000..dfd8f6c7 --- /dev/null +++ b/tests/ui/pass/enum_nested_same_enum_mut_drop.rs @@ -0,0 +1,14 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut slot: Option = None; + let o: Option<&mut Option> = Some(&mut slot); + if let Some(s) = o { + *s = Some(3); + } + match slot { + Some(y) => assert!(y == 3), + None => assert!(false), + } +}