From 5b377f4f99ddbeb6ff0f97cfb45cb1740e59a8e3 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Fri, 5 Sep 2025 15:12:49 +0800 Subject: [PATCH 01/20] first petch to eliminate [core::option] --- Makefile | 2 +- bin/main.ml | 1 + lib/Cleanup2.ml | 35 +++++++++++++++++++++++++++++++++++ 3 files changed, 37 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 20633c80..d1915807 100644 --- a/Makefile +++ b/Makefile @@ -50,7 +50,7 @@ clean-and-test: .PRECIOUS: %.llbc %.llbc: %.rs .charon_version # --mir elaborated --add-drop-bounds - $(CHARON) rustc --preset=eurydice --dest-file "$@" $(CHARON_EXTRA) -- $< + $(CHARON) rustc --monomorphize --preset=eurydice --dest-file "$@" $(CHARON_EXTRA) -- $< out/test-%/main.c: test/main.c mkdir -p out/test-$* diff --git a/bin/main.ml b/bin/main.ml index 5d8dd78c..a858ccf1 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -235,6 +235,7 @@ Supported options:|} that they were empty structs to begin with, which would send Checker off the rails *) let files = Krml.DataTypes.remove_empty_structs files in let files = Krml.Monomorphization.datatypes files in + let files = Eurydice.Cleanup2.drop_unused_type files in (* Cannot use remove_unit_buffers as it is technically incorrect *) let files = Krml.DataTypes.remove_unit_fields#visit_files () files in Eurydice.Logging.log "Phase2.13" "%a" pfiles files; diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 1cc5c5ac..90bd5605 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -1367,3 +1367,38 @@ let remove_discriminant_reads (map : Krml.DataTypes.map) files = end) #visit_files () files + +(* Remove the unused DType declarations *) +let drop_unused_type files = + let open Krml in + let seen = Hashtbl.create 41 in + + let body_of_lid = Helpers.build_map files (fun map d -> Hashtbl.add map (lid_of_decl d) d) in + + let visitor = object (self) + inherit [_] iter as super + method! visit_EQualified (before, _) lid = + self#discover before lid + method! visit_TQualified before lid = + self#discover before lid + method! visit_TApp before lid ts = + self#discover before lid; + List.iter (self#visit_typ before) ts + method private discover before lid = + if not (Hashtbl.mem seen lid) then begin + Hashtbl.add seen lid (); + if Options.debug "reachability" then + KPrint.bprintf "REACHABILITY: %a is used (via: %s) \n" plid lid + (String.concat " <- " (List.map (fun lid -> KPrint.bsprintf "%a" plid lid) before)); + + if Hashtbl.mem body_of_lid lid then + ignore (super#visit_decl (lid :: before) (Hashtbl.find body_of_lid lid)); + end + end in + visitor#visit_files [] files; + filter_decls (fun d -> + match d with + | DType (lid, _flags, _, _, _) -> + if (Hashtbl.mem seen lid) then Some d else None + | _ -> Some d + ) files From bd8a1fc102d3ca848252c9a621defdfa3ec818d6 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Wed, 10 Sep 2025 16:52:18 +0800 Subject: [PATCH 02/20] added hash table for re-polymorphize --- lib/AstOfLlbc.ml | 43 +++++++++++++++++++++++++++++++++++-------- 1 file changed, 35 insertions(+), 8 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 6892c129..65726985 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -279,9 +279,8 @@ let string_of_fn_ptr env fn_ptr = string_of_pattern (pattern_of_fn_ptr env fn_pt (** Translation of types *) -let lid_of_name (env : env) (name : Charon.Types.name) : K.lident = - let prefix, name = Krml.KList.split_at_last name in - List.map (string_of_path_elem env) prefix, string_of_path_elem env name +(* let lid_full_generic = Hashtbl.create 41*) + let width_of_integer_type (t : Charon.Types.integer_type) : K.width = match t with @@ -300,10 +299,6 @@ let width_of_integer_type (t : Charon.Types.integer_type) : K.width = | Unsigned U128 -> failwith "Internal error: `u128` should not be handled in `width_of_integer_type`." -let lid_of_type_decl_id (env : env) (id : C.type_decl_id) = - let { C.item_meta; _ } = env.get_nth_type id in - lid_of_name env item_meta.name - let constant_of_scalar_value sv = let w = width_of_integer_type (Charon.Scalars.get_ty sv) in w, Z.to_string (Charon.Scalars.get_val sv) @@ -383,7 +378,39 @@ let lookup_field env typ_id field_id = let field = List.nth fields i in ensure_named i field.field_name -let rec pre_typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ = + +(* name:: -> (name, [N], [A, B, C]) *) +let lid_full_generic = Hashtbl.create 41 + +let pure_lid_of_name (env : env) (name : Charon.Types.name) : K.lident = + let prefix, name = Krml.KList.split_at_last name in + List.map (string_of_path_elem env) prefix, string_of_path_elem env name + +let rec insert_lid_full_generic (env : env) (full_name : K.lident) (name : Charon.Types.name) = + let (item_name, generic) = + let (pre, last) = Krml.KList.split_at_last name in + match last with + | PeMonomorphized args -> pure_lid_of_name env pre, (args : C.generic_args) + | _ -> full_name, { C.types = []; regions = []; const_generics = []; trait_refs = [] } + in + let (cgs, tys) = + ( List.map (cg_of_const_generic env) generic.const_generics, + List.map (typ_of_ty env) generic.types ) + in + if not (Hashtbl.mem lid_full_generic full_name) then + L.log "AstOfLlbc" "mono name : %a\n repolyed name : %a with cgs %a and tys %a " + plid full_name plid item_name pcgs cgs ptyps tys; + Hashtbl.add lid_full_generic full_name (item_name, cgs, tys) + +and lid_of_name (env : env) (name : Charon.Types.name) : K.lident = + let lid = pure_lid_of_name env name in + insert_lid_full_generic env lid name; + lid + +and lid_of_type_decl_id (env : env) (id : C.type_decl_id) = + let { C.item_meta; _ } = env.get_nth_type id in + lid_of_name env item_meta.name +and pre_typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ = match ty with | TVar var -> K.TBound (lookup_typ env (C.expect_free_var var)) | TLiteral t -> typ_of_literal_ty env t From 9bbdcb68a3b44b3e1254af758747921c6888763d Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Wed, 10 Sep 2025 17:35:36 +0800 Subject: [PATCH 03/20] wip: trying to match the lid using hash table --- lib/AstOfLlbc.ml | 248 +++++++++++++++++++++++++++------------------- lib/PreCleanup.ml | 29 ++++-- 2 files changed, 162 insertions(+), 115 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 65726985..ebb89c6e 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -377,11 +377,153 @@ let lookup_field env typ_id field_id = let i = C.FieldId.to_int field_id in let field = List.nth fields i in ensure_named i field.field_name +let is_var v2 v1 = + match v2 with + | Var (v2, _) -> v2 = v1 + | _ -> false + +let assert_var = function + | Var (v2, ty) -> v2, ty + | _ -> assert false + +let assert_trait_clause_method = function + | TraitClauseMethod { clause_id; item_name; ts; _ } -> clause_id, item_name, ts + | _ -> assert false + +(* Regular binders *) + +let lookup_with_original_type env v1 = + let i, (v, t) = findi (fun (v2, _) -> is_var v2 v1) env.binders in + let _, ty = assert_var v in + i, t, ty + + let lookup env v1 = + let i, (_, t) = findi (fun (v2, _) -> is_var v2 v1) env.binders in + i, t + + let lookup_cg_in_expressions (env : env) (v1 : C.const_generic_var_id) = + let i, (_, t) = findi (fun (v2, _) -> v2 = ConstGenericVar v1) env.binders in + i, t + + let expression_of_cg_var_id env v = + let i, t = lookup_cg_in_expressions env v in + K.(with_type t (EBound i)) +let expression_of_var_id (env : env) (v : C.local_id) : K.expr = + let i, t = lookup env v in + K.(with_type t (EBound i)) + + (** Assume here the maximum length is 128-bit -- will throw away the larger if larger. This is a + helper function to split a 128-bit integer into two 64-bit integers and is not assumed to be + used in other contexts. Returns the **expr** pair (high64bits, low64bits) *) +let split_128bit (value : Z.t) = + let mask128 = Z.sub (Z.shift_left Z.one 128) Z.one in + let mask64 = Z.sub (Z.shift_left Z.one 64) Z.one in + (* Always truncate to 128 bits using bitwise AND *) + let value = Z.logand value mask128 in + (* Extract low 64 bits *) + let low64 = Z.logand mask64 value in + (* Shift right without sign extension (use logical shift) *) + let high64 = Z.shift_right value 64 in + let to_expr_u64bits v = + let print_Z z = Z.format "%#x" z in + K.with_type (K.TInt UInt64) @@ K.EConstant (UInt64, print_Z v) + in + to_expr_u64bits high64, to_expr_u64bits low64 + +let expression_of_int128_t (value : Z.t) = + let i128_max = Z.sub (Z.shift_left Z.one 127) Z.one in + if value > i128_max then + failwith "value is larger than the maximum value of i128"; + let i128_min = Z.neg (Z.shift_left Z.one 127) in + if value < i128_min then + failwith "value is smaller than the minimum value of i128"; + let high64, low64 = split_128bit value in + K.(with_type Builtin.int128_t (EApp (Builtin.(get_128_op ("i", "from_bits")), [ high64; low64 ]))) + +let expression_of_uint128_t (value : Z.t) = + let u128_max = Z.sub (Z.shift_left Z.one 128) Z.one in + if value > u128_max then + failwith "value is larger than the maximum value of u128"; + let high64, low64 = split_128bit value in + K.( + with_type Builtin.uint128_t (EApp (Builtin.(get_128_op ("u", "from_bits")), [ high64; low64 ]))) + + +let expression_of_scalar_value sv : K.expr = + let int_ty = Charon.Scalars.get_ty sv in + let value = Charon.Scalars.get_val sv in + match int_ty with + | C.Signed C.I128 -> expression_of_int128_t value + | C.Unsigned C.U128 -> expression_of_uint128_t value + | _ -> + let w = width_of_integer_type int_ty in + K.(with_type (TInt w) (EConstant (constant_of_scalar_value sv))) + +let expression_of_literal (_env : env) (l : C.literal) : K.expr = + match l with + | VScalar sv -> expression_of_scalar_value sv + | VBool b -> K.(with_type TBool (EBool b)) + | VStr s -> + let ascii = Utf8.ascii_of_utf8_str s in + let len = String.length s in + K.( + with_type Builtin.str_t + (EFlat + [ + Some "data", with_type Krml.Checker.c_string (EString ascii); + Some "len", with_type Krml.Helpers.usize (EConstant (SizeT, string_of_int len)); + ])) + | VChar c -> K.(with_type Builtin.char_t (EConstant (UInt32, string_of_int @@ Uchar.to_int c))) + | VByteStr lst -> + let str = List.map (Printf.sprintf "%#x") lst |> String.concat "" in + K.(with_type Krml.Checker.c_string (EString str)) + | VFloat { C.float_ty; float_value } -> + let w = float_width float_ty in + K.(with_type (TInt w) (EConstant (w, float_value))) + + let expression_of_const_generic env cg = + match cg with + | C.CgGlobal _ -> failwith "TODO: CgGLobal" + | C.CgVar var -> expression_of_cg_var_id env (C.expect_free_var var) + | C.CgValue l -> expression_of_literal env l (* name:: -> (name, [N], [A, B, C]) *) let lid_full_generic = Hashtbl.create 41 +(* Given the result type, const generics, and type arguments, return the original type such that + After applying the const generics and type arguments, we get the result type. +*) +let ty_re_polymorphize res_ty cgs ty_args = + let n_cgs = List.length cgs in + let n = List.length ty_args in + if n = 0 && n_cgs = 0 then + res_ty + else + match res_ty with + | K.TPoly (ts, t) -> + (* If already polymorphic, conservatively widen the scheme by + prepending new binders. This is a best–effort reconstruction. *) + K.TPoly ({ K.n = ts.n + n; n_cgs = ts.n_cgs + n_cgs }, t) + | _ -> + K.TPoly ({ K.n = n; n_cgs = n_cgs }, res_ty) + +(* From monomorphized codes `name::` to the original generic expression. + Work by turning the `EQualified` into `ETApp` with the appropriate type + Or, if no generics, leave as is. +*) +let re_polymorphize expr = object + inherit [_] Krml.Ast.map + method! visit_EQualified ((), ty) full_name = + try + let name, cgs, ts = Hashtbl.find lid_full_generic full_name in + if cgs = [] && ts = [] then + EQualified full_name + else + ETApp (K.with_type (ty_re_polymorphize ty cgs ts) (K.EQualified name), cgs, [], ts) + with Not_found -> EQualified full_name + end#visit_expr_w () expr + let pure_lid_of_name (env : env) (name : Charon.Types.name) : K.lident = let prefix, name = Krml.KList.split_at_last name in List.map (string_of_path_elem env) prefix, string_of_path_elem env name @@ -394,12 +536,12 @@ let rec insert_lid_full_generic (env : env) (full_name : K.lident) (name : Charo | _ -> full_name, { C.types = []; regions = []; const_generics = []; trait_refs = [] } in let (cgs, tys) = - ( List.map (cg_of_const_generic env) generic.const_generics, + ( List.map (expression_of_const_generic env) generic.const_generics, List.map (typ_of_ty env) generic.types ) in if not (Hashtbl.mem lid_full_generic full_name) then L.log "AstOfLlbc" "mono name : %a\n repolyed name : %a with cgs %a and tys %a " - plid full_name plid item_name pcgs cgs ptyps tys; + plid full_name plid item_name pexprs cgs ptyps tys; Hashtbl.add lid_full_generic full_name (item_name, cgs, tys) and lid_of_name (env : env) (name : Charon.Types.name) : K.lident = @@ -527,30 +669,6 @@ let mk_deep_copy (e : K.expr) (l : K.expr) = (* Environment: expressions *) -let is_var v2 v1 = - match v2 with - | Var (v2, _) -> v2 = v1 - | _ -> false - -let assert_var = function - | Var (v2, ty) -> v2, ty - | _ -> assert false - -let assert_trait_clause_method = function - | TraitClauseMethod { clause_id; item_name; ts; _ } -> clause_id, item_name, ts - | _ -> assert false - -(* Regular binders *) - -let lookup env v1 = - let i, (_, t) = findi (fun (v2, _) -> is_var v2 v1) env.binders in - i, t - -let lookup_with_original_type env v1 = - let i, (v, t) = findi (fun (v2, _) -> is_var v2 v1) env.binders in - let _, ty = assert_var v in - i, t, ty - (* Const generic binders *) let push_cg_binder env (t : C.const_generic_var) = @@ -628,91 +746,13 @@ let rec with_locals (env : env) (t : K.typ) (locals : C.local list) (k : env -> let b = binder_of_var env l in K.(with_type t (ELet (b, Krml.Helpers.any, with_locals env t locals k))) -let lookup_cg_in_expressions (env : env) (v1 : C.const_generic_var_id) = - let i, (_, t) = findi (fun (v2, _) -> v2 = ConstGenericVar v1) env.binders in - i, t -let expression_of_cg_var_id env v = - let i, t = lookup_cg_in_expressions env v in - K.(with_type t (EBound i)) -let expression_of_var_id (env : env) (v : C.local_id) : K.expr = - let i, t = lookup env v in - K.(with_type t (EBound i)) - -(** Assume here the maximum length is 128-bit -- will throw away the larger if larger. This is a - helper function to split a 128-bit integer into two 64-bit integers and is not assumed to be - used in other contexts. Returns the **expr** pair (high64bits, low64bits) *) -let split_128bit (value : Z.t) = - let mask128 = Z.sub (Z.shift_left Z.one 128) Z.one in - let mask64 = Z.sub (Z.shift_left Z.one 64) Z.one in - (* Always truncate to 128 bits using bitwise AND *) - let value = Z.logand value mask128 in - (* Extract low 64 bits *) - let low64 = Z.logand mask64 value in - (* Shift right without sign extension (use logical shift) *) - let high64 = Z.shift_right value 64 in - let to_expr_u64bits v = - let print_Z z = Z.format "%#x" z in - K.with_type (K.TInt UInt64) @@ K.EConstant (UInt64, print_Z v) - in - to_expr_u64bits high64, to_expr_u64bits low64 -let expression_of_int128_t (value : Z.t) = - let i128_max = Z.sub (Z.shift_left Z.one 127) Z.one in - if value > i128_max then - failwith "value is larger than the maximum value of i128"; - let i128_min = Z.neg (Z.shift_left Z.one 127) in - if value < i128_min then - failwith "value is smaller than the minimum value of i128"; - let high64, low64 = split_128bit value in - K.(with_type Builtin.int128_t (EApp (Builtin.(get_128_op ("i", "from_bits")), [ high64; low64 ]))) -let expression_of_uint128_t (value : Z.t) = - let u128_max = Z.sub (Z.shift_left Z.one 128) Z.one in - if value > u128_max then - failwith "value is larger than the maximum value of u128"; - let high64, low64 = split_128bit value in - K.( - with_type Builtin.uint128_t (EApp (Builtin.(get_128_op ("u", "from_bits")), [ high64; low64 ]))) -let expression_of_scalar_value sv : K.expr = - let int_ty = Charon.Scalars.get_ty sv in - let value = Charon.Scalars.get_val sv in - match int_ty with - | C.Signed C.I128 -> expression_of_int128_t value - | C.Unsigned C.U128 -> expression_of_uint128_t value - | _ -> - let w = width_of_integer_type int_ty in - K.(with_type (TInt w) (EConstant (constant_of_scalar_value sv))) -let expression_of_literal (_env : env) (l : C.literal) : K.expr = - match l with - | VScalar sv -> expression_of_scalar_value sv - | VBool b -> K.(with_type TBool (EBool b)) - | VStr s -> - let ascii = Utf8.ascii_of_utf8_str s in - let len = String.length s in - K.( - with_type Builtin.str_t - (EFlat - [ - Some "data", with_type Krml.Checker.c_string (EString ascii); - Some "len", with_type Krml.Helpers.usize (EConstant (SizeT, string_of_int len)); - ])) - | VChar c -> K.(with_type Builtin.char_t (EConstant (UInt32, string_of_int @@ Uchar.to_int c))) - | VByteStr lst -> - let str = List.map (Printf.sprintf "%#x") lst |> String.concat "" in - K.(with_type Krml.Checker.c_string (EString str)) - | VFloat { C.float_ty; float_value } -> - let w = float_width float_ty in - K.(with_type (TInt w) (EConstant (w, float_value))) -let expression_of_const_generic env cg = - match cg with - | C.CgGlobal _ -> failwith "TODO: CgGLobal" - | C.CgVar var -> expression_of_cg_var_id env (C.expect_free_var var) - | C.CgValue l -> expression_of_literal env l let rec expression_of_place (env : env) (p : C.place) : K.expr = (* We construct a target expression. Callers may still use the original type to tell arrays diff --git a/lib/PreCleanup.ml b/lib/PreCleanup.ml index 335b3904..8256cae7 100644 --- a/lib/PreCleanup.ml +++ b/lib/PreCleanup.ml @@ -40,7 +40,7 @@ let remove_array_eq = object inherit Krml.DeBruijn.map_counting_cg as super method! visit_expr ((n_cgs, n_binders) as env, _) e = - match e with + match AstOfLlbc.re_polymorphize e with | [%cremepat {| core::array::equality::?impl::eq[#?n](#?..)(?a1, ?a2) |}] -> let rec is_flat = function | TArray (t, _) -> is_flat t @@ -50,21 +50,28 @@ let remove_array_eq = object assert (t = u); if is_flat t then let diff = n_binders - n_cgs in - match impl with - | "{core::cmp::PartialEq<@Array> for @Array}" -> - with_type TBool (EApp ( + let pattern = Str.regexp {|{core::cmp::PartialEq<@Array<\([a-zA-Z_][a-zA-Z0-9_]*\), \([a-zA-Z_][a-zA-Z0-9_]*\)>> for @Array<\([a-zA-Z_][a-zA-Z0-9_]*\), \([a-zA-Z_][a-zA-Z0-9_]*\)>}|} in + let matches_eq_array s = + try + if Str.string_match pattern s 0 then true + else + false + with Not_found -> false in + let matches_eq_slice = Str.regexp {|{core::cmp::PartialEq<&.* \(@Slice<\([a-zA-Z_][a-zA-Z0-9_]*\)>\)> for @Array<\([a-zA-Z_][a-zA-Z0-9_]*\), \([a-zA-Z_][a-zA-Z0-9_]*\)>}|} in + let matches_eq_slice s = Str.string_match matches_eq_slice s 0 in + if matches_eq_array impl then with_type TBool (EApp ( Builtin.(expr_of_builtin_t ~cgs:(diff, [n]) array_eq [ t ]), [ a1; a2 ])) - | "{core::cmp::PartialEq<&0 (@Slice)> for @Array}" -> - with_type TBool (EApp ( + else if matches_eq_slice impl then with_type TBool (EApp ( Builtin.(expr_of_builtin_t ~cgs:(diff, [n]) array_eq_slice [ t ]), [ a1; a2 ])) - | _ -> - failwith ("unknown array eq impl: " ^ impl) - else - failwith "TODO: non-byteeq array comparison" - | _ -> super#visit_expr (env, e.typ) e + else failwith ("unknown array eq impl: " ^ impl) + else failwith "TODO: non-byteeq array comparison" + + + + | _ -> super#visit_expr (env, e.typ) e method! visit_DFunction _ cc flags n_cgs n t lid bs e = super#visit_DFunction (n_cgs, 0) cc flags n_cgs n t lid bs e end From 15684eb87b7aacc65e40628c1c3aceeafb15f65e Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Thu, 11 Sep 2025 10:03:51 +0800 Subject: [PATCH 04/20] wip: passed array2d --- Makefile | 10 +++++----- lib/PreCleanup.ml | 5 ++++- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/Makefile b/Makefile index d1915807..8b6a87d3 100644 --- a/Makefile +++ b/Makefile @@ -8,9 +8,9 @@ TEST_DIRS = $(filter-out $(BROKEN_TESTS),$(basename $(notdir $(wildcard test/*. # Warn on old versions of bash _ := $(shell bash -c '(( $${BASH_VERSION%%.*} >= 4 ))') -ifneq ($(.SHELLSTATUS),0) -_: $(error "bash version is too old; hint: brew install bash") -endif +#ifneq ($(.SHELLSTATUS),0) +#_: $(error "bash version is too old; hint: brew install bash") +#endif # Enable `foo/**` glob syntax SHELL := bash -O globstar @@ -41,7 +41,7 @@ build: CFLAGS := -Wall -Werror -Wno-unused-variable $(CFLAGS) -I$(KRML_HOME)/include CXXFLAGS := -std=c++17 -test: $(addprefix test-,$(TEST_DIRS)) custom-test-array testxx-result +test: $(addprefix test-,$(TEST_DIRS)) custom-test-array clean-and-test: $(MAKE) clean-llbc @@ -63,7 +63,7 @@ test/issue_105.llbc: CHARON_EXTRA = \ --include=core::cmp::* \ --include=core::convert::* -test/array2d.llbc: CHARON_EXTRA = --include=core::array::equality::* +# test/array2d.llbc: CHARON_EXTRA = --include=core::array::equality::* test/println.llbc: CHARON_EXTRA = \ --include=core::fmt::Arguments --include=core::fmt::rt::*::new_const \ diff --git a/lib/PreCleanup.ml b/lib/PreCleanup.ml index 8256cae7..a4d64368 100644 --- a/lib/PreCleanup.ml +++ b/lib/PreCleanup.ml @@ -50,8 +50,11 @@ let remove_array_eq = object assert (t = u); if is_flat t then let diff = n_binders - n_cgs in - let pattern = Str.regexp {|{core::cmp::PartialEq<@Array<\([a-zA-Z_][a-zA-Z0-9_]*\), \([a-zA-Z_][a-zA-Z0-9_]*\)>> for @Array<\([a-zA-Z_][a-zA-Z0-9_]*\), \([a-zA-Z_][a-zA-Z0-9_]*\)>}|} in + let pattern = + Str.regexp {|\{core::cmp::PartialEq::<@Array<.*, .*>, @Array<.*, .*>>\}|} in + (* Str.regexp {|{core::cmp::PartialEq::<@Array<\\(.*?\\), \\(.*?\\)>, @Array<\\(.*?\\), \\(.*?\\)>}|} in *) let matches_eq_array s = + s == "{core::cmp::PartialEq<@Array> for @Array}" || try if Str.string_match pattern s 0 then true else From d5880d9121d191945f419b7e2bb0309d299e06f3 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Thu, 11 Sep 2025 15:57:07 +0800 Subject: [PATCH 05/20] wip: trying to rewrite slice_len using re-ploy --- lib/AstOfLlbc.ml | 4 ++-- lib/Cleanup2.ml | 43 +++++++++++++++++++++++++++++++++++-------- 2 files changed, 37 insertions(+), 10 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index ebb89c6e..b0b271de 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -1805,8 +1805,8 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = begin (* TODO: this whole piece of code should handle TCgArray too *) match t_from, is_dst env t_to, ty_from, ty_to with - | TBuf (TApp (lid1, [ TArray (u1, n) ]), _), Some (lid2, TApp (slice_hd, [ u2 ]), t_u), _, _ - when lid1 = lid2 && u1 = u2 && slice_hd = Builtin.derefed_slice -> + | TBuf (TApp (_lid1, [ TArray (u1, n) ]), _), Some (_lid2, TApp (slice_hd, [ u2 ]), t_u), _, _ + when u1 = u2 && slice_hd = Builtin.derefed_slice -> let len = Krml.Helpers.mk_sizet (int_of_string (snd n)) in (* Cast from a struct whose last field is `t data[n]` to a struct whose last field is `Eurydice_derefed_slice data` (a.k.a. `char data[]`) *) diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 90bd5605..922134a3 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -356,7 +356,8 @@ let remove_array_from_fn files = super#visit_DFunction () cc flags n_cgs n t name bs e method! visit_EApp env e es = - match e.node with + (* let e = AstOfLlbc.re_polymorphize e in *) + match (e).node with | ETApp ( { node = EQualified ([ "core"; "array" ], "from_fn"); _ }, [ len ], @@ -1054,13 +1055,39 @@ let bonus_cleanups = inherit [_] map as super method! extend env b = b.node.name :: env - method! visit_lident _ lid = - match lid with - | [ "core"; "slice"; "{@Slice}" ], "len" -> [ "Eurydice" ], "slice_len" - | [ "core"; "slice"; "{@Slice}" ], "copy_from_slice" -> [ "Eurydice" ], "slice_copy" - | [ "core"; "slice"; "{@Slice}" ], "split_at" -> [ "Eurydice" ], "slice_split_at" - | [ "core"; "slice"; "{@Slice}" ], "split_at_mut" -> [ "Eurydice" ], "slice_split_at_mut" - | _ -> lid + method! visit_expr env e = + let match_lident lid = + let is_slice_t s = + let pattern = + Str.regexp {|\{@Slice<.*>\}|} in + s = "{@Slice}" || Str.string_match pattern s 0 + in + match lid with + | [ "core"; "slice"; s ], "len" when is_slice_t s -> true, ([ "Eurydice" ], "slice_len") + (* | [ "core"; "slice"; _s ], "len" -> true, ([ "Eurydice" ], "slice_len") *) + | [ "core"; "slice"; s ], "copy_from_slice" when is_slice_t s -> true, ([ "Eurydice" ], "slice_copy") + | [ "core"; "slice"; s ], "split_at" when is_slice_t s -> true, ([ "Eurydice" ], "slice_split_at") + | [ "core"; "slice"; s ], "split_at_mut" when is_slice_t s -> true, ([ "Eurydice" ], "slice_split_at_mut") + | _ -> false, lid + in + let e' = AstOfLlbc.re_polymorphize e in + L.log "Cleanup2" "[Bonus] Visiting e': %a\n" pexpr e'; + match e'.node with + | ETApp (expr, cgs, [], ts) -> begin + match expr.node with + | EQualified lid -> + L.log "Cleanup2" "[Bonus] Visiting lid: %a\n" plid lid; + let matched, lid = match_lident lid in + if matched then + begin + L.log "Cleanup2" "[Bonus] lid: %a matched!\n" plid lid; + with_type e.typ (ETApp ({ expr with node = EQualified lid }, cgs, [], ts)) + end + else super#visit_expr env e + + | _ -> super#visit_expr env e + end + | _ -> super#visit_expr env e method! visit_ELet ((bs, _) as env) b e1 e2 = match e1.node, e1.typ, e2.node with From 13f6d25cd74f3e9657ceedb9f9c41ccccd713a43 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Fri, 12 Sep 2025 12:00:13 +0800 Subject: [PATCH 06/20] passed slice_len by updated bonus_check and moving [drop_unused] after it --- bin/main.ml | 5 +++-- lib/Builtin.ml | 20 ++++++++++++++++++++ lib/Cleanup2.ml | 25 +++++++++++-------------- lib/PreCleanup.ml | 28 +++++++++++++++------------- 4 files changed, 49 insertions(+), 29 deletions(-) diff --git a/bin/main.ml b/bin/main.ml index a858ccf1..c9b9e477 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -254,7 +254,7 @@ Supported options:|} let errors, files = Krml.Checker.check_everything ~warn:true files in if errors then fail __FILE__ __LINE__; - let files = Krml.Inlining.drop_unused files in + (*let files = Krml.Inlining.drop_unused files in*) let files = Eurydice.Cleanup2.remove_array_temporaries#visit_files () files in Eurydice.Logging.log "Phase2.25" "%a" pfiles files; let files = Eurydice.Cleanup2.remove_array_repeats#visit_files () files in @@ -279,7 +279,7 @@ Supported options:|} let files = Eurydice.Cleanup2.remove_array_from_fn files in Eurydice.Logging.log "Phase2.6" "%a" pfiles files; (* remove_array_from_fn, above, creates further opportunities for removing unused functions. *) - let files = Krml.Inlining.drop_unused files in + (* let files = Krml.Inlining.drop_unused files in *) let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files () files in (* Creates opportunities for removing unused variables *) let files = Eurydice.Cleanup2.remove_assign_return#visit_files () files in @@ -302,6 +302,7 @@ Supported options:|} let files = Eurydice.Cleanup2.float_comments files in Eurydice.Logging.log "Phase2.95" "%a" pfiles files; let files = Eurydice.Cleanup2.bonus_cleanups#visit_files [] files in + let files = Krml.Inlining.drop_unused files in (* Macros stemming from globals -- FIXME why is this not Krml.AstToCStar.mk_macros_set? *) let files, macros = Eurydice.Cleanup2.build_macros files in diff --git a/lib/Builtin.ml b/lib/Builtin.ml index 5bc6d445..31a03ee1 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -282,6 +282,24 @@ let slice_index = arg_names = [ "s"; "i" ]; } +let slice_len = + { + name = [ "Eurydice" ], "slice_len"; + typ = Krml.Helpers.fold_arrow [ mk_slice (TBound 0)] (TInt SizeT); + n_type_args = 1; + cg_args = []; + arg_names = [ "s" ]; + } + +let slice_copy = + { + name = [ "Eurydice" ], "slice_copy"; + typ = Krml.Helpers.fold_arrow [ mk_slice (TBound 0)] (mk_slice (TBound 0)); + n_type_args = 1; + cg_args = []; + arg_names = [ "s" ]; + } + let slice_index_outparam = { name = [ "Eurydice" ], "slice_index_outparam"; @@ -730,6 +748,8 @@ let builtin_funcs = array_eq; array_eq_slice; slice_eq; + slice_len; + slice_copy; slice_index; slice_index_outparam; slice_subslice; diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 922134a3..f86dc3ff 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -1050,7 +1050,6 @@ let remove_assign_return = end let bonus_cleanups = - let open Krml in object (self) inherit [_] map as super method! extend env b = b.node.name :: env @@ -1063,25 +1062,23 @@ let bonus_cleanups = s = "{@Slice}" || Str.string_match pattern s 0 in match lid with - | [ "core"; "slice"; s ], "len" when is_slice_t s -> true, ([ "Eurydice" ], "slice_len") - (* | [ "core"; "slice"; _s ], "len" -> true, ([ "Eurydice" ], "slice_len") *) - | [ "core"; "slice"; s ], "copy_from_slice" when is_slice_t s -> true, ([ "Eurydice" ], "slice_copy") - | [ "core"; "slice"; s ], "split_at" when is_slice_t s -> true, ([ "Eurydice" ], "slice_split_at") - | [ "core"; "slice"; s ], "split_at_mut" when is_slice_t s -> true, ([ "Eurydice" ], "slice_split_at_mut") - | _ -> false, lid + | [ "core"; "slice"; s ], "len" when is_slice_t s -> true, ([ "Eurydice" ], "slice_len"), Builtin.slice_len.typ + | [ "core"; "slice"; s ], "copy_from_slice" when is_slice_t s -> true, ([ "Eurydice" ], "slice_copy"), Builtin.slice_copy.typ + | [ "core"; "slice"; s ], "split_at" when is_slice_t s -> true, ([ "Eurydice" ], "slice_split_at"), TAny (*todo*) + | [ "core"; "slice"; s ], "split_at_mut" when is_slice_t s -> true, ([ "Eurydice" ], "slice_split_at_mut"), TAny + | _ -> false, lid, TAny in let e' = AstOfLlbc.re_polymorphize e in - L.log "Cleanup2" "[Bonus] Visiting e': %a\n" pexpr e'; match e'.node with | ETApp (expr, cgs, [], ts) -> begin match expr.node with | EQualified lid -> L.log "Cleanup2" "[Bonus] Visiting lid: %a\n" plid lid; - let matched, lid = match_lident lid in + let matched, lid, t = match_lident lid in if matched then begin L.log "Cleanup2" "[Bonus] lid: %a matched!\n" plid lid; - with_type e.typ (ETApp ({ expr with node = EQualified lid }, cgs, [], ts)) + with_type e.typ (ETApp ({ expr with node = EQualified lid; typ = t }, cgs, [], ts)) end else super#visit_expr env e @@ -1095,7 +1092,7 @@ let bonus_cleanups = | ( EAny, _, ESequence [ { node = EAssign ({ node = EBound 0; _ }, e3); _ }; { node = EBound 0; _ } ] ) - -> (DeBruijn.subst Helpers.eunit 0 e3).node + -> Krml.(DeBruijn.subst Helpers.eunit 0 e3).node (* let uu; memcpy(uu, ..., src, ...); e2 --> let copy_of_src; ... *) | ( EAny, TArray (_, (_, n)), @@ -1125,11 +1122,11 @@ let bonus_cleanups = | ( EApp ({ node = EQualified _; _ }, es), _, ESequence [ { node = EAssign (e2, { node = EBound 0; _ }); _ }; e3 ] ) - when Helpers.is_uu b.node.name && List.for_all Helpers.is_readonly_c_expression es -> + when Krml.Helpers.is_uu b.node.name && List.for_all Krml.Helpers.is_readonly_c_expression es -> ESequence [ - with_type TUnit (EAssign (DeBruijn.subst Helpers.eunit 0 e2, e1)); - self#visit_expr env (DeBruijn.subst Helpers.eunit 0 e3); + with_type TUnit (EAssign (Krml.DeBruijn.subst Krml.Helpers.eunit 0 e2, e1)); + self#visit_expr env (Krml.DeBruijn.subst Krml.Helpers.eunit 0 e3); ] | _ -> super#visit_ELet env b e1 e2 end diff --git a/lib/PreCleanup.ml b/lib/PreCleanup.ml index a4d64368..b30ecc26 100644 --- a/lib/PreCleanup.ml +++ b/lib/PreCleanup.ml @@ -50,22 +50,24 @@ let remove_array_eq = object assert (t = u); if is_flat t then let diff = n_binders - n_cgs in - let pattern = + let pattern_array_eq = Str.regexp {|\{core::cmp::PartialEq::<@Array<.*, .*>, @Array<.*, .*>>\}|} in - (* Str.regexp {|{core::cmp::PartialEq::<@Array<\\(.*?\\), \\(.*?\\)>, @Array<\\(.*?\\), \\(.*?\\)>}|} in *) - let matches_eq_array s = - s == "{core::cmp::PartialEq<@Array> for @Array}" || - try - if Str.string_match pattern s 0 then true - else - false - with Not_found -> false in - let matches_eq_slice = Str.regexp {|{core::cmp::PartialEq<&.* \(@Slice<\([a-zA-Z_][a-zA-Z0-9_]*\)>\)> for @Array<\([a-zA-Z_][a-zA-Z0-9_]*\), \([a-zA-Z_][a-zA-Z0-9_]*\)>}|} in - let matches_eq_slice s = Str.string_match matches_eq_slice s 0 in - if matches_eq_array impl then with_type TBool (EApp ( + let matches_array_eq_slice = + Str.regexp {|\{core::cmp::PartialEq::<&.* @Slice<,*>, @Array<.*, .*)>>\}|} in + (*todo: this pattern is not tested yet*) + let matches_array_eq s = + match s with + | "{core::cmp::PartialEq<@Array> for @Array}" -> true + (* non-monomorphized LLBC *) + | _ -> try Str.string_match pattern_array_eq s 0 with Not_found -> false in + let matches_array_eq_slice s = + match s with + | "" -> true + | _ -> try Str.string_match matches_array_eq_slice s 0 with Not_found -> false in + if matches_array_eq impl then with_type TBool (EApp ( Builtin.(expr_of_builtin_t ~cgs:(diff, [n]) array_eq [ t ]), [ a1; a2 ])) - else if matches_eq_slice impl then with_type TBool (EApp ( + else if matches_array_eq_slice impl then with_type TBool (EApp ( Builtin.(expr_of_builtin_t ~cgs:(diff, [n]) array_eq_slice [ t ]), [ a1; a2 ])) else failwith ("unknown array eq impl: " ^ impl) From caaeee81cce862771ef703a1c79f024454e64456 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Fri, 12 Sep 2025 16:52:45 +0800 Subject: [PATCH 07/20] wip: trying to fix from_fn by adding fn_ptrs into the re-poly map --- lib/AstOfLlbc.ml | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index df17449e..846af087 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -279,9 +279,6 @@ let string_of_fn_ptr env fn_ptr = string_of_pattern (pattern_of_fn_ptr env fn_pt (** Translation of types *) -(* let lid_full_generic = Hashtbl.create 41*) - - let width_of_integer_type (t : Charon.Types.integer_type) : K.width = match t with | Signed Isize -> PtrdiffT @@ -516,11 +513,11 @@ let re_polymorphize expr = object inherit [_] Krml.Ast.map method! visit_EQualified ((), ty) full_name = try - let name, cgs, ts = Hashtbl.find lid_full_generic full_name in + let name, cgs, ts, fn_ptrs = Hashtbl.find lid_full_generic full_name in if cgs = [] && ts = [] then EQualified full_name else - ETApp (K.with_type (ty_re_polymorphize ty cgs ts) (K.EQualified name), cgs, [], ts) + ETApp (K.with_type (ty_re_polymorphize ty cgs ts) (K.EQualified name), cgs, fn_ptrs, ts) with Not_found -> EQualified full_name end#visit_expr_w () expr @@ -528,6 +525,14 @@ let pure_lid_of_name (env : env) (name : Charon.Types.name) : K.lident = let prefix, name = Krml.KList.split_at_last name in List.map (string_of_path_elem env) prefix, string_of_path_elem env name +let update_lid_full_generic_fnptrs (full_name : K.lident) (fn_ptrs : K.expr list) = + L.log "AstOfLlbc" "[re-poly] trying to update the fn_ptrs of %a to %a" plid full_name pexprs fn_ptrs; + try + let name, cgs, ts, _ = Hashtbl.find lid_full_generic full_name in + L.log "AstOfLlbc" "[re-poly] updated the fn_ptrs of %a to %a" plid full_name pexprs fn_ptrs; + Hashtbl.replace lid_full_generic full_name (name, cgs, ts, fn_ptrs) + with Not_found -> () + let rec insert_lid_full_generic (env : env) (full_name : K.lident) (name : Charon.Types.name) = let (item_name, generic) = let (pre, last) = Krml.KList.split_at_last name in @@ -542,7 +547,7 @@ let rec insert_lid_full_generic (env : env) (full_name : K.lident) (name : Charo if not (Hashtbl.mem lid_full_generic full_name) then L.log "AstOfLlbc" "mono name : %a\n repolyed name : %a with cgs %a and tys %a " plid full_name plid item_name pexprs cgs ptyps tys; - Hashtbl.add lid_full_generic full_name (item_name, cgs, tys) + Hashtbl.add lid_full_generic full_name (item_name, cgs, tys, []) and lid_of_name (env : env) (name : Charon.Types.name) : K.lident = let lid = pure_lid_of_name env name in @@ -1636,6 +1641,12 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = else hd in + begin + match hd.node with + | EQualified full_name -> update_lid_full_generic_fnptrs full_name fn_ptrs + (* wip: actually when fn_ptrs can be found, the name of hd is the short name instread of monoed full name*) + | _ -> () + end; L.log "Calls" "%s--> hd: %a" depth pexpr hd; ( hd, is_known_builtin, From 674333f62b7da1e14fd51a60c15bf35d3d372e09 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Mon, 15 Sep 2025 10:01:17 +0800 Subject: [PATCH 08/20] wip: minor fix of slice_copy --- Makefile | 8 ++++---- lib/Builtin.ml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Makefile b/Makefile index 8b6a87d3..610ea038 100644 --- a/Makefile +++ b/Makefile @@ -8,9 +8,9 @@ TEST_DIRS = $(filter-out $(BROKEN_TESTS),$(basename $(notdir $(wildcard test/*. # Warn on old versions of bash _ := $(shell bash -c '(( $${BASH_VERSION%%.*} >= 4 ))') -#ifneq ($(.SHELLSTATUS),0) -#_: $(error "bash version is too old; hint: brew install bash") -#endif +ifneq ($(.SHELLSTATUS),0) +_: $(error "bash version is too old; hint: brew install bash") +endif # Enable `foo/**` glob syntax SHELL := bash -O globstar @@ -41,7 +41,7 @@ build: CFLAGS := -Wall -Werror -Wno-unused-variable $(CFLAGS) -I$(KRML_HOME)/include CXXFLAGS := -std=c++17 -test: $(addprefix test-,$(TEST_DIRS)) custom-test-array +test: $(addprefix test-,$(TEST_DIRS)) custom-test-array testxx-result clean-and-test: $(MAKE) clean-llbc diff --git a/lib/Builtin.ml b/lib/Builtin.ml index 31a03ee1..bcb5604e 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -294,7 +294,7 @@ let slice_len = let slice_copy = { name = [ "Eurydice" ], "slice_copy"; - typ = Krml.Helpers.fold_arrow [ mk_slice (TBound 0)] (mk_slice (TBound 0)); + typ = Krml.Helpers.fold_arrow [ mk_slice (TBound 0); mk_slice (TBound 0) ] TUnit; n_type_args = 1; cg_args = []; arg_names = [ "s" ]; From 42deeed32f5b2f3a1b501be162310f5be77f7325 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Mon, 15 Sep 2025 17:13:50 +0800 Subject: [PATCH 09/20] wip: trying to find the trait func impl for from_fn --- lib/AstOfLlbc.ml | 234 +++++++++++++++++++++++++++-------------------- lib/Cleanup2.ml | 4 +- 2 files changed, 135 insertions(+), 103 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 846af087..346e3473 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -520,7 +520,21 @@ let re_polymorphize expr = object ETApp (K.with_type (ty_re_polymorphize ty cgs ts) (K.EQualified name), cgs, fn_ptrs, ts) with Not_found -> EQualified full_name end#visit_expr_w () expr - + +(* get the charon name without the last PeMonomorphized, used for match blocklist *) +let pure_c_name (name : C.name) = + let (pre, last) = Krml.KList.split_at_last name in + match last with + | PeMonomorphized _args -> pre + | _ -> name + +(* get the trait_refs from mono. charon name, used in lookup_fun *) +let trait_refs_c_name (name: C.name) : C.trait_ref list = + let (_pre, last) = Krml.KList.split_at_last name in + match last with + | PeMonomorphized args -> args.trait_refs + | _ -> [] + let pure_lid_of_name (env : env) (name : Charon.Types.name) : K.lident = let prefix, name = Krml.KList.split_at_last name in List.map (string_of_path_elem env) prefix, string_of_path_elem env name @@ -531,7 +545,7 @@ let update_lid_full_generic_fnptrs (full_name : K.lident) (fn_ptrs : K.expr list let name, cgs, ts, _ = Hashtbl.find lid_full_generic full_name in L.log "AstOfLlbc" "[re-poly] updated the fn_ptrs of %a to %a" plid full_name pexprs fn_ptrs; Hashtbl.replace lid_full_generic full_name (name, cgs, ts, fn_ptrs) - with Not_found -> () + with Not_found -> (failwith "update_lid_full_generic_fnptrs: not found") let rec insert_lid_full_generic (env : env) (full_name : K.lident) (name : Charon.Types.name) = let (item_name, generic) = @@ -1338,7 +1352,7 @@ and debug_trait_clause_mapping env (mapping : (var_id * K.typ) list) = type information required to build a proper instantiation. The function reference is an expression that is either a reference to a variable in scope (trait methods), or to a top-level qualified name, which encompasses both externally-defined function (builtins), or regular functions. *) -let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result = +let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result * C.trait_ref list = let open RustNames in let matches p = Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config p f in let builtin b = @@ -1348,13 +1362,14 @@ let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result = K.EQualified name, { ts; arg_types; ret_type; cg_types = cg_args; is_known_builtin = true } in match List.find_opt (fun (p, _) -> matches p) known_builtins with - | Some (_, b) -> builtin b + | Some (_, b) -> let hd, res = builtin b in hd, res, [] | None -> ( let lookup_result_of_fun_id fun_id = let { C.item_meta; signature; _ } = env.get_nth_function fun_id in let lid = lid_of_name env item_meta.name in L.log "Calls" "%s--> name: %a" depth plid lid; - K.EQualified lid, lookup_signature env depth signature + let trait_refs = trait_refs_c_name item_meta.name in + K.EQualified lid, lookup_signature env depth signature, trait_refs in match f.func with @@ -1382,7 +1397,8 @@ let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result = in let ret_type, arg_types = Krml.Helpers.flatten_arrow t in let cg_types, arg_types = Krml.KList.split sig_info.n_cgs arg_types in - EBound f, { ts = sig_info; cg_types; arg_types; ret_type; is_known_builtin = false } + EBound f, { ts = sig_info; cg_types; arg_types; ret_type; is_known_builtin = false }, [] + (* todo: check whether trait_refs is needed here *) | _ -> fail "Error looking trait ref: %s %s%!" (Charon.PrintTypes.trait_ref_to_string env.format_env trait_ref) @@ -1442,11 +1458,16 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = (String.concat ", " (List.map (Charon.PrintTypes.ty_to_string env.format_env) type_args)); (* The function itself, along with information about its *signature*. *) - let f, { ts; arg_types = inputs; ret_type = output; cg_types = cg_inputs; is_known_builtin } = + let f, { ts; arg_types = inputs; ret_type = output; cg_types = cg_inputs; is_known_builtin }, trait_refs_mono = lookup_fun env depth fn_ptr in L.log "Calls" "%s--> %d inputs: %a" depth (List.length inputs) ptyps inputs; L.log "Calls" "%s--> is_known_builtin?: %b" depth is_known_builtin; + L.log "Calls" "%s--> [MONO] trait from mono name: %s\n" depth + (String.concat " ++ " + (List.map (Charon.PrintTypes.trait_ref_to_string env.format_env) trait_refs)); + L.log "Calls" "%s--> [MONO] end of trait refs" depth; + (* Translate effective type and cg arguments. *) let const_generic_args = @@ -1472,6 +1493,93 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = (* Handling trait implementations for generic trait bounds in the callee. We synthesize krml expressions that correspond to each one of the trait methods that the callee expects. Order matters here. *) + + + (* MUST have the same structure as mk_clause_binders_and_args *) + let rec build_trait_ref_mapping depth (trait_refs : C.trait_ref list) = + List.concat_map + (fun (trait_ref : C.trait_ref) -> + let cname = pure_c_name (env.get_nth_trait_decl trait_ref.trait_decl_ref.binder_value.id).item_meta.name in + let name = string_of_name env cname in + L.log "Calls" "%s--> trait_ref %s: %s\n" depth name (C.show_trait_ref trait_ref); + + match trait_ref.trait_id with + | _ when List.mem name blocklisted_trait_decls -> + (* Trait not supported -- don't synthesize arguments *) + [] + | TraitImpl { id = impl_id; generics = _generics } -> + (* Call-site has resolved trait clauses into a concrete trait implementation. *) + let trait_impl : C.trait_impl = env.get_nth_trait_impl impl_id in + + (* This must be in agreement, and in the same order as mk_clause_binders_and_args *) + List.map + (fun ((_item_name, { C.id; generics }) : _ * C.global_decl_ref) -> + if + not + (generics.types = [] && generics.const_generics = [] + && generics.trait_refs = []) + then + failwith "TODO: polymorphic globals"; + let global = env.get_nth_global id in + K.with_type (typ_of_ty env global.ty) + (K.EQualified (lid_of_name env global.item_meta.name))) + trait_impl.consts + @ List.map + (fun ((item_name, bound_fn) : _ * C.fun_decl_ref C.binder) -> + let fun_decl_id = bound_fn.C.binder_value.C.id in + let fn_ptr : C.fn_ptr = + { + func = TraitMethod (trait_ref, item_name, fun_decl_id); + generics = Charon.TypesUtils.empty_generic_args; + } + in + let fn_ptr = fst3 (expression_of_fn_ptr env (depth ^ " ") fn_ptr) in + fn_ptr) + trait_impl.methods + @ build_trait_ref_mapping (" " ^ depth) + (let subst = + Charon.Substitute.make_subst_from_generics trait_impl.generics _generics + in + (*_generics.trait_refs*) + List.map + (Charon.Substitute.st_substitute_visitor#visit_trait_ref subst) + trait_impl.parent_trait_refs) + | Clause _ as clause_id -> + (* Caller it itself polymorphic and refers to one of its own clauses to synthesize + the clause arguments at call-site. We must pass whatever is relevant for this + clause, *transitively* (this means all the reachable parents). *) + let rec relevant = function + | C.ParentClause (tref', _) -> relevant tref'.trait_id + | clause_id' -> clause_id = clause_id' + in + List.rev + (Krml.KList.filter_mapi + (fun i (var, t) -> + match var with + | TraitClauseMethod { clause_id = clause_id'; _ } + | TraitClauseConstant { clause_id = clause_id'; _ } + when relevant clause_id' -> Some K.(with_type t (EBound i)) + | _ -> None) + env.binders) + | ParentClause (tref, clause_id) -> + let decl_id = tref.trait_decl_ref.binder_value.id in + let trait_decl = env.get_nth_trait_decl decl_id in + let name = string_of_name env trait_decl.item_meta.name in + let clause_id = C.TraitClauseId.to_int clause_id in + let parent_clause = List.nth trait_decl.parent_clauses clause_id in + let parent_clause_decl = + env.get_nth_trait_decl parent_clause.trait.binder_value.id + in + let parent_name = string_of_name env parent_clause_decl.item_meta.name in + Krml.KPrint.bprintf "looking up parent clause #%d of decl=%s = %s\n" clause_id name + parent_name; + if List.mem parent_name blocklisted_trait_decls then + [] + else + failwith "Don't know how to resolve trait_ref above (1)" + | _ -> failwith "Don't know how to resolve trait_ref above (2)") + trait_refs + in let fn_ptrs : K.expr list = if is_known_builtin then (* If this is a known builtin implementation, we do not materialize trait methods, on the @@ -1480,97 +1588,27 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = anyhow. *) [] else - (* MUST have the same structure as mk_clause_binders_and_args *) - let rec build_trait_ref_mapping depth (trait_refs : C.trait_ref list) = - List.concat_map - (fun (trait_ref : C.trait_ref) -> - let name = - string_of_name env - (env.get_nth_trait_decl trait_ref.trait_decl_ref.binder_value.id).item_meta.name - in - L.log "Calls" "%s--> trait_ref %s: %s\n" depth name (C.show_trait_ref trait_ref); - - match trait_ref.trait_id with - | _ when List.mem name blocklisted_trait_decls -> - (* Trait not supported -- don't synthesize arguments *) - [] - | TraitImpl { id = impl_id; generics = _generics } -> - (* Call-site has resolved trait clauses into a concrete trait implementation. *) - let trait_impl : C.trait_impl = env.get_nth_trait_impl impl_id in - - (* This must be in agreement, and in the same order as mk_clause_binders_and_args *) - List.map - (fun ((_item_name, { C.id; generics }) : _ * C.global_decl_ref) -> - if - not - (generics.types = [] && generics.const_generics = [] - && generics.trait_refs = []) - then - failwith "TODO: polymorphic globals"; - let global = env.get_nth_global id in - K.with_type (typ_of_ty env global.ty) - (K.EQualified (lid_of_name env global.item_meta.name))) - trait_impl.consts - @ List.map - (fun ((item_name, bound_fn) : _ * C.fun_decl_ref C.binder) -> - let fun_decl_id = bound_fn.C.binder_value.C.id in - let fn_ptr : C.fn_ptr = - { - func = TraitMethod (trait_ref, item_name, fun_decl_id); - generics = Charon.TypesUtils.empty_generic_args; - } - in - let fn_ptr = fst3 (expression_of_fn_ptr env (depth ^ " ") fn_ptr) in - fn_ptr) - trait_impl.methods - @ build_trait_ref_mapping (" " ^ depth) - (let subst = - Charon.Substitute.make_subst_from_generics trait_impl.generics _generics - in - (*_generics.trait_refs*) - List.map - (Charon.Substitute.st_substitute_visitor#visit_trait_ref subst) - trait_impl.parent_trait_refs) - | Clause _ as clause_id -> - (* Caller it itself polymorphic and refers to one of its own clauses to synthesize - the clause arguments at call-site. We must pass whatever is relevant for this - clause, *transitively* (this means all the reachable parents). *) - let rec relevant = function - | C.ParentClause (tref', _) -> relevant tref'.trait_id - | clause_id' -> clause_id = clause_id' - in - List.rev - (Krml.KList.filter_mapi - (fun i (var, t) -> - match var with - | TraitClauseMethod { clause_id = clause_id'; _ } - | TraitClauseConstant { clause_id = clause_id'; _ } - when relevant clause_id' -> Some K.(with_type t (EBound i)) - | _ -> None) - env.binders) - | ParentClause (tref, clause_id) -> - let decl_id = tref.trait_decl_ref.binder_value.id in - let trait_decl = env.get_nth_trait_decl decl_id in - let name = string_of_name env trait_decl.item_meta.name in - let clause_id = C.TraitClauseId.to_int clause_id in - let parent_clause = List.nth trait_decl.parent_clauses clause_id in - let parent_clause_decl = - env.get_nth_trait_decl parent_clause.trait.binder_value.id - in - let parent_name = string_of_name env parent_clause_decl.item_meta.name in - Krml.KPrint.bprintf "looking up parent clause #%d of decl=%s = %s\n" clause_id name - parent_name; - if List.mem parent_name blocklisted_trait_decls then - [] - else - failwith "Don't know how to resolve trait_ref above (1)" - | _ -> failwith "Don't know how to resolve trait_ref above (2)") - trait_refs - in build_trait_ref_mapping depth trait_refs in L.log "Calls" "%s--> trait method impls: %d" depth (List.length fn_ptrs); - + let fn_ptrs_mono : K.expr list = + if is_known_builtin then + (* If this is a known builtin implementation, we do not materialize trait methods, on the + basis that this is likely something from the standard library that exercises more features + that we can support, and that since we hand-write it, we don't need this level of precision + anyhow. *) + [] + else + build_trait_ref_mapping depth trait_refs_mono + in + (* update the fn_ptrs_mono in the table *) + begin + if fn_ptrs_mono <> [] then + match f with + | EQualified full_name -> update_lid_full_generic_fnptrs full_name fn_ptrs_mono + | _ -> () + end; + (* This needs to match what is done in the FunGroup case (i.e. when we extract a definition). There are two behaviors depending on whether the function is builtin or not. *) @@ -1641,12 +1679,6 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = else hd in - begin - match hd.node with - | EQualified full_name -> update_lid_full_generic_fnptrs full_name fn_ptrs - (* wip: actually when fn_ptrs can be found, the name of hd is the short name instread of monoed full name*) - | _ -> () - end; L.log "Calls" "%s--> hd: %a" depth pexpr hd; ( hd, is_known_builtin, diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index f86dc3ff..59545f2d 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -356,8 +356,8 @@ let remove_array_from_fn files = super#visit_DFunction () cc flags n_cgs n t name bs e method! visit_EApp env e es = - (* let e = AstOfLlbc.re_polymorphize e in *) - match (e).node with + let e' = AstOfLlbc.re_polymorphize e in + match e'.node with | ETApp ( { node = EQualified ([ "core"; "array" ], "from_fn"); _ }, [ len ], From 300c02c448bd43114289d283b6743c5a3cfaecf4 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Tue, 16 Sep 2025 11:52:38 +0800 Subject: [PATCH 10/20] fixed the name inconsistency caused by [improve_names] --- lib/Cleanup2.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 59545f2d..5be5367c 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -862,6 +862,18 @@ let improve_names files = Krml.Bundle.Lid (fst (Hashtbl.find renamed lid)) | x -> x) !Krml.Options.static_header; + let update_expr e = + match e.node with + | EQualified lid when Hashtbl.mem renamed lid -> + { e with node = EQualified (fst (Hashtbl.find renamed lid))} + | _ -> e + in + let update_value _key value = + match value with name, cgs, ts, fn_ptrs -> + let fn_ptrs = List.map update_expr fn_ptrs in + Some (name, cgs, ts, fn_ptrs) + in + Hashtbl.filter_map_inplace update_value AstOfLlbc.lid_full_generic; (object (self) inherit [_] map From 3c50bda7888de51d82b08b0268710c91c78f6559 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Tue, 16 Sep 2025 15:55:03 +0800 Subject: [PATCH 11/20] wip: fixed trivial case of from_fn and map --- lib/Cleanup2.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 5be5367c..10a568dd 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -379,6 +379,13 @@ let remove_array_from_fn files = in let lift1 = Krml.DeBruijn.lift 1 in let t_dst = H.assert_tbuf_or_tarray dst.typ in + (* erase the type of the empty closure struct. This is redundant with [Krml.remove_empty_struct] for non-monoed LLBC, + but needed for monoed LLBC because these fn_ptrs come from the table [lid_full_generic] which is not visited by + the Krml file rewriter *) + let call_mut = match call_mut.typ with + | TArrow (_closure_ref, e) -> { call_mut with typ = TArrow (TBuf (TUnit, false), e)} + | _ -> failwith "unexpected type of the call_mut closure function" + in EFor ( Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i: size_t = 0 *), @@ -412,8 +419,9 @@ let remove_array_from_fn files = ts ) -> let t_src, t_dst = match ts with - | [ t_src; t_state; t_dst ] -> - assert (t_state = TUnit); + | [ t_src; _t_state; t_dst ] -> + (* assert (t_state = TUnit); *) + (* This t_state is not visited by [remove_empty_struct] for monoed-LLBC, see the comment for call_mut above *) L.log "Cleanup2" "found array map from %a to %a" ptyp t_src ptyp t_dst; t_src, t_dst | _ -> @@ -426,6 +434,10 @@ let remove_array_from_fn files = in let lift1 = Krml.DeBruijn.lift 1 in let e_state = with_type (TBuf (e_state.typ, false)) (EAddrOf (lift1 e_state)) in + let call_mut = match call_mut.typ with + | TArrow (_closure_ref, e) -> { call_mut with typ = TArrow (TBuf (TUnit, false), e)} + | _ -> failwith "unexpected type of the call_mut closure function" + in EFor ( Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i = 0 *), From ce3f6efcc50e2b4efb161d5f2aaca3fea59e7c56 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Wed, 17 Sep 2025 10:32:04 +0800 Subject: [PATCH 12/20] apply [remove_empty_struct] on the [lid_full_generic], ignored [pass_by_ref] for nested_from_fn for now --- bin/main.ml | 2 +- lib/Cleanup2.ml | 78 ++++++++++++++++++++++++++++++++++++++++--------- 2 files changed, 65 insertions(+), 15 deletions(-) diff --git a/bin/main.ml b/bin/main.ml index 62c2f401..d7167a27 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -233,7 +233,7 @@ Supported options:|} (* Must happen now, before Monomorphization.datatypes, because otherwise MonomorphizationState.state gets filled with lids that later on get eliminated on the basis that they were empty structs to begin with, which would send Checker off the rails *) - let files = Krml.DataTypes.remove_empty_structs files in + let files = Eurydice.Cleanup2.remove_empty_structs files in let files = Krml.Monomorphization.datatypes files in let files = Eurydice.Cleanup2.drop_unused_type files in (* Cannot use remove_unit_buffers as it is technically incorrect *) diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 10a568dd..2da3e6ff 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -379,13 +379,6 @@ let remove_array_from_fn files = in let lift1 = Krml.DeBruijn.lift 1 in let t_dst = H.assert_tbuf_or_tarray dst.typ in - (* erase the type of the empty closure struct. This is redundant with [Krml.remove_empty_struct] for non-monoed LLBC, - but needed for monoed LLBC because these fn_ptrs come from the table [lid_full_generic] which is not visited by - the Krml file rewriter *) - let call_mut = match call_mut.typ with - | TArrow (_closure_ref, e) -> { call_mut with typ = TArrow (TBuf (TUnit, false), e)} - | _ -> failwith "unexpected type of the call_mut closure function" - in EFor ( Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i: size_t = 0 *), @@ -419,9 +412,8 @@ let remove_array_from_fn files = ts ) -> let t_src, t_dst = match ts with - | [ t_src; _t_state; t_dst ] -> - (* assert (t_state = TUnit); *) - (* This t_state is not visited by [remove_empty_struct] for monoed-LLBC, see the comment for call_mut above *) + | [ t_src; t_state; t_dst ] -> + assert (t_state = TUnit); L.log "Cleanup2" "found array map from %a to %a" ptyp t_src ptyp t_dst; t_src, t_dst | _ -> @@ -434,10 +426,6 @@ let remove_array_from_fn files = in let lift1 = Krml.DeBruijn.lift 1 in let e_state = with_type (TBuf (e_state.typ, false)) (EAddrOf (lift1 e_state)) in - let call_mut = match call_mut.typ with - | TArrow (_closure_ref, e) -> { call_mut with typ = TArrow (TBuf (TUnit, false), e)} - | _ -> failwith "unexpected type of the call_mut closure function" - in EFor ( Krml.Helpers.fresh_binder ~mut:true "i" H.usize, H.zero_usize (* i = 0 *), @@ -1450,3 +1438,65 @@ let drop_unused_type files = if (Hashtbl.mem seen lid) then Some d else None | _ -> Some d ) files + + +let remove_empty_structs files = + let open Krml.Idents in + let empty_structs = (object + + inherit [_] reduce + + method zero = LidSet.empty + method plus = LidSet.union + + method! visit_DType _ lid _ _ _ def = + if def = Flat [] then + LidSet.singleton lid + else + LidSet.empty + end)#visit_files () files in + + let files = List.map (fun (f, decls) -> + f, List.filter (fun d -> not (LidSet.mem (lid_of_decl d) empty_structs)) decls + ) files in + + let erase_obj = + (object + + inherit [_] map as super + + method! visit_TApp _ lid ts = + if LidSet.mem lid empty_structs then + TUnit + else + super#visit_TApp () lid ts + + method! visit_TCgApp _ t cg = + let lid, _, _ = flatten_tapp (TCgApp (t, cg)) in + if LidSet.mem lid empty_structs then + TUnit + else + super#visit_TCgApp () t cg + + method! visit_TQualified _ lid = + if LidSet.mem lid empty_structs then + TUnit + else + TQualified lid + + method! visit_EFlat env fields = + if fields = [] then begin + EUnit + end else + super#visit_EFlat env fields + end) + in + let update_value _key value = + match value with name, cgs, ts, fn_ptrs -> + let cgs = List.map (erase_obj#visit_expr_w ()) cgs in + let ts = List.map (erase_obj#visit_typ ()) ts in + let fn_ptrs = List.map (erase_obj#visit_expr_w ()) fn_ptrs in + Some (name, cgs, ts, fn_ptrs) + in + Hashtbl.filter_map_inplace update_value AstOfLlbc.lid_full_generic; + erase_obj#visit_files () files From 14c5b2078038c47a636e16f30c31d06493b55891 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Wed, 17 Sep 2025 15:35:33 +0800 Subject: [PATCH 13/20] minor: recorded different name for partial_eq --- test/core_cmp_lib.c | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/test/core_cmp_lib.c b/test/core_cmp_lib.c index 8c1e9ad2..b8f66018 100644 --- a/test/core_cmp_lib.c +++ b/test/core_cmp_lib.c @@ -7,3 +7,8 @@ bool core_cmp_impls__core__cmp__PartialEq_____for_____eq(void **x0, void **x1) { return true; } + +// same implementation for the monomorphized LLBC +bool core_cmp_impls__core__cmp__PartialEq____________eq(void **x0, void **x1) { + return true; +} From 164effc819d9a5ce3251c8ea6a20398921a1f31f Mon Sep 17 00:00:00 2001 From: ssyram Date: Fri, 26 Sep 2025 18:16:54 +0800 Subject: [PATCH 14/20] mono for Builtins with const-generics passed debug --- include/eurydice_glue.h | 8 + lib/AstOfLlbc.ml | 86 +++++++- lib/Builtin.ml | 74 +++++++ lib/Cleanup2.ml | 4 +- out/test-array2d/array2d.h | 20 +- out/test-closure_fn_cast/closure_fn_cast.c | 18 +- out/test-closure_fn_cast/closure_fn_cast.h | 12 +- out/test-const_generics/Eurydice.h | 14 +- out/test-const_generics/const_generics.c | 66 ++---- out/test-const_generics/const_generics.h | 235 ++++++++++++++------- 10 files changed, 368 insertions(+), 169 deletions(-) diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index 04b84367..29f1e53d 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -132,6 +132,9 @@ typedef struct { end) /* x is already at an array type, no need for cast */ #define Eurydice_array_to_subslice(_arraylen, x, r, t, _0, _1) \ EURYDICE_SLICE((t *)x, r.start, r.end) +// The mono version is exactly the same, just with a different name +#define Eurydice_array_to_subslice_mono(_arraylen, x, r, t, _0, _1) \ + EURYDICE_SLICE((t *)x, r.start, r.end) // Same as above, variant for when start and end are statically known #define Eurydice_array_to_subslice3(x, start, end, t_ptr) \ @@ -146,6 +149,11 @@ typedef struct { EURYDICE_SLICE((t *)x, 0, r) #define Eurydice_array_to_subslice_from(size, x, r, t, _range_t, _0) \ EURYDICE_SLICE((t *)x, r, size) +// The mono versions are exactly the same, just different names +#define Eurydice_array_to_subslice_to_mono(_size, x, r, t, _range_t, _0) \ + EURYDICE_SLICE((t *)x, 0, r) +#define Eurydice_array_to_subslice_from_mono(size, x, r, t, _range_t, _0) \ + EURYDICE_SLICE((t *)x, r, size) // Copy a slice with memcopy #define Eurydice_slice_copy(dst, src, t) \ diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index fcdf9bd9..752da775 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -191,6 +191,7 @@ module RustNames = struct map_vars_to_vars = false; match_with_trait_decl_refs = true; (* use_trait_decl_refs = true; *) + match_mono = true; } let vec = parse_pattern "alloc::vec::Vec<@>" @@ -203,14 +204,23 @@ module RustNames = struct parse_pattern "SliceIndexShared<'_, @T>", Builtin.slice_index; parse_pattern "SliceIndexMut<'_, @T>", Builtin.slice_index; + (* slices: generics *) parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I, @Clause2_Output>}::index<'_, @, core::ops::range::Range, [@]>", Builtin.slice_subslice; parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I, @Clause2_Output>}::index_mut<'_, @, core::ops::range::Range, [@]>", Builtin.slice_subslice; parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I, @Clause2_Output>}::index<'_, @, core::ops::range::RangeTo, [@]>", Builtin.slice_subslice_to; parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I, @Clause2_Output>}::index_mut<'_, @, core::ops::range::RangeTo, [@]>", Builtin.slice_subslice_to; parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I, @Clause2_Output>}::index<'_, @, core::ops::range::RangeFrom, [@]>", Builtin.slice_subslice_from; parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I, @Clause2_Output>}::index_mut<'_, @, core::ops::range::RangeFrom, [@]>", Builtin.slice_subslice_from; - - (* arrays *) + + (* slices: mono *) + parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I>}::index<'_, @, core::ops::range::Range, [@]>", Builtin.slice_subslice; + parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut<'_, @, core::ops::range::Range, [@]>", Builtin.slice_subslice; + parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I>}::index<'_, @, core::ops::range::RangeTo, [@]>", Builtin.slice_subslice_to; + parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut<'_, @, core::ops::range::RangeTo, [@]>", Builtin.slice_subslice_to; + parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I>}::index<'_, @, core::ops::range::RangeFrom, [@]>", Builtin.slice_subslice_from; + parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut<'_, @, core::ops::range::RangeFrom, [@]>", Builtin.slice_subslice_from; + + (* arrays: generics *) parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I, @Clause2_Clause0_Output>}::index<'_, @, core::ops::range::Range, [@], @>", Builtin.array_to_subslice; parse_pattern "core::array::{core::ops::index::IndexMut<[@T; @N], @I, @Clause2_Clause0_Output>}::index_mut<'_, @, core::ops::range::Range, [@], @>", Builtin.array_to_subslice; parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I, @Clause2_Clause0_Output>}::index<'_, @, core::ops::range::RangeTo, [@], @>", Builtin.array_to_subslice_to; @@ -218,13 +228,28 @@ module RustNames = struct parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I, @Clause2_Clause0_Output>}::index<'_, @, core::ops::range::RangeFrom, [@], @>", Builtin.array_to_subslice_from; parse_pattern "core::array::{core::ops::index::IndexMut<[@T; @N], @I, @Clause2_Clause0_Output>}::index_mut<'_, @, core::ops::range::RangeFrom, [@], @>", Builtin.array_to_subslice_from; + (* arrays: mono *) + parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I>}::index<'_, @, core::ops::range::Range, @>", Builtin.array_to_subslice_mono; + parse_pattern "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut<'_, @, core::ops::range::Range, @>", Builtin.array_to_subslice_mono; + parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I>}::index<'_, @, core::ops::range::RangeTo, @>", Builtin.array_to_subslice_to_mono; + parse_pattern "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut<'_, @, core::ops::range::RangeTo, @>", Builtin.array_to_subslice_to_mono; + parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I>}::index<'_, @, core::ops::range::RangeFrom, @>", Builtin.array_to_subslice_from_mono; + parse_pattern "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut<'_, @, core::ops::range::RangeFrom, @>", Builtin.array_to_subslice_from_mono; + (* slices <-> arrays *) parse_pattern "ArrayToSliceShared<'_, @T, @N>", Builtin.array_to_slice; parse_pattern "ArrayToSliceMut<'_, @T, @N>", Builtin.array_to_slice; + + (* slices <-> arrays: generics *) parse_pattern "core::convert::{core::convert::TryInto<@T, @U, @Clause2_Error>}::try_into<&'_ [@T], [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_array; parse_pattern "core::convert::{core::convert::TryInto<@T, @U, @Clause2_Error>}::try_into<&'_ [@T], &'_ [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_ref_array; parse_pattern "core::convert::{core::convert::TryInto<@T, @U, @Clause2_Error>}::try_into<&'_ mut [@T], &'_ mut [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_ref_array; + (* slices <-> arrays: mono *) + parse_pattern "core::convert::{core::convert::TryInto<@T, @U>}::try_into<&'_ [@T], [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_array; + parse_pattern "core::convert::{core::convert::TryInto<@T, @U>}::try_into<&'_ [@T], &'_ [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_ref_array; + parse_pattern "core::convert::{core::convert::TryInto<@T, @U>}::try_into<&'_ mut [@T], &'_ mut [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_ref_array; + (* iterators XXX are any of these used? *) parse_pattern "core::iter::traits::collect::IntoIterator<[@; @]>::into_iter", Builtin.array_into_iter; @@ -1349,13 +1374,40 @@ and debug_trait_clause_mapping env (mapping : (var_id * K.typ) list) = (** Compiling function instantiations into krml application nodes. *) +(* Helper for getting monomorphized generic arguments from a name *) +let try_get_mono_from_name (name : C.name) = + match List.rev name with + | PeMonomorphized generics :: _ -> Some generics + | _ -> None + +(* Only get monomorphized generics for known *Eurydice* builtins *) +let try_get_mono_generics is_known_builtin (env : env) (f : C.fn_ptr) = + if not is_known_builtin then None else + let get_from_fid fid = + let fun_decl = env.get_nth_function fid in + try_get_mono_from_name fun_decl.item_meta.name + in + match f.func with + | FunId (FRegular fid) -> get_from_fid fid + (* Builtins are always generic *) + | FunId (FBuiltin _) -> None + | TraitMethod (_, _, fid) -> get_from_fid fid + (* First step: produce an expression for the un-instantiated function reference, along with all the type information required to build a proper instantiation. The function reference is an expression that is either a reference to a variable in scope (trait methods), or to a top-level qualified name, which encompasses both externally-defined function (builtins), or regular functions. *) let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result * C.trait_ref list = let open RustNames in - let matches p = Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config p f in + let pat = pattern_of_fn_ptr env f in + L.log "Calls" "%sLooking up function: %s" depth (Charon.PrintTypes.fn_ptr_to_string env.format_env f); + L.log "Calls" "%sfn-ptr-pattern: %s" depth (string_of_pattern pat); + let matches (p : Charon.NameMatcher.pattern) = + L.log "Calls" "%smatching against pattern: %s" depth (Charon.NameMatcher.pattern_to_string { Charon.NameMatcher.tgt = TkPattern } p); + let ret = Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config p f in + L.log "Calls" "%smatch result: %b" depth ret; + ret + in let builtin b = let { Builtin.name; typ; n_type_args; cg_args; _ } = b in let ret_type, arg_types = Krml.Helpers.flatten_arrow typ in @@ -1415,13 +1467,26 @@ let fn_ptr_is_opaque env (fn_ptr : C.fn_ptr) = implement the dictionary-passing style. *) let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = let { - C.generics = { types = type_args; const_generics = const_generic_args; trait_refs; _ }; + C.generics; func; _; } = fn_ptr in + (* The function itself, along with information about its *signature*. *) + let f, { ts; arg_types = inputs; ret_type = output; cg_types = cg_inputs; is_known_builtin }, trait_refs_mono = + lookup_fun env depth fn_ptr + in + + let generics = match try_get_mono_generics is_known_builtin env fn_ptr with + | None -> generics + (* Essentially, there might still be (late-bound) region arguments in the original generics + But we don't care about them (the regions), so just ignore them. *) + | Some generics -> generics + in + let { C.types = type_args; const_generics = const_generic_args; trait_refs; _ } = generics in + (* We handle any kind of fn_ptr, whether it's a concrete function call, a concrete trait implementation method call, or an abstract trait method call (e.g. a call to T::f when T is a trait bound in scope). *) @@ -1439,9 +1504,14 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = let type_args, const_generic_args, trait_refs = let generics = match func with - | TraitMethod ({ trait_id = TraitImpl { generics; _ }; _ }, _, _) -> + | TraitMethod ({ trait_id = TraitImpl { generics; id }; _ }, _, _) -> begin L.log "Calls" "%s--> this is a trait method" depth; - generics + let trait_impl = env.get_nth_trait_impl id in + match try_get_mono_from_name trait_impl.item_meta.name with + (* The same applies here: ignoring potential region arguments *) + | Some generics when is_known_builtin -> generics + | _ -> generics + end | _ -> C.empty_generic_args in ( generics.types @ type_args, @@ -1458,10 +1528,6 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = L.log "Calls" "%s--> type_args: %s" depth (String.concat ", " (List.map (Charon.PrintTypes.ty_to_string env.format_env) type_args)); - (* The function itself, along with information about its *signature*. *) - let f, { ts; arg_types = inputs; ret_type = output; cg_types = cg_inputs; is_known_builtin }, trait_refs_mono = - lookup_fun env depth fn_ptr - in L.log "Calls" "%s--> %d inputs: %a" depth (List.length inputs) ptyps inputs; L.log "Calls" "%s--> is_known_builtin?: %b" depth is_known_builtin; L.log "Calls" "%s--> [MONO] trait from mono name: %s\n" depth diff --git a/lib/Builtin.ml b/lib/Builtin.ml index 4988b858..69940450 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -153,6 +153,23 @@ let array_to_subslice = arg_names = [ "a"; "r" ]; } +(* The version of `array_to_subslice` for monomorphic LLBC. + Core changes: there is no assoc-ty for the generics `Self::Output` + Also, its argument is a monomorphized `Range::` instead of a generic one. + The same as below for `array_to_subslice_to` and `array_to_subslice_from`. +*) +let array_to_subslice_mono = + { + name = [ "Eurydice" ], "array_to_subslice_mono"; + typ = + Krml.Helpers.fold_arrow + [ TBuf (TBound 1, false); TQualified ([ "core"; "ops"; "range"; "Range" ], "") ] + (mk_slice (TBound 1)); + n_type_args = 2; + cg_args = [ TInt SizeT ]; + arg_names = [ "a"; "r" ]; + } + let array_to_subslice_to = { name = [ "Eurydice" ], "array_to_subslice_to"; @@ -165,6 +182,19 @@ let array_to_subslice_to = arg_names = [ "a"; "r" ]; } +(* The version of `array_to_subslice_to` for monomorphic LLBC. *) +let array_to_subslice_to_mono = + { + name = [ "Eurydice" ], "array_to_subslice_to_mono"; + typ = + Krml.Helpers.fold_arrow + [ TBuf (TBound 1, false); TQualified ([ "core"; "ops"; "range"; "RangeTo" ], "") ] + (mk_slice (TBound 1)); + n_type_args = 2; + cg_args = [ TInt SizeT ]; + arg_names = [ "a"; "r" ]; + } + let array_to_subslice_from = { name = [ "Eurydice" ], "array_to_subslice_from"; @@ -177,6 +207,19 @@ let array_to_subslice_from = arg_names = [ "a"; "r" ]; } +(* The version of `array_to_subslice_from` for monomorphic LLBC. *) +let array_to_subslice_from_mono = + { + name = [ "Eurydice" ], "array_to_subslice_from_mono"; + typ = + Krml.Helpers.fold_arrow + [ TBuf (TBound 1, false); TQualified ([ "core"; "ops"; "range"; "RangeFrom" ], "") ] + (mk_slice (TBound 1)); + n_type_args = 2; + cg_args = [ TInt SizeT ]; + arg_names = [ "a"; "r" ]; + } + (* These two are placeholders that are inserted by AstOfLlbc with the intent that they should be desugared later on, once monomorphization and data type compilation, respectively, have happened. *) let array_repeat = @@ -304,6 +347,32 @@ let slice_copy = arg_names = [ "s" ]; } +let slice_split_at = + let slice = mk_slice (TBound 0) in + { + name = [ "Eurydice" ], "slice_split_at"; + typ = + Krml.Helpers.fold_arrow + [ slice; TInt SizeT ] + (K.TTuple [ slice; slice ]); + n_type_args = 1; + cg_args = []; + arg_names = [ "s"; "mid" ]; + } + +let slice_split_at_mut = + let slice = mk_slice (TBound 0) in + { + name = [ "Eurydice" ], "slice_split_at_mut"; + typ = + Krml.Helpers.fold_arrow + [ slice; TInt SizeT ] + (K.TTuple [ slice; slice ]); + n_type_args = 1; + cg_args = []; + arg_names = [ "s"; "mid" ]; + } + let slice_index_outparam = { name = [ "Eurydice" ], "slice_index_outparam"; @@ -755,6 +824,9 @@ let builtin_funcs = array_to_subslice; array_to_subslice_to; array_to_subslice_from; + array_to_subslice_mono; + array_to_subslice_to_mono; + array_to_subslice_from_mono; array_repeat; array_into_iter; array_eq; @@ -762,6 +834,8 @@ let builtin_funcs = slice_eq; slice_len; slice_copy; + slice_split_at; + slice_split_at_mut; slice_index; slice_index_outparam; slice_subslice; diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 2da3e6ff..f604a974 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -1076,8 +1076,8 @@ let bonus_cleanups = match lid with | [ "core"; "slice"; s ], "len" when is_slice_t s -> true, ([ "Eurydice" ], "slice_len"), Builtin.slice_len.typ | [ "core"; "slice"; s ], "copy_from_slice" when is_slice_t s -> true, ([ "Eurydice" ], "slice_copy"), Builtin.slice_copy.typ - | [ "core"; "slice"; s ], "split_at" when is_slice_t s -> true, ([ "Eurydice" ], "slice_split_at"), TAny (*todo*) - | [ "core"; "slice"; s ], "split_at_mut" when is_slice_t s -> true, ([ "Eurydice" ], "slice_split_at_mut"), TAny + | [ "core"; "slice"; s ], "split_at" when is_slice_t s -> true, ([ "Eurydice" ], "slice_split_at"), Builtin.slice_split_at.typ + | [ "core"; "slice"; s ], "split_at_mut" when is_slice_t s -> true, ([ "Eurydice" ], "slice_split_at_mut"), Builtin.slice_split_at_mut.typ | _ -> false, lid, TAny in let e' = AstOfLlbc.re_polymorphize e in diff --git a/out/test-array2d/array2d.h b/out/test-array2d/array2d.h index 9cbd6376..87dedc39 100644 --- a/out/test-array2d/array2d.h +++ b/out/test-array2d/array2d.h @@ -15,19 +15,23 @@ extern "C" { #endif -extern bool core_cmp_impls__core__cmp__PartialEq_u32__for_u32__eq(uint32_t *x0, uint32_t *x1); - -extern bool core_cmp_impls__core__cmp__PartialEq_u32__for_u32__ne(uint32_t *x0, uint32_t *x1); +extern bool +core_array_equality__core__cmp__PartialEq____Array__Array_u32__2usize___4usize____Array__Array_u32__2usize___4usize____eq___Array_u32__2usize____Array_u32__2usize___4usize_( + uint32_t (*x0)[2U], + uint32_t (*x1)[2U] +); bool array2d_f(uint32_t x[4U][2U]); -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 +void array2d_main(void); -typedef uint8_t core_panicking_AssertKind; +extern bool +core_array_equality__core__cmp__PartialEq____Array_u32__2usize____Array_u32__2usize____eq__u32__u32__2usize_( + uint32_t *x0, + uint32_t *x1 +); -void array2d_main(void); +extern bool core_cmp_impls__core__cmp__PartialEq___u32__u32___eq(uint32_t *x0, uint32_t *x1); #if defined(__cplusplus) } diff --git a/out/test-closure_fn_cast/closure_fn_cast.c b/out/test-closure_fn_cast/closure_fn_cast.c index afed83cf..841cdbc2 100644 --- a/out/test-closure_fn_cast/closure_fn_cast.c +++ b/out/test-closure_fn_cast/closure_fn_cast.c @@ -8,37 +8,37 @@ #include "closure_fn_cast.h" /** -This function found in impl {core::ops::function::Fn<(i32), i32> for closure_fn_cast::main::closure} +This function found in impl {core::ops::function::Fn::} */ -int32_t closure_fn_cast_main_call_fd(void **_, int32_t tupled_args) +int32_t closure_fn_cast_main_call_58(void **_, int32_t tupled_args) { int32_t x = tupled_args; return x + (int32_t)42; } /** -This function found in impl {core::ops::function::FnMut<(i32), i32> for closure_fn_cast::main::closure} +This function found in impl {core::ops::function::FnMut::} */ -int32_t closure_fn_cast_main_call_mut_68(void **state, int32_t args) +int32_t closure_fn_cast_main_call_mut_2c(void **state, int32_t args) { - return closure_fn_cast_main_call_fd(state, args); + return closure_fn_cast_main_call_58(state, args); } /** -This function found in impl {core::ops::function::FnOnce<(i32), i32> for closure_fn_cast::main::closure} +This function found in impl {core::ops::function::FnOnce::} */ -int32_t closure_fn_cast_main_call_once_fd(int32_t _) +int32_t closure_fn_cast_main_call_once_ef(int32_t _) { /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - return closure_fn_cast_main_call_mut_68(&lvalue, _); + return closure_fn_cast_main_call_mut_2c(&lvalue, _); } int32_t closure_fn_cast_main_closure_as_fn(int32_t arg1) { int32_t args = arg1; void *state = (void *)0U; - return closure_fn_cast_main_call_once_fd(args); + return closure_fn_cast_main_call_once_ef(args); } void closure_fn_cast_main(void) diff --git a/out/test-closure_fn_cast/closure_fn_cast.h b/out/test-closure_fn_cast/closure_fn_cast.h index 12076dca..0d6a75d2 100644 --- a/out/test-closure_fn_cast/closure_fn_cast.h +++ b/out/test-closure_fn_cast/closure_fn_cast.h @@ -16,19 +16,19 @@ extern "C" { #endif /** -This function found in impl {core::ops::function::Fn<(i32), i32> for closure_fn_cast::main::closure} +This function found in impl {core::ops::function::Fn::} */ -int32_t closure_fn_cast_main_call_fd(void **_, int32_t tupled_args); +int32_t closure_fn_cast_main_call_58(void **_, int32_t tupled_args); /** -This function found in impl {core::ops::function::FnMut<(i32), i32> for closure_fn_cast::main::closure} +This function found in impl {core::ops::function::FnMut::} */ -int32_t closure_fn_cast_main_call_mut_68(void **state, int32_t args); +int32_t closure_fn_cast_main_call_mut_2c(void **state, int32_t args); /** -This function found in impl {core::ops::function::FnOnce<(i32), i32> for closure_fn_cast::main::closure} +This function found in impl {core::ops::function::FnOnce::} */ -int32_t closure_fn_cast_main_call_once_fd(int32_t _); +int32_t closure_fn_cast_main_call_once_ef(int32_t _); int32_t closure_fn_cast_main_closure_as_fn(int32_t arg1); diff --git a/out/test-const_generics/Eurydice.h b/out/test-const_generics/Eurydice.h index cb39bcb7..92605815 100644 --- a/out/test-const_generics/Eurydice.h +++ b/out/test-const_generics/Eurydice.h @@ -15,19 +15,9 @@ extern "C" { #endif -/** -A monomorphic instance of core.ops.range.RangeTo -with types size_t +typedef size_t core_ops_range_RangeTo__usize_; -*/ -typedef size_t core_ops_range_RangeTo_08; - -/** -A monomorphic instance of core.ops.range.RangeFrom -with types size_t - -*/ -typedef size_t core_ops_range_RangeFrom_08; +typedef size_t core_ops_range_RangeFrom__usize_; #if defined(__cplusplus) } diff --git a/out/test-const_generics/const_generics.c b/out/test-const_generics/const_generics.c index 907464ed..d538731f 100644 --- a/out/test-const_generics/const_generics.c +++ b/out/test-const_generics/const_generics.c @@ -9,33 +9,28 @@ #include "Eurydice.h" -/** -A monomorphic instance of const_generics.serialize -with const generics -- OUT_LEN= 8 -*/ -void const_generics_serialize_3b(Eurydice_slice re, uint8_t ret[8U]) +void const_generics_serialize__8usize_(Eurydice_slice re, uint8_t ret[8U]) { uint8_t out[8U] = { 0U }; Eurydice_slice uu____0 = - Eurydice_array_to_subslice_to((size_t)8U, + Eurydice_array_to_subslice_to_mono((size_t)8U, out, (size_t)4U, uint8_t, size_t, - uint8_t []); + Eurydice_slice); uint8_t ret0[4U]; core_num__u32__to_be_bytes(Eurydice_slice_index(re, (size_t)0U, uint32_t, uint32_t *), ret0); Eurydice_slice_copy(uu____0, Eurydice_array_to_slice((size_t)4U, ret0, uint8_t), uint8_t); Eurydice_slice uu____1 = - Eurydice_array_to_subslice_from((size_t)8U, + Eurydice_array_to_subslice_from_mono((size_t)8U, out, (size_t)4U, uint8_t, size_t, - uint8_t []); + Eurydice_slice); uint8_t ret1[4U]; core_num__u32__to_be_bytes(Eurydice_slice_index(re, (size_t)1U, uint32_t, uint32_t *), ret1); Eurydice_slice_copy(uu____1, Eurydice_array_to_slice((size_t)4U, ret1, uint8_t), uint8_t); @@ -46,19 +41,13 @@ void const_generics_main(void) { uint8_t s[8U]; uint32_t buf[2U] = { 1U, 2U }; - const_generics_serialize_3b(Eurydice_array_to_slice((size_t)2U, buf, uint32_t), s); + const_generics_serialize__8usize_(Eurydice_array_to_slice((size_t)2U, buf, uint32_t), s); EURYDICE_ASSERT(s[3U] == 1U, "panic!"); EURYDICE_ASSERT(s[7U] == 2U, "panic!"); } -/** -A monomorphic instance of const_generics.mk_pairs -with types uint32_t, uint64_t -with const generics -- N= 2 -- M= 4 -*/ -const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y) +const_generics_Pair__u32__u32__2usize__2usize_ +const_generics_mk_pairs__u32__u64__2usize__4usize_(uint32_t x, uint64_t y) { uint32_t a1[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, a1[i] = x;); @@ -70,7 +59,7 @@ const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y) /* Passing arrays by value in Rust generates a copy in C */ uint64_t copy_of_a20[4U]; memcpy(copy_of_a20, a2, (size_t)4U * sizeof (uint64_t)); - const_generics_Pair_a5 p1; + const_generics_Pair__u32__u64__2usize__4usize_ p1; memcpy(p1.left, copy_of_a10, (size_t)2U * sizeof (uint32_t)); memcpy(p1.right, copy_of_a20, (size_t)4U * sizeof (uint64_t)); /* Passing arrays by value in Rust generates a copy in C */ @@ -79,14 +68,14 @@ const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y) /* Passing arrays by value in Rust generates a copy in C */ uint32_t copy_of_a1[2U]; memcpy(copy_of_a1, a1, (size_t)2U * sizeof (uint32_t)); - const_generics_Pair_87 p2; + const_generics_Pair__u64__u32__4usize__2usize_ p2; memcpy(p2.left, copy_of_a2, (size_t)4U * sizeof (uint64_t)); memcpy(p2.right, copy_of_a1, (size_t)2U * sizeof (uint32_t)); uint32_t uu____4[2U]; memcpy(uu____4, p1.left, (size_t)2U * sizeof (uint32_t)); uint32_t uu____5[2U]; memcpy(uu____5, p2.right, (size_t)2U * sizeof (uint32_t)); - const_generics_Pair_4e lit; + const_generics_Pair__u32__u32__2usize__2usize_ lit; memcpy(lit.left, uu____4, (size_t)2U * sizeof (uint32_t)); memcpy(lit.right, uu____5, (size_t)2U * sizeof (uint32_t)); return lit; @@ -101,7 +90,8 @@ _uint32_t__x2; void const_generics_main1(void) { - const_generics_Pair_4e uu____0 = const_generics_mk_pairs_e0(0U, 0ULL); + const_generics_Pair__u32__u32__2usize__2usize_ + uu____0 = const_generics_mk_pairs__u32__u64__2usize__4usize_(0U, 0ULL); uint32_t left[2U]; memcpy(left, uu____0.left, (size_t)2U * sizeof (uint32_t)); uint32_t right[2U]; @@ -117,13 +107,7 @@ void const_generics_main1(void) EURYDICE_ASSERT(uu____4.fst[0U] == uu____4.snd[0U], "panic!"); } -/** -A monomorphic instance of const_generics.f -with const generics -- FOO= 1 -- BAR= 2 -*/ -bool const_generics_f_e5(uint32_t x, size_t y) +bool const_generics_f__1usize__2u32_(uint32_t x, size_t y) { uint32_t arr1[1U]; { @@ -145,13 +129,7 @@ bool const_generics_f_e5(uint32_t x, size_t y) return uu____0; } -/** -A monomorphic instance of const_generics.f -with const generics -- FOO= 3 -- BAR= 4 -*/ -bool const_generics_f_70(uint32_t x, size_t y) +bool const_generics_f__3usize__4u32_(uint32_t x, size_t y) { uint32_t arr1[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, arr1[i] = x;); @@ -169,16 +147,10 @@ bool const_generics_f_70(uint32_t x, size_t y) return uu____0; } -/** -A monomorphic instance of const_generics.g -with const generics -- BAR= 3 -- FOO= 4 -*/ -bool const_generics_g_70(uint32_t x, size_t y) +bool const_generics_g__3usize__4u32_(uint32_t x, size_t y) { bool uu____0; - if (const_generics_f_70(x, y)) + if (const_generics_f__3usize__4u32_(x, y)) { if (x == 4U) { @@ -206,9 +178,9 @@ _bool__x2; void const_generics_main3(void) { bool x; - if (const_generics_f_e5(0U, (size_t)0U)) + if (const_generics_f__1usize__2u32_(0U, (size_t)0U)) { - x = const_generics_g_70(0U, (size_t)0U); + x = const_generics_g__3usize__4u32_(0U, (size_t)0U); } else { diff --git a/out/test-const_generics/const_generics.h b/out/test-const_generics/const_generics.h index 54340c09..8e988627 100644 --- a/out/test-const_generics/const_generics.h +++ b/out/test-const_generics/const_generics.h @@ -17,105 +17,190 @@ extern "C" { static inline void core_num__u32__to_be_bytes(uint32_t x0, uint8_t x1[4U]); -/** -A monomorphic instance of const_generics.serialize -with const generics -- OUT_LEN= 8 -*/ -void const_generics_serialize_3b(Eurydice_slice re, uint8_t ret[8U]); +extern void core_slice___Slice_u8___copy_from_slice__u8_(Eurydice_slice x0, Eurydice_slice x1); -void const_generics_main(void); - -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 +void const_generics_serialize__8usize_(Eurydice_slice re, uint8_t ret[8U]); -typedef uint8_t core_panicking_AssertKind; +void const_generics_main(void); -/** -A monomorphic instance of const_generics.Pair -with types uint32_t, uint32_t -with const generics -- $2size_t -- $2size_t -*/ -typedef struct const_generics_Pair_4e_s +typedef struct const_generics_Pair__u32__u32__2usize__2usize__s { uint32_t left[2U]; uint32_t right[2U]; } -const_generics_Pair_4e; - -/** -A monomorphic instance of const_generics.Pair -with types uint32_t, uint64_t -with const generics -- $2size_t -- $4size_t -*/ -typedef struct const_generics_Pair_a5_s +const_generics_Pair__u32__u32__2usize__2usize_; + +typedef struct const_generics_Pair__u32__u64__2usize__4usize__s { uint32_t left[2U]; uint64_t right[4U]; } -const_generics_Pair_a5; - -/** -A monomorphic instance of const_generics.Pair -with types uint64_t, uint32_t -with const generics -- $4size_t -- $2size_t -*/ -typedef struct const_generics_Pair_87_s +const_generics_Pair__u32__u64__2usize__4usize_; + +typedef struct const_generics_Pair__u64__u32__4usize__2usize__s { uint64_t left[4U]; uint32_t right[2U]; } -const_generics_Pair_87; +const_generics_Pair__u64__u32__4usize__2usize_; -/** -A monomorphic instance of const_generics.mk_pairs -with types uint32_t, uint64_t -with const generics -- N= 2 -- M= 4 -*/ -const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y); +const_generics_Pair__u32__u32__2usize__2usize_ +const_generics_mk_pairs__u32__u64__2usize__4usize_(uint32_t x, uint64_t y); void const_generics_main1(void); -/** -A monomorphic instance of const_generics.f -with const generics -- FOO= 1 -- BAR= 2 -*/ -bool const_generics_f_e5(uint32_t x, size_t y); - -/** -A monomorphic instance of const_generics.f -with const generics -- FOO= 3 -- BAR= 4 -*/ -bool const_generics_f_70(uint32_t x, size_t y); - -/** -A monomorphic instance of const_generics.g -with const generics -- BAR= 3 -- FOO= 4 -*/ -bool const_generics_g_70(uint32_t x, size_t y); +bool const_generics_f__1usize__2u32_(uint32_t x, size_t y); + +bool const_generics_f__3usize__4u32_(uint32_t x, size_t y); + +bool const_generics_g__3usize__4u32_(uint32_t x, size_t y); void const_generics_main3(void); -extern uint32_t core_clone_impls__core__clone__Clone_for_u32__clone(uint32_t *x0); +extern Eurydice_slice +core_array__core__ops__index__Index____Array_u8__8usize___core__ops__range__RangeFrom___usize____index__u8__core__ops__range__RangeFrom___usize___8usize_( + uint8_t *x0, + size_t x1 +); + +extern Eurydice_slice +core_array__core__ops__index__Index____Array_u8__8usize___core__ops__range__RangeTo___usize____index__u8__core__ops__range__RangeTo___usize___8usize_( + uint8_t *x0, + size_t x1 +); + +extern Eurydice_slice +core_array__core__ops__index__IndexMut____Array_u8__8usize___core__ops__range__RangeFrom___usize____index_mut__u8__core__ops__range__RangeFrom___usize___8usize_( + uint8_t *x0, + size_t x1 +); + +extern Eurydice_slice +core_array__core__ops__index__IndexMut____Array_u8__8usize___core__ops__range__RangeTo___usize____index_mut__u8__core__ops__range__RangeTo___usize___8usize_( + uint8_t *x0, + size_t x1 +); -extern uint64_t core_clone_impls__core__clone__Clone_for_u64__clone(uint64_t *x0); +extern uint32_t core_clone_impls__core__clone__Clone___u32___clone(uint32_t *x0); -extern uint8_t core_clone_impls__core__clone__Clone_for_u8__clone(uint8_t *x0); +extern uint64_t core_clone_impls__core__clone__Clone___u64___clone(uint64_t *x0); + +extern uint8_t core_clone_impls__core__clone__Clone___u8___clone(uint8_t *x0); + +#define core_option_Option_None 0 +#define core_option_Option_Some 1 + +typedef uint8_t core_option_Option________Slice_u8____tags; + +typedef struct core_option_Option________Slice_u8____s +{ + core_option_Option________Slice_u8____tags tag; + Eurydice_slice f0; +} +core_option_Option________Slice_u8___; + +typedef struct core_option_Option______mut___Slice_u8____s +{ + core_option_Option________Slice_u8____tags tag; + Eurydice_slice f0; +} +core_option_Option______mut___Slice_u8___; + +extern Eurydice_slice +core_slice_index__core__ops__index__Index____Slice_u8___core__ops__range__RangeFrom___usize____index__u8__core__ops__range__RangeFrom___usize__( + Eurydice_slice x0, + size_t x1 +); + +extern Eurydice_slice +core_slice_index__core__ops__index__Index____Slice_u8___core__ops__range__RangeTo___usize____index__u8__core__ops__range__RangeTo___usize__( + Eurydice_slice x0, + size_t x1 +); + +extern Eurydice_slice +core_slice_index__core__ops__index__IndexMut____Slice_u8___core__ops__range__RangeFrom___usize____index_mut__u8__core__ops__range__RangeFrom___usize__( + Eurydice_slice x0, + size_t x1 +); + +extern Eurydice_slice +core_slice_index__core__ops__index__IndexMut____Slice_u8___core__ops__range__RangeTo___usize____index_mut__u8__core__ops__range__RangeTo___usize__( + Eurydice_slice x0, + size_t x1 +); + +extern core_option_Option________Slice_u8___ +core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____get__u8_( + size_t x0, + Eurydice_slice x1 +); + +extern core_option_Option______mut___Slice_u8___ +core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____get_mut__u8_( + size_t x0, + Eurydice_slice x1 +); + +extern uint8_t +(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____get_unchecked__u8_( + size_t x0, + uint8_t (*x1)[] +))[]; + +extern uint8_t +(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____get_unchecked_mut__u8_( + size_t x0, + uint8_t (*x1)[] +))[]; + +extern Eurydice_slice +core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____index__u8_( + size_t x0, + Eurydice_slice x1 +); + +extern Eurydice_slice +core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____index_mut__u8_( + size_t x0, + Eurydice_slice x1 +); + +extern core_option_Option________Slice_u8___ +core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____get__u8_( + size_t x0, + Eurydice_slice x1 +); + +extern core_option_Option______mut___Slice_u8___ +core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____get_mut__u8_( + size_t x0, + Eurydice_slice x1 +); + +extern uint8_t +(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____get_unchecked__u8_( + size_t x0, + uint8_t (*x1)[] +))[]; + +extern uint8_t +(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____get_unchecked_mut__u8_( + size_t x0, + uint8_t (*x1)[] +))[]; + +extern Eurydice_slice +core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____index__u8_( + size_t x0, + Eurydice_slice x1 +); + +extern Eurydice_slice +core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____index_mut__u8_( + size_t x0, + Eurydice_slice x1 +); #if defined(__cplusplus) } From 7fb38dffcb03b1363046ded6f76ed2617f14320c Mon Sep 17 00:00:00 2001 From: ssyram Date: Fri, 26 Sep 2025 19:25:35 +0800 Subject: [PATCH 15/20] mono debug: fixed partial_eq --- include/eurydice_glue.h | 1 + out/test-floating_points/floating_points.h | 6 +- out/test-fn_cast/fn_cast.c | 20 +--- out/test-fn_cast/fn_cast.h | 20 +--- out/test-fn_higher_order/Eurydice.h | 9 +- out/test-fn_higher_order/fn_higher_order.c | 117 +++++++++++---------- out/test-fn_higher_order/fn_higher_order.h | 113 ++++++++------------ out/test-global_ref/global_ref.c | 2 +- out/test-global_ref/global_ref.h | 8 +- out/test-issue_102/issue_102.h | 10 -- out/test-issue_104/issue_104.c | 12 +-- out/test-issue_104/issue_104.h | 16 +-- out/test-issue_107/issue_107.c | 4 +- out/test-issue_107/issue_107.h | 4 +- out/test-issue_k630/issue_k630.h | 6 -- out/test-names/names.h | 28 ----- out/test-nested_arrays/Eurydice.h | 9 +- out/test-nested_arrays/nested_arrays.c | 70 ++++++++++-- out/test-nested_arrays/nested_arrays.h | 72 ++++++------- out/test-partial_eq/partial_eq.c | 17 +-- out/test-partial_eq/partial_eq.h | 36 ++++--- out/test-raw_pointers/raw_pointers.h | 6 -- out/test-reborrow/reborrow.h | 9 +- out/test-slice_array/slice_array.h | 12 +-- test/partial_eq_stubs.c | 17 ++- 25 files changed, 273 insertions(+), 351 deletions(-) diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index 29f1e53d..4067e60c 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -538,6 +538,7 @@ typedef const char *Prims_string; // This is temporary. Ultimately we want to be able to extract all of this. typedef void *core_fmt_Formatter; +typedef void *core_fmt_Formatter_____; #define core_fmt_rt__core__fmt__rt__Argument__a___new_display(x1, x2, x3, x4) \ NULL diff --git a/out/test-floating_points/floating_points.h b/out/test-floating_points/floating_points.h index 0e132f8d..538434bc 100644 --- a/out/test-floating_points/floating_points.h +++ b/out/test-floating_points/floating_points.h @@ -15,11 +15,9 @@ extern "C" { #endif -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 +extern size_t core_slice___Slice_f32___len__f32_(Eurydice_slice x0); -typedef uint8_t core_panicking_AssertKind; +extern size_t core_slice___Slice_f64___len__f64_(Eurydice_slice x0); void floating_points_main(void); diff --git a/out/test-fn_cast/fn_cast.c b/out/test-fn_cast/fn_cast.c index ae2e0a3f..d0ae5c30 100644 --- a/out/test-fn_cast/fn_cast.c +++ b/out/test-fn_cast/fn_cast.c @@ -7,24 +7,14 @@ #include "fn_cast.h" -/** -A monomorphic instance of fn_cast.applies -with types int32_t, int32_t - -*/ -int32_t *fn_cast_applies_99(int32_t *(*f)(int32_t *x0), int32_t *arg) +int32_t *fn_cast_id_ref__i32_(int32_t *x) { - return f(arg); + return x; } -/** -A monomorphic instance of fn_cast.id_ref -with types int32_t - -*/ -int32_t *fn_cast_id_ref_a8(int32_t *x) +int32_t *fn_cast_applies__i32__i32_(int32_t *(*f)(int32_t *x0), int32_t *arg) { - return x; + return f(arg); } typedef struct _int32_t__x2_s @@ -43,7 +33,7 @@ void fn_cast_main(void) _int32_t__x2 uu____0 = { - .fst = fn_cast_applies_99((int32_t *(*)(int32_t *x0))fn_cast_id_ref_a8, &lvalue0), + .fst = fn_cast_applies__i32__i32_((int32_t *(*)(int32_t *x0))fn_cast_id_ref__i32_, &lvalue0), .snd = &lvalue }; EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!"); diff --git a/out/test-fn_cast/fn_cast.h b/out/test-fn_cast/fn_cast.h index 1c279f13..610c6375 100644 --- a/out/test-fn_cast/fn_cast.h +++ b/out/test-fn_cast/fn_cast.h @@ -15,25 +15,9 @@ extern "C" { #endif -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 +int32_t *fn_cast_id_ref__i32_(int32_t *x); -typedef uint8_t core_panicking_AssertKind; - -/** -A monomorphic instance of fn_cast.applies -with types int32_t, int32_t - -*/ -int32_t *fn_cast_applies_99(int32_t *(*f)(int32_t *x0), int32_t *arg); - -/** -A monomorphic instance of fn_cast.id_ref -with types int32_t - -*/ -int32_t *fn_cast_id_ref_a8(int32_t *x); +int32_t *fn_cast_applies__i32__i32_(int32_t *(*f)(int32_t *x0), int32_t *arg); void fn_cast_main(void); diff --git a/out/test-fn_higher_order/Eurydice.h b/out/test-fn_higher_order/Eurydice.h index f3e8dae8..0dfb23bd 100644 --- a/out/test-fn_higher_order/Eurydice.h +++ b/out/test-fn_higher_order/Eurydice.h @@ -15,17 +15,12 @@ extern "C" { #endif -/** -A monomorphic instance of core.ops.range.Range -with types size_t - -*/ -typedef struct core_ops_range_Range_08_s +typedef struct core_ops_range_Range__usize__s { size_t start; size_t end; } -core_ops_range_Range_08; +core_ops_range_Range__usize_; #if defined(__cplusplus) } diff --git a/out/test-fn_higher_order/fn_higher_order.c b/out/test-fn_higher_order/fn_higher_order.c index 49b0febc..e2ee3263 100644 --- a/out/test-fn_higher_order/fn_higher_order.c +++ b/out/test-fn_higher_order/fn_higher_order.c @@ -7,31 +7,46 @@ #include "fn_higher_order.h" +#include "Eurydice.h" + int32_t fn_higher_order_empty_ptr(int32_t (*f)(void)) { return f(); } -int32_t fn_higher_order_more_sum_lst(int32_t *l) +size_t fn_higher_order_sum_lst__5usize_(size_t *lst) { - int32_t sum = (int32_t)0; - KRML_MAYBE_FOR3(i, - (size_t)0U, - (size_t)3U, - (size_t)1U, - size_t i0 = i; - sum = sum + l[i0];); - return sum; + size_t sum = (size_t)0U; + core_ops_range_Range__usize_ + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__(( + KRML_CLITERAL(core_ops_range_Range__usize_){ .start = (size_t)0U, .end = (size_t)5U } + )); + while (true) + { + core_option_Option__usize_ + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(&iter); + if (uu____0.tag == core_option_Option_None) + { + break; + } + else + { + size_t i = uu____0.f0; + sum = sum + lst[i]; + } + } + return sum + (size_t)5U; +} + +size_t fn_higher_order_id__usize_(size_t r) +{ + return r; } -/** -A monomorphic instance of fn_higher_order.compose_cg_apply -with types size_t, size_t, size_t -with const generics -- N= 5 -*/ size_t -fn_higher_order_compose_cg_apply_fd( +fn_higher_order_compose_cg_apply__usize__usize__usize__5usize_( size_t (*f)(size_t *x0), size_t (*g)(size_t x0), size_t *arg @@ -41,41 +56,39 @@ fn_higher_order_compose_cg_apply_fd( return uu____0(f(arg)); } -/** -A monomorphic instance of fn_higher_order.sum_lst -with const generics -- N= 5 -*/ -size_t fn_higher_order_sum_lst_c9(size_t *lst) +int32_t fn_higher_order_more_sum_lst(int32_t *l) { - size_t sum = (size_t)0U; - KRML_MAYBE_FOR5(i, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t i0 = i; - sum = sum + lst[i0];); - return sum + (size_t)5U; + int32_t sum = (int32_t)0; + core_ops_range_Range__usize_ + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__(( + KRML_CLITERAL(core_ops_range_Range__usize_){ .start = (size_t)0U, .end = (size_t)3U } + )); + while (true) + { + core_option_Option__usize_ + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(&iter); + if (uu____0.tag == core_option_Option_None) + { + break; + } + else + { + size_t i = uu____0.f0; + sum = sum + l[i]; + } + } + return sum; } -/** -A monomorphic instance of fn_higher_order.id -with types size_t - -*/ -size_t fn_higher_order_id_37(size_t r) +int32_t fn_higher_order_id__i32_(int32_t r) { return r; } -/** -A monomorphic instance of fn_higher_order.compose_cg_apply -with types int32_t, int32_t, int32_t -with const generics -- N= 3 -*/ int32_t -fn_higher_order_compose_cg_apply_82( +fn_higher_order_compose_cg_apply__i32__i32__i32__3usize_( int32_t (*f)(int32_t *x0), int32_t (*g)(int32_t x0), int32_t *arg @@ -85,16 +98,6 @@ fn_higher_order_compose_cg_apply_82( return uu____0(f(arg)); } -/** -A monomorphic instance of fn_higher_order.id -with types int32_t - -*/ -int32_t fn_higher_order_id_a8(int32_t r) -{ - return r; -} - typedef struct _size_t__x2_s { size_t *fst; @@ -114,14 +117,14 @@ void fn_higher_order_use_compose_cg(void) size_t buf0[5U] = { (size_t)1U, (size_t)2U, (size_t)3U, (size_t)4U, (size_t)5U }; size_t x = - fn_higher_order_compose_cg_apply_fd(fn_higher_order_sum_lst_c9, - fn_higher_order_id_37, + fn_higher_order_compose_cg_apply__usize__usize__usize__5usize_(fn_higher_order_sum_lst__5usize_, + fn_higher_order_id__usize_, buf0); int32_t buf[3U] = { (int32_t)10, (int32_t)11, (int32_t)12 }; int32_t y = - fn_higher_order_compose_cg_apply_82(fn_higher_order_more_sum_lst, - fn_higher_order_id_a8, + fn_higher_order_compose_cg_apply__i32__i32__i32__3usize_(fn_higher_order_more_sum_lst, + fn_higher_order_id__i32_, buf); /* original Rust expression is not an lvalue in C */ size_t lvalue = (size_t)20U; diff --git a/out/test-fn_higher_order/fn_higher_order.h b/out/test-fn_higher_order/fn_higher_order.h index 1ffd62a7..5d586587 100644 --- a/out/test-fn_higher_order/fn_higher_order.h +++ b/out/test-fn_higher_order/fn_higher_order.h @@ -15,9 +15,11 @@ extern "C" { #endif -extern int32_t core_clone_impls__core__clone__Clone_for_i32__clone(int32_t *x0); +#include "Eurydice.h" -extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0); +extern int32_t core_clone_impls__core__clone__Clone___i32___clone(int32_t *x0); + +extern size_t core_clone_impls__core__clone__Clone___usize___clone(size_t *x0); #define core_cmp_Ordering_Less -1 #define core_cmp_Ordering_Equal 0 @@ -25,118 +27,85 @@ extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0); typedef int8_t core_cmp_Ordering; -extern bool core_cmp_impls__core__cmp__PartialEq_usize__for_usize__eq(size_t *x0, size_t *x1); - -#define core_option_None 0 -#define core_option_Some 1 +extern bool core_cmp_impls__core__cmp__PartialEq___usize__usize___eq(size_t *x0, size_t *x1); -typedef uint8_t core_option_Option_77_tags; +#define core_option_Option_None 0 +#define core_option_Option_Some 1 -/** -A monomorphic instance of core.option.Option -with types core_cmp_Ordering +typedef uint8_t core_option_Option__core__cmp__Ordering__tags; -*/ -typedef struct core_option_Option_77_s +typedef struct core_option_Option__core__cmp__Ordering__s { - core_option_Option_77_tags tag; + core_option_Option__core__cmp__Ordering__tags tag; core_cmp_Ordering f0; } -core_option_Option_77; +core_option_Option__core__cmp__Ordering_; -extern core_option_Option_77 -core_cmp_impls__core__cmp__PartialOrd_usize__for_usize__partial_cmp(size_t *x0, size_t *x1); +extern core_option_Option__core__cmp__Ordering_ +core_cmp_impls__core__cmp__PartialOrd___usize__usize___partial_cmp(size_t *x0, size_t *x1); -/** -A monomorphic instance of core.option.Option -with types size_t - -*/ -typedef struct core_option_Option_08_s +typedef struct core_option_Option__usize__s { - core_option_Option_77_tags tag; + core_option_Option__core__cmp__Ordering__tags tag; size_t f0; } -core_option_Option_08; +core_option_Option__usize_; -extern core_option_Option_08 -core_iter_range__core__iter__range__Step_for_usize__backward_checked(size_t x0, size_t x1); +extern core_option_Option__usize_ +core_iter_range__core__iter__range__Step___usize___backward_checked(size_t x0, size_t x1); -extern core_option_Option_08 -core_iter_range__core__iter__range__Step_for_usize__forward_checked(size_t x0, size_t x1); +extern core_option_Option__usize_ +core_iter_range__core__iter__range__Step___usize___forward_checked(size_t x0, size_t x1); /** A monomorphic instance of K. -with types size_t, core_option_Option size_t +with types size_t, core_option_Option_ */ -typedef struct tuple_04_s +typedef struct tuple_f6_s { size_t fst; - core_option_Option_08 snd; + core_option_Option__usize_ snd; } -tuple_04; +tuple_f6; -extern tuple_04 -core_iter_range__core__iter__range__Step_for_usize__steps_between(size_t *x0, size_t *x1); +extern tuple_f6 +core_iter_range__core__iter__range__Step___usize___steps_between(size_t *x0, size_t *x1); -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 +extern core_option_Option__usize_ +core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_( + core_ops_range_Range__usize_ *x0 +); -typedef uint8_t core_panicking_AssertKind; +extern core_ops_range_Range__usize_ +core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__( + core_ops_range_Range__usize_ x0 +); int32_t fn_higher_order_empty_ptr(int32_t (*f)(void)); -int32_t fn_higher_order_more_sum_lst(int32_t *l); +size_t fn_higher_order_sum_lst__5usize_(size_t *lst); + +size_t fn_higher_order_id__usize_(size_t r); -/** -A monomorphic instance of fn_higher_order.compose_cg_apply -with types size_t, size_t, size_t -with const generics -- N= 5 -*/ size_t -fn_higher_order_compose_cg_apply_fd( +fn_higher_order_compose_cg_apply__usize__usize__usize__5usize_( size_t (*f)(size_t *x0), size_t (*g)(size_t x0), size_t *arg ); -/** -A monomorphic instance of fn_higher_order.sum_lst -with const generics -- N= 5 -*/ -size_t fn_higher_order_sum_lst_c9(size_t *lst); - -/** -A monomorphic instance of fn_higher_order.id -with types size_t +int32_t fn_higher_order_more_sum_lst(int32_t *l); -*/ -size_t fn_higher_order_id_37(size_t r); +int32_t fn_higher_order_id__i32_(int32_t r); -/** -A monomorphic instance of fn_higher_order.compose_cg_apply -with types int32_t, int32_t, int32_t -with const generics -- N= 3 -*/ int32_t -fn_higher_order_compose_cg_apply_82( +fn_higher_order_compose_cg_apply__i32__i32__i32__3usize_( int32_t (*f)(int32_t *x0), int32_t (*g)(int32_t x0), int32_t *arg ); -/** -A monomorphic instance of fn_higher_order.id -with types int32_t - -*/ -int32_t fn_higher_order_id_a8(int32_t r); - void fn_higher_order_use_compose_cg(void); void fn_higher_order_main(void); diff --git a/out/test-global_ref/global_ref.c b/out/test-global_ref/global_ref.c index cb475eed..f15ae788 100644 --- a/out/test-global_ref/global_ref.c +++ b/out/test-global_ref/global_ref.c @@ -33,7 +33,7 @@ void global_ref_main(void) /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; _____x2 uu____0 = { .fst = GLOBAL_REF_C_VAL[0U][0U], .snd = &lvalue }; - EURYDICE_ASSERT(core_cmp_impls__core__cmp__PartialEq_____for_____eq(uu____0.fst, uu____0.snd), + EURYDICE_ASSERT(core_cmp_impls__core__cmp__PartialEq____________eq(uu____0.fst, uu____0.snd), "panic!"); EURYDICE_ASSERT(global_ref_S_VAL[0U][0U][0U] == (int32_t)0, "panic!"); } diff --git a/out/test-global_ref/global_ref.h b/out/test-global_ref/global_ref.h index bf8ca97b..501819b5 100644 --- a/out/test-global_ref/global_ref.h +++ b/out/test-global_ref/global_ref.h @@ -15,13 +15,7 @@ extern "C" { #endif -extern bool core_cmp_impls__core__cmp__PartialEq_____for_____eq(void **x0, void **x1); - -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 - -typedef uint8_t core_panicking_AssertKind; +extern bool core_cmp_impls__core__cmp__PartialEq____________eq(void **x0, void **x1); extern void ***global_ref_C_VAL_local_2; diff --git a/out/test-issue_102/issue_102.h b/out/test-issue_102/issue_102.h index 7dbe6da1..865afbc3 100644 --- a/out/test-issue_102/issue_102.h +++ b/out/test-issue_102/issue_102.h @@ -15,16 +15,6 @@ extern "C" { #endif -#define issue_102_Error1_Reason1 1 -#define issue_102_Error1_Reason2 2 - -typedef uint8_t issue_102_Error1; - -#define issue_102_Error2_Reason1 3 -#define issue_102_Error2_Reason2 4 - -typedef uint8_t issue_102_Error2; - void issue_102_main(void); #if defined(__cplusplus) diff --git a/out/test-issue_104/issue_104.c b/out/test-issue_104/issue_104.c index e8d321ed..61921ae3 100644 --- a/out/test-issue_104/issue_104.c +++ b/out/test-issue_104/issue_104.c @@ -7,20 +7,14 @@ #include "issue_104.h" -/** -A monomorphic instance of issue_104.sth -with types issue_104_S -with const generics - -*/ -uint8_t issue_104_sth_50(void) +uint8_t issue_104_sth__issue_104__S_(void) { - return ISSUE_104__ISSUE_104__FUN_FOR_ISSUE_104__S__VAL; + return ISSUE_104__ISSUE_104__FUN___ISSUE_104__S___VAL; } uint8_t issue_104_call(void) { - return issue_104_sth_50(); + return issue_104_sth__issue_104__S_(); } typedef struct _uint8_t__x2_s diff --git a/out/test-issue_104/issue_104.h b/out/test-issue_104/issue_104.h index f3f507c5..37fcedf9 100644 --- a/out/test-issue_104/issue_104.h +++ b/out/test-issue_104/issue_104.h @@ -15,21 +15,9 @@ extern "C" { #endif -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 +#define ISSUE_104__ISSUE_104__FUN___ISSUE_104__S___VAL (5U) -typedef uint8_t core_panicking_AssertKind; - -#define ISSUE_104__ISSUE_104__FUN_FOR_ISSUE_104__S__VAL (5U) - -/** -A monomorphic instance of issue_104.sth -with types issue_104_S -with const generics - -*/ -uint8_t issue_104_sth_50(void); +uint8_t issue_104_sth__issue_104__S_(void); uint8_t issue_104_call(void); diff --git a/out/test-issue_107/issue_107.c b/out/test-issue_107/issue_107.c index 995bd6a4..66580d2c 100644 --- a/out/test-issue_107/issue_107.c +++ b/out/test-issue_107/issue_107.c @@ -13,9 +13,9 @@ void issue_107_main(void) } /** -This function found in impl {issue_107::Fun for issue_107::MyStruct} +This function found in impl {issue_107::Fun::} */ -uint8_t issue_107_f_90(void) +uint8_t issue_107_f_4d(void) { return 5U; } diff --git a/out/test-issue_107/issue_107.h b/out/test-issue_107/issue_107.h index 49930ae1..59d118fa 100644 --- a/out/test-issue_107/issue_107.h +++ b/out/test-issue_107/issue_107.h @@ -18,9 +18,9 @@ extern "C" { void issue_107_main(void); /** -This function found in impl {issue_107::Fun for issue_107::MyStruct} +This function found in impl {issue_107::Fun::} */ -uint8_t issue_107_f_90(void); +uint8_t issue_107_f_4d(void); #if defined(__cplusplus) } diff --git a/out/test-issue_k630/issue_k630.h b/out/test-issue_k630/issue_k630.h index ede2728a..d4b8062a 100644 --- a/out/test-issue_k630/issue_k630.h +++ b/out/test-issue_k630/issue_k630.h @@ -15,12 +15,6 @@ extern "C" { #endif -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 - -typedef uint8_t core_panicking_AssertKind; - void issue_k630_main(void); #if defined(__cplusplus) diff --git a/out/test-names/names.h b/out/test-names/names.h index 90c30b17..f902265a 100644 --- a/out/test-names/names.h +++ b/out/test-names/names.h @@ -15,34 +15,6 @@ extern "C" { #endif -#define names_Foo 0 -#define names_Bar 1 - -typedef uint8_t names_Baz_tags; - -typedef struct names_Baz_s -{ - names_Baz_tags tag; - union { - struct - { - uint32_t f0; - uint32_t f1; - } - case_Foo; - uint32_t case_Bar; - } - val; -} -names_Baz; - -typedef struct names_Foo0_s -{ - uint32_t x; - uint32_t y; -} -names_Foo0; - void names_main(void); #if defined(__cplusplus) diff --git a/out/test-nested_arrays/Eurydice.h b/out/test-nested_arrays/Eurydice.h index f3e8dae8..0dfb23bd 100644 --- a/out/test-nested_arrays/Eurydice.h +++ b/out/test-nested_arrays/Eurydice.h @@ -15,17 +15,12 @@ extern "C" { #endif -/** -A monomorphic instance of core.ops.range.Range -with types size_t - -*/ -typedef struct core_ops_range_Range_08_s +typedef struct core_ops_range_Range__usize__s { size_t start; size_t end; } -core_ops_range_Range_08; +core_ops_range_Range__usize_; #if defined(__cplusplus) } diff --git a/out/test-nested_arrays/nested_arrays.c b/out/test-nested_arrays/nested_arrays.c index e063c17c..cf002bd3 100644 --- a/out/test-nested_arrays/nested_arrays.c +++ b/out/test-nested_arrays/nested_arrays.c @@ -7,6 +7,8 @@ #include "nested_arrays.h" +#include "Eurydice.h" + const uint32_t nested_arrays_ZERO[8U] = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U }; typedef struct _uint32_t__x2_s @@ -28,19 +30,67 @@ void nested_arrays_main(void) } memcpy(keys[i0], repeat_expression, (size_t)3U * sizeof (uint32_t [8U])); } - for (size_t i0 = (size_t)0U; i0 < (size_t)3U; i0++) + core_ops_range_Range__usize_ + iter0 = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__(( + KRML_CLITERAL(core_ops_range_Range__usize_){ .start = (size_t)0U, .end = (size_t)3U } + )); + while (true) { - size_t i1 = i0; - for (size_t i2 = (size_t)0U; i2 < (size_t)3U; i2++) + core_option_Option__usize_ + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(&iter0); + if (uu____0.tag == core_option_Option_None) + { + break; + } + else { - size_t j = i2; - for (size_t i = (size_t)0U; i < (size_t)8U; i++) + size_t i = uu____0.f0; + core_ops_range_Range__usize_ + iter1 = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__(( + KRML_CLITERAL(core_ops_range_Range__usize_){ .start = (size_t)0U, .end = (size_t)3U } + )); + while (true) { - size_t k = i; - uint32_t actual = keys[i1][j][k]; - uint32_t expected = (uint32_t)k; - _uint32_t__x2 uu____0 = { .fst = &actual, .snd = &expected }; - EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!"); + core_option_Option__usize_ + uu____1 = + core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(&iter1); + if (uu____1.tag == core_option_Option_None) + { + break; + } + else + { + size_t j = uu____1.f0; + core_ops_range_Range__usize_ + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__(( + KRML_CLITERAL(core_ops_range_Range__usize_){ + .start = (size_t)0U, + .end = (size_t)8U + } + )); + while (true) + { + core_option_Option__usize_ + uu____2 = + core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(&iter); + if (uu____2.tag == core_option_Option_None) + { + break; + } + else + { + size_t k = uu____2.f0; + uint32_t actual = keys[i][j][k]; + uint32_t expected = (uint32_t)k; + _uint32_t__x2 uu____3 = { .fst = &actual, .snd = &expected }; + EURYDICE_ASSERT(uu____3.fst[0U] == uu____3.snd[0U], "panic!"); + } + } + } } } } diff --git a/out/test-nested_arrays/nested_arrays.h b/out/test-nested_arrays/nested_arrays.h index c12cd3ee..1db95a69 100644 --- a/out/test-nested_arrays/nested_arrays.h +++ b/out/test-nested_arrays/nested_arrays.h @@ -15,7 +15,9 @@ extern "C" { #endif -extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0); +#include "Eurydice.h" + +extern size_t core_clone_impls__core__clone__Clone___usize___clone(size_t *x0); #define core_cmp_Ordering_Less -1 #define core_cmp_Ordering_Equal 0 @@ -23,68 +25,60 @@ extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0); typedef int8_t core_cmp_Ordering; -extern bool core_cmp_impls__core__cmp__PartialEq_usize__for_usize__eq(size_t *x0, size_t *x1); - -#define core_option_None 0 -#define core_option_Some 1 +extern bool core_cmp_impls__core__cmp__PartialEq___usize__usize___eq(size_t *x0, size_t *x1); -typedef uint8_t core_option_Option_77_tags; +#define core_option_Option_None 0 +#define core_option_Option_Some 1 -/** -A monomorphic instance of core.option.Option -with types core_cmp_Ordering +typedef uint8_t core_option_Option__core__cmp__Ordering__tags; -*/ -typedef struct core_option_Option_77_s +typedef struct core_option_Option__core__cmp__Ordering__s { - core_option_Option_77_tags tag; + core_option_Option__core__cmp__Ordering__tags tag; core_cmp_Ordering f0; } -core_option_Option_77; +core_option_Option__core__cmp__Ordering_; -extern core_option_Option_77 -core_cmp_impls__core__cmp__PartialOrd_usize__for_usize__partial_cmp(size_t *x0, size_t *x1); +extern core_option_Option__core__cmp__Ordering_ +core_cmp_impls__core__cmp__PartialOrd___usize__usize___partial_cmp(size_t *x0, size_t *x1); -/** -A monomorphic instance of core.option.Option -with types size_t - -*/ -typedef struct core_option_Option_08_s +typedef struct core_option_Option__usize__s { - core_option_Option_77_tags tag; + core_option_Option__core__cmp__Ordering__tags tag; size_t f0; } -core_option_Option_08; +core_option_Option__usize_; -extern core_option_Option_08 -core_iter_range__core__iter__range__Step_for_usize__backward_checked(size_t x0, size_t x1); +extern core_option_Option__usize_ +core_iter_range__core__iter__range__Step___usize___backward_checked(size_t x0, size_t x1); -extern core_option_Option_08 -core_iter_range__core__iter__range__Step_for_usize__forward_checked(size_t x0, size_t x1); +extern core_option_Option__usize_ +core_iter_range__core__iter__range__Step___usize___forward_checked(size_t x0, size_t x1); /** A monomorphic instance of K. -with types size_t, core_option_Option size_t +with types size_t, core_option_Option_ */ -typedef struct tuple_04_s +typedef struct tuple_f6_s { size_t fst; - core_option_Option_08 snd; + core_option_Option__usize_ snd; } -tuple_04; - -extern tuple_04 -core_iter_range__core__iter__range__Step_for_usize__steps_between(size_t *x0, size_t *x1); +tuple_f6; -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 +extern tuple_f6 +core_iter_range__core__iter__range__Step___usize___steps_between(size_t *x0, size_t *x1); -typedef uint8_t core_panicking_AssertKind; +extern core_option_Option__usize_ +core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_( + core_ops_range_Range__usize_ *x0 +); -typedef uint32_t nested_arrays_Key[8U]; +extern core_ops_range_Range__usize_ +core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__( + core_ops_range_Range__usize_ x0 +); extern const uint32_t nested_arrays_ZERO[8U]; diff --git a/out/test-partial_eq/partial_eq.c b/out/test-partial_eq/partial_eq.c index 615ac176..3f6f5183 100644 --- a/out/test-partial_eq/partial_eq.c +++ b/out/test-partial_eq/partial_eq.c @@ -10,9 +10,9 @@ #include "Eurydice.h" /** -This function found in impl {core::cmp::PartialEq for partial_eq::Enum} +This function found in impl {core::cmp::PartialEq::} */ -inline bool partial_eq_eq_31(partial_eq_Enum *self, partial_eq_Enum *other) +inline bool partial_eq_eq_aa(partial_eq_Enum *self, partial_eq_Enum *other) { return true; } @@ -35,22 +35,25 @@ void partial_eq_main(void) { partial_eq_Enum expected = partial_eq_Enum_A; _partial_eq_Enum__x2 uu____0 = { .fst = &expected, .snd = &expected }; - EURYDICE_ASSERT(partial_eq_eq_31(uu____0.fst, uu____0.snd), "panic!"); + EURYDICE_ASSERT(partial_eq_eq_aa(uu____0.fst, uu____0.snd), "panic!"); /* original Rust expression is not an lvalue in C */ partial_eq_Enum *lvalue0 = &expected; /* original Rust expression is not an lvalue in C */ partial_eq_Enum *lvalue = &expected; __partial_eq_Enum___x2 uu____1 = { .fst = &lvalue0, .snd = &lvalue }; - EURYDICE_ASSERT(partial_eq_eq_31(uu____1.fst[0U], uu____1.snd[0U]), "panic!"); + EURYDICE_ASSERT(core_cmp_impls__core__cmp__PartialEq________partial_eq__Enum________partial_eq__Enum____eq__________partial_eq__Enum__partial_eq__Enum_(uu____1.fst, + uu____1.snd), + "panic!"); } /** -This function found in impl {core::fmt::Debug for partial_eq::Enum} +This function found in impl {core::fmt::Debug::} */ -inline core_result_Result_10 partial_eq_fmt_29(partial_eq_Enum *self, core_fmt_Formatter *f) +inline core_result_Result______core__fmt__Error_ +partial_eq_fmt_af(partial_eq_Enum *self, core_fmt_Formatter_____ *f) { return - core_fmt__core__fmt__Formatter__a___write_str(f, + core_fmt__core__fmt__Formatter________write_str_____(f, (KRML_CLITERAL(Eurydice_str){ .data = "A", .len = (size_t)1U })); } diff --git a/out/test-partial_eq/partial_eq.h b/out/test-partial_eq/partial_eq.h index f34e0071..143879c3 100644 --- a/out/test-partial_eq/partial_eq.h +++ b/out/test-partial_eq/partial_eq.h @@ -17,35 +17,39 @@ extern "C" { #include "Eurydice.h" -#define core_result_Ok 0 -#define core_result_Err 1 +#define partial_eq_Enum_A 0 -typedef uint8_t core_result_Result_10; +typedef uint8_t partial_eq_Enum; -extern core_result_Result_10 -core_fmt__core__fmt__Formatter__a___write_str(core_fmt_Formatter *x0, Eurydice_str x1); +extern bool +core_cmp_impls__core__cmp__PartialEq________partial_eq__Enum________partial_eq__Enum____eq__________partial_eq__Enum__partial_eq__Enum_( + partial_eq_Enum **x0, + partial_eq_Enum **x1 +); -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 +#define core_result_Result_Ok 0 +#define core_result_Result_Err 1 -typedef uint8_t core_panicking_AssertKind; +typedef uint8_t core_result_Result______core__fmt__Error_; -#define partial_eq_Enum_A 0 - -typedef uint8_t partial_eq_Enum; +extern core_result_Result______core__fmt__Error_ +core_fmt__core__fmt__Formatter________write_str_____( + core_fmt_Formatter_____ *x0, + Eurydice_str x1 +); /** -This function found in impl {core::cmp::PartialEq for partial_eq::Enum} +This function found in impl {core::cmp::PartialEq::} */ -bool partial_eq_eq_31(partial_eq_Enum *self, partial_eq_Enum *other); +bool partial_eq_eq_aa(partial_eq_Enum *self, partial_eq_Enum *other); void partial_eq_main(void); /** -This function found in impl {core::fmt::Debug for partial_eq::Enum} +This function found in impl {core::fmt::Debug::} */ -core_result_Result_10 partial_eq_fmt_29(partial_eq_Enum *self, core_fmt_Formatter *f); +core_result_Result______core__fmt__Error_ +partial_eq_fmt_af(partial_eq_Enum *self, core_fmt_Formatter_____ *f); #if defined(__cplusplus) } diff --git a/out/test-raw_pointers/raw_pointers.h b/out/test-raw_pointers/raw_pointers.h index c15e7ea3..3c2c87a1 100644 --- a/out/test-raw_pointers/raw_pointers.h +++ b/out/test-raw_pointers/raw_pointers.h @@ -15,12 +15,6 @@ extern "C" { #endif -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 - -typedef uint8_t core_panicking_AssertKind; - void raw_pointers_main(void); #if defined(__cplusplus) diff --git a/out/test-reborrow/reborrow.h b/out/test-reborrow/reborrow.h index 60d6dd9c..8bdcf9f8 100644 --- a/out/test-reborrow/reborrow.h +++ b/out/test-reborrow/reborrow.h @@ -15,11 +15,10 @@ extern "C" { #endif -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 - -typedef uint8_t core_panicking_AssertKind; +extern void +alloc_boxed__core__ops__drop__Drop___alloc__boxed__Box_u8__core__marker__MetaSized___u8___core__marker__Sized___alloc__alloc__Global_____drop__u8__alloc__alloc__Global_( + uint8_t **x0 +); void reborrow_main(void); diff --git a/out/test-slice_array/slice_array.h b/out/test-slice_array/slice_array.h index 38667573..5d92f0ca 100644 --- a/out/test-slice_array/slice_array.h +++ b/out/test-slice_array/slice_array.h @@ -15,12 +15,6 @@ extern "C" { #endif -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 - -typedef uint8_t core_panicking_AssertKind; - typedef struct Eurydice_slice_uint8_t_4size_t__x2_s { Eurydice_slice fst; @@ -28,6 +22,12 @@ typedef struct Eurydice_slice_uint8_t_4size_t__x2_s } Eurydice_slice_uint8_t_4size_t__x2; +extern Eurydice_slice_uint8_t_4size_t__x2 +core_slice___Slice__Array_u8__4usize____split_at_mut___Array_u8__4usize__( + Eurydice_slice x0, + size_t x1 +); + void slice_array_f1(void); void slice_array_f2(void); diff --git a/test/partial_eq_stubs.c b/test/partial_eq_stubs.c index f4cb168c..1a1b3619 100644 --- a/test/partial_eq_stubs.c +++ b/test/partial_eq_stubs.c @@ -1,6 +1,17 @@ #include "partial_eq.h" -extern core_result_Result_10 -core_fmt__core__fmt__Formatter__a___write_str(core_fmt_Formatter *x0, Eurydice_str x1) { - return core_result_Ok; +extern core_result_Result______core__fmt__Error_ +core_fmt__core__fmt__Formatter________write_str_____( + core_fmt_Formatter_____ *x0, + Eurydice_str x1 +) { + return core_result_Result_Ok; +} + +extern bool +core_cmp_impls__core__cmp__PartialEq________partial_eq__Enum________partial_eq__Enum____eq__________partial_eq__Enum__partial_eq__Enum_( + partial_eq_Enum **x0, + partial_eq_Enum **x1 +) { + return partial_eq_eq_aa(*x0, *x1); } From b4c41e8b1a1adb8a550dd03ab2927e1290f218aa Mon Sep 17 00:00:00 2001 From: ssyram Date: Fri, 26 Sep 2025 19:36:25 +0800 Subject: [PATCH 16/20] mono debug: fixed where_clauses_closures --- Makefile | 2 + lib/Cleanup2.ml | 2 +- out/test-trait_generics/trait_generics.c | 29 ++-- out/test-trait_generics/trait_generics.h | 22 ++- out/test-traits/Eurydice.h | 9 +- out/test-traits/traits.c | 22 +-- out/test-traits/traits.h | 75 +++++++++- out/test-traits2/traits2.c | 2 - out/test-traits2/traits2.h | 65 --------- out/test-traits3/traits3.c | 24 ++-- out/test-traits3/traits3.h | 28 ++-- .../where_clauses_closures.c | 84 +++++------ .../where_clauses_closures.h | 65 ++++----- .../where_clauses_simple.c | 134 ++++++------------ .../where_clauses_simple.h | 108 ++++---------- test/where_clauses_from_fn.c | 5 + 16 files changed, 260 insertions(+), 416 deletions(-) create mode 100644 test/where_clauses_from_fn.c diff --git a/Makefile b/Makefile index 610ea038..3ec1acb9 100644 --- a/Makefile +++ b/Makefile @@ -69,6 +69,8 @@ test/println.llbc: CHARON_EXTRA = \ --include=core::fmt::Arguments --include=core::fmt::rt::*::new_const \ --include=core::fmt::rt::Argument +# test-where_clauses_closures: CHARON_EXTRA = \ +# --include=core::convert::* test-partial_eq: EXTRA_C = ../../test/partial_eq_stubs.c test-nested_arrays: EXTRA = -funroll-loops 0 test-array: EXTRA = -fcomments diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index f604a974..32dbcdd3 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -491,7 +491,7 @@ let remove_trivial_into = method! visit_EApp env e es = let e = self#visit_expr_w () e in let es = List.map (self#visit_expr env) es in - match e.node, es with + match (AstOfLlbc.re_polymorphize e).node, es with | ( ETApp ({ node = EQualified ([ "core"; "convert"; _ ], "into"); _ }, [], _, [ t1; t2 ]), [ e1 ] ) when t1 = t2 -> e1.node diff --git a/out/test-trait_generics/trait_generics.c b/out/test-trait_generics/trait_generics.c index ea179f83..78a2ed26 100644 --- a/out/test-trait_generics/trait_generics.c +++ b/out/test-trait_generics/trait_generics.c @@ -8,31 +8,28 @@ #include "trait_generics.h" /** -This function found in impl {trait_generics::MyFnOnce for trait_generics::Foo} +This function found in impl {trait_generics::MyFnOnce::>} */ -/** -A monomorphic instance of trait_generics.call_once_a3 -with const generics -- K= 10 -*/ -uint32_t trait_generics_call_once_a3_95(void) +uint32_t trait_generics_call_once__10usize__29(void) { return 0U; } -/** -A monomorphic instance of trait_generics.from_fn -with types trait_generics_Foo[[$10size_t]] -with const generics - -*/ -void trait_generics_from_fn_3c(void) +void trait_generics_from_fn__trait_generics__Foo___10usize__(void) { - trait_generics_call_once_a3_95(); + trait_generics_call_once__10usize__29(); } void trait_generics_main(void) { - trait_generics_from_fn_3c(); + trait_generics_from_fn__trait_generics__Foo___10usize__(); +} + +/** +This function found in impl {core::ops::drop::Drop::>} +*/ +void trait_generics_Foo_drop__10usize__5e(void **_) +{ + } diff --git a/out/test-trait_generics/trait_generics.h b/out/test-trait_generics/trait_generics.h index ef4b5b53..11b48d92 100644 --- a/out/test-trait_generics/trait_generics.h +++ b/out/test-trait_generics/trait_generics.h @@ -16,25 +16,19 @@ extern "C" { #endif /** -This function found in impl {trait_generics::MyFnOnce for trait_generics::Foo} +This function found in impl {trait_generics::MyFnOnce::>} */ -/** -A monomorphic instance of trait_generics.call_once_a3 -with const generics -- K= 10 -*/ -uint32_t trait_generics_call_once_a3_95(void); - -/** -A monomorphic instance of trait_generics.from_fn -with types trait_generics_Foo[[$10size_t]] -with const generics +uint32_t trait_generics_call_once__10usize__29(void); -*/ -void trait_generics_from_fn_3c(void); +void trait_generics_from_fn__trait_generics__Foo___10usize__(void); void trait_generics_main(void); +/** +This function found in impl {core::ops::drop::Drop::>} +*/ +void trait_generics_Foo_drop__10usize__5e(void **_); + #if defined(__cplusplus) } #endif diff --git a/out/test-traits/Eurydice.h b/out/test-traits/Eurydice.h index f3e8dae8..0dfb23bd 100644 --- a/out/test-traits/Eurydice.h +++ b/out/test-traits/Eurydice.h @@ -15,17 +15,12 @@ extern "C" { #endif -/** -A monomorphic instance of core.ops.range.Range -with types size_t - -*/ -typedef struct core_ops_range_Range_08_s +typedef struct core_ops_range_Range__usize__s { size_t start; size_t end; } -core_ops_range_Range_08; +core_ops_range_Range__usize_; #if defined(__cplusplus) } diff --git a/out/test-traits/traits.c b/out/test-traits/traits.c index cd8b6315..d7ee9860 100644 --- a/out/test-traits/traits.c +++ b/out/test-traits/traits.c @@ -10,9 +10,9 @@ #include "Eurydice.h" /** -This function found in impl {traits::ToInt for traits::Foo} +This function found in impl {traits::ToInt::} */ -uint32_t traits_to_int_ac(traits_Foo *self) +uint32_t traits_to_int_32(traits_Foo *self) { switch (self[0U]) { @@ -34,16 +34,16 @@ uint32_t traits_to_int_ac(traits_Foo *self) } /** -This function found in impl {traits::ToInt for &0 (@Slice)} +This function found in impl {traits::ToInt::<&'_ (@Slice)>} */ -uint32_t traits_to_int_88(Eurydice_slice *self) +uint32_t traits_to_int______95(Eurydice_slice *self) { uint32_t uu____0 = - traits_to_int_ac(&Eurydice_slice_index(self[0U], (size_t)0U, traits_Foo, traits_Foo *)); + traits_to_int_32(&Eurydice_slice_index(self[0U], (size_t)0U, traits_Foo, traits_Foo *)); return uu____0 * - traits_to_int_ac(&Eurydice_slice_index(self[0U], (size_t)1U, traits_Foo, traits_Foo *)); + traits_to_int_32(&Eurydice_slice_index(self[0U], (size_t)1U, traits_Foo, traits_Foo *)); } void traits_main(void) @@ -51,8 +51,14 @@ void traits_main(void) traits_Foo foos[2U] = { traits_Foo_Foo1, traits_Foo_Foo2 }; /* original Rust expression is not an lvalue in C */ Eurydice_slice - lvalue = Eurydice_array_to_subslice3(foos, (size_t)0U, (size_t)2U, traits_Foo *); - if (!(traits_to_int_88(&lvalue) != 2U)) + lvalue = + Eurydice_array_to_subslice_mono((size_t)2U, + foos, + (KRML_CLITERAL(core_ops_range_Range__usize_){ .start = (size_t)0U, .end = (size_t)2U }), + traits_Foo, + core_ops_range_Range__usize_, + Eurydice_slice); + if (!(traits_to_int______95(&lvalue) != 2U)) { return; } diff --git a/out/test-traits/traits.h b/out/test-traits/traits.h index 7bba5518..05146dd7 100644 --- a/out/test-traits/traits.h +++ b/out/test-traits/traits.h @@ -22,15 +22,82 @@ extern "C" { typedef uint8_t traits_Foo; +extern Eurydice_slice +core_array__core__ops__index__Index____Array_traits__Foo__2usize___core__ops__range__Range___usize____index__traits__Foo__core__ops__range__Range___usize___2usize_( + traits_Foo *x0, + core_ops_range_Range__usize_ x1 +); + +#define core_option_Option_None 0 +#define core_option_Option_Some 1 + +typedef uint8_t core_option_Option________Slice_traits__Foo____tags; + +typedef struct core_option_Option________Slice_traits__Foo____s +{ + core_option_Option________Slice_traits__Foo____tags tag; + Eurydice_slice f0; +} +core_option_Option________Slice_traits__Foo___; + +typedef struct core_option_Option______mut___Slice_traits__Foo____s +{ + core_option_Option________Slice_traits__Foo____tags tag; + Eurydice_slice f0; +} +core_option_Option______mut___Slice_traits__Foo___; + +extern Eurydice_slice +core_slice_index__core__ops__index__Index____Slice_traits__Foo___core__ops__range__Range___usize____index__traits__Foo__core__ops__range__Range___usize__( + Eurydice_slice x0, + core_ops_range_Range__usize_ x1 +); + +extern core_option_Option________Slice_traits__Foo___ +core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____get__traits__Foo_( + core_ops_range_Range__usize_ x0, + Eurydice_slice x1 +); + +extern core_option_Option______mut___Slice_traits__Foo___ +core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____get_mut__traits__Foo_( + core_ops_range_Range__usize_ x0, + Eurydice_slice x1 +); + +extern traits_Foo +(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____get_unchecked__traits__Foo_( + core_ops_range_Range__usize_ x0, + traits_Foo (*x1)[] +))[]; + +extern traits_Foo +(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____get_unchecked_mut__traits__Foo_( + core_ops_range_Range__usize_ x0, + traits_Foo (*x1)[] +))[]; + +extern Eurydice_slice +core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____index__traits__Foo_( + core_ops_range_Range__usize_ x0, + Eurydice_slice x1 +); + +extern Eurydice_slice +core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____index_mut__traits__Foo_( + core_ops_range_Range__usize_ x0, + Eurydice_slice x1 +); + /** -This function found in impl {traits::ToInt for traits::Foo} +This function found in impl {traits::ToInt::} */ -uint32_t traits_to_int_ac(traits_Foo *self); +uint32_t traits_to_int_32(traits_Foo *self); /** -This function found in impl {traits::ToInt for &0 (@Slice)} +This function found in impl {traits::ToInt::<&'_ (@Slice)>} */ -uint32_t traits_to_int_88(Eurydice_slice *self); +uint32_t traits_to_int______95(Eurydice_slice *self); void traits_main(void); diff --git a/out/test-traits2/traits2.c b/out/test-traits2/traits2.c index 9e42a8e0..6e274866 100644 --- a/out/test-traits2/traits2.c +++ b/out/test-traits2/traits2.c @@ -7,8 +7,6 @@ #include "traits2.h" -#include "Eurydice.h" - void traits2_main(void) { diff --git a/out/test-traits2/traits2.h b/out/test-traits2/traits2.h index 86011594..ade6c128 100644 --- a/out/test-traits2/traits2.h +++ b/out/test-traits2/traits2.h @@ -15,71 +15,6 @@ extern "C" { #endif -#include "Eurydice.h" - -extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0); - -#define core_cmp_Ordering_Less -1 -#define core_cmp_Ordering_Equal 0 -#define core_cmp_Ordering_Greater 1 - -typedef int8_t core_cmp_Ordering; - -extern bool core_cmp_impls__core__cmp__PartialEq_usize__for_usize__eq(size_t *x0, size_t *x1); - -#define core_option_None 0 -#define core_option_Some 1 - -typedef uint8_t core_option_Option_77_tags; - -/** -A monomorphic instance of core.option.Option -with types core_cmp_Ordering - -*/ -typedef struct core_option_Option_77_s -{ - core_option_Option_77_tags tag; - core_cmp_Ordering f0; -} -core_option_Option_77; - -extern core_option_Option_77 -core_cmp_impls__core__cmp__PartialOrd_usize__for_usize__partial_cmp(size_t *x0, size_t *x1); - -/** -A monomorphic instance of core.option.Option -with types size_t - -*/ -typedef struct core_option_Option_08_s -{ - core_option_Option_77_tags tag; - size_t f0; -} -core_option_Option_08; - -extern core_option_Option_08 -core_iter_range__core__iter__range__Step_for_usize__backward_checked(size_t x0, size_t x1); - -extern core_option_Option_08 -core_iter_range__core__iter__range__Step_for_usize__forward_checked(size_t x0, size_t x1); - -/** -A monomorphic instance of K. -with types size_t, core_option_Option size_t - -*/ -typedef struct tuple_04_s -{ - size_t fst; - core_option_Option_08 snd; -} -tuple_04; - -extern tuple_04 -core_iter_range__core__iter__range__Step_for_usize__steps_between(size_t *x0, size_t *x1); - void traits2_main(void); #if defined(__cplusplus) diff --git a/out/test-traits3/traits3.c b/out/test-traits3/traits3.c index 05cc984e..b757e6b7 100644 --- a/out/test-traits3/traits3.c +++ b/out/test-traits3/traits3.c @@ -7,21 +7,7 @@ #include "traits3.h" -/** -This function found in impl {traits3::internal::KeccakItem<2usize> for (u64, u64)} -*/ -uint64_t_x2 traits3_zero_c8(void) -{ - return (KRML_CLITERAL(uint64_t_x2){ .fst = 0ULL, .snd = 0ULL }); -} - -/** -A monomorphic instance of traits3.keccak -with types (uint64_t * uint64_t) -with const generics -- N= 2 -*/ -void traits3_keccak_cc(void) +void traits3_keccak___u64__u64___2usize_(void) { } @@ -36,3 +22,11 @@ void traits3_main(void) } +/** +This function found in impl {traits3::internal::KeccakItem::<(u64, u64), 2usize>} +*/ +traits3_uint64x2_t traits3_zero_ec(void) +{ + return (KRML_CLITERAL(traits3_uint64x2_t){ .fst = 0ULL, .snd = 0ULL }); +} + diff --git a/out/test-traits3/traits3.h b/out/test-traits3/traits3.h index 1ab47318..db03dda4 100644 --- a/out/test-traits3/traits3.h +++ b/out/test-traits3/traits3.h @@ -15,31 +15,23 @@ extern "C" { #endif -typedef struct uint64_t_x2_s +void traits3_keccak___u64__u64___2usize_(void); + +void traits3_keccakx2(void); + +void traits3_main(void); + +typedef struct traits3_uint64x2_t_s { uint64_t fst; uint64_t snd; } -uint64_t_x2; +traits3_uint64x2_t; /** -This function found in impl {traits3::internal::KeccakItem<2usize> for (u64, u64)} +This function found in impl {traits3::internal::KeccakItem::<(u64, u64), 2usize>} */ -uint64_t_x2 traits3_zero_c8(void); - -/** -A monomorphic instance of traits3.keccak -with types (uint64_t * uint64_t) -with const generics -- N= 2 -*/ -void traits3_keccak_cc(void); - -void traits3_keccakx2(void); - -void traits3_main(void); - -typedef uint64_t_x2 traits3_uint64x2_t; +traits3_uint64x2_t traits3_zero_ec(void); #if defined(__cplusplus) } diff --git a/out/test-where_clauses_closures/where_clauses_closures.c b/out/test-where_clauses_closures/where_clauses_closures.c index c028b5e0..30f29be0 100644 --- a/out/test-where_clauses_closures/where_clauses_closures.c +++ b/out/test-where_clauses_closures/where_clauses_closures.c @@ -8,67 +8,22 @@ #include "where_clauses_closures.h" /** -This function found in impl {where_clauses_closures::Ops<1usize> for usize} +This function found in impl {where_clauses_closures::Ops::} */ -size_t where_clauses_closures_zero_38(void) +size_t where_clauses_closures_zero_77(void) { return (size_t)0U; } -/** -This function found in impl {where_clauses_closures::Ops<1usize> for usize} -*/ -size_t where_clauses_closures_of_usize_38(size_t x) -{ - return x; -} - -/** -This function found in impl {core::ops::function::FnMut<(usize), T> for where_clauses_closures::test::closure[TraitClause@0, TraitClause@1, TraitClause@2]} -*/ -/** -A monomorphic instance of where_clauses_closures.test.call_mut_1a -with types size_t -with const generics -- K= 1 -*/ -size_t where_clauses_closures_test_call_mut_1a_e3(void **_, size_t tupled_args) -{ - size_t i = tupled_args; - return where_clauses_closures_of_usize_38(i); -} - -/** -This function found in impl {core::ops::function::FnOnce<(usize), T> for where_clauses_closures::test::closure[TraitClause@0, TraitClause@1, TraitClause@2]} -*/ -/** -A monomorphic instance of where_clauses_closures.test.call_once_79 -with types size_t -with const generics -- K= 1 -*/ -size_t where_clauses_closures_test_call_once_79_e3(size_t _) -{ - /* original Rust expression is not an lvalue in C */ - void *lvalue = (void *)0U; - return where_clauses_closures_test_call_mut_1a_e3(&lvalue, _); -} - -/** -A monomorphic instance of where_clauses_closures.test -with types size_t -with const generics -- K= 1 -*/ -size_t_x2 where_clauses_closures_test_e3(void) +size_t_x2 where_clauses_closures_test__usize__1usize_(void) { size_t x[1U]; { /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - x[0U] = where_clauses_closures_test_call_mut_1a_e3(&lvalue, (size_t)0U); + x[0U] = where_clauses_closures_test_call_mut__usize__1usize__8a(&lvalue, (size_t)0U); } - size_t y = where_clauses_closures_zero_38(); + size_t y = where_clauses_closures_zero_77(); return (KRML_CLITERAL(size_t_x2){ .fst = x[0U], .snd = y }); } @@ -81,10 +36,37 @@ _size_t__x2; void where_clauses_closures_main(void) { - size_t_x2 uu____0 = where_clauses_closures_test_e3(); + size_t_x2 uu____0 = where_clauses_closures_test__usize__1usize_(); size_t x = uu____0.fst; size_t y = uu____0.snd; _size_t__x2 uu____1 = { .fst = &x, .snd = &y }; EURYDICE_ASSERT(uu____1.fst[0U] == uu____1.snd[0U], "panic!"); } +/** +This function found in impl {where_clauses_closures::Ops::} +*/ +size_t where_clauses_closures_of_usize_77(size_t x) +{ + return x; +} + +/** +This function found in impl {core::ops::function::FnMut::, (usize)>} +*/ +size_t where_clauses_closures_test_call_mut__usize__1usize__8a(void **_, size_t tupled_args) +{ + size_t i = tupled_args; + return where_clauses_closures_of_usize_77(i); +} + +/** +This function found in impl {core::ops::function::FnOnce::, (usize)>} +*/ +size_t where_clauses_closures_test_call_once__usize__1usize__c9(size_t _) +{ + /* original Rust expression is not an lvalue in C */ + void *lvalue = (void *)0U; + return where_clauses_closures_test_call_mut__usize__1usize__8a(&lvalue, _); +} + diff --git a/out/test-where_clauses_closures/where_clauses_closures.h b/out/test-where_clauses_closures/where_clauses_closures.h index e698334e..e4610525 100644 --- a/out/test-where_clauses_closures/where_clauses_closures.h +++ b/out/test-where_clauses_closures/where_clauses_closures.h @@ -15,45 +15,23 @@ extern "C" { #endif -extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0); +extern void +core_array_from_fn__usize__where_clauses_closures__test__closure___usize__1usize___1usize_( + size_t x0[1U] +); -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 +extern size_t core_clone_impls__core__clone__Clone___usize___clone(size_t *x0); -typedef uint8_t core_panicking_AssertKind; +static inline size_t +core_convert__core__convert__From___usize__usize___from__usize_(size_t x0); -/** -This function found in impl {where_clauses_closures::Ops<1usize> for usize} -*/ -size_t where_clauses_closures_zero_38(void); +static inline size_t +core_convert__core__convert__Into___usize__usize___into__usize__usize_(size_t x0); /** -This function found in impl {where_clauses_closures::Ops<1usize> for usize} +This function found in impl {where_clauses_closures::Ops::} */ -size_t where_clauses_closures_of_usize_38(size_t x); - -/** -This function found in impl {core::ops::function::FnMut<(usize), T> for where_clauses_closures::test::closure[TraitClause@0, TraitClause@1, TraitClause@2]} -*/ -/** -A monomorphic instance of where_clauses_closures.test.call_mut_1a -with types size_t -with const generics -- K= 1 -*/ -size_t where_clauses_closures_test_call_mut_1a_e3(void **_, size_t tupled_args); - -/** -This function found in impl {core::ops::function::FnOnce<(usize), T> for where_clauses_closures::test::closure[TraitClause@0, TraitClause@1, TraitClause@2]} -*/ -/** -A monomorphic instance of where_clauses_closures.test.call_once_79 -with types size_t -with const generics -- K= 1 -*/ -size_t where_clauses_closures_test_call_once_79_e3(size_t _); +size_t where_clauses_closures_zero_77(void); typedef struct size_t_x2_s { @@ -62,15 +40,24 @@ typedef struct size_t_x2_s } size_t_x2; +size_t_x2 where_clauses_closures_test__usize__1usize_(void); + +void where_clauses_closures_main(void); + /** -A monomorphic instance of where_clauses_closures.test -with types size_t -with const generics -- K= 1 +This function found in impl {where_clauses_closures::Ops::} */ -size_t_x2 where_clauses_closures_test_e3(void); +size_t where_clauses_closures_of_usize_77(size_t x); -void where_clauses_closures_main(void); +/** +This function found in impl {core::ops::function::FnMut::, (usize)>} +*/ +size_t where_clauses_closures_test_call_mut__usize__1usize__8a(void **_, size_t tupled_args); + +/** +This function found in impl {core::ops::function::FnOnce::, (usize)>} +*/ +size_t where_clauses_closures_test_call_once__usize__1usize__c9(size_t _); #if defined(__cplusplus) } diff --git a/out/test-where_clauses_simple/where_clauses_simple.c b/out/test-where_clauses_simple/where_clauses_simple.c index a1cf9193..30ef7304 100644 --- a/out/test-where_clauses_simple/where_clauses_simple.c +++ b/out/test-where_clauses_simple/where_clauses_simple.c @@ -8,42 +8,26 @@ #include "where_clauses_simple.h" /** -This function found in impl {where_clauses_simple::Ops for usize} +This function found in impl {where_clauses_simple::Ops::} */ -/** -A monomorphic instance of where_clauses_simple.of_u16_81 -with const generics -- K= 3 -*/ -size_t where_clauses_simple_of_u16_81_e0(uint16_t x) +size_t where_clauses_simple_of_u16__3usize__ad(uint16_t x) { return (size_t)x; } /** -This function found in impl {where_clauses_simple::Ops for usize} -*/ -/** -A monomorphic instance of where_clauses_simple.add_81 -with const generics -- K= 3 +This function found in impl {where_clauses_simple::Ops::} */ -size_t where_clauses_simple_add_81_e0(uint16_t x[3U], size_t y) +size_t where_clauses_simple_add__3usize__ad(uint16_t x[3U], size_t y) { return (size_t)x[0U] + y + (size_t)3U; } -/** -A monomorphic instance of where_clauses_simple.fn_k -with types size_t -with const generics -- K= 3 -*/ -size_t where_clauses_simple_fn_k_71(void) +size_t where_clauses_simple_fn_k__usize__3usize_(void) { - size_t x = where_clauses_simple_of_u16_81_e0(0U); + size_t x = where_clauses_simple_of_u16__3usize__ad(0U); uint16_t buf[3U] = { 0U }; - return where_clauses_simple_add_81_e0(buf, x); + return where_clauses_simple_add__3usize__ad(buf, x); } typedef struct _size_t__x2_s @@ -55,39 +39,33 @@ _size_t__x2; void where_clauses_simple_k_calls_k(void) { - size_t r = where_clauses_simple_fn_k_71(); + size_t r = where_clauses_simple_fn_k__usize__3usize_(); size_t r_expected = (size_t)3U; _size_t__x2 uu____0 = { .fst = &r, .snd = &r_expected }; EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!"); } /** -This function found in impl {where_clauses_simple::Ops<1usize> for u64} +This function found in impl {where_clauses_simple::Ops::} */ -uint64_t where_clauses_simple_add_19(uint16_t x[1U], uint64_t y) +uint64_t where_clauses_simple_of_u16_70(uint16_t x) { - return (uint64_t)x[0U] + y; + return (uint64_t)x; } /** -This function found in impl {where_clauses_simple::Ops<1usize> for u64} +This function found in impl {where_clauses_simple::Ops::} */ -uint64_t where_clauses_simple_of_u16_19(uint16_t x) +uint64_t where_clauses_simple_add_70(uint16_t x[1U], uint64_t y) { - return (uint64_t)x; + return (uint64_t)x[0U] + y; } -/** -A monomorphic instance of where_clauses_simple.fn_k -with types uint64_t -with const generics -- K= 1 -*/ -uint64_t where_clauses_simple_fn_k_3a(void) +uint64_t where_clauses_simple_fn_k__u64__1usize_(void) { - uint64_t x = where_clauses_simple_of_u16_19(0U); + uint64_t x = where_clauses_simple_of_u16_70(0U); uint16_t buf[1U] = { 0U }; - return where_clauses_simple_add_19(buf, x); + return where_clauses_simple_add_70(buf, x); } typedef struct _uint64_t__x2_s @@ -99,107 +77,75 @@ _uint64_t__x2; void where_clauses_simple_k_calls_one(void) { - uint64_t r = where_clauses_simple_fn_k_3a(); + uint64_t r = where_clauses_simple_fn_k__u64__1usize_(); uint64_t r_expected = 0ULL; _uint64_t__x2 uu____0 = { .fst = &r, .snd = &r_expected }; EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!"); } /** -This function found in impl {where_clauses_simple::Ops for usize} -*/ -/** -A monomorphic instance of where_clauses_simple.of_u16_81 -with const generics -- K= 1 +This function found in impl {where_clauses_simple::Ops::} */ -size_t where_clauses_simple_of_u16_81_74(uint16_t x) +size_t where_clauses_simple_of_u16__1usize__ff(uint16_t x) { return (size_t)x; } /** -This function found in impl {where_clauses_simple::Ops for usize} +This function found in impl {where_clauses_simple::Ops::} */ -/** -A monomorphic instance of where_clauses_simple.add_81 -with const generics -- K= 1 -*/ -size_t where_clauses_simple_add_81_74(uint16_t x[1U], size_t y) +size_t where_clauses_simple_add__1usize__ff(uint16_t x[1U], size_t y) { return (size_t)x[0U] + y + (size_t)1U; } -/** -A monomorphic instance of where_clauses_simple.fn_1 -with types size_t -with const generics - -*/ -size_t where_clauses_simple_fn_1_e6(void) +size_t where_clauses_simple_fn_1__usize_(void) { - size_t x = where_clauses_simple_of_u16_81_74(0U); + size_t x = where_clauses_simple_of_u16__1usize__ff(0U); uint16_t buf[1U] = { 0U }; - return where_clauses_simple_add_81_74(buf, x); + return where_clauses_simple_add__1usize__ff(buf, x); } void where_clauses_simple_one_calls_k(void) { - size_t r = where_clauses_simple_fn_1_e6(); + size_t r = where_clauses_simple_fn_1__usize_(); size_t r_expected = (size_t)1U; _size_t__x2 uu____0 = { .fst = &r, .snd = &r_expected }; EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!"); } -/** -A monomorphic instance of where_clauses_simple.fn_1 -with types uint64_t -with const generics - -*/ -uint64_t where_clauses_simple_fn_1_d7(void) +uint64_t where_clauses_simple_fn_1__u64_(void) { - uint64_t x = where_clauses_simple_of_u16_19(0U); + uint64_t x = where_clauses_simple_of_u16_70(0U); uint16_t buf[1U] = { 0U }; - return where_clauses_simple_add_19(buf, x); + return where_clauses_simple_add_70(buf, x); } void where_clauses_simple_one_calls_one(void) { - uint64_t r = where_clauses_simple_fn_1_d7(); + uint64_t r = where_clauses_simple_fn_1__u64_(); uint64_t r_expected = 0ULL; _uint64_t__x2 uu____0 = { .fst = &r, .snd = &r_expected }; EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!"); } -/** -A monomorphic instance of where_clauses_simple.double -with types uint64_t, size_t -with const generics - -*/ -tuple_65 where_clauses_simple_double_ed(uint64_t x, size_t y) +tuple_65 where_clauses_simple_double__u64__usize_(uint64_t x, size_t y) { uint16_t buf0[1U] = { 0U }; - uint64_t uu____0 = where_clauses_simple_add_19(buf0, x); + uint64_t uu____0 = where_clauses_simple_add_70(buf0, x); uint16_t buf[1U] = { 0U }; return - (KRML_CLITERAL(tuple_65){ .fst = uu____0, .snd = where_clauses_simple_add_81_74(buf, y) }); + ( + KRML_CLITERAL(tuple_65){ .fst = uu____0, .snd = where_clauses_simple_add__1usize__ff(buf, y) } + ); } -/** -A monomorphic instance of where_clauses_simple.double_k -with types size_t, uint64_t -with const generics -- K= 3 -*/ -tuple_b6 where_clauses_simple_double_k_7b(size_t x, uint64_t y) +tuple_b6 where_clauses_simple_double_k__usize__u64__3usize_(size_t x, uint64_t y) { uint16_t buf0[3U] = { 0U }; - size_t uu____0 = where_clauses_simple_add_81_e0(buf0, x); + size_t uu____0 = where_clauses_simple_add__3usize__ad(buf0, x); uint16_t buf[1U] = { 0U }; - return (KRML_CLITERAL(tuple_b6){ .fst = uu____0, .snd = where_clauses_simple_add_19(buf, y) }); + return (KRML_CLITERAL(tuple_b6){ .fst = uu____0, .snd = where_clauses_simple_add_70(buf, y) }); } void where_clauses_simple_main(void) @@ -208,8 +154,8 @@ void where_clauses_simple_main(void) where_clauses_simple_k_calls_one(); where_clauses_simple_one_calls_k(); where_clauses_simple_one_calls_one(); - tuple_65 x = where_clauses_simple_double_ed(1ULL, (size_t)1U); - tuple_b6 y = where_clauses_simple_double_k_7b((size_t)1U, 1ULL); + tuple_65 x = where_clauses_simple_double__u64__usize_(1ULL, (size_t)1U); + tuple_b6 y = where_clauses_simple_double_k__usize__u64__3usize_((size_t)1U, 1ULL); uint64_t x_0 = 1ULL; size_t x_1 = (size_t)2U; _uint64_t__x2 uu____0 = { .fst = &x.fst, .snd = &x_0 }; diff --git a/out/test-where_clauses_simple/where_clauses_simple.h b/out/test-where_clauses_simple/where_clauses_simple.h index b0cfdff5..994f0d57 100644 --- a/out/test-where_clauses_simple/where_clauses_simple.h +++ b/out/test-where_clauses_simple/where_clauses_simple.h @@ -15,107 +15,63 @@ extern "C" { #endif -extern uint64_t core_clone_impls__core__clone__Clone_for_u64__clone(uint64_t *x0); +extern uint64_t core_clone_impls__core__clone__Clone___u64___clone(uint64_t *x0); -extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0); +extern size_t core_clone_impls__core__clone__Clone___usize___clone(size_t *x0); -static inline uint64_t core_convert_num__core__convert__From_u16__for_u64__from(uint16_t x0); +static inline uint64_t core_convert_num__core__convert__From___u64__u16___from(uint16_t x0); -static inline size_t core_convert_num__core__convert__From_u16__for_usize__from(uint16_t x0); +static inline size_t core_convert_num__core__convert__From___usize__u16___from(uint16_t x0); -#define core_panicking_AssertKind_Eq 0 -#define core_panicking_AssertKind_Ne 1 -#define core_panicking_AssertKind_Match 2 +static inline uint64_t +core_convert__core__convert__Into___u16__u64___into__u16__u64_(uint16_t x0); -typedef uint8_t core_panicking_AssertKind; +static inline size_t +core_convert__core__convert__Into___u16__usize___into__u16__usize_(uint16_t x0); /** -This function found in impl {where_clauses_simple::Ops for usize} +This function found in impl {where_clauses_simple::Ops::} */ -/** -A monomorphic instance of where_clauses_simple.of_u16_81 -with const generics -- K= 3 -*/ -size_t where_clauses_simple_of_u16_81_e0(uint16_t x); +size_t where_clauses_simple_of_u16__3usize__ad(uint16_t x); /** -This function found in impl {where_clauses_simple::Ops for usize} -*/ -/** -A monomorphic instance of where_clauses_simple.add_81 -with const generics -- K= 3 +This function found in impl {where_clauses_simple::Ops::} */ -size_t where_clauses_simple_add_81_e0(uint16_t x[3U], size_t y); +size_t where_clauses_simple_add__3usize__ad(uint16_t x[3U], size_t y); -/** -A monomorphic instance of where_clauses_simple.fn_k -with types size_t -with const generics -- K= 3 -*/ -size_t where_clauses_simple_fn_k_71(void); +size_t where_clauses_simple_fn_k__usize__3usize_(void); void where_clauses_simple_k_calls_k(void); /** -This function found in impl {where_clauses_simple::Ops<1usize> for u64} +This function found in impl {where_clauses_simple::Ops::} */ -uint64_t where_clauses_simple_add_19(uint16_t x[1U], uint64_t y); +uint64_t where_clauses_simple_of_u16_70(uint16_t x); /** -This function found in impl {where_clauses_simple::Ops<1usize> for u64} +This function found in impl {where_clauses_simple::Ops::} */ -uint64_t where_clauses_simple_of_u16_19(uint16_t x); +uint64_t where_clauses_simple_add_70(uint16_t x[1U], uint64_t y); -/** -A monomorphic instance of where_clauses_simple.fn_k -with types uint64_t -with const generics -- K= 1 -*/ -uint64_t where_clauses_simple_fn_k_3a(void); +uint64_t where_clauses_simple_fn_k__u64__1usize_(void); void where_clauses_simple_k_calls_one(void); /** -This function found in impl {where_clauses_simple::Ops for usize} -*/ -/** -A monomorphic instance of where_clauses_simple.of_u16_81 -with const generics -- K= 1 +This function found in impl {where_clauses_simple::Ops::} */ -size_t where_clauses_simple_of_u16_81_74(uint16_t x); +size_t where_clauses_simple_of_u16__1usize__ff(uint16_t x); /** -This function found in impl {where_clauses_simple::Ops for usize} +This function found in impl {where_clauses_simple::Ops::} */ -/** -A monomorphic instance of where_clauses_simple.add_81 -with const generics -- K= 1 -*/ -size_t where_clauses_simple_add_81_74(uint16_t x[1U], size_t y); +size_t where_clauses_simple_add__1usize__ff(uint16_t x[1U], size_t y); -/** -A monomorphic instance of where_clauses_simple.fn_1 -with types size_t -with const generics - -*/ -size_t where_clauses_simple_fn_1_e6(void); +size_t where_clauses_simple_fn_1__usize_(void); void where_clauses_simple_one_calls_k(void); -/** -A monomorphic instance of where_clauses_simple.fn_1 -with types uint64_t -with const generics - -*/ -uint64_t where_clauses_simple_fn_1_d7(void); +uint64_t where_clauses_simple_fn_1__u64_(void); void where_clauses_simple_one_calls_one(void); @@ -131,13 +87,7 @@ typedef struct tuple_65_s } tuple_65; -/** -A monomorphic instance of where_clauses_simple.double -with types uint64_t, size_t -with const generics - -*/ -tuple_65 where_clauses_simple_double_ed(uint64_t x, size_t y); +tuple_65 where_clauses_simple_double__u64__usize_(uint64_t x, size_t y); /** A monomorphic instance of K. @@ -151,13 +101,7 @@ typedef struct tuple_b6_s } tuple_b6; -/** -A monomorphic instance of where_clauses_simple.double_k -with types size_t, uint64_t -with const generics -- K= 3 -*/ -tuple_b6 where_clauses_simple_double_k_7b(size_t x, uint64_t y); +tuple_b6 where_clauses_simple_double_k__usize__u64__3usize_(size_t x, uint64_t y); void where_clauses_simple_main(void); diff --git a/test/where_clauses_from_fn.c b/test/where_clauses_from_fn.c new file mode 100644 index 00000000..ac27b77c --- /dev/null +++ b/test/where_clauses_from_fn.c @@ -0,0 +1,5 @@ +#include "where_clauses_closures.h" + +extern void core_convert__core__convert__Into___usize__usize___into__usize__usize_(size_t x0[1U]) { + x0[0U] = where_clauses_closures_test_call_mut__usize__1usize__8a(NULL, 0U); +} \ No newline at end of file From 5d85eec3b53f664a9c8713c83a54dc43a8be28ba Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Tue, 30 Sep 2025 15:28:21 +0800 Subject: [PATCH 17/20] fix undefined static inline in where_clauses_closures and where-clauses_simple --- bin/main.ml | 1 + include/eurydice_glue.h | 13 ++ lib/Cleanup2.ml | 62 +++++++++ out/test-array2d/array2d.h | 12 -- out/test-const_generics/const_generics.h | 122 ------------------ out/test-floating_points/floating_points.h | 4 - out/test-issue_107/issue_107.c | 8 -- out/test-issue_107/issue_107.h | 5 - out/test-partial_eq/partial_eq.c | 11 -- out/test-partial_eq/partial_eq.h | 6 - out/test-reborrow/reborrow.h | 5 - out/test-slice_array/slice_array.h | 6 - out/test-trait_generics/trait_generics.c | 8 -- out/test-trait_generics/trait_generics.h | 5 - out/test-traits/traits.h | 50 ------- out/test-traits3/traits3.c | 8 -- out/test-traits3/traits3.h | 5 - .../where_clauses_closures.c | 10 -- .../where_clauses_closures.h | 16 --- .../where_clauses_simple.h | 6 - 20 files changed, 76 insertions(+), 287 deletions(-) diff --git a/bin/main.ml b/bin/main.ml index d7167a27..dade5a37 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -303,6 +303,7 @@ Supported options:|} Eurydice.Logging.log "Phase2.95" "%a" pfiles files; let files = Eurydice.Cleanup2.bonus_cleanups#visit_files [] files in let files = Krml.Inlining.drop_unused files in + let files = Eurydice.Cleanup2.drop_unused_monoed_func files in (* Macros stemming from globals -- FIXME why is this not Krml.AstToCStar.mk_macros_set? *) let files, macros = Eurydice.Cleanup2.build_macros files in diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index 4067e60c..a81f2f4b 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -318,6 +318,19 @@ core_convert_num__core__convert__From_u16__for_usize__from(uint16_t x) { return x; } +// for monoed where-clauses_simple +static inline uint64_t +core_convert_num__core__convert__From___u64__u16___from(uint16_t x) { + return x; +} + +static inline size_t +core_convert_num__core__convert__From___usize__u16___from(uint16_t x) { + return x; +} + + + static inline uint32_t core_num__u8__count_ones(uint8_t x0) { #ifdef _MSC_VER return __popcnt(x0); diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 32dbcdd3..2b45a3fe 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -1439,6 +1439,68 @@ let drop_unused_type files = | _ -> Some d ) files + let drop_unused_monoed_func files = + let open Krml in + let seen = Hashtbl.create 41 in + + let body_of_lid = Helpers.build_map files (fun map d -> Hashtbl.add map (lid_of_decl d) d) in + + let visitor = object (self) + inherit [_] iter as super + method! visit_EQualified (before, _) lid = + self#discover before lid + method! visit_TQualified before lid = + self#discover before lid + method! visit_TApp before lid ts = + self#discover before lid; + List.iter (self#visit_typ before) ts + method private discover before lid = + if not (Hashtbl.mem seen lid) then begin + Hashtbl.add seen lid (); + if Options.debug "reachability" then + KPrint.bprintf "REACHABILITY: %a is used (via: %s) \n" plid lid + (String.concat " <- " (List.map (fun lid -> KPrint.bsprintf "%a" plid lid) before)); + + if Hashtbl.mem body_of_lid lid then + ignore (super#visit_decl (lid :: before) (Hashtbl.find body_of_lid lid)); + end + end in + visitor#visit_files [] files; + filter_decls (fun d -> + match d with + | DFunction (_, _, _, _, _, lid, _, _) -> + L.log "Cleanup2" "[Drop] visiting function %a \n" plid lid ; + if (Hashtbl.mem seen lid) then Some d else + begin + try let _name, cgs, ts, fn_ptrs = Hashtbl.find AstOfLlbc.lid_full_generic lid in + if cgs = [] && ts = [] && fn_ptrs = [] then + Some d + else + begin L.log "Cleanup2" "[Drop] function %a droped as unused monoed func \n" plid lid; + None end + with Not_found -> begin L.log "Cleanup2" "[Drop] function %a droped as unmapped func \n" plid lid; None end + end + | DExternal (_, _, _, _, lid, _, _) -> + L.log "Cleanup2" "[Drop] visiting function %a \n" plid lid ; + if (Hashtbl.mem seen lid) then Some d else + begin + try let _name, cgs, ts, fn_ptrs = Hashtbl.find AstOfLlbc.lid_full_generic lid in + if cgs = [] && ts = [] && fn_ptrs = [] then + Some d + else + begin + L.log "Cleanup2" "[Drop] function %a droped as unused monoed func \n" plid lid; + None + end + with Not_found -> + begin + L.log "Cleanup2" "[Drop] function %a droped as unmapped func \n" plid lid; + None + end + end + | _ -> Some d + ) files + let remove_empty_structs files = let open Krml.Idents in diff --git a/out/test-array2d/array2d.h b/out/test-array2d/array2d.h index 87dedc39..cf3322db 100644 --- a/out/test-array2d/array2d.h +++ b/out/test-array2d/array2d.h @@ -15,22 +15,10 @@ extern "C" { #endif -extern bool -core_array_equality__core__cmp__PartialEq____Array__Array_u32__2usize___4usize____Array__Array_u32__2usize___4usize____eq___Array_u32__2usize____Array_u32__2usize___4usize_( - uint32_t (*x0)[2U], - uint32_t (*x1)[2U] -); - bool array2d_f(uint32_t x[4U][2U]); void array2d_main(void); -extern bool -core_array_equality__core__cmp__PartialEq____Array_u32__2usize____Array_u32__2usize____eq__u32__u32__2usize_( - uint32_t *x0, - uint32_t *x1 -); - extern bool core_cmp_impls__core__cmp__PartialEq___u32__u32___eq(uint32_t *x0, uint32_t *x1); #if defined(__cplusplus) diff --git a/out/test-const_generics/const_generics.h b/out/test-const_generics/const_generics.h index 8e988627..a3cbe19a 100644 --- a/out/test-const_generics/const_generics.h +++ b/out/test-const_generics/const_generics.h @@ -17,8 +17,6 @@ extern "C" { static inline void core_num__u32__to_be_bytes(uint32_t x0, uint8_t x1[4U]); -extern void core_slice___Slice_u8___copy_from_slice__u8_(Eurydice_slice x0, Eurydice_slice x1); - void const_generics_serialize__8usize_(Eurydice_slice re, uint8_t ret[8U]); void const_generics_main(void); @@ -57,30 +55,6 @@ bool const_generics_g__3usize__4u32_(uint32_t x, size_t y); void const_generics_main3(void); -extern Eurydice_slice -core_array__core__ops__index__Index____Array_u8__8usize___core__ops__range__RangeFrom___usize____index__u8__core__ops__range__RangeFrom___usize___8usize_( - uint8_t *x0, - size_t x1 -); - -extern Eurydice_slice -core_array__core__ops__index__Index____Array_u8__8usize___core__ops__range__RangeTo___usize____index__u8__core__ops__range__RangeTo___usize___8usize_( - uint8_t *x0, - size_t x1 -); - -extern Eurydice_slice -core_array__core__ops__index__IndexMut____Array_u8__8usize___core__ops__range__RangeFrom___usize____index_mut__u8__core__ops__range__RangeFrom___usize___8usize_( - uint8_t *x0, - size_t x1 -); - -extern Eurydice_slice -core_array__core__ops__index__IndexMut____Array_u8__8usize___core__ops__range__RangeTo___usize____index_mut__u8__core__ops__range__RangeTo___usize___8usize_( - uint8_t *x0, - size_t x1 -); - extern uint32_t core_clone_impls__core__clone__Clone___u32___clone(uint32_t *x0); extern uint64_t core_clone_impls__core__clone__Clone___u64___clone(uint64_t *x0); @@ -106,102 +80,6 @@ typedef struct core_option_Option______mut___Slice_u8____s } core_option_Option______mut___Slice_u8___; -extern Eurydice_slice -core_slice_index__core__ops__index__Index____Slice_u8___core__ops__range__RangeFrom___usize____index__u8__core__ops__range__RangeFrom___usize__( - Eurydice_slice x0, - size_t x1 -); - -extern Eurydice_slice -core_slice_index__core__ops__index__Index____Slice_u8___core__ops__range__RangeTo___usize____index__u8__core__ops__range__RangeTo___usize__( - Eurydice_slice x0, - size_t x1 -); - -extern Eurydice_slice -core_slice_index__core__ops__index__IndexMut____Slice_u8___core__ops__range__RangeFrom___usize____index_mut__u8__core__ops__range__RangeFrom___usize__( - Eurydice_slice x0, - size_t x1 -); - -extern Eurydice_slice -core_slice_index__core__ops__index__IndexMut____Slice_u8___core__ops__range__RangeTo___usize____index_mut__u8__core__ops__range__RangeTo___usize__( - Eurydice_slice x0, - size_t x1 -); - -extern core_option_Option________Slice_u8___ -core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____get__u8_( - size_t x0, - Eurydice_slice x1 -); - -extern core_option_Option______mut___Slice_u8___ -core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____get_mut__u8_( - size_t x0, - Eurydice_slice x1 -); - -extern uint8_t -(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____get_unchecked__u8_( - size_t x0, - uint8_t (*x1)[] -))[]; - -extern uint8_t -(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____get_unchecked_mut__u8_( - size_t x0, - uint8_t (*x1)[] -))[]; - -extern Eurydice_slice -core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____index__u8_( - size_t x0, - Eurydice_slice x1 -); - -extern Eurydice_slice -core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeFrom___usize____Slice_u8____index_mut__u8_( - size_t x0, - Eurydice_slice x1 -); - -extern core_option_Option________Slice_u8___ -core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____get__u8_( - size_t x0, - Eurydice_slice x1 -); - -extern core_option_Option______mut___Slice_u8___ -core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____get_mut__u8_( - size_t x0, - Eurydice_slice x1 -); - -extern uint8_t -(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____get_unchecked__u8_( - size_t x0, - uint8_t (*x1)[] -))[]; - -extern uint8_t -(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____get_unchecked_mut__u8_( - size_t x0, - uint8_t (*x1)[] -))[]; - -extern Eurydice_slice -core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____index__u8_( - size_t x0, - Eurydice_slice x1 -); - -extern Eurydice_slice -core_slice_index__core__slice__index__SliceIndex___core__ops__range__RangeTo___usize____Slice_u8____index_mut__u8_( - size_t x0, - Eurydice_slice x1 -); - #if defined(__cplusplus) } #endif diff --git a/out/test-floating_points/floating_points.h b/out/test-floating_points/floating_points.h index 538434bc..bc5ab714 100644 --- a/out/test-floating_points/floating_points.h +++ b/out/test-floating_points/floating_points.h @@ -15,10 +15,6 @@ extern "C" { #endif -extern size_t core_slice___Slice_f32___len__f32_(Eurydice_slice x0); - -extern size_t core_slice___Slice_f64___len__f64_(Eurydice_slice x0); - void floating_points_main(void); #if defined(__cplusplus) diff --git a/out/test-issue_107/issue_107.c b/out/test-issue_107/issue_107.c index 66580d2c..c817568e 100644 --- a/out/test-issue_107/issue_107.c +++ b/out/test-issue_107/issue_107.c @@ -12,11 +12,3 @@ void issue_107_main(void) } -/** -This function found in impl {issue_107::Fun::} -*/ -uint8_t issue_107_f_4d(void) -{ - return 5U; -} - diff --git a/out/test-issue_107/issue_107.h b/out/test-issue_107/issue_107.h index 59d118fa..96d38cde 100644 --- a/out/test-issue_107/issue_107.h +++ b/out/test-issue_107/issue_107.h @@ -17,11 +17,6 @@ extern "C" { void issue_107_main(void); -/** -This function found in impl {issue_107::Fun::} -*/ -uint8_t issue_107_f_4d(void); - #if defined(__cplusplus) } #endif diff --git a/out/test-partial_eq/partial_eq.c b/out/test-partial_eq/partial_eq.c index 3f6f5183..64426882 100644 --- a/out/test-partial_eq/partial_eq.c +++ b/out/test-partial_eq/partial_eq.c @@ -46,14 +46,3 @@ void partial_eq_main(void) "panic!"); } -/** -This function found in impl {core::fmt::Debug::} -*/ -inline core_result_Result______core__fmt__Error_ -partial_eq_fmt_af(partial_eq_Enum *self, core_fmt_Formatter_____ *f) -{ - return - core_fmt__core__fmt__Formatter________write_str_____(f, - (KRML_CLITERAL(Eurydice_str){ .data = "A", .len = (size_t)1U })); -} - diff --git a/out/test-partial_eq/partial_eq.h b/out/test-partial_eq/partial_eq.h index 143879c3..e9efa2fe 100644 --- a/out/test-partial_eq/partial_eq.h +++ b/out/test-partial_eq/partial_eq.h @@ -45,12 +45,6 @@ bool partial_eq_eq_aa(partial_eq_Enum *self, partial_eq_Enum *other); void partial_eq_main(void); -/** -This function found in impl {core::fmt::Debug::} -*/ -core_result_Result______core__fmt__Error_ -partial_eq_fmt_af(partial_eq_Enum *self, core_fmt_Formatter_____ *f); - #if defined(__cplusplus) } #endif diff --git a/out/test-reborrow/reborrow.h b/out/test-reborrow/reborrow.h index 8bdcf9f8..f04921cc 100644 --- a/out/test-reborrow/reborrow.h +++ b/out/test-reborrow/reborrow.h @@ -15,11 +15,6 @@ extern "C" { #endif -extern void -alloc_boxed__core__ops__drop__Drop___alloc__boxed__Box_u8__core__marker__MetaSized___u8___core__marker__Sized___alloc__alloc__Global_____drop__u8__alloc__alloc__Global_( - uint8_t **x0 -); - void reborrow_main(void); #if defined(__cplusplus) diff --git a/out/test-slice_array/slice_array.h b/out/test-slice_array/slice_array.h index 5d92f0ca..94505a81 100644 --- a/out/test-slice_array/slice_array.h +++ b/out/test-slice_array/slice_array.h @@ -22,12 +22,6 @@ typedef struct Eurydice_slice_uint8_t_4size_t__x2_s } Eurydice_slice_uint8_t_4size_t__x2; -extern Eurydice_slice_uint8_t_4size_t__x2 -core_slice___Slice__Array_u8__4usize____split_at_mut___Array_u8__4usize__( - Eurydice_slice x0, - size_t x1 -); - void slice_array_f1(void); void slice_array_f2(void); diff --git a/out/test-trait_generics/trait_generics.c b/out/test-trait_generics/trait_generics.c index 78a2ed26..77c5576b 100644 --- a/out/test-trait_generics/trait_generics.c +++ b/out/test-trait_generics/trait_generics.c @@ -25,11 +25,3 @@ void trait_generics_main(void) trait_generics_from_fn__trait_generics__Foo___10usize__(); } -/** -This function found in impl {core::ops::drop::Drop::>} -*/ -void trait_generics_Foo_drop__10usize__5e(void **_) -{ - -} - diff --git a/out/test-trait_generics/trait_generics.h b/out/test-trait_generics/trait_generics.h index 11b48d92..faefeea7 100644 --- a/out/test-trait_generics/trait_generics.h +++ b/out/test-trait_generics/trait_generics.h @@ -24,11 +24,6 @@ void trait_generics_from_fn__trait_generics__Foo___10usize__(void); void trait_generics_main(void); -/** -This function found in impl {core::ops::drop::Drop::>} -*/ -void trait_generics_Foo_drop__10usize__5e(void **_); - #if defined(__cplusplus) } #endif diff --git a/out/test-traits/traits.h b/out/test-traits/traits.h index 05146dd7..d10c1484 100644 --- a/out/test-traits/traits.h +++ b/out/test-traits/traits.h @@ -15,19 +15,11 @@ extern "C" { #endif -#include "Eurydice.h" - #define traits_Foo_Foo1 0 #define traits_Foo_Foo2 1 typedef uint8_t traits_Foo; -extern Eurydice_slice -core_array__core__ops__index__Index____Array_traits__Foo__2usize___core__ops__range__Range___usize____index__traits__Foo__core__ops__range__Range___usize___2usize_( - traits_Foo *x0, - core_ops_range_Range__usize_ x1 -); - #define core_option_Option_None 0 #define core_option_Option_Some 1 @@ -47,48 +39,6 @@ typedef struct core_option_Option______mut___Slice_traits__Foo____s } core_option_Option______mut___Slice_traits__Foo___; -extern Eurydice_slice -core_slice_index__core__ops__index__Index____Slice_traits__Foo___core__ops__range__Range___usize____index__traits__Foo__core__ops__range__Range___usize__( - Eurydice_slice x0, - core_ops_range_Range__usize_ x1 -); - -extern core_option_Option________Slice_traits__Foo___ -core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____get__traits__Foo_( - core_ops_range_Range__usize_ x0, - Eurydice_slice x1 -); - -extern core_option_Option______mut___Slice_traits__Foo___ -core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____get_mut__traits__Foo_( - core_ops_range_Range__usize_ x0, - Eurydice_slice x1 -); - -extern traits_Foo -(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____get_unchecked__traits__Foo_( - core_ops_range_Range__usize_ x0, - traits_Foo (*x1)[] -))[]; - -extern traits_Foo -(*core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____get_unchecked_mut__traits__Foo_( - core_ops_range_Range__usize_ x0, - traits_Foo (*x1)[] -))[]; - -extern Eurydice_slice -core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____index__traits__Foo_( - core_ops_range_Range__usize_ x0, - Eurydice_slice x1 -); - -extern Eurydice_slice -core_slice_index__core__slice__index__SliceIndex___core__ops__range__Range___usize____Slice_traits__Foo____index_mut__traits__Foo_( - core_ops_range_Range__usize_ x0, - Eurydice_slice x1 -); - /** This function found in impl {traits::ToInt::} */ diff --git a/out/test-traits3/traits3.c b/out/test-traits3/traits3.c index b757e6b7..a98fa041 100644 --- a/out/test-traits3/traits3.c +++ b/out/test-traits3/traits3.c @@ -22,11 +22,3 @@ void traits3_main(void) } -/** -This function found in impl {traits3::internal::KeccakItem::<(u64, u64), 2usize>} -*/ -traits3_uint64x2_t traits3_zero_ec(void) -{ - return (KRML_CLITERAL(traits3_uint64x2_t){ .fst = 0ULL, .snd = 0ULL }); -} - diff --git a/out/test-traits3/traits3.h b/out/test-traits3/traits3.h index db03dda4..975f3311 100644 --- a/out/test-traits3/traits3.h +++ b/out/test-traits3/traits3.h @@ -28,11 +28,6 @@ typedef struct traits3_uint64x2_t_s } traits3_uint64x2_t; -/** -This function found in impl {traits3::internal::KeccakItem::<(u64, u64), 2usize>} -*/ -traits3_uint64x2_t traits3_zero_ec(void); - #if defined(__cplusplus) } #endif diff --git a/out/test-where_clauses_closures/where_clauses_closures.c b/out/test-where_clauses_closures/where_clauses_closures.c index 30f29be0..350e300f 100644 --- a/out/test-where_clauses_closures/where_clauses_closures.c +++ b/out/test-where_clauses_closures/where_clauses_closures.c @@ -60,13 +60,3 @@ size_t where_clauses_closures_test_call_mut__usize__1usize__8a(void **_, size_t return where_clauses_closures_of_usize_77(i); } -/** -This function found in impl {core::ops::function::FnOnce::, (usize)>} -*/ -size_t where_clauses_closures_test_call_once__usize__1usize__c9(size_t _) -{ - /* original Rust expression is not an lvalue in C */ - void *lvalue = (void *)0U; - return where_clauses_closures_test_call_mut__usize__1usize__8a(&lvalue, _); -} - diff --git a/out/test-where_clauses_closures/where_clauses_closures.h b/out/test-where_clauses_closures/where_clauses_closures.h index e4610525..0759c623 100644 --- a/out/test-where_clauses_closures/where_clauses_closures.h +++ b/out/test-where_clauses_closures/where_clauses_closures.h @@ -15,19 +15,8 @@ extern "C" { #endif -extern void -core_array_from_fn__usize__where_clauses_closures__test__closure___usize__1usize___1usize_( - size_t x0[1U] -); - extern size_t core_clone_impls__core__clone__Clone___usize___clone(size_t *x0); -static inline size_t -core_convert__core__convert__From___usize__usize___from__usize_(size_t x0); - -static inline size_t -core_convert__core__convert__Into___usize__usize___into__usize__usize_(size_t x0); - /** This function found in impl {where_clauses_closures::Ops::} */ @@ -54,11 +43,6 @@ This function found in impl {core::ops::function::FnMut::, (usize)>} -*/ -size_t where_clauses_closures_test_call_once__usize__1usize__c9(size_t _); - #if defined(__cplusplus) } #endif diff --git a/out/test-where_clauses_simple/where_clauses_simple.h b/out/test-where_clauses_simple/where_clauses_simple.h index 994f0d57..74494c09 100644 --- a/out/test-where_clauses_simple/where_clauses_simple.h +++ b/out/test-where_clauses_simple/where_clauses_simple.h @@ -23,12 +23,6 @@ static inline uint64_t core_convert_num__core__convert__From___u64__u16___from(u static inline size_t core_convert_num__core__convert__From___usize__u16___from(uint16_t x0); -static inline uint64_t -core_convert__core__convert__Into___u16__u64___into__u16__u64_(uint16_t x0); - -static inline size_t -core_convert__core__convert__Into___u16__usize___into__u16__usize_(uint16_t x0); - /** This function found in impl {where_clauses_simple::Ops::} */ From b4f2669db9b05e247d14e094b7aa410a10c49193 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Tue, 21 Oct 2025 14:37:57 +0800 Subject: [PATCH 18/20] added some binder_value for generics --- lib/AstOfLlbc.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index f9e7e74c..6a02a65e 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -555,14 +555,14 @@ let re_polymorphize expr = let pure_c_name (name : C.name) = let pre, last = Krml.KList.split_at_last name in match last with - | PeMonomorphized _args -> pre + | PeInstantiated _args -> pre | _ -> name (* get the trait_refs from mono. charon name, used in lookup_fun *) let trait_refs_c_name (name : C.name) : C.trait_ref list = let _pre, last = Krml.KList.split_at_last name in match last with - | PeMonomorphized args -> args.trait_refs + | PeInstantiated args -> args.binder_value.trait_refs | _ -> [] let pure_lid_of_name (env : env) (name : Charon.Types.name) : K.lident = @@ -584,7 +584,7 @@ let rec insert_lid_full_generic (env : env) (full_name : K.lident) (name : Charo let item_name, generic = let pre, last = Krml.KList.split_at_last name in match last with - | PeMonomorphized args -> pure_lid_of_name env pre, (args : C.generic_args) + | PeInstantiated args -> pure_lid_of_name env pre, (args.binder_value : C.generic_args) | _ -> full_name, { C.types = []; regions = []; const_generics = []; trait_refs = [] } in let cgs, tys = @@ -1366,7 +1366,7 @@ and debug_trait_clause_mapping env (mapping : (var_id * K.typ) list) = (* Helper for getting monomorphized generic arguments from a name *) let try_get_mono_from_name (name : C.name) = match List.rev name with - | PeMonomorphized generics :: _ -> Some generics + | PeInstantiated generics :: _ -> Some generics | _ -> None (* Only get monomorphized generics for known *Eurydice* builtins *) @@ -1477,7 +1477,7 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = | None -> generics (* Essentially, there might still be (late-bound) region arguments in the original generics But we don't care about them (the regions), so just ignore them. *) - | Some generics -> generics + | Some generics -> generics.binder_value in let { C.types = type_args; const_generics = const_generic_args; trait_refs; _ } = generics in @@ -1503,7 +1503,7 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = let trait_impl = env.get_nth_trait_impl id in match try_get_mono_from_name trait_impl.item_meta.name with (* The same applies here: ignoring potential region arguments *) - | Some generics when is_known_builtin -> generics + | Some generics when is_known_builtin -> generics.binder_value | _ -> generics end | _ -> C.empty_generic_args From 3dfad3d6d9c189ccb125970720ea8c7448d84487 Mon Sep 17 00:00:00 2001 From: Kelvin_MYYZJ Date: Thu, 23 Oct 2025 18:43:33 +0800 Subject: [PATCH 19/20] Fix cremepat --- cremepat/cremepat.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/cremepat/cremepat.ml b/cremepat/cremepat.ml index 8294587c..3a802828 100644 --- a/cremepat/cremepat.ml +++ b/cremepat/cremepat.ml @@ -157,13 +157,16 @@ let compile_parse_tree (env : env) loc (* EApp (ETApp (e, ts), es) *) ppat_cons_many ~loc "EApp" [ - ppat_cons_many ~loc "ETApp" - [ - compile env head; - compile_expr_list_pattern env cgs; - compile_expr_list_pattern env methods; - compile_typ_list_pattern env ts; - ]; + (if cgs = [] && methods = [] && ts = [] then + compile env head + else + ppat_cons_many ~loc "ETApp" + [ + compile env head; + compile_expr_list_pattern env cgs; + compile_expr_list_pattern env methods; + compile_typ_list_pattern env ts; + ]); ppat_list ~loc (List.map (compile env) args); ] | Addr e -> ppat_cons_one ~loc "EAddrOf" (compile env e) From 3adc454d46f502baf3b77c7227677a2b3e7083fb Mon Sep 17 00:00:00 2001 From: Kelvin_MYYZJ Date: Fri, 24 Oct 2025 15:23:26 +0800 Subject: [PATCH 20/20] fix monomorphized resugar_loops (no step_by) --- lib/Cleanup2.ml | 161 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 161 insertions(+) diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 07a3685f..f206b8b7 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -641,6 +641,44 @@ let ends_with_return = | EReturn _ -> true | _ -> false) +let width_of_int_name name : width = + match name with + | "" -> Int8 + | "" -> Int16 + | "" -> Int32 + | "" -> Int64 + | "" -> UInt8 + | "" -> UInt16 + | "" -> UInt32 + | "" -> UInt64 + | "" -> SizeT + | _ -> invalid_arg name + +let type_of_int_name name = TInt (width_of_int_name name) +let node_of_with_type e' = e'.node +let typ_of_with_type e' = e'.typ + +let rest_of_let' e_let = + match e_let with + | ELet (_, _, e_rest) -> e_rest + | _ -> assert false + +let rest_of_let e_let' = e_let' |> node_of_with_type |> rest_of_let' + +let body_of_while' e_while = + match e_while with + | EWhile (_, e_body) -> e_body + | _ -> assert false + +let body_of_while e_while' = e_while' |> node_of_with_type |> body_of_while' + +let binder_of_let e_let = + match e_let with + | ELet (b, _, _) -> b + | _ -> assert false + +let typ_of_let e_let = e_let |> node_of_with_type |> binder_of_let |> typ_of_with_type + let resugar_loops = object(self) inherit [_] map as super @@ -877,6 +915,129 @@ let resugar_loops = self#visit_expr env e_body) ) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest) + (* Terminal position (regular range for-loop) *) + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter::?range_name + ({ start: ?e_start, end: ?e_end }); + while true { + let x = core::iter::range::?::next::?t1_name(&iter); + match x { + None -> break, + Some ? -> ?e_body + } + } + |}] when Krml.KString.starts_with range_name " + let open Krml.Helpers in + let w = width_of_int_name t1_name in + let t1 = TInt w in + let t_op = e |> rest_of_let |> body_of_while |> typ_of_let in + let e_some_i = with_type t_op (ECons ("Some", [with_type t1 (EBound 0)])) in + with_type e.typ @@ EFor (fresh_binder ~mut:true "i" t1, + e_start, + mk_lt w (Krml.DeBruijn.lift 1 e_end), + mk_incr w, + self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body)) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter::?range_name + ({ start: ?e_start, end: ?e_end }); + while true { + match (core::iter::range::?::next::?t1_name(&iter)) { + None -> break, + Some ? -> ?e_body + } + } + |}] when Krml.KString.starts_with range_name " + let open Krml.Helpers in + let w = width_of_int_name t1_name in + let t1 = TInt w in + with_type e.typ @@ EFor (fresh_binder ~mut:true "i" t1, + e_start, + mk_lt w (Krml.DeBruijn.lift 1 e_end), + mk_incr w, + self#visit_expr env e_body) + + (* Non-terminal position (regular range for-loop) *) + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter::?range_name + ({ start: ?e_start, end: ?e_end }); + while true { + let x = core::iter::range::?::next::?t1_name(&iter); + match x { + None -> break, + Some ? -> ?e_body + } + }; + ?rest.. + |}] when Krml.KString.starts_with range_name " + let open Krml.Helpers in + let w = width_of_int_name t1_name in + let t1 = TInt w in + let t_op = e |> rest_of_let |> body_of_while |> typ_of_let in + let e_some_i = with_type t_op (ECons ("Some", [with_type t1 (EBound 0)])) in + with_type e.typ @@ ESequence (with_type TUnit (EFor (fresh_binder ~mut:true "i" t1, + e_start, + mk_lt w (Krml.DeBruijn.lift 1 e_end), + mk_incr w, + self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body)) + ) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest) + + (* Special variant that appears in external crates -- TODO: do we need variants of all other + patterns? *) + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter::?range_name + ({ start: ?e_start, end: ?e_end }); + while true { + let x = core::iter::range::?::next::?t1_name(&iter); + match x { + None -> ?e2, + Some ? -> ?e_body + }; + abort + } + |}] when Krml.KString.starts_with range_name " + let open Krml.Helpers in + let w = width_of_int_name t1_name in + let t1 = TInt w in + let t_op = e |> rest_of_let |> body_of_while |> typ_of_let in + let e_some_i = with_type t_op (ECons ("Some", [with_type t1 (EBound 0)])) in + with_type e.typ @@ ESequence [ + with_type TUnit (EFor (fresh_binder ~mut:true "i" t1, + e_start, + mk_lt w (Krml.DeBruijn.lift 1 e_end), + mk_incr w, + self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body)) + ); + self#visit_expr env (Krml.DeBruijn.(subst eunit 0 (subst eunit 0 e2))) + ] + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter::?range_name + ({ start: ?e_start, end: ?e_end }); + while true { + match (core::iter::range::?::next::?t1_name(&iter)) { + None -> break, + Some ? -> ?e_body + } + }; + ?rest.. + |}] when Krml.KString.starts_with range_name " + let open Krml.Helpers in + let w = width_of_int_name t1_name in + let t1 = TInt w in + with_type e.typ @@ ESequence (with_type TUnit (EFor (fresh_binder ~mut:true "i" t1, + e_start, + mk_lt w (Krml.DeBruijn.lift 1 e_end), + mk_incr w, + self#visit_expr env e_body) + ) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest) + | _ -> super#visit_expr env e