Merge branch 'main' into aeneas-docs

AeneasVerif · Jul 9, 2024 · 5874ee6 · 5874ee6
2 parents 4ac0b8b + 589339b
commit 5874ee6
Show file tree

Hide file tree

Showing 11 changed files with 113 additions and 182 deletions.
diff --git a/charon-pin b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-e0bf68d674edbb154fe2343b2315ccac325a0c7a
+cccc38353eec92c32c0f7a755fcef4ab5b1ae863
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
@@ -94,16 +94,15 @@ let ctx_add_norm_trait_types_from_preds (span : Meta.span) (ctx : eval_ctx)
 let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool =
   match id with
   | Self | Clause _ -> true
+  | ParentClause (id, _, _) | ItemClause (id, _, _, _) ->
+      trait_instance_id_is_local_clause id
   | TraitImpl _
   | BuiltinOrAuto _
-  | TraitRef _
   | UnknownTrait _
   | FnPointer _
   | Closure _
   | Unsolved _
   | Dyn _ -> false
-  | ParentClause (id, _, _) | ItemClause (id, _, _, _) ->
-      trait_instance_id_is_local_clause id
 
 (** About the conversion functions: for now we need them (TODO: merge ety, rty, etc.),
     but they should be applied to types without regions.
@@ -149,6 +148,10 @@ let trait_ref_to_string (ctx : norm_ctx) (x : trait_ref) : string =
   let ctx = norm_ctx_to_fmt_env ctx in
   Print.Types.trait_ref_to_string ctx x
 
+let trait_decl_ref_to_string (ctx : norm_ctx) (x : trait_decl_ref) : string =
+  let ctx = norm_ctx_to_fmt_env ctx in
+  Print.Types.trait_decl_ref_to_string ctx x
+
 let trait_instance_id_to_string (ctx : norm_ctx) (x : trait_instance_id) :
     string =
   let ctx = norm_ctx_to_fmt_env ctx in
@@ -247,23 +250,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
       let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in
       let ty : ty =
         match trait_ref.trait_id with
-        | TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ }
-          ->
-            cassert_opt_span __FILE__ __LINE__
-              (ref_generics = empty_generic_args)
-              ctx.span "Higher order trait types are not supported yet";
-            log#ldebug
-              (lazy
-                ("norm_ctx_normalize_ty: trait type: trait ref: "
-               ^ ty_to_string ctx ty));
-            (* Lookup the type *)
-            let ty =
-              norm_ctx_lookup_trait_impl_ty ctx impl_id trait_ref.generics
-                type_name
-            in
-            (* Normalize *)
-            norm_ctx_normalize_ty ctx ty
-        | TraitImpl impl_id ->
+        | TraitImpl (impl_id, generics) ->
             log#ldebug
               (lazy
                 ("norm_ctx_normalize_ty (trait impl):\n- trait type: "
@@ -278,8 +265,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
             *)
             (* Lookup the type *)
             let ty =
-              norm_ctx_lookup_trait_impl_ty ctx impl_id trait_ref.generics
-                type_name
+              norm_ctx_lookup_trait_impl_ty ctx impl_id generics type_name
             in
             (* Normalize *)
             norm_ctx_normalize_ty ctx ty
@@ -350,27 +336,22 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
         over it.
  *)
 and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
-    (id : trait_instance_id) : trait_instance_id * trait_ref option =
+    (id : trait_instance_id) : trait_instance_id =
   match id with
-  | Self -> (id, None)
-  | TraitImpl _ ->
+  | Self -> id
+  | TraitImpl (impl_id, generics) ->
       (* The [TraitImpl] shouldn't be inside any projection - we check this
          elsewhere by asserting that whenever we return [None] for the impl
          trait ref, then the id actually refers to a local clause. *)
