From a1b0e585a03e56f293e55e6a33e0ac54fef83aeb Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 2 Oct 2026 21:41:59 +0000 Subject: [PATCH 1/2] Give enums nested in a body, impl, or closure a unique SMT-safe datatype name The datatype symbol of an enum was its `def_path_str`. For an enum declared inside a trait impl method or a closure, that path contains spaces, braces, and `#` (`::f::E`, `main::{closure#0}::E`), so the emitted SMT-LIB was rejected by the solver. Two same-named enums in different blocks of one function also shared a symbol and crashed the analyzer. Items whose def path is entirely in the type namespace (modules and types) keep their readable path name, which is unique and SMT-safe; any other item uses the existing `stable_def_id_symbol`. Keeping the old names for module items also keeps the generated SMT for existing programs unchanged, which matters because PCSat's running time is sensitive to symbol names. Fixes #316 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NuD8BuMA1PzziM9f59oQHb --- src/refine.rs | 14 +++++- tests/ui/fail/enum_local_in_trait_impl.rs | 56 +++++++++++++++++++++++ tests/ui/pass/enum_local_in_trait_impl.rs | 56 +++++++++++++++++++++++ 3 files changed, 125 insertions(+), 1 deletion(-) create mode 100644 tests/ui/fail/enum_local_in_trait_impl.rs create mode 100644 tests/ui/pass/enum_local_in_trait_impl.rs diff --git a/src/refine.rs b/src/refine.rs index 5a1fd8d3..3ec4a2d8 100644 --- a/src/refine.rs +++ b/src/refine.rs @@ -19,6 +19,7 @@ pub use env::{ }; use crate::chc::{DatatypeSymbol, UserDefinedPred}; +use rustc_hir::definitions::DefPathData; use rustc_middle::ty as mir_ty; use rustc_span::def_id::DefId; @@ -33,7 +34,18 @@ fn stable_def_id_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> String { } pub fn datatype_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> DatatypeSymbol { - DatatypeSymbol::new(tcx.def_path_str(did).replace("::", ".")) + // The path of an item nested in a function body, impl, or closure is neither unique nor a + // valid SMT-LIB symbol. + let is_module_item = tcx + .def_path(did) + .data + .iter() + .all(|d| matches!(d.data, DefPathData::TypeNs(_))); + if is_module_item { + DatatypeSymbol::new(tcx.def_path_str(did).replace("::", ".")) + } else { + DatatypeSymbol::new(stable_def_id_symbol(tcx, did)) + } } pub fn user_defined_pred(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> UserDefinedPred { diff --git a/tests/ui/fail/enum_local_in_trait_impl.rs b/tests/ui/fail/enum_local_in_trait_impl.rs new file mode 100644 index 00000000..eccd3611 --- /dev/null +++ b/tests/ui/fail/enum_local_in_trait_impl.rs @@ -0,0 +1,56 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +trait T { + fn f(b: bool) -> i64; +} + +struct A; +struct B; + +impl thrust_models::Model for A { + type Ty = Self; +} + +impl thrust_models::Model for B { + type Ty = Self; +} + +impl T for A { + fn f(b: bool) -> i64 { + enum E { + X(i64), + Y, + } + impl thrust_models::Model for E { + type Ty = Self; + } + let e = if b { E::X(1) } else { E::Y }; + match e { + E::X(x) => x, + E::Y => 0, + } + } +} + +impl T for B { + fn f(b: bool) -> i64 { + enum E { + Z(bool), + W(i64), + } + impl thrust_models::Model for E { + type Ty = Self; + } + let e = if b { E::Z(true) } else { E::W(5) }; + match e { + E::Z(_) => 10, + E::W(v) => v, + } + } +} + +fn main() { + assert!(A::f(true) == 1); + assert!(B::f(false) == 10); +} diff --git a/tests/ui/pass/enum_local_in_trait_impl.rs b/tests/ui/pass/enum_local_in_trait_impl.rs new file mode 100644 index 00000000..a2644a07 --- /dev/null +++ b/tests/ui/pass/enum_local_in_trait_impl.rs @@ -0,0 +1,56 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +trait T { + fn f(b: bool) -> i64; +} + +struct A; +struct B; + +impl thrust_models::Model for A { + type Ty = Self; +} + +impl thrust_models::Model for B { + type Ty = Self; +} + +impl T for A { + fn f(b: bool) -> i64 { + enum E { + X(i64), + Y, + } + impl thrust_models::Model for E { + type Ty = Self; + } + let e = if b { E::X(1) } else { E::Y }; + match e { + E::X(x) => x, + E::Y => 0, + } + } +} + +impl T for B { + fn f(b: bool) -> i64 { + enum E { + Z(bool), + W(i64), + } + impl thrust_models::Model for E { + type Ty = Self; + } + let e = if b { E::Z(true) } else { E::W(5) }; + match e { + E::Z(_) => 10, + E::W(v) => v, + } + } +} + +fn main() { + assert!(A::f(true) == 1); + assert!(B::f(false) == 5); +} From ff61c0b53c59997300c0810541cb37b1cc0fcfd8 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 02:25:47 +0000 Subject: [PATCH 2/2] Name every enum datatype by its stable def-id symbol Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NuD8BuMA1PzziM9f59oQHb --- src/refine.rs | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/src/refine.rs b/src/refine.rs index 3ec4a2d8..8669cda4 100644 --- a/src/refine.rs +++ b/src/refine.rs @@ -19,7 +19,6 @@ pub use env::{ }; use crate::chc::{DatatypeSymbol, UserDefinedPred}; -use rustc_hir::definitions::DefPathData; use rustc_middle::ty as mir_ty; use rustc_span::def_id::DefId; @@ -34,18 +33,7 @@ fn stable_def_id_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> String { } pub fn datatype_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> DatatypeSymbol { - // The path of an item nested in a function body, impl, or closure is neither unique nor a - // valid SMT-LIB symbol. - let is_module_item = tcx - .def_path(did) - .data - .iter() - .all(|d| matches!(d.data, DefPathData::TypeNs(_))); - if is_module_item { - DatatypeSymbol::new(tcx.def_path_str(did).replace("::", ".")) - } else { - DatatypeSymbol::new(stable_def_id_symbol(tcx, did)) - } + DatatypeSymbol::new(stable_def_id_symbol(tcx, did)) } pub fn user_defined_pred(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> UserDefinedPred {