Fix dependencies for the extra parameters caused by associated types …

…in fields

creusot/src/backend/clone_map.rs

@@ -260,7 +260,6 @@ impl<'tcx> CloneMap<'tcx> {
     )]
     pub(crate) fn insert(&mut self, key: CloneNode<'tcx>) -> &mut CloneInfo {
         let key = key.erase_regions(self.tcx).closure_hack(self.tcx);
-
         self.names.entry(key).or_insert_with(|| {
             if let CloneNode::Type(ty) = key && !matches!(ty.kind(), TyKind::Alias(_, _)) {
                 return if let Some((did, _)) = key.did() {
@@ -298,13 +297,17 @@ impl<'tcx> CloneMap<'tcx> {
         self.insert(node).qname_ident(name.into())
     }
 
+    #[deprecated(
+        note = "this API is bad and should be entirely eliminated. Don't introduce new usages."
+    )]
     pub(crate) fn projection(
         &mut self,
         ctx: &mut TranslationCtx<'tcx>,
         alias: AliasTy<'tcx>,
-    ) -> QName {
-        let alias = ctx.try_normalize_erasing_regions(self.param_env(ctx), alias).unwrap_or(alias);
-        self.ty(alias.def_id, alias.substs)
+    ) -> Ty<'tcx> {
+        let ty = ctx.mk_alias(AliasKind::Projection, alias);
+        let ty = ctx.try_normalize_erasing_regions(self.param_env(ctx), ty).unwrap_or(ty);
+        ty
     }
 
     pub(crate) fn ty(&mut self, def_id: DefId, subst: SubstsRef<'tcx>) -> QName {
@@ -468,8 +471,19 @@ impl<'tcx> CloneMap<'tcx> {
     fn clone_dependencies(&mut self, ctx: &mut Why3Generator<'tcx>, key: DepNode<'tcx>) {
         let key_public = self.names[&key].public;
 
-        if let Some((_, key_subst)) = key.did() {
-            // Check the substitution for nodeendencies on closures
+        if let Some((id, key_subst)) = key.did() {
+            if util::item_type(ctx.tcx, id) == ItemType::Type {
+                for p in ctx.projections_in_ty(id).to_owned() {
+                    let node = self.resolve_dep(
+                        ctx,
+                        CloneNode::new(ctx.tcx, (p.def_id, p.substs)).subst(ctx.tcx, key),
+                    );
+                    self.insert(node).public |= key_public;
+                    self.add_graph_edge(key, node);
+                }
+            }
+
+            // Check the substitution for node dependencies on closures
             walk_types(key_subst, |t| {
                 let node = match t.kind() {
                     TyKind::Alias(AliasKind::Projection, pty) => {
@@ -595,7 +609,7 @@ impl<'tcx> CloneMap<'tcx> {
                 let use_decl = self.used_types.insert(def_id).then(|| {
                     if let Some(builtin) = get_builtin(ctx.tcx, def_id) {
                         let name = QName::from_string(&builtin.as_str()).unwrap().module_qname();
-                        Use { name: name, as_: None, export: false }
+                        Use { name, as_: None, export: false }
                     } else {
                         let name = cloneable_name(ctx, item, CloneLevel::Body);
                         Use { name: name.clone(), as_: Some(name), export: false }
@@ -680,8 +694,12 @@ impl<'tcx> CloneMap<'tcx> {
 
         self.last_cloned = self.names.len();
 
-        // Broken because of closures which share a defid for the type *and* function
-        // debug_assert!(!is_cyclic_directed(&self.clone_graph), "clone graph for {:?} is cyclic", self.self_id );
+        // // Broken because of closures which share a defid for the type *and* function
+        // debug_assert!(
+        //     !petgraph::algo::is_cyclic_directed(&self.clone_graph),
+        //     "clone graph for {:?} is cyclic",
+        //     self.self_id
+        // );
 
         let mut topo = DfsPostOrder::new(&self.clone_graph, self.self_key());
         while let Some(node) = topo.walk_next(&self.clone_graph) {

creusot/src/backend/ty.rs

@@ -13,7 +13,8 @@ use rustc_hir::{def::Namespace, def_id::DefId};
 use rustc_middle::ty::{
     self,
     subst::{InternalSubsts, SubstsRef},
-    AliasKind, AliasTy, EarlyBinder, FieldDef, GenericArgKind, ParamEnv, Ty, TyCtxt, TyKind,
+    AliasKind, AliasTy, EarlyBinder, FieldDef, GenericArg, GenericArgKind, ParamEnv, Ty, TyCtxt,
+    TyKind,
 };
 use rustc_span::{Span, Symbol, DUMMY_SP};
 use rustc_type_ir::sty::TyKind::*;
@@ -198,16 +199,16 @@ fn translate_projection_ty<'tcx>(
     pty: &AliasTy<'tcx>,
 ) -> MlT {
     if let TyTranslation::Declaration(id) = mode {
-        let ix = ctx.projections_in_ty(id).iter().position(|t| t == pty);
-        if let Some(ix) = ix {
-            return MlT::TVar(Ident::build(&format!("proj{ix}")));
-        }
-    };
-
-    // eprintln!("{:?}", pty);
-    let name = names.projection(ctx, *pty);
-    MlT::TConstructor(name)
-    // MlT::UNIT
+        let ix = ctx.projections_in_ty(id).iter().position(|t| t == pty).unwrap();
+        return MlT::TVar(Ident::build(&format!("proj{ix}")));
+    } else {
+        #[allow(deprecated)]
+        let proj_ty = names.projection(ctx, *pty);
+        if let TyKind::Alias(AliasKind::Projection, aty) = proj_ty.kind() {
+            return MlT::TConstructor(names.ty(aty.def_id, aty.substs));
+        };
+        translate_ty(ctx, names, DUMMY_SP, proj_ty)
+    }
 }
 
 pub(crate) fn translate_closure_ty<'tcx>(
@@ -280,6 +281,7 @@ impl<'tcx> Why3Generator<'tcx> {
         let mut v = Vec::new();
         let param_env = self.param_env(def_id);
 
+        // FIXME: Make this a proper BFS / DFS
         let subst = InternalSubsts::identity_for_item(self.tcx, def_id);
         for f in self.adt_def(def_id).all_fields() {
             let ty = f.ty(self.tcx, subst);
@@ -295,6 +297,15 @@ impl<'tcx> Why3Generator<'tcx> {
                         }
                     }
 
+                    // Add projections of types appearing in the substitution of a field.
+                    for a in
+                        substs.iter().flat_map(GenericArg::walk).filter_map(GenericArg::as_type)
+                    {
+                        match a.kind() {
+                            TyKind::Alias(AliasKind::Projection, aty) => v.push(*aty),
+                            _ => {}
+                        };
+                    }
                     // v.extend(self.projections_in_ty(adt.did()))
                 }
                 _ => {}
@@ -519,7 +530,6 @@ pub(crate) fn translate_accessor(
         }
     }
 
-    let ty_name = names.ty(adt_did, substs);
     let acc_name = format!("{}_{}", variant.name.as_str().to_ascii_lowercase(), field.name);
 
     let param_env = ctx.param_env(adt_did);
@@ -532,9 +542,12 @@ pub(crate) fn translate_accessor(
         .map(|var| (names.constructor(var.def_id, substs), var.fields.len()))
         .collect();
 
-    let this = MlT::TApp(
-        Box::new(MlT::TConstructor(ty_name.clone().into())),
-        ty_param_names(ctx.tcx, adt_did).map(MlT::TVar).collect(),
+    let this = translate_ty_inner(
+        TyTranslation::Declaration(adt_did),
+        ctx,
+        &mut names,
+        DUMMY_SP,
+        ctx.type_of(adt_did).subst_identity(),
     );
 
     let _ = names.to_clones(ctx);

creusot/tests/should_succeed/100doors.mlcfg

@@ -506,8 +506,6 @@ module Core_Iter_Range_Impl3_Next_Interface
     type Item0.item = a
   clone CreusotContracts_Std1_Iter_Iterator_Completed_Stub as Completed0 with
     type self = Core_Ops_Range_Range_Type.t_range a
-  clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with
-    type self = Core_Ops_Range_Range_Type.t_range a
   clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
     type t = borrowed (Core_Ops_Range_Range_Type.t_range a)
   val next (self : borrowed (Core_Ops_Range_Range_Type.t_range a)) : Core_Option_Option_Type.t_option a
@@ -1291,7 +1289,6 @@ module C100doors_F
   clone Core_Iter_Range_Impl3_Next_Interface as Next0 with
     type a = usize,
     predicate Inv0.inv = Inv4.inv,
-    type Item0.item = usize,
     predicate Completed0.completed = Completed0.completed,
     predicate Produces0.produces = Produces0.produces,
     predicate Inv1.inv = Inv5.inv

creusot/tests/should_succeed/hillel.mlcfg

@@ -1679,10 +1679,6 @@ module CreusotContracts_Std1_Slice_Impl14_Completed
     ensures { result = completed self }
 
 end
-module Core_Iter_Traits_Iterator_Iterator_Item_Type
-  type self
-  type item
-end
 module Core_Slice_Iter_Impl181_Next_Interface
   type t
   use prelude.Borrow
@@ -1695,8 +1691,6 @@ module Core_Slice_Iter_Impl181_Next_Interface
     type t = t
   clone CreusotContracts_Std1_Slice_Impl14_Completed_Stub as Completed0 with
     type t = t
-  clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with
-    type self = Core_Slice_Iter_Iter_Type.t_iter t
   val next (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) : Core_Option_Option_Type.t_option t
     ensures { [#"../../../../creusot-contracts/src/std/iter.rs" 95 26 98 17] match (result) with
       | Core_Option_Option_Type.C_None -> Completed0.completed self
@@ -2174,7 +2168,6 @@ module Hillel_InsertUnique
     type self = Core_Option_Option_Type.t_option t
   clone Core_Slice_Iter_Impl181_Next_Interface as Next0 with
     type t = t,
-    type Item0.item = t,
     predicate Completed0.completed = Completed0.completed,
     predicate Produces0.produces = Produces0.produces,
     predicate Inv0.inv = Inv4.inv
@@ -2567,6 +2560,10 @@ module CreusotContracts_Std1_Iter_Iterator_Completed
     ensures { result = completed self }
 
 end
+module Core_Iter_Traits_Iterator_Iterator_Item_Type
+  type self
+  type item
+end
 module CreusotContracts_Std1_Iter_Iterator_Produces_Stub
   type self
   use seq.Seq
@@ -2607,8 +2604,6 @@ module Core_Iter_Range_Impl3_Next_Interface
     type Item0.item = a
   clone CreusotContracts_Std1_Iter_Iterator_Completed_Stub as Completed0 with
     type self = Core_Ops_Range_Range_Type.t_range a
-  clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with
-    type self = Core_Ops_Range_Range_Type.t_range a
   clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
     type t = borrowed (Core_Ops_Range_Range_Type.t_range a)
   val next (self : borrowed (Core_Ops_Range_Range_Type.t_range a)) : Core_Option_Option_Type.t_option a
@@ -3161,7 +3156,6 @@ module Hillel_Unique
   clone Core_Iter_Range_Impl3_Next_Interface as Next0 with
     type a = usize,
     predicate Inv0.inv = Inv8.inv,
-    type Item0.item = usize,
     predicate Completed0.completed = Completed0.completed,
     predicate Produces0.produces = Produces0.produces,
     predicate Inv1.inv = Inv9.inv
@@ -3809,7 +3803,6 @@ module Hillel_Fulcrum
   clone Core_Iter_Range_Impl3_Next_Interface as Next1 with
     type a = usize,
     predicate Inv0.inv = Inv5.inv,
-    type Item0.item = usize,
     predicate Completed0.completed = Completed1.completed,
     predicate Produces0.produces = Produces1.produces,
     predicate Inv1.inv = Inv6.inv
@@ -3829,7 +3822,6 @@ module Hillel_Fulcrum
     function ShallowModel0.shallow_model = ShallowModel0.shallow_model
   clone Core_Slice_Iter_Impl181_Next_Interface as Next0 with
     type t = uint32,
-    type Item0.item = uint32,
     predicate Completed0.completed = Completed0.completed,
     predicate Produces0.produces = Produces0.produces,
     predicate Inv0.inv = Inv4.inv

creusot/tests/should_succeed/iterators/01_range.mlcfg

@@ -426,10 +426,6 @@ module C01Range_SumRange
   }
 
 end
-module C01Range_Common_Iterator_Item_Type
-  type self
-  type item
-end
 module C01Range_Impl0
   use seq.Seq
   use prelude.Int
@@ -464,8 +460,6 @@ module C01Range_Impl0
     type t = C01Range_Range_Type.t_range,
     predicate Inv0.inv = Inv0.inv,
     axiom .
-  clone C01Range_Common_Iterator_Item_Type as Item0 with
-    type self = C01Range_Range_Type.t_range
   clone C01Range_Impl0_Completed as Completed0 with
     predicate Resolve0.resolve = Resolve0.resolve
   clone C01Range_Impl0_Produces as Produces0

creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg

@@ -1978,10 +1978,6 @@ end
 module C02IterMut_Impl0
   type t
 end
-module C02IterMut_Common_Iterator_Item_Type
-  type self
-  type item
-end
 module C02IterMut_Impl1
   type t
   use seq.Seq
@@ -2073,8 +2069,6 @@ module C02IterMut_Impl1
     predicate Invariant0.invariant' = Invariant0.invariant',
     predicate Inv1.inv = Inv5.inv,
     axiom .
-  clone C02IterMut_Common_Iterator_Item_Type as Item0 with
-    type self = C02IterMut_IterMut_Type.t_itermut t
   clone C02IterMut_Impl1_Completed as Completed0 with
     type t = t,
     predicate Resolve0.resolve = Resolve0.resolve,