Unique constant names

prusti-encoder/src/encoders/const.rs

@@ -50,6 +50,11 @@ pub enum ConstEncTask<'vir> {
 /// https://rustc-dev-guide.rust-lang.org/mir/index.html#representing-constants
 pub struct ConstEnc;
 
+// Counter ensuring every emitted array constant gets a unique Viper name.
+thread_local! {
+    static CONST_CTR: std::cell::Cell<usize> = const { std::cell::Cell::new(0) };
+}
+
 struct Enc<'enc, 'vir: 'enc> {
     deps: &'enc mut TaskEncoderDependencies<'vir, ConstEnc>,
     ecx: &'enc InterpCx<'vir, CompileTimeMachine<'vir>>,
@@ -130,14 +135,24 @@ impl<'enc, 'vir: 'enc> Enc<'enc, 'vir> {
                             ),
                         );
                     }
-                    // TODO: this might run into collisions
-                    let span_pos = vcx.tcx().sess.source_map().lookup_char_pos(self.span.lo());
+                    let id = CONST_CTR.with(|c| {
+                        let v = c.get();
+                        c.set(v + 1);
+                        v
+                    });
+                    // `source_callsite()` walks out of any macro expansion to the user's call site.
+                    let span_pos = vcx
+                        .tcx()
+                        .sess
+                        .source_map()
+                        .lookup_char_pos(self.span.source_callsite().lo());
                     let gen_snap_func_idn: FunctionIdn<'_, (), vir::CSnap> = FunctionIdn::new(
                         vir::vir_format_identifier!(
                             vcx,
-                            "const_{}_{}",
+                            "const_{}_{}_{}",
                             span_pos.line,
-                            span_pos.col_display
+                            span_pos.col_display,
+                            id,
                         ),
                         (),
                         kind.snapshot.downcast_ty(),

prusti-tests/tests/v2/pass/macro_const_naming.rs

@@ -0,0 +1,28 @@
+struct Wrap(i32);
+impl Wrap {
+    fn get(&self) -> i32 {
+        self.0
+    }
+}
+const ARR: [Wrap; 3] = [Wrap(1), Wrap(2), Wrap(3)];
+
+// `assert_eq!` lookalike without the `requires(false)` precondition
+macro_rules! check_eq {
+    ($l:expr, $r:expr) => {{
+        let _ = (&$l, &$r);
+    }};
+}
+
+fn test_const_multi_use() {
+    // A single textual reference (`ARR[1].get()`) lowers to multiple MIR
+    // statements that each emit a ConstOperand for `ARR` with the same source span.
+    let _ = ARR[1].get();
+}
+
+fn test() {
+    // Same macro invoked twice: identical macro-definition span across calls.
+    check_eq!([1, 2, 3], [1, 2, 3]);
+    check_eq!([4, 5, 6], [4, 5, 6]);
+    // Nested array literal: recursive emissions inside one task share the span.
+    check_eq!([[1, 2], [3, 4]], [[1, 2], [3, 4]]);
+}