From 23f41c3214df5949b79c44e46eb286158cb6f436 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 10 Jul 2025 16:05:21 +0200 Subject: [PATCH 1/5] tests: don't translate `fmt::Formatter` --- charon/src/options.rs | 1 + charon/tests/ui/dyn-trait.out | 6 ------ charon/tests/ui/gosim-demo.out | 6 ------ .../tests/ui/issue-4-slice-try-into-array.out | 6 ------ charon/tests/ui/issue-4-traits.out | 6 ------ charon/tests/ui/raw-boxes.out | 17 ----------------- charon/tests/ui/result-unwrap.out | 14 ++------------ .../ui/simple/mem-discriminant-from-derive.out | 6 ------ charon/tests/ui/simple/pointee_metadata.out | 6 ------ charon/tests/ui/simple/ptr-from-raw-parts.out | 6 ------ charon/tests/ui/simple/ptr_metadata.out | 6 ------ charon/tests/ui/simple/slice_index_range.out | 17 ----------------- charon/tests/ui/string-literal.out | 6 ------ .../ui/type_inference_is_order_dependent.out | 6 ------ charon/tests/ui/unsafe.out | 6 ------ charon/tests/ui/unsize.out | 6 ------ 16 files changed, 3 insertions(+), 118 deletions(-) diff --git a/charon/src/options.rs b/charon/src/options.rs index 6af79f2bc..6dad7eb12 100644 --- a/charon/src/options.rs +++ b/charon/src/options.rs @@ -305,6 +305,7 @@ impl CliOpts { Preset::Tests => { self.hide_allocator = !self.raw_boxes; self.rustc_args.push("--edition=2021".to_owned()); + self.exclude.push("core::fmt::Formatter".to_owned()); } } } diff --git a/charon/tests/ui/dyn-trait.out b/charon/tests/ui/dyn-trait.out index 351a550bc..d3ac6c0fe 100644 --- a/charon/tests/ui/dyn-trait.out +++ b/charon/tests/ui/dyn-trait.out @@ -3,12 +3,6 @@ // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized diff --git a/charon/tests/ui/gosim-demo.out b/charon/tests/ui/gosim-demo.out index d9a32e509..03081f8cd 100644 --- a/charon/tests/ui/gosim-demo.out +++ b/charon/tests/ui/gosim-demo.out @@ -106,12 +106,6 @@ where // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out index c33736dc2..bf392ce3b 100644 --- a/charon/tests/ui/issue-4-slice-try-into-array.out +++ b/charon/tests/ui/issue-4-slice-try-into-array.out @@ -1,11 +1,5 @@ # Final LLBC before serialization: -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out index b94e763eb..b4aaa25ca 100644 --- a/charon/tests/ui/issue-4-traits.out +++ b/charon/tests/ui/issue-4-traits.out @@ -1,11 +1,5 @@ # Final LLBC before serialization: -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized diff --git a/charon/tests/ui/raw-boxes.out b/charon/tests/ui/raw-boxes.out index bb80ee6b0..dfc01c098 100644 --- a/charon/tests/ui/raw-boxes.out +++ b/charon/tests/ui/raw-boxes.out @@ -209,23 +209,6 @@ pub struct NonNull { pointer: *const T, } -// Full name: core::fmt::FormattingOptions -pub struct FormattingOptions { - flags: u32, - width: u16, - precision: u16, -} - -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub struct Formatter<'a> -where - 'a : 'a, -{ - options: FormattingOptions, - buf: &'a mut (dyn (exists(TODO))), -} - // Full name: core::result::Result #[lang_item("Result")] pub enum Result diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out index 281d73e5a..da6a19a73 100644 --- a/charon/tests/ui/result-unwrap.out +++ b/charon/tests/ui/result-unwrap.out @@ -30,16 +30,6 @@ fn core::fmt::flags::DEBUG_UPPER_HEX_FLAG() -> u32 const core::fmt::flags::DEBUG_UPPER_HEX_FLAG: u32 = core::fmt::flags::DEBUG_UPPER_HEX_FLAG() -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub struct Formatter<'a> -where - 'a : 'a, -{ - options: FormattingOptions, - buf: &'a mut (dyn (exists(TODO))), -} - // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized @@ -140,7 +130,7 @@ pub fn {impl Debug for u32}::fmt<'_0, '_1, '_2>(@1: &'_0 (u32), @2: &'_1 mut (Fo storage_live(@8) storage_live(@3) storage_live(@4) - @4 := copy (((*(f@2)).options).flags) + @4 := copy (((*(f@2)).0).flags) @7 := core::fmt::flags::DEBUG_LOWER_HEX_FLAG @3 := move (@4) & move (@7) storage_dead(@4) @@ -156,7 +146,7 @@ pub fn {impl Debug for u32}::fmt<'_0, '_1, '_2>(@1: &'_0 (u32), @2: &'_1 mut (Fo storage_dead(@3) storage_live(@5) storage_live(@6) - @6 := copy (((*(f@2)).options).flags) + @6 := copy (((*(f@2)).0).flags) @8 := core::fmt::flags::DEBUG_UPPER_HEX_FLAG @5 := move (@6) & move (@8) storage_dead(@6) diff --git a/charon/tests/ui/simple/mem-discriminant-from-derive.out b/charon/tests/ui/simple/mem-discriminant-from-derive.out index 0a6a9abb9..f2167fc4c 100644 --- a/charon/tests/ui/simple/mem-discriminant-from-derive.out +++ b/charon/tests/ui/simple/mem-discriminant-from-derive.out @@ -68,12 +68,6 @@ where // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::result::Result #[lang_item("Result")] pub enum Result diff --git a/charon/tests/ui/simple/pointee_metadata.out b/charon/tests/ui/simple/pointee_metadata.out index e14428eff..31d835120 100644 --- a/charon/tests/ui/simple/pointee_metadata.out +++ b/charon/tests/ui/simple/pointee_metadata.out @@ -95,12 +95,6 @@ where // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::result::Result #[lang_item("Result")] pub enum Result diff --git a/charon/tests/ui/simple/ptr-from-raw-parts.out b/charon/tests/ui/simple/ptr-from-raw-parts.out index da8df36b0..24f796331 100644 --- a/charon/tests/ui/simple/ptr-from-raw-parts.out +++ b/charon/tests/ui/simple/ptr-from-raw-parts.out @@ -124,12 +124,6 @@ impl Ord for () { // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::result::Result #[lang_item("Result")] pub enum Result diff --git a/charon/tests/ui/simple/ptr_metadata.out b/charon/tests/ui/simple/ptr_metadata.out index 2b6d729bf..fe9e46184 100644 --- a/charon/tests/ui/simple/ptr_metadata.out +++ b/charon/tests/ui/simple/ptr_metadata.out @@ -124,12 +124,6 @@ impl Ord for () { // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::result::Result #[lang_item("Result")] pub enum Result diff --git a/charon/tests/ui/simple/slice_index_range.out b/charon/tests/ui/simple/slice_index_range.out index b6a93613d..21480671a 100644 --- a/charon/tests/ui/simple/slice_index_range.out +++ b/charon/tests/ui/simple/slice_index_range.out @@ -3,23 +3,6 @@ // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::FormattingOptions -pub struct FormattingOptions { - flags: u32, - width: u16, - precision: u16, -} - -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub struct Formatter<'a> -where - 'a : 'a, -{ - options: FormattingOptions, - buf: &'a mut (dyn (exists(TODO))), -} - // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized diff --git a/charon/tests/ui/string-literal.out b/charon/tests/ui/string-literal.out index 44c5985d1..f8030f1c6 100644 --- a/charon/tests/ui/string-literal.out +++ b/charon/tests/ui/string-literal.out @@ -3,12 +3,6 @@ // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized diff --git a/charon/tests/ui/type_inference_is_order_dependent.out b/charon/tests/ui/type_inference_is_order_dependent.out index 96eb0a786..c26cd4648 100644 --- a/charon/tests/ui/type_inference_is_order_dependent.out +++ b/charon/tests/ui/type_inference_is_order_dependent.out @@ -36,12 +36,6 @@ impl Default for bool { // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::fmt::Arguments #[lang_item("format_arguments")] pub opaque type Arguments<'a> diff --git a/charon/tests/ui/unsafe.out b/charon/tests/ui/unsafe.out index 64a3dae6a..5e72cd220 100644 --- a/charon/tests/ui/unsafe.out +++ b/charon/tests/ui/unsafe.out @@ -124,12 +124,6 @@ impl Ord for () { // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::result::Result #[lang_item("Result")] pub enum Result diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out index e1e9543ee..167fa7e36 100644 --- a/charon/tests/ui/unsize.out +++ b/charon/tests/ui/unsize.out @@ -27,12 +27,6 @@ where // Full name: core::fmt::Error pub struct Error {} -// Full name: core::fmt::Formatter -#[lang_item("Formatter")] -pub opaque type Formatter<'a> -where - 'a : 'a, - // Full name: core::result::Result #[lang_item("Result")] pub enum Result From b68fb046fbe53d76d6d3bbb2a6724e7da99c1af8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 10 Jul 2025 21:53:53 +0200 Subject: [PATCH 2/5] Remove leftover `self_clause_id` logic --- .../src/bin/charon-driver/translate/translate_ctx.rs | 4 ---- .../bin/charon-driver/translate/translate_generics.rs | 6 ------ .../charon-driver/translate/translate_predicates.rs | 10 +--------- 3 files changed, 1 insertion(+), 19 deletions(-) diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 133fe870c..fdefbad10 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -75,9 +75,6 @@ pub(crate) struct ItemTransCtx<'tcx, 'ctx> { pub parent_trait_clauses: Vector, /// (For traits only) accumulated trait clauses on associated types. pub item_trait_clauses: HashMap>, - /// (For method declarations only) the clause id corresponding to the explicit `Self` clause. - /// If `None` then we're in a trait declaration and should use `TraitRefKind::Self` instead. - pub self_clause_id: Option, } /// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics. @@ -171,7 +168,6 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { binding_levels: Default::default(), parent_trait_clauses: Default::default(), item_trait_clauses: Default::default(), - self_clause_id: Default::default(), } } diff --git a/charon/src/bin/charon-driver/translate/translate_generics.rs b/charon/src/bin/charon-driver/translate/translate_generics.rs index d140cd8e0..070992931 100644 --- a/charon/src/bin/charon-driver/translate/translate_generics.rs +++ b/charon/src/bin/charon-driver/translate/translate_generics.rs @@ -250,12 +250,6 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { span: Span, mut id: usize, ) -> Result { - if self.self_clause_id.is_some() { - // We added an extra first clause which hax doesn't know about, so we adapt the index - // accordingly. - // TODO: more robust tracking of clause ids between hax and charon. - id += 1; - } // The clause indices returned by hax count clauses in order, starting from the parentmost. // While adding clauses to a binding level we already need to translate types and clauses, // so the innermost item binder may not have all the clauses yet. Hence for that binder we diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index 8dc6d99d0..4e84c0ec2 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -215,15 +215,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { ); // If we are refering to a trait clause, we need to find the relevant one. let mut trait_id = match &impl_source.r#impl { - ImplExprAtom::SelfImpl { .. } => match self.self_clause_id { - None => TraitRefKind::SelfId, - // An explicit `Self` clause is bound at the top-level; we use it instead - // of the implicit `TraitRefKind::SelfId` one. - Some(id) => TraitRefKind::Clause(DeBruijnVar::bound( - self.binding_levels.depth(), - id, - )), - }, + ImplExprAtom::SelfImpl { .. } => TraitRefKind::SelfId, ImplExprAtom::LocalBound { index, .. } => { let var = self.lookup_clause_var(span, *index)?; TraitRefKind::Clause(var) From 00235bab2e726d4ee2ec68aa94fb9c7fb87b4086 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 10 Jul 2025 15:35:47 +0200 Subject: [PATCH 3/5] Translate existential predicates Co-authored-by: ssyram --- charon-ml/src/CharonVersion.ml | 2 +- charon-ml/src/NameMatcher.ml | 11 ++- charon-ml/src/PrintTypes.ml | 1 + .../src/generated/Generated_GAstOfJson.ml | 34 +++++-- charon-ml/src/generated/Generated_Types.ml | 33 +++++-- charon/Cargo.lock | 2 +- charon/Cargo.toml | 2 +- charon/src/ast/expressions_utils.rs | 24 ++++- charon/src/ast/types.rs | 35 +++++-- charon/src/ast/visitor.rs | 4 +- charon/src/bin/charon-driver/translate/mod.rs | 1 + .../translate/translate_trait_objects.rs | 84 ++++++++++++++++ .../translate/translate_types.rs | 19 +++- charon/src/name_matcher/mod.rs | 1 + charon/src/pretty/fmt_with_ctx.rs | 35 ++++++- charon/tests/ui/dyn-trait.out | 99 +++++++++++++++++-- charon/tests/ui/result-unwrap.out | 6 +- .../tests/ui/simple/generic-cast-to-dyn.out | 12 +-- charon/tests/ui/unsize.out | 16 +-- 19 files changed, 353 insertions(+), 68 deletions(-) create mode 100644 charon/src/bin/charon-driver/translate/translate_trait_objects.rs diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index c221df848..4693d42d7 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.115" +let supported_charon_version = "0.1.116" diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index 367c12cc4..5d88e3b32 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -996,12 +996,15 @@ and ty_to_pattern_aux (ctx : 'fun_body ctx) (c : to_pat_config) else Some (ty_to_pattern_aux ctx c m output) in EArrow (inputs, output) + | TError _ -> EVar None | TRawPtr (ty, RMut) -> ERawPtr (Mut, ty_to_pattern_aux ctx c m ty) | TRawPtr (ty, RShared) -> ERawPtr (Not, ty_to_pattern_aux ctx c m ty) - | TFnDef _ -> raise (Failure "Unimplemented: FnDef") - | TDynTrait _ -> raise (Failure "Unimplemented: DynTrait") - | TNever -> raise (Failure "Unimplemented: Never") - | TError _ -> EVar None + | _ -> + let fmt_env = ctx_to_fmt_env ctx in + raise + (Failure + ("Can't convert type to pattern: " + ^ PrintTypes.ty_to_string fmt_env ty)) and trait_ref_item_with_generics_to_pattern (ctx : 'fun_body ctx) (c : to_pat_config) (m : constraints) (trait_ref : T.trait_ref) diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 9c5497eb5..22e11885d 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -291,6 +291,7 @@ and ty_to_string (env : 'a fmt_env) (ty : ty) : string = let fn = fn_ptr_to_string env f.binder_value in fn | TDynTrait _ -> "dyn (TODO)" + | TExistentialPlaceholder -> "_" | TError msg -> "type_error (\"" ^ msg ^ "\")" (** Return two lists: diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index db2934d6d..fb2048f1e 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -600,11 +600,29 @@ and discriminant_layout_of_json (ctx : of_json_ctx) (js : json) : Ok ({ offset; tag_ty; encoding } : discriminant_layout) | _ -> Error "") -and existential_predicate_of_json (ctx : of_json_ctx) (js : json) : - (existential_predicate, string) result = +and dyn_predicate_of_json (ctx : of_json_ctx) (js : json) : + (dyn_predicate, string) result = combine_error_msgs js __FUNCTION__ (match js with - | `Null -> Ok () + | `Assoc [ ("Trait", trait) ] -> + let* trait = trait_decl_ref_of_json ctx trait in + Ok (Trait trait) + | `Assoc [ ("Projection", projection) ] -> + let* projection = dyn_type_constraint_of_json ctx projection in + Ok (Projection projection) + | _ -> Error "") + +and dyn_type_constraint_of_json (ctx : of_json_ctx) (js : json) : + (dyn_type_constraint, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | `Assoc + [ ("trait_item", trait_item); ("generics", generics); ("term", term) ] + -> + let* trait_item = trait_item_name_of_json ctx trait_item in + let* generics = box_of_json generic_args_of_json ctx generics in + let* term = ty_of_json ctx term in + Ok ({ trait_item; generics; term } : dyn_type_constraint) | _ -> Error "") and field_of_json (ctx : of_json_ctx) (js : json) : (field, string) result = @@ -1789,9 +1807,12 @@ and ty_of_json (ctx : of_json_ctx) (js : json) : (ty, string) result = let* x_0 = trait_ref_of_json ctx x_0 in let* x_1 = trait_item_name_of_json ctx x_1 in Ok (TTraitType (x_0, x_1)) - | `Assoc [ ("DynTrait", dyn_trait) ] -> - let* dyn_trait = existential_predicate_of_json ctx dyn_trait in - Ok (TDynTrait dyn_trait) + | `Assoc [ ("DynTrait", `List [ x_0; x_1 ]) ] -> + let* x_0 = + list_of_json (region_binder_of_json dyn_predicate_of_json) ctx x_0 + in + let* x_1 = region_of_json ctx x_1 in + Ok (TDynTrait (x_0, x_1)) | `Assoc [ ("FnPtr", fn_ptr) ] -> let* fn_ptr = region_binder_of_json @@ -1802,6 +1823,7 @@ and ty_of_json (ctx : of_json_ctx) (js : json) : (ty, string) result = | `Assoc [ ("FnDef", fn_def) ] -> let* fn_def = region_binder_of_json fn_ptr_of_json ctx fn_def in Ok (TFnDef fn_def) + | `String "ExistentialPlaceholder" -> Ok TExistentialPlaceholder | `Assoc [ ("Error", error) ] -> let* error = string_of_json ctx error in Ok (TError error) diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index b4c285ac6..0a431d980 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -249,10 +249,24 @@ and builtin_ty = | TSlice (** Primitive type *) | TStr (** Primitive type *) -(** A predicate of the form [exists where T: Trait]. - - TODO: store something useful here *) -and existential_predicate = unit +(** A predicate in a [dyn Trait] type. These predicates apply to an + existentially quentified type, represented as + [TyKind::ExistentialPlaceholder]. *) +and dyn_predicate = + | Trait of trait_decl_ref + (** Trait predicate that the target type must satisfy. *) + | Projection of dyn_type_constraint + (** Projection associated to the principal trait of this [dyn Trait]. We + don't currently support other projections. *) + +(** A projection of the form [TraitItemName = Ty], where the + [TraitItemName] is an associate type of the principal trait of a [dyn Trait] + type. *) +and dyn_type_constraint = { + trait_item : trait_item_name; + generics : generic_args; + term : ty; +} and fn_ptr = { func : fun_id_or_trait_method_ref; generics : generic_args } @@ -445,14 +459,16 @@ and ty = type Bar; // type associated to the trait Foo } ]} *) - | TDynTrait of existential_predicate + | TDynTrait of dyn_predicate region_binder list * region (** [dyn Trait] This carries an existentially quantified list of predicates, e.g. [exists where T: Into]. The predicate must quantify over a single type and no any regions or constants. - TODO: we don't translate this properly yet. *) + Only the first Predicate is used as the *principal* predicate, i.e. + the one that corresponds to a vtable. It is uniquely of the + [ExistentialTraitRef] type. *) | TFnPtr of (ty list * ty) region_binder (** Function pointer type. This is a literal pointer to a region of memory that contains a callable function. This is a function signature with @@ -469,6 +485,11 @@ and ty = given that the type here is polymorpohic in the late-bound variables (those that could appear in a function pointer type like [for<'a> fn(&'a u32)]), we need to bind them here. *) + | TExistentialPlaceholder + (** Fake type used in [dyn Trait] predicates: such a predicate has the + [Self] type existentially quantified. In order for generics to stay + consistent, we use this placeholder to represent the existentially + quantified type. *) | TError of string (** A type that could not be computed or was incorrect. *) (** Reference to a type declaration or builtin type. *) diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 601376972..28423401b 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -200,7 +200,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.115" +version = "0.1.116" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 33e2c2d05..fce7e8150 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.115" +version = "0.1.116" authors = [ "Son Ho ", "Guillaume Boisseau ", diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs index abcf42d69..4212b0c46 100644 --- a/charon/src/ast/expressions_utils.rs +++ b/charon/src/ast/expressions_utils.rs @@ -65,8 +65,16 @@ impl Place { Adt(tref) if matches!(tref.id, TypeId::Builtin(BuiltinTy::Box)) => { tref.generics.types[0].clone() } - Adt(..) | TypeVar(_) | Literal(_) | Never | TraitType(..) | DynTrait(_) | FnPtr(..) - | FnDef(..) | Error(..) => panic!("internal type error"), + Adt(..) + | TypeVar(_) + | Literal(_) + | Never + | TraitType(..) + | DynTrait(..) + | FnPtr(..) + | FnDef(..) + | Error(..) + | ExistentialPlaceholder => panic!("internal type error"), }; Place { ty: proj_ty, @@ -122,8 +130,16 @@ impl ProjectionElem { Adt(tref) if matches!(tref.id, TypeId::Builtin(BuiltinTy::Box)) => { tref.generics.types[0].clone() } - Adt(..) | TypeVar(_) | Literal(_) | Never | TraitType(..) | DynTrait(_) - | FnPtr(..) | FnDef(..) | Error(..) => { + Adt(..) + | TypeVar(_) + | Literal(_) + | Never + | TraitType(..) + | DynTrait(..) + | FnPtr(..) + | FnDef(..) + | Error(..) + | ExistentialPlaceholder => { // Type error return Err(()); } diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 8900c22e3..2402c7f7f 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -272,12 +272,6 @@ pub struct GenericParams { pub trait_type_constraints: Vector>, } -/// A predicate of the form `exists where T: Trait`. -/// -/// TODO: store something useful here -#[derive(Debug, Default, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] -pub struct ExistentialPredicate; - /// Where a given predicate came from. #[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)] pub enum PredicateOrigin { @@ -787,8 +781,9 @@ pub enum TyKind { /// This carries an existentially quantified list of predicates, e.g. `exists where T: /// Into`. The predicate must quantify over a single type and no any regions or constants. /// - /// TODO: we don't translate this properly yet. - DynTrait(ExistentialPredicate), + /// Only the first Predicate is used as the *principal* predicate, i.e. the one that + /// corresponds to a vtable. It is uniquely of the `ExistentialTraitRef` type. + DynTrait(Vec>, Region), /// Function pointer type. This is a literal pointer to a region of memory that /// contains a callable function. /// This is a function signature with limited generics: it only supports lifetime generics, not @@ -803,6 +798,10 @@ pub enum TyKind { /// variables (those that could appear in a function pointer type like `for<'a> fn(&'a u32)`), /// we need to bind them here. FnDef(RegionBinder), + /// Fake type used in `dyn Trait` predicates: such a predicate has the `Self` type + /// existentially quantified. In order for generics to stay consistent, we use this placeholder to + /// represent the existentially quantified type. + ExistentialPlaceholder, /// A type that could not be computed or was incorrect. #[drive(skip)] Error(String), @@ -902,3 +901,23 @@ pub struct FunSig { pub inputs: Vec, pub output: Ty, } + +/// A projection of the form `TraitItemName = Ty`, where the `TraitItemName` is an +/// associate type of the principal trait of a `dyn Trait` type. +#[derive(Debug, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] +pub struct DynTypeConstraint { + pub trait_item: TraitItemName, + pub generics: BoxedArgs, + pub term: Ty, +} + +/// A predicate in a `dyn Trait` type. These predicates apply to an existentially quentified type, +/// represented as `TyKind::ExistentialPlaceholder`. +#[derive(Debug, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] +pub enum DynPredicate { + /// Trait predicate that the target type must satisfy. + Trait(TraitDeclRef), + /// Projection associated to the principal trait of this `dyn Trait`. We don't currently + /// support other projections. + Projection(DynTypeConstraint), +} diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs index 41fe0f58d..17a5d10d9 100644 --- a/charon/src/ast/visitor.rs +++ b/charon/src/ast/visitor.rs @@ -43,7 +43,7 @@ use indexmap::IndexMap; drive( AbortKind, Assert, BinOp, Body, BorrowKind, BuiltinFunId, BuiltinIndexOp, BuiltinTy, Call, CastKind, ClosureInfo, ClosureKind, ConstGenericVar, ConstGenericVarId, - Disambiguator, ExistentialPredicate, Field, FieldId, FieldProjKind, FloatTy, FloatValue, + Disambiguator, DynPredicate, DynTypeConstraint, Field, FieldId, FieldProjKind, FloatTy, FloatValue, FnOperand, FunId, FunIdOrTraitMethodRef, FunSig, ImplElem, IntegerTy, Literal, LiteralTy, llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch, Locals, Name, NullOp, Opaque, Operand, PathElem, PlaceKind, ProjectionElem, RawConstantExpr, @@ -73,7 +73,7 @@ use indexmap::IndexMap; llbc_statement: llbc_ast::Statement, ullbc_statement: ullbc_ast::Statement, AggregateKind, FnPtr, ItemKind, ItemMeta, Span, ConstantExpr, FunDeclId, GlobalDeclId, TypeDeclId, TraitDeclId, TraitImplId, - FunDecl, GlobalDecl, TypeDecl, TraitDecl, TraitImpl + FunDecl, GlobalDecl, TypeDecl, TraitDecl, TraitImpl, ) )] pub trait AstVisitable: Any { diff --git a/charon/src/bin/charon-driver/translate/mod.rs b/charon/src/bin/charon-driver/translate/mod.rs index 57b4afd84..fd9f32641 100644 --- a/charon/src/bin/charon-driver/translate/mod.rs +++ b/charon/src/bin/charon-driver/translate/mod.rs @@ -11,4 +11,5 @@ pub mod translate_generics; pub mod translate_items; pub mod translate_meta; pub mod translate_predicates; +pub mod translate_trait_objects; pub mod translate_types; diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs new file mode 100644 index 000000000..38319a855 --- /dev/null +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -0,0 +1,84 @@ +use super::translate_ctx::*; +use charon_lib::ast::*; +use hax_frontend_exporter as hax; + +impl ItemTransCtx<'_, '_> { + pub fn check_at_most_one_pred_has_methods( + &self, + span: Span, + preds: &Vec>, + ) -> Result<(), Error> { + let all_ex_trait_ref = preds.iter().filter_map(|bound| { + if let hax::ExistentialPredicate::Trait(trait_ref) = &bound.value { + Some(trait_ref) + } else { + None + } + }); + if all_ex_trait_ref.count() > 1 { + raise_error!( + self, + span, + "`dyn Trait` with multiple method-bearing predicates is not supported" + ); + } + Ok(()) + } + + /// Translate generics for an exitential predicate. These generics are missing a `Self` type, + /// which we add here, represented with `ExistentialPlaceholder`. + fn translate_ex_generics( + &mut self, + span: Span, + args: &[hax::GenericArg], + ) -> Result, Error> { + let mut generics = Box::new(self.translate_generic_args(span, args, &[])?); + generics.types.insert_and_shift_ids( + TypeVarId::from_usize(0), + TyKind::ExistentialPlaceholder.into_ty(), + ); + Ok(generics) + } + + pub fn translate_existential_predicate( + &mut self, + span: Span, + pred: &hax::ExistentialPredicate, + ) -> Result { + Ok(match pred { + hax::ExistentialPredicate::Trait(tref) => DynPredicate::Trait(TraitDeclRef { + id: self.register_trait_decl_id(span, &tref.def_id), + generics: self.translate_ex_generics(span, &tref.args)?, + }), + hax::ExistentialPredicate::AutoTrait(def_id) => { + let trait_id = self.register_trait_decl_id(span, def_id); + let ty = TyKind::ExistentialPlaceholder.into_ty(); + let tref = TraitDeclRef { + id: trait_id, + generics: Box::new(GenericArgs::new_types([ty].into())), + }; + DynPredicate::Trait(tref) + } + hax::ExistentialPredicate::Projection(proj) => { + // TODO: this is incorrect if the projection doesn't apply to the principal. + let args = self.translate_ex_generics(span, &proj.args)?; + let name = self.t_ctx.translate_trait_item_name(&proj.def_id)?; + let term = match &proj.term { + hax::Term::Ty(ty) => self.translate_ty(span, ty)?, + hax::Term::Const(_) => { + raise_error!( + self, + span, + "`dyn Trait` with associated const constraints are not supported", + ) + } + }; + DynPredicate::Projection(DynTypeConstraint { + trait_item: name, + generics: args, + term, + }) + } + }) + } +} diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 84234d542..42d31abd2 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -214,10 +214,21 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { TyKind::Adt(tref) } - hax::TyKind::Dynamic(_existential_preds, _region, _) => { - // TODO: we don't translate the predicates yet because our machinery can't handle - // it. - TyKind::DynTrait(ExistentialPredicate) + hax::TyKind::Dynamic(preds, region, ..) => { + // This is a robustness check: the current version of Rustc + // accepts at most one method-bearing predicate in a trait object. + // But things may change in the future. + self.check_at_most_one_pred_has_methods(span, &preds)?; + let region = self.translate_region(span, region)?; + let preds = preds + .iter() + .map(|bound_pred| { + self.translate_region_binder(span, bound_pred, |ctx, x| { + ctx.translate_existential_predicate(span, x) + }) + }) + .try_collect()?; + TyKind::DynTrait(preds, region) } hax::TyKind::Infer(_) => { diff --git a/charon/src/name_matcher/mod.rs b/charon/src/name_matcher/mod.rs index 62e006ecc..c81da0f72 100644 --- a/charon/src/name_matcher/mod.rs +++ b/charon/src/name_matcher/mod.rs @@ -130,6 +130,7 @@ impl Pattern { | TyKind::DynTrait(..) | TyKind::FnPtr(..) | TyKind::FnDef(..) + | TyKind::ExistentialPlaceholder | TyKind::Error(..) => false, } } diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 0149478a5..0b2d3a56b 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -348,9 +348,28 @@ impl FmtWithCtx for DeclarationGroup { } } -impl FmtWithCtx for ExistentialPredicate { - fn fmt_with_ctx(&self, _ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { - write!(f, "exists(TODO)") +impl FmtWithCtx for DynPredicate { + fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + DynPredicate::Trait(trait_ref) => { + write!(f, "{}", trait_ref.with_ctx(ctx)) + } + DynPredicate::Projection(proj) => { + write!(f, "{}", proj.with_ctx(ctx)) + } + } + } +} + +impl FmtWithCtx for DynTypeConstraint { + fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!( + f, + "{}::{} = {}", + self.trait_item.0, + self.generics.with_ctx(ctx), + self.term.with_ctx(ctx) + ) } } @@ -1759,7 +1778,13 @@ impl FmtWithCtx for Ty { TyKind::TraitType(trait_ref, name) => { write!(f, "{}::{name}", trait_ref.with_ctx(ctx),) } - TyKind::DynTrait(pred) => write!(f, "dyn ({})", pred.with_ctx(ctx)), + TyKind::DynTrait(preds, region) => { + let preds = preds + .iter() + .map(|p| p.fmt_as_for(ctx).to_string()) + .format(" + "); + write!(f, "(dyn {} + {})", preds, region.with_ctx(ctx)) + } TyKind::FnPtr(io) => { write!(f, "{}", io.with_ctx(ctx)) } @@ -1770,6 +1795,8 @@ impl FmtWithCtx for Ty { }; write!(f, "{value}",) } + // To make sure this is not definable as ADT or so + TyKind::ExistentialPlaceholder => write!(f, "_"), TyKind::Error(msg) => write!(f, "type_error(\"{msg}\")"), } } diff --git a/charon/tests/ui/dyn-trait.out b/charon/tests/ui/dyn-trait.out index d3ac6c0fe..a7585aa5d 100644 --- a/charon/tests/ui/dyn-trait.out +++ b/charon/tests/ui/dyn-trait.out @@ -1,5 +1,18 @@ # Final LLBC before serialization: +// Full name: core::cmp::PartialEq +#[lang_item("eq")] +pub trait PartialEq +{ + fn eq<'_0, '_1> = eq<'_0_0, '_0_1, Self, Rhs>[Self] +} + +// Full name: core::cmp::PartialEq::eq +#[lang_item("cmp_partialeq_eq")] +pub fn eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool +where + [@TraitClause0]: PartialEq, + // Full name: core::fmt::Error pub struct Error {} @@ -37,6 +50,72 @@ pub fn fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (Formatter<'_2>)) where [@TraitClause0]: Display, +// Full name: core::marker::Tuple +#[lang_item("tuple_trait")] +pub trait Tuple +{ + parent_clause0 : [@TraitClause0]: MetaSized +} + +// Full name: core::ops::function::FnOnce +#[lang_item("fn_once")] +pub trait FnOnce +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + parent_clause2 : [@TraitClause2]: Tuple + parent_clause3 : [@TraitClause3]: Sized + type Output + fn call_once = call_once[Self] +} + +// Full name: core::ops::function::FnMut +#[lang_item("fn_mut")] +pub trait FnMut +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnOnce + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] +} + +// Full name: core::ops::function::Fn +#[lang_item("r#fn")] +pub trait Fn +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnMut + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call<'_0> = call<'_0_0, Self, Args>[Self] +} + +// Full name: core::ops::function::Fn::call +pub fn call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output +where + [@TraitClause0]: Fn, + +// Full name: core::ops::function::FnMut::call_mut +pub fn call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output +where + [@TraitClause0]: FnMut, + +// Full name: core::ops::function::FnOnce::call_once +pub fn call_once(@1: Self, @2: Args) -> @TraitClause0::Output +where + [@TraitClause0]: FnOnce, + +// Full name: core::option::Option +#[lang_item("Option")] +pub enum Option +where + [@TraitClause0]: Sized, +{ + None, + Some(T), +} + // Full name: alloc::alloc::Global #[lang_item("global_alloc_ty")] pub struct Global {} @@ -75,22 +154,22 @@ where } // Full name: test_crate::construct -fn construct(@1: T) -> alloc::boxed::Box[MetaSized, Sized] +fn construct(@1: T) -> alloc::boxed::Box<(dyn Display<_> + 'static)>[MetaSized<(dyn Display<_> + '_)>, Sized] where [@TraitClause0]: Sized, [@TraitClause1]: Display, T : 'static, // Full name: test_crate::destruct -fn destruct<'_0>(@1: &'_0 (dyn (exists(TODO)))) -> String +fn destruct<'_0>(@1: &'_0 ((dyn Display<_> + '_0))) -> String { let @0: String; // return - let x@1: &'_ (dyn (exists(TODO))); // arg #1 - let @2: &'_ (dyn (exists(TODO))); // anonymous local + let x@1: &'_ ((dyn Display<_> + '_)); // arg #1 + let @2: &'_ ((dyn Display<_> + '_)); // anonymous local storage_live(@2) @2 := &*(x@1) - @0 := {impl ToString for T}::to_string<'_, dyn (exists(TODO))>[MetaSized, Display](move (@2)) + @0 := {impl ToString for T}::to_string<'_, (dyn Display<_> + '_)>[MetaSized<(dyn Display<_> + '_)>, Display<(dyn Display<_> + '_)>](move (@2)) storage_dead(@2) return } @@ -99,13 +178,13 @@ fn destruct<'_0>(@1: &'_0 (dyn (exists(TODO)))) -> String fn combine() // Full name: test_crate::foo -fn foo<'_0, '_1, T>(@1: &'_0 (dyn (exists(TODO))), @2: &'_1 (dyn (exists(TODO)))) +fn foo<'_0, '_1, T>(@1: &'_0 ((dyn for<'a> Fn<_, (&'a (T))> + for<'a> Output::<_, (&'a (T))> = T + 'static)), @2: &'_1 ((dyn PartialEq<_, Option[@TraitClause0]> + '_1))) where [@TraitClause0]: Sized, { let @0: (); // return - let @1: &'_ (dyn (exists(TODO))); // arg #1 - let @2: &'_ (dyn (exists(TODO))); // arg #2 + let @1: &'_ ((dyn for<'a> Fn<_, (&'a (T))> + for<'a> Output::<_, (&'a (T))> = T + '_)); // arg #1 + let @2: &'_ ((dyn PartialEq<_, Option[@TraitClause0]> + '_)); // arg #2 @0 := () @0 := () @@ -113,10 +192,10 @@ where } // Full name: test_crate::bar -fn bar<'_0>(@1: &'_0 (dyn (exists(TODO)))) +fn bar<'_0>(@1: &'_0 ((dyn for<'_0> Fn<_, (&'_0_0 ((dyn Display<_> + '_0_0)))> + for<'_0> Output::<_, (&'_0_0 ((dyn Display<_> + '_0_0)))> = () + '_0))) { let @0: (); // return - let @1: &'_ (dyn (exists(TODO))); // arg #1 + let @1: &'_ ((dyn for<'_0> Fn<_, (&'_0_0 ((dyn Display<_> + '_0_0)))> + for<'_0> Output::<_, (&'_0_0 ((dyn Display<_> + '_0_0)))> = () + '_)); // arg #1 @0 := () @0 := () diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out index da6a19a73..7dec7da42 100644 --- a/charon/tests/ui/result-unwrap.out +++ b/charon/tests/ui/result-unwrap.out @@ -187,7 +187,7 @@ where [@TraitClause0]: Drop, // Full name: core::result::unwrap_failed -fn unwrap_failed<'_0, '_1>(@1: &'_0 (Str), @2: &'_1 (dyn (exists(TODO)))) -> ! +fn unwrap_failed<'_0, '_1>(@1: &'_0 (Str), @2: &'_1 ((dyn Debug<_> + '_1))) -> ! pub fn core::result::{Result[@TraitClause0, @TraitClause1]}::unwrap(@1: Result[@TraitClause0, @TraitClause1]) -> T where @@ -199,7 +199,7 @@ where let self@1: Result[@TraitClause0, @TraitClause1]; // arg #1 let e@2: E; // local let @3: !; // anonymous local - let @4: &'_ (dyn (exists(TODO))); // anonymous local + let @4: &'_ ((dyn Debug<_> + '_)); // anonymous local let @5: &'_ (E); // anonymous local storage_live(e@2) @@ -214,7 +214,7 @@ where e@2 := move ((self@1 as variant Result::Err).0) storage_live(@4) @5 := &e@2 - @4 := unsize_cast<&'_ (E), &'_ (dyn (exists(TODO))), @TraitClause2>(copy (@5)) + @4 := unsize_cast<&'_ (E), &'_ ((dyn Debug<_> + '_)), @TraitClause2>(copy (@5)) @3 := unwrap_failed<'_, '_>(const ("called `Result::unwrap()` on an `Err` value"), move (@4)) }, } diff --git a/charon/tests/ui/simple/generic-cast-to-dyn.out b/charon/tests/ui/simple/generic-cast-to-dyn.out index 246563975..a1a32b3ce 100644 --- a/charon/tests/ui/simple/generic-cast-to-dyn.out +++ b/charon/tests/ui/simple/generic-cast-to-dyn.out @@ -31,25 +31,25 @@ pub trait Sized } // Full name: test_crate::foo -fn foo<'_0, T>(@1: &'_0 (T)) -> &'_0 (dyn (exists(TODO))) +fn foo<'_0, T>(@1: &'_0 (T)) -> &'_0 ((dyn Any<_> + 'static)) where [@TraitClause0]: Sized, [@TraitClause1]: Any, { - let @0: &'_ (dyn (exists(TODO))); // return + let @0: &'_ ((dyn Any<_> + '_)); // return let x@1: &'_ (T); // arg #1 - let @2: &'_ (dyn (exists(TODO))); // anonymous local - let @3: &'_ (dyn (exists(TODO))); // anonymous local + let @2: &'_ ((dyn Any<_> + '_)); // anonymous local + let @3: &'_ ((dyn Any<_> + '_)); // anonymous local let @4: &'_ (T); // anonymous local storage_live(@2) storage_live(@3) storage_live(@4) @4 := &*(x@1) - @3 := unsize_cast<&'_ (T), &'_ (dyn (exists(TODO))), @TraitClause1>(move (@4)) + @3 := unsize_cast<&'_ (T), &'_ ((dyn Any<_> + '_)), @TraitClause1>(move (@4)) storage_dead(@4) @2 := &*(@3) - @0 := unsize_cast<&'_ (dyn (exists(TODO))), &'_ (dyn (exists(TODO))), Any>(move (@2)) + @0 := unsize_cast<&'_ ((dyn Any<_> + '_)), &'_ ((dyn Any<_> + '_)), Any<(dyn Any<_> + '_)>>(move (@2)) storage_dead(@3) storage_dead(@2) return diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out index 167fa7e36..fb5213c73 100644 --- a/charon/tests/ui/unsize.out +++ b/charon/tests/ui/unsize.out @@ -163,14 +163,14 @@ fn foo() let @9: Rc>[MetaSized>, Sized]; // anonymous local let @10: Array; // anonymous local let string@11: String; // local - let @12: &'_ (dyn (exists(TODO))); // anonymous local + let @12: &'_ ((dyn Display<_> + '_)); // anonymous local let @13: &'_ (String); // anonymous local let @14: &'_ (String); // anonymous local - let @15: alloc::boxed::Box[MetaSized, Sized]; // anonymous local + let @15: alloc::boxed::Box<(dyn Display<_> + '_)>[MetaSized<(dyn Display<_> + '_)>, Sized]; // anonymous local let @16: alloc::boxed::Box[MetaSized, Sized]; // anonymous local let @17: String; // anonymous local let @18: &'_ (String); // anonymous local - let @19: Rc[MetaSized, Sized]; // anonymous local + let @19: Rc<(dyn Display<_> + '_)>[MetaSized<(dyn Display<_> + '_)>, Sized]; // anonymous local let @20: Rc[MetaSized, Sized]; // anonymous local let @21: String; // anonymous local let @22: &'_ (String); // anonymous local @@ -215,7 +215,7 @@ fn foo() storage_live(@14) @14 := &string@11 @13 := &*(@14) - @12 := unsize_cast<&'_ (String), &'_ (dyn (exists(TODO))), {impl Display for String}>(move (@13)) + @12 := unsize_cast<&'_ (String), &'_ ((dyn Display<_> + '_)), {impl Display for String}>(move (@13)) storage_dead(@13) storage_dead(@14) storage_dead(@12) @@ -227,11 +227,11 @@ fn foo() @17 := {impl Clone for String}::clone<'_>(move (@18)) storage_dead(@18) @16 := @BoxNew[Sized](move (@17)) - @15 := unsize_cast[MetaSized, Sized], alloc::boxed::Box[MetaSized, Sized], {impl Display for String}>(move (@16)) + @15 := unsize_cast[MetaSized, Sized], alloc::boxed::Box<(dyn Display<_> + '_)>[MetaSized<(dyn Display<_> + '_)>, Sized], {impl Display for String}>(move (@16)) drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @16 storage_dead(@17) storage_dead(@16) - drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @15 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}<(dyn Display<_> + '_), Global>[MetaSized<(dyn Display<_> + '_)>, Sized]] @15 storage_dead(@15) storage_live(@19) storage_live(@20) @@ -241,11 +241,11 @@ fn foo() @21 := {impl Clone for String}::clone<'_>(move (@22)) storage_dead(@22) @20 := alloc::rc::{Rc[@TraitClause0::parent_clause0, Sized]}::new[Sized](move (@21)) - @19 := unsize_cast[MetaSized, Sized], Rc[MetaSized, Sized]>(move (@20)) + @19 := unsize_cast[MetaSized, Sized], Rc<(dyn Display<_> + '_)>[MetaSized<(dyn Display<_> + '_)>, Sized]>(move (@20)) drop[{impl Drop for Rc[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @20 storage_dead(@21) storage_dead(@20) - drop[{impl Drop for Rc[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @19 + drop[{impl Drop for Rc[@TraitClause0, @TraitClause1]}<(dyn Display<_> + '_), Global>[MetaSized<(dyn Display<_> + '_)>, Sized]] @19 storage_dead(@19) @0 := () drop[{impl Drop for String}] string@11 From af5e49f331165e63ca25071f2335da38815fc1e9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 10 Jul 2025 17:29:13 +0200 Subject: [PATCH 4/5] Translate existential predicates as a binder --- charon-ml/src/PrintTypes.ml | 1 - .../src/generated/Generated_GAstOfJson.ml | 33 +-- charon-ml/src/generated/Generated_Types.ml | 222 ++++++++--------- charon/Cargo.lock | 6 +- charon/src/ast/expressions_utils.rs | 24 +- charon/src/ast/types.rs | 42 ++-- charon/src/ast/visitor.rs | 2 +- .../translate/translate_trait_objects.rs | 124 +++++----- .../translate/translate_types.rs | 18 +- charon/src/bin/generate-ml/main.rs | 4 +- charon/src/name_matcher/mod.rs | 1 - charon/src/pretty/fmt_with_ctx.rs | 34 +-- charon/tests/ui/dyn-trait.out | 20 +- charon/tests/ui/result-unwrap.out | 6 +- charon/tests/ui/simple/dyn-fn.out | 229 ++++++++++++++++++ charon/tests/ui/simple/dyn-fn.rs | 11 + .../tests/ui/simple/generic-cast-to-dyn.out | 12 +- charon/tests/ui/unsize.out | 16 +- 18 files changed, 471 insertions(+), 334 deletions(-) create mode 100644 charon/tests/ui/simple/dyn-fn.out create mode 100644 charon/tests/ui/simple/dyn-fn.rs diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 22e11885d..9c5497eb5 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -291,7 +291,6 @@ and ty_to_string (env : 'a fmt_env) (ty : ty) : string = let fn = fn_ptr_to_string env f.binder_value in fn | TDynTrait _ -> "dyn (TODO)" - | TExistentialPlaceholder -> "_" | TError msg -> "type_error (\"" ^ msg ^ "\")" (** Return two lists: diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index fb2048f1e..148693e10 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -197,6 +197,7 @@ and binder_kind_of_json (ctx : of_json_ctx) (js : json) : let* x_1 = trait_item_name_of_json ctx x_1 in Ok (BKTraitMethod (x_0, x_1)) | `String "InherentImplBlock" -> Ok BKInherentImplBlock + | `String "Dyn" -> Ok BKDyn | `String "Other" -> Ok BKOther | _ -> Error "") @@ -604,25 +605,9 @@ and dyn_predicate_of_json (ctx : of_json_ctx) (js : json) : (dyn_predicate, string) result = combine_error_msgs js __FUNCTION__ (match js with - | `Assoc [ ("Trait", trait) ] -> - let* trait = trait_decl_ref_of_json ctx trait in - Ok (Trait trait) - | `Assoc [ ("Projection", projection) ] -> - let* projection = dyn_type_constraint_of_json ctx projection in - Ok (Projection projection) - | _ -> Error "") - -and dyn_type_constraint_of_json (ctx : of_json_ctx) (js : json) : - (dyn_type_constraint, string) result = - combine_error_msgs js __FUNCTION__ - (match js with - | `Assoc - [ ("trait_item", trait_item); ("generics", generics); ("term", term) ] - -> - let* trait_item = trait_item_name_of_json ctx trait_item in - let* generics = box_of_json generic_args_of_json ctx generics in - let* term = ty_of_json ctx term in - Ok ({ trait_item; generics; term } : dyn_type_constraint) + | `Assoc [ ("binder", binder) ] -> + let* binder = binder_of_json ty_of_json ctx binder in + Ok ({ binder } : dyn_predicate) | _ -> Error "") and field_of_json (ctx : of_json_ctx) (js : json) : (field, string) result = @@ -1807,12 +1792,9 @@ and ty_of_json (ctx : of_json_ctx) (js : json) : (ty, string) result = let* x_0 = trait_ref_of_json ctx x_0 in let* x_1 = trait_item_name_of_json ctx x_1 in Ok (TTraitType (x_0, x_1)) - | `Assoc [ ("DynTrait", `List [ x_0; x_1 ]) ] -> - let* x_0 = - list_of_json (region_binder_of_json dyn_predicate_of_json) ctx x_0 - in - let* x_1 = region_of_json ctx x_1 in - Ok (TDynTrait (x_0, x_1)) + | `Assoc [ ("DynTrait", dyn_trait) ] -> + let* dyn_trait = dyn_predicate_of_json ctx dyn_trait in + Ok (TDynTrait dyn_trait) | `Assoc [ ("FnPtr", fn_ptr) ] -> let* fn_ptr = region_binder_of_json @@ -1823,7 +1805,6 @@ and ty_of_json (ctx : of_json_ctx) (js : json) : (ty, string) result = | `Assoc [ ("FnDef", fn_def) ] -> let* fn_def = region_binder_of_json fn_ptr_of_json ctx fn_def in Ok (TFnDef fn_def) - | `String "ExistentialPlaceholder" -> Ok TExistentialPlaceholder | `Assoc [ ("Error", error) ] -> let* error = string_of_json ctx error in Ok (TError error) diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index 0a431d980..5dab6011f 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -190,9 +190,43 @@ class virtual ['self] map_ty_base_base = { index; name } end +(* Ancestors for the ty visitors *) +class ['self] iter_ty_base = + object (self : 'self) + inherit [_] iter_ty_base_base + method visit_span : 'env -> span -> unit = fun _ _ -> () + end + +class ['self] map_ty_base = + object (self : 'self) + inherit [_] map_ty_base_base + method visit_span : 'env -> span -> span = fun _ x -> x + end + +(** A value of type [T] bound by generic parameters. Used in any context where + we're adding generic parameters that aren't on the top-level item, e.g. + [for<'a>] clauses (uses [RegionBinder] for now), trait methods, GATs (TODO). +*) +type 'a0 binder = { + binder_params : generic_params; + binder_value : 'a0; + (** Named this way to highlight accesses to the inner value that might be + handling parameters incorrectly. Prefer using helper methods. *) +} + +and binder_kind = + | BKTraitMethod of trait_decl_id * trait_item_name + (** The parameters of a trait method. Used in the [methods] lists in trait + decls and trait impls. *) + | BKInherentImplBlock + (** The parameters bound in a non-trait [impl] block. Used in the [Name]s + of inherent methods. *) + | BKDyn (** Binder used for [dyn Trait] existential predicates. *) + | BKOther (** Some other use of a binder outside the main Charon ast. *) + (** An built-in function identifier, identifying a function coming from a standard library. *) -type builtin_fun_id = +and builtin_fun_id = | BoxNew (** [alloc::boxed::Box::new] *) | ArrayToSliceShared (** Cast an array as a slice. @@ -249,23 +283,25 @@ and builtin_ty = | TSlice (** Primitive type *) | TStr (** Primitive type *) -(** A predicate in a [dyn Trait] type. These predicates apply to an - existentially quentified type, represented as - [TyKind::ExistentialPlaceholder]. *) -and dyn_predicate = - | Trait of trait_decl_ref - (** Trait predicate that the target type must satisfy. *) - | Projection of dyn_type_constraint - (** Projection associated to the principal trait of this [dyn Trait]. We - don't currently support other projections. *) - -(** A projection of the form [TraitItemName = Ty], where the - [TraitItemName] is an associate type of the principal trait of a [dyn Trait] - type. *) -and dyn_type_constraint = { - trait_item : trait_item_name; - generics : generic_args; - term : ty; +(** A const generic variable in a signature or binder. *) +and const_generic_var = { + index : const_generic_var_id; + (** Index identifying the variable among other variables bound at the same + level. *) + name : string; (** Const generic name *) + ty : literal_type; (** Type of the const generic *) +} + +(** The contents of a [dyn Trait] type. *) +and dyn_predicate = { + binder : ty binder; + (** This binder binds a single type [T], which is considered existentially + quantified. The predicates in the binder apply to [T] and represent + the [dyn Trait] constraints. E.g. [dyn Iterator + Send] is + represented as [exists + Send> T]. + + Only the first trait clause may have methods. We use the vtable of + this trait in the [dyn Trait] pointer metadata. *) } and fn_ptr = { func : fun_id_or_trait_method_ref; generics : generic_args } @@ -300,9 +336,31 @@ and generic_args = { trait_refs : trait_ref list; } +(** Generic parameters for a declaration. We group the generics which come from + the Rust compiler substitutions (the regions, types and const generics) as + well as the trait clauses. The reason is that we consider that those are + parameters that need to be filled. We group in a different place the + predicates which are not trait clauses, because those enforce constraints + but do not need to be filled with witnesses/instances. *) +and generic_params = { + regions : region_var list; + types : type_var list; + const_generics : const_generic_var list; + trait_clauses : trait_clause list; + regions_outlive : (region, region) outlives_pred region_binder list; + (** The first region in the pair outlives the second region *) + types_outlive : (ty, region) outlives_pred region_binder list; + (** The type outlives the region *) + trait_type_constraints : trait_type_constraint region_binder list; + (** Constraints over trait associated types *) +} + (** Reference to a global declaration. *) and global_decl_ref = { id : global_decl_id; generics : generic_args } +(** .0 outlives .1 *) +and ('a0, 'a1) outlives_pred = 'a0 * 'a1 + and ref_kind = RMut | RShared and region = @@ -326,6 +384,17 @@ and region_id = (RegionId.id[@visitors.opaque]) (** A region variable in a signature or binder. *) and region_var = (region_id, string option) indexed_var +(** A trait predicate in a signature, of the form [Type: Trait]. This + functions like a variable binder, to which variables of the form + [TraitRefKind::Clause] can refer to. *) +and trait_clause = { + clause_id : trait_clause_id; + (** Index identifying the clause among other clauses bound at the same + level. *) + span : span option; + trait : trait_decl_ref region_binder; (** The trait that is implemented. *) +} + (** A predicate of the form [Type: Trait]. About the generics, if we write: @@ -418,6 +487,19 @@ and trait_instance_id = (** The automatically-generated implementation for [dyn Trait]. *) | UnknownTrait of string (** For error reporting. *) +(** A constraint over a trait associated type. + + Example: + {@rust[ + T : Foo + ^^^^^^^^^^ + ]} *) +and trait_type_constraint = { + trait_ref : trait_ref; + type_name : trait_item_name; + ty : ty; +} + and ty = | TAdt of type_decl_ref (** An ADT. Note that here ADTs are very general. They can be: @@ -459,16 +541,7 @@ and ty = type Bar; // type associated to the trait Foo } ]} *) - | TDynTrait of dyn_predicate region_binder list * region - (** [dyn Trait] - - This carries an existentially quantified list of predicates, e.g. - [exists where T: Into]. The predicate must quantify over a - single type and no any regions or constants. - - Only the first Predicate is used as the *principal* predicate, i.e. - the one that corresponds to a vtable. It is uniquely of the - [ExistentialTraitRef] type. *) + | TDynTrait of dyn_predicate (** [dyn Trait] *) | TFnPtr of (ty list * ty) region_binder (** Function pointer type. This is a literal pointer to a region of memory that contains a callable function. This is a function signature with @@ -485,11 +558,6 @@ and ty = given that the type here is polymorpohic in the late-bound variables (those that could appear in a function pointer type like [for<'a> fn(&'a u32)]), we need to bind them here. *) - | TExistentialPlaceholder - (** Fake type used in [dyn Trait] predicates: such a predicate has the - [Self] type existentially quantified. In order for generics to stay - consistent, we use this placeholder to represent the existentially - quantified type. *) | TError of string (** A type that could not be computed or was incorrect. *) (** Reference to a type declaration or builtin type. *) @@ -512,6 +580,9 @@ and type_id = Vec, Cell... The Array and Slice types were initially modelled as primitive in the [Ty] type. We decided to move them to built-in types as it allows for more uniform treatment throughout the codebase. *) + +(** A type variable in a signature or binder. *) +and type_var = (type_var_id, string) indexed_var [@@deriving show, eq, @@ -521,7 +592,7 @@ and type_id = name = "iter_ty"; monomorphic = [ "env" ]; variety = "iter"; - ancestors = [ "iter_ty_base_base" ]; + ancestors = [ "iter_ty_base" ]; nude = true (* Don't inherit VisitorsRuntime *); }, visitors @@ -529,7 +600,7 @@ and type_id = name = "map_ty"; monomorphic = [ "env" ]; variety = "map"; - ancestors = [ "map_ty_base_base" ]; + ancestors = [ "map_ty_base" ]; nude = true (* Don't inherit VisitorsRuntime *); }] @@ -537,14 +608,12 @@ and type_id = class ['self] iter_type_decl_base = object (self : 'self) inherit [_] iter_ty - method visit_span : 'env -> span -> unit = fun _ _ -> () method visit_attr_info : 'env -> attr_info -> unit = fun _ _ -> () end class ['self] map_type_decl_base = object (self : 'self) inherit [_] map_ty - method visit_span : 'env -> span -> span = fun _ x -> x method visit_attr_info : 'env -> attr_info -> attr_info = fun _ x -> x end @@ -559,26 +628,6 @@ type abort_kind = (** Unwind had to stop for Abi reasons or because cleanup code panicked again. *) -(** A value of type [T] bound by generic parameters. Used in any context where - we're adding generic parameters that aren't on the top-level item, e.g. - [for<'a>] clauses (uses [RegionBinder] for now), trait methods, GATs (TODO). -*) -and 'a0 binder = { - binder_params : generic_params; - binder_value : 'a0; - (** Named this way to highlight accesses to the inner value that might be - handling parameters incorrectly. Prefer using helper methods. *) -} - -and binder_kind = - | BKTraitMethod of trait_decl_id * trait_item_name - (** The parameters of a trait method. Used in the [methods] lists in trait - decls and trait impls. *) - | BKInherentImplBlock - (** The parameters bound in a non-trait [impl] block. Used in the [Name]s - of inherent methods. *) - | BKOther (** Some other use of a binder outside the main Charon ast. *) - (** Additional information for closures. *) and closure_info = { kind : closure_kind; @@ -593,16 +642,6 @@ and closure_info = { } and closure_kind = Fn | FnMut | FnOnce - -(** A const generic variable in a signature or binder. *) -and const_generic_var = { - index : const_generic_var_id; - (** Index identifying the variable among other variables bound at the same - level. *) - name : string; (** Const generic name *) - ty : literal_type; (** Type of the const generic *) -} - and disambiguator = (Disambiguator.id[@visitors.opaque]) (** Layout of the discriminant. Describes the offset of the discriminant field @@ -622,25 +661,6 @@ and field = { and field_id = (FieldId.id[@visitors.opaque]) -(** Generic parameters for a declaration. We group the generics which come from - the Rust compiler substitutions (the regions, types and const generics) as - well as the trait clauses. The reason is that we consider that those are - parameters that need to be filled. We group in a different place the - predicates which are not trait clauses, because those enforce constraints - but do not need to be filled with witnesses/instances. *) -and generic_params = { - regions : region_var list; - types : type_var list; - const_generics : const_generic_var list; - trait_clauses : trait_clause list; - regions_outlive : (region, region) outlives_pred region_binder list; - (** The first region in the pair outlives the second region *) - types_outlive : (ty, region) outlives_pred region_binder list; - (** The type outlives the region *) - trait_type_constraints : trait_type_constraint region_binder list; - (** Constraints over trait associated types *) -} - (** There are two kinds of [impl] blocks: {ul {- impl blocks linked to a type ("inherent" impl blocks following Rust @@ -781,9 +801,6 @@ and layout = { *) and name = (path_elem list[@visitors.opaque]) -(** .0 outlives .1 *) -and ('a0, 'a1) outlives_pred = 'a0 * 'a1 - (** See the comments for [Name] *) and path_elem = | PeIdent of string * disambiguator @@ -816,30 +833,6 @@ and tag_encoding = Fields: - [untagged_variant] *) -(** A trait predicate in a signature, of the form [Type: Trait]. This - functions like a variable binder, to which variables of the form - [TraitRefKind::Clause] can refer to. *) -and trait_clause = { - clause_id : trait_clause_id; - (** Index identifying the clause among other clauses bound at the same - level. *) - span : span option; - trait : trait_decl_ref region_binder; (** The trait that is implemented. *) -} - -(** A constraint over a trait associated type. - - Example: - {@rust[ - T : Foo - ^^^^^^^^^^ - ]} *) -and trait_type_constraint = { - trait_ref : trait_ref; - type_name : trait_item_name; - ty : ty; -} - (** A type declaration. Types can be opaque or transparent. @@ -890,9 +883,6 @@ and type_decl_kind = (** Used if an error happened during the extraction, and we don't panic on error. *) -(** A type variable in a signature or binder. *) -and type_var = (type_var_id, string) indexed_var - (** A placeholder for the vtable of a trait object. To be implemented in the future when [dyn Trait] is fully supported. *) and v_table = unit diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 28423401b..cfbc243af 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -788,7 +788,7 @@ checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" [[package]] name = "hax-adt-into" version = "0.3.1" -source = "git+https://github.com/AeneasVerif/hax?branch=main#d6d523d2ac84ea9f605ee6da429ab29e2ae9f8c4" +source = "git+https://github.com/AeneasVerif/hax?branch=main#d30960bf206f65f89567937978ad8fa710eb79e8" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -799,7 +799,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.3.1" -source = "git+https://github.com/AeneasVerif/hax?branch=main#d6d523d2ac84ea9f605ee6da429ab29e2ae9f8c4" +source = "git+https://github.com/AeneasVerif/hax?branch=main#d30960bf206f65f89567937978ad8fa710eb79e8" dependencies = [ "extension-traits", "hax-adt-into", @@ -816,7 +816,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.3.1" -source = "git+https://github.com/AeneasVerif/hax?branch=main#d6d523d2ac84ea9f605ee6da429ab29e2ae9f8c4" +source = "git+https://github.com/AeneasVerif/hax?branch=main#d30960bf206f65f89567937978ad8fa710eb79e8" dependencies = [ "hax-adt-into", "schemars", diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs index 4212b0c46..7f08947f5 100644 --- a/charon/src/ast/expressions_utils.rs +++ b/charon/src/ast/expressions_utils.rs @@ -65,16 +65,8 @@ impl Place { Adt(tref) if matches!(tref.id, TypeId::Builtin(BuiltinTy::Box)) => { tref.generics.types[0].clone() } - Adt(..) - | TypeVar(_) - | Literal(_) - | Never - | TraitType(..) - | DynTrait(..) - | FnPtr(..) - | FnDef(..) - | Error(..) - | ExistentialPlaceholder => panic!("internal type error"), + Adt(..) | TypeVar(_) | Literal(_) | Never | TraitType(..) | DynTrait(..) + | FnPtr(..) | FnDef(..) | Error(..) => panic!("internal type error"), }; Place { ty: proj_ty, @@ -130,16 +122,8 @@ impl ProjectionElem { Adt(tref) if matches!(tref.id, TypeId::Builtin(BuiltinTy::Box)) => { tref.generics.types[0].clone() } - Adt(..) - | TypeVar(_) - | Literal(_) - | Never - | TraitType(..) - | DynTrait(..) - | FnPtr(..) - | FnDef(..) - | Error(..) - | ExistentialPlaceholder => { + Adt(..) | TypeVar(_) | Literal(_) | Never | TraitType(..) | DynTrait(..) + | FnPtr(..) | FnDef(..) | Error(..) => { // Type error return Err(()); } diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 2402c7f7f..585acd5bb 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -229,6 +229,8 @@ pub enum BinderKind { TraitMethod(TraitDeclId, TraitItemName), /// The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods. InherentImplBlock, + /// Binder used for `dyn Trait` existential predicates. + Dyn, /// Some other use of a binder outside the main Charon ast. Other, } @@ -314,6 +316,8 @@ pub enum PredicateOrigin { // } // ``` TraitItem(TraitItemName), + /// Clauses that are part of a `dyn Trait` type. + Dyn, } // rustc counts bytes in layouts as u64 @@ -777,13 +781,7 @@ pub enum TyKind { /// ``` TraitType(TraitRef, TraitItemName), /// `dyn Trait` - /// - /// This carries an existentially quantified list of predicates, e.g. `exists where T: - /// Into`. The predicate must quantify over a single type and no any regions or constants. - /// - /// Only the first Predicate is used as the *principal* predicate, i.e. the one that - /// corresponds to a vtable. It is uniquely of the `ExistentialTraitRef` type. - DynTrait(Vec>, Region), + DynTrait(DynPredicate), /// Function pointer type. This is a literal pointer to a region of memory that /// contains a callable function. /// This is a function signature with limited generics: it only supports lifetime generics, not @@ -798,10 +796,6 @@ pub enum TyKind { /// variables (those that could appear in a function pointer type like `for<'a> fn(&'a u32)`), /// we need to bind them here. FnDef(RegionBinder), - /// Fake type used in `dyn Trait` predicates: such a predicate has the `Self` type - /// existentially quantified. In order for generics to stay consistent, we use this placeholder to - /// represent the existentially quantified type. - ExistentialPlaceholder, /// A type that could not be computed or was incorrect. #[drive(skip)] Error(String), @@ -902,22 +896,14 @@ pub struct FunSig { pub output: Ty, } -/// A projection of the form `TraitItemName = Ty`, where the `TraitItemName` is an -/// associate type of the principal trait of a `dyn Trait` type. +/// The contents of a `dyn Trait` type. #[derive(Debug, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] -pub struct DynTypeConstraint { - pub trait_item: TraitItemName, - pub generics: BoxedArgs, - pub term: Ty, -} - -/// A predicate in a `dyn Trait` type. These predicates apply to an existentially quentified type, -/// represented as `TyKind::ExistentialPlaceholder`. -#[derive(Debug, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] -pub enum DynPredicate { - /// Trait predicate that the target type must satisfy. - Trait(TraitDeclRef), - /// Projection associated to the principal trait of this `dyn Trait`. We don't currently - /// support other projections. - Projection(DynTypeConstraint), +pub struct DynPredicate { + /// This binder binds a single type `T`, which is considered existentially quantified. The + /// predicates in the binder apply to `T` and represent the `dyn Trait` constraints. + /// E.g. `dyn Iterator + Send` is represented as `exists + Send> T`. + /// + /// Only the first trait clause may have methods. We use the vtable of this trait in the `dyn + /// Trait` pointer metadata. + pub binder: Binder, } diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs index 17a5d10d9..532626086 100644 --- a/charon/src/ast/visitor.rs +++ b/charon/src/ast/visitor.rs @@ -43,7 +43,7 @@ use indexmap::IndexMap; drive( AbortKind, Assert, BinOp, Body, BorrowKind, BuiltinFunId, BuiltinIndexOp, BuiltinTy, Call, CastKind, ClosureInfo, ClosureKind, ConstGenericVar, ConstGenericVarId, - Disambiguator, DynPredicate, DynTypeConstraint, Field, FieldId, FieldProjKind, FloatTy, FloatValue, + Disambiguator, DynPredicate, Field, FieldId, FieldProjKind, FloatTy, FloatValue, FnOperand, FunId, FunIdOrTraitMethodRef, FunSig, ImplElem, IntegerTy, Literal, LiteralTy, llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch, Locals, Name, NullOp, Opaque, Operand, PathElem, PlaceKind, ProjectionElem, RawConstantExpr, diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs index 38319a855..7714c3206 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -1,84 +1,76 @@ +use crate::translate::{translate_generics::BindingLevel, translate_predicates::PredicateLocation}; + use super::translate_ctx::*; use charon_lib::ast::*; use hax_frontend_exporter as hax; impl ItemTransCtx<'_, '_> { pub fn check_at_most_one_pred_has_methods( - &self, + &mut self, span: Span, - preds: &Vec>, + preds: &hax::GenericPredicates, ) -> Result<(), Error> { - let all_ex_trait_ref = preds.iter().filter_map(|bound| { - if let hax::ExistentialPredicate::Trait(trait_ref) = &bound.value { - Some(trait_ref) - } else { - None + // Only the first clause is allowed to have methods. + for (clause, _) in preds.predicates.iter().skip(1) { + if let hax::ClauseKind::Trait(trait_predicate) = clause.kind.hax_skip_binder_ref() { + let trait_def_id = &trait_predicate.trait_ref.def_id; + let trait_def = self.hax_def(trait_def_id)?; + let has_methods = match trait_def.kind() { + hax::FullDefKind::Trait { items, .. } => items + .iter() + .any(|(assoc, _)| matches!(assoc.kind, hax::AssocKind::Fn { .. })), + hax::FullDefKind::TraitAlias { .. } => false, + _ => unreachable!(), + }; + if has_methods { + raise_error!( + self, + span, + "`dyn Trait` with multiple method-bearing predicates is not supported" + ); + } } - }); - if all_ex_trait_ref.count() > 1 { - raise_error!( - self, - span, - "`dyn Trait` with multiple method-bearing predicates is not supported" - ); } Ok(()) } - /// Translate generics for an exitential predicate. These generics are missing a `Self` type, - /// which we add here, represented with `ExistentialPlaceholder`. - fn translate_ex_generics( - &mut self, - span: Span, - args: &[hax::GenericArg], - ) -> Result, Error> { - let mut generics = Box::new(self.translate_generic_args(span, args, &[])?); - generics.types.insert_and_shift_ids( - TypeVarId::from_usize(0), - TyKind::ExistentialPlaceholder.into_ty(), - ); - Ok(generics) - } - - pub fn translate_existential_predicate( + pub fn translate_existential_predicates( &mut self, span: Span, - pred: &hax::ExistentialPredicate, + self_ty: &hax::ParamTy, + preds: &hax::GenericPredicates, + region: &hax::Region, ) -> Result { - Ok(match pred { - hax::ExistentialPredicate::Trait(tref) => DynPredicate::Trait(TraitDeclRef { - id: self.register_trait_decl_id(span, &tref.def_id), - generics: self.translate_ex_generics(span, &tref.args)?, - }), - hax::ExistentialPredicate::AutoTrait(def_id) => { - let trait_id = self.register_trait_decl_id(span, def_id); - let ty = TyKind::ExistentialPlaceholder.into_ty(); - let tref = TraitDeclRef { - id: trait_id, - generics: Box::new(GenericArgs::new_types([ty].into())), - }; - DynPredicate::Trait(tref) - } - hax::ExistentialPredicate::Projection(proj) => { - // TODO: this is incorrect if the projection doesn't apply to the principal. - let args = self.translate_ex_generics(span, &proj.args)?; - let name = self.t_ctx.translate_trait_item_name(&proj.def_id)?; - let term = match &proj.term { - hax::Term::Ty(ty) => self.translate_ty(span, ty)?, - hax::Term::Const(_) => { - raise_error!( - self, - span, - "`dyn Trait` with associated const constraints are not supported", - ) - } - }; - DynPredicate::Projection(DynTypeConstraint { - trait_item: name, - generics: args, - term, - }) - } - }) + // This is a robustness check: the current version of Rustc + // accepts at most one method-bearing predicate in a trait object. + // But things may change in the future. + self.check_at_most_one_pred_has_methods(span, preds)?; + + // Translate the region outside the binder. + let region = self.translate_region(span, region)?; + let region = region.move_under_binder(); + + // Add a binder that contains the existentially quantified type. + self.binding_levels.push(BindingLevel::new(true)); + + // Add the existentially quantified type. + let ty_id = self + .innermost_binder_mut() + .push_type_var(self_ty.index, self_ty.name.clone()); + let ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(ty_id)).into_ty(); + + self.innermost_binder_mut() + .params + .types_outlive + .push(RegionBinder::empty(OutlivesPred(ty.clone(), region))); + self.register_predicates(preds, PredicateOrigin::Dyn, &PredicateLocation::Base)?; + + let params = self.binding_levels.pop().unwrap().params; + let binder = Binder { + params: params, + skip_binder: ty, + kind: BinderKind::Dyn, + }; + Ok(DynPredicate { binder }) } } diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 42d31abd2..983826c24 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -214,21 +214,9 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { TyKind::Adt(tref) } - hax::TyKind::Dynamic(preds, region, ..) => { - // This is a robustness check: the current version of Rustc - // accepts at most one method-bearing predicate in a trait object. - // But things may change in the future. - self.check_at_most_one_pred_has_methods(span, &preds)?; - let region = self.translate_region(span, region)?; - let preds = preds - .iter() - .map(|bound_pred| { - self.translate_region_binder(span, bound_pred, |ctx, x| { - ctx.translate_existential_predicate(span, x) - }) - }) - .try_collect()?; - TyKind::DynTrait(preds, region) + hax::TyKind::Dynamic(self_ty, preds, region) => { + let pred = self.translate_existential_predicates(span, self_ty, preds, region)?; + TyKind::DynTrait(pred) } hax::TyKind::Infer(_) => { diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index a18a56449..855631400 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1220,7 +1220,7 @@ fn generate_ml( ancestors: &["ty_base_base"], name: "ty", reduce: false, - extra_types: &[], + extra_types: &["span"], })), &[ "TyKind", "TraitImplRef", @@ -1233,7 +1233,7 @@ fn generate_ml( name: "type_decl", reduce: false, extra_types: &[ - "span", "attr_info" + "attr_info" ], })), &[ "Binder", diff --git a/charon/src/name_matcher/mod.rs b/charon/src/name_matcher/mod.rs index c81da0f72..62e006ecc 100644 --- a/charon/src/name_matcher/mod.rs +++ b/charon/src/name_matcher/mod.rs @@ -130,7 +130,6 @@ impl Pattern { | TyKind::DynTrait(..) | TyKind::FnPtr(..) | TyKind::FnDef(..) - | TyKind::ExistentialPlaceholder | TyKind::Error(..) => false, } } diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 0b2d3a56b..9fe01e29c 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -350,26 +350,10 @@ impl FmtWithCtx for DeclarationGroup { impl FmtWithCtx for DynPredicate { fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { - match self { - DynPredicate::Trait(trait_ref) => { - write!(f, "{}", trait_ref.with_ctx(ctx)) - } - DynPredicate::Projection(proj) => { - write!(f, "{}", proj.with_ctx(ctx)) - } - } - } -} - -impl FmtWithCtx for DynTypeConstraint { - fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { - write!( - f, - "{}::{} = {}", - self.trait_item.0, - self.generics.with_ctx(ctx), - self.term.with_ctx(ctx) - ) + let ctx = &ctx.push_binder(Cow::Borrowed(&self.binder.params)); + let ty = self.binder.skip_binder.with_ctx(ctx); + let clauses = self.binder.params.formatted_clauses(ctx).format(" + "); + write!(f, "exists<{ty}> {clauses}") } } @@ -1778,12 +1762,8 @@ impl FmtWithCtx for Ty { TyKind::TraitType(trait_ref, name) => { write!(f, "{}::{name}", trait_ref.with_ctx(ctx),) } - TyKind::DynTrait(preds, region) => { - let preds = preds - .iter() - .map(|p| p.fmt_as_for(ctx).to_string()) - .format(" + "); - write!(f, "(dyn {} + {})", preds, region.with_ctx(ctx)) + TyKind::DynTrait(pred) => { + write!(f, "(dyn {})", pred.with_ctx(ctx)) } TyKind::FnPtr(io) => { write!(f, "{}", io.with_ctx(ctx)) @@ -1795,8 +1775,6 @@ impl FmtWithCtx for Ty { }; write!(f, "{value}",) } - // To make sure this is not definable as ADT or so - TyKind::ExistentialPlaceholder => write!(f, "_"), TyKind::Error(msg) => write!(f, "type_error(\"{msg}\")"), } } diff --git a/charon/tests/ui/dyn-trait.out b/charon/tests/ui/dyn-trait.out index a7585aa5d..98e164156 100644 --- a/charon/tests/ui/dyn-trait.out +++ b/charon/tests/ui/dyn-trait.out @@ -154,22 +154,22 @@ where } // Full name: test_crate::construct -fn construct(@1: T) -> alloc::boxed::Box<(dyn Display<_> + 'static)>[MetaSized<(dyn Display<_> + '_)>, Sized] +fn construct(@1: T) -> alloc::boxed::Box<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : 'static)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized] where [@TraitClause0]: Sized, [@TraitClause1]: Display, T : 'static, // Full name: test_crate::destruct -fn destruct<'_0>(@1: &'_0 ((dyn Display<_> + '_0))) -> String +fn destruct<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_0))) -> String { let @0: String; // return - let x@1: &'_ ((dyn Display<_> + '_)); // arg #1 - let @2: &'_ ((dyn Display<_> + '_)); // anonymous local + let x@1: &'_ ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)); // arg #1 + let @2: &'_ ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)); // anonymous local storage_live(@2) @2 := &*(x@1) - @0 := {impl ToString for T}::to_string<'_, (dyn Display<_> + '_)>[MetaSized<(dyn Display<_> + '_)>, Display<(dyn Display<_> + '_)>](move (@2)) + @0 := {impl ToString for T}::to_string<'_, (dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Display<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>](move (@2)) storage_dead(@2) return } @@ -178,13 +178,13 @@ fn destruct<'_0>(@1: &'_0 ((dyn Display<_> + '_0))) -> String fn combine() // Full name: test_crate::foo -fn foo<'_0, '_1, T>(@1: &'_0 ((dyn for<'a> Fn<_, (&'a (T))> + for<'a> Output::<_, (&'a (T))> = T + 'static)), @2: &'_1 ((dyn PartialEq<_, Option[@TraitClause0]> + '_1))) +fn foo<'_0, '_1, T>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a (T))> + _dyn : 'static + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = T)), @2: &'_1 ((dyn exists<_dyn> [@TraitClause0]: PartialEq<_dyn, Option[@TraitClause0]> + _dyn : '_1))) where [@TraitClause0]: Sized, { let @0: (); // return - let @1: &'_ ((dyn for<'a> Fn<_, (&'a (T))> + for<'a> Output::<_, (&'a (T))> = T + '_)); // arg #1 - let @2: &'_ ((dyn PartialEq<_, Option[@TraitClause0]> + '_)); // arg #2 + let @1: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a (T))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = T)); // arg #1 + let @2: &'_ ((dyn exists<_dyn> [@TraitClause0]: PartialEq<_dyn, Option[@TraitClause0]> + _dyn : '_)); // arg #2 @0 := () @0 := () @@ -192,10 +192,10 @@ where } // Full name: test_crate::bar -fn bar<'_0>(@1: &'_0 ((dyn for<'_0> Fn<_, (&'_0_0 ((dyn Display<_> + '_0_0)))> + for<'_0> Output::<_, (&'_0_0 ((dyn Display<_> + '_0_0)))> = () + '_0))) +fn bar<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: for<'_0> Fn<_dyn, (&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_2_0)))> + _dyn : '_0 + for<'_0> @TraitClause1_0::parent_clause1::parent_clause1::Output = ()))) { let @0: (); // return - let @1: &'_ ((dyn for<'_0> Fn<_, (&'_0_0 ((dyn Display<_> + '_0_0)))> + for<'_0> Output::<_, (&'_0_0 ((dyn Display<_> + '_0_0)))> = () + '_)); // arg #1 + let @1: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'_0> Fn<_dyn, (&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_2_0)))> + _dyn : '_ + for<'_0> @TraitClause1_0::parent_clause1::parent_clause1::Output = ())); // arg #1 @0 := () @0 := () diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out index 7dec7da42..b0317626a 100644 --- a/charon/tests/ui/result-unwrap.out +++ b/charon/tests/ui/result-unwrap.out @@ -187,7 +187,7 @@ where [@TraitClause0]: Drop, // Full name: core::result::unwrap_failed -fn unwrap_failed<'_0, '_1>(@1: &'_0 (Str), @2: &'_1 ((dyn Debug<_> + '_1))) -> ! +fn unwrap_failed<'_0, '_1>(@1: &'_0 (Str), @2: &'_1 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_1))) -> ! pub fn core::result::{Result[@TraitClause0, @TraitClause1]}::unwrap(@1: Result[@TraitClause0, @TraitClause1]) -> T where @@ -199,7 +199,7 @@ where let self@1: Result[@TraitClause0, @TraitClause1]; // arg #1 let e@2: E; // local let @3: !; // anonymous local - let @4: &'_ ((dyn Debug<_> + '_)); // anonymous local + let @4: &'_ ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)); // anonymous local let @5: &'_ (E); // anonymous local storage_live(e@2) @@ -214,7 +214,7 @@ where e@2 := move ((self@1 as variant Result::Err).0) storage_live(@4) @5 := &e@2 - @4 := unsize_cast<&'_ (E), &'_ ((dyn Debug<_> + '_)), @TraitClause2>(copy (@5)) + @4 := unsize_cast<&'_ (E), &'_ ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)), @TraitClause2>(copy (@5)) @3 := unwrap_failed<'_, '_>(const ("called `Result::unwrap()` on an `Err` value"), move (@4)) }, } diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out new file mode 100644 index 000000000..dab6b38e6 --- /dev/null +++ b/charon/tests/ui/simple/dyn-fn.out @@ -0,0 +1,229 @@ +# Final LLBC before serialization: + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized +} + +// Full name: core::marker::Tuple +#[lang_item("tuple_trait")] +pub trait Tuple +{ + parent_clause0 : [@TraitClause0]: MetaSized +} + +// Full name: core::ops::drop::Drop +#[lang_item("drop")] +pub trait Drop +{ + parent_clause0 : [@TraitClause0]: MetaSized + fn drop<'_0> = drop<'_0_0, Self>[Self] +} + +// Full name: core::ops::drop::Drop::drop +pub fn drop<'_0, Self>(@1: &'_0 mut (Self)) +where + [@TraitClause0]: Drop, + +// Full name: core::ops::function::FnOnce +#[lang_item("fn_once")] +pub trait FnOnce +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + parent_clause2 : [@TraitClause2]: Tuple + parent_clause3 : [@TraitClause3]: Sized + type Output + fn call_once = core::ops::function::FnOnce::call_once[Self] +} + +// Full name: core::ops::function::FnMut +#[lang_item("fn_mut")] +pub trait FnMut +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnOnce + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] +} + +// Full name: core::ops::function::Fn +#[lang_item("r#fn")] +pub trait Fn +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnMut + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] +} + +pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output +where + [@TraitClause0]: Fn, + +pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output +where + [@TraitClause0]: FnMut, + +pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output +where + [@TraitClause0]: FnOnce, + +// Full name: test_crate::takes_fn +fn takes_fn<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_0 + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool))) +{ + let @0: (); // return + let f@1: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)); // arg #1 + let counter@2: u32; // local + let @3: bool; // anonymous local + let @4: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)); // anonymous local + let @5: (&'_ mut (u32)); // anonymous local + let @6: &'_ mut (u32); // anonymous local + let @7: &'_ mut (u32); // anonymous local + + storage_live(counter@2) + counter@2 := const (0 : u32) + storage_live(@3) + storage_live(@4) + @4 := &*(f@1) + storage_live(@5) + storage_live(@6) + storage_live(@7) + @7 := &mut counter@2 + @6 := &two-phase-mut *(@7) + @5 := (move (@6)) + @3 := Fn<(dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool), (&'_ mut (u32))>::call<'_>(move (@4), move (@5)) + if move (@3) { + storage_dead(@7) + storage_dead(@6) + storage_dead(@5) + storage_dead(@4) + @0 := () + } + else { + storage_dead(@7) + storage_dead(@6) + storage_dead(@5) + storage_dead(@4) + @0 := () + } + storage_dead(@3) + storage_dead(counter@2) + @0 := () + return +} + +// Full name: test_crate::gives_fn::closure +struct closure {} + +// Full name: test_crate::gives_fn::{impl Fn<(&'_ mut (u32))> for closure}::call +fn {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_1>(@1: &'_1 (closure), @2: (&'_0 mut (u32))) -> bool +{ + let @0: bool; // return + let @1: &'_ (closure); // arg #1 + let tupled_args@2: (&'_0 mut (u32)); // arg #2 + let counter@3: &'_ mut (u32); // local + let @4: u32; // anonymous local + + storage_live(counter@3) + storage_live(@4) + counter@3 := move ((tupled_args@2).0) + @4 := copy (*(counter@3)) panic.+ const (1 : u32) + *(counter@3) := move (@4) + @0 := const (true) + return +} + +// Full name: test_crate::gives_fn::{impl FnMut<(&'_ mut (u32))> for closure}::call_mut +fn {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_1>(@1: &'_1 mut (closure), @2: (&'_0 mut (u32))) -> bool +{ + let @0: bool; // return + let state@1: &'_1 mut (closure); // arg #1 + let args@2: (&'_0 mut (u32)); // arg #2 + let @3: &'_ (closure); // anonymous local + + storage_live(@3) + @3 := &*(state@1) + @0 := {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_>(move (@3), move (args@2)) + return +} + +// Full name: test_crate::gives_fn::{impl FnOnce<(&'_ mut (u32))> for closure}::call_once +fn {impl FnOnce<(&'_ mut (u32))> for closure}::call_once<'_0>(@1: closure, @2: (&'_0 mut (u32))) -> bool +{ + let @0: bool; // return + let @1: closure; // arg #1 + let @2: (&'_ mut (u32)); // arg #2 + let @3: &'_ mut (closure); // anonymous local + + storage_live(@3) + @3 := &mut @1 + @0 := {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_>(move (@3), move (@2)) + drop[Drop] @1 + return +} + +// Full name: test_crate::gives_fn::{impl FnOnce<(&'_ mut (u32))> for closure} +impl<'_0> FnOnce<(&'_ mut (u32))> for closure { + parent_clause0 = MetaSized + parent_clause1 = Sized<(&'_ mut (u32))> + parent_clause2 = Tuple<(&'_ mut (u32))> + parent_clause3 = Sized + type Output = bool + fn call_once = {impl FnOnce<(&'_ mut (u32))> for closure}::call_once<'_0> +} + +// Full name: test_crate::gives_fn::{impl FnMut<(&'_ mut (u32))> for closure} +impl<'_0> FnMut<(&'_ mut (u32))> for closure { + parent_clause0 = MetaSized + parent_clause1 = {impl FnOnce<(&'_ mut (u32))> for closure}<'_0> + parent_clause2 = Sized<(&'_ mut (u32))> + parent_clause3 = Tuple<(&'_ mut (u32))> + fn call_mut<'_0> = {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_0_0> +} + +// Full name: test_crate::gives_fn::{impl Fn<(&'_ mut (u32))> for closure} +impl<'_0> Fn<(&'_ mut (u32))> for closure { + parent_clause0 = MetaSized + parent_clause1 = {impl FnMut<(&'_ mut (u32))> for closure}<'_0> + parent_clause2 = Sized<(&'_ mut (u32))> + parent_clause3 = Tuple<(&'_ mut (u32))> + fn call<'_0> = {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_0_0> +} + +// Full name: test_crate::gives_fn +fn gives_fn() +{ + let @0: (); // return + let @1: &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)); // anonymous local + let @2: &'_ (closure); // anonymous local + let @3: &'_ (closure); // anonymous local + let @4: closure; // anonymous local + + storage_live(@1) + storage_live(@2) + storage_live(@3) + storage_live(@4) + @4 := closure { } + @3 := &@4 + @2 := &*(@3) + @1 := unsize_cast<&'_ (closure), &'_ ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool)), {impl Fn<(&'_ mut (u32))> for closure}<'_>>(move (@2)) + storage_dead(@2) + @0 := takes_fn<'_>(move (@1)) + storage_dead(@1) + storage_dead(@4) + storage_dead(@3) + @0 := () + return +} + + + diff --git a/charon/tests/ui/simple/dyn-fn.rs b/charon/tests/ui/simple/dyn-fn.rs new file mode 100644 index 000000000..c71ace687 --- /dev/null +++ b/charon/tests/ui/simple/dyn-fn.rs @@ -0,0 +1,11 @@ +fn takes_fn(f: &dyn for<'a> Fn(&'a mut u32) -> bool) { + let mut counter = 0; + if f(&mut counter) {} +} + +fn gives_fn() { + takes_fn(&|counter| { + *counter += 1; + true + }) +} diff --git a/charon/tests/ui/simple/generic-cast-to-dyn.out b/charon/tests/ui/simple/generic-cast-to-dyn.out index a1a32b3ce..abdf997f2 100644 --- a/charon/tests/ui/simple/generic-cast-to-dyn.out +++ b/charon/tests/ui/simple/generic-cast-to-dyn.out @@ -31,25 +31,25 @@ pub trait Sized } // Full name: test_crate::foo -fn foo<'_0, T>(@1: &'_0 (T)) -> &'_0 ((dyn Any<_> + 'static)) +fn foo<'_0, T>(@1: &'_0 (T)) -> &'_0 ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : 'static)) where [@TraitClause0]: Sized, [@TraitClause1]: Any, { - let @0: &'_ ((dyn Any<_> + '_)); // return + let @0: &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)); // return let x@1: &'_ (T); // arg #1 - let @2: &'_ ((dyn Any<_> + '_)); // anonymous local - let @3: &'_ ((dyn Any<_> + '_)); // anonymous local + let @2: &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)); // anonymous local + let @3: &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)); // anonymous local let @4: &'_ (T); // anonymous local storage_live(@2) storage_live(@3) storage_live(@4) @4 := &*(x@1) - @3 := unsize_cast<&'_ (T), &'_ ((dyn Any<_> + '_)), @TraitClause1>(move (@4)) + @3 := unsize_cast<&'_ (T), &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)), @TraitClause1>(move (@4)) storage_dead(@4) @2 := &*(@3) - @0 := unsize_cast<&'_ ((dyn Any<_> + '_)), &'_ ((dyn Any<_> + '_)), Any<(dyn Any<_> + '_)>>(move (@2)) + @0 := unsize_cast<&'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)), &'_ ((dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)), Any<(dyn exists<_dyn> [@TraitClause0]: Any<_dyn> + _dyn : '_)>>(move (@2)) storage_dead(@3) storage_dead(@2) return diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out index fb5213c73..67e135068 100644 --- a/charon/tests/ui/unsize.out +++ b/charon/tests/ui/unsize.out @@ -163,14 +163,14 @@ fn foo() let @9: Rc>[MetaSized>, Sized]; // anonymous local let @10: Array; // anonymous local let string@11: String; // local - let @12: &'_ ((dyn Display<_> + '_)); // anonymous local + let @12: &'_ ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)); // anonymous local let @13: &'_ (String); // anonymous local let @14: &'_ (String); // anonymous local - let @15: alloc::boxed::Box<(dyn Display<_> + '_)>[MetaSized<(dyn Display<_> + '_)>, Sized]; // anonymous local + let @15: alloc::boxed::Box<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized]; // anonymous local let @16: alloc::boxed::Box[MetaSized, Sized]; // anonymous local let @17: String; // anonymous local let @18: &'_ (String); // anonymous local - let @19: Rc<(dyn Display<_> + '_)>[MetaSized<(dyn Display<_> + '_)>, Sized]; // anonymous local + let @19: Rc<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized]; // anonymous local let @20: Rc[MetaSized, Sized]; // anonymous local let @21: String; // anonymous local let @22: &'_ (String); // anonymous local @@ -215,7 +215,7 @@ fn foo() storage_live(@14) @14 := &string@11 @13 := &*(@14) - @12 := unsize_cast<&'_ (String), &'_ ((dyn Display<_> + '_)), {impl Display for String}>(move (@13)) + @12 := unsize_cast<&'_ (String), &'_ ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)), {impl Display for String}>(move (@13)) storage_dead(@13) storage_dead(@14) storage_dead(@12) @@ -227,11 +227,11 @@ fn foo() @17 := {impl Clone for String}::clone<'_>(move (@18)) storage_dead(@18) @16 := @BoxNew[Sized](move (@17)) - @15 := unsize_cast[MetaSized, Sized], alloc::boxed::Box<(dyn Display<_> + '_)>[MetaSized<(dyn Display<_> + '_)>, Sized], {impl Display for String}>(move (@16)) + @15 := unsize_cast[MetaSized, Sized], alloc::boxed::Box<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized], {impl Display for String}>(move (@16)) drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @16 storage_dead(@17) storage_dead(@16) - drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}<(dyn Display<_> + '_), Global>[MetaSized<(dyn Display<_> + '_)>, Sized]] @15 + drop[{impl Drop for alloc::boxed::Box[@TraitClause0, @TraitClause1]}<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_), Global>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized]] @15 storage_dead(@15) storage_live(@19) storage_live(@20) @@ -241,11 +241,11 @@ fn foo() @21 := {impl Clone for String}::clone<'_>(move (@22)) storage_dead(@22) @20 := alloc::rc::{Rc[@TraitClause0::parent_clause0, Sized]}::new[Sized](move (@21)) - @19 := unsize_cast[MetaSized, Sized], Rc<(dyn Display<_> + '_)>[MetaSized<(dyn Display<_> + '_)>, Sized]>(move (@20)) + @19 := unsize_cast[MetaSized, Sized], Rc<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized]>(move (@20)) drop[{impl Drop for Rc[@TraitClause0, @TraitClause1]}[MetaSized, Sized]] @20 storage_dead(@21) storage_dead(@20) - drop[{impl Drop for Rc[@TraitClause0, @TraitClause1]}<(dyn Display<_> + '_), Global>[MetaSized<(dyn Display<_> + '_)>, Sized]] @19 + drop[{impl Drop for Rc[@TraitClause0, @TraitClause1]}<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_), Global>[MetaSized<(dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)>, Sized]] @19 storage_dead(@19) @0 := () drop[{impl Drop for String}] string@11 From d078e2ec316f30879e877cf315f304fba136bc1b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 11 Jul 2025 14:20:27 +0200 Subject: [PATCH 5/5] ci: tell the user how we chose the commit to run --- .github/workflows/ci.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 697872ed4..926b6b6c5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -82,6 +82,7 @@ jobs: CHARON: ${{needs.select-dep-versions.outputs.charon}} AENEAS: ${{needs.select-dep-versions.outputs.aeneas}} run: | + echo 'Using the aeneas commit selected by `select-dep-versions`' nix flake update --refresh \ charon aeneas \ --override-input charon github:aeneasverif/charon/$CHARON \ @@ -99,6 +100,7 @@ jobs: CHARON: ${{needs.select-dep-versions.outputs.charon}} EURYDICE: ${{needs.select-dep-versions.outputs.eurydice}} run: | + echo 'Using the eurydice commit selected by `select-dep-versions`' nix flake update --refresh \ charon eurydice \ --override-input charon github:aeneasverif/charon/$CHARON \ @@ -117,6 +119,7 @@ jobs: EURYDICE: ${{needs.select-dep-versions.outputs.eurydice}} LIBCRUX: ${{needs.select-dep-versions.outputs.libcrux}} run: | + echo 'Using the eurydice and libcrux commits selected by `select-dep-versions`' nix flake update --refresh \ charon eurydice \ --override-input charon github:aeneasverif/charon/$CHARON \