From 994b9c099ce91bb75e03593ddf05613f59e0ea17 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 23 Sep 2024 08:13:48 +0200 Subject: [PATCH] fix(engine/fstar): fix super typeclasses attributes The PR #902 was reverted by #909 because #902 was generated redundant fields names in classes for super clauses, which is a problem for F*. This PR changes the naming scheme of super clauses for typeclasses in F*. Those names now take into account the trait name. The super trait names are now a 5 characters base 62 encoding of the hash of the predicate ID concatenated with the trait name. Fixes #630. --- engine/backends/fstar/fstar_ast.ml | 1 + engine/backends/fstar/fstar_backend.ml | 30 +++++++--- engine/lib/utils.ml | 17 ++++++ .../toolchain__traits into-fstar.snap | 56 ++++++++++++++----- tests/traits/src/lib.rs | 9 +++ 5 files changed, 92 insertions(+), 21 deletions(-) diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml index 0ead59bd5..5c0120883 100644 --- a/engine/backends/fstar/fstar_ast.ml +++ b/engine/backends/fstar/fstar_ast.ml @@ -32,6 +32,7 @@ let pat (pat : AST.pattern') = AST.{ pat; prange = dummyRange } module Attrs = struct let no_method = term @@ AST.Var FStar_Parser_Const.no_method_lid + let tcinstance = term @@ AST.Var FStar_Parser_Const.tcinstance_lid end let tcresolve = term @@ AST.Var FStar_Parser_Const.tcresolve_lid diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 6430fc633..350178d52 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -339,6 +339,12 @@ struct in F.mk_e_abs [ pat ] (F.mk_e_app trait args) + and name_of_super_clause (trait_goal : trait_goal) (base_name : string) = + String.hash + (U.Concrete_ident_view.to_definition_name trait_goal.trait + ^ "*" ^ base_name) + |> base62_of_int 5 |> ( ^ ) "_super_" + and pimpl_expr span (ie : impl_expr) = let some = Option.some in let hax_unstable_impl_exprs = false in @@ -353,7 +359,7 @@ struct pimpl_expr span impl | Parent { impl; ident } when hax_unstable_impl_exprs -> let* impl = pimpl_expr span impl in - let trait = "_super_" ^ ident.name in + let trait = name_of_super_clause ident.goal ident.name in F.term @@ F.AST.Project (impl, F.lid [ trait ]) |> some | ImplApp { impl; args = [] } when hax_unstable_impl_exprs -> pimpl_expr span impl @@ -1158,7 +1164,7 @@ struct :: List.map ~f: (fun { - goal = { trait; args }; + goal = { trait; args } as goal; name = impl_ident_name; } -> let base = @@ -1167,10 +1173,11 @@ struct let args = List.map ~f:(pgeneric_value e.span) args in - ( F.id (name ^ "_" ^ impl_ident_name), + ( F.id + (name ^ name_of_super_clause goal impl_ident_name), (* Dodgy concatenation *) None, - [], + [ F.Attrs.tcinstance ], F.mk_e_app base args )) bounds | TIFn ty @@ -1363,9 +1370,9 @@ struct |> List.filter_map ~f:(fun c -> match c with | GCType { goal = bound; name = id } -> - let name = "_super_" ^ id in + let name = name_of_super_clause bound id in let typ = pgeneric_constraint_type e.span c in - Some (F.id name, None, [ F.Attrs.no_method ], typ) + Some (F.id name, None, [ F.Attrs.tcinstance ], typ) | GCProjection _ -> (* TODO: Not yet implemented, see https://github.com/hacspec/hax/issues/785 *) None @@ -1436,14 +1443,21 @@ struct (F.lid [ name ], pty ii_span typ) :: List.map ~f:(fun (_impl_expr, impl_ident) -> - (F.lid [ name ^ "_" ^ impl_ident.name ], F.tc_solve)) + ( F.lid + [ + name + ^ name_of_super_clause impl_ident.goal + impl_ident.name; + ], + F.tc_solve )) parent_bounds) items in let parent_bounds_fields = List.map ~f:(fun (_impl_expr, impl_ident) -> - (F.lid [ "_super_" ^ impl_ident.name ], F.tc_solve)) + ( F.lid [ name_of_super_clause impl_ident.goal impl_ident.name ], + F.tc_solve )) parent_bounds in let fields = parent_bounds_fields @ fields in diff --git a/engine/lib/utils.ml b/engine/lib/utils.ml index 2c95d2f88..db433c35d 100644 --- a/engine/lib/utils.ml +++ b/engine/lib/utils.ml @@ -108,6 +108,23 @@ include ( (** Generates a temporary file path that ends with `suffix` *) end) +(** Formats an integer as base 62 *) +let base62_of_int len : int -> string = + let alphabet = + "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz" + in + let max = String.length alphabet in + fun n -> + let n = ref n in + let f _i = + let i = !n % max in + n := !n / max; + String.get alphabet i + in + let arr = Array.init len ~f in + Array.rev_inplace arr; + String.of_array arr + module List = struct include Base.List diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 75062d160..5dd64aedc 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.tcinstance]_super_U5QdG:t_BlockSizeUser v_Self } class t_BlockBackend (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_15949286759387124191:t_ParBlocksSizeUser v_Self; + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_sNdEU: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 @@ -329,11 +329,11 @@ let impl (#v_TypeArg: Type0) (v_ConstArg: usize) : t_Trait Prims.unit v_TypeArg } class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_8779313392680198588:t_Trait v_Self - v_TypeArg - v_ConstArg; + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_cyxbI:t_Trait v_Self v_TypeArg v_ConstArg; f_AssocType:Type0; - f_AssocType_6369404467997533198:t_Trait f_AssocType v_TypeArg v_ConstArg + [@@@ FStar.Tactics.Typeclasses.tcinstance]f_AssocType_super_6oYyd:t_Trait f_AssocType + v_TypeArg + v_ConstArg } let associated_function_caller @@ -454,14 +454,44 @@ open FStar.Mul class t_Trait1 (v_Self: Type0) = { f_T:Type0; - f_T_1640036513185240095:t_Trait1 f_T + [@@@ FStar.Tactics.Typeclasses.tcinstance]f_T_super_OOsUn:t_Trait1 f_T } class t_Trait2 (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_4567617955834163411:t_Trait1 v_Self; + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_ev6bP:t_Trait1 v_Self; f_U:Type0 } ''' +"Traits.Super_clauses_names.fst" = ''' +module Traits.Super_clauses_names +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +class t_A (v_Self: Type0) = { __marker_trait_t_A:Prims.unit } + +class t_B (v_Self: Type0) = { __marker_trait_t_B:Prims.unit } + +class t_C (v_Self: Type0) = { __marker_trait_t_C:Prims.unit } + +class t_ChildTrait1 (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_9FQrt:t_A v_Self; + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_sXIun:t_B v_Self; + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_C3uwc:t_C v_Self +} + +class t_ChildTrait2 (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_9FQrt:t_A v_Self; + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_sXIun:t_B v_Self; + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_C3uwc:t_C v_Self +} + +class t_ChildTrait3 (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_9FQrt:t_A v_Self; + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_sXIun:t_B v_Self; + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_C3uwc:t_C v_Self +} +''' "Traits.Type_alias_bounds_issue_707_.fst" = ''' module Traits.Type_alias_bounds_issue_707_ #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -541,7 +571,7 @@ class t_Lang (v_Self: Type0) = { } class t_SuperTrait (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self; + [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_ex7xP: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 @@ -553,7 +583,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_ex7xP = 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 @@ -561,8 +591,8 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 = class t_Foo (v_Self: Type0) = { f_AssocType:Type0; - f_AssocType_15525962639250476383:t_SuperTrait f_AssocType; - f_AssocType_17265963849229885182:Core.Clone.t_Clone f_AssocType; + [@@@ FStar.Tactics.Typeclasses.tcinstance]f_AssocType_super_SntST:t_SuperTrait f_AssocType; + [@@@ FStar.Tactics.Typeclasses.tcinstance]f_AssocType_super_LqPiP:Core.Clone.t_Clone f_AssocType; f_N:usize; f_assoc_f_pre:Prims.unit -> Type0; f_assoc_f_post:Prims.unit -> Prims.unit -> Type0; @@ -621,7 +651,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_15525962639250476383 = FStar.Tactics.Typeclasses.solve; + f_AssocType_super_SntST = 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); diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs index e8968be87..b01c838a4 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -276,3 +276,12 @@ mod recursive_trait_with_assoc_type { type U; } } + +mod super_clauses_names { + trait A {} + trait B {} + trait C {} + trait ChildTrait1: A + B + C {} + trait ChildTrait2: A + B + C {} + trait ChildTrait3: A + B + C {} +}