From d1547e45adac5a65143cdf566098df2f0b700ddb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 4 Jan 2025 19:47:08 +0100 Subject: [PATCH 1/8] Name matcher: Clearer support for patterns without generics --- charon/src/name_matcher/mod.rs | 36 ++++++++++++++++------ charon/tests/test-rust-name-matcher.rs | 2 +- charon/tests/ui/rust-name-matcher-tests.rs | 5 +-- 3 files changed, 31 insertions(+), 12 deletions(-) diff --git a/charon/src/name_matcher/mod.rs b/charon/src/name_matcher/mod.rs index a53b486cb..1815d7e4e 100644 --- a/charon/src/name_matcher/mod.rs +++ b/charon/src/name_matcher/mod.rs @@ -49,14 +49,20 @@ impl Pattern { } pub fn matches(&self, ctx: &TranslatedCrate, name: &Name) -> bool { - self.matches_with_generics(ctx, name, &GenericArgs::empty()) + self.matches_with_generics(ctx, name, None) + } + + pub fn matches_item(&self, ctx: &TranslatedCrate, item: AnyTransItem<'_>) -> bool { + let generics = item.generic_params().identity_args(); + let name = &item.item_meta().name; + self.matches_with_generics(ctx, name, Some(&generics)) } pub fn matches_with_generics( &self, ctx: &TranslatedCrate, name: &Name, - args: &GenericArgs, + args: Option<&GenericArgs>, ) -> bool { let zipped = self.elems.iter().zip_longest(&name.name).collect_vec(); let zipped_len = zipped.len(); @@ -64,7 +70,7 @@ impl Pattern { let is_last = i + 1 == zipped_len; match x { EitherOrBoth::Both(pat, elem) => { - let args = if is_last { args } else { &GenericArgs::empty() }; + let args = if is_last { args } else { None }; if !pat.matches_with_generics(ctx, elem, args) { return false; } @@ -89,11 +95,11 @@ impl Pattern { let Some(type_name) = ctx.item_name(*type_id) else { return false; }; - self.matches_with_generics(ctx, type_name, args) + self.matches_with_generics(ctx, type_name, Some(args)) } TyKind::Adt(TypeId::Builtin(builtin_ty), args) => { let name = builtin_ty.get_name(); - self.matches_with_generics(ctx, &name, args) + self.matches_with_generics(ctx, &name, Some(args)) } TyKind::Adt(TypeId::Tuple, _) | TyKind::TypeVar(..) @@ -153,7 +159,7 @@ impl PatElem { &self, ctx: &TranslatedCrate, elem: &PathElem, - args: &GenericArgs, + args: Option<&GenericArgs>, ) -> bool { match (self, elem) { (PatElem::Glob, _) => true, @@ -168,7 +174,7 @@ impl PatElem { // `crate` is a special keyword that referes to the current crate. let same_ident = pat_ident == ident || (pat_ident == "crate" && ident == &ctx.real_crate_name); - same_ident && (generics.is_empty() || PatTy::matches_generics(ctx, generics, args)) + same_ident && PatTy::matches_generics(ctx, generics, args) } (PatElem::Impl(_pat), PathElem::Impl(ImplElem::Ty(..), _)) => { // TODO @@ -181,7 +187,7 @@ impl PatElem { let Some(trait_name) = ctx.item_name(timpl.impl_trait.trait_id) else { return false; }; - pat.matches_with_generics(ctx, trait_name, &timpl.impl_trait.generics) + pat.matches_with_generics(ctx, trait_name, Some(&timpl.impl_trait.generics)) } _ => false, } @@ -189,7 +195,19 @@ impl PatElem { } impl PatTy { - pub fn matches_generics(ctx: &TranslatedCrate, pats: &[Self], generics: &GenericArgs) -> bool { + pub fn matches_generics( + ctx: &TranslatedCrate, + pats: &[Self], + generics: Option<&GenericArgs>, + ) -> bool { + let Some(generics) = generics else { + // If we'r ematching on a plain name without generics info, we ignore pattern generics. + return true; + }; + if pats.is_empty() { + // If no generics are provided, this counts as a match. + return true; + } // We don't include regions in patterns. if pats.len() != generics.types.len() + generics.const_generics.len() { return false; diff --git a/charon/tests/test-rust-name-matcher.rs b/charon/tests/test-rust-name-matcher.rs index af49648df..bdd10369a 100644 --- a/charon/tests/test-rust-name-matcher.rs +++ b/charon/tests/test-rust-name-matcher.rs @@ -45,7 +45,7 @@ fn test_name_matcher() -> anyhow::Result<()> { .filter_map(|a| parse_pattern_attr(a)) .collect_vec(); for (pass, pat) in patterns { - let passes = pat.matches(&crate_data, name); + let passes = pat.matches_item(&crate_data, item); if passes != pass { if passes { panic!( diff --git a/charon/tests/ui/rust-name-matcher-tests.rs b/charon/tests/ui/rust-name-matcher-tests.rs index 7f5c642fb..5aca0f729 100644 --- a/charon/tests/ui/rust-name-matcher-tests.rs +++ b/charon/tests/ui/rust-name-matcher-tests.rs @@ -16,15 +16,16 @@ mod foo { #[pattern::pass("test_crate::Trait")] #[pattern::fail("test_crate::Trait<_>")] -#[pattern::fail("test_crate::Trait<_, _>")] +#[pattern::pass("test_crate::Trait<_, _>")] trait Trait { #[pattern::pass("test_crate::Trait::method")] - #[pattern::fail("test_crate::Trait<_>::method")] + #[pattern::pass("test_crate::Trait<_>::method")] fn method(); } #[pattern::pass("test_crate::{impl test_crate::Trait<_> for _}")] #[pattern::pass("test_crate::{impl test_crate::Trait<_, _>}")] +#[pattern::fail("test_crate::{impl test_crate::Trait<_>}")] #[pattern::fail("test_crate::{impl test_crate::Trait<_, _> for _}")] #[pattern::pass( "test_crate::{impl test_crate::Trait> for alloc::boxed::Box<_>}" From a0c6bcbab9d87919de73a79bf17a29488abd1794 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 4 Jan 2025 19:40:04 +0100 Subject: [PATCH 2/8] Track the target of each `GenericArgs` --- charon-ml/src/CharonVersion.ml | 2 +- charon-ml/src/generated/Generated_GAst.ml | 8 -- .../src/generated/Generated_GAstOfJson.ml | 15 +++ charon-ml/src/generated/Generated_Types.ml | 17 ++- charon/Cargo.lock | 2 +- charon/Cargo.toml | 2 +- charon/src/ast/krate.rs | 6 + charon/src/ast/types.rs | 18 ++- charon/src/ast/types_utils.rs | 114 +++++++++++------- .../translate/translate_constants.rs | 9 +- .../translate/translate_functions_to_ullbc.rs | 67 ++++++---- .../translate/translate_predicates.rs | 24 ++-- .../translate/translate_traits.rs | 50 ++++++-- .../translate/translate_types.rs | 35 ++++-- charon/src/bin/generate-ml/main.rs | 3 +- charon/src/name_matcher/mod.rs | 2 +- charon/src/pretty/fmt_with_ctx.rs | 2 + charon/src/transform/check_generics.rs | 4 +- .../src/transform/index_to_function_calls.rs | 2 +- .../transform/insert_assign_return_unit.rs | 7 +- charon/src/transform/ops_to_function_calls.rs | 2 + 21 files changed, 275 insertions(+), 116 deletions(-) diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index 91d3ad308..e312aef44 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/charon-ml/src/CharonVersion.ml @@ -1,3 +1,3 @@ (* This is an automatically generated file, generated from `charon/Cargo.toml`. *) (* To re-generate this file, rune `make` in the root directory *) -let supported_charon_version = "0.1.60" +let supported_charon_version = "0.1.61" diff --git a/charon-ml/src/generated/Generated_GAst.ml b/charon-ml/src/generated/Generated_GAst.ml index 010ce869e..a1803c0e6 100644 --- a/charon-ml/src/generated/Generated_GAst.ml +++ b/charon-ml/src/generated/Generated_GAst.ml @@ -113,14 +113,6 @@ and call = { func : fn_operand; args : operand list; dest : place } *) and assertion = { cond : operand; expected : bool } -(** The id of a translated item. *) -and any_decl_id = - | IdType of type_decl_id - | IdFun of fun_decl_id - | IdGlobal of global_decl_id - | IdTraitDecl of trait_decl_id - | IdTraitImpl of trait_impl_id - and closure_kind = Fn | FnMut | FnOnce (** Additional information for closures. diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index a28270add..6222a4567 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -1057,6 +1057,20 @@ and trait_type_constraint_of_json (ctx : of_json_ctx) (js : json) : Ok ({ trait_ref; type_name; ty } : trait_type_constraint) | _ -> Error "") +and generics_source_of_json (ctx : of_json_ctx) (js : json) : + (generics_source, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | `Assoc [ ("Item", item) ] -> + let* item = any_decl_id_of_json ctx item in + Ok (Item item) + | `Assoc [ ("Method", `List [ x_0; x_1 ]) ] -> + let* x_0 = trait_decl_id_of_json ctx x_0 in + let* x_1 = trait_item_name_of_json ctx x_1 in + Ok (Method (x_0, x_1)) + | `String "Builtin" -> Ok Builtin + | _ -> Error "") + and generic_args_of_json (ctx : of_json_ctx) (js : json) : (generic_args, string) result = combine_error_msgs js __FUNCTION__ @@ -1067,6 +1081,7 @@ and generic_args_of_json (ctx : of_json_ctx) (js : json) : ("types", types); ("const_generics", const_generics); ("trait_refs", trait_refs); + ("target", _); ] -> let* regions = vector_of_json region_id_of_json region_of_json ctx regions diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index d0c6a6eaf..261470f09 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -298,8 +298,16 @@ class virtual ['self] mapreduce_const_generic_base = fun _ x -> (x, self#zero) end +(** The id of a translated item. *) +type any_decl_id = + | IdType of type_decl_id + | IdFun of fun_decl_id + | IdGlobal of global_decl_id + | IdTraitDecl of trait_decl_id + | IdTraitImpl of trait_impl_id + (** Const Generic Values. Either a primitive value, or a variable corresponding to a primitve value *) -type const_generic = +and const_generic = | CgGlobal of global_decl_id (** A global constant *) | CgVar of const_generic_var_id de_bruijn_var (** A const generic variable *) | CgValue of literal (** A concrete value *) @@ -549,6 +557,13 @@ and trait_impl_ref = { impl_generics : generic_args; } +(** Each `GenericArgs` is meant for a corresponding `GenericParams`; this describes which one. *) +and generics_source = + | Item of any_decl_id (** A top-level item. *) + | Method of trait_decl_id * trait_item_name (** A trait method. *) + | Builtin (** A builtin item like `Box`. *) + +(** A set of generic arguments. *) and generic_args = { regions : region list; types : ty list; diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 4535df235..c7fb22fc0 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -213,7 +213,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.60" +version = "0.1.61" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 8579aee20..5d060a000 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.60" +version = "0.1.61" authors = ["Son Ho "] edition = "2021" license = "Apache-2.0" diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index e6bcca84c..6d6c952a8 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -218,6 +218,12 @@ impl<'ctx> AnyTransItem<'ctx> { } } + /// See [`GenericParams::identity_args`]. + pub fn identity_args(&self) -> GenericArgs { + self.generic_params() + .identity_args(GenericsSource::Item(self.id())) + } + /// We can't implement `AstVisitable` because of the `'static` constraint, but it's ok because /// `AnyTransItem` isn't contained in any of our types. pub fn drive(&self, visitor: &mut V) -> ControlFlow { diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 7f29b2e3f..e6b4b67d4 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -195,13 +195,29 @@ pub struct TraitTypeConstraint { pub ty: Ty, } -#[derive(Default, Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)] +/// Each `GenericArgs` is meant for a corresponding `GenericParams`; this describes which one. +#[derive(Debug, Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)] +pub enum GenericsSource { + /// A top-level item. + Item(AnyTransId), + /// A trait method. + Method(TraitDeclId, TraitItemName), + /// A builtin item like `Box`. + Builtin, +} + +/// A set of generic arguments. +#[derive(Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)] pub struct GenericArgs { pub regions: Vector, pub types: Vector, pub const_generics: Vector, // TODO: rename to match [GenericParams]? pub trait_refs: Vector, + #[charon::opaque] + #[drive(skip)] + /// Each `GenericArgs` is meant for a corresponding `GenericParams`; this records which one. + pub target: GenericsSource, } /// A value of type `T` bound by regions. We should use `binder` instead but this causes name clash diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 7b7aac53f..e6e16bee7 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -5,6 +5,7 @@ use derive_generic_visitor::*; use std::collections::HashSet; use std::convert::Infallible; use std::iter::Iterator; +use std::mem; use std::ops::Index; impl GenericParams { @@ -71,12 +72,12 @@ impl GenericParams { /// Construct a set of generic arguments in the scope of `self` that matches `self` and feeds /// each required parameter with itself. E.g. given parameters for ` where U: /// PartialEq`, the arguments would be `[@TraitClause0]`. - pub fn identity_args(&self) -> GenericArgs { - self.identity_args_at_depth(DeBruijnId::zero()) + pub fn identity_args(&self, target: GenericsSource) -> GenericArgs { + self.identity_args_at_depth(target, DeBruijnId::zero()) } /// Like `identity_args` but uses variables bound at the given depth. - pub fn identity_args_at_depth(&self, depth: DeBruijnId) -> GenericArgs { + pub fn identity_args_at_depth(&self, target: GenericsSource, depth: DeBruijnId) -> GenericArgs { GenericArgs { regions: self .regions @@ -91,25 +92,7 @@ impl GenericParams { kind: TraitRefKind::Clause(DeBruijnVar::bound(depth, id)), trait_decl_ref: clause.trait_.clone(), }), - } - } - - /// Like `identity_args`, but uses free variables instead of bound ones. - pub fn free_identity_args(&self) -> GenericArgs { - GenericArgs { - regions: self - .regions - .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::free(id))), - types: self - .types - .map_ref_indexed(|id, _| TyKind::TypeVar(DeBruijnVar::free(id)).into_ty()), - const_generics: self - .const_generics - .map_ref_indexed(|id, _| ConstGeneric::Var(DeBruijnVar::free(id))), - trait_refs: self.trait_clauses.map_ref_indexed(|id, clause| TraitRef { - kind: TraitRefKind::Clause(DeBruijnVar::free(id)), - trait_decl_ref: clause.trait_.clone(), - }), + target, } } } @@ -142,6 +125,7 @@ impl GenericArgs { types, const_generics, trait_refs, + target: _, } = self; regions.len() + types.len() + const_generics.len() + trait_refs.len() } @@ -150,14 +134,20 @@ impl GenericArgs { self.len() == 0 } - pub fn empty() -> Self { - GenericArgs::default() + pub fn empty(target: GenericsSource) -> Self { + GenericArgs { + regions: Default::default(), + types: Default::default(), + const_generics: Default::default(), + trait_refs: Default::default(), + target, + } } - pub fn new_from_types(types: Vector) -> Self { + pub fn new_for_builtin(types: Vector) -> Self { GenericArgs { types, - ..Self::default() + ..Self::empty(GenericsSource::Builtin) } } @@ -166,15 +156,23 @@ impl GenericArgs { types: Vector, const_generics: Vector, trait_refs: Vector, + target: GenericsSource, ) -> Self { Self { regions, types, const_generics, trait_refs, + target, } } + /// Changes the target. + pub fn with_target(mut self, target: GenericsSource) -> Self { + self.target = target; + self + } + /// Check whether this matches the given `GenericParams`. /// TODO: check more things, e.g. that the trait refs use the correct trait and generics. pub fn matches(&self, params: &GenericParams) -> bool { @@ -189,43 +187,38 @@ impl GenericArgs { /// because the first type argument is the type for which the trait is /// implemented. pub fn pop_first_type_arg(&self) -> (Ty, Self) { - let GenericArgs { - regions, - types, - const_generics, - trait_refs, - } = self; - let mut it = types.iter(); - let ty = it.next().unwrap().clone(); - let types = it.cloned().collect(); - ( - ty, - GenericArgs { - regions: regions.clone(), - types, - const_generics: const_generics.clone(), - trait_refs: trait_refs.clone(), - }, - ) + let mut generics = self.clone(); + let mut it = mem::take(&mut generics.types).into_iter(); + let ty = it.next().unwrap(); + generics.types = it.collect(); + (ty, generics) } /// Concatenate this set of arguments with another one. Use with care, you must manage the /// order of arguments correctly. - pub fn concat(mut self, other: &Self) -> Self { + pub fn concat(mut self, target: GenericsSource, other: &Self) -> Self { let Self { regions, types, const_generics, trait_refs, + target: _, } = other; self.regions.extend_from_slice(regions); self.types.extend_from_slice(types); self.const_generics.extend_from_slice(const_generics); self.trait_refs.extend_from_slice(trait_refs); + self.target = target; self } } +impl GenericsSource { + pub fn item>(id: I) -> Self { + Self::Item(id.into()) + } +} + impl IntegerTy { pub fn is_signed(&self) -> bool { matches!( @@ -278,7 +271,7 @@ impl Ty { /// Return the unit type pub fn mk_unit() -> Ty { - TyKind::Adt(TypeId::Tuple, GenericArgs::empty()).into_ty() + TyKind::Adt(TypeId::Tuple, GenericArgs::empty(GenericsSource::Builtin)).into_ty() } /// Return true if this is a scalar type @@ -381,6 +374,35 @@ impl std::ops::Deref for Ty { /// For deref patterns. unsafe impl std::ops::DerefPure for Ty {} +impl TypeId { + pub fn generics_target(&self) -> GenericsSource { + match *self { + TypeId::Adt(decl_id) => GenericsSource::item(decl_id), + TypeId::Tuple | TypeId::Builtin(..) => GenericsSource::Builtin, + } + } +} + +impl FunId { + pub fn generics_target(&self) -> GenericsSource { + match *self { + FunId::Regular(fun_id) => GenericsSource::item(fun_id), + FunId::Builtin(..) => GenericsSource::Builtin, + } + } +} + +impl FunIdOrTraitMethodRef { + pub fn generics_target(&self) -> GenericsSource { + match self { + FunIdOrTraitMethodRef::Fun(fun_id) => fun_id.generics_target(), + FunIdOrTraitMethodRef::Trait(trait_ref, name, _) => { + GenericsSource::Method(trait_ref.trait_decl_ref.skip_binder.trait_id, name.clone()) + } + } + } +} + impl Field { /// The new name for this field, as suggested by the `#[charon::rename]` attribute. pub fn renamed_name(&self) -> Option<&str> { diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs index 2c394e5cc..c4602c2be 100644 --- a/charon/src/bin/charon-driver/translate/translate_constants.rs +++ b/charon/src/bin/charon-driver/translate/translate_constants.rs @@ -112,9 +112,14 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { generics, trait_refs ); - let generics = self.translate_generic_args(span, generics, trait_refs, None)?; - let global_id = self.register_global_decl_id(span, id); + let generics = self.translate_generic_args( + span, + generics, + trait_refs, + None, + GenericsSource::item(global_id), + )?; RawConstantExpr::Global(GlobalDeclRef { id: global_id, generics, diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs index 31bd020c3..febc01d41 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs @@ -127,13 +127,15 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { overrides_default, .. } => { + let impl_id = self.register_trait_impl_id(span, impl_id); let impl_ref = TraitImplRef { - impl_id: self.register_trait_impl_id(span, impl_id), + impl_id, generics: self.translate_generic_args( span, impl_generics, impl_required_impl_exprs, None, + GenericsSource::item(impl_id), )?, }; let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?; @@ -648,7 +650,12 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { )) } hax::AggregateKind::Tuple => Ok(Rvalue::Aggregate( - AggregateKind::Adt(TypeId::Tuple, None, None, GenericArgs::empty()), + AggregateKind::Adt( + TypeId::Tuple, + None, + None, + GenericArgs::empty(GenericsSource::Builtin), + ), operands_t, )), hax::AggregateKind::Adt( @@ -666,13 +673,18 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // types we need. let _ = user_annotation; - // Translate the substitution - let generics = - self.translate_generic_args(span, substs, trait_refs, None)?; - let type_id = self.translate_type_id(span, adt_id)?; // Sanity check - matches!(&type_id, TypeId::Adt(_)); + assert!(matches!(&type_id, TypeId::Adt(_))); + + // Translate the substitution + let generics = self.translate_generic_args( + span, + substs, + trait_refs, + None, + type_id.generics_target(), + )?; use hax::AdtKind; let variant_id = match kind { @@ -694,6 +706,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { closure_args.tupled_sig ); + let fun_id = self.register_fun_decl_id(span, def_id); + // Retrieve the late-bound variables. let binder = closure_args.tupled_sig.as_ref().rebind(()); // Translate the substitution @@ -702,10 +716,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { &closure_args.parent_args, &closure_args.parent_trait_refs, Some(binder), + GenericsSource::item(fun_id), )?; - let def_id = self.register_fun_decl_id(span, def_id); - let akind = AggregateKind::Closure(def_id, generics); + let akind = AggregateKind::Closure(fun_id, generics); Ok(Rvalue::Aggregate(akind, operands_t)) } @@ -782,14 +796,6 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { _ => None, }; - // Translate the type parameters - let generics = self.translate_generic_args(span, substs, trait_refs, binder)?; - - // Translate the arguments - let args = args - .map(|args| self.translate_arguments(span, args)) - .transpose()?; - // Trait information trace!( "Trait information:\n- def_id: {:?}\n- impl source:\n{:?}", @@ -804,7 +810,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // Check if the function is considered primitive: primitive // functions benefit from special treatment. - let func = if let Some(builtin_fun) = builtin_fun { + let fun_id = if let Some(builtin_fun) = builtin_fun { // Primitive function. // // Note that there are subtleties with regards to the way types parameters @@ -859,8 +865,26 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { } } }; + + // Translate the type parameters + let generics = self.translate_generic_args( + span, + substs, + trait_refs, + binder, + fun_id.generics_target(), + )?; + + // Translate the arguments + let args = args + .map(|args| self.translate_arguments(span, args)) + .transpose()?; + let sfid = SubstFunId { - func: FnPtr { func, generics }, + func: FnPtr { + func: fun_id, + generics, + }, args, }; Ok(SubstFunIdOrPanic::Fun(sfid)) @@ -1321,7 +1345,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { TypeId::Adt(adt_decl_id), variant, None, - sig.generics.identity_args(), + sig.generics + .identity_args(GenericsSource::item(adt_decl_id)), ), args, ), @@ -1486,7 +1511,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { let state_ty = { // Group the state types into a tuple let state_ty = - TyKind::Adt(TypeId::Tuple, GenericArgs::new_from_types(state.clone())) + TyKind::Adt(TypeId::Tuple, GenericArgs::new_for_builtin(state.clone())) .into_ty(); // Depending on the kind of the closure, add a reference match &kind { diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index 771faa95d..874e71689 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -37,15 +37,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { Ok(()) } - pub(crate) fn translate_trait_decl_ref( + pub(crate) fn translate_poly_trait_ref( &mut self, span: Span, bound_trait_ref: &hax::Binder, ) -> Result { self.translate_region_binder(span, bound_trait_ref, move |ctx, trait_ref| { - let trait_id = ctx.register_trait_decl_id(span, &trait_ref.def_id); - let generics = ctx.translate_generic_args(span, &trait_ref.generic_args, &[], None)?; - Ok(TraitDeclRef { trait_id, generics }) + ctx.translate_trait_ref(span, trait_ref) }) } @@ -66,7 +64,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { ) -> Result { let trait_id = self.register_trait_decl_id(span, &trait_ref.def_id); // For now a trait has no required bounds, so we pass an empty list. - let generics = self.translate_generic_args(span, &trait_ref.generic_args, &[], None)?; + let generics = self.translate_generic_args( + span, + &trait_ref.generic_args, + &[], + None, + GenericsSource::item(trait_id), + )?; Ok(TraitDeclRef { trait_id, generics }) } @@ -188,7 +192,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { span: Span, impl_expr: &hax::ImplExpr, ) -> Result { - let trait_decl_ref = self.translate_trait_decl_ref(span, &impl_expr.r#trait)?; + let trait_decl_ref = self.translate_poly_trait_ref(span, &impl_expr.r#trait)?; match self.translate_trait_impl_expr_aux(span, impl_expr, trait_decl_ref.clone()) { Ok(res) => Ok(res), @@ -223,7 +227,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { generics, } => { let impl_id = self.register_trait_impl_id(span, impl_def_id); - let generics = self.translate_generic_args(span, generics, nested, None)?; + let generics = self.translate_generic_args( + span, + generics, + nested, + None, + GenericsSource::item(impl_id), + )?; TraitRef { kind: TraitRefKind::TraitImpl(impl_id, generics), trait_decl_ref, diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index 22ebd7912..e919ff32b 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -95,12 +95,13 @@ impl BodyTransCtx<'_, '_> { let fun_generics = bt_ctx .outermost_binder() .params - .identity_args_at_depth(DeBruijnId::one()) + .identity_args_at_depth(GenericsSource::item(def_id), DeBruijnId::one()) .concat( - &bt_ctx - .innermost_binder() - .params - .identity_args_at_depth(DeBruijnId::zero()), + GenericsSource::item(fun_id), + &bt_ctx.innermost_binder().params.identity_args_at_depth( + GenericsSource::Method(def_id.into(), item_name.clone()), + DeBruijnId::zero(), + ), ); Ok(FunDeclRef { id: fun_id, @@ -120,9 +121,11 @@ impl BodyTransCtx<'_, '_> { if hax_item.has_value { // The parameters of the constant are the same as those of the item that // declares them. + let id = self.register_global_decl_id(item_span, item_def_id); + let generics_target = GenericsSource::item(id); let gref = GlobalDeclRef { - id: self.register_global_decl_id(item_span, item_def_id), - generics: self.the_only_binder().params.identity_args(), + id, + generics: self.the_only_binder().params.identity_args(generics_target), }; const_defaults.insert(item_name.clone(), gref); }; @@ -211,8 +214,13 @@ impl BodyTransCtx<'_, '_> { let trait_id = self.register_trait_decl_id(span, implemented_trait_id); let implemented_trait = { let implemented_trait = &trait_pred.trait_ref; - let generics = - self.translate_generic_args(span, &implemented_trait.generic_args, &[], None)?; + let generics = self.translate_generic_args( + span, + &implemented_trait.generic_args, + &[], + None, + GenericsSource::item(trait_id), + )?; TraitDeclRef { trait_id, generics } }; @@ -256,12 +264,22 @@ impl BodyTransCtx<'_, '_> { let fun_generics = bt_ctx .outermost_binder() .params - .identity_args_at_depth(DeBruijnId::one()) + .identity_args_at_depth( + GenericsSource::item(def_id), + DeBruijnId::one(), + ) .concat( + GenericsSource::item(fun_id), &bt_ctx .innermost_binder() .params - .identity_args_at_depth(DeBruijnId::zero()), + .identity_args_at_depth( + GenericsSource::Method( + trait_id.into(), + name.clone(), + ), + DeBruijnId::zero(), + ), ); Ok(FunDeclRef { id: fun_id, @@ -282,11 +300,17 @@ impl BodyTransCtx<'_, '_> { } hax::FullDefKind::AssocConst { .. } => { let id = self.register_global_decl_id(item_span, item_def_id); + let generics_target = GenericsSource::item(id); // The parameters of the constant are the same as those of the item that // declares them. let generics = match &impl_item.value { - Provided { .. } => self.the_only_binder().params.identity_args(), - _ => implemented_trait.generics.clone(), + Provided { .. } => { + self.the_only_binder().params.identity_args(generics_target) + } + _ => implemented_trait + .generics + .clone() + .with_target(generics_target), }; let gref = GlobalDeclRef { id, generics }; consts.push((name, gref)); diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 04c57fb12..34541ebb6 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -144,12 +144,18 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { } => { trace!("Adt: {:?}", def_id); - // Translate the type parameters instantiation - let mut generics = self.translate_generic_args(span, substs, trait_refs, None)?; - // Retrieve the type identifier let type_id = self.translate_type_id(span, def_id)?; + // Translate the type parameters instantiation + let mut generics = self.translate_generic_args( + span, + substs, + trait_refs, + None, + type_id.generics_target(), + )?; + // Filter the type arguments. // TODO: do this in a micro-pass if let TypeId::Builtin(builtin_ty) = type_id { @@ -171,7 +177,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { trace!("Str"); let id = TypeId::Builtin(BuiltinTy::Str); - TyKind::Adt(id, GenericArgs::empty()) + TyKind::Adt(id, GenericArgs::empty(GenericsSource::Builtin)) } hax::TyKind::Array(ty, const_param) => { trace!("Array"); @@ -180,14 +186,23 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { let tys = vec![self.translate_ty(span, ty)?].into(); let cgs = vec![c].into(); let id = TypeId::Builtin(BuiltinTy::Array); - TyKind::Adt(id, GenericArgs::new(Vector::new(), tys, cgs, Vector::new())) + TyKind::Adt( + id, + GenericArgs::new( + Vector::new(), + tys, + cgs, + Vector::new(), + GenericsSource::Builtin, + ), + ) } hax::TyKind::Slice(ty) => { trace!("Slice"); let tys = vec![self.translate_ty(span, ty)?].into(); let id = TypeId::Builtin(BuiltinTy::Slice); - TyKind::Adt(id, GenericArgs::new_from_types(tys)) + TyKind::Adt(id, GenericArgs::new_for_builtin(tys)) } hax::TyKind::Ref(region, ty, mutability) => { trace!("Ref"); @@ -220,7 +235,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { params.push(param_ty); } - TyKind::Adt(TypeId::Tuple, GenericArgs::new_from_types(params)) + TyKind::Adt(TypeId::Tuple, GenericArgs::new_for_builtin(params)) } hax::TyKind::Param(param) => { @@ -240,8 +255,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { hax::TyKind::Foreign(def_id) => { trace!("Foreign"); - let def_id = self.translate_type_id(span, def_id)?; - TyKind::Adt(def_id, GenericArgs::empty()) + let adt_id = self.translate_type_id(span, def_id)?; + TyKind::Adt(adt_id, GenericArgs::empty(adt_id.generics_target())) } hax::TyKind::Infer(_) => { trace!("Infer"); @@ -310,6 +325,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { substs: &[hax::GenericArg], trait_refs: &[hax::ImplExpr], late_bound: Option>, + target: GenericsSource, ) -> Result { use hax::GenericArg::*; trace!("{:?}", substs); @@ -353,6 +369,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { types, const_generics, trait_refs, + target, }) } diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index b60bd70fc..8941ac338 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1118,7 +1118,6 @@ fn generate_ml( extra_types: &[], })), &[ "Var", - "AnyTransId", "FnOperand", "Call", "Assert", @@ -1253,6 +1252,7 @@ fn generate_ml( "type_var_id", ], })), &[ + "AnyTransId", "ConstGeneric", ]), // Can't merge into above because aeneas uses the above alongside their own partial @@ -1276,6 +1276,7 @@ fn generate_ml( "TraitImplRef", "FunDeclRef", "GlobalDeclRef", + "GenericsSource", "GenericArgs", ]), // TODO: can't merge into above because of field name clashes (`types`, `regions` etc). diff --git a/charon/src/name_matcher/mod.rs b/charon/src/name_matcher/mod.rs index 1815d7e4e..d521c9e89 100644 --- a/charon/src/name_matcher/mod.rs +++ b/charon/src/name_matcher/mod.rs @@ -53,7 +53,7 @@ impl Pattern { } pub fn matches_item(&self, ctx: &TranslatedCrate, item: AnyTransItem<'_>) -> bool { - let generics = item.generic_params().identity_args(); + let generics = item.identity_args(); let name = &item.item_meta().name; self.matches_with_generics(ctx, name, Some(&generics)) } diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 962317ab6..fe4b05439 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -304,6 +304,7 @@ impl GenericArgs { types, const_generics, trait_refs: _, + target: _, } = self; for x in regions { params.push(x.fmt_with_ctx(ctx)); @@ -327,6 +328,7 @@ impl GenericArgs { types, const_generics, trait_refs, + target: _, } = self; for x in regions { params.push(x.fmt_with_ctx(ctx)); diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index 964c92089..a91e1c006 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -37,7 +37,9 @@ impl CheckGenericsVisitor<'_> { } } fn generics_should_match_item(&mut self, args: &GenericArgs, item_id: impl Into) { - if let Some(item) = self.translated.get_item(item_id.into()) { + let item_id = item_id.into(); + assert_eq!(args.target, GenericsSource::item(item_id)); + if let Some(item) = self.translated.get_item(item_id) { let params = item.generic_params(); self.generics_should_match(args, params); } else { diff --git a/charon/src/transform/index_to_function_calls.rs b/charon/src/transform/index_to_function_calls.rs index 92bb78751..41d5a32e2 100644 --- a/charon/src/transform/index_to_function_calls.rs +++ b/charon/src/transform/index_to_function_calls.rs @@ -70,7 +70,7 @@ impl<'a> IndexVisitor<'a> { } else { TyKind::Adt( TypeId::Builtin(BuiltinTy::Slice), - GenericArgs::new_from_types(vec![elem_ty].into()), + GenericArgs::new_for_builtin(vec![elem_ty].into()), ) .into_ty() }; diff --git a/charon/src/transform/insert_assign_return_unit.rs b/charon/src/transform/insert_assign_return_unit.rs index 5a04bdf0a..00c7864fe 100644 --- a/charon/src/transform/insert_assign_return_unit.rs +++ b/charon/src/transform/insert_assign_return_unit.rs @@ -12,7 +12,12 @@ fn transform_st(locals: &Locals, st: &mut Statement) -> Vec { if let RawStatement::Return = &mut st.content { let ret_place = locals.return_place(); let unit_value = Rvalue::Aggregate( - AggregateKind::Adt(TypeId::Tuple, None, None, GenericArgs::empty()), + AggregateKind::Adt( + TypeId::Tuple, + None, + None, + GenericArgs::empty(GenericsSource::Builtin), + ), Vec::new(), ); let assign_st = Statement::new(st.span, RawStatement::Assign(ret_place, unit_value)); diff --git a/charon/src/transform/ops_to_function_calls.rs b/charon/src/transform/ops_to_function_calls.rs index 64fa918bd..478db4940 100644 --- a/charon/src/transform/ops_to_function_calls.rs +++ b/charon/src/transform/ops_to_function_calls.rs @@ -23,6 +23,7 @@ fn transform_st(s: &mut Statement) { vec![ty.clone()].into(), vec![cg.clone()].into(), vec![].into(), + GenericsSource::Builtin, ); let func = FnOperand::Regular(FnPtr { func, generics }); s.content = RawStatement::Call(Call { @@ -42,6 +43,7 @@ fn transform_st(s: &mut Statement) { vec![ty.clone()].into(), vec![cg.clone()].into(), vec![].into(), + GenericsSource::Builtin, ); let func = FnOperand::Regular(FnPtr { func, generics }); s.content = RawStatement::Call(Call { From 135dccd7f97f81a7421f0bcf5cba5fd31a41f719 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 4 Jan 2025 21:50:54 +0100 Subject: [PATCH 3/8] Simplify `check_generics` --- charon/src/transform/check_generics.rs | 170 ++++++------------------- 1 file changed, 42 insertions(+), 128 deletions(-) diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index a91e1c006..04913f4a5 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -10,143 +10,61 @@ use super::{ctx::TransformPass, TransformCtx}; struct CheckGenericsVisitor<'a> { translated: &'a TranslatedCrate, error_ctx: &'a mut ErrorCtx, - // Count how many `GenericArgs` we handled. This is to make sure we don't miss one. - discharged_args: u32, // Tracks an enclosing span to make errors useful. - item_span: Span, + span: Span, } impl CheckGenericsVisitor<'_> { fn error(&mut self, message: impl Display) { - let span = self.item_span; let message = message.to_string(); - register_error_or_panic!(self.error_ctx, self.translated, span, message); - } - - /// Count that we just discharged one instance of `GenericArgs`. - fn discharged_one_generics(&mut self) { - self.discharged_args += 1; - } - - fn generics_should_match(&mut self, args: &GenericArgs, params: &GenericParams) { - self.discharged_one_generics(); - if !args.matches(params) { - self.error(format!( - "Mismatched generics:\nexpected: {params:?}\n got: {args:?}" - )) - } - } - fn generics_should_match_item(&mut self, args: &GenericArgs, item_id: impl Into) { - let item_id = item_id.into(); - assert_eq!(args.target, GenericsSource::item(item_id)); - if let Some(item) = self.translated.get_item(item_id) { - let params = item.generic_params(); - self.generics_should_match(args, params); - } else { - self.discharged_one_generics(); - } - } - fn check_typeid_generics(&mut self, args: &GenericArgs, ty_kind: &TypeId) { - match ty_kind { - TypeId::Adt(id) => self.generics_should_match_item(args, *id), - TypeId::Tuple => { - self.discharged_one_generics(); - if !(args.regions.is_empty() - && args.const_generics.is_empty() - && args.trait_refs.is_empty()) - { - self.error("Mismatched generics: generics for a tuple should be only types") - } - } - TypeId::Builtin(..) => { - // TODO: check generics for built-in types - self.discharged_one_generics() - } - } + register_error_or_panic!(self.error_ctx, self.translated, self.span, message); } } -// Visitor functions impl VisitAst for CheckGenericsVisitor<'_> { - fn enter_aggregate_kind(&mut self, agg: &AggregateKind) { + fn visit_aggregate_kind(&mut self, agg: &AggregateKind) -> ControlFlow { match agg { - AggregateKind::Adt(kind, _, _, args) => { - self.check_typeid_generics(args, kind); - } - AggregateKind::Closure(_id, _args) => { + AggregateKind::Adt(..) => self.visit_inner(agg)?, + AggregateKind::Closure(_id, args) => { // TODO(#194): handle closure generics properly - // self.generics_should_match_item(args, *id); - self.discharged_one_generics() + // This does not visit the args themselves, only their contents, because we mess up + // closure generics for now. + self.visit_inner(args)? } - AggregateKind::Array(..) => {} - } - } - fn enter_fn_ptr(&mut self, fn_ptr: &FnPtr) { - match &fn_ptr.func { - FunIdOrTraitMethodRef::Fun(FunId::Regular(id)) => { - let args = &fn_ptr.generics; - self.generics_should_match_item(args, *id); - } - FunIdOrTraitMethodRef::Trait(tref, method, _) => { - let trait_id = tref.trait_decl_ref.skip_binder.trait_id; - if let Some(trait_decl) = self.translated.trait_decls.get(trait_id) { - if let Some((_, bound_fn)) = trait_decl - .required_methods - .iter() - .chain(trait_decl.provided_methods.iter()) - .find(|(n, _)| n == method) - { - // Function generics should match expected method generics. - self.generics_should_match(&fn_ptr.generics, &bound_fn.params); - } else { - self.discharged_one_generics() - } - } else { - self.discharged_one_generics() - } - } - FunIdOrTraitMethodRef::Fun(FunId::Builtin(..)) => { - // TODO: check generics for built-in types - self.discharged_one_generics() - } - } - } - fn enter_fun_decl_ref(&mut self, fun_ref: &FunDeclRef) { - self.generics_should_match_item(&fun_ref.generics, fun_ref.id); - } - fn enter_global_decl_ref(&mut self, global_ref: &GlobalDeclRef) { - self.generics_should_match_item(&global_ref.generics, global_ref.id); - } - fn enter_trait_decl_ref(&mut self, tref: &TraitDeclRef) { - self.generics_should_match_item(&tref.generics, tref.trait_id); - } - fn enter_trait_impl_ref(&mut self, impl_ref: &TraitImplRef) { - self.generics_should_match_item(&impl_ref.generics, impl_ref.impl_id); - } - fn enter_trait_ref(&mut self, tref: &TraitRef) { - match &tref.kind { - TraitRefKind::TraitImpl(id, args) => self.generics_should_match_item(args, *id), - TraitRefKind::BuiltinOrAuto(..) - | TraitRefKind::Dyn(..) - | TraitRefKind::Clause(..) - | TraitRefKind::ParentClause(..) - | TraitRefKind::ItemClause(..) - | TraitRefKind::SelfId - | TraitRefKind::Unknown(_) => {} - } - } - fn enter_ty(&mut self, ty: &Ty) { - if let TyKind::Adt(kind, args) = ty.kind() { - self.check_typeid_generics(args, kind); + AggregateKind::Array(..) => self.visit_inner(agg)?, } + Continue(()) } fn enter_generic_args(&mut self, args: &GenericArgs) { - if self.discharged_args == 0 { - // Ensure we counted all `GenericArgs` - panic!("Unexpected `GenericArgs` in the AST! {args:?}") + let params = match &args.target { + GenericsSource::Item(item_id) => { + let Some(item) = self.translated.get_item(*item_id) else { + return; + }; + item.generic_params() + } + GenericsSource::Method(trait_id, method_name) => { + let Some(trait_decl) = self.translated.trait_decls.get(*trait_id) else { + return; + }; + let Some((_, bound_fn)) = trait_decl + .required_methods + .iter() + .chain(trait_decl.provided_methods.iter()) + .find(|(n, _)| n == method_name) + else { + return; + }; + &bound_fn.params + } + GenericsSource::Builtin => return, + }; + if !args.matches(params) { + self.error(format!( + "Mismatched generics:\nexpected: {params:?}\n got: {args:?}" + )) } - self.discharged_args -= 1; } // Special case that is not represented as a `GenericArgs`. @@ -178,10 +96,11 @@ impl VisitAst for CheckGenericsVisitor<'_> { } fn visit_llbc_statement(&mut self, st: &Statement) -> ControlFlow { - let old_span = self.item_span; - self.item_span = st.span; + // Track span for more precise error messages. + let old_span = self.span; + self.span = st.span; self.visit_inner(st)?; - self.item_span = old_span; + self.span = old_span; Continue(()) } } @@ -193,14 +112,9 @@ impl TransformPass for Check { let mut visitor = CheckGenericsVisitor { translated: &ctx.translated, error_ctx: &mut ctx.errors, - discharged_args: 0, - item_span: item.item_meta().span, + span: item.item_meta().span, }; item.drive(&mut visitor); - assert_eq!( - visitor.discharged_args, 0, - "Got confused about `GenericArgs` locations" - ); } } } From 17d754e2b7aaaf23dfec38e4f6e3e8c3f4735d38 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 4 Jan 2025 20:56:38 +0100 Subject: [PATCH 4/8] Run `check_generics` before transformation passes too --- charon/src/transform/check_generics.rs | 7 +++++-- charon/src/transform/mod.rs | 4 +++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index 04913f4a5..e2e5ca116 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -9,6 +9,7 @@ use super::{ctx::TransformPass, TransformCtx}; #[derive(Visitor)] struct CheckGenericsVisitor<'a> { translated: &'a TranslatedCrate, + phase: &'static str, error_ctx: &'a mut ErrorCtx, // Tracks an enclosing span to make errors useful. span: Span, @@ -16,7 +17,7 @@ struct CheckGenericsVisitor<'a> { impl CheckGenericsVisitor<'_> { fn error(&mut self, message: impl Display) { - let message = message.to_string(); + let message = format!("Found inconsistent generics {}:\n{message}", self.phase); register_error_or_panic!(self.error_ctx, self.translated, self.span, message); } } @@ -105,13 +106,15 @@ impl VisitAst for CheckGenericsVisitor<'_> { } } -pub struct Check; +// The argument is a name to disambiguate the two times we run this check. +pub struct Check(pub &'static str); impl TransformPass for Check { fn transform_ctx(&self, ctx: &mut TransformCtx) { for item in ctx.translated.all_items() { let mut visitor = CheckGenericsVisitor { translated: &ctx.translated, error_ctx: &mut ctx.errors, + phase: self.0, span: item.item_meta().span, }; item.drive(&mut visitor); diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index 7ba3daf3b..c5fb9e4ae 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -37,6 +37,8 @@ use Pass::*; pub static ULLBC_PASSES: &[Pass] = &[ // Move clauses on associated types to be parent clauses NonBody(&lift_associated_item_clauses::Transform), + // Check that all supplied generic types match the corresponding generic parameters. + NonBody(&check_generics::Check("after translation")), // # Micro-pass: hide some overly-common traits we don't need: Sized, Sync, Allocator, etc.. NonBody(&hide_marker_traits::Transform), // # Micro-pass: filter the trait impls that were marked invisible since we couldn't filter @@ -125,7 +127,7 @@ pub static LLBC_PASSES: &[Pass] = &[ // comments. StructuredBody(&recover_body_comments::Transform), // Check that all supplied generic types match the corresponding generic parameters. - NonBody(&check_generics::Check), + NonBody(&check_generics::Check("after transformations")), // Use `DeBruijnVar::Free` for the variables bound in item signatures. NonBody(&unbind_item_vars::Check), ]; From e7230d3e2eb03bd58733966c9c32412b0ffbe563 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 5 Jan 2025 20:46:30 +0100 Subject: [PATCH 5/8] Run `check_generics` at the end even in ullbc mode --- charon/src/bin/charon-driver/driver.rs | 15 ++++++++++++--- charon/src/transform/mod.rs | 20 +++++++++++++++----- 2 files changed, 27 insertions(+), 8 deletions(-) diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index 46bf9c6cc..ad38ab2f9 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -2,7 +2,9 @@ use crate::translate::translate_crate_to_ullbc; use charon_lib::export; use charon_lib::options; use charon_lib::reorder_decls::compute_reordered_decls; -use charon_lib::transform::{LLBC_PASSES, ULLBC_PASSES}; +use charon_lib::transform::{ + FINAL_CLEANUP_PASSES, INITIAL_CLEANUP_PASSES, LLBC_PASSES, ULLBC_PASSES, +}; use charon_lib::ullbc_to_llbc; use rustc_driver::{Callbacks, Compilation}; use rustc_interface::{interface::Compiler, Queries}; @@ -231,6 +233,10 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa // serializing the result. // Run the micro-passes that clean up bodies. + for pass in INITIAL_CLEANUP_PASSES.iter() { + trace!("# Starting pass {}", pass.name()); + pass.run(&mut ctx) + } for pass in ULLBC_PASSES.iter() { trace!("# Starting pass {}", pass.name()); pass.run(&mut ctx) @@ -265,7 +271,6 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa trace!("# Starting pass {}", pass.name()); pass.run(&mut ctx) } - // # Reorder the graph of dependencies and compute the strictly // connex components to: // - compute the order in which to extract the definitions @@ -281,7 +286,11 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa } } - trace!("Done"); + // Final passes before serialization. + for pass in FINAL_CLEANUP_PASSES.iter() { + trace!("# Starting pass {}", pass.name()); + pass.run(&mut ctx) + } // Update the error count internal.error_count = ctx.errors.error_count; diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index c5fb9e4ae..295aa7417 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -34,7 +34,8 @@ pub use ctx::TransformCtx; use ctx::{LlbcPass, TransformPass, UllbcPass}; use Pass::*; -pub static ULLBC_PASSES: &[Pass] = &[ +/// Item and type cleanup passes. +pub static INITIAL_CLEANUP_PASSES: &[Pass] = &[ // Move clauses on associated types to be parent clauses NonBody(&lift_associated_item_clauses::Transform), // Check that all supplied generic types match the corresponding generic parameters. @@ -44,6 +45,14 @@ pub static ULLBC_PASSES: &[Pass] = &[ // # Micro-pass: filter the trait impls that were marked invisible since we couldn't filter // them out earlier. NonBody(&filter_invisible_trait_impls::Transform), + // # Micro-pass: whenever we call a trait method on a known type, refer to the method `FunDecl` + // directly instead of going via a `TraitRef`. This is done before `reorder_decls` to remove + // some sources of mutual recursion. + UnstructuredBody(&skip_trait_refs_when_known::Transform), +]; + +/// Body cleanup passes on the ullbc. +pub static ULLBC_PASSES: &[Pass] = &[ // # Micro-pass: merge single-origin gotos into their parent. This drastically reduces the // graph size of the CFG. UnstructuredBody(&merge_goto_chains::Transform), @@ -64,10 +73,6 @@ pub static ULLBC_PASSES: &[Pass] = &[ // # Micro-pass: desugar the constants to other values/operands as much // as possible. UnstructuredBody(&simplify_constants::Transform), - // # Micro-pass: whenever we call a trait method on a known type, refer to the method `FunDecl` - // directly instead of going via a `TraitRef`. This is done before `reorder_decls` to remove - // some sources of mutual recursion. - UnstructuredBody(&skip_trait_refs_when_known::Transform), // # Micro-pass: the first local variable of closures is the // closure itself. This is not consistent with the closure signature, // which ignores this first variable. This micro-pass updates this. @@ -91,6 +96,7 @@ pub static ULLBC_PASSES: &[Pass] = &[ UnstructuredBody(&filter_unreachable_blocks::Transform), ]; +/// Body cleanup passes after control flow reconstruction. pub static LLBC_PASSES: &[Pass] = &[ // # Micro-pass: `panic!()` expands to a new function definition each time. This pass cleans // those up. @@ -126,6 +132,10 @@ pub static LLBC_PASSES: &[Pass] = &[ // statements. This must be last after all the statement-affecting passes to avoid losing // comments. StructuredBody(&recover_body_comments::Transform), +]; + +/// Final passes to run at the end. +pub static FINAL_CLEANUP_PASSES: &[Pass] = &[ // Check that all supplied generic types match the corresponding generic parameters. NonBody(&check_generics::Check("after transformations")), // Use `DeBruijnVar::Free` for the variables bound in item signatures. From c37224b9e82b8fa8637dd01d7cf6870d62659698 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 5 Jan 2025 20:55:02 +0100 Subject: [PATCH 6/8] Make CFG reconstruction and `reorder_decls` into passes --- charon/src/bin/charon-driver/driver.rs | 17 ------ .../translate/translate_crate_to_ullbc.rs | 1 + charon/src/transform/ctx.rs | 2 + charon/src/transform/mod.rs | 7 +++ charon/src/transform/reorder_decls.rs | 12 ++++- charon/src/transform/ullbc_to_llbc.rs | 52 +++++++++++-------- 6 files changed, 51 insertions(+), 40 deletions(-) diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index ad38ab2f9..a8822d9ed 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -1,11 +1,9 @@ use crate::translate::translate_crate_to_ullbc; use charon_lib::export; use charon_lib::options; -use charon_lib::reorder_decls::compute_reordered_decls; use charon_lib::transform::{ FINAL_CLEANUP_PASSES, INITIAL_CLEANUP_PASSES, LLBC_PASSES, ULLBC_PASSES, }; -use charon_lib::ullbc_to_llbc; use rustc_driver::{Callbacks, Compilation}; use rustc_interface::{interface::Compiler, Queries}; use rustc_middle::ty::TyCtxt; @@ -258,26 +256,11 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa // - or they want the structured LLBC, in which case we reconstruct the // control-flow and apply micro-passes if !options.ullbc { - // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing - // the control flow. - ullbc_to_llbc::translate_functions(&mut ctx); - - if options.print_built_llbc { - info!("# LLBC resulting from control-flow reconstruction:\n\n{ctx}\n",); - } - // Run the micro-passes that clean up bodies. for pass in LLBC_PASSES.iter() { trace!("# Starting pass {}", pass.name()); pass.run(&mut ctx) } - // # Reorder the graph of dependencies and compute the strictly - // connex components to: - // - compute the order in which to extract the definitions - // - find the recursive definitions - // - group the mutually recursive definitions - let reordered_decls = compute_reordered_decls(&ctx); - ctx.translated.ordered_decls = Some(reordered_decls); if options.print_llbc { println!("# Final LLBC before serialization:\n\n{ctx}\n"); diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs index 8bf964364..910e25799 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs @@ -301,6 +301,7 @@ pub fn translate<'tcx, 'ctx>( no_code_duplication: options.no_code_duplication, hide_marker_traits: options.hide_marker_traits, no_merge_goto_chains: options.no_merge_goto_chains, + print_built_llbc: options.print_built_llbc, item_opacities: ctx.options.item_opacities, }; diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index 06b9d1ec2..1b586cad8 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -18,6 +18,8 @@ pub struct TransformOptions { pub hide_marker_traits: bool, /// Do not merge the chains of gotos. pub no_merge_goto_chains: bool, + /// Print the llbc just after control-flow reconstruction. + pub print_built_llbc: bool, /// List of patterns to assign a given opacity to. Same as the corresponding `TranslateOptions` /// field. pub item_opacities: Vec<(NamePattern, ItemOpacity)>, diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index 295aa7417..3eb339d93 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -98,6 +98,8 @@ pub static ULLBC_PASSES: &[Pass] = &[ /// Body cleanup passes after control flow reconstruction. pub static LLBC_PASSES: &[Pass] = &[ + // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing the control flow. + NonBody(&ullbc_to_llbc::Transform), // # Micro-pass: `panic!()` expands to a new function definition each time. This pass cleans // those up. StructuredBody(&inline_local_panic_functions::Transform), @@ -132,6 +134,11 @@ pub static LLBC_PASSES: &[Pass] = &[ // statements. This must be last after all the statement-affecting passes to avoid losing // comments. StructuredBody(&recover_body_comments::Transform), + // # Reorder the graph of dependencies and compute the strictly connex components to: + // - compute the order in which to extract the definitions + // - find the recursive definitions + // - group the mutually recursive definitions + NonBody(&reorder_decls::Transform), ]; /// Final passes to run at the end. diff --git a/charon/src/transform/reorder_decls.rs b/charon/src/transform/reorder_decls.rs index 13656fa1e..0807eaa2a 100644 --- a/charon/src/transform/reorder_decls.rs +++ b/charon/src/transform/reorder_decls.rs @@ -12,6 +12,8 @@ use serde::{Deserialize, Serialize}; use std::fmt::{Debug, Display, Error}; use std::vec::Vec; +use super::ctx::TransformPass; + /// A (group of) top-level declaration(s), properly reordered. /// "G" stands for "generic" #[derive( @@ -483,7 +485,7 @@ fn group_declarations_from_scc( reordered_decls } -pub fn compute_reordered_decls(ctx: &TransformCtx) -> DeclarationsGroups { +fn compute_reordered_decls(ctx: &TransformCtx) -> DeclarationsGroups { trace!(); // Step 1: explore the declarations to build the graph @@ -516,6 +518,14 @@ pub fn compute_reordered_decls(ctx: &TransformCtx) -> DeclarationsGroups { reordered_decls } +pub struct Transform; +impl TransformPass for Transform { + fn transform_ctx(&self, ctx: &mut TransformCtx) { + let reordered_decls = compute_reordered_decls(&ctx); + ctx.translated.ordered_decls = Some(reordered_decls); + } +} + #[cfg(test)] mod tests { #[test] diff --git a/charon/src/transform/ullbc_to_llbc.rs b/charon/src/transform/ullbc_to_llbc.rs index 57faa6e54..c6d7c167f 100644 --- a/charon/src/transform/ullbc_to_llbc.rs +++ b/charon/src/transform/ullbc_to_llbc.rs @@ -36,6 +36,8 @@ use petgraph::Direction; use std::cmp::Ordering; use std::collections::{BTreeSet, HashMap, HashSet, VecDeque}; +use super::ctx::TransformPass; + /// Control-Flow Graph type Cfg = DiGraphMap; @@ -1742,28 +1744,34 @@ fn translate_body(ctx: &mut TransformCtx, no_code_duplication: bool, body: &mut *body = Structured(tgt_body); } -/// Translate the functions by reconstructing the control-flow. -pub fn translate_functions(ctx: &mut TransformCtx) { - // Translate the bodies one at a time. - ctx.for_each_body(|ctx, body| { - translate_body(ctx, ctx.options.no_code_duplication, body); - }); +pub struct Transform; +impl TransformPass for Transform { + fn transform_ctx(&self, ctx: &mut TransformCtx) { + // Translate the bodies one at a time. + ctx.for_each_body(|ctx, body| { + translate_body(ctx, ctx.options.no_code_duplication, body); + }); - // Print the functions - let fmt_ctx = ctx.into_fmt(); - for fun in &ctx.translated.fun_decls { - trace!( - "# Signature:\n{}\n\n# Function definition:\n{}\n", - fmt_ctx.format_object(&fun.signature), - fmt_ctx.format_object(fun), - ); - } - // Print the global variables - for global in &ctx.translated.global_decls { - trace!( - "# Type:\n{}\n\n# Global definition:\n{}\n", - fmt_ctx.format_object(&global.ty), - fmt_ctx.format_object(global) - ); + // Print the functions + let fmt_ctx = ctx.into_fmt(); + for fun in &ctx.translated.fun_decls { + trace!( + "# Signature:\n{}\n\n# Function definition:\n{}\n", + fmt_ctx.format_object(&fun.signature), + fmt_ctx.format_object(fun), + ); + } + // Print the global variables + for global in &ctx.translated.global_decls { + trace!( + "# Type:\n{}\n\n# Global definition:\n{}\n", + fmt_ctx.format_object(&global.ty), + fmt_ctx.format_object(global) + ); + } + + if ctx.options.print_built_llbc { + info!("# LLBC resulting from control-flow reconstruction:\n\n{ctx}\n",); + } } } From b0b84d81b222c0940f6cef1e8c63eabc97e62bb8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 5 Jan 2025 21:03:44 +0100 Subject: [PATCH 7/8] Write test output on failure too --- charon/tests/ui.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/charon/tests/ui.rs b/charon/tests/ui.rs index 9902bfb5f..0eb6bb219 100644 --- a/charon/tests/ui.rs +++ b/charon/tests/ui.rs @@ -8,6 +8,7 @@ use anyhow::{anyhow, bail}; use assert_cmd::prelude::{CommandCargoExt, OutputAssertExt}; use indoc::indoc as unindent; use libtest_mimic::Trial; +use snapbox::filter::Filter as _; use std::{ error::Error, fs::read_to_string, @@ -233,6 +234,12 @@ fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> { } TestKind::PrettyLlbc => { if !output.status.success() { + if output.status.code() != Some(101) { + // Write output file anyway to make debugging easier. + let actual = snapbox::Data::text(stdout); + let actual = snapbox::filter::FilterNewlines.filter(actual); + actual.write_to_path(&test_case.expected)?; + } bail!("Compilation failed: {stderr}") } stdout From 52221b2bffdddb1e8a17b856cdd4aae828782186 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 5 Jan 2025 22:20:21 +0100 Subject: [PATCH 8/8] Add context to `check_generics` errors --- charon/src/ast/krate.rs | 22 +++++++++++----------- charon/src/ast/visitor.rs | 4 ++++ charon/src/transform/check_generics.rs | 17 ++++++++++++++++- 3 files changed, 31 insertions(+), 12 deletions(-) diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index 6d6c952a8..5f9857925 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -227,12 +227,12 @@ impl<'ctx> AnyTransItem<'ctx> { /// We can't implement `AstVisitable` because of the `'static` constraint, but it's ok because /// `AnyTransItem` isn't contained in any of our types. pub fn drive(&self, visitor: &mut V) -> ControlFlow { - match self { - AnyTransItem::Type(d) => d.drive(visitor), - AnyTransItem::Fun(d) => d.drive(visitor), - AnyTransItem::Global(d) => d.drive(visitor), - AnyTransItem::TraitDecl(d) => d.drive(visitor), - AnyTransItem::TraitImpl(d) => d.drive(visitor), + match *self { + AnyTransItem::Type(d) => visitor.visit(d), + AnyTransItem::Fun(d) => visitor.visit(d), + AnyTransItem::Global(d) => visitor.visit(d), + AnyTransItem::TraitDecl(d) => visitor.visit(d), + AnyTransItem::TraitImpl(d) => visitor.visit(d), } } } @@ -263,11 +263,11 @@ impl<'ctx> AnyTransItemMut<'ctx> { /// `AnyTransItemMut` isn't contained in any of our types. pub fn drive_mut(&mut self, visitor: &mut V) -> ControlFlow { match self { - AnyTransItemMut::Type(d) => d.drive_mut(visitor), - AnyTransItemMut::Fun(d) => d.drive_mut(visitor), - AnyTransItemMut::Global(d) => d.drive_mut(visitor), - AnyTransItemMut::TraitDecl(d) => d.drive_mut(visitor), - AnyTransItemMut::TraitImpl(d) => d.drive_mut(visitor), + AnyTransItemMut::Type(d) => visitor.visit(*d), + AnyTransItemMut::Fun(d) => visitor.visit(*d), + AnyTransItemMut::Global(d) => visitor.visit(*d), + AnyTransItemMut::TraitDecl(d) => visitor.visit(*d), + AnyTransItemMut::TraitImpl(d) => visitor.visit(*d), } } } diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs index e9be37b88..7930530eb 100644 --- a/charon/src/ast/visitor.rs +++ b/charon/src/ast/visitor.rs @@ -75,6 +75,10 @@ use index_vec::Idx; ) )] pub trait AstVisitable: Any { + /// The name of the type, used for debug logging. + fn name(&self) -> &'static str { + std::any::type_name::() + } /// Visit all occurrences of that type inside `self`, in pre-order traversal. fn dyn_visit(&self, f: impl FnMut(&T)) { self.drive(&mut DynVisitor::new_shared::(f)); diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index e2e5ca116..13e0763a5 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -1,5 +1,6 @@ //! Check that all supplied generic types match the corresponding generic parameters. use derive_generic_visitor::*; +use itertools::Itertools; use std::fmt::Display; use crate::{errors::ErrorCtx, llbc_ast::*, register_error_or_panic}; @@ -13,16 +14,29 @@ struct CheckGenericsVisitor<'a> { error_ctx: &'a mut ErrorCtx, // Tracks an enclosing span to make errors useful. span: Span, + /// Remember the names of the types visited up to here. + visit_stack: Vec<&'static str>, } impl CheckGenericsVisitor<'_> { fn error(&mut self, message: impl Display) { - let message = format!("Found inconsistent generics {}:\n{message}", self.phase); + let message = format!( + "Found inconsistent generics {}:\n{message}\nVisitor stack:\n {}", + self.phase, + self.visit_stack.iter().rev().join("\n ") + ); register_error_or_panic!(self.error_ctx, self.translated, self.span, message); } } impl VisitAst for CheckGenericsVisitor<'_> { + fn visit<'a, T: AstVisitable>(&'a mut self, x: &T) -> ControlFlow { + self.visit_stack.push(x.name()); + x.drive(self)?; // default behavior + self.visit_stack.pop(); + Continue(()) + } + fn visit_aggregate_kind(&mut self, agg: &AggregateKind) -> ControlFlow { match agg { AggregateKind::Adt(..) => self.visit_inner(agg)?, @@ -116,6 +130,7 @@ impl TransformPass for Check { error_ctx: &mut ctx.errors, phase: self.0, span: item.item_meta().span, + visit_stack: Default::default(), }; item.drive(&mut visitor); }