Better Unsized Type support

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.129"
+let supported_charon_version = "0.1.130"

charon-ml/src/ExpressionsUtils.ml

@@ -1,7 +1,7 @@
 open Expressions
 
 let unop_can_fail : unop -> bool = function
-  | Neg (OPanic | OUB) | Cast _ | PtrMetadata -> true
+  | Neg (OPanic | OUB) | Cast _ -> true
   | Neg OWrap | Not -> false
 
 let binop_can_fail : binop -> bool = function

charon-ml/src/GAst.ml

@@ -53,5 +53,6 @@ type 'fun_body gcrate = {
   global_decls : global_decl GlobalDeclId.Map.t;
   trait_decls : trait_decl TraitDeclId.Map.t;
   trait_impls : trait_impl TraitImplId.Map.t;
+  unit_metadata : global_decl_ref;
 }
 [@@deriving show]

charon-ml/src/GAstOfJson.ml

@@ -96,6 +96,7 @@ and gtranslated_crate_of_json
           ("global_decls", globals);
           ("trait_decls", trait_decls);
           ("trait_impls", trait_impls);
+          ("unit_metadata", unit_metadata);
           ("ordered_decls", declarations);
         ] ->
         let* ctx = id_to_file_of_json files in
@@ -126,6 +127,7 @@ and gtranslated_crate_of_json
           vector_of_json trait_impl_id_of_json trait_impl_of_json ctx
             trait_impls
         in
+        let* unit_metadata = global_decl_ref_of_json ctx unit_metadata in
 
         let type_decls =
           TypeDeclId.Map.of_list
@@ -159,6 +161,7 @@ and gtranslated_crate_of_json
             global_decls;
             trait_decls;
             trait_impls;
+            unit_metadata;
           }
     | _ -> Error "")
 

charon-ml/src/LlbcAstUtils.ml

@@ -207,6 +207,7 @@ class ['self] map_crate_with_span =
         global_decls;
         trait_decls;
         trait_impls;
+        unit_metadata;
       } =
         crate
       in
