From 47a550d7b502dc7d3f5fe789c71acd7c91045159 Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 23 Nov 2025 21:43:28 +0900 Subject: [PATCH 1/8] Enable to handle some promoted constants --- src/analyze/basic_block.rs | 102 ++++++++++++++++++++++++++++++++++++- src/refine/env.rs | 53 ++++--------------- 2 files changed, 110 insertions(+), 45 deletions(-) diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 9f6ee49..095dd3e 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -125,11 +125,111 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { clauses } + fn const_bytes_ty( + &self, + ty: mir_ty::Ty<'tcx>, + alloc: mir::interpret::ConstAllocation, + range: std::ops::Range, + ) -> PlaceType { + let alloc = alloc.inner(); + let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(range); + match ty.kind() { + mir_ty::TyKind::Str => { + let content = std::str::from_utf8(bytes).unwrap(); + PlaceType::with_ty_and_term( + rty::Type::string(), + chc::Term::string(content.to_owned()), + ) + } + mir_ty::TyKind::Bool => { + PlaceType::with_ty_and_term(rty::Type::bool(), chc::Term::bool(bytes[0] != 0)) + } + mir_ty::Int(_) => { + // TODO: see target endianess + let val = match bytes.len() { + 1 => i8::from_ne_bytes(bytes.try_into().unwrap()) as i64, + 2 => i16::from_ne_bytes(bytes.try_into().unwrap()) as i64, + 4 => i32::from_ne_bytes(bytes.try_into().unwrap()) as i64, + 8 => i64::from_ne_bytes(bytes.try_into().unwrap()), + _ => unimplemented!("const int bytes len: {}", bytes.len()), + }; + PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(val)) + } + _ => unimplemented!("const bytes ty: {:?}", ty), + } + } + + fn const_value_ty(&self, val: &mir::ConstValue<'tcx>, ty: &mir_ty::Ty<'tcx>) -> PlaceType { + use mir::{interpret::Scalar, ConstValue, Mutability}; + match (ty.kind(), val) { + (mir_ty::TyKind::Int(_), ConstValue::Scalar(Scalar::Int(val))) => { + let val = val.try_to_int(val.size()).unwrap(); + PlaceType::with_ty_and_term( + rty::Type::int(), + chc::Term::int(val.try_into().unwrap()), + ) + } + (mir_ty::TyKind::Bool, ConstValue::Scalar(Scalar::Int(val))) => { + PlaceType::with_ty_and_term( + rty::Type::bool(), + chc::Term::bool(val.try_to_bool().unwrap()), + ) + } + ( + mir_ty::TyKind::Ref(_, elem, Mutability::Not), + ConstValue::Scalar(Scalar::Ptr(ptr, _)), + ) => { + // Pointer::into_parts is OK for CtfeProvenance + // in later version of rustc it has prov_and_relative_offset that ensures this + let (prov, offset) = ptr.into_parts(); + let global_alloc = self.tcx.global_alloc(prov.alloc_id()); + match global_alloc { + mir::interpret::GlobalAlloc::Memory(alloc) => { + let layout = self + .tcx + .layout_of(mir_ty::ParamEnv::reveal_all().and(*elem)) + .unwrap(); + let size = layout.size; + let range = + offset.bytes() as usize..(offset.bytes() + size.bytes()) as usize; + self.const_bytes_ty(*elem, alloc, range).immut() + } + _ => unimplemented!("const ptr alloc: {:?}", global_alloc), + } + } + (mir_ty::TyKind::Ref(_, elem, Mutability::Not), ConstValue::Slice { data, meta }) => { + let end = (*meta).try_into().unwrap(); + self.const_bytes_ty(*elem, *data, 0..end).immut() + } + _ => unimplemented!("const: {:?}, ty: {:?}", val, ty), + } + } + + fn const_ty(&self, const_: &mir::Const<'tcx>) -> PlaceType { + match const_ { + mir::Const::Val(val, ty) => self.const_value_ty(val, ty), + mir::Const::Unevaluated(unevaluated, ty) => { + // since all constants are immutable in current setup, + // it should be okay to evaluate them here on-the-fly + let param_env = self.tcx.param_env(self.local_def_id); + let val = self + .tcx + .const_eval_resolve(param_env, *unevaluated, None) + .unwrap(); + self.const_value_ty(&val, ty) + } + _ => unimplemented!("const: {:?}", const_), + } + } + fn operand_type(&self, mut operand: Operand<'tcx>) -> PlaceType { if let Operand::Copy(p) | Operand::Move(p) = &mut operand { *p = self.elaborate_place(p); } - let ty = self.env.operand_type(operand.clone()); + let ty = match &operand { + Operand::Copy(place) | Operand::Move(place) => self.env.place_type(*place), + Operand::Constant(operand) => self.const_ty(&operand.const_), + }; tracing::debug!(operand = ?operand, ty = %ty.display(), "operand_type"); ty } diff --git a/src/refine/env.rs b/src/refine/env.rs index a1edbc1..f18dadb 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -2,8 +2,7 @@ use std::collections::{BTreeMap, HashMap}; use pretty::{termcolor, Pretty}; use rustc_index::IndexVec; -use rustc_middle::mir::{self, Local, Operand, Place, PlaceElem}; -use rustc_middle::ty as mir_ty; +use rustc_middle::mir::{Local, Place, PlaceElem}; use rustc_target::abi::{FieldIdx, VariantIdx}; use crate::chc; @@ -454,6 +453,14 @@ impl PlaceType { builder.build(ty, term) } + pub fn immut(self) -> PlaceType { + let mut builder = PlaceTypeBuilder::default(); + let (inner_ty, inner_term) = builder.subsume(self); + let ty = rty::PointerType::immut_to(inner_ty).into(); + let term = chc::Term::box_(inner_term); + builder.build(ty, term) + } + pub fn tuple(ptys: Vec) -> PlaceType { let mut builder = PlaceTypeBuilder::default(); let mut tys = Vec::new(); @@ -951,48 +958,6 @@ impl Env { self.var_type(local.into()) } - pub fn operand_type(&self, operand: Operand<'_>) -> PlaceType { - use mir::{interpret::Scalar, Const, ConstValue, Mutability}; - match operand { - Operand::Copy(place) | Operand::Move(place) => self.place_type(place), - Operand::Constant(operand) => { - let Const::Val(val, ty) = operand.const_ else { - unimplemented!("const: {:?}", operand.const_); - }; - match (ty.kind(), val) { - (mir_ty::TyKind::Int(_), ConstValue::Scalar(Scalar::Int(val))) => { - let val = val.try_to_int(val.size()).unwrap(); - PlaceType::with_ty_and_term( - rty::Type::int(), - chc::Term::int(val.try_into().unwrap()), - ) - } - (mir_ty::TyKind::Bool, ConstValue::Scalar(Scalar::Int(val))) => { - PlaceType::with_ty_and_term( - rty::Type::bool(), - chc::Term::bool(val.try_to_bool().unwrap()), - ) - } - ( - mir_ty::TyKind::Ref(_, elem, Mutability::Not), - ConstValue::Slice { data, meta }, - ) if matches!(elem.kind(), mir_ty::TyKind::Str) => { - let end = meta.try_into().unwrap(); - let content = data - .inner() - .inspect_with_uninit_and_ptr_outside_interpreter(0..end); - let content = std::str::from_utf8(content).unwrap(); - PlaceType::with_ty_and_term( - rty::PointerType::immut_to(rty::Type::string()).into(), - chc::Term::box_(chc::Term::string(content.to_owned())), - ) - } - _ => unimplemented!("const: {:?}, ty: {:?}", val, ty), - } - } - } - } - fn borrow_var(&mut self, var: Var, prophecy: TempVarIdx) -> PlaceType { match *self.flow_binding(var).expect("borrowing unbound var") { FlowBinding::Box(x) => { From 17e3a9ea56f9d3aae8ac6bd637b9b689a3e8f543 Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 23 Nov 2025 21:44:19 +0900 Subject: [PATCH 2/8] Resolve trait method DefId in type_call --- src/analyze/basic_block.rs | 14 +++++++++++++- tests/ui/fail/trait.rs | 22 ++++++++++++++++++++++ tests/ui/pass/trait.rs | 22 ++++++++++++++++++++++ 3 files changed, 57 insertions(+), 1 deletion(-) create mode 100644 tests/ui/fail/trait.rs create mode 100644 tests/ui/pass/trait.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 095dd3e..d04c1ba 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -572,9 +572,21 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { rty::FunctionType::new([param1, param2].into_iter().collect(), ret).into() } 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",); + } + let rty_args = args.types().map(|ty| self.type_builder.build(ty)).collect(); self.ctx - .def_ty_with_args(def_id, rty_args) + .def_ty_with_args(resolved_def_id, rty_args) .expect("unknown def") .ty .vacuous() 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/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()); +} From 5ca8cece8af4e484788acae8175146895992e79a Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 23 Nov 2025 21:45:39 +0900 Subject: [PATCH 3/8] Enable to type lifted closure functions --- src/analyze.rs | 22 ++++++++++++++++++++++ src/analyze/crate_.rs | 7 ++----- src/analyze/local_def.rs | 3 +-- 3 files changed, 25 insertions(+), 7 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index a1ebd34..d0cad7d 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -340,4 +340,26 @@ impl<'tcx> Analyzer<'tcx> { self.tcx.dcx().err(format!("verification error: {:?}", err)); } } + + // replacement of `self.tcx.fn_sig(local_def_id).instantiate_identity().skip_binder()` + // to workaround the following error when used with closures: + // > to get the signature of a closure, use `args.as_closure().sig()` not `fn_sig()` + pub fn local_fn_sig(&self, local_def_id: LocalDefId) -> mir_ty::FnSig<'tcx> { + let ty = self.tcx.type_of(local_def_id).instantiate_identity(); + let sig = if let mir_ty::TyKind::Closure(_, substs) = ty.kind() { + substs.as_closure().sig().skip_binder() + } else { + ty.fn_sig(self.tcx).skip_binder() + }; + + // take input/output from MIR body to obtain lifted closure function type + let body = self.tcx.optimized_mir(local_def_id); + self.tcx.mk_fn_sig( + body.args_iter().map(|arg| body.local_decls[arg].ty), + body.return_ty(), + sig.c_variadic, + sig.unsafety, + sig.abi, + ) + } } diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index e15ca49..d3d3b1d 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()); diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 58e4b8b..05ee058 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -169,8 +169,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } pub fn expected_ty(&mut self) -> rty::RefinedType { - let sig = self.tcx.fn_sig(self.local_def_id); - let sig = sig.instantiate_identity().skip_binder(); + let sig = self.ctx.local_fn_sig(self.local_def_id); let mut param_resolver = analyze::annot::ParamResolver::default(); for (input_ident, input_ty) in self From 965b92d2adf56151267354c07d1fbe232e77b60a Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 23 Nov 2025 21:46:12 +0900 Subject: [PATCH 4/8] 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 c859419..eb68665 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -189,6 +189,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), } } @@ -308,6 +309,7 @@ where unimplemented!("unsupported ADT: {:?}", ty); } } + mir_ty::TyKind::Closure(_, args) => self.build(args.as_closure().tupled_upvars_ty()), kind => unimplemented!("ty: {:?}", kind), } } From 9acc59f1d8a1deb6501b93f7e450dcc0bce13260 Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 24 Nov 2025 00:30:18 +0900 Subject: [PATCH 5/8] 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 eb68665..e812f4d 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -210,6 +210,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, @@ -225,6 +230,7 @@ impl<'tcx> TypeBuilder<'tcx> { param_rtys: Default::default(), param_refinement: None, ret_rty: None, + abi, } } } @@ -344,6 +350,7 @@ where param_rtys: Default::default(), param_refinement: None, ret_rty: None, + abi: Default::default(), } .build(); BasicBlockType { ty, locals } @@ -359,6 +366,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> { @@ -478,6 +486,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 ce6ef5e..4934316 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 da2918071c8402e9b2ff03ff7061a7132197a9fa Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 24 Nov 2025 00:30:44 +0900 Subject: [PATCH 6/8] 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 d04c1ba..eb94ad3 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 6f5db32..3516f4f 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -616,6 +616,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 4934316..ed933ec 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 3daf10d5c901c3281a147e58eeadd3171291baed Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 24 Nov 2025 01:12:39 +0900 Subject: [PATCH 7/8] Enable to type unit via ZeroSized --- src/analyze/basic_block.rs | 3 +++ tests/ui/fail/closure_mut_0.rs | 12 ++++++++++++ tests/ui/pass/closure_mut_0.rs | 11 +++++++++++ 3 files changed, 26 insertions(+) create mode 100644 tests/ui/fail/closure_mut_0.rs create mode 100644 tests/ui/pass/closure_mut_0.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index eb94ad3..afbd3a2 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -213,6 +213,9 @@ 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::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/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); +} From c222080ba67b8ea483f586df05aacc2eef8d4d42 Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 24 Nov 2025 01:31:18 +0900 Subject: [PATCH 8/8] 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 e812f4d..e204ecf 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -335,9 +335,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); +}