From e4721b235f63ad80ff620e3ebcaca1294fa565f4 Mon Sep 17 00:00:00 2001 From: coord_e Date: Thu, 23 Jul 2026 11:13:29 +0000 Subject: [PATCH 1/2] Stop register_def of target of extern_spec_fn --- src/analyze/crate_.rs | 46 +++++++++++++++++++++++++------------------ 1 file changed, 27 insertions(+), 19 deletions(-) diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 74198f18..981ed3a8 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -60,11 +60,36 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } fn refine_local_defs(&mut self) { + let mut keys = self.tcx.mir_keys(()).clone(); for local_def_id in self.tcx.mir_keys(()) { - if self.tcx.def_kind(*local_def_id).is_fn_like() { - self.refine_fn_def(*local_def_id); + let analyzer = self.ctx.local_def_analyzer(*local_def_id); + if analyzer.is_annotated_as_extern_spec_fn() { + let target_def_id = analyzer.extern_spec_fn_target_def_id(); + if let Some(local_target_def_id) = target_def_id.as_local() { + keys.swap_remove(&local_target_def_id); + } + } + if analyzer.is_annotated_as_ignored() { + self.skip_analysis.insert(*local_def_id); + keys.swap_remove(local_def_id); + } + if analyzer.is_annotated_as_predicate() { + analyzer.analyze_predicate_definition(); + self.skip_analysis.insert(*local_def_id); + keys.swap_remove(local_def_id); + } + if analyzer.is_annotated_as_formula_fn() { + self.ctx.register_formula_fn(*local_def_id); + self.skip_analysis.insert(*local_def_id); + keys.swap_remove(local_def_id); + } + if !self.tcx.def_kind(*local_def_id).is_fn_like() { + keys.swap_remove(local_def_id); } } + for local_def_id in &keys { + self.refine_fn_def(*local_def_id); + } } #[tracing::instrument(skip(self), fields(def_id = %self.tcx.def_path_str(local_def_id)))] @@ -83,23 +108,6 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.skip_analysis.insert(local_def_id); } - if analyzer.is_annotated_as_ignored() { - self.skip_analysis.insert(local_def_id); - return; - } - - if analyzer.is_annotated_as_predicate() { - analyzer.analyze_predicate_definition(); - self.skip_analysis.insert(local_def_id); - return; - } - - if analyzer.is_annotated_as_formula_fn() { - self.ctx.register_formula_fn(local_def_id); - self.skip_analysis.insert(local_def_id); - return; - } - // skip analysis if the def is closure defined in skipped def if let Some(root_local_def_id) = self .tcx From 60de711faeeb5b8cac753f8d9a1ff9ec698a2b84 Mon Sep 17 00:00:00 2001 From: coord_e Date: Thu, 23 Jul 2026 11:14:01 +0000 Subject: [PATCH 2/2] Prioritize trait method spec keys --- src/analyze/crate_.rs | 13 +++++++++++++ tests/ui/fail/partialeq_impl.rs | 30 ++++++++++++++++++++++++++++++ tests/ui/pass/partialeq_impl.rs | 30 ++++++++++++++++++++++++++++++ 3 files changed, 73 insertions(+) create mode 100644 tests/ui/fail/partialeq_impl.rs create mode 100644 tests/ui/pass/partialeq_impl.rs diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 981ed3a8..09a9629d 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -60,7 +60,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } fn refine_local_defs(&mut self) { + // Prioritize trait method specs so that they are always available when refining trait impl + // functions; see the partialeq_impl.rs case. let mut keys = self.tcx.mir_keys(()).clone(); + let mut trait_method_spec_keys = HashSet::new(); for local_def_id in self.tcx.mir_keys(()) { let analyzer = self.ctx.local_def_analyzer(*local_def_id); if analyzer.is_annotated_as_extern_spec_fn() { @@ -68,6 +71,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { if let Some(local_target_def_id) = target_def_id.as_local() { keys.swap_remove(&local_target_def_id); } + if matches!( + self.tcx.def_kind(target_def_id), + rustc_hir::def::DefKind::AssocFn + ) { + trait_method_spec_keys.insert(*local_def_id); + keys.swap_remove(local_def_id); + } } if analyzer.is_annotated_as_ignored() { self.skip_analysis.insert(*local_def_id); @@ -87,6 +97,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { keys.swap_remove(local_def_id); } } + for local_def_id in &trait_method_spec_keys { + self.refine_fn_def(*local_def_id); + } for local_def_id in &keys { self.refine_fn_def(*local_def_id); } diff --git a/tests/ui/fail/partialeq_impl.rs b/tests/ui/fail/partialeq_impl.rs new file mode 100644 index 00000000..219f155b --- /dev/null +++ b/tests/ui/fail/partialeq_impl.rs @@ -0,0 +1,30 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +enum X { + A(i32), +} + +impl thrust_models::Model for X { + type Ty = Self; +} + +impl PartialEq for X { + fn eq(&self, other: &X) -> bool { + match (self, other) { + (Self::A(lhs), Self::A(rhs)) => !lhs.eq(rhs), + } + } +} + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] +fn rand() -> X { + unimplemented!() +} + +fn main() { + let x = rand(); + assert!(x == x); +} diff --git a/tests/ui/pass/partialeq_impl.rs b/tests/ui/pass/partialeq_impl.rs new file mode 100644 index 00000000..3e532d34 --- /dev/null +++ b/tests/ui/pass/partialeq_impl.rs @@ -0,0 +1,30 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +enum X { + A(i32), +} + +impl thrust_models::Model for X { + type Ty = Self; +} + +impl PartialEq for X { + fn eq(&self, other: &X) -> bool { + match (self, other) { + (Self::A(lhs), Self::A(rhs)) => lhs.eq(rhs), + } + } +} + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] +fn rand() -> X { + unimplemented!() +} + +fn main() { + let x = rand(); + assert!(x == x); +}