Fix panic from cross-crate FnDef impl-path collision (#2559)

Author: mmcloughlin

source/rust_verify_test/tests/fndef_types.rs

@@ -2037,3 +2037,28 @@ test_verify_one_file_with_options! {
         }
     } => Ok(())
 }
+
+test_verify_one_file_with_options! {
+    // Regression test for a panic due to fndef impl path collision across
+    // crates.
+    //
+    // The test defines 12 `Clone` impls in the crate root, which are enough to
+    // collide with the `Clone` impls for `Ghost` and `Tracked` in
+    // `verus_builtin` at the same disambiguator (brought in by `["vstd"]`).
+    #[test] fndef_impl_path_includes_crate ["vstd"] => verus_code! {
+        use vstd::prelude::*;
+
+        struct S0;  impl Clone for S0  { fn clone(&self) -> Self { S0  } }
+        struct S1;  impl Clone for S1  { fn clone(&self) -> Self { S1  } }
+        struct S2;  impl Clone for S2  { fn clone(&self) -> Self { S2  } }
+        struct S3;  impl Clone for S3  { fn clone(&self) -> Self { S3  } }
+        struct S4;  impl Clone for S4  { fn clone(&self) -> Self { S4  } }
+        struct S5;  impl Clone for S5  { fn clone(&self) -> Self { S5  } }
+        struct S6;  impl Clone for S6  { fn clone(&self) -> Self { S6  } }
+        struct S7;  impl Clone for S7  { fn clone(&self) -> Self { S7  } }
+        struct S8;  impl Clone for S8  { fn clone(&self) -> Self { S8  } }
+        struct S9;  impl Clone for S9  { fn clone(&self) -> Self { S9  } }
+        struct S10; impl Clone for S10 { fn clone(&self) -> Self { S10 } }
+        struct S11; impl Clone for S11 { fn clone(&self) -> Self { S11 } }
+    } => Ok(())
+}

source/vir/src/ast_simplify.rs

@@ -24,7 +24,8 @@ use crate::context::GlobalCtx;
 use crate::def::dummy_param_name;
 use crate::def::is_dummy_param_name;
 use crate::def::{
-    Spanned, positional_field_ident, prefix_tuple_param, prefix_tuple_variant, user_local_name,
+    Spanned, impl_fndef_path, positional_field_ident, prefix_tuple_param, prefix_tuple_variant,
+    user_local_name,
 };
 use crate::messages::Span;
 use crate::messages::{error, internal_error};
@@ -1049,17 +1050,10 @@ fn add_fndef_axioms_to_function(
             Arc::new(TypX::Datatype(tuple_dt, Arc::new(arg_typs), Arc::new(vec![])));
         let trait_typ_args = Arc::new(vec![self_typ, args_tuple_typ]);
 
-        let mk_impl_path = |kind: ClosureKind| {
-            Arc::new(crate::ast::PathX {
-                krate: CrateId::Internal,
-                segments: Arc::new(vec![crate::def::impl_fndef(&function.x.name, kind)]),
-            })
-        };
-
         let mut trait_impls_out: Vec<TraitImpl> = Vec::new();
         for kind in [ClosureKind::Fn, ClosureKind::FnMut, ClosureKind::FnOnce] {
             let trait_implx = crate::ast::TraitImplX {
-                impl_path: mk_impl_path(kind),
+                impl_path: impl_fndef_path(&function.x.name, kind),
                 typ_params: function.x.typ_params.clone(),
                 typ_bounds: function.x.typ_bounds.clone(),
                 trait_path: kind.trait_path(),
@@ -1074,7 +1068,7 @@ fn add_fndef_axioms_to_function(
 
         let assoc_typ_implx = crate::ast::AssocTypeImplX {
             name: Arc::new("Output".to_string()),
-            impl_path: mk_impl_path(ClosureKind::FnOnce),
+            impl_path: impl_fndef_path(&function.x.name, ClosureKind::FnOnce),
             typ_params: function.x.typ_params.clone(),
             typ_bounds: function.x.typ_bounds.clone(),
             trait_path: ClosureKind::FnOnce.trait_path(),

source/vir/src/def.rs

@@ -645,10 +645,8 @@ pub(crate) fn impl_closure(kind: ClosureKind, id: usize) -> Ident {
     Arc::new(format!("{}{}{}", PREFIX_IMPL_CLOSURE, kind, id))
 }
 
-pub(crate) fn impl_fndef(fun: &Fun, kind: ClosureKind) -> Ident {
-    let joined =
-        fun.path.segments.iter().map(|s| s.as_str()).collect::<Vec<_>>().join(PATH_SEPARATOR);
-    Arc::new(format!("{}{}{}", PREFIX_IMPL_FNDEF, kind, joined))
+pub(crate) fn impl_fndef_path(fun: &Fun, kind: ClosureKind) -> Path {
+    fun.path.push_segment(Arc::new(format!("{}{}", PREFIX_IMPL_FNDEF, kind)))
 }
 
 impl NameCtxt {