-      (id, None)
-  | Clause _ -> (id, None)
-  | BuiltinOrAuto _ -> (id, None)
-  | ParentClause (inst_id, decl_id, clause_id) -> (
-      let inst_id, impl = norm_ctx_normalize_trait_instance_id ctx inst_id in
+      let generics = norm_ctx_normalize_generic_args ctx generics in
+      TraitImpl (impl_id, generics)
+  | Clause _ -> id
+  | BuiltinOrAuto _ -> id
+  | ParentClause (inst_id, decl_id, clause_id) -> begin
+      let inst_id = norm_ctx_normalize_trait_instance_id ctx inst_id in
       (* Check if the inst_id refers to a specific implementation, if yes project *)
-      match impl with
-      | None ->
-          (* This is actually a local clause *)
-          sanity_check_opt_span __FILE__ __LINE__
-            (trait_instance_id_is_local_clause inst_id)
-            ctx.span;
-          (ParentClause (inst_id, decl_id, clause_id), None)
-      | Some impl ->
+      match inst_id with
+      | TraitImpl (impl_id, generics) ->
           (* We figure out the parent clause by doing the following:
              {[
                // The implementation we are looking at
@@ -383,27 +364,24 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
              ]}
           *)
           (* Lookup the clause *)
-          let impl_id =
-            TypesUtils.trait_instance_id_as_trait_impl impl.trait_id
-          in
           let clause =
-            norm_ctx_lookup_trait_impl_parent_clause ctx impl_id impl.generics
+            norm_ctx_lookup_trait_impl_parent_clause ctx impl_id generics
               clause_id
           in
           (* Normalize the clause *)
-          let clause = norm_ctx_normalize_trait_ref ctx clause in
-          (TraitRef clause, Some clause))
-  | ItemClause (inst_id, decl_id, item_name, clause_id) -> (
-      let inst_id, impl = norm_ctx_normalize_trait_instance_id ctx inst_id in
-      (* Check if the inst_id refers to a specific implementation, if yes project *)
-      match impl with
-      | None ->
+          norm_ctx_normalize_trait_instance_id ctx clause.trait_id
+      | _ ->
           (* This is actually a local clause *)
           sanity_check_opt_span __FILE__ __LINE__
             (trait_instance_id_is_local_clause inst_id)
             ctx.span;
-          (ItemClause (inst_id, decl_id, item_name, clause_id), None)
-      | Some impl ->
+          ParentClause (inst_id, decl_id, clause_id)
+    end
+  | ItemClause (inst_id, decl_id, item_name, clause_id) -> begin
+      let inst_id = norm_ctx_normalize_trait_instance_id ctx inst_id in
+      (* Check if the inst_id refers to a specific implementation, if yes project *)
+      match inst_id with
+      | TraitImpl (impl_id, generics) ->
           (* We figure out the item clause by doing the following:
              {[
                // The implementation we are looking at
@@ -416,49 +394,30 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
              ]}
           *)
           (* Lookup the impl *)
-          let impl_id =
-            TypesUtils.trait_instance_id_as_trait_impl impl.trait_id
-          in
           let clause =
-            norm_ctx_lookup_trait_impl_item_clause ctx impl_id impl.generics
+            norm_ctx_lookup_trait_impl_item_clause ctx impl_id generics
               item_name clause_id
           in
           (* Normalize the clause *)
-          let clause = norm_ctx_normalize_trait_ref ctx clause in
-          (TraitRef clause, Some clause))
-  | TraitRef { trait_id = TraitImpl trait_id; generics; trait_decl_ref } ->
-      (* We can't simplify the id *yet* : we will simplify it when projecting.
-         However, we have an implementation to return *)
-      (* Normalize the generics *)
-      let generics = norm_ctx_normalize_generic_args ctx generics in
-      let trait_decl_ref =
-        norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref
-      in
-      let trait_ref : trait_ref =
-        { trait_id = TraitImpl trait_id; generics; trait_decl_ref }
-      in
-      (TraitRef trait_ref, Some trait_ref)
-  | TraitRef trait_ref ->
-      (* The trait instance id necessarily refers to a local sub-clause. We
-         can't project over it and can only peel off the [TraitRef] wrapper *)
-      sanity_check_opt_span __FILE__ __LINE__
-        (trait_instance_id_is_local_clause trait_ref.trait_id)
-        ctx.span;
-      sanity_check_opt_span __FILE__ __LINE__
-        (trait_ref.generics = empty_generic_args)
-        ctx.span;
-      (trait_ref.trait_id, None)
+          norm_ctx_normalize_trait_instance_id ctx clause.trait_id
+      | _ ->
+          (* This is actually a local clause *)
+          sanity_check_opt_span __FILE__ __LINE__
+            (trait_instance_id_is_local_clause inst_id)
+            ctx.span;
+          ItemClause (inst_id, decl_id, item_name, clause_id)
+    end
   | FnPointer ty ->
       let ty = norm_ctx_normalize_ty ctx ty in
       (* TODO: we might want to return the ref to the function pointer,
          in order to later normalize a call to this function pointer *)
-      (FnPointer ty, None)
+      FnPointer ty
   | Closure (fid, generics) ->
       let generics = norm_ctx_normalize_generic_args ctx generics in
-      (Closure (fid, generics), None)
+      Closure (fid, generics)
   | Unsolved _ | UnknownTrait _ ->
       (* This is actually an error case *)
-      (id, None)
+      id
   | Dyn _ ->
       craise_opt_span __FILE__ __LINE__ ctx.span
         "Dynamic trait types are not supported yet"
@@ -477,31 +436,16 @@ and norm_ctx_normalize_trait_ref (ctx : norm_ctx) (trait_ref : trait_ref) :
       ("norm_ctx_normalize_trait_ref: "
       ^ trait_ref_to_string ctx trait_ref
       ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref));
