diff --git a/prusti-encoder/src/encoders/ty/generics/args_ty.rs b/prusti-encoder/src/encoders/ty/generics/args_ty.rs index 6ada2017595..e92a9aa0e42 100644 --- a/prusti-encoder/src/encoders/ty/generics/args_ty.rs +++ b/prusti-encoder/src/encoders/ty/generics/args_ty.rs @@ -53,7 +53,7 @@ impl TaskEncoder for GArgsTyEnc { let decomp = RustTyDecomposition::from_ty(arg, task_key.context); params.ty_expr(deps, decomp) }) - .collect::>(); + .collect::, _>>()?; let const_args = task_key .args .iter() diff --git a/prusti-encoder/src/encoders/ty/generics/builtin_trait/mod.rs b/prusti-encoder/src/encoders/ty/generics/builtin_trait/mod.rs new file mode 100644 index 00000000000..8300b470f56 --- /dev/null +++ b/prusti-encoder/src/encoders/ty/generics/builtin_trait/mod.rs @@ -0,0 +1,206 @@ +use crate::encoders::ty::{ + RustTy, + generics::{GParams, GenericParams, GenericParamsEnc, r#trait::TraitEnc}, + lifted::TyConstructorEnc, +}; +use prusti_rustc_interface::{middle::ty, span::def_id::DefId}; + +use task_encoder::{CacheRef, EncodeFullError, TaskEncoder}; +use vir::vir_format_identifier; + +pub mod sized_trait; +pub mod tuple_trait; + +pub type SizedTraitEnc = BuiltinTraitEnc; +pub type TupleTraitEnc = BuiltinTraitEnc; + +/// Trait that must be implemented by all builtin trait markers. +/// +/// This trait defines the interface that marker types must implement to work with +/// `SpecialTraitEnc`. The marker types should be zero-sized structs that are `'static`. +trait BuiltinTrait { + /// Returns the DefId of this builtin trait. + fn def_id() -> DefId; + + /// Returns the expression representing whether the given type implements this trait. + /// + /// # Returns + /// + /// - `Ok(Some(expr))` - The type implements the trait; `expr` is a boolean expression + /// that evaluates to true when the trait is implemented + /// - `Ok(None)` - The type definitely does not implement this trait + /// - `Err(_)` - An error occurred during encoding + fn does_impl<'vir>( + deps: &mut task_encoder::TaskEncoderDependencies<'vir, BuiltinTraitEnc>, + ctx: GParams<'vir>, + ty: ty::Ty<'vir>, + ) -> Result>, EncodeFullError<'vir, BuiltinTraitEnc>> + where + Self: Sized + 'static; + + /// Provides access to the encoder cache for this builtin trait. + /// + /// This should be implemented using the `task_encoder::encoder_cache!` macro. + fn with_cache<'vir, F, R>(f: F) -> R + where + Self: Sized + 'static, + F: FnOnce(&'vir CacheRef<'vir, BuiltinTraitEnc>) -> R; +} + +/// Generic wrapper for encoding builtin traits. +/// +/// This struct wraps a marker type `T` that implements `BuiltinTrait` and provides +/// a `TaskEncoder` implementation for it. The wrapper handles the common encoding +/// logic while delegating trait-specific decisions to the marker type. +pub struct BuiltinTraitEnc(std::marker::PhantomData); + +#[derive(PartialEq, Eq, Clone, Copy, Debug, Hash)] +pub enum BuiltinTraitEncTask<'a> { + Activate, + Encode(RustTy<'a>), +} + +#[derive(Clone, Debug)] +pub struct TraitData<'a> { + trait_: ::OutputRef<'a>, + trait_generics: GenericParams<'a>, +} +impl<'a> TraitData<'a> { + fn new( + trait_: ::OutputRef<'a>, + trait_generics: GenericParams<'a>, + ) -> Box { + Box::new(Self { + trait_, + trait_generics, + }) + } +} + +#[derive(Clone, Debug)] +pub enum BuiltinTraitEncOutput<'a> { + Activated(Box>), + TypeCheck(Option>), +} + +impl TaskEncoder for BuiltinTraitEnc { + const ENCODER_NAME: &'static str = "builtin trait encoder"; + // Need to delegate to the `BuiltinTrait` to implement the `with_cache` due to issues + // described in `task_encoder::encoder_cache!` + fn with_cache<'vir, F, R>(f: F) -> R + where + F: FnOnce(&'vir task_encoder::CacheRef<'vir, Self>) -> R, + T: 'vir, + { + T::with_cache(f) + } + + type TaskDescription<'vir> = BuiltinTraitEncTask<'vir>; + type OutputFullLocal<'vir> = BuiltinTraitEncOutput<'vir>; + + fn task_to_key<'vir>(task: &Self::TaskDescription<'vir>) -> Self::TaskKey<'vir> { + *task + } + + fn do_encode_full<'vir>( + task_key: &Self::TaskKey<'vir>, + deps: &mut task_encoder::TaskEncoderDependencies<'vir, Self>, + ) -> task_encoder::EncodeFullResult<'vir, Self> { + deps.emit_output_ref(*task_key, ())?; + match task_key { + BuiltinTraitEncTask::Activate => { + let trait_did = T::def_id(); + let trait_ = deps.require_ref::(trait_did)?; + + let trait_generics = { + let params = TraitEnc::trait_params(trait_did); + deps.require_dep::(params)? + }; + Ok(( + (BuiltinTraitEncOutput::Activated(TraitData::new(trait_, trait_generics))), + (), + )) + } + BuiltinTraitEncTask::Encode(rust_ty) => { + assert!(!rust_ty.specifics.is_param()); + + let ty = rust_ty.erased_ty_for_builtin_traits(); + + let check = T::does_impl(deps, rust_ty.params, ty)?; + + Ok(((BuiltinTraitEncOutput::TypeCheck(check)), ())) + } + } + } + + fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { + let outputs = Self::all_outputs_local_no_errors(program); + + let mut trait_info = None; + let mut checks = Vec::new(); + + for output in outputs { + match output { + BuiltinTraitEncOutput::Activated(box data) => { + trait_info = Some((data.trait_, data.trait_generics)); + } + BuiltinTraitEncOutput::TypeCheck(Some(check)) => { + checks.push(check); + } + _ => {} + } + } + let Some((trait_, trait_generics)) = trait_info else { + return; + }; + + vir::with_vcx(|vcx| { + let trait_impl_fun = trait_.impl_fun; + let trait_impl_for_unknown_fun = trait_.impl_for_unknown_fun; + + let unknown_type_check = { + let self_expr = trait_generics.ty_exprs()[0]; + + let is_unknown = + vcx.mk_adt_discriminator_expr(self_expr, TyConstructorEnc::UNKNOWN_TYPE_NAME); + let extracted_id = + TyConstructorEnc::unknown_type_id_accessor(vcx).call()(self_expr); + + let unknown_impls = trait_impl_for_unknown_fun.call()( + extracted_id, + &trait_generics.ty_exprs()[1..], + trait_generics.const_exprs(), + ); + + vir::expr! {vcx; (is_unknown) && (unknown_impls) } + }; + + checks.push(unknown_type_check); + + let ensures = vcx.mk_eq_expr(vcx.mk_result(vir::TYPE_BOOL), vcx.mk_disj(&checks)); + + let trait_impl_fun = vcx.mk_function( + trait_impl_fun, + (trait_generics.ty_decls(), trait_generics.const_decls()), + &[], + vcx.alloc_slice(&[ensures]), + Some(&vir::DecreasesGenData::Star), + None, + ); + + program.add_function(trait_impl_fun); + + let trait_impl_unknown_fun = + vcx.mk_domain_function(trait_impl_for_unknown_fun, false, None); + + let trait_domain = vcx.mk_domain( + vir_format_identifier!(vcx, "trait_{}", trait_.trait_name), + &[], + &[], + vcx.alloc_slice(&[trait_impl_unknown_fun]), + None, + ); + program.add_domain(trait_domain); + }); + } +} diff --git a/prusti-encoder/src/encoders/ty/generics/builtin_trait/sized_trait.rs b/prusti-encoder/src/encoders/ty/generics/builtin_trait/sized_trait.rs new file mode 100644 index 00000000000..2841f14f62a --- /dev/null +++ b/prusti-encoder/src/encoders/ty/generics/builtin_trait/sized_trait.rs @@ -0,0 +1,138 @@ +use crate::encoders::ty::generics::{ + GParams, builtin_trait::BuiltinTraitEnc, trait_impls::TraitImplEnc, +}; +use prusti_rustc_interface::middle::{ty, ty::Upcast}; +use task_encoder::EncodeFullError; + +use prusti_rustc_interface::span::def_id::DefId; +pub struct SizedTrait; + +impl super::BuiltinTrait for SizedTrait { + task_encoder::encoder_cache!(BuiltinTraitEnc); + + fn def_id() -> DefId { + vir::with_vcx(|vcx| vcx.tcx().lang_items().sized_trait().unwrap()) + } + + fn does_impl<'vir>( + deps: &mut task_encoder::TaskEncoderDependencies<'vir, BuiltinTraitEnc>, + ctx: GParams<'vir>, + ty: ty::Ty<'vir>, + ) -> Result>, EncodeFullError<'vir, BuiltinTraitEnc>> { + vir::with_vcx(|vcx| { + let sizedness = sizedness_for_ty(vcx.tcx(), ty); + let check = match sizedness { + Sizedness::Unsized => None, + Sizedness::Sized => Some(sizedness_check(vcx, deps, ctx, ty, None)?), + Sizedness::Dependent(dep_ty) => { + Some(sizedness_check(vcx, deps, ctx, ty, Some(dep_ty))?) + } + }; + + Ok(check) + }) + } +} + +fn sizedness_check<'vir>( + vcx: &'vir vir::VirCtxt<'vir>, + deps: &mut task_encoder::TaskEncoderDependencies<'vir, BuiltinTraitEnc>, + impl_ctx: GParams<'vir>, + impl_ty: ty::Ty<'vir>, + depended_on: Option>, +) -> Result, EncodeFullError<'vir, BuiltinTraitEnc>> { + let tcx = vcx.tcx(); + + let sized_did = tcx.lang_items().sized_trait().unwrap(); + + let impls_sized = ty::TraitRef::new_from_args( + tcx, + sized_did, + tcx.mk_args_trait(impl_ty, std::iter::empty()), + ); + + let param_env = ty::ParamEnv::new( + tcx.mk_clauses( + depended_on + .map(|dep_ty| ty::TraitRef::new(tcx, sized_did, [dep_ty]).upcast(tcx)) + .as_slice(), + ), + ); + + let impl_ctx = GParams::new(impl_ctx.rust_params(), param_env, false); + + TraitImplEnc::impl_block_check(vcx, deps, impl_ctx, impls_sized) +} + +#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] +pub enum Sizedness<'tcx> { + /// A type is definitely `Sized` + Sized, + /// A type is definitely not `Sized` + Unsized, + /// The sizedness of the type depends on the sizedness some other type contained within + Dependent(ty::Ty<'tcx>), +} + +impl<'tcx> Sizedness<'tcx> { + fn map(self, f: impl FnOnce(ty::Ty<'tcx>) -> ty::Ty<'tcx>) -> Self { + match self { + Sizedness::Dependent(ty) => Sizedness::Dependent(f(ty)), + other => other, + } + } +} + +/// Modified version of `https://doc.rust-lang.org/nightly/nightly-rustc/rustc_ty_utils/ty/fn.sizedness_constraint_for_ty.html` +fn sizedness_for_ty<'tcx>(tcx: ty::TyCtxt<'tcx>, ty: ty::Ty<'tcx>) -> Sizedness<'tcx> { + match ty.kind() { + // Always `Sized` + ty::Bool + | ty::Char + | ty::Int(..) + | ty::Uint(..) + | ty::Float(..) + | ty::RawPtr(..) + | ty::Ref(..) + | ty::FnDef(..) + | ty::FnPtr(..) + | ty::Array(..) + | ty::Closure(..) + | ty::CoroutineClosure(..) + | ty::Coroutine(..) + | ty::CoroutineWitness(..) + | ty::Never => Sizedness::Sized, + + ty::Str | ty::Slice(..) | ty::Dynamic(..) => Sizedness::Unsized, + + // Maybe `Sized` + ty::Param(..) | ty::Alias(..) | ty::Error(_) => Sizedness::Dependent(ty), + + // We cannot instantiate the binder, so just return the *original* type back, + // but only if the inner type has a sized constraint. Thus we skip the binder, + // but don't actually use the result from `sizedness_for_ty`. + ty::UnsafeBinder(inner_ty) => sizedness_for_ty(tcx, inner_ty.skip_binder()).map(|_| ty), + + // Never `Sized` + ty::Foreign(..) => Sizedness::Unsized, + + // Recursive cases + ty::Pat(ty, _) => sizedness_for_ty(tcx, *ty), + + // Empty tuple always `Sized`, otherwise sizedness depends on last field + ty::Tuple(tys) => tys + .last() + .map_or(Sizedness::Sized, |last| sizedness_for_ty(tcx, *last)), + + ty::Adt(adt, args) => adt + .sizedness_constraint(tcx, ty::SizedTraitKind::Sized) + .map_or(Sizedness::Sized, |intermediate| { + let ty = intermediate.instantiate(tcx, args); + sizedness_for_ty(tcx, ty) + }), + + ty::Placeholder(..) | ty::Bound(..) | ty::Infer(..) => { + panic!("unexpected type `{ty:?}` in `sizedness_for_ty`") + } + } +} diff --git a/prusti-encoder/src/encoders/ty/generics/builtin_trait/tuple_trait.rs b/prusti-encoder/src/encoders/ty/generics/builtin_trait/tuple_trait.rs new file mode 100644 index 00000000000..a2abc4dbcdd --- /dev/null +++ b/prusti-encoder/src/encoders/ty/generics/builtin_trait/tuple_trait.rs @@ -0,0 +1,40 @@ +use crate::encoders::ty::generics::{ + GParams, builtin_trait::BuiltinTraitEnc, trait_impls::TraitImplEnc, +}; +use prusti_rustc_interface::{middle::ty, span::def_id::DefId}; +use task_encoder::EncodeFullError; + +pub struct TupleTrait; + +impl super::BuiltinTrait for TupleTrait { + task_encoder::encoder_cache!(BuiltinTraitEnc); + + fn def_id() -> DefId { + vir::with_vcx(|vcx| vcx.tcx().lang_items().tuple_trait().unwrap()) + } + + fn does_impl<'vir>( + deps: &mut task_encoder::TaskEncoderDependencies<'vir, BuiltinTraitEnc>, + ctx: GParams<'vir>, + ty: ty::Ty<'vir>, + ) -> Result>, EncodeFullError<'vir, BuiltinTraitEnc>> { + vir::with_vcx(|vcx| { + let tcx = vcx.tcx(); + + let tuple_trait_did = tcx.lang_items().tuple_trait().unwrap(); + + let check = if matches!(ty.kind(), ty::TyKind::Tuple(..)) { + let impls_tuple = ty::TraitRef::new_from_args( + tcx, + tuple_trait_did, + tcx.mk_args_trait(ty, std::iter::empty()), + ); + Some(TraitImplEnc::impl_block_check(vcx, deps, ctx, impls_tuple)?) + } else { + None + }; + + Ok(check) + }) + } +} diff --git a/prusti-encoder/src/encoders/ty/generics/mod.rs b/prusti-encoder/src/encoders/ty/generics/mod.rs index 15600638041..961291e527b 100644 --- a/prusti-encoder/src/encoders/ty/generics/mod.rs +++ b/prusti-encoder/src/encoders/ty/generics/mod.rs @@ -3,11 +3,13 @@ mod params; mod casters; mod args_ty; mod args; +pub mod builtin_trait; pub mod r#trait; pub mod trait_fn; pub mod trait_impls; pub use args::*; pub use args_ty::*; +pub use builtin_trait::*; pub use params::*; pub use use_casters::*; diff --git a/prusti-encoder/src/encoders/ty/generics/params.rs b/prusti-encoder/src/encoders/ty/generics/params.rs index 819dda2795a..81c3b29aa11 100644 --- a/prusti-encoder/src/encoders/ty/generics/params.rs +++ b/prusti-encoder/src/encoders/ty/generics/params.rs @@ -3,7 +3,7 @@ use prusti_rustc_interface::{ middle::ty, span::{def_id::DefId, symbol}, }; -use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; +use task_encoder::{EncodeFullError, EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; use vir::{CastType, HasType}; use crate::encoders::{ @@ -27,6 +27,8 @@ pub struct GParams<'tcx> { /// This flag indicates whether this is the case, so that we can replace it /// with the actual `Self` parameter when needed. is_trait_extern_spec: bool, + /// A suffix to disambiguate generic parameters of different contexts + suffix: Option<&'static str>, } impl<'tcx> GParams<'tcx> { @@ -39,6 +41,7 @@ impl<'tcx> GParams<'tcx> { params, env, is_trait_extern_spec, + suffix: None, } } @@ -89,6 +92,13 @@ impl<'tcx> GParams<'tcx> { ); } + pub fn with_suffix(self, suffix: &'static str) -> Self { + Self { + suffix: Some(suffix), + ..self + } + } + /// Tries to normalize associated types of the corresponding type. Returns /// `Some` if managed to normalize (or there were no associated types), else /// returns None. @@ -230,7 +240,7 @@ impl<'vir> GenericParams<'vir> { self.const_exprs()[self.map_idx(param.index).unwrap_err()] } - fn map_idx(&self, index: u32) -> Result { + pub(super) fn map_idx(&self, index: u32) -> Result { let result = self.indices[index as usize]; assert!( result.ok().is_none_or(|i| i != usize::MAX), @@ -257,27 +267,27 @@ impl<'vir> GenericParams<'vir> { &self, deps: &mut TaskEncoderDependencies<'vir, E>, ty: RustTyDecomposition<'vir>, - ) -> vir::ExprTyVal<'vir> { + ) -> Result, EncodeFullError<'vir, E>> { if let TySpecifics::Param(RustParamData::Generic) = &ty.ty.specifics { let param = ty.args.expect_param(); - return match param { + return Ok(match param { GParamVariant::Param(p) => self.ty_exprs[self.map_idx(p.index).unwrap()], GParamVariant::Alias(alias) => vir::with_vcx(|vcx| { let tcx = vcx.tcx(); let trait_did = tcx.associated_item(alias.def_id).container_id(tcx); - let trait_data = deps.require_ref::(trait_did).unwrap(); + let trait_data = deps.require_ref::(trait_did)?; let args = GArgs::new(ty.args.context, alias.args); - let args = deps.require_dep::(args).unwrap(); - (trait_data.assoc_types[&alias.def_id])(args.get_ty(), args.get_const()) - }), - }; + let args = deps.require_dep::(args)?; + Ok((trait_data.assoc_types[&alias.def_id])( + args.get_ty(), + args.get_const(), + )) + })?, + }); } - let ty_constructor = deps - .require_ref::(ty.ty) - .unwrap() - .ty_constructor; - let args = deps.require_dep::(ty.args).unwrap(); - ty_constructor(args.get_ty(), args.get_const()) + let ty_constructor = deps.require_ref::(ty.ty)?.ty_constructor; + let args = deps.require_dep::(ty.args)?; + Ok(ty_constructor(args.get_ty(), args.get_const())) } } @@ -298,7 +308,12 @@ impl TaskEncoder for GenericParamsEnc { deps.emit_output_ref(*task_key, ())?; vir::with_vcx(|vcx| { let sanitize = |name: symbol::Symbol, index: u32| { - vir::ViperIdent::sanitize(vcx, &format!("{name}${index}")).to_str() + let name = if let Some(suffix) = task_key.suffix { + format!("{name}${index}_{suffix}") + } else { + format!("{name}${index}") + }; + vir::ViperIdent::sanitize(vcx, &name).to_str() }; let mut indices = vec![Ok(usize::MAX); task_key.params.len()]; diff --git a/prusti-encoder/src/encoders/ty/generics/trait.rs b/prusti-encoder/src/encoders/ty/generics/trait.rs index 29fe3b540b6..70b07be215c 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait.rs @@ -3,7 +3,16 @@ use rustc_hash::FxHashMap; use task_encoder::{EncodeFullResult, OutputRefAny, TaskEncoder, TaskEncoderDependencies}; use vir::{FunctionIdn, vir_format_identifier}; -use crate::encoders::ty::generics::{GParams, GenericParamsEnc}; +use crate::encoders::ty::{ + RustTyDecomposition, + generics::{ + GParams, GenericParamsEnc, + builtin_trait::{BuiltinTraitEncTask, SizedTraitEnc, TupleTraitEnc}, + trait_impls::TraitImplEnc, + }, + lifted::TyConstructorEnc, + pure::TyPureEnc, +}; pub struct TraitEnc; @@ -12,7 +21,17 @@ pub struct TraitEncOutputRef<'vir> { pub trait_name: &'vir str, pub assoc_types: FxHashMap>, + pub assoc_consts: + FxHashMap>, pub impl_fun: FunctionIdn<'vir, (vir::ManyTyVal, vir::ManyCSnap), vir::Bool>, + pub impl_for_unknown_fun: + FunctionIdn<'vir, (vir::Int, vir::ManyTyVal, vir::ManyCSnap), vir::Bool>, +} + +#[derive(Debug, Clone)] +pub struct TraitEncOutput<'vir> { + trait_domain: vir::Domain<'vir>, + impl_fun: vir::Function<'vir>, } impl<'vir> OutputRefAny for TraitEncOutputRef<'vir> {} @@ -28,11 +47,13 @@ impl TaskEncoder for TraitEnc { type TaskDescription<'vir> = DefId; type OutputRef<'vir> = TraitEncOutputRef<'vir>; - type OutputFullLocal<'vir> = vir::Domain<'vir>; + type OutputFullLocal<'vir> = Option>; fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { - for dom in Self::all_outputs_local_no_errors(program) { - program.add_domain(dom); + for output in TraitEnc::all_outputs_local_no_errors(program) { + let Some(output) = output else { continue }; + program.add_domain(output.trait_domain); + program.add_function(output.impl_fun); } } @@ -42,50 +63,140 @@ impl TaskEncoder for TraitEnc { ) -> EncodeFullResult<'vir, Self> { vir::with_vcx(|vcx| { let tcx = vcx.tcx(); - let trait_params = GParams::from(*task_key); + let trait_params = Self::trait_params(*task_key); let trait_generics = deps.require_dep::(trait_params)?; + let trait_args = (trait_generics.ty_args(), trait_generics.const_args()); + let trait_decls = (trait_generics.ty_decls(), trait_generics.const_decls()); + let trait_name = vcx.alloc_str(tcx.item_name(task_key).as_str()); let mut dom_funcs = Vec::new(); let mut assoc_types = FxHashMap::default(); + let mut assoc_consts = FxHashMap::default(); + + let mk_identifier = |item_name, item_type| { + vir_format_identifier!(vcx, "{trait_name}_assoc_{item_type}_{item_name}") + }; for item in tcx.associated_items(task_key).in_definition_order() { - if !matches!(item.kind, ty::AssocKind::Type { .. }) { - continue; + let assoc_did = item.def_id; + let assoc_name = tcx.item_name(assoc_did); + let params = deps + .require_dep::(GParams::from(assoc_did)) + .unwrap(); + let args = (params.ty_args(), params.const_args()); + match item.kind { + ty::AssocKind::Type { .. } => { + let fun = FunctionIdn::new( + mk_identifier(assoc_name, "type"), + args, + vir::TYPE_TYVAL, + ); + assoc_types.insert(assoc_did, fun); + dom_funcs.push(vcx.mk_domain_function(fun, false, None)); + } + ty::AssocKind::Const { .. } => { + let rust_ty = tcx.type_of(assoc_did).skip_binder(); + let decomp = RustTyDecomposition::from_ty(rust_ty, assoc_did); + let ret_ty = (deps.require_ref::(decomp.ty).unwrap().domain)(); + + let fun = + FunctionIdn::new(mk_identifier(assoc_name, "const"), args, ret_ty); + assoc_consts.insert(assoc_did, fun); + dom_funcs.push(vcx.mk_domain_function(fun, false, None)); + } + ty::AssocKind::Fn { .. } => {} } - - let def_id = item.def_id; - - // item_generics also includes parameters of trait itself - let item_params = GParams::from(def_id); - let item_generics = deps.require_dep::(item_params)?; - let item_name = tcx.item_name(def_id); - - let type_func = FunctionIdn::new( - vir_format_identifier!(vcx, "{trait_name}_assoc_type_{item_name}"), - (item_generics.ty_args(), item_generics.const_args()), - vir::TYPE_TYVAL, - ); - assoc_types.insert(def_id, type_func); - dom_funcs.push(vcx.mk_domain_function(type_func, false, None)); } let impl_fun = FunctionIdn::new( - vir_format_identifier!(vcx, "impl_{trait_name}"), - (trait_generics.ty_args(), trait_generics.const_args()), + vir_format_identifier!(vcx, "{trait_name}_impl"), + trait_args, vir::TYPE_BOOL, ); + let impl_for_unknown_fun = { + // Omit the `Self` type as it is known to be the unknown type + let ty_args = &trait_args.0[1..]; + let const_args = trait_args.1; + FunctionIdn::new( + vir_format_identifier!(vcx, "{trait_name}_impl_for_unknown"), + (vir::TYPE_INT, ty_args, const_args), + vir::TYPE_BOOL, + ) + }; + + // Emit the impl function reference early, so that it can be used to encode caller + // bounds without causing dependency cycles. deps.emit_output_ref( *task_key, TraitEncOutputRef { trait_name, assoc_types, + assoc_consts, impl_fun, + impl_for_unknown_fun, }, )?; - dom_funcs.push(vcx.mk_domain_function(impl_fun, false, None)); + // When encoding builtin traits, emitting of the impl function is handled by + // their respective builtin trait encoders. Activate them here. + if tcx.lang_items().sized_trait() == Some(*task_key) { + deps.require_dep::(BuiltinTraitEncTask::Activate)?; + return Ok((None, ())); + } + if tcx.lang_items().tuple_trait() == Some(*task_key) { + deps.require_dep::(BuiltinTraitEncTask::Activate)?; + return Ok((None, ())); + } + + let impl_fun_body = { + let mut trait_impl_checks: Vec<_> = tcx + .all_impls(*task_key) + .map(|impl_did| { + deps.require_dep::(impl_did) + .unwrap() + .impl_condition + }) + .collect(); + + let unknown_type_check = { + let self_expr = trait_generics.ty_exprs()[0]; + + let is_unknown_type = vcx + .mk_adt_discriminator_expr(self_expr, TyConstructorEnc::UNKNOWN_TYPE_NAME); + + let extracted_id = + TyConstructorEnc::unknown_type_id_accessor(vcx).call()(self_expr); + + let unknown_impls = impl_for_unknown_fun( + extracted_id, + &trait_generics.ty_exprs()[1..], + trait_generics.const_exprs(), + ); + + vir::expr! { vcx; + (is_unknown_type) && (unknown_impls) + } + }; + trait_impl_checks.push(unknown_type_check); + + vcx.mk_disj(&trait_impl_checks) + }; + + let ensures = vcx.mk_eq_expr(vcx.mk_result(vir::TYPE_BOOL), impl_fun_body); + + let impl_fun = vcx.mk_function( + impl_fun, + trait_decls, + &[], + vcx.alloc_slice(&[ensures]), + Some(&vir::DecreasesGenData::Star), + None, + ); + + let impl_for_unknown_fun = vcx.mk_domain_function(impl_for_unknown_fun, false, None); + dom_funcs.push(impl_for_unknown_fun); let trait_domain = vcx.mk_domain( vir_format_identifier!(vcx, "trait_{trait_name}"), @@ -95,7 +206,19 @@ impl TaskEncoder for TraitEnc { None, ); - Ok((trait_domain, ())) + Ok(( + Some(TraitEncOutput { + trait_domain, + impl_fun, + }), + (), + )) }) } } + +impl TraitEnc { + pub(super) fn trait_params<'tcx>(trait_did: DefId) -> GParams<'tcx> { + GParams::from(trait_did).with_suffix("trait") + } +} diff --git a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs index 46c66e658d7..f048bf1353a 100644 --- a/prusti-encoder/src/encoders/ty/generics/trait_impls.rs +++ b/prusti-encoder/src/encoders/ty/generics/trait_impls.rs @@ -1,14 +1,18 @@ +use std::collections::VecDeque; + use prusti_interface::{PrustiError, specs::specifications::SpecQuery}; use prusti_rustc_interface::{ + index::bit_set::DenseBitSet, middle::{mir, ty}, span::def_id::DefId, }; -use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{Domain, Method, MethodIdn, vir_format_identifier}; +use task_encoder::{EncodeFullError, EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; +use vir::{CastType, Domain, Method, MethodIdn, vir_format_identifier}; use crate::{ encoders::{ - FunctionCallEnc, MirLocalDefEnc, MirLocalDefEncTask, MirSpecEnc, Pure, + ConstEnc, FunctionCallEnc, MirLocalDefEnc, MirLocalDefEncTask, MirSpecEnc, Pure, + r#const::ConstEncTask, mir_fn::{CallTaskDescription, RustSignature}, pure::spec::MirSpecEncMode, ty::{ @@ -17,6 +21,7 @@ use crate::{ GArgs, GArgsCastEnc, GArgsTyEnc, GParams, GenericParamsEnc, r#trait::TraitEnc, trait_fn::TraitFnEnc, }, + lifted::TyConstructorEnc, }, }, trait_support::is_function_with_body, @@ -24,6 +29,11 @@ use crate::{ pub struct TraitImplEnc; +#[derive(Debug, Clone)] +pub struct TraitImplEncOutput<'vir> { + pub impl_condition: vir::ExprBool<'vir>, +} + impl TaskEncoder for TraitImplEnc { task_encoder::encoder_cache!(TraitImplEnc); const ENCODER_NAME: &'static str = "trait impl encoder"; @@ -42,6 +52,7 @@ impl TaskEncoder for TraitImplEnc { } type TaskDescription<'vir> = DefId; + type OutputFullDependency<'vir> = TraitImplEncOutput<'vir>; type OutputFullLocal<'vir> = (Domain<'vir>, Vec>); fn do_encode_full<'vir>( @@ -64,8 +75,6 @@ impl TaskEncoder for TraitImplEnc { let trait_data = deps.require_ref::(trait_did)?; let trait_name = trait_data.trait_name; - let args = deps.require_dep::(GArgs::new(impl_context, trait_ref.args))?; - let mut axioms = Vec::new(); let mut methods = Vec::new(); @@ -73,16 +82,8 @@ impl TaskEncoder for TraitImplEnc { let implementing_ty = RustTyDecomposition::from_ty(implementing_ty, impl_context); let implementing_ty = implementing_ty.ty.name(); - let impl_fun = trait_data.impl_fun; let impl_ty_decls = impl_params.ty_decls(); let impl_const_decls = impl_params.const_decls(); - let trait_tys = args.get_ty(); - let trait_consts = args.get_const(); - - axioms.push(vcx.mk_domain_axiom( - vir_format_identifier!(vcx, "{trait_name}_impl_{implementing_ty}_{idx}_does_impl"), - vir::expr! {forall ..[impl_ty_decls], ..[impl_const_decls] :: {[impl_fun(trait_tys, trait_consts)]} [impl_fun(trait_tys, trait_consts)]}, - )); for impl_item in tcx.associated_items(task_key).in_definition_order() { let trait_item_def_id = impl_item.trait_item_def_id.unwrap(); @@ -97,9 +98,7 @@ impl TaskEncoder for TraitImplEnc { // parameters of assoc item include already substituted arguments let impl_item_context = GParams::from(impl_item_def_id); - let impl_item_params = deps - .require_dep::(impl_item_context) - .unwrap(); + let impl_item_params = deps.require_dep::(impl_item_context)?; // The ty and const decls of the trait items are the decls of // the item itself prefixed by the decls of the impl itself. @@ -146,10 +145,15 @@ impl TaskEncoder for TraitImplEnc { tcx.type_of(impl_item_def_id).instantiate_identity(), impl_item_context, ), - ); + )?; axioms.push(vcx.mk_domain_axiom( - vir_format_identifier!(vcx, "{trait_name}_impl_{implementing_ty}_{idx}_assoc_type_{item_name}"), - vir::expr! {forall ..[trait_ty_decls], ..[trait_const_decls] :: {[assoc_type(trait_tys, trait_consts)]} ([assoc_type(trait_tys, trait_consts)]) == (assoc_type_expr)}, + vir_format_identifier!( + vcx, + "{trait_name}_impl_{implementing_ty}_{idx}_assoc_type_{item_name}" + ), + vir::expr! {forall ..[trait_ty_decls], ..[trait_const_decls] :: + {[assoc_type(trait_tys, trait_consts)]} + ([assoc_type(trait_tys, trait_consts)]) == (assoc_type_expr)}, )); } ty::AssocKind::Fn { .. } => { @@ -430,6 +434,10 @@ impl TaskEncoder for TraitImplEnc { } } + let trait_ref = tcx.impl_trait_ref(task_key).unwrap().instantiate_identity(); + let impl_condition = + Self::impl_block_check(vcx, deps, GParams::from(*task_key), trait_ref)?; + Ok(( ( vcx.mk_domain( @@ -444,8 +452,273 @@ impl TaskEncoder for TraitImplEnc { ), methods, ), - (), + TraitImplEncOutput { impl_condition }, )) }) } } +impl TraitImplEnc { + fn bitset_from(iter: impl IntoIterator, size: usize) -> DenseBitSet { + iter.into_iter() + .fold(DenseBitSet::new_empty(size), |mut acc, idx| { + acc.insert(idx); + acc + }) + } + fn projection_deps<'vir>( + projection: ty::ProjectionPredicate<'vir>, + generics_count: usize, + ) -> (DenseBitSet, DenseBitSet) { + let generic_idx = |arg: ty::GenericArg| match arg.kind() { + ty::GenericArgKind::Type(ty) if let ty::TyKind::Param(p) = ty.kind() => Some(p.index), + ty::GenericArgKind::Const(const_) if let ty::ConstKind::Param(p) = const_.kind() => { + Some(p.index) + } + _ => None, + }; + + let required = projection + .projection_term + .args + .iter() + .flat_map(|arg| arg.walk().filter_map(generic_idx)); + + let produced = projection.term.walk().filter_map(generic_idx); + + ( + Self::bitset_from(required, generics_count), + Self::bitset_from(produced, generics_count), + ) + } + + fn order_projections<'vir>( + known_generics: impl IntoIterator, + projections: impl IntoIterator>, + generics_count: usize, + ) -> Vec> { + let mut known_generics = Self::bitset_from(known_generics, generics_count); + + let mut worklist: VecDeque<_> = projections + .into_iter() + .map(|p| (p, Self::projection_deps(p, generics_count))) + .collect(); + + let mut ordered = Vec::new(); + + while let Some((proj, (required, produced))) = worklist.pop_front() { + if known_generics.superset(&required) { + known_generics.union(&produced); + ordered.push(proj); + } else { + worklist.push_back((proj, (required, produced))); + } + } + + ordered + } + + fn discover_bind_points<'vir, E: TaskEncoder + 'vir + ?Sized>( + deps: &mut TaskEncoderDependencies<'vir, E>, + generic_map: &mut GenericsMap<'vir>, + ctx: GParams<'vir>, + expr: vir::ExprTyVal<'vir>, + ty: ty::Ty<'vir>, + ) -> Result<(), EncodeFullError<'vir, E>> { + if let ty::TyKind::Param(p) = ty.kind() { + generic_map.try_insert(p.index, expr.upcast_ty()); + return Ok(()); + } + + let decomp = RustTyDecomposition::from_ty(ty, ctx); + let ty_enc = deps.require_ref::(decomp.ty)?; + + let args = decomp.args.args(); + let inner_types = args.iter().filter_map(|arg| arg.as_type()); + for (i, inner_ty) in inner_types.enumerate() { + let accessor = ty_enc.ty_param_accessors[i]; + let inner_expr = accessor.call()(expr); + + Self::discover_bind_points(deps, generic_map, ctx, inner_expr, inner_ty)?; + } + + let inner_consts = args.iter().filter_map(|arg| arg.as_const()); + for (i, inner_const) in inner_consts.enumerate() { + let accessor = ty_enc.const_param_accessors[i]; + let inner_expr = accessor.call()(expr); + + if let ty::ConstKind::Param(p) = inner_const.kind() { + generic_map.try_insert(p.index, inner_expr.upcast_ty()); + } + } + Ok(()) + } + + pub(super) fn impl_block_check<'vir, E: TaskEncoder + 'vir + ?Sized>( + vcx: &'vir vir::VirCtxt<'vir>, + deps: &mut TaskEncoderDependencies<'vir, E>, + impl_ctx: GParams<'vir>, + trait_ref: ty::TraitRef<'vir>, + ) -> Result, EncodeFullError<'vir, E>> { + let tcx = vcx.tcx(); + let impl_ctx = impl_ctx.with_suffix("impl"); + let impl_params = deps.require_dep::(impl_ctx)?; + + let trait_ctx = TraitEnc::trait_params(trait_ref.def_id); + let trait_params = deps.require_dep::(trait_ctx)?; + + let args = deps.require_dep::(GArgs::new(impl_ctx, trait_ref.args))?; + + let generics_count = impl_ctx.rust_params().len(); + + // Collect the bindings for the generics of this impl block + let mut generics_map = GenericsMap::new(generics_count); + + // Walk the trait type generic arguments + let impl_rust_tys = trait_ref.args.iter().filter_map(|arg| arg.as_type()); + for (ty_arg, rust_ty) in std::iter::zip(trait_params.ty_exprs(), impl_rust_tys) { + Self::discover_bind_points(deps, &mut generics_map, trait_ctx, ty_arg, rust_ty)?; + } + + // Walk the trait const generic arguments + let impl_rust_consts = trait_ref.args.iter().filter_map(|arg| arg.as_const()); + for (const_arg, rust_const) in std::iter::zip(trait_params.const_exprs(), impl_rust_consts) + { + if let ty::ConstKind::Param(p) = rust_const.kind() { + generics_map.try_insert(p.index, const_arg.upcast_ty()); + } + } + + let mut checks = Vec::new(); + // Collect checks for the generics of the trait and their corresponding arguments in the impl + for (trait_ty_param, ty_args) in std::iter::zip(trait_params.ty_exprs(), args.get_ty()) { + checks.push(vcx.mk_eq_expr(trait_ty_param, ty_args)); + } + for (trait_const_param, const_args) in + std::iter::zip(trait_params.const_exprs(), args.get_const()) + { + checks.push(vcx.mk_eq_expr(trait_const_param, const_args)); + } + + let caller_bounds = impl_ctx.typing_env().param_env.caller_bounds(); + + // Collect checks for the trait bounds + let trait_preds = caller_bounds + .iter() + .filter_map(ty::Clause::as_trait_clause) + .map(ty::Binder::skip_binder); + for trait_pred in trait_preds { + let trait_did = trait_pred.def_id(); + let trait_ = deps.require_ref::(trait_did)?; + let gargs = GArgs::new(impl_ctx, trait_pred.trait_ref.args); + let gargs = deps.require_dep::(gargs)?; + + let impl_check = (trait_.impl_fun)(gargs.get_ty(), gargs.get_const()); + checks.push(impl_check); + } + + // Collect checks for the projection predicates. These have to be processed in a way such that + // any bindpoints they introduce are introduced with the let-bindings in the correct order. + let proj_preds = caller_bounds + .iter() + .filter_map(ty::Clause::as_projection_clause) + .map(ty::Binder::skip_binder); + let proj_preds = Self::order_projections(generics_map.keys(), proj_preds, generics_count); + for proj_pred in proj_preds { + let trait_did = proj_pred.trait_def_id(tcx); + let trait_ = deps.require_ref::(trait_did)?; + let gargs = GArgs::new(impl_ctx, proj_pred.projection_term.args); + let gargs = deps.require_dep::(gargs)?; + + let (projection, expr): (vir::ExprDyn, vir::ExprDyn) = match proj_pred.term.kind() { + ty::TermKind::Ty(ty) => { + let projection = + trait_.assoc_types[&proj_pred.def_id()](gargs.get_ty(), gargs.get_const()); + let decomp = RustTyDecomposition::from_ty(ty, impl_ctx); + let ty_expr = impl_params.ty_expr(deps, decomp)?; + Self::discover_bind_points(deps, &mut generics_map, impl_ctx, projection, ty)?; + (projection.upcast_ty(), ty_expr.upcast_ty()) + } + ty::TermKind::Const(const_) => { + let projection = + trait_.assoc_consts[&proj_pred.def_id()](gargs.get_ty(), gargs.get_const()); + let ty = tcx.type_of(proj_pred.def_id()).instantiate_identity(); + let const_task = ConstEncTask::Ty { + const_, + ty, + context: impl_ctx, + }; + let const_expr = deps.require_dep::(const_task)?; + if let ty::ConstKind::Param(p) = const_.kind() { + generics_map.try_insert(p.index, const_expr.upcast_ty()); + } + (projection.upcast_ty(), const_expr.upcast_ty()) + } + }; + + let projection_check = vcx.mk_eq_expr(projection, expr); + checks.push(projection_check); + } + + let checks = vcx.mk_conj(&checks); + + Ok(generics_map + .insertion_ordered() + .rfold(checks, |acc, (idx, expr)| { + let idx = impl_params.map_idx(idx); + let decl = match idx { + Result::Ok(idx) => impl_params.ty_decls()[idx].upcast_ty(), + Result::Err(idx) => impl_params.const_decls()[idx].upcast_ty(), + }; + vcx.mk_let_expr(decl, expr, acc) + })) + } +} + +/// Collects bindings for generics in the order they are discovered. +#[derive(Clone, Debug)] +struct GenericsMap<'vir> { + order: usize, + map: Vec)>>, +} + +impl<'vir> GenericsMap<'vir> { + fn new(size: usize) -> Self { + GenericsMap { + order: 0, + map: vec![None; size], + } + } + + /// Insert the given expression as the binding for the `idx`-th generic, while recording the + /// insertion order. Returns `false` if the generic already has a binding, and `true` + /// otherwise. + fn try_insert(&mut self, idx: u32, expr: vir::ExprDyn<'vir>) -> bool { + let idx = idx as usize; + if self.map[idx].is_some() { + return false; + } + self.map[idx] = Some((self.order, expr)); + self.order += 1; + true + } + + /// Collect the bindings in their insertion order. + fn insertion_ordered(&self) -> impl DoubleEndedIterator)> { + let mut ordered = self + .map + .iter() + .enumerate() + .filter_map(|(idx, opt)| opt.map(|(order, expr)| (order, (idx as u32, expr)))) + .collect::>(); + ordered.sort_by_key(|(order, _)| *order); + ordered.into_iter().map(|(_, (idx, expr))| (idx, expr)) + } + + /// Already present generics. + fn keys(&self) -> impl Iterator { + self.map + .iter() + .enumerate() + .filter_map(|(idx, opt)| opt.as_ref().map(|_| idx as u32)) + } +} diff --git a/prusti-encoder/src/encoders/ty/lifted/ty_constructor.rs b/prusti-encoder/src/encoders/ty/lifted/ty_constructor.rs index c9e7a92769a..e8452245824 100644 --- a/prusti-encoder/src/encoders/ty/lifted/ty_constructor.rs +++ b/prusti-encoder/src/encoders/ty/lifted/ty_constructor.rs @@ -1,7 +1,10 @@ use task_encoder::{EncodeFullResult, OutputRefAny, TaskEncoder}; use vir::{CallableIdn, CastType, FunctionIdn, HasType}; -use crate::encoders::ty::{RustParamData, RustTy, TySpecifics, generics::GenericParamsEnc}; +use crate::encoders::ty::{ + RustParamData, RustTy, TySpecifics, + generics::{BuiltinTraitEncTask, GenericParamsEnc, SizedTraitEnc, TupleTraitEnc}, +}; use super::r#typeof::{TypeOfEnc, TypeOfEncOutputRef}; @@ -97,6 +100,7 @@ impl TaskEncoder for TyConstructorEnc { ) }) .collect::>(); + let const_accessor_functions = params .const_decls() .iter() @@ -131,6 +135,12 @@ impl TaskEncoder for TyConstructorEnc { .collect::>>(); let variant = vcx.mk_adt_constructor(type_function_ident.name().to_str(), vcx.alloc_slice(&args)); + + // NOTE: These calls depend on the ref output of this encoder + let builtin_trait_task = BuiltinTraitEncTask::Encode(task_key); + deps.require_dep::(builtin_trait_task)?; + deps.require_dep::(builtin_trait_task)?; + Ok((variant, ())) }) } @@ -138,9 +148,8 @@ impl TaskEncoder for TyConstructorEnc { fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { let mut constructors = Self::all_outputs_local_no_errors(program); vir::with_vcx(|vcx| { - let args = vcx.alloc_array(&[vcx.mk_local_decl("non_unit", vir::TYPE_INT)]); - let unknown = vcx.mk_adt_constructor("Unknown_type", args); - constructors.push(unknown); + let args = vcx.alloc_array(&[vcx.mk_local_decl(Self::UNKNOWN_TYPE_ID, vir::TYPE_INT)]); + constructors.push(vcx.mk_adt_constructor(Self::UNKNOWN_TYPE_NAME, args)); let adt = vcx.mk_adt( vir::ViperIdent::new("Type"), &[], @@ -150,3 +159,15 @@ impl TaskEncoder for TyConstructorEnc { }) } } + +impl TyConstructorEnc { + /// The name of the constructor for the unknown type variant in the `Type` ADT. + pub const UNKNOWN_TYPE_NAME: &str = "Unknown_type"; + const UNKNOWN_TYPE_ID: &str = "id"; + + pub fn unknown_type_id_accessor<'vir>( + vcx: &'vir vir::VirCtxt<'vir>, + ) -> vir::AdtDestructor<'vir, vir::TyVal, vir::Int> { + vcx.mk_adt_destructor(Self::UNKNOWN_TYPE_ID, vir::TYPE_TYVAL, vir::TYPE_INT) + } +} diff --git a/prusti-encoder/src/encoders/ty/rust_ty.rs b/prusti-encoder/src/encoders/ty/rust_ty.rs index 85aa81b8ded..ba9d076c999 100644 --- a/prusti-encoder/src/encoders/ty/rust_ty.rs +++ b/prusti-encoder/src/encoders/ty/rust_ty.rs @@ -73,6 +73,7 @@ impl<'tcx> RustTyDecomposition<'tcx> { let data = RustTyData { name: symbol::Symbol::intern("Real"), params: GParams::empty(), + erased_ty: None, }; let specifics = TySpecifics::Builtin(RustBuiltinData::BuiltinReal); Self { @@ -242,6 +243,7 @@ pub type RustBuiltin<'tcx> = >::BuiltinData; #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] pub struct RustTyData<'tcx> { pub name: symbol::Symbol, + erased_ty: Option>, pub params: GParams<'tcx>, } @@ -249,6 +251,13 @@ impl<'tcx> RustTyData<'tcx> { pub fn name(&self) -> &str { self.name.as_str() } + + /// NOTE: a hack to get the `ty::Ty` to the encoders for builtin traits like `Sized` or `Tuple`. + /// Should not be used for other purposes + pub(super) fn erased_ty_for_builtin_traits(&self) -> ty::Ty<'tcx> { + self.erased_ty + .expect("should be `Some` when called in special trait encoders") + } } #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] @@ -303,13 +312,14 @@ impl<'tcx> TyData<'tcx, RustTyDatas> { let ty = context.normalize(ty); let name = Self::ty_name(ty); - let (params, args) = Self::identity_for_ty(ty, context.is_trait_extern_spec()); + let (erased_ty, params, args) = Self::identity_for_ty(ty, context.is_trait_extern_spec()); let args = GArgs::new(context, args); let data = RustTyData { name: symbol::Symbol::intern(&name), + erased_ty: erased_ty.into(), params, }; - let specifics = TySpecifics::from_ty(ty); + let specifics = TySpecifics::from_ty(erased_ty); let maybe_inhabited = vir::with_vcx(|vcx| !ty.is_privately_uninhabited(vcx.tcx(), context.typing_env())); RustTyDecomposition { @@ -321,10 +331,11 @@ impl<'tcx> TyData<'tcx, RustTyDatas> { fn from_prim_ty(ty: ty::Ty<'tcx>) -> RustTyDecomposition<'tcx> { let name = Self::prim_ty_name(ty); - let (params, args) = Self::identity_for_prim_ty(ty); + let (erased_ty, params, args) = Self::identity_for_prim_ty(ty); let args = GArgs::new(params, args); let data = RustTyData { name: symbol::Symbol::intern(&name), + erased_ty: erased_ty.into(), params, }; let specifics = TySpecifics::from_prim_ty(ty); @@ -387,80 +398,103 @@ impl<'tcx> TyData<'tcx, RustTyDatas> { /// For the ty `MyStruct` (with defn /// `struct MyStruct> { ... }`), returns - /// `([>], [i32])`. + /// `(MyStruct, [>], [i32])`. pub(super) fn identity_for_ty( ty: ty::Ty<'tcx>, is_trait_extern_spec: bool, - ) -> (GParams<'tcx>, ty::GenericArgsRef<'tcx>) { - let (params, args) = match *ty.kind() { + ) -> (ty::Ty<'tcx>, GParams<'tcx>, ty::GenericArgsRef<'tcx>) { + let tcx = vir::with_vcx(|vcx| vcx.tcx()); + let (new_ty, params, args) = match *ty.kind() { _ if ty.is_primitive() => return Self::identity_for_prim_ty(ty), - ty::TyKind::Adt(adt, args) => (GParams::from(adt.did()), args), + ty::TyKind::Adt(adt, args) => { + let params = GParams::from(adt.did()); + let new_ty = ty::Ty::new_adt(tcx, adt, params.rust_params()); + (new_ty, params, args) + } ty::TyKind::Tuple(tys) => { let gtys = (0..tys.len()).map(|idx| TySpecifics::new_param_ty(idx as u32)); ( + ty::Ty::new_tup_from_iter(tcx, gtys.clone()), GParams::empty_env(Self::args_from_tys(gtys)), Self::args_from_tys(tys), ) } - ty::TyKind::Array(ty, cst) => vir::with_vcx(|vcx| { - let gcst = TySpecifics::new_param_const(0).into(); - let gty = TySpecifics::new_param_ty(1).into(); - let gparams = Self::args_from_generics([gcst, gty]); - let predicate = - vcx.tcx() - .mk_predicate(ty::Binder::dummy(ty::PredicateKind::Clause( - ty::ClauseKind::ConstArgHasType( - gcst.expect_const(), - vcx.tcx().types.usize, - ), - ))); - let param_env = - ty::ParamEnv::new(vcx.tcx().mk_clauses(&[predicate.expect_clause()])); + ty::TyKind::Array(ty, cst) => { + let gcst = TySpecifics::new_param_const(0); + let gty = TySpecifics::new_param_ty(1); + let gargs = Self::args_from_generics([gcst.into(), gty.into()]); + let predicate = tcx.mk_predicate(ty::Binder::dummy(ty::PredicateKind::Clause( + ty::ClauseKind::ConstArgHasType(gcst, tcx.types.usize), + ))); + let param_env = ty::ParamEnv::new(tcx.mk_clauses(&[predicate.expect_clause()])); ( - GParams::new(gparams, param_env, false), + ty::Ty::new_array_with_const_len(tcx, gty, gcst), + GParams::new(gargs, param_env, false), Self::args_from_generics([cst.into(), ty.into()]), ) - }), - ty::TyKind::Slice(ty) | ty::TyKind::RawPtr(ty, _) => { - let gty = Self::args_from_tys([TySpecifics::new_param_ty(0)]); - (GParams::empty_env(gty), Self::args_from_tys([ty])) } - ty::TyKind::Ref(region, ty, _) => { + ty::TyKind::Slice(ty) => { + let gty = TySpecifics::new_param_ty(0); + let params = GParams::empty_env(Self::args_from_tys([gty])); + let new_ty = ty::Ty::new_slice(tcx, gty); + (new_ty, params, Self::args_from_tys([ty])) + } + ty::TyKind::RawPtr(ty, mutbl) => { + let gty = TySpecifics::new_param_ty(0); + let params = GParams::empty_env(Self::args_from_tys([gty])); + let new_ty = ty::Ty::new_ptr(tcx, gty, mutbl); + (new_ty, params, Self::args_from_tys([ty])) + } + ty::TyKind::Ref(region, ty, mutbl) => { // TODO: what lifetime should we use here? - let param_region = vir::with_vcx(|vcx| vcx.tcx().lifetimes.re_erased.into()); - let param_ty = TySpecifics::new_param_ty(1).into(); - let gty = Self::args_from_generics([param_region, param_ty]); + let param_region = tcx.lifetimes.re_erased; + let gty = TySpecifics::new_param_ty(1); ( - GParams::empty_env(gty), + ty::Ty::new_ref(tcx, param_region, gty, mutbl), + GParams::empty_env(Self::args_from_generics([param_region.into(), gty.into()])), Self::args_from_generics([region.into(), ty.into()]), ) } - ty::TyKind::Alias(..) | ty::TyKind::Param(_) => { - let gty = Self::args_from_tys([TySpecifics::new_param_ty(0)]); - (GParams::empty_env(gty), Self::args_from_tys([ty])) + ty::TyKind::Alias(_, _) | ty::TyKind::Param(_) | ty::TyKind::Dynamic(..) => { + let gty = TySpecifics::new_param_ty(0); + let gargs = Self::args_from_tys([gty]); + // Note: an `Alias` is turned into a `Param` here with the alias + // itself as the type argument. + (gty, GParams::empty_env(gargs), Self::args_from_tys([ty])) } - ty::TyKind::Closure(did, args) => vir::with_vcx(|vcx| { - let identity = ty::List::identity_for_item(vcx.tcx(), did); - let gargs = vcx.tcx().mk_args(identity.as_closure().parent_args()); - let args = vcx.tcx().mk_args(args.as_closure().parent_args()); + ty::TyKind::Closure(did, args) => { + let identity = ty::List::identity_for_item(tcx, did); + // We only want to fully erase the parent information + let parts = ty::ClosureArgsParts { + parent_args: identity.as_closure().parent_args(), + closure_kind_ty: tcx.erase_regions(args.as_closure().kind_ty()), + closure_sig_as_fn_ptr_ty: tcx + .erase_regions(args.as_closure().sig_as_fn_ptr_ty()), + tupled_upvars_ty: tcx.erase_regions(args.as_closure().tupled_upvars_ty()), + }; + let erased = ty::ClosureArgs::new(tcx, parts); + let gargs = tcx.mk_args(identity.as_closure().parent_args()); + let args = tcx.mk_args(args.as_closure().parent_args()); ( - GParams::new(gargs, vcx.tcx().param_env(did), is_trait_extern_spec), + ty::Ty::new_closure(tcx, did, erased.args), + GParams::new(gargs, tcx.param_env(did), is_trait_extern_spec), args, ) - }), - ty::TyKind::Never - | ty::TyKind::Str - | ty::TyKind::FnPtr(..) - | ty::TyKind::Dynamic(..) => (GParams::empty(), ty::GenericArgs::empty()), + } + ty::TyKind::Never | ty::TyKind::Str | ty::TyKind::FnPtr(..) => { + (ty, GParams::empty(), ty::GenericArgs::empty()) + } _ => todo!("instantiate_identity_for_type for {:?}", ty), }; params.check(args); - (params, args) + (new_ty, params, args) } - fn identity_for_prim_ty(ty: ty::Ty<'tcx>) -> (GParams<'tcx>, ty::GenericArgsRef<'tcx>) { + fn identity_for_prim_ty( + ty: ty::Ty<'tcx>, + ) -> (ty::Ty<'tcx>, GParams<'tcx>, ty::GenericArgsRef<'tcx>) { assert!(ty.is_primitive()); - (GParams::empty(), ty::GenericArgs::empty()) + (ty, GParams::empty(), ty::GenericArgs::empty()) } fn args_from_tys(tys: impl IntoIterator>) -> ty::GenericArgsRef<'tcx> { @@ -489,29 +523,25 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { let fields = args .iter() .enumerate() - .map(|(i, _)| RustFieldData { + .map(|(i, inner)| RustFieldData { name: symbol::Symbol::intern(&format!("_{i}")), fid: abi::FieldIdx::from_usize(i), - ty: LazyRustTy(Self::new_param_ty(i as u32)), + ty: LazyRustTy(inner), }) .collect::>(); TySpecifics::mk_structlike((), fields) } - ty::TyKind::Array(_, _) => TySpecifics::ArrayLike(ArrayData { + ty::TyKind::Array(inner, _) => TySpecifics::ArrayLike(ArrayData { slice: false, - data: LazyRustTy(Self::new_param_ty(1)), + data: LazyRustTy(*inner), }), - ty::TyKind::Slice(_) => TySpecifics::ArrayLike(ArrayData { + ty::TyKind::Slice(inner) => TySpecifics::ArrayLike(ArrayData { slice: true, - data: LazyRustTy(Self::new_param_ty(0)), + data: LazyRustTy(*inner), }), - ty::TyKind::Ref(_, _, mutability) => match mutability { - ty::Mutability::Mut => { - TySpecifics::mk_mutref(LazyRustTy(TySpecifics::new_param_ty(1))) - } - ty::Mutability::Not => { - TySpecifics::mk_immref(LazyRustTy(TySpecifics::new_param_ty(1))) - } + ty::TyKind::Ref(_, inner, mutability) => match mutability { + ty::Mutability::Mut => TySpecifics::mk_mutref(LazyRustTy(*inner)), + ty::Mutability::Not => TySpecifics::mk_immref(LazyRustTy(*inner)), }, // TODO: add raw pointer support ty::TyKind::RawPtr(..) => TySpecifics::mk_opaque(()), @@ -571,14 +601,8 @@ impl<'tcx> TySpecifics<'tcx, RustTyDatas> { } } else { match adt.adt_kind() { - ty::AdtKind::Struct => { - let data = Self::from_struct(adt.non_enum_variant()); - Self::StructLike(data) - } - ty::AdtKind::Enum => { - let data = Self::from_enum(adt); - Self::EnumLike(data) - } + ty::AdtKind::Struct => Self::StructLike(Self::from_struct(adt.non_enum_variant())), + ty::AdtKind::Enum => Self::EnumLike(Self::from_enum(adt)), ty::AdtKind::Union => { // TODO: add union support Self::mk_opaque(()) diff --git a/prusti-encoder/src/encoders/ty/use_impure.rs b/prusti-encoder/src/encoders/ty/use_impure.rs index 7db5da51a2f..9fea283622d 100644 --- a/prusti-encoder/src/encoders/ty/use_impure.rs +++ b/prusti-encoder/src/encoders/ty/use_impure.rs @@ -1,5 +1,5 @@ use prusti_rustc_interface::abi; -use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; +use task_encoder::{EncodeFullError, EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; use vir::{CastType, PredicateIdn}; use crate::encoders::{ @@ -120,7 +120,7 @@ impl TaskEncoder for TyUseImpureEnc { deps.emit_output_ref(*task_key, ())?; let ty_impure = deps.require_dep::(task_key.ty)?; - let mut walker = TyUseImpureWalker::new(deps, task_key.args); + let mut walker = TyUseImpureWalker::new(deps, task_key.args)?; let ty_use_impure = walker.encode_ty(task_key.ty.zip(ty_impure), task_key.maybe_inhabited); Ok(((), ty_use_impure.alloc())) } @@ -137,9 +137,12 @@ struct TyUseImpureWalker<'a, 'vir> { } impl<'a, 'vir> TyUseImpureWalker<'a, 'vir> { - fn new(deps: &'a mut TaskEncoderDependencies<'vir, TyUseImpureEnc>, args: GArgs<'vir>) -> Self { - let args_t = deps.require_dep::(args).unwrap(); - Self { deps, args_t, args } + fn new( + deps: &'a mut TaskEncoderDependencies<'vir, TyUseImpureEnc>, + args: GArgs<'vir>, + ) -> Result> { + let args_t = deps.require_dep::(args)?; + Ok(Self { deps, args_t, args }) } fn encode_ty( diff --git a/prusti-encoder/src/lib.rs b/prusti-encoder/src/lib.rs index e4683931bba..19fb27ecfda 100644 --- a/prusti-encoder/src/lib.rs +++ b/prusti-encoder/src/lib.rs @@ -24,7 +24,8 @@ use crate::encoders::{ custom::PairUseEnc, ty::{ generics::{ - GArgsCastEnc, r#trait::TraitEnc, trait_fn::TraitFnEnc, trait_impls::TraitImplEnc, + GArgsCastEnc, SizedTraitEnc, TupleTraitEnc, r#trait::TraitEnc, trait_fn::TraitFnEnc, + trait_impls::TraitImplEnc, }, interpretation::bitvec::BitVecEnc, lifted::{TyConstructorEnc, TypeOfEnc}, @@ -113,6 +114,8 @@ pub fn test_entrypoint<'tcx>( TraitEnc::emit_outputs(&mut program); TraitFnEnc::emit_outputs(&mut program); TraitImplEnc::emit_outputs(&mut program); + SizedTraitEnc::emit_outputs(&mut program); + TupleTraitEnc::emit_outputs(&mut program); if std::env::var("LOCAL_TESTING").is_ok() { std::fs::write("local-testing/simple.vpr", program.code()).unwrap();