Merge pull request #1534 from Nadrieril/update-rustc

Update rustc to latest nightly

Author: W95Psp

.github/workflows/charon.yml

@@ -1,6 +1,5 @@
 #![feature(rustc_private)]
 #![feature(box_patterns)]
-#![feature(concat_idents)]
 #![feature(trait_alias)]
 #![allow(unused_imports)]
 #![allow(unused_variables)]

cli/driver/src/driver.rs

@@ -1086,6 +1086,7 @@ open Phase_utils
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Reject.RawOrMutPointer
   |> Phases.And_mut_defsite
   |> Phases.Reconstruct_asserts

engine/backends/coq/coq/coq_backend.ml

@@ -555,6 +555,7 @@ open Phase_utils
 module TransformToInputLanguage =
   [%functor_application
     Phases.Reject.Unsafe(Features.Rust)
+    |> Phases.Drop_metasized
     |> Phases.Reject.RawOrMutPointer
     |> Phases.And_mut_defsite
     |> Phases.Reconstruct_asserts

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -1911,6 +1911,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
     Phases.Reject.RawOrMutPointer(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Transform_hax_lib_inline
   |> Phases.Specialize
   |> Phases.Drop_sized_trait

engine/backends/fstar/fstar_backend.ml

@@ -887,6 +887,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Reject.RawOrMutPointer
   |> Phases.Transform_hax_lib_inline
   |> Phases.Simplify_question_marks

engine/backends/proverif/proverif_backend.ml

@@ -118,6 +118,10 @@ let c_attr (attr : Thir.attribute) : attr option =
       in
       let kind = DocComment { kind; body = comment } in
       Some { kind; span = Span.of_thir span }
+  | Parsed (AutomaticallyDerived span) ->
+      (* Restore behavior before PR #1534 *)
+      let kind = Tool { path = "automatically_derived"; tokens = "" } in
+      Some { kind; span = Span.of_thir span }
   | Unparsed { args = Eq { expr = { symbol; _ }; _ }; path = "doc"; span; _ } ->
       (* Looks for `#[doc = "something"]` *)
       let kind = DocComment { kind = DCKLine; body = symbol } in
@@ -1105,8 +1109,6 @@ end) : EXPR = struct
         match non_traits with
         | [] -> TDyn { witness = W.dyn; goals }
         | _ -> assertion_failure [ span ] "type Dyn with non trait predicate")
-    | Dynamic (_, _, DynStar) ->
-        unimplemented ~issue_id:931 [ span ] "type DynStar"
     | Coroutine _ ->
         unimplemented ~issue_id:924 [ span ]
           "Got type `Coroutine`: coroutines are not supported by hax"
@@ -1377,7 +1379,7 @@ let is_automatically_derived (attrs : Thir.attribute list) =
     ~f:(function
       (* This will break once these attributes get properly parsed. It will
           then be very easy to parse them correctly *)
-      | Unparsed { path; _ } -> String.equal path "automatically_derived"
+      | Parsed (AutomaticallyDerived _) -> true
       | _ -> false)
     attrs
 
@@ -1516,7 +1518,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
   in
   (* TODO: things might be unnamed (e.g. constants) *)
   match (item.kind : Thir.item_kind) with
-  | Const (_, _, generics, body) ->
+  | Const (_, generics, _, body) ->
       mk
       @@ Fn
            {
@@ -1526,14 +1528,14 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
              params = [];
              safety = Safe;
            }
-  | Static (_, _, true, _) ->
+  | Static (true, _, _, _) ->
       unimplemented ~issue_id:1343 [ item.span ]
         "Mutable static items are not supported."
-  | Static (_, _ty, false, body) ->
+  | Static (false, _, _ty, body) ->
       let name = Concrete_ident.of_def_id ~value:true (assert_item_def_id ()) in
       let generics = { params = []; constraints = [] } in
       mk (Fn { name; generics; body = c_body body; params = []; safety = Safe })
-  | TyAlias (_, ty, generics) ->
+  | TyAlias (_, generics, ty) ->
       mk
       @@ TyAlias
            {
@@ -1552,13 +1554,13 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
              params = c_fn_params item.span params;
              safety = c_header_safety safety;
            }
-  | (Enum (_, _, generics, _) | Struct (_, _, generics)) when erased ->
+  | (Enum (_, generics, _, _) | Struct (_, generics, _)) when erased ->
       let generics = c_generics generics in
       let is_struct = match item.kind with Struct _ -> true | _ -> false in
       let def_id = assert_item_def_id () in
       let name = Concrete_ident.of_def_id ~value:false def_id in
       mk @@ Type { name; generics; variants = []; is_struct }
-  | Enum (_, variants, generics, repr) ->
+  | Enum (_, generics, variants, repr) ->
       let def_id = assert_item_def_id () in
       let generics = c_generics generics in
       let is_struct = false in
@@ -1616,7 +1618,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
         mk_one (Type { name; generics; variants; is_struct }) :: discs
       in
       if is_primitive then cast_fun :: result else result
-  | Struct (_, v, generics) ->
+  | Struct (_, generics, v) ->
       let generics = c_generics generics in
       let def_id = assert_item_def_id () in
       let is_struct = true in
@@ -1643,7 +1645,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
       let variants = [ v ] in
       let name = Concrete_ident.of_def_id ~value:false def_id in
       mk @@ Type { name; generics; variants; is_struct }
-  | Trait (No, safety, _, generics, _bounds, items) ->
+  | Trait (NotConst, No, safety, _, generics, _bounds, items) ->
       let items =
         List.filter
           ~f:(fun { attributes; _ } -> not (should_skip attributes))
@@ -1666,8 +1668,10 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
       let items = List.map ~f:c_trait_item items in
       let safety = csafety safety in
       mk @@ Trait { name; generics; items; safety }
-  | Trait (Yes, _, _, _, _, _) ->
+  | Trait (_, Yes, _, _, _, _, _) ->
       unimplemented ~issue_id:930 [ item.span ] "Auto trait"
+  | Trait (Const, _, _, _, _, _, _) ->
+      unimplemented ~issue_id:930 [ item.span ] "Const trait"
   | Impl { of_trait = None; generics; items; _ } ->
       let items =
         List.filter
@@ -1814,7 +1818,9 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
           {
             path = List.map ~f:(fun x -> fst x.ident) segments;
             is_external =
-              List.exists ~f:(function Err -> true | _ -> false) res;
+              List.exists
+                ~f:(function None | Some Err -> true | _ -> false)
+                res;
             (* TODO: this should represent local/external? *)
             rename;
           }

engine/lib/import_thir.ml

@@ -0,0 +1,193 @@
+(** This phase gets rid of the MetaSized bound. See
+    https://github.com/cryspen/hax/pull/1534. *)
+
+open! Prelude
+
+module%inlined_contents Make (F : Features.T) = struct
+  open Ast
+  module FA = F
+  module FB = FA
+
+  include
+    Phase_utils.MakeBase (F) (FB)
+      (struct
+        let phase_id = [%auto_phase_name auto]
+      end)
+
+  module UA = Ast_utils.Make (F)
+
+  module Implem : ImplemT.T = struct
+    let metadata = metadata
+
+    module S = struct
+      include Features.SUBTYPE.Id
+    end
+
+    [%%inline_defs dmutability + dsafety_kind]
+
+    let rec dimpl_expr (span : span) (i : A.impl_expr) : B.impl_expr option =
+      let* kind = dimpl_expr_kind span i.kind in
+      let* goal = dtrait_goal span i.goal in
+      Some B.{ kind; goal }
+
+    and dtrait_goal (span : span) (r : A.trait_goal) : B.trait_goal option =
+      let*? _ = not (Concrete_ident.eq_name Core__marker__MetaSized r.trait) in
+      Some
+        B.{ trait = r.trait; args = List.map ~f:(dgeneric_value span) r.args }
+
+    and dimpl_expr_exn message span i =
+      match dimpl_expr span i with
+      | None -> Error.assertion_failure span message
+      | Some impl -> impl
+
+    and dimpl_ident (span : span) (r : A.impl_ident) : B.impl_ident option =
+      let* goal = dtrait_goal span r.goal in
+      Some B.{ goal; name = r.name }
+
+    and dty (span : span) (ty : A.ty) : B.ty =
+      match ty with
+      | TAssociatedType { impl; item } ->
+          let impl =
+            dimpl_expr_exn "MetaSized has no associated type" span impl
+          in
+          TAssociatedType { impl; item }
+      | [%inline_arms "dty.*" - TAssociatedType] -> auto
+
+    and dprojection_predicate (span : span) (r : A.projection_predicate) :
+        B.projection_predicate =
+      {
+        impl = dimpl_expr_exn "MetaSized cannot be projected" span r.impl;
+        assoc_item = r.assoc_item;
+        typ = dty span r.typ;
+      }
+
+    and dimpl_expr_kind (span : span) (i : A.impl_expr_kind) :
+        B.impl_expr_kind option =
+      match i with
+      | Parent { impl; ident } ->
+          let* impl = dimpl_expr span impl in
+          let* ident = dimpl_ident span ident in
+          Some (B.Parent { impl; ident })
+      | Projection { impl; item; ident } ->
+          let impl = dimpl_expr_exn "MetaSized have no projection" span impl in
+          let* ident = dimpl_ident span ident in
+          Some (B.Projection { impl; item; ident })
+      | ImplApp { impl; args } ->
+          let* impl = dimpl_expr span impl in
+          let args = List.filter_map ~f:(dimpl_expr span) args in
+          Some (B.ImplApp { impl; args })
+      | Builtin tr ->
+          let* tr = dtrait_goal span tr in
+          Some (B.Builtin tr)
+      | Concrete tr ->
+          let* tr = dtrait_goal span tr in
+          Some (B.Concrete tr)
+      | [%inline_arms
+          "dimpl_expr_kind.*" - Parent - Projection - ImplApp - Builtin
+          - Concrete] ->
+          map (fun x ->
+              Some
+                (let result : B.impl_expr_kind = x in
+                 result))
+
+    and dexpr' (span : span) (expr : A.expr') : B.expr' =
+      match expr with
+      | App { f; args; generic_args; bounds_impls; trait } ->
+          let dgeneric_values = List.map ~f:(dgeneric_value span) in
+          App
+            {
+              f = dexpr f;
+              args = List.map ~f:dexpr args;
+              generic_args = dgeneric_values generic_args;
+              bounds_impls = List.filter_map ~f:(dimpl_expr span) bounds_impls;
+              trait =
+                Option.map
+                  ~f:
+                    (dimpl_expr_exn "MetaSized have no method" span
+                    *** dgeneric_values)
+                  trait;
+            }
+      | [%inline_arms "dexpr'.*" - App] -> auto
+    [@@inline_ands
+      bindings_of dty - dimpl_expr - dexpr' - dprojection_predicate
+      - dimpl_expr_kind - dty - dimpl_ident]
+
+    let rec dimpl_item' (span : span) (ii : A.impl_item') : B.impl_item' =
+      match ii with
+      | IIType { typ; parent_bounds } ->
+          IIType
+            {
+              typ = dty span typ;
+              parent_bounds =
+                List.filter_map
+                  ~f:(fun (impl, ident) ->
+                    let* impl = dimpl_expr span impl in
+                    let* ident = dimpl_ident span ident in
+                    Some (impl, ident))
+                  parent_bounds;
+            }
+          (* | _ -> Obj.magic () *)
+      | [%inline_arms "dimpl_item'.*" - IIType] -> auto
+
+    and dtrait_item' (span : span) (ti : A.trait_item') : B.trait_item' =
+      match ti with
+      | TIType idents -> TIType (List.filter_map ~f:(dimpl_ident span) idents)
+      | [%inline_arms "dtrait_item'.*" - TIType] -> auto
+
+    and dgeneric_constraint (span : span)
+        (generic_constraint : A.generic_constraint) :
+        B.generic_constraint option =
+      match generic_constraint with
+      | GCLifetime (lf, witness) ->
+          Some (B.GCLifetime (lf, S.lifetime span witness))
+      | GCType impl_ident ->
+          let* impl = dimpl_ident span impl_ident in
+          Some (B.GCType impl)
+      | GCProjection projection ->
+          Some (B.GCProjection (dprojection_predicate span projection))
+
+    and dgenerics (span : span) (g : A.generics) : B.generics =
+      {
+        params = List.map ~f:(dgeneric_param span) g.params;
+        constraints =
+          List.filter_map ~f:(dgeneric_constraint span) g.constraints;
+      }
+
+    and ditem' (span : span) (item : A.item') : B.item' =
+      match item with
+      | Impl
+          {
+            generics;
+            self_ty;
+            of_trait = trait_id, trait_generics;
+            items;
+            parent_bounds;
+            safety;
+          } ->
+          B.Impl
+            {
+              generics = dgenerics span generics;
+              self_ty = dty span self_ty;
+              of_trait =
+                (trait_id, List.map ~f:(dgeneric_value span) trait_generics);
+              items = List.map ~f:dimpl_item items;
+              parent_bounds =
+                List.filter_map
+                  ~f:(fun (impl, ident) ->
+                    let* impl = dimpl_expr span impl in
+                    let* ident = dimpl_ident span ident in
+                    Some (impl, ident))
+                  parent_bounds;
+              safety = dsafety_kind span safety;
+            }
+      | [%inline_arms "ditem'.*" - Impl] -> auto
+    [@@inline_ands
+      "Item.*" - ditem' - dimpl_item' - dtrait_item' - dgeneric_constraint
+      - dgenerics]
+
+    [%%inline_defs ditems]
+  end
+
+  include Implem
+end
+[@@add "subtype.ml"]

engine/lib/phases/phase_drop_metasized.ml

@@ -0,0 +1,16 @@
+(** This phase gets rid of the MetaSized bound. See
+    https://github.com/cryspen/hax/pull/1534. *)
+
+open! Prelude
+
+module Make (F : Features.T) : sig
+  include module type of struct
+    module FA = F
+    module FB = FA
+    module A = Ast.Make (F)
+    module B = Ast.Make (FB)
+    module ImplemT = Phase_utils.MakePhaseImplemT (A) (B)
+  end
+
+  include ImplemT.T
+end