-  let { trait_id; generics; trait_decl_ref } = trait_ref in
+  let { trait_id; trait_decl_ref } = trait_ref in
+
   (* Check if the id is an impl, otherwise normalize it *)
-  let trait_id, norm_trait_ref =
-    norm_ctx_normalize_trait_instance_id ctx trait_id
-  in
-  match norm_trait_ref with
-  | None ->
-      log#ldebug
-        (lazy
-          ("norm_ctx_normalize_trait_ref: no norm: "
-          ^ trait_instance_id_to_string ctx trait_id));
-      let generics = norm_ctx_normalize_generic_args ctx generics in
-      let trait_decl_ref =
-        norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref
-      in
-      { trait_id; generics; trait_decl_ref }
-  | Some trait_ref ->
-      log#ldebug
-        (lazy
-          ("norm_ctx_normalize_trait_ref: normalized to: "
-          ^ trait_ref_to_string ctx trait_ref));
-      sanity_check_opt_span __FILE__ __LINE__
-        (generics = empty_generic_args)
-        ctx.span;
-      trait_ref
+  let trait_id = norm_ctx_normalize_trait_instance_id ctx trait_id in
+  let trait_decl_ref = norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref in
+  log#ldebug
+    (lazy
+      ("norm_ctx_normalize_trait_ref: no norm: "
+      ^ trait_instance_id_to_string ctx trait_id));
+  { trait_id; trait_decl_ref }
 
 (* Not sure this one is really necessary *)
 and norm_ctx_normalize_trait_decl_ref (ctx : norm_ctx)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
@@ -1641,9 +1641,9 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx)
         (fun (c : Types.trait_clause) -> c.clause_id = clause_id)
         clauses
     in
-    let trait_id = clause.trait_id in
+    let trait_id = clause.trait.trait_decl_id in
     let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in
-    let args = clause.clause_generics in
+    let args = clause.trait.decl_generics in
     trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
       impl_trait_decl.item_meta.name params args
   in

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
@@ -587,9 +587,6 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         *)
         match trait_ref.trait_id with
         | Self ->
-            sanity_check __FILE__ __LINE__
-              (trait_ref.generics = empty_generic_args)
-              span;
             extract_trait_instance_id_with_dot span ctx fmt no_params_tys false
               trait_ref.trait_id;
             F.pp_print_string fmt type_name
