From f2945d472d0cc2b965b2fa5833a452a99ee1b7f7 Mon Sep 17 00:00:00 2001 From: ssyram Date: Mon, 27 Oct 2025 16:32:44 +0800 Subject: [PATCH 01/16] Eurydice::opaque added --- bin/main.ml | 4 +-- include/eurydice_glue.h | 2 ++ lib/AstOfLlbc.ml | 51 +++++++++++++++++++++++++++++++++-- lib/Builtin.ml | 22 +++++++++++++-- test/dyn_trait_struct_type.rs | 12 ++++----- 5 files changed, 79 insertions(+), 12 deletions(-) diff --git a/bin/main.ml b/bin/main.ml index bcafa11e..e3b56f95 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -208,7 +208,7 @@ Supported options:|} in let files = Eurydice.Cleanup1.cleanup files in - Eurydice.Logging.log "Phase2" "%a" pfiles files; + Eurydice.Logging.log "Phase2" "Phase 2 start:\n%a" pfiles files; let errors, files = Krml.Checker.check_everything ~warn:true files in if errors then fail __FILE__ __LINE__; @@ -217,7 +217,7 @@ Supported options:|} let files = Eurydice.Cleanup2.resugar_loops#visit_files () files in let files = Eurydice.Cleanup1.remove_terminal_returns#visit_files true files in let files = Eurydice.Cleanup1.remove_terminal_continues#visit_files false files in - Eurydice.Logging.log "Phase2.1" "%a" pfiles files; + Eurydice.Logging.log "Phase2.1" "Phase 2.1:\n%a" pfiles files; (* Sanity check for the big rewriting above. *) let errors, files = Krml.Checker.check_everything ~warn:true files in if errors then diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index ac11afee..cbba21dc 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -62,6 +62,8 @@ using std::type_identity_t; #define Eurydice_alignof(t) alignof(t) +#define Eurydice_opaque(t, reason) *((t *)0) + // SLICES, ARRAYS, ETC. // We define several slice types in order to define builtin definitions for diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 9a00d3b7..619bfd6c 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -1718,6 +1718,9 @@ let expression_of_operand (env : env) (op : C.operand) : K.expr = fail "expression_of_operand Constant: %s" (Charon.PrintExpressions.operand_to_string env.format_env op) end + | Constant { kind = COpaque reason; ty } -> + let typ = typ_of_ty env ty in + Builtin.opaque_with_reason typ reason | Constant _ -> fail "expression_of_operand: %s" (Charon.PrintExpressions.operand_to_string env.format_env op) @@ -1804,10 +1807,14 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = mk_reference e metadata | NullaryOp (SizeOf, ty) -> let t = typ_of_ty env ty in - K.(with_type TBool (EApp (Builtin.(expr_of_builtin_t sizeof [ t ]), []))) + K.( + with_type (TInt SizeT) + (EApp (Builtin.(expr_of_builtin_t sizeof [ t ]), [ Krml.Helpers.eunit ]))) | NullaryOp (AlignOf, ty) -> let t = typ_of_ty env ty in - K.(with_type TBool (EApp (Builtin.(expr_of_builtin_t alignof [ t ]), []))) + K.( + with_type (TInt SizeT) + (EApp (Builtin.(expr_of_builtin_t alignof [ t ]), [ Krml.Helpers.eunit ]))) | UnaryOp (Cast (CastScalar (_, dst)), e) -> let dst = typ_of_literal_ty env dst in K.with_type dst (K.ECast (expression_of_operand env e, dst)) @@ -1855,6 +1862,46 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = (K.ETApp (array_to_slice, [ len ], [], [ t ])) in K.(with_type (Builtin.mk_slice t) (EApp (array_to_slice, [ e ]))) + | MetaVTablePtr trait_ref, TBuf (_, _), _ -> + (* Cast from T to T where Unsized is a user-defined DST. + We build the vtable pointer for the trait object here. *) + let vtable_ptr = + let vtable_instance = + match trait_ref.kind with + | TraitImpl { id; generics } -> + let trait_impl = env.get_nth_trait_impl id in + begin + match trait_impl.vtable with + | Some instance -> { instance with C.generics } + | None -> failwith "Trait impl has no vtable instance" + end + | _ -> failwith "unsupported trait_ref kind in unsize cast" + in + let instance_def = env.get_nth_global vtable_instance.C.id in + let instance_ty = + let subst = + Charon.Substitute.make_subst_from_generics instance_def.generics + vtable_instance.generics + in + let real_ty = Charon.Substitute.(ty_substitute subst instance_def.ty) in + typ_of_ty env real_ty + in + let vtable_instance = + K.with_type instance_ty (K.EQualified (lid_of_name env instance_def.item_meta.name)) + in + addrof vtable_instance + in + let coercion = + K.with_type + (K.TBuf (Builtin.c_void_t, false)) + (K.ECast (e, K.TBuf (Builtin.c_void_t, false))) + in + (* Do not use `mk_reference` here, + as `e` itself is already the target, not its reference *) + K.( + with_type + (Builtin.mk_dst_ref Builtin.c_void_t vtable_ptr.typ) + (EFlat [ Some "ptr", coercion; Some "meta", vtable_ptr ])) | _ -> Krml.Warn.fatal_error "unknown unsize cast: `%s`\nt_to=%a\nt_from=%a" (Charon.PrintExpressions.cast_kind_to_string env.format_env ck) diff --git a/lib/Builtin.ml b/lib/Builtin.ml index 3a326eb2..bf7dcae6 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -7,7 +7,10 @@ end let vec : K.lident = [ "Eurydice" ], "vec" let mk_vec (t : K.typ) : K.typ = K.TApp (vec, [ t ]) let dst_ref = [ "Eurydice" ], "dst_ref" + +(** Given `T` and `TMeta`, returns `Eurydice::dst_ref` *) let mk_dst_ref (t : K.typ) (meta : K.typ) : K.typ = K.TApp (dst_ref, [ t; meta ]) + let slice : K.lident = dst_ref let mk_slice (t : K.typ) : K.typ = K.TApp (slice, [ t; TInt SizeT ]) let range : K.lident = [ "core"; "ops"; "range" ], "Range" @@ -161,7 +164,7 @@ let get_128_op (kind, op) : K.expr = expr_of_builtin @@ Op128Map.find (kind, op) let sizeof = { name = [ "Eurydice" ], "sizeof"; - typ = Krml.Helpers.fold_arrow [] (TInt SizeT); + typ = Krml.Helpers.fold_arrow [ TUnit ] (TInt SizeT); n_type_args = 1; cg_args = []; arg_names = []; @@ -172,12 +175,26 @@ let sizeof = let alignof = { name = [ "Eurydice" ], "alignof"; - typ = Krml.Helpers.fold_arrow [] (TInt SizeT); + typ = Krml.Helpers.fold_arrow [ TUnit ] (TInt SizeT); n_type_args = 1; cg_args = []; arg_names = []; } +let opaque = + { + name = [ "Eurydice" ], "opaque"; + typ = Krml.Helpers.fold_arrow [ TBuf (c_char_t, false) ] (TBound 0); + n_type_args = 1; + cg_args = []; + arg_names = [ "reason" ]; + } + +let opaque_with_reason ret_t reason = + let app_typ = Krml.Helpers.fold_arrow [ TBuf (c_char_t, false) ] ret_t in + let opaque = K.with_type app_typ (K.ETApp (expr_of_builtin opaque, [], [], [ ret_t ])) in + K.with_type ret_t (K.EApp (opaque, [ K.with_type (TBuf (c_char_t, false)) (K.EString reason) ])) + let array_to_slice = { name = [ "Eurydice" ], "array_to_slice"; @@ -936,6 +953,7 @@ let builtin_funcs = [ sizeof; alignof; + opaque; array_repeat; array_into_iter; array_eq; diff --git a/test/dyn_trait_struct_type.rs b/test/dyn_trait_struct_type.rs index 2ec44e84..90efcca8 100644 --- a/test/dyn_trait_struct_type.rs +++ b/test/dyn_trait_struct_type.rs @@ -1,14 +1,14 @@ trait Trait { fn method(&self); } -// impl Trait for i32 { -// fn method(&self) { -// assert!(*self > 0); -// } -// } +impl Trait for i32 { + fn method(&self) { + assert!(*self > 0); + } +} fn use_trait(t: &dyn Trait) { t.method(); } fn main() { - // use_trait(&100); + use_trait(&100); } \ No newline at end of file From 84c24fbadf8088a2000db3f14a58d52d79c2337c Mon Sep 17 00:00:00 2001 From: ssyram Date: Mon, 27 Oct 2025 17:26:42 +0800 Subject: [PATCH 02/16] fixed eurydice_glue Definitions of `sizeof`, `alignof` & `opaque` --- include/eurydice_glue.h | 6 +-- .../dyn_trait_struct_type.c | 52 ++++++++++++++++++- .../dyn_trait_struct_type.h | 23 +++++++- 3 files changed, 75 insertions(+), 6 deletions(-) diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index cbba21dc..c1909c7c 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -58,11 +58,11 @@ using std::type_identity_t; // SIZEOF, ALIGNOF -#define Eurydice_sizeof(t) sizeof(t) +#define Eurydice_sizeof(t, _) sizeof(t) -#define Eurydice_alignof(t) alignof(t) +#define Eurydice_alignof(t, _) _Alignof(t) -#define Eurydice_opaque(t, reason) *((t *)0) +#define Eurydice_opaque(reason, t, _) *((t *)0) // SLICES, ARRAYS, ETC. diff --git a/out/test-dyn_trait_struct_type/dyn_trait_struct_type.c b/out/test-dyn_trait_struct_type/dyn_trait_struct_type.c index 8319afe3..26177667 100644 --- a/out/test-dyn_trait_struct_type/dyn_trait_struct_type.c +++ b/out/test-dyn_trait_struct_type/dyn_trait_struct_type.c @@ -7,14 +7,64 @@ #include "dyn_trait_struct_type.h" -void dyn_trait_struct_type_main(void) +/** +This function found in impl {dyn_trait_struct_type::Trait for i32} +*/ +void dyn_trait_struct_type__vtable_drop_shim__80(Eurydice_dst_ref_06 dyn_self) +{ + +} + +/** +This function found in impl {dyn_trait_struct_type::Trait for i32} +*/ +void dyn_trait_struct_type_method_80(int32_t *self) { + EURYDICE_ASSERT(self[0U] > (int32_t)0, "panic!"); +} +/** +This function found in impl {dyn_trait_struct_type::Trait for i32} +*/ +void dyn_trait_struct_type_method__vtable_method__80(Eurydice_dst_ref_06 _) +{ + dyn_trait_struct_type_method_80((int32_t *)_.ptr); } +static size_t _vtable__local_0 = Eurydice_sizeof(int32_t, size_t); + +static size_t _vtable__local_1 = Eurydice_alignof(int32_t, size_t); + +static dyn_trait_struct_type_Trait__vtable_ +_vtable__local_2 = + { + .size = _vtable__local_0, .align = _vtable__local_1, + .drop = dyn_trait_struct_type__vtable_drop_shim__80, + .method_method = dyn_trait_struct_type_method__vtable_method__80, + .super_trait_0 = Eurydice_opaque("missing supertrait vtable", + core_marker_MetaSized__vtable_ *, + core_marker_MetaSized__vtable_ *) + }; + +const +dyn_trait_struct_type_Trait__vtable_ +dyn_trait_struct_type__dyn_trait_struct_type__Trait_for_i32___vtable_ = _vtable__local_2; + void dyn_trait_struct_type_use_trait(Eurydice_dst_ref_06 t) { Eurydice_dst_ref_06 uu____0 = t; uu____0.meta->method_method(uu____0); } +void dyn_trait_struct_type_main(void) +{ + /* original Rust expression is not an lvalue in C */ + int32_t lvalue = (int32_t)100; + dyn_trait_struct_type_use_trait(( + KRML_CLITERAL(Eurydice_dst_ref_06){ + .ptr = (Eurydice_c_void_t *)&lvalue, + .meta = &dyn_trait_struct_type__dyn_trait_struct_type__Trait_for_i32___vtable_ + } + )); +} + diff --git a/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h b/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h index dba39c63..d7c3b03a 100644 --- a/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h +++ b/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h @@ -37,8 +37,6 @@ typedef struct core_marker_MetaSized__vtable__s } core_marker_MetaSized__vtable_; -void dyn_trait_struct_type_main(void); - typedef struct dyn_trait_struct_type_Trait__vtable__s dyn_trait_struct_type_Trait__vtable_; /** @@ -63,8 +61,29 @@ typedef struct dyn_trait_struct_type_Trait__vtable__s } dyn_trait_struct_type_Trait__vtable_; +/** +This function found in impl {dyn_trait_struct_type::Trait for i32} +*/ +void dyn_trait_struct_type__vtable_drop_shim__80(Eurydice_dst_ref_06 dyn_self); + +/** +This function found in impl {dyn_trait_struct_type::Trait for i32} +*/ +void dyn_trait_struct_type_method_80(int32_t *self); + +/** +This function found in impl {dyn_trait_struct_type::Trait for i32} +*/ +void dyn_trait_struct_type_method__vtable_method__80(Eurydice_dst_ref_06 _); + +extern const +dyn_trait_struct_type_Trait__vtable_ +dyn_trait_struct_type__dyn_trait_struct_type__Trait_for_i32___vtable_; + void dyn_trait_struct_type_use_trait(Eurydice_dst_ref_06 t); +void dyn_trait_struct_type_main(void); + #if defined(__cplusplus) } #endif From fed098077f1a8036715a87194fc2864dd3a8bc8b Mon Sep 17 00:00:00 2001 From: ssyram Date: Mon, 27 Oct 2025 18:05:28 +0800 Subject: [PATCH 03/16] rename example --- test/{dyn_trait_struct_type.rs => dyn_trait.rs} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename test/{dyn_trait_struct_type.rs => dyn_trait.rs} (100%) diff --git a/test/dyn_trait_struct_type.rs b/test/dyn_trait.rs similarity index 100% rename from test/dyn_trait_struct_type.rs rename to test/dyn_trait.rs From 39f9d6ad96035f48d3a2ee74aa697b22b5b09586 Mon Sep 17 00:00:00 2001 From: ssyram Date: Mon, 27 Oct 2025 18:07:11 +0800 Subject: [PATCH 04/16] more on renaming example --- out/test-dyn_trait/dyn_trait.c | 69 ++++++++++++++ out/test-dyn_trait/dyn_trait.h | 90 ++++++++++++++++++ .../dyn_trait_struct_type.c | 70 -------------- .../dyn_trait_struct_type.h | 92 ------------------- 4 files changed, 159 insertions(+), 162 deletions(-) create mode 100644 out/test-dyn_trait/dyn_trait.c create mode 100644 out/test-dyn_trait/dyn_trait.h delete mode 100644 out/test-dyn_trait_struct_type/dyn_trait_struct_type.c delete mode 100644 out/test-dyn_trait_struct_type/dyn_trait_struct_type.h diff --git a/out/test-dyn_trait/dyn_trait.c b/out/test-dyn_trait/dyn_trait.c new file mode 100644 index 00000000..ea880705 --- /dev/null +++ b/out/test-dyn_trait/dyn_trait.c @@ -0,0 +1,69 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "dyn_trait.h" + +/** +This function found in impl {dyn_trait::Trait for i32} +*/ +void dyn_trait__vtable_drop_shim__92(Eurydice_dst_ref_dd dyn_self) +{ + +} + +/** +This function found in impl {dyn_trait::Trait for i32} +*/ +void dyn_trait_method_92(int32_t *self) +{ + EURYDICE_ASSERT(self[0U] > (int32_t)0, "panic!"); +} + +/** +This function found in impl {dyn_trait::Trait for i32} +*/ +void dyn_trait_method__vtable_method__92(Eurydice_dst_ref_dd _) +{ + dyn_trait_method_92((int32_t *)_.ptr); +} + +static size_t _vtable__local_0 = Eurydice_sizeof(int32_t, size_t); + +static size_t _vtable__local_1 = Eurydice_alignof(int32_t, size_t); + +static dyn_trait_Trait__vtable_ +_vtable__local_2 = + { + .size = _vtable__local_0, .align = _vtable__local_1, .drop = dyn_trait__vtable_drop_shim__92, + .method_method = dyn_trait_method__vtable_method__92, + .super_trait_0 = Eurydice_opaque("missing supertrait vtable", + core_marker_MetaSized__vtable_ *, + core_marker_MetaSized__vtable_ *) + }; + +const +dyn_trait_Trait__vtable_ +dyn_trait__dyn_trait__Trait_for_i32___vtable_ = _vtable__local_2; + +void dyn_trait_use_trait(Eurydice_dst_ref_dd t) +{ + Eurydice_dst_ref_dd uu____0 = t; + uu____0.meta->method_method(uu____0); +} + +void dyn_trait_main(void) +{ + /* original Rust expression is not an lvalue in C */ + int32_t lvalue = (int32_t)100; + dyn_trait_use_trait(( + KRML_CLITERAL(Eurydice_dst_ref_dd){ + .ptr = (Eurydice_c_void_t *)&lvalue, + .meta = &dyn_trait__dyn_trait__Trait_for_i32___vtable_ + } + )); +} + diff --git a/out/test-dyn_trait/dyn_trait.h b/out/test-dyn_trait/dyn_trait.h new file mode 100644 index 00000000..5475b13f --- /dev/null +++ b/out/test-dyn_trait/dyn_trait.h @@ -0,0 +1,90 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef dyn_trait_H +#define dyn_trait_H + +#include "eurydice_glue.h" + + +#if defined(__cplusplus) +extern "C" { +#endif + +typedef struct core_marker_MetaSized__vtable__s core_marker_MetaSized__vtable_; + +/** +A monomorphic instance of Eurydice.dst_ref +with types Eurydice_c_void_t, core_marker_MetaSized_{vtable}* + +*/ +typedef struct Eurydice_dst_ref_05_s +{ + Eurydice_c_void_t *ptr; + core_marker_MetaSized__vtable_ *meta; +} +Eurydice_dst_ref_05; + +typedef struct core_marker_MetaSized__vtable__s +{ + size_t size; + size_t align; + void (*drop)(Eurydice_dst_ref_05 x0); +} +core_marker_MetaSized__vtable_; + +typedef struct dyn_trait_Trait__vtable__s dyn_trait_Trait__vtable_; + +/** +A monomorphic instance of Eurydice.dst_ref +with types Eurydice_c_void_t, dyn_trait_Trait_{vtable}* + +*/ +typedef struct Eurydice_dst_ref_dd_s +{ + Eurydice_c_void_t *ptr; + dyn_trait_Trait__vtable_ *meta; +} +Eurydice_dst_ref_dd; + +typedef struct dyn_trait_Trait__vtable__s +{ + size_t size; + size_t align; + void (*drop)(Eurydice_dst_ref_dd x0); + void (*method_method)(Eurydice_dst_ref_dd x0); + core_marker_MetaSized__vtable_ *super_trait_0; +} +dyn_trait_Trait__vtable_; + +/** +This function found in impl {dyn_trait::Trait for i32} +*/ +void dyn_trait__vtable_drop_shim__92(Eurydice_dst_ref_dd dyn_self); + +/** +This function found in impl {dyn_trait::Trait for i32} +*/ +void dyn_trait_method_92(int32_t *self); + +/** +This function found in impl {dyn_trait::Trait for i32} +*/ +void dyn_trait_method__vtable_method__92(Eurydice_dst_ref_dd _); + +extern const dyn_trait_Trait__vtable_ dyn_trait__dyn_trait__Trait_for_i32___vtable_; + +void dyn_trait_use_trait(Eurydice_dst_ref_dd t); + +void dyn_trait_main(void); + +#if defined(__cplusplus) +} +#endif + +#define dyn_trait_H_DEFINED +#endif /* dyn_trait_H */ diff --git a/out/test-dyn_trait_struct_type/dyn_trait_struct_type.c b/out/test-dyn_trait_struct_type/dyn_trait_struct_type.c deleted file mode 100644 index 26177667..00000000 --- a/out/test-dyn_trait_struct_type/dyn_trait_struct_type.c +++ /dev/null @@ -1,70 +0,0 @@ -/* - This file was generated by KaRaMeL - - F* version: - - */ - -#include "dyn_trait_struct_type.h" - -/** -This function found in impl {dyn_trait_struct_type::Trait for i32} -*/ -void dyn_trait_struct_type__vtable_drop_shim__80(Eurydice_dst_ref_06 dyn_self) -{ - -} - -/** -This function found in impl {dyn_trait_struct_type::Trait for i32} -*/ -void dyn_trait_struct_type_method_80(int32_t *self) -{ - EURYDICE_ASSERT(self[0U] > (int32_t)0, "panic!"); -} - -/** -This function found in impl {dyn_trait_struct_type::Trait for i32} -*/ -void dyn_trait_struct_type_method__vtable_method__80(Eurydice_dst_ref_06 _) -{ - dyn_trait_struct_type_method_80((int32_t *)_.ptr); -} - -static size_t _vtable__local_0 = Eurydice_sizeof(int32_t, size_t); - -static size_t _vtable__local_1 = Eurydice_alignof(int32_t, size_t); - -static dyn_trait_struct_type_Trait__vtable_ -_vtable__local_2 = - { - .size = _vtable__local_0, .align = _vtable__local_1, - .drop = dyn_trait_struct_type__vtable_drop_shim__80, - .method_method = dyn_trait_struct_type_method__vtable_method__80, - .super_trait_0 = Eurydice_opaque("missing supertrait vtable", - core_marker_MetaSized__vtable_ *, - core_marker_MetaSized__vtable_ *) - }; - -const -dyn_trait_struct_type_Trait__vtable_ -dyn_trait_struct_type__dyn_trait_struct_type__Trait_for_i32___vtable_ = _vtable__local_2; - -void dyn_trait_struct_type_use_trait(Eurydice_dst_ref_06 t) -{ - Eurydice_dst_ref_06 uu____0 = t; - uu____0.meta->method_method(uu____0); -} - -void dyn_trait_struct_type_main(void) -{ - /* original Rust expression is not an lvalue in C */ - int32_t lvalue = (int32_t)100; - dyn_trait_struct_type_use_trait(( - KRML_CLITERAL(Eurydice_dst_ref_06){ - .ptr = (Eurydice_c_void_t *)&lvalue, - .meta = &dyn_trait_struct_type__dyn_trait_struct_type__Trait_for_i32___vtable_ - } - )); -} - diff --git a/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h b/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h deleted file mode 100644 index d7c3b03a..00000000 --- a/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h +++ /dev/null @@ -1,92 +0,0 @@ -/* - This file was generated by KaRaMeL - - F* version: - - */ - -#ifndef dyn_trait_struct_type_H -#define dyn_trait_struct_type_H - -#include "eurydice_glue.h" - - -#if defined(__cplusplus) -extern "C" { -#endif - -typedef struct core_marker_MetaSized__vtable__s core_marker_MetaSized__vtable_; - -/** -A monomorphic instance of Eurydice.dst_ref -with types Eurydice_c_void_t, core_marker_MetaSized_{vtable}* - -*/ -typedef struct Eurydice_dst_ref_05_s -{ - Eurydice_c_void_t *ptr; - core_marker_MetaSized__vtable_ *meta; -} -Eurydice_dst_ref_05; - -typedef struct core_marker_MetaSized__vtable__s -{ - size_t size; - size_t align; - void (*drop)(Eurydice_dst_ref_05 x0); -} -core_marker_MetaSized__vtable_; - -typedef struct dyn_trait_struct_type_Trait__vtable__s dyn_trait_struct_type_Trait__vtable_; - -/** -A monomorphic instance of Eurydice.dst_ref -with types Eurydice_c_void_t, dyn_trait_struct_type_Trait_{vtable}* - -*/ -typedef struct Eurydice_dst_ref_06_s -{ - Eurydice_c_void_t *ptr; - dyn_trait_struct_type_Trait__vtable_ *meta; -} -Eurydice_dst_ref_06; - -typedef struct dyn_trait_struct_type_Trait__vtable__s -{ - size_t size; - size_t align; - void (*drop)(Eurydice_dst_ref_06 x0); - void (*method_method)(Eurydice_dst_ref_06 x0); - core_marker_MetaSized__vtable_ *super_trait_0; -} -dyn_trait_struct_type_Trait__vtable_; - -/** -This function found in impl {dyn_trait_struct_type::Trait for i32} -*/ -void dyn_trait_struct_type__vtable_drop_shim__80(Eurydice_dst_ref_06 dyn_self); - -/** -This function found in impl {dyn_trait_struct_type::Trait for i32} -*/ -void dyn_trait_struct_type_method_80(int32_t *self); - -/** -This function found in impl {dyn_trait_struct_type::Trait for i32} -*/ -void dyn_trait_struct_type_method__vtable_method__80(Eurydice_dst_ref_06 _); - -extern const -dyn_trait_struct_type_Trait__vtable_ -dyn_trait_struct_type__dyn_trait_struct_type__Trait_for_i32___vtable_; - -void dyn_trait_struct_type_use_trait(Eurydice_dst_ref_06 t); - -void dyn_trait_struct_type_main(void); - -#if defined(__cplusplus) -} -#endif - -#define dyn_trait_struct_type_H_DEFINED -#endif /* dyn_trait_struct_type_H */ From bdc0d6496349f5aa547635bee665361b2b993f0f Mon Sep 17 00:00:00 2001 From: ssyram Date: Thu, 30 Oct 2025 15:34:20 +0800 Subject: [PATCH 05/16] updated as per advised --- include/eurydice_glue.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index c1909c7c..318e5cd1 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -62,7 +62,7 @@ using std::type_identity_t; #define Eurydice_alignof(t, _) _Alignof(t) -#define Eurydice_opaque(reason, t, _) *((t *)0) +#define Eurydice_opaque(reason, t, _) KRML_EABORT(t, reason) // SLICES, ARRAYS, ETC. From 88e28d9613523f1c9a30e29ab09ad897493fb27e Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Fri, 31 Oct 2025 10:58:27 +0800 Subject: [PATCH 06/16] first attempt on support generics in IdGlobal --- lib/AstOfLlbc.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 802dc4eb..9cf1d0c1 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -2630,7 +2630,8 @@ let decl_of_id (env : env) (id : C.item_id) : K.decl option = body )))) | IdGlobal id -> let global = env.get_nth_global id in - let { C.item_meta; ty; def_id; _ } = global in + let { C.item_meta; generics; ty; def_id; _ } = global in + let env = { env with generic_params = generics } in let name = item_meta.name in let def = env.get_nth_global def_id in L.log "AstOfLlbc" "Visiting global: %s\n%s" (string_of_name env name) @@ -2657,6 +2658,7 @@ let decl_of_id (env : env) (id : C.item_id) : K.decl option = [] in let body = env.get_nth_function def.init in + let env = push_type_binders env generics.types in L.log "AstOfLlbc" "Corresponding body:%s" (Charon.PrintLlbcAst.Ast.fun_decl_to_string env.format_env " " " " body); begin From 0e1ad9c444beff80689dc90a5382c5f0a99226ba Mon Sep 17 00:00:00 2001 From: ssyram Date: Fri, 31 Oct 2025 14:31:46 +0800 Subject: [PATCH 07/16] further fix: handles also CGs --- lib/AstOfLlbc.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 9cf1d0c1..f45e18b2 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -2658,6 +2658,7 @@ let decl_of_id (env : env) (id : C.item_id) : K.decl option = [] in let body = env.get_nth_function def.init in + let env = push_cg_binders env generics.const_generics in let env = push_type_binders env generics.types in L.log "AstOfLlbc" "Corresponding body:%s" (Charon.PrintLlbcAst.Ast.fun_decl_to_string env.format_env " " " " body); From 1eeb7fac422729bd6b9f080109ea59e283560e2d Mon Sep 17 00:00:00 2001 From: ssyram Date: Fri, 31 Oct 2025 16:20:17 +0800 Subject: [PATCH 08/16] Add generics to global decl --- lib/AstOfLlbc.ml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index f45e18b2..ec1cd946 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -2665,13 +2665,27 @@ let decl_of_id (env : env) (id : C.item_id) : K.decl option = begin match body.body with | Some body -> + if List.length generics.const_generics <> 0 then + fail + "Global variables with const generics are not supported, please consider using \ + mono LLBC: %s" + (string_of_name env name); let ret_var = List.hd body.locals.locals in let body = with_locals env ty body.locals.locals (fun env -> expression_of_block env ret_var.index body.body) in - Some (K.DGlobal (flags, lid_of_name env name, 0, ty, body)) - | None -> Some (K.DExternal (None, [], 0, 0, lid_of_name env name, ty, [])) + Some (K.DGlobal (flags, lid_of_name env name, List.length generics.types, ty, body)) + | None -> + Some + (K.DExternal + ( None, + [], + List.length generics.const_generics, + List.length generics.types, + lid_of_name env name, + ty, + [] )) end | IdTraitDecl _ | IdTraitImpl _ -> None From 5fa9ee8fed3ee6ec04766be6521a46f08cd6ba07 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Tue, 4 Nov 2025 14:44:41 +0800 Subject: [PATCH 09/16] wip:trying to add ETApp for generic vtable pointer --- lib/AstOfLlbc.ml | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 8fba6f83..d13355b9 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -1873,13 +1873,15 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = let trait_impl = env.get_nth_trait_impl id in begin match trait_impl.vtable with - | Some instance -> { instance with C.generics } + | Some instance -> { instance with generics } | None -> failwith "Trait impl has no vtable instance" end | _ -> failwith "unsupported trait_ref kind in unsize cast" in let instance_def = env.get_nth_global vtable_instance.C.id in - let instance_ty = + let generic_typs = List.map (typ_of_ty env) vtable_instance.generics.types in + let cgs = List.map (expression_of_const_generic env) vtable_instance.generics.const_generics in + let ret_typ = let subst = Charon.Substitute.make_subst_from_generics instance_def.generics vtable_instance.generics @@ -1887,9 +1889,19 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = let real_ty = Charon.Substitute.(ty_substitute subst instance_def.ty) in typ_of_ty env real_ty in - let vtable_instance = + L.log "Ast" "[debug] ret_typ:%a\n" ptyp ret_typ; + (* let ret_typ = typ_of_ty env instance_def.ty in *) + let instance_ty = + let ts = { K.n = List.length generic_typs; K.n_cgs = List.length cgs } in + K.TPoly (ts, ret_typ) + (* List.fold_right (fun t acc -> K.TArrow (t, acc)) generic_typs ret_typ *) + in + let vtable_func_head = K.with_type instance_ty (K.EQualified (lid_of_name env instance_def.item_meta.name)) in + let vtable_instance = + K.with_type ret_typ (K.ETApp (vtable_func_head, cgs, [], generic_typs)) + in addrof vtable_instance in let coercion = From 0b8d6803b386dc50c4ec120442d5c75ab64bbe70 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Mon, 10 Nov 2025 19:45:51 +0800 Subject: [PATCH 10/16] Revert "wip:trying to add ETApp for generic vtable pointer" This reverts commit 5fa9ee8fed3ee6ec04766be6521a46f08cd6ba07. --- lib/AstOfLlbc.ml | 18 +++--------------- 1 file changed, 3 insertions(+), 15 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index f8841295..cd96b7b5 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -1871,15 +1871,13 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = let trait_impl = env.get_nth_trait_impl id in begin match trait_impl.vtable with - | Some instance -> { instance with generics } + | Some instance -> { instance with C.generics } | None -> failwith "Trait impl has no vtable instance" end | _ -> failwith "unsupported trait_ref kind in unsize cast" in let instance_def = env.get_nth_global vtable_instance.C.id in - let generic_typs = List.map (typ_of_ty env) vtable_instance.generics.types in - let cgs = List.map (expression_of_const_generic env) vtable_instance.generics.const_generics in - let ret_typ = + let instance_ty = let subst = Charon.Substitute.make_subst_from_generics instance_def.generics vtable_instance.generics @@ -1887,18 +1885,8 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = let real_ty = Charon.Substitute.(ty_substitute subst instance_def.ty) in typ_of_ty env real_ty in - L.log "Ast" "[debug] ret_typ:%a\n" ptyp ret_typ; - (* let ret_typ = typ_of_ty env instance_def.ty in *) - let instance_ty = - let ts = { K.n = List.length generic_typs; K.n_cgs = List.length cgs } in - K.TPoly (ts, ret_typ) - (* List.fold_right (fun t acc -> K.TArrow (t, acc)) generic_typs ret_typ *) - in - let vtable_func_head = - K.with_type instance_ty (K.EQualified (lid_of_name env instance_def.item_meta.name)) - in let vtable_instance = - K.with_type ret_typ (K.ETApp (vtable_func_head, cgs, [], generic_typs)) + K.with_type instance_ty (K.EQualified (lid_of_name env instance_def.item_meta.name)) in addrof vtable_instance in From a7149888c1fc86734bcafac5d4b9d682922f86ad Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Wed, 12 Nov 2025 11:27:49 +0800 Subject: [PATCH 11/16] first attempt on aggressively inlining [ELet]s in DGlobal --- bin/main.ml | 12 +++++++----- lib/Cleanup2.ml | 20 ++++++++++++++++++++ 2 files changed, 27 insertions(+), 5 deletions(-) diff --git a/bin/main.ml b/bin/main.ml index efbb1b5d..6bb65e9f 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -227,8 +227,9 @@ Supported options:|} (* Following the krml order of phases here *) let files = Krml.Inlining.inline_type_abbrevs files in let files = Krml.Monomorphization.functions files in - Eurydice.Logging.log "Phase2.12" "%a" pfiles files; + Eurydice.Logging.log "Phase2.12" "2.12%a" pfiles files; let files = Krml.Simplify.optimize_lets files in + Eurydice.Logging.log "Phase2.12" "2.121%a" pfiles files; let files = Krml.DataTypes.simplify files in (* Must happen now, before Monomorphization.datatypes, because otherwise MonomorphizationState.state gets filled with lids that later on get eliminated on the basis @@ -237,7 +238,7 @@ Supported options:|} let files = Krml.Monomorphization.datatypes 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; + Eurydice.Logging.log "Phase2.13" "2.13%a" pfiles files; let files = Krml.Inlining.inline files in let files = match config with @@ -292,15 +293,16 @@ Supported options:|} (* These two need to come before... *) let files = Krml.Inlining.cross_call_analysis files in let files = Krml.Simplify.remove_unused files in - Eurydice.Logging.log "Phase2.7" "%a" pfiles files; + Eurydice.Logging.log "Phase2.7" "2.7%a" pfiles files; + let files = Eurydice.Cleanup2.aggressive_inlining_lets_global#visit_files () files in (* This chunk which reuses key elements of simplify2 *) let files = Eurydice.Cleanup2.check_addrof#visit_files () files in let files = Krml.Simplify.sequence_to_let#visit_files () files in let files = Eurydice.Cleanup2.hoist#visit_files [] files in let files = Eurydice.Cleanup2.fixup_hoist#visit_files () files in - Eurydice.Logging.log "Phase2.75" "%a" pfiles files; + Eurydice.Logging.log "Phase2.75" "2.75%a" pfiles files; let files = Eurydice.Cleanup2.globalize_global_locals files in - Eurydice.Logging.log "Phase2.8" "%a" pfiles files; + Eurydice.Logging.log "Phase2.8" "2.8%a" pfiles files; let files = Eurydice.Cleanup2.reconstruct_for_loops#visit_files () files in let files = Krml.Simplify.misc_cosmetic#visit_files () files in let files = Krml.Simplify.let_to_sequence#visit_files () files in diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 20b227da..f9a5f343 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -1212,6 +1212,26 @@ let fixup_hoist = DGlobal (flags, name, n, ret, Krml.Simplify.fixup_return_pos expr) end +(* For the [DGlobal], we do the following two inlining of [let] in order to + avoid the non-constant initializer of struct fields *) +let aggressive_inlining_lets_global = + object (self) + inherit [_] map + + method private optimize_ELet _b e1 e2 = + match e2.node with + | EBound 0 -> e1.node + | _ -> (Krml.DeBruijn.subst e1 0 e2).node + + method! visit_DGlobal () flags name n ret expr = + let rec optimize_expr expr = + match expr.node with + | ELet (b, e1, e2) -> with_type expr.typ (self#optimize_ELet b e1 (optimize_expr e2)) + | _ -> expr + in + DGlobal (flags, name, n, ret, optimize_expr expr) + end + (** For any [DGlobal], if the expression has any locals remaining We should let them also be globals, so to make the overall expr valid. From dd341af6534c0234ace5baf55ba1b37a4121e5f4 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Tue, 18 Nov 2025 12:58:47 +0800 Subject: [PATCH 12/16] minor: the ptr field in vtable ptr should not be const --- lib/AstOfLlbc.ml | 4 +++- out/test-dyn_trait/dyn_trait.c | 35 ++++++++++++++-------------------- out/test-dyn_trait/dyn_trait.h | 28 +++++++++++++-------------- 3 files changed, 31 insertions(+), 36 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 83718bf3..f63a8658 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -547,6 +547,7 @@ and ptr_typ_of_ty (env : env) ~const (ty : Charon.Types.ty) : K.typ = | TAdt { id = TBuiltin TStr; _ } -> Builtin.str_t ~const (* Special case to handle DynTrait *) | TDynTrait pred -> + let const = false in Builtin.mk_dst_ref ~const Builtin.c_void_t (K.TBuf (vtable_typ_of_dyn_pred env pred, false)) (* General case, all &T is turned to either thin T* or fat Eurydice::DstRef *) | _ -> ( @@ -1961,7 +1962,8 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = (K.ETApp (array_to_slice, [ len ], [], [ t ])) in K.(with_type (Builtin.mk_slice ~const t) (EApp (array_to_slice, [ e ]))) - | MetaVTablePtr trait_ref, TBuf (_, const), _ -> + | MetaVTablePtr trait_ref, TBuf (_, _), _ -> + let const = false in (* Cast from T to T where Unsized is a user-defined DST. We build the vtable pointer for the trait object here. *) (* TODO: I'm not sure whether this should be for vtable instance for now *) diff --git a/out/test-dyn_trait/dyn_trait.c b/out/test-dyn_trait/dyn_trait.c index ea880705..5c62eddb 100644 --- a/out/test-dyn_trait/dyn_trait.c +++ b/out/test-dyn_trait/dyn_trait.c @@ -10,7 +10,7 @@ /** This function found in impl {dyn_trait::Trait for i32} */ -void dyn_trait__vtable_drop_shim__92(Eurydice_dst_ref_dd dyn_self) +void dyn_trait__vtable_drop_shim__92(Eurydice_dst_ref_mut_dd dyn_self) { } @@ -18,7 +18,7 @@ void dyn_trait__vtable_drop_shim__92(Eurydice_dst_ref_dd dyn_self) /** This function found in impl {dyn_trait::Trait for i32} */ -void dyn_trait_method_92(int32_t *self) +void dyn_trait_method_92(const int32_t *self) { EURYDICE_ASSERT(self[0U] > (int32_t)0, "panic!"); } @@ -26,32 +26,25 @@ void dyn_trait_method_92(int32_t *self) /** This function found in impl {dyn_trait::Trait for i32} */ -void dyn_trait_method__vtable_method__92(Eurydice_dst_ref_dd _) +void dyn_trait_method__vtable_method__92(Eurydice_dst_ref_mut_dd _) { - dyn_trait_method_92((int32_t *)_.ptr); + dyn_trait_method_92((const int32_t *)_.ptr); } -static size_t _vtable__local_0 = Eurydice_sizeof(int32_t, size_t); - -static size_t _vtable__local_1 = Eurydice_alignof(int32_t, size_t); - -static dyn_trait_Trait__vtable_ -_vtable__local_2 = +const +dyn_trait_Trait__vtable_ +dyn_trait__dyn_trait__Trait_for_i32___vtable_ = { - .size = _vtable__local_0, .align = _vtable__local_1, .drop = dyn_trait__vtable_drop_shim__92, - .method_method = dyn_trait_method__vtable_method__92, + .size = Eurydice_sizeof(int32_t, size_t), .align = Eurydice_alignof(int32_t, size_t), + .drop = dyn_trait__vtable_drop_shim__92, .method_method = dyn_trait_method__vtable_method__92, .super_trait_0 = Eurydice_opaque("missing supertrait vtable", - core_marker_MetaSized__vtable_ *, - core_marker_MetaSized__vtable_ *) + const core_marker_MetaSized__vtable_ *, + const core_marker_MetaSized__vtable_ *) }; -const -dyn_trait_Trait__vtable_ -dyn_trait__dyn_trait__Trait_for_i32___vtable_ = _vtable__local_2; - -void dyn_trait_use_trait(Eurydice_dst_ref_dd t) +void dyn_trait_use_trait(Eurydice_dst_ref_mut_dd t) { - Eurydice_dst_ref_dd uu____0 = t; + Eurydice_dst_ref_mut_dd uu____0 = t; uu____0.meta->method_method(uu____0); } @@ -60,7 +53,7 @@ void dyn_trait_main(void) /* original Rust expression is not an lvalue in C */ int32_t lvalue = (int32_t)100; dyn_trait_use_trait(( - KRML_CLITERAL(Eurydice_dst_ref_dd){ + KRML_CLITERAL(Eurydice_dst_ref_mut_dd){ .ptr = (Eurydice_c_void_t *)&lvalue, .meta = &dyn_trait__dyn_trait__Trait_for_i32___vtable_ } diff --git a/out/test-dyn_trait/dyn_trait.h b/out/test-dyn_trait/dyn_trait.h index 5475b13f..7124eed5 100644 --- a/out/test-dyn_trait/dyn_trait.h +++ b/out/test-dyn_trait/dyn_trait.h @@ -18,67 +18,67 @@ extern "C" { typedef struct core_marker_MetaSized__vtable__s core_marker_MetaSized__vtable_; /** -A monomorphic instance of Eurydice.dst_ref +A monomorphic instance of Eurydice.dst_ref_mut with types Eurydice_c_void_t, core_marker_MetaSized_{vtable}* */ -typedef struct Eurydice_dst_ref_05_s +typedef struct Eurydice_dst_ref_mut_05_s { Eurydice_c_void_t *ptr; core_marker_MetaSized__vtable_ *meta; } -Eurydice_dst_ref_05; +Eurydice_dst_ref_mut_05; typedef struct core_marker_MetaSized__vtable__s { size_t size; size_t align; - void (*drop)(Eurydice_dst_ref_05 x0); + void (*drop)(Eurydice_dst_ref_mut_05 x0); } core_marker_MetaSized__vtable_; typedef struct dyn_trait_Trait__vtable__s dyn_trait_Trait__vtable_; /** -A monomorphic instance of Eurydice.dst_ref +A monomorphic instance of Eurydice.dst_ref_mut with types Eurydice_c_void_t, dyn_trait_Trait_{vtable}* */ -typedef struct Eurydice_dst_ref_dd_s +typedef struct Eurydice_dst_ref_mut_dd_s { Eurydice_c_void_t *ptr; dyn_trait_Trait__vtable_ *meta; } -Eurydice_dst_ref_dd; +Eurydice_dst_ref_mut_dd; typedef struct dyn_trait_Trait__vtable__s { size_t size; size_t align; - void (*drop)(Eurydice_dst_ref_dd x0); - void (*method_method)(Eurydice_dst_ref_dd x0); - core_marker_MetaSized__vtable_ *super_trait_0; + void (*drop)(Eurydice_dst_ref_mut_dd x0); + void (*method_method)(Eurydice_dst_ref_mut_dd x0); + const core_marker_MetaSized__vtable_ *super_trait_0; } dyn_trait_Trait__vtable_; /** This function found in impl {dyn_trait::Trait for i32} */ -void dyn_trait__vtable_drop_shim__92(Eurydice_dst_ref_dd dyn_self); +void dyn_trait__vtable_drop_shim__92(Eurydice_dst_ref_mut_dd dyn_self); /** This function found in impl {dyn_trait::Trait for i32} */ -void dyn_trait_method_92(int32_t *self); +void dyn_trait_method_92(const int32_t *self); /** This function found in impl {dyn_trait::Trait for i32} */ -void dyn_trait_method__vtable_method__92(Eurydice_dst_ref_dd _); +void dyn_trait_method__vtable_method__92(Eurydice_dst_ref_mut_dd _); extern const dyn_trait_Trait__vtable_ dyn_trait__dyn_trait__Trait_for_i32___vtable_; -void dyn_trait_use_trait(Eurydice_dst_ref_dd t); +void dyn_trait_use_trait(Eurydice_dst_ref_mut_dd t); void dyn_trait_main(void); From 194a6f847505cb07cf668d7e14946605ac4d88ac Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Tue, 18 Nov 2025 14:00:41 +0800 Subject: [PATCH 13/16] minor --- lib/AstOfLlbc.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index f63a8658..bd96f98b 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -547,8 +547,8 @@ and ptr_typ_of_ty (env : env) ~const (ty : Charon.Types.ty) : K.typ = | TAdt { id = TBuiltin TStr; _ } -> Builtin.str_t ~const (* Special case to handle DynTrait *) | TDynTrait pred -> - let const = false in - Builtin.mk_dst_ref ~const Builtin.c_void_t (K.TBuf (vtable_typ_of_dyn_pred env pred, false)) + Builtin.mk_dst_ref ~const:false Builtin.c_void_t + (K.TBuf (vtable_typ_of_dyn_pred env pred, false)) (* General case, all &T is turned to either thin T* or fat Eurydice::DstRef *) | _ -> ( let typ = typ_of_ty env ty in @@ -1963,7 +1963,6 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = in K.(with_type (Builtin.mk_slice ~const t) (EApp (array_to_slice, [ e ]))) | MetaVTablePtr trait_ref, TBuf (_, _), _ -> - let const = false in (* Cast from T to T where Unsized is a user-defined DST. We build the vtable pointer for the trait object here. *) (* TODO: I'm not sure whether this should be for vtable instance for now *) @@ -1991,7 +1990,7 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = let vtable_instance = K.with_type instance_ty (K.EQualified (lid_of_name env instance_def.item_meta.name)) in - addrof ~const vtable_instance + addrof ~const:false vtable_instance in let coercion = K.with_type @@ -2002,7 +2001,7 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = as `e` itself is already the target, not its reference *) K.( with_type - (Builtin.mk_dst_ref ~const Builtin.c_void_t vtable_ptr.typ) + (Builtin.mk_dst_ref ~const:false Builtin.c_void_t vtable_ptr.typ) (EFlat [ Some "ptr", coercion; Some "meta", vtable_ptr ])) | _, _, _ -> Krml.KPrint.bprintf "t_to = %a\n" ptyp t_to; From 6331fe1716422274f889de75fee4a752baea7bcc Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Tue, 18 Nov 2025 23:33:06 +0800 Subject: [PATCH 14/16] updated [const] flag for IdGlobal --- lib/AstOfLlbc.ml | 15 +-------------- out/test-dyn_trait/dyn_trait.c | 1 - out/test-dyn_trait/dyn_trait.h | 2 +- 3 files changed, 2 insertions(+), 16 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index bd96f98b..aa100393 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -2746,21 +2746,8 @@ let decl_of_id (env : env) (id : C.item_id) : K.decl option = (Charon.PrintLlbcAst.Ast.global_decl_to_string env.format_env " " " " def); let ty = typ_of_ty env ty in let flags = - [ Krml.Common.Const "" ] - @ match global.global_kind with - | NamedConst | AnonConst -> - (* This is trickier: const can be evaluated at compile-time, so in theory, we could just - emit a macro, except (!) in C, arrays need to be top-level declarations (not macros) - because even with compound literals, you can't do `((int[1]){0})[0]` in expression - position. - - We can't use the test "is_bufcreate" because the expression might only be a bufcreate - *after* simplification, so we rely on the type here. *) - if Krml.Helpers.is_array ty then - [] - else - [ Macro ] + | NamedConst | AnonConst -> [ Krml.Common.Const ""; Krml.Common.Macro ] | Static -> (* This one needs to have an address, so definitely not emitting it as a macro. *) [] diff --git a/out/test-dyn_trait/dyn_trait.c b/out/test-dyn_trait/dyn_trait.c index 5c62eddb..a8573f26 100644 --- a/out/test-dyn_trait/dyn_trait.c +++ b/out/test-dyn_trait/dyn_trait.c @@ -31,7 +31,6 @@ void dyn_trait_method__vtable_method__92(Eurydice_dst_ref_mut_dd _) dyn_trait_method_92((const int32_t *)_.ptr); } -const dyn_trait_Trait__vtable_ dyn_trait__dyn_trait__Trait_for_i32___vtable_ = { diff --git a/out/test-dyn_trait/dyn_trait.h b/out/test-dyn_trait/dyn_trait.h index 7124eed5..ff71274c 100644 --- a/out/test-dyn_trait/dyn_trait.h +++ b/out/test-dyn_trait/dyn_trait.h @@ -76,7 +76,7 @@ This function found in impl {dyn_trait::Trait for i32} */ void dyn_trait_method__vtable_method__92(Eurydice_dst_ref_mut_dd _); -extern const dyn_trait_Trait__vtable_ dyn_trait__dyn_trait__Trait_for_i32___vtable_; +extern dyn_trait_Trait__vtable_ dyn_trait__dyn_trait__Trait_for_i32___vtable_; void dyn_trait_use_trait(Eurydice_dst_ref_mut_dd t); From 5e8e25986a195fdb306274696193476924c0c9e0 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Wed, 19 Nov 2025 17:26:31 +0800 Subject: [PATCH 15/16] an Adhoc definition of [Eurydice_opaque] to pass the test --- include/eurydice_glue.h | 2 +- out/test-global_ref/global_ref.c | 2 +- out/test-global_ref/global_ref.h | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index 673c03f3..3c84d34e 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -62,7 +62,7 @@ using std::type_identity_t; #define Eurydice_alignof(t, _) _Alignof(t) -#define Eurydice_opaque(reason, t, _) KRML_EABORT(t, reason) +#define Eurydice_opaque(reason, t, _) (t)0 // SLICES, ARRAYS, ETC. diff --git a/out/test-global_ref/global_ref.c b/out/test-global_ref/global_ref.c index b15c6ce0..9889a266 100644 --- a/out/test-global_ref/global_ref.c +++ b/out/test-global_ref/global_ref.c @@ -19,7 +19,7 @@ static const int32_t *S_VAL_local_1 = &S_VAL_local_0; static const int32_t *const *S_VAL_local_2 = &S_VAL_local_1; -const int32_t *const *const *const global_ref_S_VAL = &S_VAL_local_2; +const int32_t *const *const *global_ref_S_VAL = &S_VAL_local_2; typedef struct const_____x2_s { diff --git a/out/test-global_ref/global_ref.h b/out/test-global_ref/global_ref.h index 99f390ed..16bfb0a3 100644 --- a/out/test-global_ref/global_ref.h +++ b/out/test-global_ref/global_ref.h @@ -28,7 +28,7 @@ extern void *const *const *global_ref_C_VAL_local_2; #define GLOBAL_REF_C_VAL (&global_ref_C_VAL_local_2) -extern const int32_t *const *const *const global_ref_S_VAL; +extern const int32_t *const *const *global_ref_S_VAL; void global_ref_main(void); From 0420fbb85bbbaedada1208ae386721004b1ed9e5 Mon Sep 17 00:00:00 2001 From: Ling Zhang Date: Wed, 3 Dec 2025 17:43:35 +0800 Subject: [PATCH 16/16] wip: strange duplicated typedefs in dyn_trait.h --- out/test-dyn_trait/dyn_trait.h | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/out/test-dyn_trait/dyn_trait.h b/out/test-dyn_trait/dyn_trait.h index ff71274c..59606875 100644 --- a/out/test-dyn_trait/dyn_trait.h +++ b/out/test-dyn_trait/dyn_trait.h @@ -17,6 +17,8 @@ extern "C" { typedef struct core_marker_MetaSized__vtable__s core_marker_MetaSized__vtable_; +typedef struct core_marker_MetaSized__vtable__s core_marker_MetaSized__vtable_; + /** A monomorphic instance of Eurydice.dst_ref_mut with types Eurydice_c_void_t, core_marker_MetaSized_{vtable}* @@ -29,6 +31,8 @@ typedef struct Eurydice_dst_ref_mut_05_s } Eurydice_dst_ref_mut_05; +typedef struct core_marker_MetaSized__vtable__s core_marker_MetaSized__vtable_; + typedef struct core_marker_MetaSized__vtable__s { size_t size; @@ -39,6 +43,8 @@ core_marker_MetaSized__vtable_; typedef struct dyn_trait_Trait__vtable__s dyn_trait_Trait__vtable_; +typedef struct dyn_trait_Trait__vtable__s dyn_trait_Trait__vtable_; + /** A monomorphic instance of Eurydice.dst_ref_mut with types Eurydice_c_void_t, dyn_trait_Trait_{vtable}* @@ -51,6 +57,12 @@ typedef struct Eurydice_dst_ref_mut_dd_s } Eurydice_dst_ref_mut_dd; +typedef struct dyn_trait_Trait__vtable__s dyn_trait_Trait__vtable_; + +typedef struct dyn_trait_Trait__vtable__s dyn_trait_Trait__vtable_; + +typedef struct dyn_trait_Trait__vtable__s dyn_trait_Trait__vtable_; + typedef struct dyn_trait_Trait__vtable__s { size_t size;