From c01320997fd8862e272c83c2f2fae7607de8d003 Mon Sep 17 00:00:00 2001 From: coord_e Date: Sat, 14 Feb 2026 12:24:32 +0900 Subject: [PATCH 1/7] Introduce Array sort --- src/chc.rs | 31 ++++++++++++++++- src/chc/format_context.rs | 72 ++++++++++++++++++++++++--------------- src/chc/hoice.rs | 4 +-- src/chc/unbox.rs | 1 + src/rty.rs | 4 +++ 5 files changed, 81 insertions(+), 31 deletions(-) diff --git a/src/chc.rs b/src/chc.rs index 4f1b2c9..5030aa2 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -95,6 +95,7 @@ pub enum Sort { Box(Box), Mut(Box), Tuple(Vec), + Array(Box, Box), Datatype(DatatypeSort), } @@ -137,6 +138,21 @@ where .group() } } + Sort::Array(s1, s2) => { + if matches!(**s1, Sort::Int) { + s2.pretty(allocator).brackets() + } else { + allocator.text("array").append( + allocator + .line() + .append(s1.pretty_atom(allocator)) + .append(allocator.text("->")) + .append(allocator.line()) + .append(s2.pretty_atom(allocator)) + .parens(), + ) + } + } Sort::Datatype(sort) => sort.pretty(allocator), } } @@ -164,18 +180,22 @@ impl Sort { fn walk_impl<'a, 'b>(&'a self, mut f: Box) { f(self); match self { + Sort::Null | Sort::Int | Sort::Bool | Sort::String | Sort::Param(_) => {} Sort::Box(s) | Sort::Mut(s) => s.walk(Box::new(&mut f)), Sort::Tuple(ss) => { for s in ss { s.walk(Box::new(&mut f)); } } + Sort::Array(s1, s2) => { + s1.walk(Box::new(&mut f)); + s2.walk(Box::new(&mut f)); + } Sort::Datatype(sort) => { for s in &sort.args { s.walk(Box::new(&mut f)); } } - _ => {} } } @@ -233,6 +253,10 @@ impl Sort { Sort::Tuple(sorts) } + pub fn array(from: Sort, to: Sort) -> Self { + Sort::Array(Box::new(from), Box::new(to)) + } + pub fn datatype(symbol: DatatypeSymbol, args: Vec) -> Self { Sort::Datatype(DatatypeSort { symbol, args }) } @@ -257,6 +281,7 @@ impl Sort { Sort::Tuple(ts) => ts.iter().all(Sort::is_singleton), Sort::Box(s) => s.is_singleton(), Sort::Mut(s) => s.is_singleton(), + Sort::Array(_, s) => s.is_singleton(), _ => false, } } @@ -271,6 +296,10 @@ impl Sort { s.instantiate_params(args); } } + Sort::Array(s1, s2) => { + s1.instantiate_params(args); + s2.instantiate_params(args); + } Sort::Datatype(sort) => { for s in &mut sort.args { s.instantiate_params(args); diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index 2123315..9454827 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -68,11 +68,11 @@ fn atom_sorts(clause: &chc::Clause, a: &chc::Atom, sorts: &mut BTreeSet { +pub(super) struct SortSymbol<'a> { inner: &'a chc::Sort, } -impl<'a> std::fmt::Display for Sort<'a> { +impl<'a> std::fmt::Display for SortSymbol<'a> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self.inner { chc::Sort::Null => write!(f, "Null"), @@ -80,15 +80,18 @@ impl<'a> std::fmt::Display for Sort<'a> { chc::Sort::Bool => write!(f, "Bool"), chc::Sort::String => write!(f, "String"), chc::Sort::Param(i) => write!(f, "T{}", i), - chc::Sort::Box(s) => write!(f, "Box{}", Sort::new(s).sorts()), - chc::Sort::Mut(s) => write!(f, "Mut{}", Sort::new(s).sorts()), - chc::Sort::Tuple(ss) => write!(f, "Tuple{}", Sorts::new(ss)), - chc::Sort::Datatype(s) => write!(f, "{}{}", s.symbol, Sorts::new(&s.args)), + chc::Sort::Box(s) => write!(f, "Box{}", SortSymbol::new(s).sorts()), + chc::Sort::Mut(s) => write!(f, "Mut{}", SortSymbol::new(s).sorts()), + chc::Sort::Tuple(ss) => write!(f, "Tuple{}", SortSymbols::new(ss)), + chc::Sort::Array(s1, s2) => { + write!(f, "Array{}", SortSymbols::new(&[*s1.clone(), *s2.clone()])) + } + chc::Sort::Datatype(s) => write!(f, "{}{}", s.symbol, SortSymbols::new(&s.args)), } } } -impl<'a> Sort<'a> { +impl<'a> SortSymbol<'a> { pub fn new(inner: &'a chc::Sort) -> Self { Self { inner } } @@ -103,11 +106,11 @@ impl<'a> Sort<'a> { } #[derive(Debug, Clone)] -struct Sorts<'a> { +struct SortSymbols<'a> { inner: &'a [chc::Sort], } -impl<'a> std::fmt::Display for Sorts<'a> { +impl<'a> std::fmt::Display for SortSymbols<'a> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { if self.inner.is_empty() { return Ok(()); @@ -117,21 +120,21 @@ impl<'a> std::fmt::Display for Sorts<'a> { if i != 0 { write!(f, "-")?; } - write!(f, "{}", Sort::new(s))?; + write!(f, "{}", SortSymbol::new(s))?; } write!(f, ">")?; Ok(()) } } -impl<'a> Sorts<'a> { +impl<'a> SortSymbols<'a> { pub fn new(inner: &'a [chc::Sort]) -> Self { Self { inner } } } fn builtin_sort_datatype(s: chc::Sort) -> Option { - let symbol = Sort::new(&s).to_symbol(); + let symbol = SortSymbol::new(&s).to_symbol(); let d = match s { chc::Sort::Null => chc::Datatype { symbol, @@ -143,7 +146,7 @@ fn builtin_sort_datatype(s: chc::Sort) -> Option { }], }, chc::Sort::Box(inner) => { - let ss = Sort::new(&inner).sorts(); + let ss = SortSymbol::new(&inner).sorts(); chc::Datatype { symbol, params: 0, @@ -158,7 +161,7 @@ fn builtin_sort_datatype(s: chc::Sort) -> Option { } } chc::Sort::Mut(inner) => { - let ss = Sort::new(&inner).sorts(); + let ss = SortSymbol::new(&inner).sorts(); chc::Datatype { symbol, params: 0, @@ -179,7 +182,7 @@ fn builtin_sort_datatype(s: chc::Sort) -> Option { } } chc::Sort::Tuple(elems) => { - let ss = Sorts::new(&elems); + let ss = SortSymbols::new(&elems); let selectors = elems .iter() .enumerate() @@ -229,7 +232,7 @@ fn monomorphize_datatype( if datatype.params == 0 { return None; } - let ss = Sorts::new(&sort.args); + let ss = SortSymbols::new(&sort.args); let mono_datatype = chc::Datatype { symbol: chc::DatatypeSymbol::new(format!("{}{}", datatype.symbol, ss)), params: 0, @@ -281,37 +284,37 @@ impl FormatContext { } pub fn box_ctor(&self, sort: &chc::Sort) -> impl std::fmt::Display { - let ss = Sort::new(sort).sorts(); + let ss = SortSymbol::new(sort).sorts(); format!("box{ss}") } pub fn box_current(&self, sort: &chc::Sort) -> impl std::fmt::Display { - let ss = Sort::new(sort).sorts(); + let ss = SortSymbol::new(sort).sorts(); format!("box_current{ss}") } pub fn mut_ctor(&self, sort: &chc::Sort) -> impl std::fmt::Display { - let ss = Sort::new(sort).sorts(); + let ss = SortSymbol::new(sort).sorts(); format!("mut{ss}") } pub fn mut_current(&self, sort: &chc::Sort) -> impl std::fmt::Display { - let ss = Sort::new(sort).sorts(); + let ss = SortSymbol::new(sort).sorts(); format!("mut_current{ss}") } pub fn mut_final(&self, sort: &chc::Sort) -> impl std::fmt::Display { - let ss = Sort::new(sort).sorts(); + let ss = SortSymbol::new(sort).sorts(); format!("mut_final{ss}") } pub fn tuple_ctor(&self, sorts: &[chc::Sort]) -> impl std::fmt::Display { - let ss = Sorts::new(sorts); + let ss = SortSymbols::new(sorts); format!("tuple{ss}") } pub fn tuple_proj(&self, sorts: &[chc::Sort], idx: usize) -> impl std::fmt::Display { - let ss = Sorts::new(sorts); + let ss = SortSymbols::new(sorts); format!("tuple_proj{ss}.{idx}") } @@ -320,12 +323,12 @@ impl FormatContext { sort: &chc::DatatypeSort, ctor_sym: &chc::DatatypeSymbol, ) -> impl std::fmt::Display { - let ss = Sorts::new(&sort.args); + let ss = SortSymbols::new(&sort.args); format!("{}{}", ctor_sym, ss) } pub fn datatype_discr(&self, sort: &chc::DatatypeSort) -> impl std::fmt::Display { - let ss = Sorts::new(&sort.args); + let ss = SortSymbols::new(&sort.args); let sym = chc::DatatypeSymbol::new(format!("{}{}", sort.symbol, ss)); self.datatype_discr_def(&sym) } @@ -335,7 +338,7 @@ impl FormatContext { } pub fn matcher_pred(&self, p: &chc::MatcherPred) -> impl std::fmt::Display { - let ss = Sorts::new(&p.datatype_args); + let ss = SortSymbols::new(&p.datatype_args); let sym = chc::DatatypeSymbol::new(format!("{}{}", p.datatype_symbol, ss)); self.matcher_pred_def(&sym) } @@ -344,9 +347,22 @@ impl FormatContext { format!("matcher_pred<{}>", self.fmt_datatype_symbol(sym)) } + fn fmt_sort_impl(&self, sort: &chc::Sort) -> Box { + match sort { + chc::Sort::Array(s1, s2) => { + let s1 = self.fmt_sort(s1); + let s2 = self.fmt_sort(s2); + Box::new(format!("(Array {} {})", s1, s2)) + } + _ => { + let sym = SortSymbol::new(sort).to_symbol(); + Box::new(self.fmt_datatype_symbol(&sym)) + } + } + } + pub fn fmt_sort(&self, sort: &chc::Sort) -> impl std::fmt::Display { - let sym = Sort::new(sort).to_symbol(); - self.fmt_datatype_symbol(&sym) + self.fmt_sort_impl(sort) } pub fn fmt_datatype_symbol(&self, sym: &chc::DatatypeSymbol) -> impl std::fmt::Display { diff --git a/src/chc/hoice.rs b/src/chc/hoice.rs index c7c1cd8..ee62691 100644 --- a/src/chc/hoice.rs +++ b/src/chc/hoice.rs @@ -16,8 +16,8 @@ fn symbol_references(ty: &chc::Datatype) -> Vec { for ctor in &ty.ctors { for selector in &ctor.selectors { selector.sort.walk(|s| { - // TODO: stop using format_context::Sort directly - res.push(chc::format_context::Sort::new(s).to_symbol()); + // TODO: stop using format_context::SortSymbol directly + res.push(chc::format_context::SortSymbol::new(s).to_symbol()); }); } } diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index cb5ce8f..b3b24d5 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -70,6 +70,7 @@ fn unbox_sort(sort: Sort) -> Sort { Sort::Box(inner) => unbox_sort(*inner), Sort::Mut(inner) => Sort::Mut(Box::new(unbox_sort(*inner))), Sort::Tuple(sorts) => Sort::Tuple(sorts.into_iter().map(unbox_sort).collect()), + Sort::Array(s1, s2) => Sort::Array(Box::new(unbox_sort(*s1)), Box::new(unbox_sort(*s2))), Sort::Datatype(sort) => Sort::Datatype(unbox_datatype_sort(sort)), } } diff --git a/src/rty.rs b/src/rty.rs index 331a9a0..5eb69c9 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1539,6 +1539,10 @@ fn subst_ty_params_in_sort(sort: &mut chc::Sort, subst: &TypeParamSubst) { subst_ty_params_in_sort(s, subst); } } + chc::Sort::Array(s1, s2) => { + subst_ty_params_in_sort(s1, subst); + subst_ty_params_in_sort(s2, subst); + } chc::Sort::Datatype(dt_sort) => { for s in dt_sort.args_mut() { subst_ty_params_in_sort(s, subst); From 568b85811aa38dd393ccf7943efdb7a96367f187 Mon Sep 17 00:00:00 2001 From: coord_e Date: Sat, 14 Feb 2026 14:02:58 +0900 Subject: [PATCH 2/7] Add Type::Array --- src/rty.rs | 102 +++++++++++++++++++++++++++++++++++++++++++ src/rty/subtyping.rs | 6 +++ 2 files changed, 108 insertions(+) diff --git a/src/rty.rs b/src/rty.rs index 5eb69c9..7e45866 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -635,6 +635,89 @@ impl ParamType { } } +/// An array type. +#[derive(Debug, Clone)] +pub struct ArrayType { + pub index: Box>, + pub elem: Box>, +} + +impl<'a, 'b, T, D> Pretty<'a, D, termcolor::ColorSpec> for &'b ArrayType +where + T: chc::Var, + D: pretty::DocAllocator<'a, termcolor::ColorSpec>, + D::Doc: Clone, +{ + fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { + allocator.text("Array").append( + self.index + .pretty(allocator) + .append(allocator.text(", ")) + .append(self.elem.pretty(allocator)) + .angles(), + ) + } +} + +impl ArrayType { + pub fn new(index: Type, elem: Type) -> Self { + ArrayType { + index: Box::new(RefinedType::unrefined(index)), + elem: Box::new(RefinedType::unrefined(elem)), + } + } + + pub fn subst_var(self, mut f: F) -> ArrayType + where + F: FnMut(T) -> chc::Term, + { + ArrayType { + index: Box::new(self.index.subst_var(&mut f)), + elem: Box::new(self.elem.subst_var(&mut f)), + } + } + + pub fn map_var(self, mut f: F) -> ArrayType + where + F: FnMut(T) -> U, + { + ArrayType { + index: Box::new(self.index.map_var(&mut f)), + elem: Box::new(self.elem.map_var(&mut f)), + } + } + + pub fn strip_refinement(self) -> ArrayType { + ArrayType { + index: Box::new(RefinedType::unrefined(self.index.strip_refinement())), + elem: Box::new(RefinedType::unrefined(self.elem.strip_refinement())), + } + } + + pub fn free_ty_params(&self) -> HashSet { + self.index + .free_ty_params() + .into_iter() + .chain(self.elem.free_ty_params()) + .collect() + } + + pub fn subst_ty_params(&mut self, subst: &TypeParamSubst) + where + T: chc::Var, + { + self.index.subst_ty_params(subst); + self.elem.subst_ty_params(subst); + } + + pub fn unify_ty_params(self, other: ArrayType) -> TypeParamSubst + where + T: chc::Var, + { + unify_tys_params([*self.index, *self.elem], [*other.index, *other.elem]) + } +} + /// An underlying type of a refinement type. #[derive(Debug, Clone)] pub enum Type { @@ -646,6 +729,7 @@ pub enum Type { Pointer(PointerType), Function(FunctionType), Tuple(TupleType), + Array(ArrayType), Enum(EnumType), } @@ -673,6 +757,12 @@ impl From> for Type { } } +impl From> for Type { + fn from(t: ArrayType) -> Type { + Type::Array(t) + } +} + impl From> for Type { fn from(t: EnumType) -> Type { Type::Enum(t) @@ -695,6 +785,7 @@ where Type::Pointer(ty) => ty.pretty(allocator), Type::Function(ty) => ty.pretty(allocator), Type::Tuple(ty) => ty.pretty(allocator), + Type::Array(ty) => ty.pretty(allocator), Type::Enum(ty) => ty.pretty(allocator), } } @@ -839,6 +930,11 @@ impl Type { let elem_sorts = ty.elems.iter().map(|ty| ty.ty.to_sort()).collect(); chc::Sort::tuple(elem_sorts) } + Type::Array(ty) => { + let index_sort = ty.index.ty.to_sort(); + let elem_sort = ty.elem.ty.to_sort(); + chc::Sort::array(index_sort, elem_sort) + } Type::Enum(ty) => { let arg_sorts = ty.args.iter().map(|ty| ty.ty.to_sort()).collect(); chc::Sort::datatype(ty.symbol.clone(), arg_sorts) @@ -859,6 +955,7 @@ impl Type { Type::Pointer(ty) => Type::Pointer(ty.subst_var(f)), Type::Function(ty) => Type::Function(ty), Type::Tuple(ty) => Type::Tuple(ty.subst_var(f)), + Type::Array(ty) => Type::Array(ty.subst_var(f)), Type::Enum(ty) => Type::Enum(ty.subst_var(f)), } } @@ -876,6 +973,7 @@ impl Type { Type::Pointer(ty) => Type::Pointer(ty.map_var(f)), Type::Function(ty) => Type::Function(ty), Type::Tuple(ty) => Type::Tuple(ty.map_var(f)), + Type::Array(ty) => Type::Array(ty.map_var(f)), Type::Enum(ty) => Type::Enum(ty.map_var(f)), } } @@ -894,6 +992,7 @@ impl Type { Type::Pointer(ty) => Type::Pointer(ty.strip_refinement()), Type::Function(ty) => Type::Function(ty), Type::Tuple(ty) => Type::Tuple(ty.strip_refinement()), + Type::Array(ty) => Type::Array(ty.strip_refinement()), Type::Enum(ty) => Type::Enum(ty.strip_refinement()), } } @@ -905,6 +1004,7 @@ impl Type { Type::Pointer(ty) => ty.free_ty_params(), Type::Function(ty) => ty.free_ty_params(), Type::Tuple(ty) => ty.free_ty_params(), + Type::Array(ty) => ty.free_ty_params(), Type::Enum(ty) => ty.free_ty_params(), } } @@ -1471,6 +1571,7 @@ impl RefinedType { ty.subst_ty_params(&subst) } Type::Tuple(ty) => ty.subst_ty_params(subst), + Type::Array(ty) => ty.subst_ty_params(subst), Type::Enum(ty) => ty.subst_ty_params(subst), } } @@ -1509,6 +1610,7 @@ impl RefinedType { ty1.unify_ty_params(ty2).strip_refinement().vacuous() } (Type::Tuple(ty1), Type::Tuple(ty2)) => ty1.unify_ty_params(ty2), + (Type::Array(ty1), Type::Array(ty2)) => ty1.unify_ty_params(ty2), (Type::Enum(ty1), Type::Enum(ty2)) => ty1.unify_ty_params(ty2), (t1, t2) => panic!("unify_ty_params: mismatched types t1={:?}, t2={:?}", t1, t2), } diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs index 82465a8..20d6f34 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -114,6 +114,12 @@ where let cs = builder.relate_sub_refined_type(&got.ret, &expected.ret); clauses.extend(cs); } + (Type::Array(got), Type::Array(expected)) => { + let cs1 = self.relate_sub_refined_type(&got.index, &expected.index); + clauses.extend(cs1); + let cs2 = self.relate_sub_refined_type(&got.elem, &expected.elem); + clauses.extend(cs2); + } _ => panic!( "inconsistent types: got={}, expected={}", got.display(), From 031b8b1b9c1f10bf763a97b179564ee7bc863704 Mon Sep 17 00:00:00 2001 From: coord_e Date: Sat, 14 Feb 2026 23:00:08 +0900 Subject: [PATCH 3/7] Enable Uint const evaulation --- src/analyze/basic_block.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index a785495..bba37ce 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -209,7 +209,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { 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))) => { + ( + mir_ty::TyKind::Int(_) | mir_ty::TyKind::Uint(_), + ConstValue::Scalar(Scalar::Int(val)), + ) => { let val = val.try_to_int(val.size()).unwrap(); PlaceType::with_ty_and_term( rty::Type::int(), From b6afbca886dfac5315d5cf101ed830e5ef4b56a0 Mon Sep 17 00:00:00 2001 From: coord_e Date: Sat, 14 Feb 2026 23:02:09 +0900 Subject: [PATCH 4/7] Parse select and store calls in annotations --- src/annot.rs | 76 ++++++++++++++++++++++++++++++++++++++++++++-------- src/chc.rs | 25 +++++++++++++++-- 2 files changed, 88 insertions(+), 13 deletions(-) diff --git a/src/annot.rs b/src/annot.rs index 769e0e5..270aed1 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -145,6 +145,8 @@ pub enum ParseAttrError { UnexpectedTerm { context: &'static str }, #[error("unexpected formula {context}")] UnexpectedFormula { context: &'static str }, + #[error("unknown method {ident:?} with {arg_count} arguments")] + UnknownMethod { ident: Ident, arg_count: usize }, } impl ParseAttrError { @@ -176,6 +178,10 @@ impl ParseAttrError { fn unexpected_formula(context: &'static str) -> Self { ParseAttrError::UnexpectedFormula { context } } + + fn unknown_method(ident: Ident, arg_count: usize) -> Self { + ParseAttrError::UnknownMethod { ident, arg_count } + } } type Result = std::result::Result; @@ -422,7 +428,7 @@ where } fn parse_arg_terms(&mut self) -> Result>> { - if self.look_ahead_token(0).is_none() { + if self.look_ahead_token_tree(0).is_none() { return Ok(Vec::new()); } @@ -607,23 +613,60 @@ where fn parse_postfix(&mut self) -> Result> { let formula_or_term = self.parse_atom()?; - let mut fields = Vec::new(); + enum Field { + Select(chc::Term), + Store(chc::Term, chc::Term), + Index(usize), + } + + let mut fields: Vec> = Vec::new(); while let Some(Token { kind: TokenKind::Dot, .. }) = self.look_ahead_token(0) { self.consume(); - match self.next_token("field")? { - Token { - kind: TokenKind::Literal(lit), - .. - } if matches!(lit.kind, LitKind::Integer) => { + let t = self.next_token("field")?.clone(); + if let Token { + kind: TokenKind::Literal(lit), + .. + } = t + { + if matches!(lit.kind, LitKind::Integer) { let idx = lit.symbol.as_str().parse().unwrap(); - fields.push(idx); + fields.push(Field::Index(idx)); + continue; } - t => return Err(ParseAttrError::unexpected_token("field", t.clone())), } + if let Some((ident, _)) = t.ident() { + let next_tt = self.look_ahead_token_tree(0); + if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, args)) = next_tt { + let args = args.clone(); + self.consume(); + let mut parser = Parser { + resolver: self.boxed_resolver(), + self_type_name: self.self_type_name.clone(), + cursor: args.trees(), + formula_existentials: self.formula_existentials.clone(), + }; + let args = parser.parse_arg_terms()?; + match ident.as_str() { + "select" if args.len() == 1 => { + fields.push(Field::Select(args.into_iter().next().unwrap())); + continue; + } + "store" if args.len() == 2 => { + let mut args = args.into_iter(); + let idx = args.next().unwrap(); + let val = args.next().unwrap(); + fields.push(Field::Store(idx, val)); + continue; + } + _ => return Err(ParseAttrError::unknown_method(ident, args.len())), + } + } + } + return Err(ParseAttrError::unexpected_token("field", t.clone())); } if fields.is_empty() { @@ -633,8 +676,19 @@ where let (term, sort) = formula_or_term .into_term() .ok_or_else(|| ParseAttrError::unexpected_formula("before projection"))?; - let term = fields.iter().fold(term, |acc, idx| acc.tuple_proj(*idx)); - let sort = fields.iter().fold(sort, |acc, idx| acc.tuple_elem(*idx)); + let sort = fields + .iter() + .try_fold(sort, |acc, field| match (acc, field) { + (acc, Field::Index(idx)) => Ok(acc.tuple_elem(*idx)), + (acc, Field::Store(_, _)) => Ok(acc), + (chc::Sort::Array(_, elem), Field::Select(_)) => Ok(*elem), + (acc, _) => Err(ParseAttrError::unsorted_op("select", acc.clone())), + })?; + let term = fields.into_iter().fold(term, |acc, field| match field { + Field::Index(idx) => acc.tuple_proj(idx), + Field::Store(idx, val) => acc.store(idx, val), + Field::Select(idx) => acc.select(idx), + }); Ok(FormulaOrTerm::Term(term, sort)) } diff --git a/src/chc.rs b/src/chc.rs index 5030aa2..f6b8fb9 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -390,7 +390,7 @@ impl Function { self.is_infix } - fn sort(&self, _args: I) -> Sort + fn sort(&self, args: I) -> Sort where I: IntoIterator, { @@ -405,6 +405,13 @@ impl Function { Self::LT => Sort::bool(), Self::NOT => Sort::bool(), Self::NEG => Sort::int(), + Self::STORE => args.into_iter().next().unwrap(), + Self::SELECT => { + let Sort::Array(_, elem) = args.into_iter().next().unwrap() else { + panic!("invalid SELECT sort"); + }; + *elem + } _ => unimplemented!(), } } @@ -419,6 +426,8 @@ impl Function { pub const LT: Function = Function::infix("<"); pub const NOT: Function = Function::new("not"); pub const NEG: Function = Function::new("-"); + pub const STORE: Function = Function::new("store"); + pub const SELECT: Function = Function::new("select"); } /// A logical term. @@ -590,7 +599,11 @@ impl Term { Term::BoxCurrent(t) => t.sort(var_sort).deref(), Term::MutCurrent(t) => t.sort(var_sort).deref(), Term::MutFinal(t) => t.sort(var_sort).deref(), - Term::App(fun, args) => fun.sort(args.iter().map(|t| t.sort(&mut var_sort))), + Term::App(fun, args) => { + // TODO: remove this + let mut var_sort: Box Sort> = Box::new(var_sort); + fun.sort(args.iter().map(|t| t.sort(&mut var_sort))) + } Term::Tuple(ts) => { // TODO: remove this let mut var_sort: Box Sort> = Box::new(var_sort); @@ -719,6 +732,14 @@ impl Term { Term::App(Function::NEG, vec![self]) } + pub fn select(self, index: Self) -> Self { + Term::App(Function::SELECT, vec![self, index]) + } + + pub fn store(self, index: Self, elem: Self) -> Self { + Term::App(Function::STORE, vec![self, index, elem]) + } + pub fn tuple(ts: Vec>) -> Self { Term::Tuple(ts) } From 1f80a696c0a2361d4f495509f6bcb5ca68da0156 Mon Sep 17 00:00:00 2001 From: coord_e Date: Sat, 14 Feb 2026 23:50:32 +0900 Subject: [PATCH 5/7] Use GenericArgs from Instance when resolved --- src/analyze/basic_block.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index bba37ce..f31e320 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -579,7 +579,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { { // TODO: handle const_fn_def on Env side let func_ty = if let Some((def_id, args)) = func.const_fn_def() { - let resolved_def_id = if self.ctx.is_fn_trait_method(def_id) { + let (resolved_def_id, resolved_args) = if self.ctx.is_fn_trait_method(def_id) { // When calling a closure via `Fn`/`FnMut`/`FnOnce` trait, // we simply replace the def_id with the closure's function def_id. // This skips shims, and makes self arguments mismatch. visitor::RustCallVisitor @@ -588,7 +588,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { panic!("expected closure arg for fn trait"); }; tracing::debug!(?closure_def_id, "closure instance"); - *closure_def_id + (*closure_def_id, args) } else { let param_env = self .tcx @@ -597,17 +597,17 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let instance = mir_ty::Instance::resolve(self.tcx, param_env, def_id, args).unwrap(); if let Some(instance) = instance { - instance.def_id() + (instance.def_id(), instance.args) } else { - def_id + (def_id, args) } }; if def_id != resolved_def_id { - tracing::info!(?def_id, ?resolved_def_id, "resolve",); + tracing::info!(?def_id, ?resolved_def_id, ?resolved_args, "resolved"); } self.ctx - .def_ty_with_args(resolved_def_id, args) + .def_ty_with_args(resolved_def_id, resolved_args) .expect("unknown def") .ty .vacuous() From e46ca39d2fe4fa7c6d21da39dea087c499647cec Mon Sep 17 00:00:00 2001 From: coord_e Date: Sat, 14 Feb 2026 23:50:54 +0900 Subject: [PATCH 6/7] Resolve in thrust::extern_spec_fn --- src/analyze/local_def.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 11a3524..c1b0f7b 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -387,7 +387,16 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { rustc_hir::def::DefKind::Fn | rustc_hir::def::DefKind::AssocFn ) { assert!(self.inner_def_id.is_none(), "invalid extern_spec_fn"); - self.inner_def_id = Some(def_id); + + let args = typeck_result.node_args(hir_id); + let param_env = self.tcx.param_env(self.outer_def_id); + let instance = + mir_ty::Instance::resolve(self.tcx, param_env, def_id, args).unwrap(); + if let Some(instance) = instance { + self.inner_def_id = Some(instance.def_id()); + } else { + self.inner_def_id = Some(def_id); + } } } } From 839cf5c4b51793316ec63dbce722d0f56759b645 Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 15 Feb 2026 00:10:13 +0900 Subject: [PATCH 7/7] Support some of std::vec::Vec methods --- src/refine/template.rs | 16 ++++++++ std.rs | 87 ++++++++++++++++++++++++++++++++++++++++++ tests/ui/fail/vec_1.rs | 8 ++++ tests/ui/fail/vec_2.rs | 10 +++++ tests/ui/fail/vec_3.rs | 14 +++++++ tests/ui/pass/vec_1.rs | 9 +++++ tests/ui/pass/vec_2.rs | 11 ++++++ tests/ui/pass/vec_3.rs | 14 +++++++ 8 files changed, 169 insertions(+) create mode 100644 tests/ui/fail/vec_1.rs create mode 100644 tests/ui/fail/vec_2.rs create mode 100644 tests/ui/fail/vec_3.rs create mode 100644 tests/ui/pass/vec_1.rs create mode 100644 tests/ui/pass/vec_2.rs create mode 100644 tests/ui/pass/vec_3.rs diff --git a/src/refine/template.rs b/src/refine/template.rs index 29ff975..6d3b5dd 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -141,6 +141,13 @@ impl<'tcx> TypeBuilder<'tcx> { mir_ty::TyKind::Adt(def, params) if def.is_box() => { rty::PointerType::own(self.build(params.type_at(0))).into() } + // TODO: Declare this in std.rs + mir_ty::TyKind::Adt(def, params) + if self.tcx.is_diagnostic_item(rustc_span::sym::Vec, def.did()) => + { + let content = rty::ArrayType::new(rty::Type::Int, self.build(params.type_at(0))); + rty::TupleType::new(vec![content.into(), rty::Type::Int]).into() + } mir_ty::TyKind::Adt(def, params) => { if def.is_enum() { let sym = refine::datatype_symbol(self.tcx, def.did()); @@ -269,6 +276,15 @@ where mir_ty::TyKind::Adt(def, params) if def.is_box() => { rty::PointerType::own(self.build(params.type_at(0))).into() } + mir_ty::TyKind::Adt(def, params) + if self + .inner + .tcx + .is_diagnostic_item(rustc_span::sym::Vec, def.did()) => + { + let content = rty::ArrayType::new(rty::Type::Int, self.build(params.type_at(0))); + rty::TupleType::new(vec![content.into(), rty::Type::Int]).into() + } mir_ty::TyKind::Adt(def, params) => { if def.is_enum() { let sym = refine::datatype_symbol(self.inner.tcx, def.did()); diff --git a/std.rs b/std.rs index 206d5ea..d823a4a 100644 --- a/std.rs +++ b/std.rs @@ -201,3 +201,90 @@ fn _extern_spec_i32_is_positive(x: i32) -> bool { fn _extern_spec_i32_is_negative(x: i32) -> bool { i32::is_negative(x) } + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures(result.1 == 0)] +fn _extern_spec_vec_new() -> Vec { + Vec::::new() +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures(^vec == ((*vec).0.store((*vec).1, elem), (*vec).1 + 1))] +fn _extern_spec_vec_push(vec: &mut Vec, elem: T) { + Vec::push(vec, elem) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures(result == (*vec).1)] +fn _extern_spec_vec_len(vec: &Vec) -> usize { + Vec::len(vec) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(index < (*vec).1)] +#[thrust::ensures(*result == (*vec).0.select(index))] +fn _extern_spec_vec_index(vec: &Vec, index: usize) -> &T { + as std::ops::Index>::index(vec, index) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(index < (*vec).1)] +#[thrust::ensures( + *result == (*vec).0.select(index) && + ^result == (^vec).0.select(index) && + ^vec == ((*vec).0.store(index, ^result), (*vec).1) +)] +fn _extern_spec_vec_index_mut(vec: &mut Vec, index: usize) -> &mut T { + as std::ops::IndexMut>::index_mut(vec, index) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures((^vec).1 == 0)] +fn _extern_spec_vec_clear(vec: &mut Vec) { + Vec::clear(vec) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (^vec).0 == (*vec).0 && ( + ( + (*vec).1 > 0 && + (^vec).1 == (*vec).1 - 1 && + result == std::option::Option::::Some((*vec).0.select((*vec).1 - 1)) + ) || ( + (*vec).1 == 0 && + (^vec).1 == 0 && + result == std::option::Option::::None() + ) + ) +)] +fn _extern_spec_vec_pop(vec: &mut Vec) -> Option { + Vec::pop(vec) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures(result == ((*vec).1 == 0))] +fn _extern_spec_vec_is_empty(vec: &Vec) -> bool { + Vec::is_empty(vec) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + ( + (*vec).1 > len && + ^vec == ((*vec).0, len) + ) || ( + (*vec).1 <= len && + ^vec == *vec + ) +)] +fn _extern_spec_vec_truncate(vec: &mut Vec, len: usize) { + Vec::truncate(vec, len) +} diff --git a/tests/ui/fail/vec_1.rs b/tests/ui/fail/vec_1.rs new file mode 100644 index 0000000..43f772b --- /dev/null +++ b/tests/ui/fail/vec_1.rs @@ -0,0 +1,8 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v = Vec::new(); + v.push(0); + assert!(v.len() == 0); +} diff --git a/tests/ui/fail/vec_2.rs b/tests/ui/fail/vec_2.rs new file mode 100644 index 0000000..420adb7 --- /dev/null +++ b/tests/ui/fail/vec_2.rs @@ -0,0 +1,10 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v = Vec::new(); + v.push(0); + v[0] += 1; + assert!(v.pop().unwrap() == 1); + assert!(v.pop().unwrap() == 1); +} diff --git a/tests/ui/fail/vec_3.rs b/tests/ui/fail/vec_3.rs new file mode 100644 index 0000000..811ce70 --- /dev/null +++ b/tests/ui/fail/vec_3.rs @@ -0,0 +1,14 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v = Vec::new(); + v.push(0); + v.push(1); + v.push(2); + assert!(v.len() == 2); + v.truncate(1); + assert!(v[1] == 0); + v.clear(); + assert!(v.len() == 1); +} diff --git a/tests/ui/pass/vec_1.rs b/tests/ui/pass/vec_1.rs new file mode 100644 index 0000000..cdab8ce --- /dev/null +++ b/tests/ui/pass/vec_1.rs @@ -0,0 +1,9 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v = Vec::new(); + v.push(0); + assert!(v.len() == 1); + assert!(v[0] == 0); +} diff --git a/tests/ui/pass/vec_2.rs b/tests/ui/pass/vec_2.rs new file mode 100644 index 0000000..419a351 --- /dev/null +++ b/tests/ui/pass/vec_2.rs @@ -0,0 +1,11 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v = Vec::new(); + v.push(0); + v[0] += 1; + v.push(1); + assert!(v.pop().unwrap() == 1); + assert!(v.pop().unwrap() == 1); +} diff --git a/tests/ui/pass/vec_3.rs b/tests/ui/pass/vec_3.rs new file mode 100644 index 0000000..a560af3 --- /dev/null +++ b/tests/ui/pass/vec_3.rs @@ -0,0 +1,14 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v = Vec::new(); + v.push(0); + v.push(1); + v.push(2); + assert!(v.len() == 3); + v.truncate(1); + assert!(v[0] == 0); + v.clear(); + assert!(v.len() == 0); +}