From 6823360ced7935d026b1694399b1f21477926e73 Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 23 Nov 2025 21:44:19 +0900 Subject: [PATCH 1/7] Resolve trait method DefId in type_call --- src/analyze/basic_block.rs | 25 +++++++++++++++++++------ tests/ui/fail/trait.rs | 22 ++++++++++++++++++++++ tests/ui/fail/trait_param.rs | 26 ++++++++++++++++++++++++++ tests/ui/pass/trait.rs | 22 ++++++++++++++++++++++ tests/ui/pass/trait_param.rs | 26 ++++++++++++++++++++++++++ 5 files changed, 115 insertions(+), 6 deletions(-) create mode 100644 tests/ui/fail/trait.rs create mode 100644 tests/ui/fail/trait_param.rs create mode 100644 tests/ui/pass/trait.rs create mode 100644 tests/ui/pass/trait_param.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 8b21ca2..3038675 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -568,12 +568,25 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let ret = rty::RefinedType::new(rty::Type::unit(), ret_formula.into()); rty::FunctionType::new([param1, param2].into_iter().collect(), ret).into() } - Some((def_id, args)) => self - .ctx - .def_ty_with_args(def_id, args) - .expect("unknown def") - .ty - .vacuous(), + Some((def_id, args)) => { + let param_env = self.tcx.param_env(self.local_def_id); + let instance = + mir_ty::Instance::resolve(self.tcx, param_env, def_id, args).unwrap(); + let resolved_def_id = if let Some(instance) = instance { + instance.def_id() + } else { + def_id + }; + if def_id != resolved_def_id { + tracing::info!(?def_id, ?resolved_def_id, "resolve",); + } + + self.ctx + .def_ty_with_args(resolved_def_id, args) + .expect("unknown def") + .ty + .vacuous() + } _ => self.operand_type(func.clone()).ty, }; let expected_args: IndexVec<_, _> = args diff --git a/tests/ui/fail/trait.rs b/tests/ui/fail/trait.rs new file mode 100644 index 0000000..8cd3881 --- /dev/null +++ b/tests/ui/fail/trait.rs @@ -0,0 +1,22 @@ +//@error-in-other-file: Unsat + +trait BoolLike { + fn truthy(&self) -> bool; +} + +impl BoolLike for bool { + fn truthy(&self) -> bool { + *self + } +} + +impl BoolLike for i32 { + fn truthy(&self) -> bool { + *self != 0 + } +} + +fn main() { + assert!(1_i32.truthy()); + assert!(false.truthy()); +} diff --git a/tests/ui/fail/trait_param.rs b/tests/ui/fail/trait_param.rs new file mode 100644 index 0000000..b0d6081 --- /dev/null +++ b/tests/ui/fail/trait_param.rs @@ -0,0 +1,26 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +trait BoolLike { + fn truthy(&self) -> bool; +} + +impl BoolLike for bool { + fn truthy(&self) -> bool { + *self + } +} + +impl BoolLike for i32 { + fn truthy(&self) -> bool { + *self != 0 + } +} + +fn falsy(value: T) -> bool { + value.truthy() +} + +fn main() { + assert!(falsy(0_i32)); +} diff --git a/tests/ui/pass/trait.rs b/tests/ui/pass/trait.rs new file mode 100644 index 0000000..35dc65e --- /dev/null +++ b/tests/ui/pass/trait.rs @@ -0,0 +1,22 @@ +//@check-pass + +trait BoolLike { + fn truthy(&self) -> bool; +} + +impl BoolLike for bool { + fn truthy(&self) -> bool { + *self + } +} + +impl BoolLike for i32 { + fn truthy(&self) -> bool { + *self != 0 + } +} + +fn main() { + assert!(1_i32.truthy()); + assert!(true.truthy()); +} diff --git a/tests/ui/pass/trait_param.rs b/tests/ui/pass/trait_param.rs new file mode 100644 index 0000000..7cc4179 --- /dev/null +++ b/tests/ui/pass/trait_param.rs @@ -0,0 +1,26 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +trait BoolLike { + fn truthy(&self) -> bool; +} + +impl BoolLike for bool { + fn truthy(&self) -> bool { + *self + } +} + +impl BoolLike for i32 { + fn truthy(&self) -> bool { + *self != 0 + } +} + +fn falsy(value: T) -> bool { + !value.truthy() +} + +fn main() { + assert!(falsy(0_i32)); +} From 3569233b53679eda7794862d7e5011944d58dd5f Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 23 Nov 2025 21:45:39 +0900 Subject: [PATCH 2/7] Enable to type lifted closure functions --- src/analyze.rs | 10 ++++++++++ src/analyze/crate_.rs | 7 ++----- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index fff56b4..e393ace 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -364,4 +364,14 @@ impl<'tcx> Analyzer<'tcx> { sig.abi, ) } + + /// Computes the signature of the local function. + /// + /// This is a drop-in replacement of `self.tcx.fn_sig(local_def_id).instantiate_identity().skip_binder()`, + /// but extracts parameter and return types directly from [`mir::Body`] to obtain a signature that + /// reflects the actual type of lifted closure functions. + pub fn local_fn_sig(&self, local_def_id: LocalDefId) -> mir_ty::FnSig<'tcx> { + let body = self.tcx.optimized_mir(local_def_id); + self.local_fn_sig_with_body(local_def_id, body) + } } diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index d6e343d..2a17b11 100644 --- a/src/analyze/crate_.rs +++ b/src/analyze/crate_.rs @@ -39,6 +39,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { #[tracing::instrument(skip(self), fields(def_id = %self.tcx.def_path_str(local_def_id)))] fn refine_fn_def(&mut self, local_def_id: LocalDefId) { + let sig = self.ctx.local_fn_sig(local_def_id); + let mut analyzer = self.ctx.local_def_analyzer(local_def_id); if analyzer.is_annotated_as_trusted() { @@ -46,11 +48,6 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.trusted.insert(local_def_id.to_def_id()); } - let sig = self - .tcx - .fn_sig(local_def_id) - .instantiate_identity() - .skip_binder(); use mir_ty::TypeVisitableExt as _; if sig.has_param() && !analyzer.is_fully_annotated() { self.ctx.register_deferred_def(local_def_id.to_def_id()); From 38065ddb65b8d7ce62da2a737db5fa43d28f475e Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 23 Nov 2025 21:46:12 +0900 Subject: [PATCH 3/7] Enable to type closures --- src/refine/template.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/refine/template.rs b/src/refine/template.rs index 446c450..c7f480c 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -163,6 +163,7 @@ impl<'tcx> TypeBuilder<'tcx> { unimplemented!("unsupported ADT: {:?}", ty); } } + mir_ty::TyKind::Closure(_, args) => self.build(args.as_closure().tupled_upvars_ty()), kind => unimplemented!("unrefined_ty: {:?}", kind), } } @@ -282,6 +283,7 @@ where unimplemented!("unsupported ADT: {:?}", ty); } } + mir_ty::TyKind::Closure(_, args) => self.build(args.as_closure().tupled_upvars_ty()), kind => unimplemented!("ty: {:?}", kind), } } From 5dba87ec029f305690630e9945b6630dd6e1c694 Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 24 Nov 2025 00:30:18 +0900 Subject: [PATCH 4/7] Add rty::FunctionAbi and attach it to rty::FunctionType --- src/refine/template.rs | 10 ++++++- src/rty.rs | 63 ++++++++++++++++++++++++++++++++++++------ 2 files changed, 64 insertions(+), 9 deletions(-) diff --git a/src/refine/template.rs b/src/refine/template.rs index c7f480c..b57dae5 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -184,6 +184,11 @@ impl<'tcx> TypeBuilder<'tcx> { registry: &'a mut R, sig: mir_ty::FnSig<'tcx>, ) -> FunctionTemplateTypeBuilder<'tcx, 'a, R> { + let abi = match sig.abi { + rustc_target::spec::abi::Abi::Rust => rty::FunctionAbi::Rust, + rustc_target::spec::abi::Abi::RustCall => rty::FunctionAbi::RustCall, + _ => unimplemented!("unsupported function ABI: {:?}", sig.abi), + }; FunctionTemplateTypeBuilder { inner: self.clone(), registry, @@ -199,6 +204,7 @@ impl<'tcx> TypeBuilder<'tcx> { param_rtys: Default::default(), param_refinement: None, ret_rty: None, + abi, } } } @@ -318,6 +324,7 @@ where param_rtys: Default::default(), param_refinement: None, ret_rty: None, + abi: Default::default(), } .build(); BasicBlockType { ty, locals } @@ -333,6 +340,7 @@ pub struct FunctionTemplateTypeBuilder<'tcx, 'a, R> { param_refinement: Option>, param_rtys: HashMap>, ret_rty: Option>, + abi: rty::FunctionAbi, } impl<'tcx, 'a, R> FunctionTemplateTypeBuilder<'tcx, 'a, R> { @@ -441,6 +449,6 @@ where .with_scope(&builder) .build_refined(self.ret_ty) }); - rty::FunctionType::new(param_rtys, ret_rty) + rty::FunctionType::new(param_rtys, ret_rty).with_abi(self.abi) } } diff --git a/src/rty.rs b/src/rty.rs index 64b8dfb..b780d44 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -83,6 +83,36 @@ where } } +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)] +pub enum FunctionAbi { + #[default] + Rust, + RustCall, +} + +impl std::fmt::Display for FunctionAbi { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + f.write_str(self.name()) + } +} + +impl FunctionAbi { + pub fn name(&self) -> &'static str { + match self { + FunctionAbi::Rust => "rust", + FunctionAbi::RustCall => "rust-call", + } + } + + pub fn is_rust(&self) -> bool { + matches!(self, FunctionAbi::Rust) + } + + pub fn is_rust_call(&self) -> bool { + matches!(self, FunctionAbi::RustCall) + } +} + /// A function type. /// /// In Thrust, function types are closed. Because of that, function types, thus its parameters and @@ -92,6 +122,7 @@ where pub struct FunctionType { pub params: IndexVec>, pub ret: Box>, + pub abi: FunctionAbi, } impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b FunctionType @@ -100,15 +131,25 @@ where D::Doc: Clone, { fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { + let abi = match self.abi { + FunctionAbi::Rust => allocator.nil(), + abi => allocator + .text("extern") + .append(allocator.space()) + .append(allocator.as_string(abi)) + .append(allocator.space()), + }; let separator = allocator.text(",").append(allocator.line()); - allocator - .intersperse(self.params.iter().map(|ty| ty.pretty(allocator)), separator) - .parens() - .append(allocator.space()) - .append(allocator.text("→")) - .append(allocator.line()) - .append(self.ret.pretty(allocator)) - .group() + abi.append( + allocator + .intersperse(self.params.iter().map(|ty| ty.pretty(allocator)), separator) + .parens(), + ) + .append(allocator.space()) + .append(allocator.text("→")) + .append(allocator.line()) + .append(self.ret.pretty(allocator)) + .group() } } @@ -120,9 +161,15 @@ impl FunctionType { FunctionType { params, ret: Box::new(ret), + abi: FunctionAbi::Rust, } } + pub fn with_abi(mut self, abi: FunctionAbi) -> Self { + self.abi = abi; + self + } + /// Because function types are always closed in Thrust, we can convert this into /// [`Type`]. pub fn into_closed_ty(self) -> Type { From ae1e2269b08f69c1d78147a86ddf5952b96695b7 Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 24 Nov 2025 00:30:44 +0900 Subject: [PATCH 5/7] Enable to type closure calls --- src/analyze/basic_block.rs | 46 ++++++++++++++++++++++++++++++++---- src/chc.rs | 4 ++++ src/rty.rs | 23 ++++++++++++++++++ tests/ui/fail/closure_mut.rs | 12 ++++++++++ tests/ui/pass/closure_mut.rs | 12 ++++++++++ 5 files changed, 93 insertions(+), 4 deletions(-) create mode 100644 tests/ui/fail/closure_mut.rs create mode 100644 tests/ui/pass/closure_mut.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 3038675..848eba0 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -84,16 +84,54 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { ) -> Vec { let mut clauses = Vec::new(); - if expected_args.is_empty() { - // elaboration: we need at least one predicate variable in parameter (see mir_function_ty_impl) - expected_args.push(rty::RefinedType::unrefined(rty::Type::unit()).vacuous()); - } tracing::debug!( got = %got.display(), expected = %crate::pretty::FunctionType::new(&expected_args, &expected_ret).display(), "fn_sub_type" ); + match got.abi { + rty::FunctionAbi::Rust => { + if expected_args.is_empty() { + // elaboration: we need at least one predicate variable in parameter (see mir_function_ty_impl) + expected_args.push(rty::RefinedType::unrefined(rty::Type::unit()).vacuous()); + } + } + rty::FunctionAbi::RustCall => { + // &Closure, { v: (own i32, own bool) | v = (<0>, ) } + // => + // &Closure, { v: i32 | (, _) = (<0>, ) }, { v: bool | (_, ) = (<0>, ) } + + let rty::RefinedType { ty, mut refinement } = + expected_args.pop().expect("rust-call last arg"); + let ty = ty.into_tuple().expect("rust-call last arg is tuple"); + let mut replacement_tuple = Vec::new(); // will be (, _) or (_, ) + for elem in &ty.elems { + let existential = refinement.existentials.push(elem.ty.to_sort()); + replacement_tuple.push(chc::Term::var(rty::RefinedTypeVar::Existential( + existential, + ))); + } + + for (i, elem) in ty.elems.into_iter().enumerate() { + let mut param_ty = elem.deref(); + param_ty + .refinement + .push_conj(refinement.clone().subst_value_var(|| { + let mut value_elems = replacement_tuple.clone(); + value_elems[i] = chc::Term::var(rty::RefinedTypeVar::Value).boxed(); + chc::Term::tuple(value_elems) + })); + expected_args.push(param_ty); + } + + tracing::info!( + expected = %crate::pretty::FunctionType::new(&expected_args, &expected_ret).display(), + "rust-call expanded", + ); + } + } + // TODO: check sty and length is equal let mut builder = self.env.build_clause(); for (param_idx, param_rty) in got.params.iter_enumerated() { diff --git a/src/chc.rs b/src/chc.rs index a4f70af..a5f046e 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -623,6 +623,10 @@ impl Term { Term::Mut(Box::new(t1), Box::new(t2)) } + pub fn boxed(self) -> Self { + Term::Box(Box::new(self)) + } + pub fn box_current(self) -> Self { Term::BoxCurrent(Box::new(self)) } diff --git a/src/rty.rs b/src/rty.rs index b780d44..d5d88d2 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1351,6 +1351,29 @@ impl RefinedType { RefinedType { ty, refinement } } + pub fn deref(self) -> Self { + let RefinedType { + ty, + refinement: outer_refinement, + } = self; + let inner_ty = ty.into_pointer().expect("invalid deref"); + if inner_ty.is_mut() { + // losing info about proph + panic!("invalid deref"); + } + let RefinedType { + ty: inner_ty, + refinement: mut inner_refinement, + } = *inner_ty.elem; + inner_refinement.push_conj( + outer_refinement.subst_value_var(|| chc::Term::var(RefinedTypeVar::Value).boxed()), + ); + RefinedType { + ty: inner_ty, + refinement: inner_refinement, + } + } + pub fn subst_var(self, mut f: F) -> RefinedType where F: FnMut(FV) -> chc::Term, diff --git a/tests/ui/fail/closure_mut.rs b/tests/ui/fail/closure_mut.rs new file mode 100644 index 0000000..0b0a8ea --- /dev/null +++ b/tests/ui/fail/closure_mut.rs @@ -0,0 +1,12 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut x = 1; + let mut incr = |by: i32| { + x += by; + }; + incr(5); + incr(5); + assert!(x == 10); +} diff --git a/tests/ui/pass/closure_mut.rs b/tests/ui/pass/closure_mut.rs new file mode 100644 index 0000000..d50c074 --- /dev/null +++ b/tests/ui/pass/closure_mut.rs @@ -0,0 +1,12 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut x = 1; + let mut incr = |by: i32| { + x += by; + }; + incr(5); + incr(5); + assert!(x == 11); +} From d2692ae3ba3bcd968fdb31b2d521da50e07744f0 Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 24 Nov 2025 01:12:39 +0900 Subject: [PATCH 6/7] Enable to type unit via ZeroSized --- src/analyze/basic_block.rs | 6 ++++++ tests/ui/fail/closure_mut_0.rs | 12 ++++++++++++ tests/ui/fail/closure_param.rs | 14 ++++++++++++++ tests/ui/pass/closure_mut_0.rs | 11 +++++++++++ tests/ui/pass/closure_param.rs | 14 ++++++++++++++ 5 files changed, 57 insertions(+) create mode 100644 tests/ui/fail/closure_mut_0.rs create mode 100644 tests/ui/fail/closure_param.rs create mode 100644 tests/ui/pass/closure_mut_0.rs create mode 100644 tests/ui/pass/closure_param.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 848eba0..907146a 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -213,6 +213,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { chc::Term::bool(val.try_to_bool().unwrap()), ) } + (mir_ty::TyKind::Tuple(tys), _) if tys.is_empty() => { + PlaceType::with_ty_and_term(rty::Type::unit(), chc::Term::tuple(vec![])) + } + (mir_ty::TyKind::Closure(_, args), _) if args.as_closure().upvar_tys().is_empty() => { + PlaceType::with_ty_and_term(rty::Type::unit(), chc::Term::tuple(vec![])) + } ( mir_ty::TyKind::Ref(_, elem, Mutability::Not), ConstValue::Scalar(Scalar::Ptr(ptr, _)), diff --git a/tests/ui/fail/closure_mut_0.rs b/tests/ui/fail/closure_mut_0.rs new file mode 100644 index 0000000..a08196d --- /dev/null +++ b/tests/ui/fail/closure_mut_0.rs @@ -0,0 +1,12 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut x = 1; + x += 1; + let mut incr = || { + x += 1; + }; + incr(); + assert!(x == 2); +} diff --git a/tests/ui/fail/closure_param.rs b/tests/ui/fail/closure_param.rs new file mode 100644 index 0000000..bd9dc23 --- /dev/null +++ b/tests/ui/fail/closure_param.rs @@ -0,0 +1,14 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn take_fn T>(f: F) -> T { + f(42) +} + +fn main() { + let y = take_fn(|x| { + assert!(x == 41); + x + 1 + }); + assert!(y == 42); +} diff --git a/tests/ui/pass/closure_mut_0.rs b/tests/ui/pass/closure_mut_0.rs new file mode 100644 index 0000000..5f39a0f --- /dev/null +++ b/tests/ui/pass/closure_mut_0.rs @@ -0,0 +1,11 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut x = 1; + let mut incr = || { + x += 1; + }; + incr(); + assert!(x == 2); +} diff --git a/tests/ui/pass/closure_param.rs b/tests/ui/pass/closure_param.rs new file mode 100644 index 0000000..0188ca9 --- /dev/null +++ b/tests/ui/pass/closure_param.rs @@ -0,0 +1,14 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn take_fn T>(f: F) -> T { + f(41) +} + +fn main() { + let y = take_fn(|x| { + assert!(x == 41); + x + 1 + }); + assert!(y == 42); +} From 3a0ccfe6ef0b576aeaad96a19ec1fc786af5a6f4 Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 24 Nov 2025 01:31:18 +0900 Subject: [PATCH 7/7] Ensure bb fn type params are sorted by locals --- src/refine/template.rs | 5 ++++- tests/ui/fail/closure_no_capture.rs | 9 +++++++++ tests/ui/pass/closure_no_capture.rs | 9 +++++++++ 3 files changed, 22 insertions(+), 1 deletion(-) create mode 100644 tests/ui/fail/closure_no_capture.rs create mode 100644 tests/ui/pass/closure_no_capture.rs diff --git a/src/refine/template.rs b/src/refine/template.rs index b57dae5..da8e4b6 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -309,9 +309,12 @@ where where I: IntoIterator)>, { + // this is necessary for local_def::Analyzer::elaborate_unused_args + let mut live_locals: Vec<_> = live_locals.into_iter().collect(); + live_locals.sort_by_key(|(local, _)| *local); + let mut locals = IndexVec::::new(); let mut tys = Vec::new(); - // TODO: avoid two iteration and assumption of FunctionParamIdx match between locals and ty for (local, ty) in live_locals { locals.push((local, ty.mutbl)); tys.push(ty); diff --git a/tests/ui/fail/closure_no_capture.rs b/tests/ui/fail/closure_no_capture.rs new file mode 100644 index 0000000..edabc34 --- /dev/null +++ b/tests/ui/fail/closure_no_capture.rs @@ -0,0 +1,9 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let incr = |x| { + x + 1 + }; + assert!(incr(2) == 2); +} diff --git a/tests/ui/pass/closure_no_capture.rs b/tests/ui/pass/closure_no_capture.rs new file mode 100644 index 0000000..02f38aa --- /dev/null +++ b/tests/ui/pass/closure_no_capture.rs @@ -0,0 +1,9 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let incr = |x| { + x + 1 + }; + assert!(incr(1) == 2); +}