From 9a6e5f117ca01c90deece68a29f7b28d428865da Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 21 Nov 2025 17:10:24 +0100 Subject: [PATCH 01/26] Add support for type aliases with associated types --- .../src/encoders/ty/generics/args.rs | 58 +++++++++++++-- .../src/encoders/ty/generics/args_ty.rs | 40 ++++++++++- .../src/encoders/ty/generics/params.rs | 72 ++++++++++++++++++- prusti-encoder/src/lib.rs | 3 +- prusti-tests/tests/verify/pass/type_alias.rs | 23 ++++++ 5 files changed, 184 insertions(+), 12 deletions(-) create mode 100644 prusti-tests/tests/verify/pass/type_alias.rs diff --git a/prusti-encoder/src/encoders/ty/generics/args.rs b/prusti-encoder/src/encoders/ty/generics/args.rs index 5bf0cd8205c..dfb02bab929 100644 --- a/prusti-encoder/src/encoders/ty/generics/args.rs +++ b/prusti-encoder/src/encoders/ty/generics/args.rs @@ -1,4 +1,10 @@ -use prusti_rustc_interface::middle::ty; +use crate::{ + DefId, + encoders::ty::{RustTyDecomposition, pure::TyPureEnc}, +}; +use prusti_rustc_interface::middle::{ty, ty::TyCtxt}; +use task_encoder::TaskEncoder; +use vir::{CastType, FunctionGenData, FunctionIdn, LocalDeclData, TyVal, ViperIdent, VirCtxt}; use super::GParams; @@ -10,6 +16,15 @@ pub struct GArgs<'tcx> { pub(super) args: &'tcx [ty::GenericArg<'tcx>], } +pub enum GParamVariant<'vir> { + Param(ty::ParamTy), + Alias( + &'vir str, + &'vir str, + Vec<(ty::Ty<'vir>, ty::Ty<'vir>, &'vir str)>, + ), +} + impl<'tcx> GArgs<'tcx> { pub fn new(context: impl Into>, args: &'tcx [ty::GenericArg<'tcx>]) -> Self { GArgs { @@ -34,12 +49,45 @@ impl<'tcx> GArgs<'tcx> { self.context.normalize(ty) } - pub fn expect_param(self) -> ty::ParamTy { + pub fn expect_param<'vir>(self) -> GParamVariant<'vir> { assert_eq!(self.args.len(), 1); match self.args[0].expect_ty().kind() { - ty::TyKind::Param(p) => *p, - // TODO: this needs to be changed to support type aliases - ty::TyKind::Alias(..) => panic!("type aliases are not currently supported"), + ty::TyKind::Param(p) => GParamVariant::Param(*p), + ty::TyKind::Alias(k, t) => { + vir::with_vcx(|vcx| { + let tcx = vcx.tcx(); + let trait_name = vcx.alloc_str( + tcx.item_name(tcx.associated_item(t.def_id).container_id(tcx)) + .as_str(), + ); + let type_name = vcx.alloc_str(tcx.item_name(t.def_id).as_str()); + let assoc_type_substs = tcx + .all_impls(tcx.associated_item(t.def_id).container_id(tcx)) + .map(|imp| { + let imp_type = tcx.type_of(imp).instantiate_identity(); + let assoc_types = tcx + .associated_items(imp) + .filter_by_name_unhygienic_and_kind( + tcx.item_name(t.def_id), + ty::AssocTag::Type, + ) + .collect::>(); + assert!(assoc_types.len() == 1); + let assoc_type = + tcx.type_of(assoc_types[0].def_id).instantiate_identity(); + let st_name = vcx.alloc_str( + match tcx.type_of(imp).instantiate_identity().kind() { + ty::Adt(adt_def, _) => tcx.item_name(adt_def.did()), + _ => unreachable!(), + } + .as_str(), + ); + (imp_type, assoc_type, st_name) + }) + .collect::>(); + GParamVariant::Alias(&trait_name, &type_name, assoc_type_substs) + }) + } other => panic!("expected type parameter, {other:?}"), } } diff --git a/prusti-encoder/src/encoders/ty/generics/args_ty.rs b/prusti-encoder/src/encoders/ty/generics/args_ty.rs index dc7a5ecd55b..e5afe876a65 100644 --- a/prusti-encoder/src/encoders/ty/generics/args_ty.rs +++ b/prusti-encoder/src/encoders/ty/generics/args_ty.rs @@ -1,7 +1,12 @@ use prusti_rustc_interface::middle::ty; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; +use vir::ViperIdent; -use crate::encoders::{ConstEnc, r#const::ConstEncTask, ty::RustTyDecomposition}; +use crate::encoders::{ + ConstEnc, + r#const::ConstEncTask, + ty::{RustTyDecomposition, generics::params}, +}; use super::{GArgs, GenericParamsEnc}; @@ -32,17 +37,31 @@ impl TaskEncoder for GArgsTyEnc { task_encoder::encoder_cache!(GArgsTyEnc); type TaskDescription<'tcx> = GArgs<'tcx>; type OutputFullDependency<'vir> = GArgsTy<'vir>; + type OutputFullLocal<'vir> = Option>; fn task_to_key<'vir>(task: &Self::TaskDescription<'vir>) -> Self::TaskKey<'vir> { *task } + fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { + for output in GArgsTyEnc::all_outputs_local_no_errors() { + if let Some(dom) = output { + program.add_domain(dom); + } + } + } + fn do_encode_full<'vir>( task_key: &Self::TaskKey<'vir>, deps: &mut TaskEncoderDependencies<'vir, Self>, ) -> EncodeFullResult<'vir, Self> { deps.emit_output_ref(*task_key, ())?; let params = deps.require_dep::(task_key.context)?; + let mut builder = params::Builder { + functions: Vec::new(), + axioms: Vec::new(), + domain_name: "", + }; let ty_args = task_key .args .iter() @@ -52,7 +71,7 @@ impl TaskEncoder for GArgsTyEnc { let decomp = vir::with_vcx(|vcx| { RustTyDecomposition::from_ty(arg, vcx.tcx(), task_key.context) }); - params.ty_expr(deps, decomp) + params.ty_expr(deps, decomp, &mut builder) }) .collect::>(); let const_args = task_key @@ -81,6 +100,21 @@ impl TaskEncoder for GArgsTyEnc { ty_args: vcx.alloc_slice(&ty_args), const_args: vcx.alloc_slice(&const_args), }); - Ok(((), args)) + if builder.functions.len() > 0 { + vir::with_vcx(|vcx| { + Ok(( + Some(vcx.mk_domain( + ViperIdent::new(builder.domain_name), + &[], + vcx.alloc_slice(&builder.axioms), + vcx.alloc_slice(&builder.functions), + None, + )), + args, + )) + }) + } else { + Ok((None, args)) + } } } diff --git a/prusti-encoder/src/encoders/ty/generics/params.rs b/prusti-encoder/src/encoders/ty/generics/params.rs index 0220487fada..ba115647b0a 100644 --- a/prusti-encoder/src/encoders/ty/generics/params.rs +++ b/prusti-encoder/src/encoders/ty/generics/params.rs @@ -4,11 +4,16 @@ use prusti_rustc_interface::{ span::{def_id::DefId, symbol}, }; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{CastType, HasType}; +use vir::{CastType, DomainAxiomData, FunctionIdn, HasType, ViperIdent}; use crate::encoders::{ TyUsePureEnc, - ty::{RustTyDecomposition, data::TySpecifics, generics::GArgsTyEnc, lifted::TyConstructorEnc}, + ty::{ + RustTyDecomposition, + data::TySpecifics, + generics::{GArgsTyEnc, GParamVariant}, + lifted::TyConstructorEnc, + }, }; /// The list of defined parameters in a given context. E.g. the type parameters @@ -177,6 +182,12 @@ impl<'vir> From for GParams<'vir> { /// (handles the type parameters). pub struct GenericParamsEnc; +pub struct Builder<'vir> { + pub axioms: Vec>, + pub functions: Vec>, + pub domain_name: &'vir str, +} + #[derive(Debug, Clone)] pub struct GenericParams<'vir> { ty_args: &'vir [vir::TypeTyVal<'vir>], @@ -247,10 +258,65 @@ impl<'vir> GenericParams<'vir> { &self, deps: &mut TaskEncoderDependencies<'vir, E>, ty: RustTyDecomposition<'vir>, + builder: &mut Builder<'vir>, ) -> vir::ExprTyVal<'vir> { if let TySpecifics::Param(()) = &ty.ty.specifics { let param = ty.args.expect_param(); - return self.ty_exprs[self.map_idx(param.index).unwrap()]; + return match param { + GParamVariant::Param(p) => self.ty_exprs[self.map_idx(p.index).unwrap()], + GParamVariant::Alias(trait_name, type_name, assoc_type_substs) => { + vir::with_vcx(|vcx| { + let idn: FunctionIdn<'_, vir::TyVal, vir::TyVal> = FunctionIdn::new( + ViperIdent::new( + vcx.alloc_str(&format!("{}_Assoc_{}_func", trait_name, type_name)), + ), + vir::TYPE_TYVAL, + vir::TYPE_TYVAL, + ); + let assoc_type_func = vcx.mk_domain_function(idn, false, None); + builder.functions.push(assoc_type_func); + let mut axioms = assoc_type_substs + .iter() + .map(|(impl_type, assoc_type, impl_name)| { + let impl_type_expr = self.ty_expr( + deps, + RustTyDecomposition::from_ty( + *impl_type, + vcx.tcx(), + ty.args.context, + ), + builder, + ); + let assoc_type_expr = self.ty_expr( + deps, + RustTyDecomposition::from_ty( + *assoc_type, + vcx.tcx(), + ty.args.context, + ), + builder, + ); + vcx.alloc(DomainAxiomData { + name: vcx.alloc_str(&format!( + "{}_Assoc_{}_{}", + trait_name, type_name, impl_name + )), + expr: vir::expr! {([idn](impl_type_expr)) == (assoc_type_expr)}, + }) + }) + .collect::>(); + builder.axioms.append(&mut axioms); + builder.domain_name = + vcx.alloc_str(&format!("{}_Assoc_{}", trait_name, type_name)); + match ty.ty.data.params.params[0].expect_ty().kind() { + ty::TyKind::Param(p) => { + (idn)(self.ty_exprs[self.map_idx(p.index).unwrap()]) + } + _ => unreachable!(), + } + }) + } + }; } let ty_constructor = deps .require_ref::(ty.ty) diff --git a/prusti-encoder/src/lib.rs b/prusti-encoder/src/lib.rs index 014c6113637..067428d2722 100644 --- a/prusti-encoder/src/lib.rs +++ b/prusti-encoder/src/lib.rs @@ -21,7 +21,7 @@ use crate::encoders::{ Impure, Pure, custom::PairUseEnc, ty::{ - generics::GArgsCastEnc, + generics::{GArgsCastEnc, GArgsTyEnc}, interpretation::bitvec::BitVecEnc, lifted::{TyConstructorEnc, TypeOfEnc}, }, @@ -103,6 +103,7 @@ pub fn test_entrypoint<'tcx>( program.header("custom"); PairUseEnc::emit_outputs(&mut program); + GArgsTyEnc::emit_outputs(&mut program); if std::env::var("LOCAL_TESTING").is_ok() { std::fs::write("local-testing/simple.vpr", program.code()).unwrap(); diff --git a/prusti-tests/tests/verify/pass/type_alias.rs b/prusti-tests/tests/verify/pass/type_alias.rs new file mode 100644 index 00000000000..0f8501ebf58 --- /dev/null +++ b/prusti-tests/tests/verify/pass/type_alias.rs @@ -0,0 +1,23 @@ + +fn foo (x: Y::SomeType) { + +} + +trait MyTrait { + type SomeType; +} + +struct St1{} +struct St2{} + +impl MyTrait for St1 { + type SomeType = u32; +} + +impl MyTrait for St2 { + type SomeType = u64; +} + +fn bar() { + foo::(5); +} From 2b776293b210179043da7ccc31a2719fe56ef84b Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 21 Nov 2025 17:13:20 +0100 Subject: [PATCH 02/26] Run clippy --- .../src/encoders/ty/generics/args.rs | 73 ++++++++----------- .../src/encoders/ty/generics/args_ty.rs | 11 +-- 2 files changed, 38 insertions(+), 46 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/args.rs b/prusti-encoder/src/encoders/ty/generics/args.rs index dfb02bab929..e484472037e 100644 --- a/prusti-encoder/src/encoders/ty/generics/args.rs +++ b/prusti-encoder/src/encoders/ty/generics/args.rs @@ -1,10 +1,4 @@ -use crate::{ - DefId, - encoders::ty::{RustTyDecomposition, pure::TyPureEnc}, -}; -use prusti_rustc_interface::middle::{ty, ty::TyCtxt}; -use task_encoder::TaskEncoder; -use vir::{CastType, FunctionGenData, FunctionIdn, LocalDeclData, TyVal, ViperIdent, VirCtxt}; +use prusti_rustc_interface::middle::ty; use super::GParams; @@ -53,41 +47,38 @@ impl<'tcx> GArgs<'tcx> { assert_eq!(self.args.len(), 1); match self.args[0].expect_ty().kind() { ty::TyKind::Param(p) => GParamVariant::Param(*p), - ty::TyKind::Alias(k, t) => { - vir::with_vcx(|vcx| { - let tcx = vcx.tcx(); - let trait_name = vcx.alloc_str( - tcx.item_name(tcx.associated_item(t.def_id).container_id(tcx)) + ty::TyKind::Alias(k, t) => vir::with_vcx(|vcx| { + let tcx = vcx.tcx(); + let trait_name = vcx.alloc_str( + tcx.item_name(tcx.associated_item(t.def_id).container_id(tcx)) + .as_str(), + ); + let type_name = vcx.alloc_str(tcx.item_name(t.def_id).as_str()); + let assoc_type_substs = tcx + .all_impls(tcx.associated_item(t.def_id).container_id(tcx)) + .map(|imp| { + let imp_type = tcx.type_of(imp).instantiate_identity(); + let assoc_types = tcx + .associated_items(imp) + .filter_by_name_unhygienic_and_kind( + tcx.item_name(t.def_id), + ty::AssocTag::Type, + ) + .collect::>(); + assert!(assoc_types.len() == 1); + let assoc_type = tcx.type_of(assoc_types[0].def_id).instantiate_identity(); + let st_name = vcx.alloc_str( + match tcx.type_of(imp).instantiate_identity().kind() { + ty::Adt(adt_def, _) => tcx.item_name(adt_def.did()), + _ => unreachable!(), + } .as_str(), - ); - let type_name = vcx.alloc_str(tcx.item_name(t.def_id).as_str()); - let assoc_type_substs = tcx - .all_impls(tcx.associated_item(t.def_id).container_id(tcx)) - .map(|imp| { - let imp_type = tcx.type_of(imp).instantiate_identity(); - let assoc_types = tcx - .associated_items(imp) - .filter_by_name_unhygienic_and_kind( - tcx.item_name(t.def_id), - ty::AssocTag::Type, - ) - .collect::>(); - assert!(assoc_types.len() == 1); - let assoc_type = - tcx.type_of(assoc_types[0].def_id).instantiate_identity(); - let st_name = vcx.alloc_str( - match tcx.type_of(imp).instantiate_identity().kind() { - ty::Adt(adt_def, _) => tcx.item_name(adt_def.did()), - _ => unreachable!(), - } - .as_str(), - ); - (imp_type, assoc_type, st_name) - }) - .collect::>(); - GParamVariant::Alias(&trait_name, &type_name, assoc_type_substs) - }) - } + ); + (imp_type, assoc_type, st_name) + }) + .collect::>(); + GParamVariant::Alias(trait_name, type_name, assoc_type_substs) + }), other => panic!("expected type parameter, {other:?}"), } } diff --git a/prusti-encoder/src/encoders/ty/generics/args_ty.rs b/prusti-encoder/src/encoders/ty/generics/args_ty.rs index e5afe876a65..8c3220c4c8c 100644 --- a/prusti-encoder/src/encoders/ty/generics/args_ty.rs +++ b/prusti-encoder/src/encoders/ty/generics/args_ty.rs @@ -44,10 +44,11 @@ impl TaskEncoder for GArgsTyEnc { } fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { - for output in GArgsTyEnc::all_outputs_local_no_errors() { - if let Some(dom) = output { - program.add_domain(dom); - } + for dom in GArgsTyEnc::all_outputs_local_no_errors() + .into_iter() + .flatten() + { + program.add_domain(dom); } } @@ -100,7 +101,7 @@ impl TaskEncoder for GArgsTyEnc { ty_args: vcx.alloc_slice(&ty_args), const_args: vcx.alloc_slice(&const_args), }); - if builder.functions.len() > 0 { + if !builder.functions.is_empty() { vir::with_vcx(|vcx| { Ok(( Some(vcx.mk_domain( From cfc09fd7b96a3d3a733d9bcc513396673dac0987 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 21 Nov 2025 17:19:56 +0100 Subject: [PATCH 03/26] Solve clippy issue --- prusti-encoder/src/encoders/ty/generics/args.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prusti-encoder/src/encoders/ty/generics/args.rs b/prusti-encoder/src/encoders/ty/generics/args.rs index e484472037e..49afaf82c25 100644 --- a/prusti-encoder/src/encoders/ty/generics/args.rs +++ b/prusti-encoder/src/encoders/ty/generics/args.rs @@ -47,7 +47,7 @@ impl<'tcx> GArgs<'tcx> { assert_eq!(self.args.len(), 1); match self.args[0].expect_ty().kind() { ty::TyKind::Param(p) => GParamVariant::Param(*p), - ty::TyKind::Alias(k, t) => vir::with_vcx(|vcx| { + ty::TyKind::Alias(_k, t) => vir::with_vcx(|vcx| { let tcx = vcx.tcx(); let trait_name = vcx.alloc_str( tcx.item_name(tcx.associated_item(t.def_id).container_id(tcx)) From f1aee2a22c0149ffbbda95810625d19b0dab7cc9 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Mon, 24 Nov 2025 11:11:32 +0100 Subject: [PATCH 04/26] Fix issue with associated types for primitive implementations --- prusti-encoder/src/encoders/ty/generics/args.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/args.rs b/prusti-encoder/src/encoders/ty/generics/args.rs index 49afaf82c25..ed87d48fc04 100644 --- a/prusti-encoder/src/encoders/ty/generics/args.rs +++ b/prusti-encoder/src/encoders/ty/generics/args.rs @@ -68,11 +68,7 @@ impl<'tcx> GArgs<'tcx> { assert!(assoc_types.len() == 1); let assoc_type = tcx.type_of(assoc_types[0].def_id).instantiate_identity(); let st_name = vcx.alloc_str( - match tcx.type_of(imp).instantiate_identity().kind() { - ty::Adt(adt_def, _) => tcx.item_name(adt_def.did()), - _ => unreachable!(), - } - .as_str(), + tcx.type_of(imp).instantiate_identity().to_string().as_str(), ); (imp_type, assoc_type, st_name) }) From f5c131e0cd16b0e5b3b2b7b68b3938e5924f6da6 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Tue, 25 Nov 2025 15:55:18 +0100 Subject: [PATCH 05/26] Move generation of trait/impl into its own encoder --- prusti-encoder/src/encoders/ty/data.rs | 30 ++++-- .../src/encoders/ty/generics/args.rs | 44 ++------- .../src/encoders/ty/generics/args_ty.rs | 34 +------ .../src/encoders/ty/generics/mod.rs | 2 + .../src/encoders/ty/generics/params.rs | 81 ++++----------- .../src/encoders/ty/generics/trait_impls.rs | 99 +++++++++++++++++++ .../src/encoders/ty/generics/traits.rs | 66 +++++++++++++ .../src/encoders/ty/kinds/enumlike.rs | 10 ++ .../src/encoders/ty/kinds/structlike.rs | 33 ++++++- prusti-encoder/src/encoders/ty/rust_ty.rs | 20 ++-- prusti-encoder/src/encoders/ty/use_impure.rs | 6 +- prusti-encoder/src/encoders/ty/use_pure.rs | 6 +- prusti-encoder/src/lib.rs | 5 +- 13 files changed, 282 insertions(+), 154 deletions(-) create mode 100644 prusti-encoder/src/encoders/ty/generics/trait_impls.rs create mode 100644 prusti-encoder/src/encoders/ty/generics/traits.rs diff --git a/prusti-encoder/src/encoders/ty/data.rs b/prusti-encoder/src/encoders/ty/data.rs index 7448521ac5c..92400819cfe 100644 --- a/prusti-encoder/src/encoders/ty/data.rs +++ b/prusti-encoder/src/encoders/ty/data.rs @@ -6,6 +6,8 @@ use std::{ use prusti_rustc_interface::abi; +use prusti_rustc_interface::span::def_id::DefId; + pub trait TyDatas<'vir>: Debug + Clone + Copy { type TyData: Debug + Clone + 'vir = (); @@ -46,12 +48,14 @@ pub struct StructData<'vir, D: TyDatas<'vir>> { pub data: D::StructData, pub inhabited: bool, pub fields: Vec, + pub did: Option, } pub struct EnumData<'vir, D: TyDatas<'vir>> { pub data: D::EnumData, pub inhabited: bool, pub variants: Vec>, + pub did: Option, } pub struct VariantData<'vir, D: TyDatas<'vir>> { @@ -99,16 +103,22 @@ impl<'vir, D: TyDatas<'vir>> TySpecifics<'vir, D> { Self::MutRef(data) } - pub fn mk_structlike(data: D::StructData, inhabited: bool, fields: Vec) -> Self { - Self::StructLike(StructData::new(data, inhabited, fields)) + pub fn mk_structlike( + data: D::StructData, + inhabited: bool, + fields: Vec, + did: Option, + ) -> Self { + Self::StructLike(StructData::new(data, inhabited, fields, did)) } pub fn mk_enumlike( data: D::EnumData, inhabited: bool, variants: Vec>, + did: Option, ) -> Self { - Self::EnumLike(EnumData::new(data, inhabited, variants)) + Self::EnumLike(EnumData::new(data, inhabited, variants, did)) } pub fn is_param(&self) -> bool { @@ -253,6 +263,7 @@ impl<'vir, D: TyDatas<'vir>> StructData<'vir, D> { data: (&self.data, &other.data), inhabited: self.inhabited, fields: fields.collect(), + did: self.did, } } } @@ -269,6 +280,7 @@ impl<'vir, D: TyDatas<'vir>> EnumData<'vir, D> { data: (&self.data, &other.data), inhabited: self.inhabited, variants: variants.map(|(v1, v2)| v1.zip(v2)).collect(), + did: self.did, } } } @@ -291,10 +303,10 @@ impl<'vir, D1: TyDatas<'vir>, D2: TyDatas<'vir>> TyDatas<'vir> for (D1, D2) { // Deref implementations macro_rules! impls { - ($container:ident$( { $field:ident: $ty:ty })?) => { + ($container:ident$( { $field:ident: $ty:ty $(, $did:ident)?})?) => { impl<'vir, D: TyDatas<'vir>> $container<'vir, D> { - pub fn new(data: D::$container, inhabited: bool $(, $field: $ty)?) -> Self { - Self { data, inhabited, $($field,)? } + pub fn new(data: D::$container, inhabited: bool $(, $field: $ty $(, $did: Option)?)?) -> Self { + Self { data, inhabited, $($field, $($did,)?)? } } } @@ -306,7 +318,7 @@ impl<'vir, D: TyDatas<'vir>> Debug for $container<'vir, D> { impl<'vir, D: TyDatas<'vir>> Clone for $container<'vir, D> { fn clone(&self) -> Self { - Self { data: self.data.clone(), inhabited: self.inhabited, $($field: self.$field.clone())? } + Self { data: self.data.clone(), inhabited: self.inhabited, $($field: self.$field.clone() $(, $did: self.$did.clone())?)? } } } @@ -368,8 +380,8 @@ impl<'vir, D: TyDatas<'vir>> $container<'vir, D> { impls!(TyData { specifics: TySpecifics<'vir, D> }); impl_zip!(TyData.specifics); -impls!(StructData { fields: Vec }); -impls!(EnumData { variants: Vec> }); +impls!(StructData { fields: Vec, did }); +impls!(EnumData { variants: Vec>, did }); impls!(VariantData { inner: StructData<'vir, D> }); impl_zip!(VariantData.inner); diff --git a/prusti-encoder/src/encoders/ty/generics/args.rs b/prusti-encoder/src/encoders/ty/generics/args.rs index ed87d48fc04..01d0302bfe0 100644 --- a/prusti-encoder/src/encoders/ty/generics/args.rs +++ b/prusti-encoder/src/encoders/ty/generics/args.rs @@ -1,4 +1,7 @@ -use prusti_rustc_interface::middle::ty; +use prusti_rustc_interface::{middle::ty, span::def_id::DefId}; +use task_encoder::{TaskEncoder, TaskEncoderDependencies}; + +use crate::encoders::ty::generics::trait_impls::TraitImplEnc; use super::GParams; @@ -10,13 +13,9 @@ pub struct GArgs<'tcx> { pub(super) args: &'tcx [ty::GenericArg<'tcx>], } -pub enum GParamVariant<'vir> { +pub enum GParamVariant { Param(ty::ParamTy), - Alias( - &'vir str, - &'vir str, - Vec<(ty::Ty<'vir>, ty::Ty<'vir>, &'vir str)>, - ), + Alias(DefId), } impl<'tcx> GArgs<'tcx> { @@ -43,38 +42,11 @@ impl<'tcx> GArgs<'tcx> { self.context.normalize(ty) } - pub fn expect_param<'vir>(self) -> GParamVariant<'vir> { + pub fn expect_param(self) -> GParamVariant { assert_eq!(self.args.len(), 1); match self.args[0].expect_ty().kind() { ty::TyKind::Param(p) => GParamVariant::Param(*p), - ty::TyKind::Alias(_k, t) => vir::with_vcx(|vcx| { - let tcx = vcx.tcx(); - let trait_name = vcx.alloc_str( - tcx.item_name(tcx.associated_item(t.def_id).container_id(tcx)) - .as_str(), - ); - let type_name = vcx.alloc_str(tcx.item_name(t.def_id).as_str()); - let assoc_type_substs = tcx - .all_impls(tcx.associated_item(t.def_id).container_id(tcx)) - .map(|imp| { - let imp_type = tcx.type_of(imp).instantiate_identity(); - let assoc_types = tcx - .associated_items(imp) - .filter_by_name_unhygienic_and_kind( - tcx.item_name(t.def_id), - ty::AssocTag::Type, - ) - .collect::>(); - assert!(assoc_types.len() == 1); - let assoc_type = tcx.type_of(assoc_types[0].def_id).instantiate_identity(); - let st_name = vcx.alloc_str( - tcx.type_of(imp).instantiate_identity().to_string().as_str(), - ); - (imp_type, assoc_type, st_name) - }) - .collect::>(); - GParamVariant::Alias(trait_name, type_name, assoc_type_substs) - }), + ty::TyKind::Alias(_k, t) => GParamVariant::Alias(t.def_id), other => panic!("expected type parameter, {other:?}"), } } diff --git a/prusti-encoder/src/encoders/ty/generics/args_ty.rs b/prusti-encoder/src/encoders/ty/generics/args_ty.rs index 8c3220c4c8c..46d4a3dfc59 100644 --- a/prusti-encoder/src/encoders/ty/generics/args_ty.rs +++ b/prusti-encoder/src/encoders/ty/generics/args_ty.rs @@ -37,32 +37,17 @@ impl TaskEncoder for GArgsTyEnc { task_encoder::encoder_cache!(GArgsTyEnc); type TaskDescription<'tcx> = GArgs<'tcx>; type OutputFullDependency<'vir> = GArgsTy<'vir>; - type OutputFullLocal<'vir> = Option>; fn task_to_key<'vir>(task: &Self::TaskDescription<'vir>) -> Self::TaskKey<'vir> { *task } - fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { - for dom in GArgsTyEnc::all_outputs_local_no_errors() - .into_iter() - .flatten() - { - program.add_domain(dom); - } - } - fn do_encode_full<'vir>( task_key: &Self::TaskKey<'vir>, deps: &mut TaskEncoderDependencies<'vir, Self>, ) -> EncodeFullResult<'vir, Self> { deps.emit_output_ref(*task_key, ())?; let params = deps.require_dep::(task_key.context)?; - let mut builder = params::Builder { - functions: Vec::new(), - axioms: Vec::new(), - domain_name: "", - }; let ty_args = task_key .args .iter() @@ -72,7 +57,7 @@ impl TaskEncoder for GArgsTyEnc { let decomp = vir::with_vcx(|vcx| { RustTyDecomposition::from_ty(arg, vcx.tcx(), task_key.context) }); - params.ty_expr(deps, decomp, &mut builder) + params.ty_expr(deps, decomp) }) .collect::>(); let const_args = task_key @@ -101,21 +86,6 @@ impl TaskEncoder for GArgsTyEnc { ty_args: vcx.alloc_slice(&ty_args), const_args: vcx.alloc_slice(&const_args), }); - if !builder.functions.is_empty() { - vir::with_vcx(|vcx| { - Ok(( - Some(vcx.mk_domain( - ViperIdent::new(builder.domain_name), - &[], - vcx.alloc_slice(&builder.axioms), - vcx.alloc_slice(&builder.functions), - None, - )), - args, - )) - }) - } else { - Ok((None, args)) - } + Ok(((), args)) } } diff --git a/prusti-encoder/src/encoders/ty/generics/mod.rs b/prusti-encoder/src/encoders/ty/generics/mod.rs index 66aea9f38af..626ec23318a 100644 --- a/prusti-encoder/src/encoders/ty/generics/mod.rs +++ b/prusti-encoder/src/encoders/ty/generics/mod.rs @@ -3,6 +3,8 @@ mod params; mod casters; mod args_ty; mod args; +pub mod traits; +pub mod trait_impls; pub use args::*; pub use args_ty::*; diff --git a/prusti-encoder/src/encoders/ty/generics/params.rs b/prusti-encoder/src/encoders/ty/generics/params.rs index ba115647b0a..d9a53d78604 100644 --- a/prusti-encoder/src/encoders/ty/generics/params.rs +++ b/prusti-encoder/src/encoders/ty/generics/params.rs @@ -11,7 +11,7 @@ use crate::encoders::{ ty::{ RustTyDecomposition, data::TySpecifics, - generics::{GArgsTyEnc, GParamVariant}, + generics::{GArgsTyEnc, GParamVariant, traits::TraitEnc}, lifted::TyConstructorEnc, }, }; @@ -181,13 +181,6 @@ impl<'vir> From for GParams<'vir> { /// `fn foo(x: U)` into the Viper `method foo(x: Ref, T: Type, U: Type)` /// (handles the type parameters). pub struct GenericParamsEnc; - -pub struct Builder<'vir> { - pub axioms: Vec>, - pub functions: Vec>, - pub domain_name: &'vir str, -} - #[derive(Debug, Clone)] pub struct GenericParams<'vir> { ty_args: &'vir [vir::TypeTyVal<'vir>], @@ -258,64 +251,32 @@ impl<'vir> GenericParams<'vir> { &self, deps: &mut TaskEncoderDependencies<'vir, E>, ty: RustTyDecomposition<'vir>, - builder: &mut Builder<'vir>, ) -> vir::ExprTyVal<'vir> { if let TySpecifics::Param(()) = &ty.ty.specifics { let param = ty.args.expect_param(); return match param { GParamVariant::Param(p) => self.ty_exprs[self.map_idx(p.index).unwrap()], - GParamVariant::Alias(trait_name, type_name, assoc_type_substs) => { - vir::with_vcx(|vcx| { - let idn: FunctionIdn<'_, vir::TyVal, vir::TyVal> = FunctionIdn::new( - ViperIdent::new( - vcx.alloc_str(&format!("{}_Assoc_{}_func", trait_name, type_name)), - ), - vir::TYPE_TYVAL, - vir::TYPE_TYVAL, - ); - let assoc_type_func = vcx.mk_domain_function(idn, false, None); - builder.functions.push(assoc_type_func); - let mut axioms = assoc_type_substs - .iter() - .map(|(impl_type, assoc_type, impl_name)| { - let impl_type_expr = self.ty_expr( - deps, - RustTyDecomposition::from_ty( - *impl_type, - vcx.tcx(), - ty.args.context, - ), - builder, - ); - let assoc_type_expr = self.ty_expr( - deps, - RustTyDecomposition::from_ty( - *assoc_type, - vcx.tcx(), - ty.args.context, - ), - builder, - ); - vcx.alloc(DomainAxiomData { - name: vcx.alloc_str(&format!( - "{}_Assoc_{}_{}", - trait_name, type_name, impl_name - )), - expr: vir::expr! {([idn](impl_type_expr)) == (assoc_type_expr)}, - }) - }) - .collect::>(); - builder.axioms.append(&mut axioms); - builder.domain_name = - vcx.alloc_str(&format!("{}_Assoc_{}", trait_name, type_name)); - match ty.ty.data.params.params[0].expect_ty().kind() { - ty::TyKind::Param(p) => { - (idn)(self.ty_exprs[self.map_idx(p.index).unwrap()]) - } - _ => unreachable!(), + GParamVariant::Alias(assoc_item_did) => vir::with_vcx(|vcx| { + let tcx = vcx.tcx(); + let trait_data = deps + .require_dep::( + tcx.associated_item(assoc_item_did).container_id(tcx), + ) + .unwrap(); + let assoc_funs = trait_data + .type_did_fun_mapping + .iter() + .filter(|(assoc_did, _)| *assoc_did == assoc_item_did) + .map(|(_, assoc_fun)| assoc_fun) + .collect::>(); + assert!(assoc_funs.len() == 1); + match ty.ty.data.params.params[0].expect_ty().kind() { + ty::TyKind::Param(p) => { + (assoc_funs[0])(self.ty_exprs[self.map_idx(p.index).unwrap()]) } - }) - } + _ => unreachable!(), + } + }), }; } let ty_constructor = deps diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs new file mode 100644 index 00000000000..bf9b7cb3002 --- /dev/null +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -0,0 +1,99 @@ +use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; +use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; +use vir::{Domain, FunctionIdn, ViperIdent}; + +use crate::encoders::ty::{ + RustTyDecomposition, + generics::{GParams, GenericParamsEnc, traits::TraitEnc}, +}; + +pub struct TraitImplEnc; + +impl TaskEncoder for TraitImplEnc { + task_encoder::encoder_cache!(TraitImplEnc); + + fn task_to_key<'vir>(task: &Self::TaskDescription<'vir>) -> Self::TaskKey<'vir> { + *task + } + + fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { + for dom in TraitImplEnc::all_outputs_local_no_errors() { + program.add_domain(dom); + } + } + + type TaskDescription<'vir> = (DefId, GParams<'vir>); + type OutputFullLocal<'vir> = Domain<'vir>; + + fn do_encode_full<'vir>( + task_key: &Self::TaskKey<'vir>, + deps: &mut TaskEncoderDependencies<'vir, Self>, + ) -> EncodeFullResult<'vir, Self> { + deps.emit_output_ref(*task_key, ())?; + + let params = deps.require_dep::(task_key.1)?; + + vir::with_vcx(|vcx| { + let tcx = vcx.tcx(); + let trait_did = tcx + .impl_trait_ref(task_key.0) + .unwrap() + .instantiate_identity() + .def_id; + let trait_data = deps.require_dep::(trait_did)?; + + let mut axs = Vec::new(); + + tcx.associated_items(task_key.0) + .in_definition_order() + .filter(|item| matches!(item.kind, AssocKind::Type { data: _ })) + .for_each(|impl_item| { + trait_data + .type_did_fun_mapping + .into_iter() + .filter(|(assoc_did, _)| Some(*assoc_did) == impl_item.trait_item_def_id) + .for_each(|(_, assoc_fun)| { + let impl_type_expr = params.ty_expr( + deps, + RustTyDecomposition::from_ty( + tcx.type_of(task_key.0).instantiate_identity(), + tcx, + task_key.1, + ), + ); + let assoc_type_expr = params.ty_expr( + deps, + RustTyDecomposition::from_ty( + tcx.type_of(impl_item.def_id).instantiate_identity(), + tcx, + task_key.1, + ), + ); + axs.push(vcx.mk_domain_axiom( + ViperIdent::new(vcx.alloc_str(&format!( + "{}_Assoc_{}_{}", + trait_data.trait_name, + tcx.item_name(impl_item.def_id).to_string(), + tcx.type_of(task_key.0).instantiate_identity().to_string() + ))), + vir::expr! {([assoc_fun](impl_type_expr)) == (assoc_type_expr)}, + )) + }); + }); + + let dom = vcx.mk_domain( + ViperIdent::new(vcx.alloc_str(&format!( + "t_{}_{}", + trait_data.trait_name, + tcx.type_of(task_key.0).instantiate_identity().to_string() + ))), + &[], + vcx.alloc_slice(&axs), + &[], + None, + ); + + Ok((dom, ())) + }) + } +} diff --git a/prusti-encoder/src/encoders/ty/generics/traits.rs b/prusti-encoder/src/encoders/ty/generics/traits.rs new file mode 100644 index 00000000000..e56e6ef586d --- /dev/null +++ b/prusti-encoder/src/encoders/ty/generics/traits.rs @@ -0,0 +1,66 @@ +use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; +use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; +use vir::{Domain, FunctionIdn, ViperIdent}; + +pub struct TraitEnc; + +#[derive(Debug, Clone, Copy)] +pub struct TraitData<'vir> { + pub trait_name: &'vir str, + pub type_did_fun_mapping: &'vir [(DefId, FunctionIdn<'vir, vir::TyVal, vir::TyVal>)], +} + +impl TaskEncoder for TraitEnc { + task_encoder::encoder_cache!(TraitEnc); + + fn task_to_key<'vir>(task: &Self::TaskDescription<'vir>) -> Self::TaskKey<'vir> { + *task + } + + type TaskDescription<'vir> = DefId; + + type OutputFullDependency<'vir> = TraitData<'vir>; + type OutputFullLocal<'vir> = vir::Domain<'vir>; + + fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { + for dom in TraitEnc::all_outputs_local_no_errors() { + program.add_domain(dom); + } + } + + fn do_encode_full<'vir>( + task_key: &Self::TaskKey<'vir>, + deps: &mut TaskEncoderDependencies<'vir, Self>, + ) -> EncodeFullResult<'vir, Self> { + deps.emit_output_ref(*task_key, ())?; + vir::with_vcx(|vcx| { + let tcx = vcx.tcx(); + let trait_name = vcx.alloc_str(tcx.item_name(task_key).as_str()); + let type_did_fun_mapping = tcx.associated_items(task_key).in_definition_order().filter(|item| matches!(item.kind, AssocKind::Type{data: _})).map(|item| (item.def_id, FunctionIdn::new( + ViperIdent::new( + vcx.alloc_str(&format!("{}_Assoc_{}_func", trait_name, tcx.item_name(item.def_id))), + ), + vir::TYPE_TYVAL, + vir::TYPE_TYVAL, + ))).collect::>(); + let assoc_funs = type_did_fun_mapping + .iter() + .map(|(_, function_idn)| vcx.mk_domain_function(*function_idn, false, None)) + .collect::>(); + let trait_domain = vcx.mk_domain( + ViperIdent::new(vcx.alloc_str(&format!("t_{}", trait_name))), + &[], + &[], + vcx.alloc_slice(assoc_funs.as_slice()), + None, + ); + Ok(( + trait_domain, + TraitData { + trait_name, + type_did_fun_mapping: vcx.alloc_slice(type_did_fun_mapping.as_slice()), + }, + )) + }) + } +} diff --git a/prusti-encoder/src/encoders/ty/kinds/enumlike.rs b/prusti-encoder/src/encoders/ty/kinds/enumlike.rs index 3d0c5320c8f..5e43ddda951 100644 --- a/prusti-encoder/src/encoders/ty/kinds/enumlike.rs +++ b/prusti-encoder/src/encoders/ty/kinds/enumlike.rs @@ -19,6 +19,10 @@ pub(crate) fn ty_pure<'vir>( deps: &mut TaskEncoderDependencies<'vir, TyPureEnc>, builder: &mut AdtBuilder<'vir>, ) -> Result, EncodeFullError<'vir, TyPureEnc>> { + if let Some(d) = data.did { + super::structlike::generate_axioms_for_impls(d, deps)?; + } + let discr_ty = deps.require_dep::(RustTyDecomposition::from_prim_ty(data.discr).ty)?; let discr_prim = discr_ty.expect_primitive(); @@ -60,6 +64,7 @@ pub(crate) fn ty_pure<'vir>( }, data.inhabited, variants, + data.did, )) } @@ -69,6 +74,10 @@ pub(crate) fn ty_impure<'vir>( deps: &mut TaskEncoderDependencies<'vir, TyImpureEnc>, builder: &mut PredicateBuilder<'vir>, ) -> Result, EncodeFullError<'vir, TyImpureEnc>> { + if let Some(d) = data.did { + super::structlike::generate_axioms_for_impls(d, deps)?; + } + let ref_self_decl = builder.ref_self_decl(); let ref_self = builder.vcx.mk_local_ex(ref_self_decl); @@ -181,5 +190,6 @@ pub(crate) fn ty_impure<'vir>( }, data.inhabited, variants.into_iter().map(|v| v.3).collect::>(), + data.did, )) } diff --git a/prusti-encoder/src/encoders/ty/kinds/structlike.rs b/prusti-encoder/src/encoders/ty/kinds/structlike.rs index 2c7a6fcaab8..d425e9eaad0 100644 --- a/prusti-encoder/src/encoders/ty/kinds/structlike.rs +++ b/prusti-encoder/src/encoders/ty/kinds/structlike.rs @@ -3,14 +3,17 @@ use crate::encoders::{ ty::{ RustTyDatas, data::{StructData, TyData}, + generics::{GParams, trait_impls::TraitImplEnc}, impure::{ImpureTyDatas, PredicateBuilder, TyImpureEnc, TyImpureFieldData}, pure::{AdtBuilder, PureTyDatas, TyPureEnc, TyPureFieldData, TyPureStructData}, use_pure::TyUsePureEnc, }, }; -use task_encoder::{EncodeFullError, TaskEncoderDependencies}; +use task_encoder::{EncodeFullError, TaskEncoder, TaskEncoderDependencies}; use vir::{CastType, HasType, PredicateIdn}; +use prusti_rustc_interface::span::def_id::DefId; + pub(crate) fn ty_pure<'vir>( task_key: &TyData<'vir, RustTyDatas>, data: &StructData<'vir, RustTyDatas>, @@ -20,6 +23,25 @@ pub(crate) fn ty_pure<'vir>( ty_pure_variant("", None, task_key, data, deps, builder) } +pub(super) fn generate_axioms_for_impls<'vir, E: TaskEncoder + 'vir + ?Sized>( + did: DefId, + deps: &mut TaskEncoderDependencies<'vir, E>, +) -> Result<(), EncodeFullError<'vir, E>> { + vir::with_vcx(|vcx| { + let tcx = vcx.tcx(); + for trait_id in tcx.visible_traits() { + for impl_id in tcx.all_impls(trait_id) { + if tcx.type_of(impl_id).instantiate_identity() + == tcx.type_of(did).instantiate_identity() + { + deps.require_dep::((impl_id, GParams::empty()))?; + } + } + } + Ok(()) + }) +} + pub(super) fn ty_pure_variant<'vir>( prefix: &str, discr: Option>, @@ -28,6 +50,9 @@ pub(super) fn ty_pure_variant<'vir>( deps: &mut TaskEncoderDependencies<'vir, TyPureEnc>, builder: &mut AdtBuilder<'vir>, ) -> Result, EncodeFullError<'vir, TyPureEnc>> { + if let Some(d) = data.did { + generate_axioms_for_impls(d, deps)?; + } let field_tys = data .fields .iter() @@ -51,6 +76,7 @@ pub(super) fn ty_pure_variant<'vir>( }, data.inhabited, des, + data.did, )) } @@ -95,6 +121,9 @@ pub(crate) fn ty_impure_variant<'vir>( deps: &mut TaskEncoderDependencies<'vir, TyImpureEnc>, builder: &mut PredicateBuilder<'vir>, ) -> Result, EncodeFullError<'vir, TyImpureEnc>> { + if let Some(d) = data.did { + generate_axioms_for_impls(d, deps)?; + } let fields = data .fields .iter() @@ -194,7 +223,7 @@ pub(crate) fn ty_impure_variant<'vir>( }; Ok(( - StructData::new((), data.inhabited, field_accessors), + StructData::new((), data.inhabited, field_accessors, data.did), pred_owned, variant_snap_expr, )) diff --git a/prusti-encoder/src/encoders/ty/rust_ty.rs b/prusti-encoder/src/encoders/ty/rust_ty.rs index 3f5950e9a21..7d28c0c0f0a 100644 --- a/prusti-encoder/src/encoders/ty/rust_ty.rs +++ b/prusti-encoder/src/encoders/ty/rust_ty.rs @@ -14,6 +14,8 @@ use super::{ generics::{GArgs, GParams}, }; +use prusti_rustc_interface::span::def_id::DefId; + #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct RustTyDecomposition<'tcx> { pub ty: RustTy<'tcx>, @@ -442,7 +444,7 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { ty: LazyRustTy(Self::new_param_ty(i as u32)), }) .collect::>(); - TySpecifics::mk_structlike((), true, fields) + TySpecifics::mk_structlike((), true, fields, None) } ty::TyKind::Array(..) | ty::TyKind::Slice(..) => { // TODO: add array/slice support @@ -470,13 +472,13 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { ty: LazyRustTy(ty), }) .collect::>(); - TySpecifics::mk_structlike((), true, fields) + TySpecifics::mk_structlike((), true, fields, None) } ty::TyKind::Never => { let data = vir::with_vcx(|vcx| RustEnumData { discr: vcx.tcx().types.isize, }); - TySpecifics::mk_enumlike(data, false, Vec::new()) + TySpecifics::mk_enumlike(data, false, Vec::new(), None) } // TODO: add str support ty::TyKind::Str => TySpecifics::mk_opaque(()), @@ -496,12 +498,12 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { fid: abi::FieldIdx::from_usize(0), ty: LazyRustTy(Self::new_param_ty(0)), }]; - return TySpecifics::mk_structlike((), true, fields); + return TySpecifics::mk_structlike((), true, fields, Some(adt.did())); } match adt.adt_kind() { ty::AdtKind::Struct => { - let data = Self::from_struct(adt.non_enum_variant()); + let data = Self::from_struct(adt.non_enum_variant(), adt.did()); Self::StructLike(data) } ty::AdtKind::Enum => { @@ -515,9 +517,9 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { } } - fn from_struct(variant: &ty::VariantDef) -> StructData<'tcx, RustTyDatas> { + fn from_struct(variant: &ty::VariantDef, did: DefId) -> StructData<'tcx, RustTyDatas> { let fields = Self::from_fields(&variant.fields); - StructData::new((), true, fields) + StructData::new((), true, fields, Some(did)) } fn from_enum(adt: ty::AdtDef<'tcx>) -> EnumData<'tcx, RustTyDatas> { @@ -537,11 +539,11 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { discr_val: discr.val, }, true, - StructData::new((), true, fields), + StructData::new((), true, fields, Some(adt.did())), ) }) .collect::>(); - EnumData::new(data, true, variants) + EnumData::new(data, true, variants, Some(adt.did())) }) } diff --git a/prusti-encoder/src/encoders/ty/use_impure.rs b/prusti-encoder/src/encoders/ty/use_impure.rs index 0ffc7e02d52..fb8a287811d 100644 --- a/prusti-encoder/src/encoders/ty/use_impure.rs +++ b/prusti-encoder/src/encoders/ty/use_impure.rs @@ -196,12 +196,13 @@ impl<'a, 'vir> TyUseImpureWalker<'a, 'vir> { }) .collect::>(); let inhabited = data.inhabited; + let did = data.did; let data = TyUseImpureStructData { args: self.args_t, ref_to_pred, impure: *data.1, }; - StructData::new(data, inhabited, fields) + StructData::new(data, inhabited, fields, did) } fn encode_enumlike( @@ -219,11 +220,12 @@ impl<'a, 'vir> TyUseImpureWalker<'a, 'vir> { }) .collect::>(); let inhabited = data.inhabited; + let did = data.did; let data = TyUseImpureEnumData { args: self.args_t, impure: *data.1, }; - EnumData::new(data, inhabited, variants) + EnumData::new(data, inhabited, variants, did) } } diff --git a/prusti-encoder/src/encoders/ty/use_pure.rs b/prusti-encoder/src/encoders/ty/use_pure.rs index 64101dabf7b..38d984b2c0f 100644 --- a/prusti-encoder/src/encoders/ty/use_pure.rs +++ b/prusti-encoder/src/encoders/ty/use_pure.rs @@ -199,11 +199,12 @@ impl<'a, 'vir> TyUsePureWalker<'a, 'vir> { }) .collect::>(); let inhabited = data.inhabited; + let did = data.did; let data = TyUsePureStructData { args: self.args_t, pure: *data.1, }; - StructData::new(data, inhabited, fields) + StructData::new(data, inhabited, fields, did) } fn encode_enumlike( @@ -211,6 +212,7 @@ impl<'a, 'vir> TyUsePureWalker<'a, 'vir> { data: &EnumData<'vir, (RustTyDatas, PureTyDatas)>, params: GParams<'vir>, ) -> EnumData<'vir, UsePureTyDatas> { + let did = data.did; let variants = data .variants .iter() @@ -219,7 +221,7 @@ impl<'a, 'vir> TyUsePureWalker<'a, 'vir> { VariantData::new(*variant.1, variant.inhabited, structlike) }) .collect::>(); - EnumData::new(*data.1, data.inhabited, variants) + EnumData::new(*data.1, data.inhabited, variants, did) } } diff --git a/prusti-encoder/src/lib.rs b/prusti-encoder/src/lib.rs index 067428d2722..3c2565ee1b7 100644 --- a/prusti-encoder/src/lib.rs +++ b/prusti-encoder/src/lib.rs @@ -21,7 +21,7 @@ use crate::encoders::{ Impure, Pure, custom::PairUseEnc, ty::{ - generics::{GArgsCastEnc, GArgsTyEnc}, + generics::{GArgsCastEnc, GArgsTyEnc, trait_impls::TraitImplEnc, traits::TraitEnc}, interpretation::bitvec::BitVecEnc, lifted::{TyConstructorEnc, TypeOfEnc}, }, @@ -103,7 +103,8 @@ pub fn test_entrypoint<'tcx>( program.header("custom"); PairUseEnc::emit_outputs(&mut program); - GArgsTyEnc::emit_outputs(&mut program); + TraitEnc::emit_outputs(&mut program); + TraitImplEnc::emit_outputs(&mut program); if std::env::var("LOCAL_TESTING").is_ok() { std::fs::write("local-testing/simple.vpr", program.code()).unwrap(); From 24c66d75c28d5bec549e02626e257fd34db3bdab Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Tue, 25 Nov 2025 15:57:26 +0100 Subject: [PATCH 06/26] Run clippy --fix --- prusti-encoder/src/encoders/ty/generics/args.rs | 2 -- prusti-encoder/src/encoders/ty/generics/args_ty.rs | 3 +-- prusti-encoder/src/encoders/ty/generics/params.rs | 2 +- prusti-encoder/src/encoders/ty/generics/trait_impls.rs | 10 +++++----- prusti-encoder/src/encoders/ty/generics/traits.rs | 2 +- prusti-encoder/src/lib.rs | 2 +- 6 files changed, 9 insertions(+), 12 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/args.rs b/prusti-encoder/src/encoders/ty/generics/args.rs index 01d0302bfe0..4a74766fa36 100644 --- a/prusti-encoder/src/encoders/ty/generics/args.rs +++ b/prusti-encoder/src/encoders/ty/generics/args.rs @@ -1,7 +1,5 @@ use prusti_rustc_interface::{middle::ty, span::def_id::DefId}; -use task_encoder::{TaskEncoder, TaskEncoderDependencies}; -use crate::encoders::ty::generics::trait_impls::TraitImplEnc; use super::GParams; diff --git a/prusti-encoder/src/encoders/ty/generics/args_ty.rs b/prusti-encoder/src/encoders/ty/generics/args_ty.rs index 46d4a3dfc59..7b68d3838f1 100644 --- a/prusti-encoder/src/encoders/ty/generics/args_ty.rs +++ b/prusti-encoder/src/encoders/ty/generics/args_ty.rs @@ -1,11 +1,10 @@ use prusti_rustc_interface::middle::ty; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::ViperIdent; use crate::encoders::{ ConstEnc, r#const::ConstEncTask, - ty::{RustTyDecomposition, generics::params}, + ty::RustTyDecomposition, }; use super::{GArgs, GenericParamsEnc}; diff --git a/prusti-encoder/src/encoders/ty/generics/params.rs b/prusti-encoder/src/encoders/ty/generics/params.rs index d9a53d78604..9415ec66f97 100644 --- a/prusti-encoder/src/encoders/ty/generics/params.rs +++ b/prusti-encoder/src/encoders/ty/generics/params.rs @@ -4,7 +4,7 @@ use prusti_rustc_interface::{ span::{def_id::DefId, symbol}, }; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{CastType, DomainAxiomData, FunctionIdn, HasType, ViperIdent}; +use vir::{CastType, HasType}; use crate::encoders::{ TyUsePureEnc, diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index bf9b7cb3002..a04edfa64a0 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -1,6 +1,6 @@ use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{Domain, FunctionIdn, ViperIdent}; +use vir::{Domain, ViperIdent}; use crate::encoders::ty::{ RustTyDecomposition, @@ -50,7 +50,7 @@ impl TaskEncoder for TraitImplEnc { .for_each(|impl_item| { trait_data .type_did_fun_mapping - .into_iter() + .iter() .filter(|(assoc_did, _)| Some(*assoc_did) == impl_item.trait_item_def_id) .for_each(|(_, assoc_fun)| { let impl_type_expr = params.ty_expr( @@ -73,8 +73,8 @@ impl TaskEncoder for TraitImplEnc { ViperIdent::new(vcx.alloc_str(&format!( "{}_Assoc_{}_{}", trait_data.trait_name, - tcx.item_name(impl_item.def_id).to_string(), - tcx.type_of(task_key.0).instantiate_identity().to_string() + tcx.item_name(impl_item.def_id), + tcx.type_of(task_key.0).instantiate_identity() ))), vir::expr! {([assoc_fun](impl_type_expr)) == (assoc_type_expr)}, )) @@ -85,7 +85,7 @@ impl TaskEncoder for TraitImplEnc { ViperIdent::new(vcx.alloc_str(&format!( "t_{}_{}", trait_data.trait_name, - tcx.type_of(task_key.0).instantiate_identity().to_string() + tcx.type_of(task_key.0).instantiate_identity() ))), &[], vcx.alloc_slice(&axs), diff --git a/prusti-encoder/src/encoders/ty/generics/traits.rs b/prusti-encoder/src/encoders/ty/generics/traits.rs index e56e6ef586d..f5cb9492837 100644 --- a/prusti-encoder/src/encoders/ty/generics/traits.rs +++ b/prusti-encoder/src/encoders/ty/generics/traits.rs @@ -1,6 +1,6 @@ use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{Domain, FunctionIdn, ViperIdent}; +use vir::{FunctionIdn, ViperIdent}; pub struct TraitEnc; diff --git a/prusti-encoder/src/lib.rs b/prusti-encoder/src/lib.rs index 3c2565ee1b7..3bfc17c0bef 100644 --- a/prusti-encoder/src/lib.rs +++ b/prusti-encoder/src/lib.rs @@ -21,7 +21,7 @@ use crate::encoders::{ Impure, Pure, custom::PairUseEnc, ty::{ - generics::{GArgsCastEnc, GArgsTyEnc, trait_impls::TraitImplEnc, traits::TraitEnc}, + generics::{GArgsCastEnc, trait_impls::TraitImplEnc, traits::TraitEnc}, interpretation::bitvec::BitVecEnc, lifted::{TyConstructorEnc, TypeOfEnc}, }, From 5ed73d93787ea6c5af3d20b011ea27f983247676 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Tue, 25 Nov 2025 17:16:17 +0100 Subject: [PATCH 07/26] Fix issue that trait/impl encodings use invalid identifiers --- .../src/encoders/ty/generics/args.rs | 1 - .../src/encoders/ty/generics/args_ty.rs | 6 +--- .../src/encoders/ty/generics/trait_impls.rs | 14 +++++---- .../src/encoders/ty/generics/traits.rs | 31 +++++++++++++------ 4 files changed, 31 insertions(+), 21 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/args.rs b/prusti-encoder/src/encoders/ty/generics/args.rs index 4a74766fa36..5017a2ee73e 100644 --- a/prusti-encoder/src/encoders/ty/generics/args.rs +++ b/prusti-encoder/src/encoders/ty/generics/args.rs @@ -1,6 +1,5 @@ use prusti_rustc_interface::{middle::ty, span::def_id::DefId}; - use super::GParams; /// The instantiation of generic arguments, typically found in `TyKind::Adt` and diff --git a/prusti-encoder/src/encoders/ty/generics/args_ty.rs b/prusti-encoder/src/encoders/ty/generics/args_ty.rs index 7b68d3838f1..dc7a5ecd55b 100644 --- a/prusti-encoder/src/encoders/ty/generics/args_ty.rs +++ b/prusti-encoder/src/encoders/ty/generics/args_ty.rs @@ -1,11 +1,7 @@ use prusti_rustc_interface::middle::ty; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use crate::encoders::{ - ConstEnc, - r#const::ConstEncTask, - ty::RustTyDecomposition, -}; +use crate::encoders::{ConstEnc, r#const::ConstEncTask, ty::RustTyDecomposition}; use super::{GArgs, GenericParamsEnc}; diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index a04edfa64a0..d8c1f1bfc75 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -1,6 +1,6 @@ use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{Domain, ViperIdent}; +use vir::{Domain, ViperIdent, vir_format_identifier}; use crate::encoders::ty::{ RustTyDecomposition, @@ -70,23 +70,25 @@ impl TaskEncoder for TraitImplEnc { ), ); axs.push(vcx.mk_domain_axiom( - ViperIdent::new(vcx.alloc_str(&format!( + vir_format_identifier!( + vcx, "{}_Assoc_{}_{}", trait_data.trait_name, tcx.item_name(impl_item.def_id), tcx.type_of(task_key.0).instantiate_identity() - ))), + ), vir::expr! {([assoc_fun](impl_type_expr)) == (assoc_type_expr)}, )) }); }); let dom = vcx.mk_domain( - ViperIdent::new(vcx.alloc_str(&format!( + vir_format_identifier!( + vcx, "t_{}_{}", trait_data.trait_name, - tcx.type_of(task_key.0).instantiate_identity() - ))), + tcx.type_of(task_key.0).instantiate_identity().to_string() + ), &[], vcx.alloc_slice(&axs), &[], diff --git a/prusti-encoder/src/encoders/ty/generics/traits.rs b/prusti-encoder/src/encoders/ty/generics/traits.rs index f5cb9492837..393019b5de8 100644 --- a/prusti-encoder/src/encoders/ty/generics/traits.rs +++ b/prusti-encoder/src/encoders/ty/generics/traits.rs @@ -1,6 +1,6 @@ use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{FunctionIdn, ViperIdent}; +use vir::{FunctionIdn, ViperIdent, vir_format_identifier}; pub struct TraitEnc; @@ -36,19 +36,32 @@ impl TaskEncoder for TraitEnc { vir::with_vcx(|vcx| { let tcx = vcx.tcx(); let trait_name = vcx.alloc_str(tcx.item_name(task_key).as_str()); - let type_did_fun_mapping = tcx.associated_items(task_key).in_definition_order().filter(|item| matches!(item.kind, AssocKind::Type{data: _})).map(|item| (item.def_id, FunctionIdn::new( - ViperIdent::new( - vcx.alloc_str(&format!("{}_Assoc_{}_func", trait_name, tcx.item_name(item.def_id))), - ), - vir::TYPE_TYVAL, - vir::TYPE_TYVAL, - ))).collect::>(); + let type_did_fun_mapping = tcx + .associated_items(task_key) + .in_definition_order() + .filter(|item| matches!(item.kind, AssocKind::Type { data: _ })) + .map(|item| { + ( + item.def_id, + FunctionIdn::new( + vir_format_identifier!( + vcx, + "{}_Assoc_{}_func", + trait_name, + tcx.item_name(item.def_id), + ), + vir::TYPE_TYVAL, + vir::TYPE_TYVAL, + ), + ) + }) + .collect::>(); let assoc_funs = type_did_fun_mapping .iter() .map(|(_, function_idn)| vcx.mk_domain_function(*function_idn, false, None)) .collect::>(); let trait_domain = vcx.mk_domain( - ViperIdent::new(vcx.alloc_str(&format!("t_{}", trait_name))), + vir_format_identifier!(vcx, "t_{}", trait_name), &[], &[], vcx.alloc_slice(assoc_funs.as_slice()), From 0fd9e87304c1a34f60bc7da0048519048bb8eba1 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Tue, 25 Nov 2025 17:17:19 +0100 Subject: [PATCH 08/26] Run clippy --fix --- prusti-encoder/src/encoders/ty/generics/trait_impls.rs | 2 +- prusti-encoder/src/encoders/ty/generics/traits.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index d8c1f1bfc75..ff4ebeb8a6d 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -1,6 +1,6 @@ use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{Domain, ViperIdent, vir_format_identifier}; +use vir::{Domain, vir_format_identifier}; use crate::encoders::ty::{ RustTyDecomposition, diff --git a/prusti-encoder/src/encoders/ty/generics/traits.rs b/prusti-encoder/src/encoders/ty/generics/traits.rs index 393019b5de8..ce6be0e25f2 100644 --- a/prusti-encoder/src/encoders/ty/generics/traits.rs +++ b/prusti-encoder/src/encoders/ty/generics/traits.rs @@ -1,6 +1,6 @@ use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{FunctionIdn, ViperIdent, vir_format_identifier}; +use vir::{FunctionIdn, vir_format_identifier}; pub struct TraitEnc; From 7a743e60817f5ee17e1178b164f3949b5395c647 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Tue, 25 Nov 2025 17:38:06 +0100 Subject: [PATCH 09/26] Add impl function for traits --- .../src/encoders/ty/generics/trait_impls.rs | 24 +++++++++++-------- .../src/encoders/ty/generics/traits.rs | 13 ++++++++-- 2 files changed, 25 insertions(+), 12 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index ff4ebeb8a6d..bafa57e1b6f 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -44,6 +44,18 @@ impl TaskEncoder for TraitImplEnc { let mut axs = Vec::new(); + let struct_ty = tcx.type_of(task_key.0).instantiate_identity(); + + let struct_ty_expr = params.ty_expr( + deps, + RustTyDecomposition::from_ty(struct_ty, tcx, task_key.1), + ); + + axs.push(vcx.mk_domain_axiom( + vir_format_identifier!(vcx, "{}_impl_{}", trait_data.trait_name, struct_ty), + vir::expr! {[trait_data.impl_fun](struct_ty_expr)}, + )); + tcx.associated_items(task_key.0) .in_definition_order() .filter(|item| matches!(item.kind, AssocKind::Type { data: _ })) @@ -53,14 +65,6 @@ impl TaskEncoder for TraitImplEnc { .iter() .filter(|(assoc_did, _)| Some(*assoc_did) == impl_item.trait_item_def_id) .for_each(|(_, assoc_fun)| { - let impl_type_expr = params.ty_expr( - deps, - RustTyDecomposition::from_ty( - tcx.type_of(task_key.0).instantiate_identity(), - tcx, - task_key.1, - ), - ); let assoc_type_expr = params.ty_expr( deps, RustTyDecomposition::from_ty( @@ -75,9 +79,9 @@ impl TaskEncoder for TraitImplEnc { "{}_Assoc_{}_{}", trait_data.trait_name, tcx.item_name(impl_item.def_id), - tcx.type_of(task_key.0).instantiate_identity() + struct_ty ), - vir::expr! {([assoc_fun](impl_type_expr)) == (assoc_type_expr)}, + vir::expr! {([assoc_fun](struct_ty_expr)) == (assoc_type_expr)}, )) }); }); diff --git a/prusti-encoder/src/encoders/ty/generics/traits.rs b/prusti-encoder/src/encoders/ty/generics/traits.rs index ce6be0e25f2..2f5cf9f0f7e 100644 --- a/prusti-encoder/src/encoders/ty/generics/traits.rs +++ b/prusti-encoder/src/encoders/ty/generics/traits.rs @@ -8,6 +8,7 @@ pub struct TraitEnc; pub struct TraitData<'vir> { pub trait_name: &'vir str, pub type_did_fun_mapping: &'vir [(DefId, FunctionIdn<'vir, vir::TyVal, vir::TyVal>)], + pub impl_fun: FunctionIdn<'vir, vir::TyVal, vir::Bool>, } impl TaskEncoder for TraitEnc { @@ -56,15 +57,22 @@ impl TaskEncoder for TraitEnc { ) }) .collect::>(); - let assoc_funs = type_did_fun_mapping + let mut funcs = type_did_fun_mapping .iter() .map(|(_, function_idn)| vcx.mk_domain_function(*function_idn, false, None)) .collect::>(); + let impl_fun = FunctionIdn::new( + vir_format_identifier!(vcx, "{}_impl", trait_name), + vir::TYPE_TYVAL, + vir::TYPE_BOOL, + ); + let impl_fun_data = vcx.mk_domain_function(impl_fun, false, None); + funcs.push(impl_fun_data); let trait_domain = vcx.mk_domain( vir_format_identifier!(vcx, "t_{}", trait_name), &[], &[], - vcx.alloc_slice(assoc_funs.as_slice()), + vcx.alloc_slice(funcs.as_slice()), None, ); Ok(( @@ -72,6 +80,7 @@ impl TaskEncoder for TraitEnc { TraitData { trait_name, type_did_fun_mapping: vcx.alloc_slice(type_did_fun_mapping.as_slice()), + impl_fun, }, )) }) From cfaeef021a32bf7de18db094afc22b3a35a4791b Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Thu, 27 Nov 2025 12:39:55 +0100 Subject: [PATCH 10/26] fix issues --- .../src/encoders/ty/generics/args.rs | 10 ++++++-- .../src/encoders/ty/generics/params.rs | 9 ++------ .../src/encoders/ty/generics/trait_impls.rs | 9 +++++--- .../{type_alias.rs => traits/assoc_type.rs} | 0 .../pass/traits/assoc_type_gen_trait.rs | 23 +++++++++++++++++++ 5 files changed, 39 insertions(+), 12 deletions(-) rename prusti-tests/tests/verify/pass/{type_alias.rs => traits/assoc_type.rs} (100%) create mode 100644 prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs diff --git a/prusti-encoder/src/encoders/ty/generics/args.rs b/prusti-encoder/src/encoders/ty/generics/args.rs index 5017a2ee73e..c12a7d480ea 100644 --- a/prusti-encoder/src/encoders/ty/generics/args.rs +++ b/prusti-encoder/src/encoders/ty/generics/args.rs @@ -12,7 +12,7 @@ pub struct GArgs<'tcx> { pub enum GParamVariant { Param(ty::ParamTy), - Alias(DefId), + Alias(DefId, u32), } impl<'tcx> GArgs<'tcx> { @@ -43,7 +43,13 @@ impl<'tcx> GArgs<'tcx> { assert_eq!(self.args.len(), 1); match self.args[0].expect_ty().kind() { ty::TyKind::Param(p) => GParamVariant::Param(*p), - ty::TyKind::Alias(_k, t) => GParamVariant::Alias(t.def_id), + ty::TyKind::Alias(_k, t) => { + let alias_arg_ty = t.args[0].as_type().unwrap().kind(); + match alias_arg_ty { + ty::TyKind::Param(p) => GParamVariant::Alias(t.def_id, p.index), + _ => unreachable!(), + } + } other => panic!("expected type parameter, {other:?}"), } } diff --git a/prusti-encoder/src/encoders/ty/generics/params.rs b/prusti-encoder/src/encoders/ty/generics/params.rs index 9415ec66f97..06aba207dc5 100644 --- a/prusti-encoder/src/encoders/ty/generics/params.rs +++ b/prusti-encoder/src/encoders/ty/generics/params.rs @@ -256,7 +256,7 @@ impl<'vir> GenericParams<'vir> { let param = ty.args.expect_param(); return match param { GParamVariant::Param(p) => self.ty_exprs[self.map_idx(p.index).unwrap()], - GParamVariant::Alias(assoc_item_did) => vir::with_vcx(|vcx| { + GParamVariant::Alias(assoc_item_did, idx) => vir::with_vcx(|vcx| { let tcx = vcx.tcx(); let trait_data = deps .require_dep::( @@ -270,12 +270,7 @@ impl<'vir> GenericParams<'vir> { .map(|(_, assoc_fun)| assoc_fun) .collect::>(); assert!(assoc_funs.len() == 1); - match ty.ty.data.params.params[0].expect_ty().kind() { - ty::TyKind::Param(p) => { - (assoc_funs[0])(self.ty_exprs[self.map_idx(p.index).unwrap()]) - } - _ => unreachable!(), - } + (assoc_funs[0])(self.ty_exprs[self.map_idx(idx).unwrap()]) }), }; } diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index bafa57e1b6f..64509c4f832 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -31,7 +31,7 @@ impl TaskEncoder for TraitImplEnc { ) -> EncodeFullResult<'vir, Self> { deps.emit_output_ref(*task_key, ())?; - let params = deps.require_dep::(task_key.1)?; + let params = deps.require_dep::(GParams::from(task_key.0))?; vir::with_vcx(|vcx| { let tcx = vcx.tcx(); @@ -48,7 +48,7 @@ impl TaskEncoder for TraitImplEnc { let struct_ty_expr = params.ty_expr( deps, - RustTyDecomposition::from_ty(struct_ty, tcx, task_key.1), + RustTyDecomposition::from_ty(struct_ty, tcx, GParams::from(task_key.0)), ); axs.push(vcx.mk_domain_axiom( @@ -65,12 +65,15 @@ impl TaskEncoder for TraitImplEnc { .iter() .filter(|(assoc_did, _)| Some(*assoc_did) == impl_item.trait_item_def_id) .for_each(|(_, assoc_fun)| { + let params = deps + .require_dep::(GParams::from(impl_item.def_id)) + .unwrap(); let assoc_type_expr = params.ty_expr( deps, RustTyDecomposition::from_ty( tcx.type_of(impl_item.def_id).instantiate_identity(), tcx, - task_key.1, + GParams::from(impl_item.def_id), ), ); axs.push(vcx.mk_domain_axiom( diff --git a/prusti-tests/tests/verify/pass/type_alias.rs b/prusti-tests/tests/verify/pass/traits/assoc_type.rs similarity index 100% rename from prusti-tests/tests/verify/pass/type_alias.rs rename to prusti-tests/tests/verify/pass/traits/assoc_type.rs diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs new file mode 100644 index 00000000000..1e5796e28e8 --- /dev/null +++ b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs @@ -0,0 +1,23 @@ + +fn foo, X> (x: Y::SomeType) { + +} + +trait MyTrait { + type SomeType; +} + +struct St1{} +struct St2{} + +impl MyTrait for St1 { + type SomeType = T; +} + +impl MyTrait for St2 { + type SomeType = u64; +} + +fn bar() { + foo::(5.2); +} From fd627e42e6eee50823229abf47a5cfddb5b8f3a6 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 28 Nov 2025 12:37:38 +0100 Subject: [PATCH 11/26] Support generic traits --- .../src/encoders/ty/generics/args.rs | 14 +++----- .../src/encoders/ty/generics/params.rs | 34 ++++++++++++++----- .../src/encoders/ty/generics/trait_impls.rs | 18 ++++++++-- .../src/encoders/ty/generics/traits.rs | 11 +++--- .../pass/traits/assoc_type_gen_trait.rs | 13 ++++--- vir/src/macros.rs | 5 ++- 6 files changed, 61 insertions(+), 34 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/args.rs b/prusti-encoder/src/encoders/ty/generics/args.rs index c12a7d480ea..c556c228d86 100644 --- a/prusti-encoder/src/encoders/ty/generics/args.rs +++ b/prusti-encoder/src/encoders/ty/generics/args.rs @@ -10,9 +10,9 @@ pub struct GArgs<'tcx> { pub(super) args: &'tcx [ty::GenericArg<'tcx>], } -pub enum GParamVariant { +pub enum GParamVariant<'tcx> { Param(ty::ParamTy), - Alias(DefId, u32), + Alias(ty::AliasTy<'tcx>), } impl<'tcx> GArgs<'tcx> { @@ -39,17 +39,11 @@ impl<'tcx> GArgs<'tcx> { self.context.normalize(ty) } - pub fn expect_param(self) -> GParamVariant { + pub fn expect_param(self) -> GParamVariant<'tcx> { assert_eq!(self.args.len(), 1); match self.args[0].expect_ty().kind() { ty::TyKind::Param(p) => GParamVariant::Param(*p), - ty::TyKind::Alias(_k, t) => { - let alias_arg_ty = t.args[0].as_type().unwrap().kind(); - match alias_arg_ty { - ty::TyKind::Param(p) => GParamVariant::Alias(t.def_id, p.index), - _ => unreachable!(), - } - } + ty::TyKind::Alias(_k, t) => GParamVariant::Alias(*t), other => panic!("expected type parameter, {other:?}"), } } diff --git a/prusti-encoder/src/encoders/ty/generics/params.rs b/prusti-encoder/src/encoders/ty/generics/params.rs index 06aba207dc5..89e1bfabb7b 100644 --- a/prusti-encoder/src/encoders/ty/generics/params.rs +++ b/prusti-encoder/src/encoders/ty/generics/params.rs @@ -1,6 +1,9 @@ use prusti_interface::specs::typed::ExternSpecKind; use prusti_rustc_interface::{ - middle::ty, + middle::{ + ty, + ty::{ParamTy, TyKind}, + }, span::{def_id::DefId, symbol}, }; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; @@ -176,6 +179,13 @@ impl<'vir> From for GParams<'vir> { } } +fn expect_param(kind: &TyKind) -> ParamTy { + match kind { + TyKind::Param(p) => *p, + _ => unreachable!(), + } +} + /// Handles everything relating to the encoding of generic parameters (both for /// Rust functions and type definitions). Used to turn e.g. the Rust function /// `fn foo(x: U)` into the Viper `method foo(x: Ref, T: Type, U: Type)` @@ -256,21 +266,27 @@ impl<'vir> GenericParams<'vir> { let param = ty.args.expect_param(); return match param { GParamVariant::Param(p) => self.ty_exprs[self.map_idx(p.index).unwrap()], - GParamVariant::Alias(assoc_item_did, idx) => vir::with_vcx(|vcx| { + GParamVariant::Alias(a) => vir::with_vcx(|vcx| { let tcx = vcx.tcx(); - let trait_data = deps - .require_dep::( - tcx.associated_item(assoc_item_did).container_id(tcx), - ) - .unwrap(); + let trait_did = tcx.associated_item(a.def_id).container_id(tcx); + let trait_data = deps.require_dep::(trait_did).unwrap(); let assoc_funs = trait_data .type_did_fun_mapping .iter() - .filter(|(assoc_did, _)| *assoc_did == assoc_item_did) + .filter(|(assoc_did, _)| *assoc_did == a.def_id) .map(|(_, assoc_fun)| assoc_fun) .collect::>(); assert!(assoc_funs.len() == 1); - (assoc_funs[0])(self.ty_exprs[self.map_idx(idx).unwrap()]) + let tys = &a + .args + .iter() + .map(|arg| { + self.ty_exprs[self + .map_idx(expect_param(arg.expect_ty().kind()).index) + .unwrap()] + }) + .collect::>(); + (assoc_funs[0])(tys) }), }; } diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index 64509c4f832..68d73b9c360 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -1,6 +1,6 @@ use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{Domain, vir_format_identifier}; +use vir::{CastType, Domain, vir_format_identifier}; use crate::encoders::ty::{ RustTyDecomposition, @@ -32,6 +32,7 @@ impl TaskEncoder for TraitImplEnc { deps.emit_output_ref(*task_key, ())?; let params = deps.require_dep::(GParams::from(task_key.0))?; + let trait_params = params.ty_exprs(); vir::with_vcx(|vcx| { let tcx = vcx.tcx(); @@ -51,9 +52,20 @@ impl TaskEncoder for TraitImplEnc { RustTyDecomposition::from_ty(struct_ty, tcx, GParams::from(task_key.0)), ); + let mut vec = Vec::new(); + vec.push(struct_ty_expr); + vec.extend(trait_params.to_owned()); + let trait_tys = &vec; + + let impl_fun = trait_data.impl_fun; + let trait_ty_decls = params + .ty_decls() + .iter() + .map(|dec| dec.upcast_ty()) + .collect::>(); axs.push(vcx.mk_domain_axiom( vir_format_identifier!(vcx, "{}_impl_{}", trait_data.trait_name, struct_ty), - vir::expr! {[trait_data.impl_fun](struct_ty_expr)}, + vir::expr! {forall ..[trait_ty_decls] :: {[impl_fun(trait_tys)]} [impl_fun(trait_tys)]}, )); tcx.associated_items(task_key.0) @@ -84,7 +96,7 @@ impl TaskEncoder for TraitImplEnc { tcx.item_name(impl_item.def_id), struct_ty ), - vir::expr! {([assoc_fun](struct_ty_expr)) == (assoc_type_expr)}, + vir::expr! {forall ..[trait_ty_decls] :: {[assoc_fun(trait_tys)]} ([assoc_fun(trait_tys)]) == (assoc_type_expr)}, )) }); }); diff --git a/prusti-encoder/src/encoders/ty/generics/traits.rs b/prusti-encoder/src/encoders/ty/generics/traits.rs index 2f5cf9f0f7e..fc6e2b187fc 100644 --- a/prusti-encoder/src/encoders/ty/generics/traits.rs +++ b/prusti-encoder/src/encoders/ty/generics/traits.rs @@ -2,13 +2,15 @@ use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; use vir::{FunctionIdn, vir_format_identifier}; +use crate::encoders::ty::generics::{GParams, GenericParamsEnc}; + pub struct TraitEnc; #[derive(Debug, Clone, Copy)] pub struct TraitData<'vir> { pub trait_name: &'vir str, - pub type_did_fun_mapping: &'vir [(DefId, FunctionIdn<'vir, vir::TyVal, vir::TyVal>)], - pub impl_fun: FunctionIdn<'vir, vir::TyVal, vir::Bool>, + pub type_did_fun_mapping: &'vir [(DefId, FunctionIdn<'vir, vir::ManyTyVal, vir::TyVal>)], + pub impl_fun: FunctionIdn<'vir, vir::ManyTyVal, vir::Bool>, } impl TaskEncoder for TraitEnc { @@ -36,6 +38,7 @@ impl TaskEncoder for TraitEnc { deps.emit_output_ref(*task_key, ())?; vir::with_vcx(|vcx| { let tcx = vcx.tcx(); + let params = deps.require_dep::(GParams::from(*task_key))?; let trait_name = vcx.alloc_str(tcx.item_name(task_key).as_str()); let type_did_fun_mapping = tcx .associated_items(task_key) @@ -51,7 +54,7 @@ impl TaskEncoder for TraitEnc { trait_name, tcx.item_name(item.def_id), ), - vir::TYPE_TYVAL, + vcx.alloc_slice(&(vec![vir::TYPE_TYVAL; params.ty_exprs().len()])), vir::TYPE_TYVAL, ), ) @@ -63,7 +66,7 @@ impl TaskEncoder for TraitEnc { .collect::>(); let impl_fun = FunctionIdn::new( vir_format_identifier!(vcx, "{}_impl", trait_name), - vir::TYPE_TYVAL, + vcx.alloc_slice(&(vec![vir::TYPE_TYVAL; params.ty_exprs().len()])), vir::TYPE_BOOL, ); let impl_fun_data = vcx.mk_domain_function(impl_fun, false, None); diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs index 1e5796e28e8..28ff9b43b25 100644 --- a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs +++ b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs @@ -1,23 +1,26 @@ -fn foo, X> (x: Y::SomeType) { +fn foo, Z> (x: Y::SomeType, y: Y::SomeOtherType) { } -trait MyTrait { +trait MyTrait { type SomeType; + type SomeOtherType; } struct St1{} struct St2{} -impl MyTrait for St1 { +impl MyTrait for St1 { type SomeType = T; + type SomeOtherType = T2; } -impl MyTrait for St2 { +impl MyTrait for St2 { type SomeType = u64; + type SomeOtherType = T; } fn bar() { - foo::(5.2); + foo::(5.2, 6); } diff --git a/vir/src/macros.rs b/vir/src/macros.rs index bebd8ac21c5..adc0b93e83a 100644 --- a/vir/src/macros.rs +++ b/vir/src/macros.rs @@ -402,9 +402,8 @@ macro_rules! expr_inner { ) }; (@forall_qvars($qvars:ident); :: $($tokens:tt)*) => { compile_error!(concat!("VIR missing triggers or body: `" , stringify!($($tokens)*), "`")) }; - (@forall_qvars($qvars:ident); , ..[$outer:ident] $($tokens:tt)*) => { { - $qvars.extend($outer.iter().map(|local| $crate::CastType::as_dyn(vcx!().mk_local_decl_local(local)))); - let $outer: Vec<$crate::ExprGen<_, _, _>> = $outer.iter().map(|local| vcx!().mk_local_ex_local(local)).collect(); + (@forall_qvars($qvars:ident); , ..[$outer_decls:ident] $($tokens:tt)*) => { { + $qvars.extend($outer_decls.clone()); $crate::expr_inner!(@forall_qvars($qvars); $($tokens)*) } }; (@forall_qvars($qvars:ident); , $qvar:ident : $qtype:tt $($tokens:tt)* ) => { { From 1d36e9dff707a23200a9c9c42659ed331f930a5f Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 28 Nov 2025 12:38:39 +0100 Subject: [PATCH 12/26] Run clippy --- prusti-encoder/src/encoders/ty/generics/args.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prusti-encoder/src/encoders/ty/generics/args.rs b/prusti-encoder/src/encoders/ty/generics/args.rs index c556c228d86..f64e37ec43b 100644 --- a/prusti-encoder/src/encoders/ty/generics/args.rs +++ b/prusti-encoder/src/encoders/ty/generics/args.rs @@ -1,4 +1,4 @@ -use prusti_rustc_interface::{middle::ty, span::def_id::DefId}; +use prusti_rustc_interface::middle::ty; use super::GParams; From 1f10be8fca23ab43908ca8f8c840a42d94585f17 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 28 Nov 2025 14:59:20 +0100 Subject: [PATCH 13/26] Make trait and impl support different number of parameters --- .../src/encoders/ty/generics/trait_impls.rs | 28 ++++++++----------- .../pass/traits/assoc_type_gen_trait.rs | 3 +- 2 files changed, 13 insertions(+), 18 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index 68d73b9c360..ef5ace2bd53 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -4,7 +4,7 @@ use vir::{CastType, Domain, vir_format_identifier}; use crate::encoders::ty::{ RustTyDecomposition, - generics::{GParams, GenericParamsEnc, traits::TraitEnc}, + generics::{GArgs, GArgsTyEnc, GParams, GenericParamsEnc, traits::TraitEnc}, }; pub struct TraitImplEnc; @@ -31,38 +31,32 @@ impl TaskEncoder for TraitImplEnc { ) -> EncodeFullResult<'vir, Self> { deps.emit_output_ref(*task_key, ())?; - let params = deps.require_dep::(GParams::from(task_key.0))?; - let trait_params = params.ty_exprs(); - vir::with_vcx(|vcx| { let tcx = vcx.tcx(); - let trait_did = tcx + + let params = deps.require_dep::(GParams::from(task_key.0))?; + + let trait_ref = tcx .impl_trait_ref(task_key.0) .unwrap() - .instantiate_identity() - .def_id; + .instantiate_identity(); + let trait_did = trait_ref.def_id; let trait_data = deps.require_dep::(trait_did)?; + let args = deps + .require_dep::(GArgs::new(GParams::from(task_key.0), trait_ref.args))?; + let mut axs = Vec::new(); let struct_ty = tcx.type_of(task_key.0).instantiate_identity(); - let struct_ty_expr = params.ty_expr( - deps, - RustTyDecomposition::from_ty(struct_ty, tcx, GParams::from(task_key.0)), - ); - - let mut vec = Vec::new(); - vec.push(struct_ty_expr); - vec.extend(trait_params.to_owned()); - let trait_tys = &vec; - let impl_fun = trait_data.impl_fun; let trait_ty_decls = params .ty_decls() .iter() .map(|dec| dec.upcast_ty()) .collect::>(); + let trait_tys = args.get_ty(); axs.push(vcx.mk_domain_axiom( vir_format_identifier!(vcx, "{}_impl_{}", trait_data.trait_name, struct_ty), vir::expr! {forall ..[trait_ty_decls] :: {[impl_fun(trait_tys)]} [impl_fun(trait_tys)]}, diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs index 28ff9b43b25..0759a5bae32 100644 --- a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs +++ b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs @@ -16,11 +16,12 @@ impl MyTrait for St1 { type SomeOtherType = T2; } -impl MyTrait for St2 { +impl MyTrait for St2 { type SomeType = u64; type SomeOtherType = T; } fn bar() { foo::(5.2, 6); + foo::(5, false); } From eb9ff51756bd8710671348570ca6b8a99ca5bf37 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 28 Nov 2025 15:09:23 +0100 Subject: [PATCH 14/26] Adapt test file --- .../pass/traits/assoc_type_gen_trait.rs | 30 ++++++++++++++----- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs index 0759a5bae32..7cc97c55df9 100644 --- a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs +++ b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs @@ -1,27 +1,41 @@ -fn foo, Z> (x: Y::SomeType, y: Y::SomeOtherType) { - +fn foo, Z> (x: Y::SomeType, y: Y::SomeOtherType, z: Y) { + let res: X = z.gen(); } trait MyTrait { type SomeType; type SomeOtherType; + + fn gen(self) -> T; } -struct St1{} -struct St2{} +struct St1{ + x: T +} +struct St2{ + y: T +} -impl MyTrait for St1 { +impl MyTrait for St1 { type SomeType = T; type SomeOtherType = T2; + + fn gen(self) -> T{ + self.x + } } -impl MyTrait for St2 { +impl MyTrait for St2 { type SomeType = u64; type SomeOtherType = T; + + fn gen(self) -> T{ + self.y + } } fn bar() { - foo::(5.2, 6); - foo::(5, false); + foo::, u32>(5.2, 6, St1 {x: 5.5}); + foo::, bool>(5, false, St2 {y: true}); } From 352b4ff4d0f1bf01733df5721806d77a7d31cbbb Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 28 Nov 2025 15:21:56 +0100 Subject: [PATCH 15/26] Adapt test file --- .../tests/verify/pass/traits/assoc_type_gen_trait.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs index 7cc97c55df9..f0290c37596 100644 --- a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs +++ b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs @@ -28,7 +28,7 @@ impl MyTrait for St1 { impl MyTrait for St2 { type SomeType = u64; - type SomeOtherType = T; + type SomeOtherType = SomeWrapper; fn gen(self) -> T{ self.y @@ -37,5 +37,9 @@ impl MyTrait for St2 { fn bar() { foo::, u32>(5.2, 6, St1 {x: 5.5}); - foo::, bool>(5, false, St2 {y: true}); + foo::, bool>(5, SomeWrapper {val: false}, St2 {y: true}); +} + +struct SomeWrapper { + val: T } From d58857986ecf19dcae9bc40ff3d99ac371d9a00b Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Tue, 2 Dec 2025 11:42:11 +0100 Subject: [PATCH 16/26] Fix cycle issue for simple test cases --- .../src/encoders/ty/generics/trait_impls.rs | 35 +++++++++++++++---- 1 file changed, 29 insertions(+), 6 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index ef5ace2bd53..32f1a4956f4 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -43,8 +43,22 @@ impl TaskEncoder for TraitImplEnc { let trait_did = trait_ref.def_id; let trait_data = deps.require_dep::(trait_did)?; - let args = deps - .require_dep::(GArgs::new(GParams::from(task_key.0), trait_ref.args))?; + // for some reason, just using all args (which includes the struct at index 0) + // leads to a cycle for simple test cases -> split up and add struct manually + let args = deps.require_dep::(GArgs::new( + GParams::from(task_key.0), + &trait_ref.args[1..], + ))?; + + let struct_ty = tcx.type_of(task_key.0).instantiate_identity(); + let struct_ty_expr = params.ty_expr( + deps, + RustTyDecomposition::from_ty(struct_ty, tcx, GParams::from(task_key.0)), + ); + + let mut vec = Vec::new(); + vec.push(struct_ty_expr); + vec.append(&mut args.get_ty().to_owned()); let mut axs = Vec::new(); @@ -56,10 +70,15 @@ impl TaskEncoder for TraitImplEnc { .iter() .map(|dec| dec.upcast_ty()) .collect::>(); - let trait_tys = args.get_ty(); - axs.push(vcx.mk_domain_axiom( + let trait_tys = vcx.alloc_slice(&vec); + axs.push( + vcx.mk_domain_axiom( vir_format_identifier!(vcx, "{}_impl_{}", trait_data.trait_name, struct_ty), - vir::expr! {forall ..[trait_ty_decls] :: {[impl_fun(trait_tys)]} [impl_fun(trait_tys)]}, + if trait_ty_decls.is_empty() { + vir::expr! {[impl_fun(trait_tys)]} + } else { + vir::expr! {forall ..[trait_ty_decls] :: {[impl_fun(trait_tys)]} [impl_fun(trait_tys)]} + } )); tcx.associated_items(task_key.0) @@ -90,7 +109,11 @@ impl TaskEncoder for TraitImplEnc { tcx.item_name(impl_item.def_id), struct_ty ), - vir::expr! {forall ..[trait_ty_decls] :: {[assoc_fun(trait_tys)]} ([assoc_fun(trait_tys)]) == (assoc_type_expr)}, + if trait_ty_decls.is_empty() { + vir::expr! {([assoc_fun(trait_tys)]) == (assoc_type_expr)} + } else { + vir::expr! {forall ..[trait_ty_decls] :: {[assoc_fun(trait_tys)]} ([assoc_fun(trait_tys)]) == (assoc_type_expr)} + } )) }); }); From 1f5b71afba895da05c586531759894edc811a06e Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 5 Dec 2025 10:50:16 +0100 Subject: [PATCH 17/26] Allow associated types to be generic --- .../src/encoders/ty/generics/params.rs | 15 +++++-- .../src/encoders/ty/generics/trait_impls.rs | 31 +++++++++++-- .../src/encoders/ty/generics/traits.rs | 5 ++- .../pass/traits/assoc_type_gen_assoc.rs | 23 ++++++++++ .../traits/assoc_type_gen_trait_gen_assoc.rs | 45 +++++++++++++++++++ .../verify/pass/traits/gen_assoc_type.rs | 27 +++++++++++ 6 files changed, 139 insertions(+), 7 deletions(-) create mode 100644 prusti-tests/tests/verify/pass/traits/assoc_type_gen_assoc.rs create mode 100644 prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait_gen_assoc.rs create mode 100644 prusti-tests/tests/verify/pass/traits/gen_assoc_type.rs diff --git a/prusti-encoder/src/encoders/ty/generics/params.rs b/prusti-encoder/src/encoders/ty/generics/params.rs index 89e1bfabb7b..ae2605318e7 100644 --- a/prusti-encoder/src/encoders/ty/generics/params.rs +++ b/prusti-encoder/src/encoders/ty/generics/params.rs @@ -16,6 +16,7 @@ use crate::encoders::{ data::TySpecifics, generics::{GArgsTyEnc, GParamVariant, traits::TraitEnc}, lifted::TyConstructorEnc, + pure::TyPureEnc, }, }; @@ -281,9 +282,17 @@ impl<'vir> GenericParams<'vir> { .args .iter() .map(|arg| { - self.ty_exprs[self - .map_idx(expect_param(arg.expect_ty().kind()).index) - .unwrap()] + match arg.expect_ty().kind() { + TyKind::Param(p) => self.ty_exprs[self.map_idx(p.index).unwrap()], + _ => self.ty_expr( + deps, + RustTyDecomposition::from_ty( + arg.expect_ty(), + tcx, + ty.args.context, + ), + ), + } }) .collect::>(); (assoc_funs[0])(tys) diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index 32f1a4956f4..ee7c68a2f5f 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -1,3 +1,5 @@ +use std::any::Any; + use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; use vir::{CastType, Domain, vir_format_identifier}; @@ -90,10 +92,18 @@ impl TaskEncoder for TraitImplEnc { .iter() .filter(|(assoc_did, _)| Some(*assoc_did) == impl_item.trait_item_def_id) .for_each(|(_, assoc_fun)| { - let params = deps + // construct arguments for assoc_item function + // parameters of the trait are substituted + // by the arguments used in the impl + // parameters of the associated type are kept + + // parameters of assoc item include already substituted arguments + let assoc_params = deps .require_dep::(GParams::from(impl_item.def_id)) .unwrap(); - let assoc_type_expr = params.ty_expr( + + // the type we want to resolve the type alias to + let assoc_type_expr = assoc_params.ty_expr( deps, RustTyDecomposition::from_ty( tcx.type_of(impl_item.def_id).instantiate_identity(), @@ -101,6 +111,21 @@ impl TaskEncoder for TraitImplEnc { GParams::from(impl_item.def_id), ), ); + let assoc_decls = assoc_params + .ty_decls() + .iter() + .map(|dec| dec.upcast_ty()) + .collect::>(); + + // Combine substituted trait params with the params of the associated type + let mut trait_ty_decls = trait_ty_decls.clone(); + trait_ty_decls.extend_from_slice(&assoc_decls[params.ty_exprs().len()..]); + + // Combine substituted trait params decls with the params of the associated type + let mut vec = vec.clone(); + vec.extend_from_slice(&assoc_params.ty_exprs()[params.ty_exprs().len()..]); + let trait_tys = vcx.alloc_slice(&vec); + axs.push(vcx.mk_domain_axiom( vir_format_identifier!( vcx, @@ -114,7 +139,7 @@ impl TaskEncoder for TraitImplEnc { } else { vir::expr! {forall ..[trait_ty_decls] :: {[assoc_fun(trait_tys)]} ([assoc_fun(trait_tys)]) == (assoc_type_expr)} } - )) + )); }); }); diff --git a/prusti-encoder/src/encoders/ty/generics/traits.rs b/prusti-encoder/src/encoders/ty/generics/traits.rs index fc6e2b187fc..6af37519d6a 100644 --- a/prusti-encoder/src/encoders/ty/generics/traits.rs +++ b/prusti-encoder/src/encoders/ty/generics/traits.rs @@ -45,6 +45,9 @@ impl TaskEncoder for TraitEnc { .in_definition_order() .filter(|item| matches!(item.kind, AssocKind::Type { data: _ })) .map(|item| { + let params_type = deps + .require_dep::(GParams::from(item.def_id)) + .unwrap(); ( item.def_id, FunctionIdn::new( @@ -54,7 +57,7 @@ impl TaskEncoder for TraitEnc { trait_name, tcx.item_name(item.def_id), ), - vcx.alloc_slice(&(vec![vir::TYPE_TYVAL; params.ty_exprs().len()])), + vcx.alloc_slice(&(vec![vir::TYPE_TYVAL; params_type.ty_exprs().len()])), // params_type also includes parameters of trait itself vir::TYPE_TYVAL, ), ) diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_assoc.rs b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_assoc.rs new file mode 100644 index 00000000000..fb72bd7dec7 --- /dev/null +++ b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_assoc.rs @@ -0,0 +1,23 @@ + +fn foo (x: Y::SomeType) { + +} + +trait MyTrait { + type SomeType; +} + +struct St1{} +struct St2{} + +impl MyTrait for St1 { + type SomeType = X; +} + +impl MyTrait for St2 { + type SomeType = u64; +} + +fn bar() { + foo::(5); +} diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait_gen_assoc.rs b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait_gen_assoc.rs new file mode 100644 index 00000000000..3b508b90a14 --- /dev/null +++ b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait_gen_assoc.rs @@ -0,0 +1,45 @@ + +fn foo, Z> (x: Y::SomeType>, y: Y::SomeOtherType, z: Y) { + let res: X = z.gen(); +} + +trait MyTrait { + type SomeType; + type SomeOtherType; + + fn gen(self) -> T; +} + +struct St1{ + x: T +} +struct St2{ + y: T +} + +impl MyTrait for St1 { + type SomeType = A; + type SomeOtherType = T2; + + fn gen(self) -> T{ + self.x + } +} + +impl MyTrait for St2 { + type SomeType = T; + type SomeOtherType = SomeWrapper; + + fn gen(self) -> T{ + self.y + } +} + +fn bar() { + foo::, u32>(SomeWrapper {val: 5.5}, 6, St1 {x: 5.5}); + foo::, bool>(true, SomeWrapper {val: false}, St2 {y: true}); +} + +struct SomeWrapper { + val: T +} diff --git a/prusti-tests/tests/verify/pass/traits/gen_assoc_type.rs b/prusti-tests/tests/verify/pass/traits/gen_assoc_type.rs new file mode 100644 index 00000000000..b0bb7f130e8 --- /dev/null +++ b/prusti-tests/tests/verify/pass/traits/gen_assoc_type.rs @@ -0,0 +1,27 @@ + +fn foo (x: Y::SomeType) { + +} + +trait MyTrait { + type SomeType; +} + +struct St1{} +struct St2{} + +impl MyTrait for St1 { + type SomeType = SomeWrapper; +} + +impl MyTrait for St2 { + type SomeType = u64; +} + +fn bar() { + foo::(SomeWrapper {val: 5}); +} + +struct SomeWrapper { + val: T +} From 970de0532768f07012404ccd6ec4285d67c948b1 Mon Sep 17 00:00:00 2001 From: --global <--global> Date: Fri, 5 Dec 2025 15:12:54 +0100 Subject: [PATCH 18/26] Run clippy --- prusti-encoder/src/encoders/ty/generics/params.rs | 10 +--------- prusti-encoder/src/encoders/ty/generics/trait_impls.rs | 1 - 2 files changed, 1 insertion(+), 10 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/params.rs b/prusti-encoder/src/encoders/ty/generics/params.rs index ae2605318e7..1263488dc0d 100644 --- a/prusti-encoder/src/encoders/ty/generics/params.rs +++ b/prusti-encoder/src/encoders/ty/generics/params.rs @@ -2,7 +2,7 @@ use prusti_interface::specs::typed::ExternSpecKind; use prusti_rustc_interface::{ middle::{ ty, - ty::{ParamTy, TyKind}, + ty::TyKind, }, span::{def_id::DefId, symbol}, }; @@ -16,7 +16,6 @@ use crate::encoders::{ data::TySpecifics, generics::{GArgsTyEnc, GParamVariant, traits::TraitEnc}, lifted::TyConstructorEnc, - pure::TyPureEnc, }, }; @@ -180,13 +179,6 @@ impl<'vir> From for GParams<'vir> { } } -fn expect_param(kind: &TyKind) -> ParamTy { - match kind { - TyKind::Param(p) => *p, - _ => unreachable!(), - } -} - /// Handles everything relating to the encoding of generic parameters (both for /// Rust functions and type definitions). Used to turn e.g. the Rust function /// `fn foo(x: U)` into the Viper `method foo(x: Ref, T: Type, U: Type)` diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index ee7c68a2f5f..c325f8ce7d1 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -1,4 +1,3 @@ -use std::any::Any; use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; From 0ec6d6fbc788267ef478c70fecc5c611b9c5f712 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 5 Dec 2025 16:57:02 +0100 Subject: [PATCH 19/26] Generate domains for all implementations of traits (even for primitive datatypes) --- prusti-encoder/src/encoders/mir_fn/mod.rs | 17 +++++++++- .../src/encoders/ty/generics/params.rs | 23 ++++--------- .../src/encoders/ty/generics/trait_impls.rs | 33 ++++++++----------- .../src/encoders/ty/kinds/enumlike.rs | 8 ----- .../src/encoders/ty/kinds/structlike.rs | 30 +---------------- .../verify/pass/traits/primitive_impl.rs | 17 ++++++++++ 6 files changed, 54 insertions(+), 74 deletions(-) create mode 100644 prusti-tests/tests/verify/pass/traits/primitive_impl.rs diff --git a/prusti-encoder/src/encoders/mir_fn/mod.rs b/prusti-encoder/src/encoders/mir_fn/mod.rs index ba9d492bc79..9e99f6d08b3 100644 --- a/prusti-encoder/src/encoders/mir_fn/mod.rs +++ b/prusti-encoder/src/encoders/mir_fn/mod.rs @@ -6,7 +6,7 @@ pub use function::*; pub use method::*; pub use signature::*; -use crate::encoders::ty::generics::{GArgs, GParams}; +use crate::encoders::ty::generics::{GArgs, GParams, trait_impls::TraitImplEnc}; use prusti_interface::specs::specifications::SpecQuery; use prusti_rustc_interface::{hir, middle::ty, span::def_id::DefId}; @@ -61,4 +61,19 @@ pub fn encode_all_in_crate<'tcx>(tcx: ty::TyCtxt<'tcx>) { } } } + + for def_id in tcx.hir_crate_items(()).definitions() { + if let hir::def::DefKind::Impl { of_trait: true } = tcx.def_kind(def_id) { + TraitImplEnc::encode(def_id.to_def_id(), false).unwrap(); + } + } + + // for trait_id in tcx.visible_traits() { + // for impl_id in tcx.all_impls(trait_id) { + // { + // TraitImplEnc::encode(impl_id, false).unwrap(); + // } + + // } + // } } diff --git a/prusti-encoder/src/encoders/ty/generics/params.rs b/prusti-encoder/src/encoders/ty/generics/params.rs index 1263488dc0d..09376c752ab 100644 --- a/prusti-encoder/src/encoders/ty/generics/params.rs +++ b/prusti-encoder/src/encoders/ty/generics/params.rs @@ -1,9 +1,6 @@ use prusti_interface::specs::typed::ExternSpecKind; use prusti_rustc_interface::{ - middle::{ - ty, - ty::TyKind, - }, + middle::{ty, ty::TyKind}, span::{def_id::DefId, symbol}, }; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; @@ -273,18 +270,12 @@ impl<'vir> GenericParams<'vir> { let tys = &a .args .iter() - .map(|arg| { - match arg.expect_ty().kind() { - TyKind::Param(p) => self.ty_exprs[self.map_idx(p.index).unwrap()], - _ => self.ty_expr( - deps, - RustTyDecomposition::from_ty( - arg.expect_ty(), - tcx, - ty.args.context, - ), - ), - } + .map(|arg| match arg.expect_ty().kind() { + TyKind::Param(p) => self.ty_exprs[self.map_idx(p.index).unwrap()], + _ => self.ty_expr( + deps, + RustTyDecomposition::from_ty(arg.expect_ty(), tcx, ty.args.context), + ), }) .collect::>(); (assoc_funs[0])(tys) diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index c325f8ce7d1..94ec0a787eb 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -1,4 +1,3 @@ - use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; use vir::{CastType, Domain, vir_format_identifier}; @@ -23,7 +22,7 @@ impl TaskEncoder for TraitImplEnc { } } - type TaskDescription<'vir> = (DefId, GParams<'vir>); + type TaskDescription<'vir> = DefId; type OutputFullLocal<'vir> = Domain<'vir>; fn do_encode_full<'vir>( @@ -35,27 +34,21 @@ impl TaskEncoder for TraitImplEnc { vir::with_vcx(|vcx| { let tcx = vcx.tcx(); - let params = deps.require_dep::(GParams::from(task_key.0))?; + let ctx = GParams::from(*task_key); + + let params = deps.require_dep::(ctx)?; - let trait_ref = tcx - .impl_trait_ref(task_key.0) - .unwrap() - .instantiate_identity(); + let trait_ref = tcx.impl_trait_ref(task_key).unwrap().instantiate_identity(); let trait_did = trait_ref.def_id; let trait_data = deps.require_dep::(trait_did)?; // for some reason, just using all args (which includes the struct at index 0) // leads to a cycle for simple test cases -> split up and add struct manually - let args = deps.require_dep::(GArgs::new( - GParams::from(task_key.0), - &trait_ref.args[1..], - ))?; - - let struct_ty = tcx.type_of(task_key.0).instantiate_identity(); - let struct_ty_expr = params.ty_expr( - deps, - RustTyDecomposition::from_ty(struct_ty, tcx, GParams::from(task_key.0)), - ); + let args = deps.require_dep::(GArgs::new(ctx, &trait_ref.args[1..]))?; + + let struct_ty = tcx.type_of(task_key).instantiate_identity(); + let struct_ty_expr = + params.ty_expr(deps, RustTyDecomposition::from_ty(struct_ty, tcx, ctx)); let mut vec = Vec::new(); vec.push(struct_ty_expr); @@ -63,7 +56,7 @@ impl TaskEncoder for TraitImplEnc { let mut axs = Vec::new(); - let struct_ty = tcx.type_of(task_key.0).instantiate_identity(); + let struct_ty = tcx.type_of(task_key).instantiate_identity(); let impl_fun = trait_data.impl_fun; let trait_ty_decls = params @@ -82,7 +75,7 @@ impl TaskEncoder for TraitImplEnc { } )); - tcx.associated_items(task_key.0) + tcx.associated_items(*task_key) .in_definition_order() .filter(|item| matches!(item.kind, AssocKind::Type { data: _ })) .for_each(|impl_item| { @@ -147,7 +140,7 @@ impl TaskEncoder for TraitImplEnc { vcx, "t_{}_{}", trait_data.trait_name, - tcx.type_of(task_key.0).instantiate_identity().to_string() + tcx.type_of(*task_key).instantiate_identity().to_string() ), &[], vcx.alloc_slice(&axs), diff --git a/prusti-encoder/src/encoders/ty/kinds/enumlike.rs b/prusti-encoder/src/encoders/ty/kinds/enumlike.rs index 5e43ddda951..3c840d9c928 100644 --- a/prusti-encoder/src/encoders/ty/kinds/enumlike.rs +++ b/prusti-encoder/src/encoders/ty/kinds/enumlike.rs @@ -19,10 +19,6 @@ pub(crate) fn ty_pure<'vir>( deps: &mut TaskEncoderDependencies<'vir, TyPureEnc>, builder: &mut AdtBuilder<'vir>, ) -> Result, EncodeFullError<'vir, TyPureEnc>> { - if let Some(d) = data.did { - super::structlike::generate_axioms_for_impls(d, deps)?; - } - let discr_ty = deps.require_dep::(RustTyDecomposition::from_prim_ty(data.discr).ty)?; let discr_prim = discr_ty.expect_primitive(); @@ -74,10 +70,6 @@ pub(crate) fn ty_impure<'vir>( deps: &mut TaskEncoderDependencies<'vir, TyImpureEnc>, builder: &mut PredicateBuilder<'vir>, ) -> Result, EncodeFullError<'vir, TyImpureEnc>> { - if let Some(d) = data.did { - super::structlike::generate_axioms_for_impls(d, deps)?; - } - let ref_self_decl = builder.ref_self_decl(); let ref_self = builder.vcx.mk_local_ex(ref_self_decl); diff --git a/prusti-encoder/src/encoders/ty/kinds/structlike.rs b/prusti-encoder/src/encoders/ty/kinds/structlike.rs index d425e9eaad0..df104405e68 100644 --- a/prusti-encoder/src/encoders/ty/kinds/structlike.rs +++ b/prusti-encoder/src/encoders/ty/kinds/structlike.rs @@ -3,17 +3,14 @@ use crate::encoders::{ ty::{ RustTyDatas, data::{StructData, TyData}, - generics::{GParams, trait_impls::TraitImplEnc}, impure::{ImpureTyDatas, PredicateBuilder, TyImpureEnc, TyImpureFieldData}, pure::{AdtBuilder, PureTyDatas, TyPureEnc, TyPureFieldData, TyPureStructData}, use_pure::TyUsePureEnc, }, }; -use task_encoder::{EncodeFullError, TaskEncoder, TaskEncoderDependencies}; +use task_encoder::{EncodeFullError, TaskEncoderDependencies}; use vir::{CastType, HasType, PredicateIdn}; -use prusti_rustc_interface::span::def_id::DefId; - pub(crate) fn ty_pure<'vir>( task_key: &TyData<'vir, RustTyDatas>, data: &StructData<'vir, RustTyDatas>, @@ -23,25 +20,6 @@ pub(crate) fn ty_pure<'vir>( ty_pure_variant("", None, task_key, data, deps, builder) } -pub(super) fn generate_axioms_for_impls<'vir, E: TaskEncoder + 'vir + ?Sized>( - did: DefId, - deps: &mut TaskEncoderDependencies<'vir, E>, -) -> Result<(), EncodeFullError<'vir, E>> { - vir::with_vcx(|vcx| { - let tcx = vcx.tcx(); - for trait_id in tcx.visible_traits() { - for impl_id in tcx.all_impls(trait_id) { - if tcx.type_of(impl_id).instantiate_identity() - == tcx.type_of(did).instantiate_identity() - { - deps.require_dep::((impl_id, GParams::empty()))?; - } - } - } - Ok(()) - }) -} - pub(super) fn ty_pure_variant<'vir>( prefix: &str, discr: Option>, @@ -50,9 +28,6 @@ pub(super) fn ty_pure_variant<'vir>( deps: &mut TaskEncoderDependencies<'vir, TyPureEnc>, builder: &mut AdtBuilder<'vir>, ) -> Result, EncodeFullError<'vir, TyPureEnc>> { - if let Some(d) = data.did { - generate_axioms_for_impls(d, deps)?; - } let field_tys = data .fields .iter() @@ -121,9 +96,6 @@ pub(crate) fn ty_impure_variant<'vir>( deps: &mut TaskEncoderDependencies<'vir, TyImpureEnc>, builder: &mut PredicateBuilder<'vir>, ) -> Result, EncodeFullError<'vir, TyImpureEnc>> { - if let Some(d) = data.did { - generate_axioms_for_impls(d, deps)?; - } let fields = data .fields .iter() diff --git a/prusti-tests/tests/verify/pass/traits/primitive_impl.rs b/prusti-tests/tests/verify/pass/traits/primitive_impl.rs new file mode 100644 index 00000000000..b0ad4285167 --- /dev/null +++ b/prusti-tests/tests/verify/pass/traits/primitive_impl.rs @@ -0,0 +1,17 @@ +fn foo> (x: Y::SomeOtherType) { + +} + +trait SomeTrait { + type SomeType; + type SomeOtherType; +} + +impl SomeTrait for u32 { + type SomeType = X; + type SomeOtherType = Y; +} + +fn bar() { + foo::(5); +} \ No newline at end of file From 060201a6105fc54ce79e3e573f651a5e61babd73 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Mon, 8 Dec 2025 14:22:51 +0100 Subject: [PATCH 20/26] Run fmt on tests --- .../tests/verify/pass/traits/assoc_type.rs | 9 +++----- .../pass/traits/assoc_type_gen_assoc.rs | 9 +++----- .../pass/traits/assoc_type_gen_trait.rs | 21 +++++++++---------- .../traits/assoc_type_gen_trait_gen_assoc.rs | 21 +++++++++---------- .../verify/pass/traits/gen_assoc_type.rs | 13 +++++------- .../verify/pass/traits/primitive_impl.rs | 8 +++---- 6 files changed, 34 insertions(+), 47 deletions(-) diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type.rs b/prusti-tests/tests/verify/pass/traits/assoc_type.rs index 0f8501ebf58..de09a75b58a 100644 --- a/prusti-tests/tests/verify/pass/traits/assoc_type.rs +++ b/prusti-tests/tests/verify/pass/traits/assoc_type.rs @@ -1,14 +1,11 @@ - -fn foo (x: Y::SomeType) { - -} +fn foo(x: Y::SomeType) {} trait MyTrait { type SomeType; } -struct St1{} -struct St2{} +struct St1 {} +struct St2 {} impl MyTrait for St1 { type SomeType = u32; diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_assoc.rs b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_assoc.rs index fb72bd7dec7..9e7c2e55957 100644 --- a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_assoc.rs +++ b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_assoc.rs @@ -1,14 +1,11 @@ - -fn foo (x: Y::SomeType) { - -} +fn foo(x: Y::SomeType) {} trait MyTrait { type SomeType; } -struct St1{} -struct St2{} +struct St1 {} +struct St2 {} impl MyTrait for St1 { type SomeType = X; diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs index f0290c37596..d50084655d0 100644 --- a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs +++ b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait.rs @@ -1,5 +1,4 @@ - -fn foo, Z> (x: Y::SomeType, y: Y::SomeOtherType, z: Y) { +fn foo, Z>(x: Y::SomeType, y: Y::SomeOtherType, z: Y) { let res: X = z.gen(); } @@ -10,18 +9,18 @@ trait MyTrait { fn gen(self) -> T; } -struct St1{ - x: T +struct St1 { + x: T, } -struct St2{ - y: T +struct St2 { + y: T, } impl MyTrait for St1 { type SomeType = T; type SomeOtherType = T2; - fn gen(self) -> T{ + fn gen(self) -> T { self.x } } @@ -30,16 +29,16 @@ impl MyTrait for St2 { type SomeType = u64; type SomeOtherType = SomeWrapper; - fn gen(self) -> T{ + fn gen(self) -> T { self.y } } fn bar() { - foo::, u32>(5.2, 6, St1 {x: 5.5}); - foo::, bool>(5, SomeWrapper {val: false}, St2 {y: true}); + foo::, u32>(5.2, 6, St1 { x: 5.5 }); + foo::, bool>(5, SomeWrapper { val: false }, St2 { y: true }); } struct SomeWrapper { - val: T + val: T, } diff --git a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait_gen_assoc.rs b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait_gen_assoc.rs index 3b508b90a14..67e3365e2ba 100644 --- a/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait_gen_assoc.rs +++ b/prusti-tests/tests/verify/pass/traits/assoc_type_gen_trait_gen_assoc.rs @@ -1,5 +1,4 @@ - -fn foo, Z> (x: Y::SomeType>, y: Y::SomeOtherType, z: Y) { +fn foo, Z>(x: Y::SomeType>, y: Y::SomeOtherType, z: Y) { let res: X = z.gen(); } @@ -10,18 +9,18 @@ trait MyTrait { fn gen(self) -> T; } -struct St1{ - x: T +struct St1 { + x: T, } -struct St2{ - y: T +struct St2 { + y: T, } impl MyTrait for St1 { type SomeType = A; type SomeOtherType = T2; - fn gen(self) -> T{ + fn gen(self) -> T { self.x } } @@ -30,16 +29,16 @@ impl MyTrait for St2 { type SomeType = T; type SomeOtherType = SomeWrapper; - fn gen(self) -> T{ + fn gen(self) -> T { self.y } } fn bar() { - foo::, u32>(SomeWrapper {val: 5.5}, 6, St1 {x: 5.5}); - foo::, bool>(true, SomeWrapper {val: false}, St2 {y: true}); + foo::, u32>(SomeWrapper { val: 5.5 }, 6, St1 { x: 5.5 }); + foo::, bool>(true, SomeWrapper { val: false }, St2 { y: true }); } struct SomeWrapper { - val: T + val: T, } diff --git a/prusti-tests/tests/verify/pass/traits/gen_assoc_type.rs b/prusti-tests/tests/verify/pass/traits/gen_assoc_type.rs index b0bb7f130e8..058e84bbe50 100644 --- a/prusti-tests/tests/verify/pass/traits/gen_assoc_type.rs +++ b/prusti-tests/tests/verify/pass/traits/gen_assoc_type.rs @@ -1,14 +1,11 @@ - -fn foo (x: Y::SomeType) { - -} +fn foo(x: Y::SomeType) {} trait MyTrait { type SomeType; } -struct St1{} -struct St2{} +struct St1 {} +struct St2 {} impl MyTrait for St1 { type SomeType = SomeWrapper; @@ -19,9 +16,9 @@ impl MyTrait for St2 { } fn bar() { - foo::(SomeWrapper {val: 5}); + foo::(SomeWrapper { val: 5 }); } struct SomeWrapper { - val: T + val: T, } diff --git a/prusti-tests/tests/verify/pass/traits/primitive_impl.rs b/prusti-tests/tests/verify/pass/traits/primitive_impl.rs index b0ad4285167..a17a87abe4c 100644 --- a/prusti-tests/tests/verify/pass/traits/primitive_impl.rs +++ b/prusti-tests/tests/verify/pass/traits/primitive_impl.rs @@ -1,6 +1,4 @@ -fn foo> (x: Y::SomeOtherType) { - -} +fn foo>(x: Y::SomeOtherType) {} trait SomeTrait { type SomeType; @@ -10,8 +8,8 @@ trait SomeTrait { impl SomeTrait for u32 { type SomeType = X; type SomeOtherType = Y; -} +} fn bar() { foo::(5); -} \ No newline at end of file +} From 81885ab05d29cdf8eafebb8b1188db9a6c079d08 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Mon, 8 Dec 2025 14:33:16 +0100 Subject: [PATCH 21/26] Implement PR feedback --- .../src/encoders/ty/generics/trait_impls.rs | 27 ++++++++++--------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index 94ec0a787eb..36ed185090c 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -135,20 +135,21 @@ impl TaskEncoder for TraitImplEnc { }); }); - let dom = vcx.mk_domain( - vir_format_identifier!( - vcx, - "t_{}_{}", - trait_data.trait_name, - tcx.type_of(*task_key).instantiate_identity().to_string() + Ok(( + vcx.mk_domain( + vir_format_identifier!( + vcx, + "t_{}_{}", + trait_data.trait_name, + tcx.type_of(*task_key).instantiate_identity().to_string() + ), + &[], + vcx.alloc_slice(&axs), + &[], + None, ), - &[], - vcx.alloc_slice(&axs), - &[], - None, - ); - - Ok((dom, ())) + (), + )) }) } } From 0b21b463ca4422ea529c01ebed6d59be02108066 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Mon, 8 Dec 2025 15:17:28 +0100 Subject: [PATCH 22/26] use iterator chain instead of vec --- .../src/encoders/ty/generics/trait_impls.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index 36ed185090c..eb55963bff1 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -1,3 +1,5 @@ +use std::iter; + use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; use vir::{CastType, Domain, vir_format_identifier}; @@ -50,10 +52,6 @@ impl TaskEncoder for TraitImplEnc { let struct_ty_expr = params.ty_expr(deps, RustTyDecomposition::from_ty(struct_ty, tcx, ctx)); - let mut vec = Vec::new(); - vec.push(struct_ty_expr); - vec.append(&mut args.get_ty().to_owned()); - let mut axs = Vec::new(); let struct_ty = tcx.type_of(task_key).instantiate_identity(); @@ -64,7 +62,11 @@ impl TaskEncoder for TraitImplEnc { .iter() .map(|dec| dec.upcast_ty()) .collect::>(); - let trait_tys = vcx.alloc_slice(&vec); + let trait_tys = vcx.alloc_slice( + &iter::once(struct_ty_expr) + .chain(args.get_ty().to_owned()) + .collect::>(), + ); axs.push( vcx.mk_domain_axiom( vir_format_identifier!(vcx, "{}_impl_{}", trait_data.trait_name, struct_ty), @@ -113,10 +115,8 @@ impl TaskEncoder for TraitImplEnc { let mut trait_ty_decls = trait_ty_decls.clone(); trait_ty_decls.extend_from_slice(&assoc_decls[params.ty_exprs().len()..]); - // Combine substituted trait params decls with the params of the associated type - let mut vec = vec.clone(); - vec.extend_from_slice(&assoc_params.ty_exprs()[params.ty_exprs().len()..]); - let trait_tys = vcx.alloc_slice(&vec); + // Combine substituted trait params with the params of the associated type + let trait_tys = vcx.alloc_slice(&iter::once(struct_ty_expr).chain(args.get_ty().to_owned()).chain(assoc_params.ty_exprs()[params.ty_exprs().len()..].to_owned()).collect::>()); axs.push(vcx.mk_domain_axiom( vir_format_identifier!( From d71b2a29679f42b5943835d74b5ec561f4920184 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Mon, 8 Dec 2025 15:25:14 +0100 Subject: [PATCH 23/26] Implement feedback from PR --- .../src/encoders/ty/generics/trait_impls.rs | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index eb55963bff1..6b3e904189f 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -69,13 +69,10 @@ impl TaskEncoder for TraitImplEnc { ); axs.push( vcx.mk_domain_axiom( - vir_format_identifier!(vcx, "{}_impl_{}", trait_data.trait_name, struct_ty), - if trait_ty_decls.is_empty() { - vir::expr! {[impl_fun(trait_tys)]} - } else { + vir_format_identifier!(vcx, "{}_impl_{}", trait_data.trait_name, struct_ty), vir::expr! {forall ..[trait_ty_decls] :: {[impl_fun(trait_tys)]} [impl_fun(trait_tys)]} - } - )); + ) + ); tcx.associated_items(*task_key) .in_definition_order() @@ -126,11 +123,7 @@ impl TaskEncoder for TraitImplEnc { tcx.item_name(impl_item.def_id), struct_ty ), - if trait_ty_decls.is_empty() { - vir::expr! {([assoc_fun(trait_tys)]) == (assoc_type_expr)} - } else { - vir::expr! {forall ..[trait_ty_decls] :: {[assoc_fun(trait_tys)]} ([assoc_fun(trait_tys)]) == (assoc_type_expr)} - } + vir::expr! {forall ..[trait_ty_decls] :: {[assoc_fun(trait_tys)]} ([assoc_fun(trait_tys)]) == (assoc_type_expr)} )); }); }); From 3e1b4b4fc39edc6dad0bd29af348f0893fd10b38 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Mon, 8 Dec 2025 15:53:18 +0100 Subject: [PATCH 24/26] Use HashMap instead of slice of pairs --- .../src/encoders/ty/generics/params.rs | 9 +- .../src/encoders/ty/generics/trait_impls.rs | 89 +++++++++---------- .../src/encoders/ty/generics/traits.rs | 16 ++-- 3 files changed, 52 insertions(+), 62 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/generics/params.rs b/prusti-encoder/src/encoders/ty/generics/params.rs index 09376c752ab..4061df1d525 100644 --- a/prusti-encoder/src/encoders/ty/generics/params.rs +++ b/prusti-encoder/src/encoders/ty/generics/params.rs @@ -260,13 +260,6 @@ impl<'vir> GenericParams<'vir> { let tcx = vcx.tcx(); let trait_did = tcx.associated_item(a.def_id).container_id(tcx); let trait_data = deps.require_dep::(trait_did).unwrap(); - let assoc_funs = trait_data - .type_did_fun_mapping - .iter() - .filter(|(assoc_did, _)| *assoc_did == a.def_id) - .map(|(_, assoc_fun)| assoc_fun) - .collect::>(); - assert!(assoc_funs.len() == 1); let tys = &a .args .iter() @@ -278,7 +271,7 @@ impl<'vir> GenericParams<'vir> { ), }) .collect::>(); - (assoc_funs[0])(tys) + (trait_data.type_did_fun_mapping.get(&a.def_id).unwrap())(tys) }), }; } diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index 6b3e904189f..da29367bd46 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -78,54 +78,49 @@ impl TaskEncoder for TraitImplEnc { .in_definition_order() .filter(|item| matches!(item.kind, AssocKind::Type { data: _ })) .for_each(|impl_item| { - trait_data - .type_did_fun_mapping + let assoc_fun = trait_data.type_did_fun_mapping.get(&impl_item.trait_item_def_id.unwrap()).unwrap(); + // construct arguments for assoc_item function + // parameters of the trait are substituted + // by the arguments used in the impl + // parameters of the associated type are kept + + // parameters of assoc item include already substituted arguments + let assoc_params = deps + .require_dep::(GParams::from(impl_item.def_id)) + .unwrap(); + + // the type we want to resolve the type alias to + let assoc_type_expr = assoc_params.ty_expr( + deps, + RustTyDecomposition::from_ty( + tcx.type_of(impl_item.def_id).instantiate_identity(), + tcx, + GParams::from(impl_item.def_id), + ), + ); + let assoc_decls = assoc_params + .ty_decls() .iter() - .filter(|(assoc_did, _)| Some(*assoc_did) == impl_item.trait_item_def_id) - .for_each(|(_, assoc_fun)| { - // construct arguments for assoc_item function - // parameters of the trait are substituted - // by the arguments used in the impl - // parameters of the associated type are kept - - // parameters of assoc item include already substituted arguments - let assoc_params = deps - .require_dep::(GParams::from(impl_item.def_id)) - .unwrap(); - - // the type we want to resolve the type alias to - let assoc_type_expr = assoc_params.ty_expr( - deps, - RustTyDecomposition::from_ty( - tcx.type_of(impl_item.def_id).instantiate_identity(), - tcx, - GParams::from(impl_item.def_id), - ), - ); - let assoc_decls = assoc_params - .ty_decls() - .iter() - .map(|dec| dec.upcast_ty()) - .collect::>(); - - // Combine substituted trait params with the params of the associated type - let mut trait_ty_decls = trait_ty_decls.clone(); - trait_ty_decls.extend_from_slice(&assoc_decls[params.ty_exprs().len()..]); - - // Combine substituted trait params with the params of the associated type - let trait_tys = vcx.alloc_slice(&iter::once(struct_ty_expr).chain(args.get_ty().to_owned()).chain(assoc_params.ty_exprs()[params.ty_exprs().len()..].to_owned()).collect::>()); - - axs.push(vcx.mk_domain_axiom( - vir_format_identifier!( - vcx, - "{}_Assoc_{}_{}", - trait_data.trait_name, - tcx.item_name(impl_item.def_id), - struct_ty - ), - vir::expr! {forall ..[trait_ty_decls] :: {[assoc_fun(trait_tys)]} ([assoc_fun(trait_tys)]) == (assoc_type_expr)} - )); - }); + .map(|dec| dec.upcast_ty()) + .collect::>(); + + // Combine substituted trait params with the params of the associated type + let mut trait_ty_decls = trait_ty_decls.clone(); + trait_ty_decls.extend_from_slice(&assoc_decls[params.ty_exprs().len()..]); + + // Combine substituted trait params with the params of the associated type + let trait_tys = vcx.alloc_slice(&iter::once(struct_ty_expr).chain(args.get_ty().to_owned()).chain(assoc_params.ty_exprs()[params.ty_exprs().len()..].to_owned()).collect::>()); + + axs.push(vcx.mk_domain_axiom( + vir_format_identifier!( + vcx, + "{}_Assoc_{}_{}", + trait_data.trait_name, + tcx.item_name(impl_item.def_id), + struct_ty + ), + vir::expr! {forall ..[trait_ty_decls] :: {[assoc_fun(trait_tys)]} ([assoc_fun(trait_tys)]) == (assoc_type_expr)} + )); }); Ok(( diff --git a/prusti-encoder/src/encoders/ty/generics/traits.rs b/prusti-encoder/src/encoders/ty/generics/traits.rs index 6af37519d6a..c863f5f86c2 100644 --- a/prusti-encoder/src/encoders/ty/generics/traits.rs +++ b/prusti-encoder/src/encoders/ty/generics/traits.rs @@ -1,3 +1,5 @@ +use std::collections::HashMap; + use prusti_rustc_interface::{middle::ty::AssocKind, span::def_id::DefId}; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; use vir::{FunctionIdn, vir_format_identifier}; @@ -6,10 +8,10 @@ use crate::encoders::ty::generics::{GParams, GenericParamsEnc}; pub struct TraitEnc; -#[derive(Debug, Clone, Copy)] +#[derive(Debug, Clone)] pub struct TraitData<'vir> { pub trait_name: &'vir str, - pub type_did_fun_mapping: &'vir [(DefId, FunctionIdn<'vir, vir::ManyTyVal, vir::TyVal>)], + pub type_did_fun_mapping: HashMap>, pub impl_fun: FunctionIdn<'vir, vir::ManyTyVal, vir::Bool>, } @@ -57,15 +59,15 @@ impl TaskEncoder for TraitEnc { trait_name, tcx.item_name(item.def_id), ), - vcx.alloc_slice(&(vec![vir::TYPE_TYVAL; params_type.ty_exprs().len()])), // params_type also includes parameters of trait itself + vcx.alloc_slice(&vec![vir::TYPE_TYVAL; params_type.ty_exprs().len()]), // params_type also includes parameters of trait itself vir::TYPE_TYVAL, ), ) }) - .collect::>(); + .collect::>>(); let mut funcs = type_did_fun_mapping - .iter() - .map(|(_, function_idn)| vcx.mk_domain_function(*function_idn, false, None)) + .values() + .map(|function_idn| vcx.mk_domain_function(*function_idn, false, None)) .collect::>(); let impl_fun = FunctionIdn::new( vir_format_identifier!(vcx, "{}_impl", trait_name), @@ -85,7 +87,7 @@ impl TaskEncoder for TraitEnc { trait_domain, TraitData { trait_name, - type_did_fun_mapping: vcx.alloc_slice(type_did_fun_mapping.as_slice()), + type_did_fun_mapping, impl_fun, }, )) From 681da9f897b7cd3c3241638a24e4472a34367a9a Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 12 Dec 2025 16:03:52 +0100 Subject: [PATCH 25/26] Implement feedback from PR --- prusti-encoder/src/encoders/mir_fn/mod.rs | 12 ++------ prusti-encoder/src/encoders/ty/data.rs | 30 ++++++------------- .../src/encoders/ty/generics/trait_impls.rs | 20 ++++--------- .../src/encoders/ty/kinds/enumlike.rs | 2 -- .../src/encoders/ty/kinds/structlike.rs | 3 +- prusti-encoder/src/encoders/ty/rust_ty.rs | 20 ++++++------- prusti-encoder/src/encoders/ty/use_impure.rs | 6 ++-- prusti-encoder/src/encoders/ty/use_pure.rs | 6 ++-- 8 files changed, 31 insertions(+), 68 deletions(-) diff --git a/prusti-encoder/src/encoders/mir_fn/mod.rs b/prusti-encoder/src/encoders/mir_fn/mod.rs index 9e99f6d08b3..0aee2668542 100644 --- a/prusti-encoder/src/encoders/mir_fn/mod.rs +++ b/prusti-encoder/src/encoders/mir_fn/mod.rs @@ -62,18 +62,12 @@ pub fn encode_all_in_crate<'tcx>(tcx: ty::TyCtxt<'tcx>) { } } + // This creates the impl encoding for all traits in the crate + // To iterate over all _visible_ impl blocks, + // use tcx.visible_traits and tcx.all_impls(trait_id) for def_id in tcx.hir_crate_items(()).definitions() { if let hir::def::DefKind::Impl { of_trait: true } = tcx.def_kind(def_id) { TraitImplEnc::encode(def_id.to_def_id(), false).unwrap(); } } - - // for trait_id in tcx.visible_traits() { - // for impl_id in tcx.all_impls(trait_id) { - // { - // TraitImplEnc::encode(impl_id, false).unwrap(); - // } - - // } - // } } diff --git a/prusti-encoder/src/encoders/ty/data.rs b/prusti-encoder/src/encoders/ty/data.rs index 92400819cfe..04013548c62 100644 --- a/prusti-encoder/src/encoders/ty/data.rs +++ b/prusti-encoder/src/encoders/ty/data.rs @@ -6,8 +6,6 @@ use std::{ use prusti_rustc_interface::abi; -use prusti_rustc_interface::span::def_id::DefId; - pub trait TyDatas<'vir>: Debug + Clone + Copy { type TyData: Debug + Clone + 'vir = (); @@ -48,14 +46,12 @@ pub struct StructData<'vir, D: TyDatas<'vir>> { pub data: D::StructData, pub inhabited: bool, pub fields: Vec, - pub did: Option, } pub struct EnumData<'vir, D: TyDatas<'vir>> { pub data: D::EnumData, pub inhabited: bool, pub variants: Vec>, - pub did: Option, } pub struct VariantData<'vir, D: TyDatas<'vir>> { @@ -103,22 +99,16 @@ impl<'vir, D: TyDatas<'vir>> TySpecifics<'vir, D> { Self::MutRef(data) } - pub fn mk_structlike( - data: D::StructData, - inhabited: bool, - fields: Vec, - did: Option, - ) -> Self { - Self::StructLike(StructData::new(data, inhabited, fields, did)) + pub fn mk_structlike(data: D::StructData, inhabited: bool, fields: Vec) -> Self { + Self::StructLike(StructData::new(data, inhabited, fields)) } pub fn mk_enumlike( data: D::EnumData, inhabited: bool, variants: Vec>, - did: Option, ) -> Self { - Self::EnumLike(EnumData::new(data, inhabited, variants, did)) + Self::EnumLike(EnumData::new(data, inhabited, variants)) } pub fn is_param(&self) -> bool { @@ -263,7 +253,6 @@ impl<'vir, D: TyDatas<'vir>> StructData<'vir, D> { data: (&self.data, &other.data), inhabited: self.inhabited, fields: fields.collect(), - did: self.did, } } } @@ -280,7 +269,6 @@ impl<'vir, D: TyDatas<'vir>> EnumData<'vir, D> { data: (&self.data, &other.data), inhabited: self.inhabited, variants: variants.map(|(v1, v2)| v1.zip(v2)).collect(), - did: self.did, } } } @@ -303,10 +291,10 @@ impl<'vir, D1: TyDatas<'vir>, D2: TyDatas<'vir>> TyDatas<'vir> for (D1, D2) { // Deref implementations macro_rules! impls { - ($container:ident$( { $field:ident: $ty:ty $(, $did:ident)?})?) => { + ($container:ident$( { $field:ident: $ty:ty })?) => { impl<'vir, D: TyDatas<'vir>> $container<'vir, D> { - pub fn new(data: D::$container, inhabited: bool $(, $field: $ty $(, $did: Option)?)?) -> Self { - Self { data, inhabited, $($field, $($did,)?)? } + pub fn new(data: D::$container, inhabited: bool $(, $field: $ty)?) -> Self { + Self { data, inhabited, $($field,)? } } } @@ -318,7 +306,7 @@ impl<'vir, D: TyDatas<'vir>> Debug for $container<'vir, D> { impl<'vir, D: TyDatas<'vir>> Clone for $container<'vir, D> { fn clone(&self) -> Self { - Self { data: self.data.clone(), inhabited: self.inhabited, $($field: self.$field.clone() $(, $did: self.$did.clone())?)? } + Self { data: self.data.clone(), inhabited: self.inhabited, $($field: self.$field.clone())? } } } @@ -380,8 +368,8 @@ impl<'vir, D: TyDatas<'vir>> $container<'vir, D> { impls!(TyData { specifics: TySpecifics<'vir, D> }); impl_zip!(TyData.specifics); -impls!(StructData { fields: Vec, did }); -impls!(EnumData { variants: Vec>, did }); +impls!(StructData { fields: Vec }); +impls!(EnumData { variants: Vec> }); impls!(VariantData { inner: StructData<'vir, D> }); impl_zip!(VariantData.inner); diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index da29367bd46..d6bd48e454e 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -44,13 +44,7 @@ impl TaskEncoder for TraitImplEnc { let trait_did = trait_ref.def_id; let trait_data = deps.require_dep::(trait_did)?; - // for some reason, just using all args (which includes the struct at index 0) - // leads to a cycle for simple test cases -> split up and add struct manually - let args = deps.require_dep::(GArgs::new(ctx, &trait_ref.args[1..]))?; - - let struct_ty = tcx.type_of(task_key).instantiate_identity(); - let struct_ty_expr = - params.ty_expr(deps, RustTyDecomposition::from_ty(struct_ty, tcx, ctx)); + let args = deps.require_dep::(GArgs::new(ctx, trait_ref.args))?; let mut axs = Vec::new(); @@ -62,11 +56,8 @@ impl TaskEncoder for TraitImplEnc { .iter() .map(|dec| dec.upcast_ty()) .collect::>(); - let trait_tys = vcx.alloc_slice( - &iter::once(struct_ty_expr) - .chain(args.get_ty().to_owned()) - .collect::>(), - ); + let trait_tys = args.get_ty(); + axs.push( vcx.mk_domain_axiom( vir_format_identifier!(vcx, "{}_impl_{}", trait_data.trait_name, struct_ty), @@ -104,13 +95,12 @@ impl TaskEncoder for TraitImplEnc { .map(|dec| dec.upcast_ty()) .collect::>(); - // Combine substituted trait params with the params of the associated type + // Combine substituted trait ty decls with the decls of the associated type let mut trait_ty_decls = trait_ty_decls.clone(); trait_ty_decls.extend_from_slice(&assoc_decls[params.ty_exprs().len()..]); // Combine substituted trait params with the params of the associated type - let trait_tys = vcx.alloc_slice(&iter::once(struct_ty_expr).chain(args.get_ty().to_owned()).chain(assoc_params.ty_exprs()[params.ty_exprs().len()..].to_owned()).collect::>()); - + let trait_tys = vcx.alloc_slice(&iter::empty().chain(args.get_ty().to_owned()).chain(assoc_params.ty_exprs()[params.ty_exprs().len()..].to_owned()).collect::>()); axs.push(vcx.mk_domain_axiom( vir_format_identifier!( vcx, diff --git a/prusti-encoder/src/encoders/ty/kinds/enumlike.rs b/prusti-encoder/src/encoders/ty/kinds/enumlike.rs index 3c840d9c928..3d0c5320c8f 100644 --- a/prusti-encoder/src/encoders/ty/kinds/enumlike.rs +++ b/prusti-encoder/src/encoders/ty/kinds/enumlike.rs @@ -60,7 +60,6 @@ pub(crate) fn ty_pure<'vir>( }, data.inhabited, variants, - data.did, )) } @@ -182,6 +181,5 @@ pub(crate) fn ty_impure<'vir>( }, data.inhabited, variants.into_iter().map(|v| v.3).collect::>(), - data.did, )) } diff --git a/prusti-encoder/src/encoders/ty/kinds/structlike.rs b/prusti-encoder/src/encoders/ty/kinds/structlike.rs index df104405e68..2c7a6fcaab8 100644 --- a/prusti-encoder/src/encoders/ty/kinds/structlike.rs +++ b/prusti-encoder/src/encoders/ty/kinds/structlike.rs @@ -51,7 +51,6 @@ pub(super) fn ty_pure_variant<'vir>( }, data.inhabited, des, - data.did, )) } @@ -195,7 +194,7 @@ pub(crate) fn ty_impure_variant<'vir>( }; Ok(( - StructData::new((), data.inhabited, field_accessors, data.did), + StructData::new((), data.inhabited, field_accessors), pred_owned, variant_snap_expr, )) diff --git a/prusti-encoder/src/encoders/ty/rust_ty.rs b/prusti-encoder/src/encoders/ty/rust_ty.rs index 7d28c0c0f0a..3f5950e9a21 100644 --- a/prusti-encoder/src/encoders/ty/rust_ty.rs +++ b/prusti-encoder/src/encoders/ty/rust_ty.rs @@ -14,8 +14,6 @@ use super::{ generics::{GArgs, GParams}, }; -use prusti_rustc_interface::span::def_id::DefId; - #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct RustTyDecomposition<'tcx> { pub ty: RustTy<'tcx>, @@ -444,7 +442,7 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { ty: LazyRustTy(Self::new_param_ty(i as u32)), }) .collect::>(); - TySpecifics::mk_structlike((), true, fields, None) + TySpecifics::mk_structlike((), true, fields) } ty::TyKind::Array(..) | ty::TyKind::Slice(..) => { // TODO: add array/slice support @@ -472,13 +470,13 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { ty: LazyRustTy(ty), }) .collect::>(); - TySpecifics::mk_structlike((), true, fields, None) + TySpecifics::mk_structlike((), true, fields) } ty::TyKind::Never => { let data = vir::with_vcx(|vcx| RustEnumData { discr: vcx.tcx().types.isize, }); - TySpecifics::mk_enumlike(data, false, Vec::new(), None) + TySpecifics::mk_enumlike(data, false, Vec::new()) } // TODO: add str support ty::TyKind::Str => TySpecifics::mk_opaque(()), @@ -498,12 +496,12 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { fid: abi::FieldIdx::from_usize(0), ty: LazyRustTy(Self::new_param_ty(0)), }]; - return TySpecifics::mk_structlike((), true, fields, Some(adt.did())); + return TySpecifics::mk_structlike((), true, fields); } match adt.adt_kind() { ty::AdtKind::Struct => { - let data = Self::from_struct(adt.non_enum_variant(), adt.did()); + let data = Self::from_struct(adt.non_enum_variant()); Self::StructLike(data) } ty::AdtKind::Enum => { @@ -517,9 +515,9 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { } } - fn from_struct(variant: &ty::VariantDef, did: DefId) -> StructData<'tcx, RustTyDatas> { + fn from_struct(variant: &ty::VariantDef) -> StructData<'tcx, RustTyDatas> { let fields = Self::from_fields(&variant.fields); - StructData::new((), true, fields, Some(did)) + StructData::new((), true, fields) } fn from_enum(adt: ty::AdtDef<'tcx>) -> EnumData<'tcx, RustTyDatas> { @@ -539,11 +537,11 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { discr_val: discr.val, }, true, - StructData::new((), true, fields, Some(adt.did())), + StructData::new((), true, fields), ) }) .collect::>(); - EnumData::new(data, true, variants, Some(adt.did())) + EnumData::new(data, true, variants) }) } diff --git a/prusti-encoder/src/encoders/ty/use_impure.rs b/prusti-encoder/src/encoders/ty/use_impure.rs index fb8a287811d..0ffc7e02d52 100644 --- a/prusti-encoder/src/encoders/ty/use_impure.rs +++ b/prusti-encoder/src/encoders/ty/use_impure.rs @@ -196,13 +196,12 @@ impl<'a, 'vir> TyUseImpureWalker<'a, 'vir> { }) .collect::>(); let inhabited = data.inhabited; - let did = data.did; let data = TyUseImpureStructData { args: self.args_t, ref_to_pred, impure: *data.1, }; - StructData::new(data, inhabited, fields, did) + StructData::new(data, inhabited, fields) } fn encode_enumlike( @@ -220,12 +219,11 @@ impl<'a, 'vir> TyUseImpureWalker<'a, 'vir> { }) .collect::>(); let inhabited = data.inhabited; - let did = data.did; let data = TyUseImpureEnumData { args: self.args_t, impure: *data.1, }; - EnumData::new(data, inhabited, variants, did) + EnumData::new(data, inhabited, variants) } } diff --git a/prusti-encoder/src/encoders/ty/use_pure.rs b/prusti-encoder/src/encoders/ty/use_pure.rs index 38d984b2c0f..64101dabf7b 100644 --- a/prusti-encoder/src/encoders/ty/use_pure.rs +++ b/prusti-encoder/src/encoders/ty/use_pure.rs @@ -199,12 +199,11 @@ impl<'a, 'vir> TyUsePureWalker<'a, 'vir> { }) .collect::>(); let inhabited = data.inhabited; - let did = data.did; let data = TyUsePureStructData { args: self.args_t, pure: *data.1, }; - StructData::new(data, inhabited, fields, did) + StructData::new(data, inhabited, fields) } fn encode_enumlike( @@ -212,7 +211,6 @@ impl<'a, 'vir> TyUsePureWalker<'a, 'vir> { data: &EnumData<'vir, (RustTyDatas, PureTyDatas)>, params: GParams<'vir>, ) -> EnumData<'vir, UsePureTyDatas> { - let did = data.did; let variants = data .variants .iter() @@ -221,7 +219,7 @@ impl<'a, 'vir> TyUsePureWalker<'a, 'vir> { VariantData::new(*variant.1, variant.inhabited, structlike) }) .collect::>(); - EnumData::new(*data.1, data.inhabited, variants, did) + EnumData::new(*data.1, data.inhabited, variants) } } From 20948c9e9198a72222bf372deecf6198d99eeacc Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 12 Dec 2025 16:08:29 +0100 Subject: [PATCH 26/26] Fix indentation --- prusti-encoder/src/encoders/ty/data.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/data.rs b/prusti-encoder/src/encoders/ty/data.rs index 04013548c62..7448521ac5c 100644 --- a/prusti-encoder/src/encoders/ty/data.rs +++ b/prusti-encoder/src/encoders/ty/data.rs @@ -291,9 +291,9 @@ impl<'vir, D1: TyDatas<'vir>, D2: TyDatas<'vir>> TyDatas<'vir> for (D1, D2) { // Deref implementations macro_rules! impls { - ($container:ident$( { $field:ident: $ty:ty })?) => { + ($container:ident$( { $field:ident: $ty:ty })?) => { impl<'vir, D: TyDatas<'vir>> $container<'vir, D> { - pub fn new(data: D::$container, inhabited: bool $(, $field: $ty)?) -> Self { + pub fn new(data: D::$container, inhabited: bool $(, $field: $ty)?) -> Self { Self { data, inhabited, $($field,)? } } } @@ -306,7 +306,7 @@ impl<'vir, D: TyDatas<'vir>> Debug for $container<'vir, D> { impl<'vir, D: TyDatas<'vir>> Clone for $container<'vir, D> { fn clone(&self) -> Self { - Self { data: self.data.clone(), inhabited: self.inhabited, $($field: self.$field.clone())? } + Self { data: self.data.clone(), inhabited: self.inhabited, $($field: self.$field.clone())? } } }