diff --git a/bin/main.ml b/bin/main.ml index b5c76050..69a088b0 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -207,7 +207,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 @@ -230,8 +230,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 @@ -240,7 +241,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 @@ -295,15 +296,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/include/eurydice_glue.h b/include/eurydice_glue.h index 8aaaf623..ff6b3944 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -58,9 +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(reason, t, _) (t)0 // SLICES, ARRAYS, ETC. diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 8c392013..1f2d6051 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -566,7 +566,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 -> - 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 @@ -1784,6 +1785,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) @@ -1898,10 +1902,14 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = mk_reference ~const:(const_of_ref_kind rk) 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)) @@ -1964,6 +1972,47 @@ 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 (_, _), _ -> + (* 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 *) + 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 ~const:false 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 ~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; Krml.KPrint.bprintf "destruct_arr_dst_ref t_to = None? %b\n" @@ -2697,45 +2746,49 @@ 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) (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. *) [] 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); 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 diff --git a/lib/Builtin.ml b/lib/Builtin.ml index b700e233..87da5eee 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -229,7 +229,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 = []; @@ -240,12 +240,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 suffix_of_const const = if const then "_shared" @@ -908,6 +922,7 @@ let builtin_funcs = [ sizeof; alignof; + opaque; array_repeat; array_eq; array_eq_slice_mut; diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index c2521b7c..0d0ac244 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -1242,6 +1242,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. diff --git a/out/test-dyn_trait/dyn_trait.c b/out/test-dyn_trait/dyn_trait.c new file mode 100644 index 00000000..a8573f26 --- /dev/null +++ b/out/test-dyn_trait/dyn_trait.c @@ -0,0 +1,61 @@ +/* + 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_mut_dd dyn_self) +{ + +} + +/** +This function found in impl {dyn_trait::Trait for i32} +*/ +void dyn_trait_method_92(const 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_mut_dd _) +{ + dyn_trait_method_92((const int32_t *)_.ptr); +} + +dyn_trait_Trait__vtable_ +dyn_trait__dyn_trait__Trait_for_i32___vtable_ = + { + .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", + const core_marker_MetaSized__vtable_ *, + const core_marker_MetaSized__vtable_ *) + }; + +void dyn_trait_use_trait(Eurydice_dst_ref_mut_dd t) +{ + Eurydice_dst_ref_mut_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_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 new file mode 100644 index 00000000..59606875 --- /dev/null +++ b/out/test-dyn_trait/dyn_trait.h @@ -0,0 +1,102 @@ +/* + 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_; + +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}* + +*/ +typedef struct Eurydice_dst_ref_mut_05_s +{ + Eurydice_c_void_t *ptr; + core_marker_MetaSized__vtable_ *meta; +} +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; + size_t align; + void (*drop)(Eurydice_dst_ref_mut_05 x0); +} +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}* + +*/ +typedef struct Eurydice_dst_ref_mut_dd_s +{ + Eurydice_c_void_t *ptr; + dyn_trait_Trait__vtable_ *meta; +} +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; + size_t align; + 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_mut_dd dyn_self); + +/** +This function found in impl {dyn_trait::Trait for i32} +*/ +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_mut_dd _); + +extern dyn_trait_Trait__vtable_ dyn_trait__dyn_trait__Trait_for_i32___vtable_; + +void dyn_trait_use_trait(Eurydice_dst_ref_mut_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-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); diff --git a/test/dyn_trait.rs b/test/dyn_trait.rs new file mode 100644 index 00000000..90efcca8 --- /dev/null +++ b/test/dyn_trait.rs @@ -0,0 +1,14 @@ +trait Trait { + fn method(&self); +} +impl Trait for i32 { + fn method(&self) { + assert!(*self > 0); + } +} +fn use_trait(t: &dyn Trait) { + t.method(); +} +fn main() { + use_trait(&100); +} \ No newline at end of file diff --git a/test/dyn_trait_struct_type.rs b/test/dyn_trait_struct_type.rs deleted file mode 100644 index c72f0195..00000000 --- a/test/dyn_trait_struct_type.rs +++ /dev/null @@ -1,16 +0,0 @@ -trait Trait { - fn method(&self); -} - -// impl Trait for i32 { -// fn method(&self) { -// assert!(*self > 0); -// } -// } - -fn use_trait(t: &dyn Trait) { - t.method(); -} -fn main() { - // use_trait(&100); -} \ No newline at end of file