@@ -606,28 +603,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
 and extract_trait_ref (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
     (tr : trait_ref) : unit =
-  let use_brackets = tr.generics <> empty_generic_args && inside in
-  if use_brackets then F.pp_print_string fmt "(";
-  (* We may need to filter the parameters if the trait is builtin *)
-  let generics =
-    match tr.trait_id with
-    | TraitImpl id -> (
-        match
-          TraitImplId.Map.find_opt id ctx.trait_impls_filter_type_args_map
-        with
-        | None -> tr.generics
-        | Some filter ->
-            let types =
-              List.filter_map
-                (fun (b, x) -> if b then Some x else None)
-                (List.combine filter tr.generics.types)
-            in
-            { tr.generics with types })
-    | _ -> tr.generics
-  in
-  extract_trait_instance_id span ctx fmt no_params_tys inside tr.trait_id;
-  extract_generic_args span ctx fmt no_params_tys generics;
-  if use_brackets then F.pp_print_string fmt ")"
+  extract_trait_instance_id span ctx fmt no_params_tys inside tr.trait_id
 
 and extract_trait_decl_ref (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
@@ -715,9 +691,27 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx)
          (associated type, etc.). We should have caught this elsewhere. *)
       save_error __FILE__ __LINE__ (Some span) "Unexpected occurrence of `Self`";
       F.pp_print_string fmt "ERROR(\"Unexpected Self\")"
-  | TraitImpl id ->
+  | TraitImpl (id, generics) ->
+      (* We may need to filter the parameters if the trait is builtin *)
+      let generics =
+        match
+          TraitImplId.Map.find_opt id ctx.trait_impls_filter_type_args_map
+        with
+        | None -> generics
+        | Some filter ->
+            let types =
+              List.filter_map
+                (fun (b, x) -> if b then Some x else None)
+                (List.combine filter generics.types)
+            in
+            { generics with types }
+      in
       let name = ctx_get_trait_impl span id ctx in
-      F.pp_print_string fmt name
+      let use_brackets = generics <> empty_generic_args && inside in
+      if use_brackets then F.pp_print_string fmt "(";
+      F.pp_print_string fmt name;
+      extract_generic_args span ctx fmt no_params_tys generics;
+      if use_brackets then F.pp_print_string fmt ")"
   | Clause id ->
       let name = ctx_get_local_trait_clause span id ctx in
       F.pp_print_string fmt name
@@ -733,8 +727,6 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx)
       in
       extract_trait_instance_id_with_dot span ctx fmt no_params_tys true inst_id;
       F.pp_print_string fmt (add_brackets name)
-  | TraitRef trait_ref ->
-      extract_trait_ref span ctx fmt no_params_tys inside trait_ref
   | UnknownTrait _ ->
       (* This is an error case *)
       craise __FILE__ __LINE__ span "Unexpected"

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
@@ -133,17 +133,15 @@ let symbolic_instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
       List.fold_left_map
         (fun tr_map (c : trait_clause) ->
           let subst = mk_subst tr_map in
-          let { trait_id = trait_decl_id; clause_generics; _ } = c in
+          let { trait_decl_id; decl_generics; _ } = c.trait in
           let generics =
-            Substitute.generic_args_substitute subst clause_generics
+            Substitute.generic_args_substitute subst decl_generics
           in
           let trait_decl_ref = { trait_decl_id; decl_generics = generics } in
           (* Note that because we directly refer to the clause, we give it
              empty generics *)
           let trait_id = Clause c.clause_id in
-          let trait_ref =
-            { trait_id; generics = empty_generic_args; trait_decl_ref }
-          in
+          let trait_ref = { trait_id; trait_decl_ref } in
           (* Update the traits map *)
           let tr_map = TraitClauseId.Map.add c.clause_id trait_id tr_map in
           (tr_map, trait_ref))