Vtable Instance Support

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

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.
 

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<T,Meta> *)
   | _ -> (
       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<Sized> to T<Unsized> 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
 

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;

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.
 

out/test-dyn_trait/dyn_trait.c

@@ -0,0 +1,61 @@
+/* 
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+
+  F* version: <unknown>
+
+ */
+
+#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_
+      }
+    ));
+}
+