multi-target: handle items that aren't defined on all targets

charon/src/export/multi_target.rs

@@ -360,12 +360,12 @@ impl<'a> ItemDeduplicator<'a> {
         this.apply_merge_decisions(decisions);
     }
 
-    /// Group items by (base_name, item_kind), keeping only groups that have items in all targets.
+    /// Group items by (base_name, item_kind). Each group contains the versions of that item
+    /// across all targets where it exists.
     fn discover_groups(
         krate: &TranslatedCrate,
         _errors: &mut ErrorCtx,
     ) -> IndexVec<TargetGroupId, TargetGroup> {
-        let num_targets = krate.target_information.len();
         let mut groups_map: SeqHashMap<
             (Name, std::mem::Discriminant<ItemId>),
             SeqHashMap<TargetTriple, ItemId>,
@@ -388,7 +388,7 @@ impl<'a> ItemDeduplicator<'a> {
             let prev_len = groups_map.len();
             let remap: HashMap<ItemId, ItemId> = groups_map
                 .values()
-                .filter(|ids| ids.len() == num_targets)
+                .filter(|ids| !ids.is_empty())
                 .cloned()
                 .map(|ids| TargetGroup { ids })
                 .flat_map(|g| g.into_remap_entries())
@@ -408,14 +408,14 @@ impl<'a> ItemDeduplicator<'a> {
                     }
                 }
             }
-            groups_map.retain(|_, v| v.len() == num_targets);
+            // Remove empty groups (from collisions) and check for convergence.
+            groups_map.retain(|_, v| !v.is_empty());
             if prev_len == groups_map.len() {
                 break;
             }
         }
         let groups: IndexVec<TargetGroupId, TargetGroup> = groups_map
             .into_values()
-            .filter(|per_target| per_target.len() == num_targets)
             .map(|ids| TargetGroup { ids })
             .collect();
         groups

charon/tests/cargo/multi-targets.out

@@ -1,4 +1,4 @@
-pub fn multi_targets::no_os::riscv64gc-unknown-none-elf(left_1: u64, right_2: u64) -> u64
+pub fn multi_targets::no_os(left_1: u64, right_2: u64) -> u64
 {
     let _0: u64; // return
     let left_1: u64; // arg #1
@@ -20,29 +20,7 @@ pub fn multi_targets::no_os::riscv64gc-unknown-none-elf(left_1: u64, right_2: u6
     return
 }
 
-pub fn multi_targets::on_unix::i686-unknown-linux-gnu(left_1: u64, right_2: u64) -> u64
-{
-    let _0: u64; // return
-    let left_1: u64; // arg #1
-    let right_2: u64; // arg #2
-    let _3: u64; // anonymous local
-    let _4: u64; // anonymous local
-    let _5: (u64, bool); // anonymous local
-
-    storage_live(_5)
-    storage_live(_3)
-    _3 = copy left_1
-    storage_live(_4)
-    _4 = copy right_2
-    _5 = copy _3 checked.+ copy _4
-    assert(move _5.1 == false) (overflow) else panic
-    _0 = move _5.0
-    storage_dead(_4)
-    storage_dead(_3)
-    return
-}
-
-pub fn multi_targets::on_unix::x86_64-apple-darwin(left_1: u64, right_2: u64) -> u64
+pub fn multi_targets::on_unix(left_1: u64, right_2: u64) -> u64
 {
     let _0: u64; // return
     let left_1: u64; // arg #1

charon/tests/ui/ml-multi-target-name-matcher-tests.out

@@ -1,12 +1,12 @@
-fn test_crate::x86_only::x86_64-apple-darwin() -> u64
+fn test_crate::x86_only() -> u64
 {
     let _0: u64; // return
 
     _0 = const 42 : u64
     return
 }
 
-fn test_crate::arm_only::aarch64-apple-darwin() -> u64
+fn test_crate::arm_only() -> u64
 {
     let _0: u64; // return
 

charon/tests/ui/ml-multi-target-name-matcher-tests.rs

@@ -4,20 +4,17 @@
 //! target-specific items get a `PeTarget` path element appended to their name. The name
 //! matcher should handle these correctly.
 
-// Target-specific functions get a PeTarget path element after multi-target merging.
 #[cfg(target_arch = "x86_64")]
-#[pattern::pass("test_crate::x86_only::x86_64-apple-darwin")]
-#[pattern::pass("test_crate::x86_only::_")]
-#[pattern::fail("test_crate::x86_only")]
+#[pattern::pass("test_crate::x86_only")]
 #[pattern::fail("test_crate::x86_only::aarch64-apple-darwin")]
+#[pattern::fail("test_crate::x86_only::x86_64-apple-darwin")]
 fn x86_only() -> u64 {
     42
 }
 
 #[cfg(target_arch = "aarch64")]
-#[pattern::pass("test_crate::arm_only::aarch64-apple-darwin")]
-#[pattern::pass("test_crate::arm_only::_")]
-#[pattern::fail("test_crate::arm_only")]
+#[pattern::pass("test_crate::arm_only")]
+#[pattern::fail("test_crate::arm_only::aarch64-apple-darwin")]
 #[pattern::fail("test_crate::arm_only::x86_64-apple-darwin")]
 fn arm_only() -> u64 {
     99

charon/tests/ui/multi-target/issue-1157-single-target-suffix.out

@@ -0,0 +1,17 @@
+fn test_crate::aarch64_only() -> u32
+{
+    let _0: u32; // return
+
+    _0 = const 1 : u32
+    return
+}
+
+fn test_crate::x86_64_only() -> u32
+{
+    let _0: u32; // return
+
+    _0 = const 2 : u32
+    return
+}
+
+

charon/tests/ui/multi-target/issue-1157-single-target-suffix.rs

@@ -0,0 +1,10 @@
+//@ charon-args=--targets=x86_64-pc-windows-msvc,aarch64-apple-darwin,i686-unknown-linux-gnu
+#[cfg(target_arch = "aarch64")]
+fn aarch64_only() -> u32 {
+    1
+}
+
+#[cfg(target_arch = "x86_64")]
+fn x86_64_only() -> u32 {
+    2
+}

charon/tests/ui/multi-target/issue-1158-partial-dedup.out

@@ -0,0 +1,31 @@
+fn test_crate::x86_common() -> u32
+{
+    let _0: u32; // return
+
+    _0 = const 42 : u32
+    return
+}
+
+fn test_crate::x86_different::x86_64-pc-windows-msvc() -> u32
+{
+    let _0: u32; // return
+
+    _0 = const 64 : u32
+    return
+}
+
+fn test_crate::x86_different::i686-unknown-linux-gnu() -> u32
+{
+    let _0: u32; // return
+
+    _0 = const 32 : u32
+    return
+}
+
+fn test_crate::x86_different() -> u32
+= target_dispatch {
+    x86_64-pc-windows-msvc => test_crate::x86_different::x86_64-pc-windows-msvc,
+    i686-unknown-linux-gnu => test_crate::x86_different::i686-unknown-linux-gnu,
+}
+
+

charon/tests/ui/multi-target/issue-1158-partial-dedup.rs

@@ -0,0 +1,15 @@
+//@ charon-args=--targets=x86_64-pc-windows-msvc,aarch64-apple-darwin,i686-unknown-linux-gnu
+#[cfg(any(target_arch = "x86_64", target_arch = "x86"))]
+fn x86_common() -> u32 {
+    42
+}
+
+#[cfg(target_arch = "x86_64")]
+fn x86_different() -> u32 {
+    64
+}
+
+#[cfg(target_arch = "x86")]
+fn x86_different() -> u32 {
+    32
+}