@@ -235,6 +236,9 @@ class ['self] map_crate_with_span =
       let trait_impls =
         TraitImplId.Map.map (self#visit_trait_impl decl_span_info) trait_impls
       in
+      let unit_metadata =
+        self#visit_global_decl_ref decl_span_info unit_metadata
+      in
       {
         name;
         options;
@@ -245,6 +249,7 @@ class ['self] map_crate_with_span =
         global_decls;
         trait_decls;
         trait_impls;
+        unit_metadata;
       }
   end
 
@@ -386,6 +391,7 @@ class ['self] iter_crate_with_span =
         global_decls;
         trait_decls;
         trait_impls;
+        unit_metadata;
       } =
         crate
       in
@@ -404,7 +410,8 @@ class ['self] iter_crate_with_span =
         trait_decls;
       TraitImplId.Map.iter
         (fun _ -> self#visit_trait_impl decl_span_info)
-        trait_impls
+        trait_impls;
+      self#visit_global_decl_ref decl_span_info unit_metadata
   end
 
 (** For error reporting: compute which local definitions (transitively) depend

charon-ml/src/PrintExpressions.ml

@@ -58,6 +58,7 @@ let rec projection_elem_to_string (env : 'a fmt_env) (sub : string)
       | Some variant_id ->
           let variant_name = adt_variant_to_string env adt_id variant_id in
           "(" ^ sub ^ " as " ^ variant_name ^ ")." ^ field_name)
+  | PtrMetadata -> sub ^ ".metadata"
 
 and place_to_string (env : 'a fmt_env) (p : place) : string =
   match p.kind with
@@ -90,7 +91,6 @@ and unop_to_string (env : 'a fmt_env) (unop : unop) : string =
   match unop with
   | Not -> "¬"
   | Neg om -> overflow_mode_to_string om ^ ".-"
-  | PtrMetadata -> "ptr_metadata"
   | Cast cast_kind -> cast_kind_to_string env cast_kind
 
 and overflow_mode_to_string (mode : overflow_mode) : string =
@@ -145,20 +145,22 @@ and operand_to_string (env : 'a fmt_env) (op : operand) : string =
 and rvalue_to_string (env : 'a fmt_env) (rv : rvalue) : string =
   match rv with
   | Use op -> operand_to_string env op
-  | RvRef (p, bk) -> begin
+  | RvRef (p, bk, op) -> begin
+      let op = operand_to_string env op in
       let p = place_to_string env p in
       match bk with
-      | BShared -> "&" ^ p
-      | BMut -> "&mut " ^ p
-      | BTwoPhaseMut -> "&two-phase " ^ p
-      | BUniqueImmutable -> "&uniq " ^ p
-      | BShallow -> "&shallow " ^ p
+      | BShared -> "&(" ^ p ^ ", " ^ op ^ ")"
+      | BMut -> "&mut (" ^ p ^ ", " ^ op ^ ")"
+      | BTwoPhaseMut -> "&two-phase (" ^ p ^ ", " ^ op ^ ")"
+      | BUniqueImmutable -> "&uniq (" ^ p ^ ", " ^ op ^ ")"
+      | BShallow -> "&shallow (" ^ p ^ ", " ^ op ^ ")"
     end
-  | RawPtr (p, pk) -> begin
+  | RawPtr (p, pk, op) -> begin
+      let op = operand_to_string env op in
       let p = place_to_string env p in
       match pk with
-      | RShared -> "&raw const " ^ p
-      | RMut -> "&raw mut " ^ p
+      | RShared -> "&raw const (" ^ p ^ ", " ^ op ^ ")"
+      | RMut -> "&raw mut (" ^ p ^ ", " ^ op ^ ")"
     end
   | NullaryOp (op, ty) ->
       nullop_to_string env op ^ "<" ^ ty_to_string env ty ^ ">"

charon-ml/src/PrintTypes.ml

@@ -289,7 +289,17 @@ and ty_to_string (env : 'a fmt_env) (ty : ty) : string =
       let env = fmt_env_push_regions env f.binder_regions in
       let fn = fn_ptr_to_string env f.binder_value in
       fn
-  | TDynTrait _ -> "dyn (TODO)"
+  | TDynTrait pred ->
+      let regions, clauses =
+        generic_params_to_strings env pred.binder.binder_params
+      in
+      let reg_str =
+        match regions with
+        | [] -> ""
+        | r :: _ -> " + " ^ r
+      in
+      "dyn (" ^ String.concat " + " clauses ^ reg_str ^ ")"
+  | TPtrMetadata ty -> "PtrMetadata(" ^ ty_to_string env ty ^ ")"
   | TError msg -> "type_error (\"" ^ msg ^ "\")"
 
 (** Return two lists:
@@ -402,14 +412,14 @@ and raw_attribute_to_string (attr : raw_attribute) : string =
   in
   attr.path ^ args
 
-let trait_param_to_string (env : 'a fmt_env) (clause : trait_param) : string =
+and trait_param_to_string (env : 'a fmt_env) (clause : trait_param) : string =
   let clause_id = trait_clause_id_to_string env clause.clause_id in
   let trait =
     region_binder_to_string trait_decl_ref_to_string env clause.trait
   in
   "[" ^ clause_id ^ "]: " ^ trait
 
-let generic_params_to_strings (env : 'a fmt_env) (generics : generic_params) :
+and generic_params_to_strings (env : 'a fmt_env) (generics : generic_params) :
     string list * string list =
   let ({ regions; types; const_generics; trait_clauses; _ } : generic_params) =
     generics

charon-ml/src/generated/Generated_Expressions.ml

@@ -245,6 +245,14 @@ and projection_elem =
           be used as left-values and right-values. We should never have
           projections to fields of symbolic variants (they should have been
           expanded before through a match). *)
+  | PtrMetadata
+      (** A built-in pointer (a reference, raw pointer, or [Box]) in Rust is
+          always a fat pointer: it contains an address and metadata for the
+          pointed-to place. This metadata is empty for sized types, it's the
+          length for slices, and the vtable for [dyn Trait].
+
+          We consider such pointers to be like a struct with two fields; this
+          represent access to the metadata "field". *)
   | ProjIndex of operand * bool
       (** MIR imposes that the argument to an index projection be a local
           variable, meaning that even constant indices into arrays are let-bound
@@ -270,11 +278,24 @@ and projection_elem =
     "R" or "Rv", this would avoid collisions *)
 and rvalue =
   | Use of operand  (** Lifts an operand as an rvalue. *)
-  | RvRef of place * borrow_kind  (** Takes a reference to the given place. *)
-  | RawPtr of place * ref_kind
+  | RvRef of place * borrow_kind * operand
+      (** Takes a reference to the given place. The [Operand] refers to the init
+          value of the metadata, it is [()] if no metadata
+
+          Fields:
+          - [place]
+          - [kind]
+          - [ptr_metadata] *)
+  | RawPtr of place * ref_kind * operand
       (** Takes a raw pointer with the given mutability to the given place. This
           is generated by pointer casts like [&v as *const _] or raw borrow
-          expressions like [&raw const v.] *)
+          expressions like [&raw const v.] Like [Ref], the [Operand] refers to
+          the init value of the metadata, it is [()] if no metadata.
+
+          Fields:
+          - [place]
+          - [kind]
+          - [ptr_metadata] *)
   | BinaryOp of binop * operand * operand
       (** Binary operations (note that we merge "checked" and "unchecked"
           binops) *)
@@ -306,29 +327,17 @@ and rvalue =
           Remark: in case of closures, the aggregated value groups the closure
           id together with its state. *)
   | Len of place * ty * const_generic option
-      (** Length of a memory location. The run-time length of e.g. a vector or a
-          slice is represented differently (but pretty-prints the same, FIXME).
-          Should be seen as a function of signature:
-          - [fn<T;N>(&[T;N]) -> usize]
-          - [fn<T>(&[T]) -> usize]
-
-          We store the type argument and the const generic (the latter only for
-          arrays).
-
-          [Len] is automatically introduced by rustc, notably for the bound
-          checks: we eliminate it together with the bounds checks whenever
-          possible. There are however occurrences that we don't eliminate (yet).
-          For instance, for the following Rust code:
+      (** Length of a place of type [[T]] or [[T; N]]. This applies to the place
+          itself, not to a pointer value. This is inserted by rustc in a single
+          case: slice patterns.
           {@rust[
             fn slice_pattern_4(x: &[()]) {
                 match x {
                     [_named] => (),
                     _ => (),
                 }
             }
-          ]}
-          rustc introduces a check that the length of the slice is exactly equal
-          to 1 and that we preserve. *)
+          ]} *)
   | Repeat of operand * ty * const_generic
       (** [Repeat(x, n)] creates an array where [x] is copied [n] times.
 
@@ -343,9 +352,6 @@ and rvalue =
 and unop =
   | Not
   | Neg of overflow_mode  (** This can overflow, for [-i::MIN]. *)
-  | PtrMetadata
-      (** Retreive the metadata part of a fat pointer. For slices, this
-          retreives their length. *)
   | Cast of cast_kind
       (** Casts are rvalues in MIR, but we treat them as unops. *)
 

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -1336,6 +1336,7 @@ and projection_elem_of_json (ctx : of_json_ctx) (js : json) :
         let* x_0 = field_proj_kind_of_json ctx x_0 in
         let* x_1 = field_id_of_json ctx x_1 in
         Ok (Field (x_0, x_1))
+    | `String "PtrMetadata" -> Ok PtrMetadata
     | `Assoc
         [ ("Index", `Assoc [ ("offset", offset); ("from_end", from_end) ]) ] ->
         let* offset = box_of_json operand_of_json ctx offset in
@@ -1359,8 +1360,11 @@ and ptr_metadata_of_json (ctx : of_json_ctx) (js : json) :
     | `String "None" -> Ok NoMetadata
     | `String "Length" -> Ok Length
     | `Assoc [ ("VTable", v_table) ] ->
-        let* v_table = v_table_of_json ctx v_table in
+        let* v_table = type_decl_ref_of_json ctx v_table in
         Ok (VTable v_table)
+    | `Assoc [ ("InheritFrom", inherit_from) ] ->
+        let* inherit_from = ty_of_json ctx inherit_from in
+        Ok (InheritFrom inherit_from)
     | _ -> Error "")
 
 and raw_attribute_of_json (ctx : of_json_ctx) (js : json) :
@@ -1431,14 +1435,30 @@ and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result =
     | `Assoc [ ("Use", use) ] ->
         let* use = operand_of_json ctx use in
         Ok (Use use)
-    | `Assoc [ ("Ref", `List [ x_0; x_1 ]) ] ->
-        let* x_0 = place_of_json ctx x_0 in
-        let* x_1 = borrow_kind_of_json ctx x_1 in
-        Ok (RvRef (x_0, x_1))
-    | `Assoc [ ("RawPtr", `List [ x_0; x_1 ]) ] ->
-        let* x_0 = place_of_json ctx x_0 in
-        let* x_1 = ref_kind_of_json ctx x_1 in
-        Ok (RawPtr (x_0, x_1))
+    | `Assoc
+        [
+          ( "Ref",
+            `Assoc
+              [
+                ("place", place); ("kind", kind); ("ptr_metadata", ptr_metadata);
+              ] );
+        ] ->
+        let* place = place_of_json ctx place in
+        let* kind = borrow_kind_of_json ctx kind in
+        let* ptr_metadata = operand_of_json ctx ptr_metadata in
+        Ok (RvRef (place, kind, ptr_metadata))
+    | `Assoc
+        [
+          ( "RawPtr",
+            `Assoc
+              [
+                ("place", place); ("kind", kind); ("ptr_metadata", ptr_metadata);
+              ] );
+        ] ->
+        let* place = place_of_json ctx place in
+        let* kind = ref_kind_of_json ctx kind in
+        let* ptr_metadata = operand_of_json ctx ptr_metadata in
+        Ok (RawPtr (place, kind, ptr_metadata))
     | `Assoc [ ("BinaryOp", `List [ x_0; x_1; x_2 ]) ] ->
         let* x_0 = binop_of_json ctx x_0 in
         let* x_1 = operand_of_json ctx x_1 in
@@ -1866,6 +1886,9 @@ and ty_of_json (ctx : of_json_ctx) (js : json) : (ty, string) result =
     | `Assoc [ ("FnDef", fn_def) ] ->
         let* fn_def = region_binder_of_json fn_ptr_of_json ctx fn_def in
         Ok (TFnDef fn_def)
+    | `Assoc [ ("PtrMetadata", ptr_metadata) ] ->
+        let* ptr_metadata = ty_of_json ctx ptr_metadata in
+        Ok (TPtrMetadata ptr_metadata)
     | `Assoc [ ("Error", error) ] ->
         let* error = string_of_json ctx error in
         Ok (TError error)
@@ -1891,9 +1914,7 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) :
         let* src = item_kind_of_json ctx src in
         let* kind = type_decl_kind_of_json ctx kind in
         let* layout = option_of_json layout_of_json ctx layout in
-        let* ptr_metadata =
-          option_of_json ptr_metadata_of_json ctx ptr_metadata
-        in
+        let* ptr_metadata = ptr_metadata_of_json ctx ptr_metadata in
         Ok
           ({ def_id; item_meta; generics; src; kind; layout; ptr_metadata }
             : type_decl)
@@ -1990,7 +2011,6 @@ and unop_of_json (ctx : of_json_ctx) (js : json) : (unop, string) result =
     | `Assoc [ ("Neg", neg) ] ->
         let* neg = overflow_mode_of_json ctx neg in
         Ok (Neg neg)
-    | `String "PtrMetadata" -> Ok PtrMetadata
     | `Assoc [ ("Cast", cast) ] ->
         let* cast = cast_kind_of_json ctx cast in
         Ok (Cast cast)
@@ -2009,12 +2029,6 @@ and unsizing_metadata_of_json (ctx : of_json_ctx) (js : json) :
     | `String "Unknown" -> Ok MetaUnknown
     | _ -> Error "")
 
-and v_table_of_json (ctx : of_json_ctx) (js : json) : (v_table, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Null -> Ok ()
-    | _ -> Error "")
-
 and variant_of_json (ctx : of_json_ctx) (js : json) : (variant, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with