Roll pinned Rust toolchain

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.180"
+let supported_charon_version = "0.1.181"

charon-ml/src/NameMatcher.ml

@@ -342,7 +342,7 @@ let update_rmap (c : match_config) (m : maps) (id : var) (v : T.region) : bool =
     | RVar var ->
         let dbid, varid =
           match var with
-          | Bound (dbid, varid) -> (dbid, varid)
+          | Bound (dbid, varid) -> (dbid.index, varid)
           | Free varid -> (List.length m.rmap.bound_regions - 1, varid)
         in
         begin
@@ -457,7 +457,7 @@ let rec match_name_with_generics (ctx : 'fun_body ctx) (c : match_config)
      element, use the monomorphized args and continue matching without that
      element *)
   let n, g =
-    match List.rev n with
+    match List.rev n.name with
     | PeInstantiated binder :: rest_rev ->
         let mono_args = binder.binder_value in
         (* In this case, we may still have some late-bound generics in `g`, this could ONLY happen for regions *)
@@ -475,7 +475,7 @@ let rec match_name_with_generics (ctx : 'fun_body ctx) (c : match_config)
           else mono_args
         in
         (List.rev rest_rev, merged_args)
-    | _ -> (n, g)
+    | _ -> (n.name, g)
   in
   match (p, n) with
   | [], [] ->
@@ -511,7 +511,7 @@ let rec match_name_with_generics (ctx : 'fun_body ctx) (c : match_config)
       pid = id
       && T.Disambiguator.of_int pd = d
       && pg = []
-      && match_name_with_generics ctx c p n g
+      && match_name_with_generics ctx c p { name = n } g
   | PImpl pty :: p, PeImpl impl :: n -> (
       (* We have to distinguish two cases:
          - the impl is an inherent impl (linked to a type)
@@ -520,13 +520,13 @@ let rec match_name_with_generics (ctx : 'fun_body ctx) (c : match_config)
       match impl with
       | ImplElemTy bound_ty ->
           match_expr_with_ty ctx c (mk_empty_maps ()) pty bound_ty.binder_value
-          && match_name_with_generics ctx c p n g
+          && match_name_with_generics ctx c p { name = n } g
       | ImplElemTrait impl_id ->
           match_expr_with_trait_impl_id ctx c pty impl_id
-          && match_name_with_generics ctx c p n g)
+          && match_name_with_generics ctx c p { name = n } g)
   | PWild :: p, _ :: n ->
       (* Wildcard: skip this element in the name *)
-      match_name_with_generics ctx c p n g
+      match_name_with_generics ctx c p { name = n } g
   | _ -> false
 
 and match_name (ctx : 'fun_body ctx) (c : match_config) (p : pattern)
@@ -733,7 +733,7 @@ let match_fn_ptr (ctx : 'fun_body ctx) (c : match_config) (p : pattern)
   match func.kind with
   | FunId (FBuiltin fid) -> (
       let to_name (s : string list) : T.name =
-        List.map (fun s -> T.PeIdent (s, T.Disambiguator.of_int 0)) s
+        { name = List.map (fun s -> T.PeIdent (s, T.Disambiguator.of_int 0)) s }
       in
       match fid with
       | BoxNew -> (
@@ -841,7 +841,7 @@ let lookup_var_in_maps (m : constraints)
     'a option =
   let dbid, varid =
     match var with
-    | Bound (dbid, varid) -> (dbid, varid)
+    | Bound (dbid, varid) -> (dbid.index, varid)
     | Free varid -> (List.length m - 1, varid)
   in
   match List.nth_opt m dbid with
@@ -956,12 +956,12 @@ let literal_to_pattern (_c : to_pat_config) (lit : Values.literal) : literal =
 let rec name_with_generic_args_to_pattern_aux (ctx : 'fun_body ctx)
     (c : to_pat_config) (n : T.name) (generics : generic_args option) : pattern
     =
-  match n with
+  match n.name with
   | [] -> raise (Failure "Empty names are not valid")
   | [ e ] -> path_elem_with_generic_args_to_pattern ctx c e generics
-  | e :: n ->
+  | e :: n_tail ->
       path_elem_with_generic_args_to_pattern ctx c e None
-      @ name_with_generic_args_to_pattern_aux ctx c n generics
+      @ name_with_generic_args_to_pattern_aux ctx c { name = n_tail } generics
 
 and name_to_pattern_aux (ctx : 'fun_body ctx) (c : to_pat_config) (n : T.name) :
     pattern =
@@ -1490,20 +1490,21 @@ module NameMatcherMap = struct
   let match_name_with_generics_prefix (ctx : 'fun_body ctx) (c : match_config)
       (p : pattern) (n : T.name) (g : T.generic_args) :
       (T.name * T.generic_args) option =
-    if List.length p = List.length n then
+    if List.length p = List.length n.name then
       if match_name_with_generics ctx c p n g then
-        Some ([], TypesUtils.empty_generic_args)
+        Some ({ name = [] }, TypesUtils.empty_generic_args)
+      else None
+    else if List.length p < List.length n.name then
+      let npre, nend = Collections.List.split_at n.name (List.length p) in
+      if match_name ctx c p { name = npre } then Some ({ name = nend }, g)
       else None
-    else if List.length p < List.length n then
-      let npre, nend = Collections.List.split_at n (List.length p) in
-      if match_name ctx c p npre then Some (nend, g) else None
     else None
 
   let rec find_with_generics_opt (ctx : 'fun_body ctx) (c : match_config)
       (name : Types.name) (g : Types.generic_args) (m : 'a t) : 'a option =
     let (Node (node_v, children)) = m in
     (* Check if we reached the destination *)
-    match name with
+    match name.name with
     | [] | [ PeInstantiated _ ] ->
         (* For tree search, we also consider monomorphized elements as terminal
            since they represent instantiation details, not logical structure.

charon-ml/src/PrintTypes.ml

@@ -95,7 +95,7 @@ let lookup_var_in_env (env : 'a fmt_env)
   else
     let dbid, varid =
       match var with
-      | Bound (dbid, varid) -> (dbid, varid)
+      | Bound (dbid, varid) -> (dbid.index, varid)
       | Free varid ->
           let len = List.length env.generics in
           let dbid = len - 1 in
@@ -483,7 +483,7 @@ and path_elem_to_string (env : 'a fmt_env) (e : path_elem) : string =
   | PeTarget target -> target
 
 and name_to_string (env : 'a fmt_env) (n : name) : string =
-  let name = List.map (path_elem_to_string env) n in
+  let name = List.map (path_elem_to_string env) n.name in
   String.concat "::" name
 
 and raw_attribute_to_string (attr : raw_attribute) : string =

charon-ml/src/Substitute.ml

@@ -99,7 +99,7 @@ let subst_free_vars (subst : single_binder_subst) : subst =
 *)
 let subst_at_binder_zero (subst : single_binder_subst) : subst =
   let subst_if_zero subst nosubst = function
-    | Bound (dbid, id) when dbid = 0 -> subst id
+    | Bound (dbid, id) when dbid.index = 0 -> subst id
     | var -> nosubst var
   in
   {
@@ -114,8 +114,9 @@ let subst_at_binder_zero (subst : single_binder_subst) : subst =
     variables to remove the current binder level. *)
 let subst_remove_binder_zero (subst : single_binder_subst) : subst =
   let subst_remove_zero subst nosubst = function
-    | Bound (dbid, id) when dbid = 0 -> subst id
-    | Bound (dbid, varid) when dbid > 0 -> nosubst (Bound (dbid - 1, varid))
+    | Bound (dbid, id) when dbid.index = 0 -> subst id
+    | Bound (dbid, varid) when dbid.index > 0 ->
+        nosubst (Bound ({ index = dbid.index - 1 }, varid))
     | var -> nosubst var
   in
   {
@@ -129,7 +130,7 @@ let subst_remove_binder_zero (subst : single_binder_subst) : subst =
 (** Move a whole expression under one level of binder. *)
 let move_under_binder_subst : subst =
   let shift = function
-    | Bound (dbid, var) -> Bound (dbid + 1, var)
+    | Bound (dbid, var) -> Bound ({ index = dbid.index + 1 }, var)
     | Free _ as var -> var
   in
   {
@@ -144,7 +145,7 @@ let move_under_binder_subst : subst =
 let st_shift_visitor =
   object (self)
     inherit [_] map_statement
-    method! visit_de_bruijn_id delta dbid = dbid + delta
+    method! visit_de_bruijn_id delta dbid = { index = dbid.index + delta }
   end
 
 (* Shift the the substitution under one binder. *)

charon-ml/src/TypesUtils.ml

@@ -28,7 +28,7 @@ type 'a item_binder = {
 type bound_fun_sig = fun_sig item_binder
 
 let to_name (ls : string list) : name =
-  List.map (fun s -> PeIdent (s, Disambiguator.zero)) ls
+  { name = List.map (fun s -> PeIdent (s, Disambiguator.zero)) ls }
 
 let as_ident (e : path_elem) : string =
   match e with
@@ -178,7 +178,7 @@ let trait_instance_id_as_trait_impl (id : trait_ref_kind) :
   | _ -> raise (Failure "Unreachable")
 
 (* Make a debruijn variable of index 0 *)
-let zero_db_var (varid : 'id) : 'id de_bruijn_var = Bound (0, varid)
+let zero_db_var (varid : 'id) : 'id de_bruijn_var = Bound ({ index = 0 }, varid)
 
 let free_var_of_db_var (var : 'id de_bruijn_var) : 'id option =
   match var with
@@ -187,11 +187,11 @@ let free_var_of_db_var (var : 'id de_bruijn_var) : 'id option =
 
 let decr_db_var : 'id de_bruijn_var -> 'id de_bruijn_var = function
   | Free id -> Free id
-  | Bound (dbid, id) -> Bound (dbid - 1, id)
+  | Bound (dbid, id) -> Bound ({ index = dbid.index - 1 }, id)
 
 let incr_db_var : 'id de_bruijn_var -> 'id de_bruijn_var = function
   | Free id -> Free id
-  | Bound (dbid, id) -> Bound (dbid + 1, id)
+  | Bound (dbid, id) -> Bound ({ index = dbid.index + 1 }, id)
 
 let empty_generic_args : generic_args =
   { regions = []; types = []; const_generics = []; trait_refs = [] }

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -695,7 +695,10 @@ and de_bruijn_id_of_json (ctx : of_json_ctx) (js : json) :
     (de_bruijn_id, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
-    | x -> int_of_json ctx x
+    | `Assoc [ ("index", index) ] ->
+        let* index = int_of_json ctx index in
+        Ok ({ index } : de_bruijn_id)
+    | `Int i -> Ok ({ index = i } : de_bruijn_id)
     | _ -> Error "")
 
 and de_bruijn_var_of_json :
@@ -1483,7 +1486,12 @@ and monomorphize_mut_of_json (ctx : of_json_ctx) (js : json) :
 and name_of_json (ctx : of_json_ctx) (js : json) : (name, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
-    | x -> list_of_json path_elem_of_json ctx x
+    | `Assoc [ ("name", name) ] ->
+        let* name = list_of_json path_elem_of_json ctx name in
+        Ok ({ name } : name)
+    | `List _ ->
+        let* name = list_of_json path_elem_of_json ctx js in
+        Ok ({ name } : name)
     | _ -> Error "")
 
 and nullop_of_json (ctx : of_json_ctx) (js : json) : (nullop, string) result =

charon-ml/src/generated/Generated_Types.ml

@@ -38,7 +38,7 @@ type trait_type_constraint_id = TraitTypeConstraintId.id
 
 (** The index of a binder, counting from the innermost. See [[DeBruijnVar]] for
     details. *)
-type de_bruijn_id = int
+type de_bruijn_id = { index : int }
 
 (** Type-level variable.
 
@@ -985,7 +985,7 @@ and layout = {
 
     Also note that the first path element in the name is always the crate name.
 *)
-and name = (path_elem list[@visitors.opaque])
+and name = { name : path_elem list [@visitors.opaque] }
 
 (** See the comments for [Name] *)
 and path_elem =

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.180"
+version = "0.1.181"
 authors = [
     "Son Ho <hosonmarc@gmail.com>",
     "Guillaume Boisseau <nadrieril+git@gmail.com>",

charon/hax-frontend/src/constant_utils/uneval.rs

@@ -3,6 +3,7 @@ use super::*;
 use rustc_const_eval::interpret::{FnVal, InterpResult, interp_ok};
 use rustc_middle::mir::interpret;
 use rustc_middle::{mir, ty};
+use rustc_middle::query::QueryKey;
 
 impl ConstantLiteral {
     /// Rustc always represents string constants as `&[u8]`, but this
@@ -133,7 +134,6 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx>
                 {
                     val.sinto(s)
                 } else {
-                    use crate::rustc_middle::query::Key;
                     let span = tcx
                         .def_ident_span(ucv.def)
                         .unwrap_or_else(|| ucv.def.default_span(tcx));
@@ -192,7 +192,7 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
             ConstantExprKind::Literal(ConstantLiteral::byte_str(bytes))
         }
         (ty::ValTreeKind::Branch(fields), ty::Array(..) | ty::Slice(..) | ty::Tuple(..)) => {
-            let fields = fields.iter().copied().map(|field| field.sinto(s)).collect();
+            let fields = fields.iter().map(|field| field.sinto(s)).collect();
             match ty.kind() {
                 ty::Array(..) | ty::Slice(..) => ConstantExprKind::Array { fields },
                 ty::Tuple(_) => ConstantExprKind::Tuple { fields },

charon/hax-frontend/src/lib.rs

@@ -1,5 +1,4 @@
 #![allow(rustdoc::private_intra_doc_links)]
-#![feature(if_let_guard)]
 #![feature(macro_metavar_expr)]
 #![feature(rustc_private)]
 #![feature(sized_hierarchy)]

charon/hax-frontend/src/rustc_utils.rs

@@ -81,10 +81,9 @@ impl<'tcx, S: UnderOwnerState<'tcx>> HasParamEnv<'tcx> for S {
         }
     }
     fn typing_env(&self) -> ty::TypingEnv<'tcx> {
-        ty::TypingEnv {
-            param_env: self.param_env(),
-            typing_mode: ty::TypingMode::PostAnalysis,
-        }
+        let tcx = self.base().tcx;
+        let def_id = self.owner_id();
+        ty::TypingEnv::post_analysis(tcx, def_id)
     }
 }
 
@@ -211,7 +210,7 @@ pub fn assoc_tys_for_trait<'tcx>(
                 .in_definition_order()
                 .filter(|assoc| matches!(assoc.kind, ty::AssocKind::Type { .. }))
                 .filter(|assoc| tcx.generics_of(assoc.def_id).own_params.is_empty())
-                .map(|assoc| ty::AliasTy::new(tcx, assoc.def_id, tref.args)),
+                .map(|assoc| ty::AliasTy::new(tcx, ty::AliasTyKind::Projection { def_id: assoc.def_id }, tref.args)),
         );
         for clause in tcx
             .explicit_super_predicates_of(tref.def_id)
@@ -250,7 +249,7 @@ pub fn dyn_self_ty<'tcx>(
         .map(|alias_ty| {
             let proj = ty::ProjectionPredicate {
                 projection_term: alias_ty.into(),
-                term: ty::Ty::new_alias(tcx, ty::Projection, alias_ty).into(),
+                term: ty::Ty::new_alias(tcx, alias_ty).into(),
             };
             let proj = ty::ExistentialProjection::erase_self_ty(tcx, proj);
             ty::Binder::dummy(ty::ExistentialPredicate::Projection(proj))

charon/hax-frontend/src/traits.rs

@@ -224,7 +224,7 @@ pub fn translate_item_ref<'tcx, S: UnderOwnerState<'tcx>>(
 pub fn inherits_parent_clauses<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> bool {
     use rustc_hir::def::DefKind::*;
     match tcx.def_kind(def_id) {
-        AssocTy | AssocFn | AssocConst | Closure | Ctor(..) | Variant | AnonConst | InlineConst => {
+        AssocTy { .. } | AssocFn { .. } | AssocConst { .. } | Closure { .. } | Ctor(..) | Variant | AnonConst { .. } | InlineConst { .. } => {
             true
         }
         _ => false,