From 46c0d0d46341cb9af584219c84f452b77bec3d81 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 19 Sep 2026 03:06:31 +0000 Subject: [PATCH] Model unsigned integers as non-negative `usize`, `u32` and `u64` now have `thrust_models::model::UInt` as their model, and a value whose model is `UInt` is refined with `v >= 0`. The fact is an assumption where such a value is read and an obligation where one is produced, so unsigned subtraction that may underflow is now rejected. `TypeBuilder::build` therefore yields a `rty::RefinedType`. The refinement describes the value as a whole: a refinement nested in a type has no counterpart on the value side, where the analyzer keeps the facts about the parts of a value in the formula of a `PlaceType`, so nested positions are left unrefined. Enum variant fields are the exception, as they are related against the field's own value, and `EnumVariantDef` records them as refinement types. In annotations `Int` and `UInt` mix through `model::Integer`, and an `Array` of either integer model is indexed by both through `model::IndexModel`. An annotated refinement is conjoined onto what the model already says about the value rather than replacing it. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01RiJqqjcQaJoLMyZ5PJZ1dM --- src/analyze.rs | 3 - src/analyze/annot.rs | 8 ++ src/analyze/annot_fn.rs | 6 +- src/analyze/basic_block.rs | 20 ++-- src/analyze/did_cache.rs | 8 ++ src/chc.rs | 4 + src/refine/basic_block.rs | 5 +- src/refine/env.rs | 10 +- src/refine/template.rs | 142 ++++++++++++++++---------- src/rty.rs | 16 ++- std.rs | 181 ++++++++++++++++++++------------- tests/ui/fail/ghost_const.rs | 6 +- tests/ui/fail/unsigned_loop.rs | 12 +++ tests/ui/fail/unsigned_sub.rs | 9 ++ tests/ui/pass/ghost_const.rs | 6 +- tests/ui/pass/unsigned_loop.rs | 12 +++ tests/ui/pass/unsigned_sub.rs | 10 ++ 17 files changed, 298 insertions(+), 160 deletions(-) create mode 100644 tests/ui/fail/unsigned_loop.rs create mode 100644 tests/ui/fail/unsigned_sub.rs create mode 100644 tests/ui/pass/unsigned_loop.rs create mode 100644 tests/ui/pass/unsigned_sub.rs diff --git a/src/analyze.rs b/src/analyze.rs index fce97595..d6f9670c 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -441,7 +441,6 @@ impl<'tcx> Analyzer<'tcx> { generic_args .types() .map(|ty| type_builder.build(ty)) - .map(rty::RefinedType::unrefined) .collect(), ); def_ty.ty.as_function().cloned() @@ -484,7 +483,6 @@ impl<'tcx> Analyzer<'tcx> { generic_args .types() .map(|ty| type_builder.build(ty)) - .map(rty::RefinedType::unrefined) .collect(), ); return Some(def_ty); @@ -508,7 +506,6 @@ impl<'tcx> Analyzer<'tcx> { generic_args .types() .map(|ty| type_builder.build(ty)) - .map(rty::RefinedType::unrefined) .collect(), ); deferred_ty_cache diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 390518dc..8d4a81df 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -66,6 +66,14 @@ pub fn int_model_path() -> [Symbol; 3] { ] } +pub fn uint_model_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("uint_model"), + ] +} + pub fn mut_model_path() -> [Symbol; 3] { [ Symbol::intern("thrust"), diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 92a8b2c7..0518f68c 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -250,7 +250,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let term = if ty.to_sort().is_singleton() { // the analyzer don't expect params with singleton sorts to be used in formula... // FIXME: fix the analyzer side to uniformly accept all params - Self::singleton_term_for_ty(&ty).unwrap() + Self::singleton_term_for_ty(&ty.ty).unwrap() } else { chc::Term::var(param_idx) }; @@ -578,7 +578,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let generic_args = mir_ty::EarlyBinder::bind(generic_args).instantiate(self.tcx, self.generic_args); let elem_ty = generic_args.type_at(idx); - self.type_builder.build(elem_ty) + self.type_builder.build(elem_ty).ty } fn adt_arg_type_at( @@ -589,7 +589,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let mir_ty::TyKind::Adt(_, args) = self.expr_ty(expr).kind() else { panic!("expected ADT"); }; - self.type_builder.build(args.type_at(idx)) + self.type_builder.build(args.type_at(idx)).ty } fn variant_ctor_term( diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index e244aa3a..3afa3891 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -549,7 +549,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { // // TODO: Stop embedding knowledge of `<[T; N] as Model>::Ty` in the analyzer let mut builder = PlaceTypeBuilder::default(); - let elem_ty = self.type_builder.build(mir_elem_ty).vacuous(); + let elem_ty = self.type_builder.build(mir_elem_ty).vacuous().ty; let mut arr_term = chc::Term::array_empty(chc::Sort::int(), elem_ty.to_sort()); for (i, field) in fields.iter().enumerate() { @@ -583,7 +583,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .field_tys .clone() .into_iter() - .map(|ty| rty::RefinedType::unrefined(ty.vacuous())); + .map(|rty| rty.vacuous()); let rty_args: IndexVec<_, _> = args .types() @@ -658,7 +658,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { ) => { // Only treat unsizing as identity when both sides resolve to the same model. let mut op_pty = self.operand_type(operand); - let expected_ty = self.type_builder.build(ty).vacuous(); + let expected_ty = self.type_builder.build(ty).vacuous().ty; if op_pty.ty.to_sort() != expected_ty.to_sort() { unimplemented!("unsize cast: {:?} -> {:?}", op_pty.ty, expected_ty); } @@ -1049,17 +1049,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .expect("ghost formula function takes the ghost value as its first parameter"); let mut params: IndexVec<_, _> = param_tys .iter() - .map(|ty| rty::RefinedType::unrefined(self.type_builder.build(*ty)).vacuous()) + .map(|ty| self.type_builder.build(*ty).vacuous()) .collect(); if params.is_empty() { // elaboration: we need at least one predicate variable in parameter params.push(rty::RefinedType::unrefined(rty::Type::unit()).vacuous()); } - let value_ty = self.type_builder.build(*value_ty); - let func_ty = rty::FunctionType::new( - params, - rty::RefinedType::new(value_ty.vacuous(), formula_fn.to_refinement()), - ); + let mut value_rty = self.type_builder.build(*value_ty).vacuous(); + value_rty.refinement.push_conj(formula_fn.to_refinement()); + let func_ty = rty::FunctionType::new(params, value_rty); let args = formula_fn .param_idents() @@ -1133,7 +1131,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn add_prophecy_var(&mut self, statement_index: usize, ty: mir_ty::Ty<'tcx>) { let ty = self.type_builder.build(ty); - let temp_var = self.env.push_temp_var(ty.vacuous()); + let temp_var = self.env.push_temp_var(ty.vacuous().ty); self.prophecy_vars.insert(statement_index, temp_var); tracing::debug!(stmt_idx = %statement_index, temp_var = ?temp_var, "add_prophecy_var"); } @@ -1154,7 +1152,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { prophecy_ty: mir_ty::Ty<'tcx>, ) -> rty::RefinedType { let prophecy_ty = self.type_builder.build(prophecy_ty); - let prophecy = self.env.push_temp_var(prophecy_ty.vacuous()); + let prophecy = self.env.push_temp_var(prophecy_ty.vacuous().ty); let place = self.elaborate_place_for_borrow(&referent); self.env.borrow_place(place, prophecy).into() } diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index d29f8510..1e78e77c 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -15,6 +15,7 @@ struct DefIds { model_ty: OnceCell>, int_model: OnceCell>, + uint_model: OnceCell>, mut_model: OnceCell>, box_model: OnceCell>, array_model: OnceCell>, @@ -138,6 +139,13 @@ impl<'tcx> DefIdCache<'tcx> { .get_or_init(|| self.annotated_def(&crate::analyze::annot::int_model_path())) } + pub fn uint_model(&self) -> Option { + *self + .def_ids + .uint_model + .get_or_init(|| self.annotated_def(&crate::analyze::annot::uint_model_path())) + } + pub fn mut_model(&self) -> Option { *self .def_ids diff --git a/src/chc.rs b/src/chc.rs index ac8e3b99..fcdde7db 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1781,6 +1781,10 @@ impl Body { self.formula.is_bottom() || self.atoms.iter().any(|a| a.is_bottom()) } + pub fn has_pred_var(&self) -> bool { + self.atoms.iter().any(|a| matches!(a.pred, Pred::Var(_))) + } + pub fn push_conj(&mut self, other: impl Into>) { let Body { atoms, formula } = other.into(); self.atoms.extend(atoms); diff --git a/src/refine/basic_block.rs b/src/refine/basic_block.rs index e02e1d68..23874719 100644 --- a/src/refine/basic_block.rs +++ b/src/refine/basic_block.rs @@ -170,9 +170,10 @@ impl BasicBlockType { }; mapping.insert(idx, mapped_idx); - // to be sure + // to be sure: only the last parameter carries the predicate variable of the + // precondition; the others carry at most what their model says about them. if idx != last_param_idx { - assert!(param_ty.refinement.is_top()); + assert!(!param_ty.refinement.has_pred_var()); } } diff --git a/src/refine/env.rs b/src/refine/env.rs index 88397fa6..177377b8 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -422,7 +422,7 @@ impl PlaceType { let mut field_terms = Vec::new(); let mut field_tys = Vec::new(); for field_ty in variant.field_tys.clone() { - let mut rty = rty::RefinedType::unrefined(field_ty.vacuous()); + let mut rty = field_ty.vacuous(); rty.instantiate_ty_params(inner_ty.args.clone()); let (ty, field_ex_var) = builder.subsume_rty(rty.boxed()); @@ -766,7 +766,7 @@ where for field_ty in &variant_def.field_tys { let x = self.temp_vars.next_index(); fields.push(x); - let mut field_ty = rty::RefinedType::unrefined(field_ty.clone().vacuous()); + let mut field_ty = field_ty.clone().vacuous(); field_ty.instantiate_ty_params(ty.args.clone()); let guarded_field_ty = field_ty.guarded( chc::Term::var(discr_var.into()) @@ -977,9 +977,7 @@ where let arg_rtys = { let def = self.enum_defs.enum_def(sym); - let expected_tys = def - .field_tys() - .map(|ty| rty::RefinedType::unrefined(ty.clone().vacuous()).boxed()); + let expected_tys = def.field_tys().map(|rty| rty.clone().vacuous().boxed()); let got_tys = field_tys.iter().map(|ty| ty.clone().into()); rty::unify_tys_params(expected_tys, got_tys).into_args(def.ty_params, |_| { panic!("var_type: should unify all params") @@ -1147,7 +1145,7 @@ where let mut pred_args = vec![]; for field_ty in enum_def.field_tys() { - let mut field_rty = rty::RefinedType::unrefined(field_ty.clone().vacuous()); + let mut field_rty = field_ty.clone().vacuous(); field_rty.instantiate_ty_params(ety.args.clone()); let field_type = field_rty.ty; diff --git a/src/refine/template.rs b/src/refine/template.rs index 246688cc..80c8a885 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -60,13 +60,14 @@ where } } -/// Translates [`mir_ty::Ty`] to [`rty::Type`]. +/// Translates [`mir_ty::Ty`] to [`rty::RefinedType`]. /// /// This struct implements a translation from Rust MIR types to Thrust types. -/// Thrust types may contain refinement predicates which do not exist in MIR types, -/// and [`TypeBuilder`] solely builds types with null refinement (true) in -/// [`TypeBuilder::build`]. This also provides [`TypeBuilder::for_template`] to build -/// refinement types by filling unknown predicates with templates with predicate variables. +/// Thrust types may contain refinement predicates which do not exist in MIR types, and +/// [`TypeBuilder::build`] fills them with what the model of the type says about its values +/// (an unsigned integer is non-negative, and nothing for the other models). This also provides +/// [`TypeBuilder::for_template`] to build refinement types by filling unknown predicates with +/// templates with predicate variables. #[derive(Clone)] pub struct TypeBuilder<'tcx> { tcx: mir_ty::TyCtxt<'tcx>, @@ -174,49 +175,79 @@ impl<'tcx> TypeBuilder<'tcx> { adt: &mir_ty::AdtDef<'tcx>, args: &'tcx mir_ty::List>, ) -> Option> { - if Some(adt.did()) == self.def_ids.int_model() { + if Some(adt.did()) == self.def_ids.int_model() + || Some(adt.did()) == self.def_ids.uint_model() + { return Some(rty::Type::int()); } if Some(adt.did()) == self.def_ids.mut_model() { - let elem_ty = self.build(args.type_at(0)); + let elem_ty = self.build_ty(args.type_at(0)); return Some(rty::PointerType::mut_to(elem_ty).into()); } if Some(adt.did()) == self.def_ids.box_model() { - let elem_ty = self.build(args.type_at(0)); + let elem_ty = self.build_ty(args.type_at(0)); return Some(rty::PointerType::own(elem_ty).into()); } if Some(adt.did()) == self.def_ids.array_model() { - let idx_ty = self.build(args.type_at(0)); - let elem_ty = self.build(args.type_at(1)); + let idx_ty = self.build_ty(args.type_at(0)); + let elem_ty = self.build_ty(args.type_at(1)); return Some(rty::ArrayType::new(idx_ty, elem_ty).into()); } if Some(adt.did()) == self.def_ids.closure_model() { let tupled_upvars_ty = args.type_at(0); - return Some(self.build(tupled_upvars_ty)); + return Some(self.build_ty(tupled_upvars_ty)); } None } + /// What the model of `ty` says about every value of that type: an unsigned integer is + /// non-negative, and nothing for the other models. + /// + /// This describes the value as a whole. A refinement nested in a type (a field of a + /// tuple, an element of an array) is out of reach of the analyzer, which carries the + /// facts about the parts of a value in the formula of its [`refine::PlaceType`] instead. + fn model_refinement(&self, ty: mir_ty::Ty<'tcx>) -> rty::Refinement { + let is_unsigned = match self.resolve_model_ty(ty).kind() { + mir_ty::TyKind::Adt(def, _) => Some(def.did()) == self.def_ids.uint_model(), + _ => false, + }; + if !is_unsigned { + return rty::Refinement::top(); + } + chc::Atom::new( + chc::KnownPred::GREATER_THAN_OR_EQUAL.into(), + vec![ + chc::Term::var(rty::RefinedTypeVar::Value), + chc::Term::int(0), + ], + ) + .into() + } + + pub fn build(&self, ty: mir_ty::Ty<'tcx>) -> rty::RefinedType { + rty::RefinedType::new(self.build_ty(ty), self.model_refinement(ty)) + } + // TODO: consolidate two impls - pub fn build(&self, ty: mir_ty::Ty<'tcx>) -> rty::Type { + fn build_ty(&self, ty: mir_ty::Ty<'tcx>) -> rty::Type { let ty = self.resolve_model_ty(ty); match ty.kind() { mir_ty::TyKind::Bool => rty::Type::bool(), mir_ty::TyKind::Str => rty::Type::string(), mir_ty::TyKind::Ref(_, elem_ty, mir_ty::Mutability::Not) => { - let elem_ty = self.build(*elem_ty); + let elem_ty = self.build_ty(*elem_ty); rty::PointerType::immut_to(elem_ty).into() } mir_ty::TyKind::Tuple(ts) => { // elaboration: all fields are boxed let elems = ts .iter() - .map(|ty| rty::PointerType::own(self.build(ty)).into()) + .map(|ty| rty::PointerType::own(self.build_ty(ty)).into()) .collect(); rty::TupleType::new(elems).into() } @@ -228,9 +259,9 @@ impl<'tcx> TypeBuilder<'tcx> { let params = sig .inputs() .iter() - .map(|ty| rty::RefinedType::unrefined(self.build(*ty)).vacuous()) + .map(|ty| self.build(*ty).vacuous()) .collect(); - let ret = rty::RefinedType::unrefined(self.build(sig.output())); + let ret = self.build(sig.output()); rty::FunctionType::new(params, ret.vacuous()).into() } mir_ty::TyKind::Adt(def, params) => { @@ -239,10 +270,7 @@ impl<'tcx> TypeBuilder<'tcx> { } if def.is_enum() { let sym = refine::datatype_symbol(self.tcx, def.did()); - let args: IndexVec<_, _> = params - .types() - .map(|ty| rty::RefinedType::unrefined(self.build(ty))) - .collect(); + let args: IndexVec<_, _> = params.types().map(|ty| self.build(ty)).collect(); rty::EnumType::new(sym, args).into() } else if def.is_struct() { let elem_tys = def @@ -250,7 +278,7 @@ impl<'tcx> TypeBuilder<'tcx> { .map(|field| { let ty = field.ty(self.tcx, params); // elaboration: all fields are boxed - rty::PointerType::own(self.build(ty)).into() + rty::PointerType::own(self.build_ty(ty)).into() }) .collect(); rty::TupleType::new(elem_tys).into() @@ -327,7 +355,7 @@ impl<'tcx> TypeBuilder<'tcx> { } } -/// Translates [`mir_ty::Ty`] to [`rty::Type`] using templates for refinements. +/// Translates [`mir_ty::Ty`] to [`rty::RefinedType`] using templates for unknown refinements. /// /// [`rty::Template`] is a refinement type in the form of `{ T | P(x1, ..., xn) }` where `P` is a /// predicate variable. When constructing a template, we need to know which variables can affect the @@ -361,48 +389,54 @@ where adt: &mir_ty::AdtDef<'tcx>, args: &'tcx mir_ty::List>, ) -> Option> { - if Some(adt.did()) == self.inner.def_ids.int_model() { + if Some(adt.did()) == self.inner.def_ids.int_model() + || Some(adt.did()) == self.inner.def_ids.uint_model() + { return Some(rty::Type::int()); } if Some(adt.did()) == self.inner.def_ids.mut_model() { - let elem_ty = self.build(args.type_at(0)); + let elem_ty = self.build_ty(args.type_at(0)); return Some(rty::PointerType::mut_to(elem_ty).into()); } if Some(adt.did()) == self.inner.def_ids.box_model() { - let elem_ty = self.build(args.type_at(0)); + let elem_ty = self.build_ty(args.type_at(0)); return Some(rty::PointerType::own(elem_ty).into()); } if Some(adt.did()) == self.inner.def_ids.array_model() { - let idx_ty = self.build(args.type_at(0)); - let elem_ty = self.build(args.type_at(1)); + let idx_ty = self.build_ty(args.type_at(0)); + let elem_ty = self.build_ty(args.type_at(1)); return Some(rty::ArrayType::new(idx_ty, elem_ty).into()); } if Some(adt.did()) == self.inner.def_ids.closure_model() { let tupled_upvars_ty = args.type_at(0); - return Some(self.build(tupled_upvars_ty)); + return Some(self.build_ty(tupled_upvars_ty)); } None } - pub fn build(&mut self, ty: mir_ty::Ty<'tcx>) -> rty::Type { + pub fn build(&mut self, ty: mir_ty::Ty<'tcx>) -> rty::RefinedType { + rty::RefinedType::new(self.build_ty(ty), self.inner.model_refinement(ty)) + } + + fn build_ty(&mut self, ty: mir_ty::Ty<'tcx>) -> rty::Type { let ty = self.inner.resolve_model_ty(ty); match ty.kind() { mir_ty::TyKind::Bool => rty::Type::bool(), mir_ty::TyKind::Str => rty::Type::string(), mir_ty::TyKind::Ref(_, elem_ty, mir_ty::Mutability::Not) => { - let elem_ty = self.build(*elem_ty); + let elem_ty = self.build_ty(*elem_ty); rty::PointerType::immut_to(elem_ty).into() } mir_ty::TyKind::Tuple(ts) => { // elaboration: all fields are boxed let elems = ts .iter() - .map(|ty| rty::PointerType::own(self.build(ty)).into()) + .map(|ty| rty::PointerType::own(self.build_ty(ty)).into()) .collect(); rty::TupleType::new(elems).into() } @@ -429,7 +463,7 @@ where .map(|field| { let ty = field.ty(self.inner.tcx, params); // elaboration: all fields are boxed - rty::PointerType::own(self.build(ty)).into() + rty::PointerType::own(self.build_ty(ty)).into() }) .collect(); rty::TupleType::new(elem_tys).into() @@ -441,11 +475,15 @@ where } } + /// Builds a refinement type whose refinement is an unknown predicate, conjoined with + /// what the model of `ty` already tells us about its values. pub fn build_refined(&mut self, ty: mir_ty::Ty<'tcx>) -> rty::RefinedType { // TODO: consider building ty with scope - let ty = self.inner.for_template(self.registry).build(ty).vacuous(); - let tmpl = self.scope.build_template().build(ty); - self.registry.register_template(tmpl) + let known = self.inner.for_template(self.registry).build(ty).vacuous(); + let tmpl = self.scope.build_template().build(known.ty); + let mut rty = self.registry.register_template(tmpl); + rty.refinement.push_conj(known.refinement); + rty } fn build_basic_block_with_precondition( @@ -481,9 +519,7 @@ where param_rtys: Default::default(), param_refinement: precondition, // not generating pvar of BB post - ret_rty: Some(rty::RefinedType::unrefined( - self.inner.build(ret_ty).vacuous(), - )), + ret_rty: Some(self.inner.build(ret_ty).vacuous()), abi: Default::default(), } .build(); @@ -547,8 +583,9 @@ impl<'tcx, 'a, R> FunctionTemplateTypeBuilder<'tcx, 'a, R> { &mut self, refinement: rty::Refinement, ) -> &mut Self { - let ty = self.inner.build(self.ret_ty); - self.ret_rty = Some(rty::RefinedType::new(ty.vacuous(), refinement)); + let mut rty = self.inner.build(self.ret_ty).vacuous(); + rty.refinement.push_conj(refinement); + self.ret_rty = Some(rty); self } @@ -569,9 +606,8 @@ impl<'tcx, 'a, R> FunctionTemplateTypeBuilder<'tcx, 'a, R> { match first { rty::TypePositionStep::Param(idx) => { if !self.param_rtys.contains_key(idx) { - let ty = self.inner.build(self.param_tys[idx.index()].ty).vacuous(); - self.param_rtys - .insert(*idx, rty::RefinedType::unrefined(ty)); + let rty = self.inner.build(self.param_tys[idx.index()].ty).vacuous(); + self.param_rtys.insert(*idx, rty); } self.param_rtys .get_mut(idx) @@ -580,8 +616,7 @@ impl<'tcx, 'a, R> FunctionTemplateTypeBuilder<'tcx, 'a, R> { } rty::TypePositionStep::Return => { if self.ret_rty.is_none() { - let ty = self.inner.build(self.ret_ty).vacuous(); - self.ret_rty = Some(rty::RefinedType::unrefined(ty)); + self.ret_rty = Some(self.inner.build(self.ret_ty).vacuous()); } self.ret_rty .as_mut() @@ -611,8 +646,9 @@ where .unwrap_or_else(|| { if idx == self.param_tys.len() - 1 { if let Some(param_refinement) = &self.param_refinement { - let ty = self.inner.build(param_ty.ty); - rty::RefinedType::new(ty.vacuous(), param_refinement.clone()) + let mut rty = self.inner.build(param_ty.ty).vacuous(); + rty.refinement.push_conj(param_refinement.clone()); + rty } else { self.inner .for_template(self.registry) @@ -620,14 +656,12 @@ where .build_refined(param_ty.ty) } } else if self.param_refinement.is_some() { - rty::RefinedType::unrefined(self.inner.build(param_ty.ty).vacuous()) + self.inner.build(param_ty.ty).vacuous() } else { - rty::RefinedType::unrefined( - self.inner - .for_template(self.registry) - .build(param_ty.ty) - .vacuous(), - ) + self.inner + .for_template(self.registry) + .build(param_ty.ty) + .vacuous() } }); let param_rty = if param_ty.mutbl.is_mut() { diff --git a/src/rty.rs b/src/rty.rs index cea3583d..0a7e89c3 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -691,7 +691,7 @@ impl TupleType { pub struct EnumVariantDef { pub name: chc::DatatypeSymbol, pub discr: u32, - pub field_tys: Vec>, + pub field_tys: Vec>, } /// A definition of an enum datatype. @@ -703,7 +703,7 @@ pub struct EnumDatatypeDef { } impl EnumDatatypeDef { - pub fn field_tys(&self) -> impl Iterator> { + pub fn field_tys(&self) -> impl Iterator> { self.variants.iter().flat_map(|v| &v.field_tys) } } @@ -1469,6 +1469,10 @@ impl Formula { self.body.is_bottom() } + pub fn has_pred_var(&self) -> bool { + self.body.has_pred_var() + } + pub fn top() -> Self { Formula::new(IndexVec::new(), chc::Body::top()) } @@ -1653,7 +1657,7 @@ where impl RefinedType { /// Installs `refinement` at the sub-type addressed by `steps`. /// - /// An empty `steps` slice replaces the refinement at this node; otherwise + /// An empty `steps` slice conjoins the refinement to the one at this node; otherwise /// each step navigates one level deeper per [`TypePositionStep`]. pub fn install_refinement_at( &mut self, @@ -1661,7 +1665,7 @@ impl RefinedType { refinement: Refinement, ) { let Some((step, rest)) = steps.split_first() else { - self.refinement = refinement; + self.refinement.push_conj(refinement); return; }; match step { @@ -1715,6 +1719,10 @@ impl RefinedType { RefinedType { ty, refinement } } + pub fn to_sort(&self) -> chc::Sort { + self.ty.to_sort() + } + pub fn refined_with_term(ty: Type, term: chc::Term) -> Self { let term = term.map_var(RefinedTypeVar::Free); let refinement = chc::Term::var(RefinedTypeVar::Value).equal_to(term); diff --git a/std.rs b/std.rs index 96d88669..f23c00e8 100644 --- a/std.rs +++ b/std.rs @@ -9,58 +9,84 @@ mod thrust_models { pub mod model { use std::marker::PhantomData; - #[thrust::def::int_model] - pub struct Int; + /// Models denoting a mathematical integer. + /// + /// Arithmetic and comparison mix these freely: the model of an unsigned integer + /// denotes the same mathematical integers as [`Int`], only non-negative ones. + pub trait Integer {} + + impl Integer for Int {} + impl Integer for UInt {} + + /// Models usable as an index into `Array`. + pub trait IndexModel {} + + impl IndexModel for I {} + impl IndexModel for UInt {} + impl IndexModel for Int {} + + macro_rules! integer_model_ops { + ($M:ty) => { + impl PartialEq for $M where T: super::Model, T::Ty: Integer { + #[thrust::ignored] + fn eq(&self, _other: &T) -> bool { + unimplemented!() + } + } - impl PartialEq for Int where T: super::Model { - #[thrust::ignored] - fn eq(&self, _other: &T) -> bool { - unimplemented!() - } - } + impl PartialOrd for $M where T: super::Model, T::Ty: Integer { + #[thrust::ignored] + fn partial_cmp(&self, _other: &T) -> Option { + unimplemented!() + } + } - impl PartialOrd for Int where T: super::Model { - #[thrust::ignored] - fn partial_cmp(&self, _other: &T) -> Option { - unimplemented!() - } - } + impl std::ops::Add for $M where T: super::Model, T::Ty: Integer { + type Output = Self; - impl std::ops::Add for Int where T: super::Model { - type Output = Self; + #[thrust::ignored] + fn add(self, _rhs: T) -> Self::Output { + unimplemented!() + } + } - #[thrust::ignored] - fn add(self, _rhs: T) -> Self::Output { - unimplemented!() - } - } + impl std::ops::Sub for $M where T: super::Model, T::Ty: Integer { + type Output = Self; - impl std::ops::Sub for Int where T: super::Model { - type Output = Self; + #[thrust::ignored] + fn sub(self, _rhs: T) -> Self::Output { + unimplemented!() + } + } - #[thrust::ignored] - fn sub(self, _rhs: T) -> Self::Output { - unimplemented!() - } - } + impl std::ops::Mul for $M where T: super::Model, T::Ty: Integer { + type Output = Self; - impl std::ops::Mul for Int where T: super::Model { - type Output = Self; + #[thrust::ignored] + fn mul(self, _rhs: T) -> Self::Output { + unimplemented!() + } + } - #[thrust::ignored] - fn mul(self, _rhs: T) -> Self::Output { - unimplemented!() - } + impl std::ops::Neg for $M { + type Output = Int; + + #[thrust::ignored] + fn neg(self) -> Self::Output { + unimplemented!() + } + } + }; } - impl std::ops::Neg for Int { - type Output = Self; + #[thrust::def::int_model] + pub struct Int; - #[thrust::ignored] - fn neg(self) -> Self::Output { - unimplemented!() - } - } + #[thrust::def::uint_model] + pub struct UInt; + + integer_model_ops!(Int); + integer_model_ops!(UInt); #[thrust::def::mut_model] pub struct Mut(PhantomData); @@ -137,7 +163,7 @@ mod thrust_models { } } - impl std::ops::Index for Array where U: super::Model { + impl std::ops::Index for Array where U: super::Model, U::Ty: IndexModel { type Output = T; #[thrust::ignored] @@ -150,7 +176,9 @@ mod thrust_models { #[allow(dead_code)] #[thrust::def::array_store] #[thrust::ignored] - pub fn store(&self, _index: U, _value: T) -> Self where U: super::Model { + pub fn store(&self, _index: U, _value: T) -> Self + where U: super::Model, U::Ty: IndexModel + { unimplemented!() } } @@ -189,8 +217,8 @@ mod thrust_models { #[thrust::def::seq_model] pub struct Seq { - pub array: Array, - pub length: Int, + pub array: Array, + pub length: UInt, } impl PartialEq for Seq where U: super::Model { @@ -200,7 +228,7 @@ mod thrust_models { } } - impl std::ops::Index for Seq where U: super::Model { + impl std::ops::Index for Seq where U: super::Model, U::Ty: Integer { type Output = T; #[thrust::ignored] @@ -227,7 +255,7 @@ mod thrust_models { #[allow(dead_code)] #[thrust::def::seq_len] #[thrust::ignored] - pub fn len(&self) -> Int { + pub fn len(&self) -> UInt { unimplemented!() } @@ -255,61 +283,72 @@ mod thrust_models { type Ty = model::Int; } - macro_rules! int_model { - ($T:ty) => { - impl Model for $T { - type Ty = model::Int; - } + impl Model for model::UInt { + type Ty = model::UInt; + } - impl PartialEq for $T { + macro_rules! model_arith { + ($T:ty, $M:ty) => { + impl PartialEq<$M> for $T { #[thrust::ignored] - fn eq(&self, _other: &model::Int) -> bool { + fn eq(&self, _other: &$M) -> bool { unimplemented!() } } - impl PartialOrd for $T { + impl PartialOrd<$M> for $T { #[thrust::ignored] - fn partial_cmp(&self, _other: &model::Int) -> Option { + fn partial_cmp(&self, _other: &$M) -> Option { unimplemented!() } } - impl std::ops::Add for $T { - type Output = model::Int; + impl std::ops::Add<$M> for $T { + type Output = $M; #[thrust::ignored] - fn add(self, _rhs: model::Int) -> Self::Output { + fn add(self, _rhs: $M) -> Self::Output { unimplemented!() } } - impl std::ops::Sub for $T { - type Output = model::Int; + impl std::ops::Sub<$M> for $T { + type Output = $M; #[thrust::ignored] - fn sub(self, _rhs: model::Int) -> Self::Output { + fn sub(self, _rhs: $M) -> Self::Output { unimplemented!() } } - impl std::ops::Mul for $T { - type Output = model::Int; + impl std::ops::Mul<$M> for $T { + type Output = $M; #[thrust::ignored] - fn mul(self, _rhs: model::Int) -> Self::Output { + fn mul(self, _rhs: $M) -> Self::Output { unimplemented!() } } }; } - int_model!(isize); - int_model!(i32); - int_model!(i64); - int_model!(usize); - int_model!(u32); - int_model!(u64); + macro_rules! integer_model { + ($T:ty, $M:ty) => { + impl Model for $T { + type Ty = $M; + } + + model_arith!($T, model::Int); + model_arith!($T, model::UInt); + }; + } + + integer_model!(isize, model::Int); + integer_model!(i32, model::Int); + integer_model!(i64, model::Int); + integer_model!(usize, model::UInt); + integer_model!(u32, model::UInt); + integer_model!(u64, model::UInt); impl Model for bool { type Ty = bool; diff --git a/tests/ui/fail/ghost_const.rs b/tests/ui/fail/ghost_const.rs index 2cc9cf57..c39fb58e 100644 --- a/tests/ui/fail/ghost_const.rs +++ b/tests/ui/fail/ghost_const.rs @@ -1,15 +1,15 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -use thrust_models::model::{Int, Seq}; +use thrust_models::model::{Seq, UInt}; use thrust_models::Ghost; #[thrust_macros::requires(s.len() == 0)] -fn expect_empty(s: Ghost>) { +fn expect_empty(s: Ghost>) { let _ = s; } fn main() { - let s = thrust_macros::ghost!(|| -> Seq { Seq::singleton(Seq::::empty().len()) }); + let s = thrust_macros::ghost!(|| -> Seq { Seq::singleton(Seq::::empty().len()) }); expect_empty(s); } diff --git a/tests/ui/fail/unsigned_loop.rs b/tests/ui/fail/unsigned_loop.rs new file mode 100644 index 00000000..208b9b63 --- /dev/null +++ b/tests/ui/fail/unsigned_loop.rs @@ -0,0 +1,12 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +#[thrust_macros::ensures(result == 0)] +fn count_down(mut n: u32) -> u32 { + while n > 1 { + n -= 1; + } + n +} + +fn main() {} diff --git a/tests/ui/fail/unsigned_sub.rs b/tests/ui/fail/unsigned_sub.rs new file mode 100644 index 00000000..1aea6543 --- /dev/null +++ b/tests/ui/fail/unsigned_sub.rs @@ -0,0 +1,9 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +#[thrust_macros::ensures(result == x - y)] +fn diff(x: u32, y: u32) -> u32 { + x - y +} + +fn main() {} diff --git a/tests/ui/pass/ghost_const.rs b/tests/ui/pass/ghost_const.rs index 6e2158ef..f725c3db 100644 --- a/tests/ui/pass/ghost_const.rs +++ b/tests/ui/pass/ghost_const.rs @@ -1,15 +1,15 @@ //@check-pass //@compile-flags: -C debug-assertions=off -use thrust_models::model::{Int, Seq}; +use thrust_models::model::{Seq, UInt}; use thrust_models::Ghost; #[thrust_macros::requires(s.len() == 0)] -fn expect_empty(s: Ghost>) { +fn expect_empty(s: Ghost>) { let _ = s; } fn main() { - let s = thrust_macros::ghost!(|| -> Seq { Seq::empty() }); + let s = thrust_macros::ghost!(|| -> Seq { Seq::empty() }); expect_empty(s); } diff --git a/tests/ui/pass/unsigned_loop.rs b/tests/ui/pass/unsigned_loop.rs new file mode 100644 index 00000000..a7d9a628 --- /dev/null +++ b/tests/ui/pass/unsigned_loop.rs @@ -0,0 +1,12 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +#[thrust_macros::ensures(result == 0)] +fn count_down(mut n: u32) -> u32 { + while n > 0 { + n -= 1; + } + n +} + +fn main() {} diff --git a/tests/ui/pass/unsigned_sub.rs b/tests/ui/pass/unsigned_sub.rs new file mode 100644 index 00000000..eb17433b --- /dev/null +++ b/tests/ui/pass/unsigned_sub.rs @@ -0,0 +1,10 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +#[thrust_macros::requires(x >= y)] +#[thrust_macros::ensures(result == x - y)] +fn diff(x: u32, y: u32) -> u32 { + x - y +} + +fn main() {}