From d976f640d0879d2de4b021be55deecaadbfffdf4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 30 Dec 2024 14:33:09 +0100 Subject: [PATCH 1/7] Clarify method call generics --- frontend/exporter/src/types/mir.rs | 116 +++++++++++++---------------- 1 file changed, 53 insertions(+), 63 deletions(-) diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index db5839bc9..cec767048 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -410,75 +410,61 @@ pub(crate) fn get_function_from_def_id_and_generics<'tcx, S: BaseState<'tcx> + H (def_id.sinto(s), generics, trait_refs, source) } -/// Get a `FunOperand` from an `Operand` used in a function call. -/// Return the [DefId] of the function referenced by an operand, with the -/// parameters substitution. -/// The [Operand] comes from a [TerminatorKind::Call]. -#[cfg(feature = "rustc")] -fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>( - s: &S, - op: &rustc_middle::mir::Operand<'tcx>, -) -> (FunOperand, Vec, Vec, Option) { - // Match on the func operand: it should be a constant as we don't support - // closures for now. - use rustc_middle::mir::Operand; - use rustc_middle::ty::TyKind; - let ty = op.ty(&s.mir().local_decls, s.base().tcx); - trace!("type: {:?}", ty); - // If the type of the value is one of the singleton types that corresponds to each function, - // that's enough information. - if let TyKind::FnDef(def_id, generics) = ty.kind() { - let (fun_id, generics, trait_refs, trait_info) = - get_function_from_def_id_and_generics(s, *def_id, *generics); - return (FunOperand::Id(fun_id), generics, trait_refs, trait_info); - } - match op { - Operand::Constant(_) => { - unimplemented!("{:?}", op); - } - Operand::Move(place) => { - // Function pointer. A fn pointer cannot have bound variables or trait references, so - // we don't need to extract generics, trait refs, etc. - let place = place.sinto(s); - (FunOperand::Move(place), Vec::new(), Vec::new(), None) - } - Operand::Copy(_place) => { - unimplemented!("{:?}", op); - } - } -} - #[cfg(feature = "rustc")] fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasOwnerId>( s: &S, terminator: &rustc_middle::mir::TerminatorKind<'tcx>, ) -> TerminatorKind { - if let rustc_middle::mir::TerminatorKind::Call { + use rustc_middle::mir::Operand; + use rustc_middle::ty::TyKind; + let rustc_middle::mir::TerminatorKind::Call { func, args, destination, target, unwind, - call_source, fn_span, + .. } = terminator - { - let (fun, generics, trait_refs, trait_info) = get_function_from_operand(s, func); + else { + unreachable!() + }; - TerminatorKind::Call { - fun, + let ty = func.ty(&s.mir().local_decls, s.base().tcx); + let fun = if let TyKind::FnDef(def_id, generics) = ty.kind() { + // The type of the value is one of the singleton types that corresponds to each function, + // which is enough information. + let (def_id, generics, trait_refs, trait_info) = + get_function_from_def_id_and_generics(s, *def_id, *generics); + FunOperand::Static { + def_id, generics, - args: args.sinto(s), - destination: destination.sinto(s), - target: target.sinto(s), - unwind: unwind.sinto(s), - call_source: call_source.sinto(s), - fn_span: fn_span.sinto(s), trait_refs, trait_info, } } else { - unreachable!() + match func { + Operand::Constant(_) => { + unimplemented!("{:?}", func); + } + Operand::Move(place) => { + // Function pointer or closure. + let place = place.sinto(s); + FunOperand::DynamicMove(place) + } + Operand::Copy(_place) => { + unimplemented!("{:?}", func); + } + } + }; + + TerminatorKind::Call { + fun, + args: args.sinto(s), + destination: destination.sinto(s), + target: target.sinto(s), + unwind: unwind.sinto(s), + fn_span: fn_span.sinto(s), } } @@ -562,13 +548,25 @@ pub enum SwitchTargets { SwitchInt(IntUintTy, Vec<(ScalarInt, BasicBlock)>, BasicBlock), } +/// A value of type `fn<...> A -> B` that can be called. #[derive_group(Serializers)] #[derive(Clone, Debug, JsonSchema)] pub enum FunOperand { - /// Call to a top-level function designated by its id - Id(DefId), - /// Use of a closure - Move(Place), + /// Call to a statically-known function. + Static { + def_id: DefId, + /// If `Some`, this is a method call on the given trait reference. Otherwise this is a call + /// to a known function. + trait_info: Option, + /// If this is a trait method call, this only includes the method generics; the trait + /// generics are included in the `ImplExpr` in `trait_info`. + generics: Vec, + /// Trait predicates required by the function generics. Like for `generics`, this only + /// includes the predicates required by the method, if applicable. + trait_refs: Vec, + }, + /// Use of a closure or a function pointer value. Counts as a move from the given place. + DynamicMove(Place), } #[derive_group(Serializers)] @@ -607,18 +605,11 @@ pub enum TerminatorKind { )] Call { fun: FunOperand, - /// We truncate the substitution so as to only include the arguments - /// relevant to the method (and not the trait) if it is a trait method - /// call. See [ParamsInfo] for the full details. - generics: Vec, args: Vec>, destination: Place, target: Option, unwind: UnwindAction, - call_source: CallSource, fn_span: Span, - trait_refs: Vec, - trait_info: Option, }, TailCall { func: Operand, @@ -1208,7 +1199,6 @@ sinto_todo!(rustc_middle::mir, UserTypeProjection); sinto_todo!(rustc_middle::mir, MirSource<'tcx>); sinto_todo!(rustc_middle::mir, CoroutineInfo<'tcx>); sinto_todo!(rustc_middle::mir, VarDebugInfo<'tcx>); -sinto_todo!(rustc_middle::mir, CallSource); sinto_todo!(rustc_middle::mir, UnwindTerminateReason); sinto_todo!(rustc_middle::mir::coverage, CoverageKind); sinto_todo!(rustc_middle::mir::interpret, ConstAllocation<'a>); From 64e1730c99f47d5e0b3a1411b3de0ef1121ea008 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 30 Dec 2024 14:52:07 +0100 Subject: [PATCH 2/7] Provide late bound generics to function calls --- frontend/exporter/src/types/mir.rs | 42 +++++++++++++++++++++++++----- 1 file changed, 36 insertions(+), 6 deletions(-) diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index cec767048..e17a018e8 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -5,6 +5,8 @@ use crate::prelude::*; use crate::sinto_as_usize; #[cfg(feature = "rustc")] +use rustc_middle::{mir, ty}; +#[cfg(feature = "rustc")] use tracing::trace; #[derive_group(Serializers)] @@ -415,9 +417,8 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO s: &S, terminator: &rustc_middle::mir::TerminatorKind<'tcx>, ) -> TerminatorKind { - use rustc_middle::mir::Operand; - use rustc_middle::ty::TyKind; - let rustc_middle::mir::TerminatorKind::Call { + let tcx = s.base().tcx; + let mir::TerminatorKind::Call { func, args, destination, @@ -430,8 +431,12 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO unreachable!() }; - let ty = func.ty(&s.mir().local_decls, s.base().tcx); - let fun = if let TyKind::FnDef(def_id, generics) = ty.kind() { + let ty = func.ty(&s.mir().local_decls, tcx); + let hax_ty: crate::Ty = ty.sinto(s); + let TyKind::Arrow(sig) = hax_ty.kind() else { + unreachable!("Attempting to call non-function type: {ty:?}") + }; + let fun_op = if let ty::TyKind::FnDef(def_id, generics) = ty.kind() { // The type of the value is one of the singleton types that corresponds to each function, // which is enough information. let (def_id, generics, trait_refs, trait_info) = @@ -443,6 +448,7 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO trait_info, } } else { + use mir::Operand; match func { Operand::Constant(_) => { unimplemented!("{:?}", func); @@ -458,8 +464,27 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO } }; + let late_bound_generics = sig + .bound_vars + .iter() + .map(|var| match var { + BoundVariableKind::Region(r) => r, + BoundVariableKind::Ty(..) => { + unreachable!("Found late-bound type variable") + } + BoundVariableKind::Const => { + unreachable!("Found late-bound const variable") + } + }) + .map(|_| { + GenericArg::Lifetime(Region { + kind: RegionKind::ReErased, + }) + }) + .collect(); TerminatorKind::Call { - fun, + fun: fun_op, + late_bound_generics, args: args.sinto(s), destination: destination.sinto(s), target: target.sinto(s), @@ -605,6 +630,11 @@ pub enum TerminatorKind { )] Call { fun: FunOperand, + /// A `FunOperand` is a value of type `fn<...> A -> B`. The generics in `<...>` are called + /// "late-bound" and are instantiated anew at each call site. This list provides the + /// generics used at this call-site. They are all lifetimes and at the time of writing are + /// all erased lifetimes. + late_bound_generics: Vec, args: Vec>, destination: Place, target: Option, From 6a71603bebf029012e7fc0d4ff334e89a867fcc5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 12 Dec 2024 11:28:31 +0100 Subject: [PATCH 3/7] Improve `ClosureArgs` for use in `AggregateKind` --- frontend/exporter/src/types/mir.rs | 22 ++------- frontend/exporter/src/types/new/full_def.rs | 6 +-- frontend/exporter/src/types/ty.rs | 52 +++++++++++++++++---- 3 files changed, 50 insertions(+), 30 deletions(-) diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index e17a018e8..3ef70894c 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -955,26 +955,12 @@ pub enum AggregateKind { Option, Option, ), - #[custom_arm(rustc_middle::mir::AggregateKind::Closure(rust_id, generics) => { - let def_id : DefId = rust_id.sinto(s); - // The generics is meant to be converted to a function signature. Note - // that Rustc does its job: the PolyFnSig binds the captured local - // type, regions, etc. variables, which means we can treat the local - // closure like any top-level function. + #[custom_arm(rustc_middle::mir::AggregateKind::Closure(def_id, generics) => { let closure = generics.as_closure(); - let sig = closure.sig().sinto(s); - - // Solve the predicates from the parent (i.e., the item which defines the closure). - let tcx = s.base().tcx; - let parent_generics = closure.parent_args(); - let parent_generics_ref = tcx.mk_args(parent_generics); - // TODO: does this handle nested closures? - let parent = tcx.generics_of(rust_id).parent.unwrap(); - let trait_refs = solve_item_required_traits(s, parent, parent_generics_ref); - - AggregateKind::Closure(def_id, parent_generics.sinto(s), trait_refs, sig) + let args = ClosureArgs::sfrom(s, *def_id, closure); + AggregateKind::Closure(def_id.sinto(s), args) })] - Closure(DefId, Vec, Vec, PolyFnSig), + Closure(DefId, ClosureArgs), Coroutine(DefId, Vec), CoroutineClosure(DefId, Vec), RawPtr(Ty, Mutability), diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index cacd983e4..2cbc427ab 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -271,10 +271,8 @@ pub enum FullDefKind { is_const: bool, #[value({ let fun_type = s.base().tcx.type_of(s.owner_id()).instantiate_identity(); - match fun_type.kind() { - ty::TyKind::Closure(_, args) => args.as_closure().sinto(s), - _ => unreachable!(), - } + let ty::TyKind::Closure(_, args) = fun_type.kind() else { unreachable!() }; + ClosureArgs::sfrom(s, s.owner_id(), args.as_closure()) })] args: ClosureArgs, }, diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index c0b12fd4d..1a52b0c10 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -1272,21 +1272,57 @@ pub enum AliasRelationDirection { } /// Reflects [`ty::ClosureArgs`] -#[derive(AdtInto)] -#[args(<'tcx, S: UnderOwnerState<'tcx> >, from: ty::ClosureArgs>, state: S as s)] -#[derive(Clone, Debug, JsonSchema)] +#[derive(Clone, Debug, Hash, PartialEq, Eq, PartialOrd, Ord, JsonSchema)] #[derive_group(Serializers)] pub struct ClosureArgs { - #[value(self.kind().sinto(s))] + /// The base kind of this closure. The kinds are ordered by inclusion: any `Fn` works as an + /// `FnMut`, and any `FnMut` works as an `FnOnce`. pub kind: ClosureKind, - #[value(self.parent_args().sinto(s))] + /// The arguments to the parent (i.e., the item which defines the closure). pub parent_args: Vec, - #[value(self.sig().sinto(s))] - pub sig: PolyFnSig, - #[value(self.upvar_tys().sinto(s))] + /// The solved predicates from the parent (i.e., the item which defines the closure). + pub parent_trait_refs: Vec, + /// The proper `fn(A, B, C) -> D` signature of the closure. + pub untupled_sig: PolyFnSig, + /// The signature of the closure as one input and one output, where the input arguments are + /// tupled. This is relevant to implementing the `Fn*` traits. + pub tupled_sig: PolyFnSig, + /// The set of captured variables. Together they form the state of the closure. pub upvar_tys: Vec, } +#[cfg(feature = "rustc")] +impl ClosureArgs { + // Manual implementation because we need the `def_id` of the closure. + pub(crate) fn sfrom<'tcx, S>( + s: &S, + def_id: RDefId, + from: ty::ClosureArgs>, + ) -> Self + where + S: UnderOwnerState<'tcx>, + { + let tcx = s.base().tcx; + let sig = from.sig(); + ClosureArgs { + kind: from.kind().sinto(s), + parent_args: from.parent_args().sinto(s), + // The solved predicates from the parent (i.e., the item which defines the closure). + parent_trait_refs: { + // TODO: handle nested closures + let parent = tcx.generics_of(def_id).parent.unwrap(); + let parent_generics_ref = tcx.mk_args(from.parent_args()); + solve_item_required_traits(s, parent, parent_generics_ref) + }, + tupled_sig: sig.sinto(s), + untupled_sig: tcx + .signature_unclosure(sig, rustc_hir::Safety::Safe) + .sinto(s), + upvar_tys: from.upvar_tys().sinto(s), + } + } +} + /// Reflects [`ty::ClosureKind`] #[derive(AdtInto)] #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::ClosureKind, state: S as _tcx)] From 4e62c29f85c34ddc426da64902a373509a0bbff4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 12 Dec 2024 11:29:02 +0100 Subject: [PATCH 4/7] Split off `TyKind::Closure` from `TyKind::Arrow` --- engine/lib/import_thir.ml | 4 ++-- frontend/exporter/src/types/mir.rs | 6 +++-- frontend/exporter/src/types/ty.rs | 18 ++++++++++----- ...oolchain__attribute-opaque into-fstar.snap | 2 +- .../toolchain__traits into-fstar.snap | 22 +++++++++---------- 5 files changed, 30 insertions(+), 22 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index cea5112ac..356b8eb07 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1004,8 +1004,8 @@ end) : EXPR = struct | Float k -> TFloat (match k with F16 -> F16 | F32 -> F32 | F64 -> F64 | F128 -> F128) - | Arrow value -> - let ({ inputs; output; _ } : Thir.ty_fn_sig) = value.value in + | Arrow signature | Closure (_, { untupled_sig = signature; _ }) -> + let ({ inputs; output; _ } : Thir.ty_fn_sig) = signature.value in let inputs = if List.is_empty inputs then [ U.unit_typ ] else List.map ~f:(c_ty span) inputs diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 3ef70894c..c05438ce2 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -433,8 +433,10 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO let ty = func.ty(&s.mir().local_decls, tcx); let hax_ty: crate::Ty = ty.sinto(s); - let TyKind::Arrow(sig) = hax_ty.kind() else { - unreachable!("Attempting to call non-function type: {ty:?}") + let sig = match hax_ty.kind() { + TyKind::Arrow(sig) => sig, + TyKind::Closure(_, args) => &args.untupled_sig, + _ => unreachable!("Attempting to call non-function type: {ty:?}"), }; let fun_op = if let ty::TyKind::FnDef(def_id, generics) = ty.kind() { // The type of the value is one of the singleton types that corresponds to each function, diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index 1a52b0c10..7c18a4521 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -802,15 +802,21 @@ pub enum TyKind { let sig = tcx.fn_sig(*def).instantiate(tcx, generics); TyKind::Arrow(Box::new(sig.sinto(s))) }, - ty::TyKind::Closure (_def_id, generics) => { - let sig = generics.as_closure().sig(); - let sig = s.base().tcx.signature_unclosure(sig, rustc_hir::Safety::Safe); - TyKind::Arrow(Box::new(sig.sinto(s))) - }, )] - /// Reflects [`ty::TyKind::FnPtr`], [`ty::TyKind::FnDef`] and [`ty::TyKind::Closure`] + /// Reflects [`ty::TyKind::FnPtr`] and [`ty::TyKind::FnDef`] Arrow(Box), + #[custom_arm( + ty::TyKind::Closure (def_id, generics) => { + let closure = generics.as_closure(); + TyKind::Closure( + def_id.sinto(s), + ClosureArgs::sfrom(s, *def_id, closure), + ) + }, + )] + Closure(DefId, ClosureArgs), + #[custom_arm( ty::TyKind::Adt(adt_def, generics) => { let def_id = adt_def.did().sinto(s); diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap index d6c17d867..6454004a7 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -110,7 +110,7 @@ val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : eqtype val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : eqtype class t_TrGeneric (v_Self: Type0) (v_U: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_6168282666194871449:Core.Clone.t_Clone v_U; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_13225137425257751668:Core.Clone.t_Clone v_U; f_f_pre:v_U -> Type0; f_f_post:v_U -> v_Self -> Type0; f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result) diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 3976241ee..aa66a93db 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -35,11 +35,11 @@ open FStar.Mul class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 } class t_ParBlocksSizeUser (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_10960599340086055385:t_BlockSizeUser v_Self + [@@@ FStar.Tactics.Typeclasses.no_method]_super_17750095326162477464:t_BlockSizeUser v_Self } class t_BlockBackend (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_15949286759387124191:t_ParBlocksSizeUser v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_7661532914804666209:t_ParBlocksSizeUser v_Self; f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0; f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0; f_proc_block:x0: Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global @@ -55,7 +55,7 @@ open FStar.Mul class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit } class t_Foo (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_5461126672499050919:t_Bar v_Self f_U; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_16210070100893052778:t_Bar v_Self f_U; f_U:Type0 } ''' @@ -387,11 +387,11 @@ let method_caller () class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_11748868061750783190:t_Trait v_Self + [@@@ FStar.Tactics.Typeclasses.no_method]_super_1779568480311729828:t_Trait v_Self v_TypeArg v_ConstArg; f_AssocType:Type0; - f_AssocType_5566993444404141271:t_Trait f_AssocType v_TypeArg v_ConstArg + f_AssocType_7414800425644916102:t_Trait f_AssocType v_TypeArg v_ConstArg } ''' "Traits.Interlaced_consts_types.fst" = ''' @@ -468,11 +468,11 @@ open FStar.Mul class t_Trait1 (v_Self: Type0) = { f_T:Type0; - f_T_7805326132379548775:t_Trait1 f_T + f_T_2328060197809802853:t_Trait1 f_T } class t_Trait2 (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_4567617955834163411:t_Trait1 v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4351024728553910126:t_Trait1 v_Self; f_U:Type0 } ''' @@ -549,7 +549,7 @@ let t_Error_cast_to_repr (x: t_Error) : isize = match x <: t_Error with | Error_ type t_Struct = | Struct : t_Struct class t_SuperTrait (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_9529721400157967266:Core.Clone.t_Clone v_Self; f_function_of_super_trait_pre:v_Self -> Type0; f_function_of_super_trait_post:v_Self -> u32 -> Type0; f_function_of_super_trait:x0: v_Self @@ -561,7 +561,7 @@ class t_SuperTrait (v_Self: Type0) = { [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_SuperTrait_for_i32: t_SuperTrait i32 = { - _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve; + _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve; f_function_of_super_trait_pre = (fun (self: i32) -> true); f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true); f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32 @@ -613,7 +613,7 @@ let use_impl_trait (_: Prims.unit) : Prims.unit = class t_Foo (v_Self: Type0) = { f_AssocType:Type0; - f_AssocType_15012754260415912210:t_SuperTrait f_AssocType; + f_AssocType_12248650268031145847:t_SuperTrait f_AssocType; f_N:usize; f_assoc_f_pre:Prims.unit -> Type0; f_assoc_f_post:Prims.unit -> Prims.unit -> Type0; @@ -650,7 +650,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x let impl_Foo_for_tuple_: t_Foo Prims.unit = { f_AssocType = i32; - f_AssocType_15012754260415912210 = FStar.Tactics.Typeclasses.solve; + f_AssocType_12248650268031145847 = FStar.Tactics.Typeclasses.solve; f_N = sz 32; f_assoc_f_pre = (fun (_: Prims.unit) -> true); f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true); From eafd5355a9b7a16d0ffff125e1090e903018e49f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 30 Dec 2024 15:57:24 +0100 Subject: [PATCH 5/7] Properly account for predicates on ADT constructors --- frontend/exporter/src/traits/utils.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/frontend/exporter/src/traits/utils.rs b/frontend/exporter/src/traits/utils.rs index cc06e573e..202915236 100644 --- a/frontend/exporter/src/traits/utils.rs +++ b/frontend/exporter/src/traits/utils.rs @@ -76,6 +76,9 @@ pub fn required_predicates<'tcx>( .iter() .map(|(clause, _span)| *clause), ), + // The tuple struct/variant constructor functions inherit the generics and predicates from + // their parents. + Variant | Ctor(..) => return required_predicates(tcx, tcx.parent(def_id)), // We consider all predicates on traits to be outputs Trait => None, // `predicates_defined_on` ICEs on other def kinds. From 79e2da0452a0b94056becba46b98304ca230a502 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 31 Dec 2024 11:58:38 +0100 Subject: [PATCH 6/7] Discard more-precise implemented method signatures --- frontend/exporter/src/types/new/full_def.rs | 66 ++++++++++++++++++++- 1 file changed, 65 insertions(+), 1 deletion(-) diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index 2cbc427ab..4473fa76c 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -252,7 +252,7 @@ pub enum FullDefKind { inline: InlineAttr, #[value(s.base().tcx.constness(s.owner_id()) == rustc_hir::Constness::Const)] is_const: bool, - #[value(s.base().tcx.fn_sig(s.owner_id()).instantiate_identity().sinto(s))] + #[value(get_method_sig(s).sinto(s))] sig: PolyFnSig, #[value(s.owner_id().as_local().map(|ldid| Body::body(ldid, s)))] body: Option, @@ -767,6 +767,70 @@ where } } +/// The signature of a method impl may be a subtype of the one expected from the trait decl, as in +/// the example below. For correctness, we must be able to map from the method generics declared in +/// the trait to the actual method generics. Because this would require type inference, we instead +/// simply return the declared signature. This will cause issues if it is possible to use such a +/// more-specific implementation with its more-specific type, but we have a few other issues with +/// lifetime-generic function pointers anyway so this is unlikely to cause problems. +/// +/// ```ignore +/// trait MyCompare: Sized { +/// fn compare(self, other: Other) -> bool; +/// } +/// impl<'a> MyCompare<&'a ()> for &'a () { +/// // This implementation is more general because it works for non-`'a` refs. Note that only +/// // late-bound vars may differ in this way. +/// // `<&'a () as MyCompare<&'a ()>>::compare` has type `fn<'b>(&'a (), &'b ()) -> bool`, +/// // but type `fn(&'a (), &'a ()) -> bool` was expected from the trait declaration. +/// fn compare<'b>(self, _other: &'b ()) -> bool { +/// true +/// } +/// } +/// ``` +#[cfg(feature = "rustc")] +fn get_method_sig<'tcx, S>(s: &S) -> ty::PolyFnSig<'tcx> +where + S: UnderOwnerState<'tcx>, +{ + let tcx = s.base().tcx; + let def_id = s.owner_id(); + let real_sig = tcx.fn_sig(def_id).instantiate_identity(); + let item = tcx.associated_item(def_id); + if !matches!(item.container, ty::AssocItemContainer::ImplContainer) { + return real_sig; + } + let Some(decl_method_id) = item.trait_item_def_id else { + return real_sig; + }; + let declared_sig = tcx.fn_sig(decl_method_id); + + // TODO(Nadrieril): Temporary hack: if the signatures have the same number of bound vars, we + // keep the real signature. While the declared signature is more correct, it is also less + // normalized and we can't normalize without erasing regions but regions are crucial in + // function signatures. Hence we cheat here, until charon gains proper normalization + // capabilities. + if declared_sig.skip_binder().bound_vars().len() == real_sig.bound_vars().len() { + return real_sig; + } + + let impl_def_id = item.container_id(tcx); + // The trait predicate that is implemented by the surrounding impl block. + let implemented_trait_ref = tcx + .impl_trait_ref(impl_def_id) + .unwrap() + .instantiate_identity(); + // Construct arguments for the declared method generics in the context of the implemented + // method generics. + let impl_args = ty::GenericArgs::identity_for_item(tcx, def_id); + let decl_args = impl_args.rebase_onto(tcx, impl_def_id, implemented_trait_ref.args); + let sig = declared_sig.instantiate(tcx, decl_args); + // Avoids accidentally using the same lifetime name twice in the same scope + // (once in impl parameters, second in the method declaration late-bound vars). + let sig = tcx.anonymize_bound_vars(sig); + sig +} + #[cfg(feature = "rustc")] fn get_ctor_contents<'tcx, S, Body>(s: &S, ctor_of: CtorOf) -> FullDefKind where From 63422f3fc0033b79a84aeb4dd0f60d43a853d42f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Jan 2025 16:04:53 +0100 Subject: [PATCH 7/7] Use `supposely_unreachable!` to get better errors --- frontend/exporter/src/types/mir.rs | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index c05438ce2..ffc2535c2 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -436,7 +436,11 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO let sig = match hax_ty.kind() { TyKind::Arrow(sig) => sig, TyKind::Closure(_, args) => &args.untupled_sig, - _ => unreachable!("Attempting to call non-function type: {ty:?}"), + _ => supposely_unreachable_fatal!( + s, + "TerminatorKind_Call_expected_fn_type"; + { ty } + ), }; let fun_op = if let ty::TyKind::FnDef(def_id, generics) = ty.kind() { // The type of the value is one of the singleton types that corresponds to each function, @@ -471,11 +475,12 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO .iter() .map(|var| match var { BoundVariableKind::Region(r) => r, - BoundVariableKind::Ty(..) => { - unreachable!("Found late-bound type variable") - } - BoundVariableKind::Const => { - unreachable!("Found late-bound const variable") + BoundVariableKind::Ty(..) | BoundVariableKind::Const => { + supposely_unreachable_fatal!( + s, + "non_lifetime_late_bound"; + { var } + ) } }) .map(|_| {