From 6d24f98bd782fcac14df8323dab6e1bad2c1b8de Mon Sep 17 00:00:00 2001 From: Richard Wohlbold Date: Sat, 16 May 2026 13:32:15 +0200 Subject: [PATCH 1/3] Fix duplicate constant names in macro expansions --- prusti-encoder/src/encoders/const.rs | 41 ++++++++++++++----- .../tests/v2/pass/macro_const_naming.rs | 4 ++ 2 files changed, 35 insertions(+), 10 deletions(-) create mode 100644 prusti-tests/tests/v2/pass/macro_const_naming.rs diff --git a/prusti-encoder/src/encoders/const.rs b/prusti-encoder/src/encoders/const.rs index 334bfc640b8..a66f7260eeb 100644 --- a/prusti-encoder/src/encoders/const.rs +++ b/prusti-encoder/src/encoders/const.rs @@ -130,18 +130,39 @@ 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 gen_snap_func_idn: FunctionIdn<'_, (), vir::CSnap> = FunctionIdn::new( + // We need to choose a unique identifier to avoid name collisions. + // This is tricky for constants in macro expansions. + // Expanding the same macro twice leads to identical `self.span` values. + // We choose to keep identifiers simpler if we are in a non-macro context. + let source_map = vcx.tcx().sess.source_map(); + let source_span = self.span.source_callsite(); + let callsite = source_map.lookup_char_pos(source_span.lo()); + let name = if source_span == self.span { + // Non-macro case: a single position is already unique. vir::vir_format_identifier!( vcx, - "const_{}_{}", - span_pos.line, - span_pos.col_display - ), - (), - kind.snapshot.downcast_ty(), - ); + "const_{}_{}_{}", + callsite.line, + callsite.col_display, + self.span.lo().0, + ) + } else { + // Macro case: the macro definition site (`self.span`) distinguishes constants + // within one invocation; the call site distinguishes between invocations. + let original = source_map.lookup_char_pos(self.span.lo()); + vir::vir_format_identifier!( + vcx, + "const_{}_{}_{}__{}_{}_{}", + callsite.line, + callsite.col_display, + source_span.lo().0, + original.line, + original.col_display, + self.span.lo().0, + ) + }; + let gen_snap_func_idn: FunctionIdn<'_, (), vir::CSnap> = + FunctionIdn::new(name, (), kind.snapshot.downcast_ty()); self.functions.push(vcx.mk_function( gen_snap_func_idn, (), diff --git a/prusti-tests/tests/v2/pass/macro_const_naming.rs b/prusti-tests/tests/v2/pass/macro_const_naming.rs new file mode 100644 index 00000000000..e9bb5e9e10f --- /dev/null +++ b/prusti-tests/tests/v2/pass/macro_const_naming.rs @@ -0,0 +1,4 @@ +fn test() { + assert_eq!([1, 2, 3], [1, 2, 3]); + assert_eq!([4, 5, 6], [4, 5, 6]); +} From d0218e646837e24c856dae266a001ff4a1e0d3df Mon Sep 17 00:00:00 2001 From: Richard Wohlbold Date: Thu, 21 May 2026 11:50:59 +0200 Subject: [PATCH 2/3] Use span+counter for consts --- prusti-encoder/src/encoders/const.rs | 54 +++++++++---------- .../tests/v2/pass/macro_const_naming.rs | 17 ++++++ 2 files changed, 41 insertions(+), 30 deletions(-) diff --git a/prusti-encoder/src/encoders/const.rs b/prusti-encoder/src/encoders/const.rs index a66f7260eeb..c9f4dd9a290 100644 --- a/prusti-encoder/src/encoders/const.rs +++ b/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 = const { std::cell::Cell::new(0) }; +} + struct Enc<'enc, 'vir: 'enc> { deps: &'enc mut TaskEncoderDependencies<'vir, ConstEnc>, ecx: &'enc InterpCx<'vir, CompileTimeMachine<'vir>>, @@ -130,39 +135,28 @@ impl<'enc, 'vir: 'enc> Enc<'enc, 'vir> { ), ); } - // We need to choose a unique identifier to avoid name collisions. - // This is tricky for constants in macro expansions. - // Expanding the same macro twice leads to identical `self.span` values. - // We choose to keep identifiers simpler if we are in a non-macro context. - let source_map = vcx.tcx().sess.source_map(); - let source_span = self.span.source_callsite(); - let callsite = source_map.lookup_char_pos(source_span.lo()); - let name = if source_span == self.span { - // Non-macro case: a single position is already unique. + 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_{}_{}_{}", - callsite.line, - callsite.col_display, - self.span.lo().0, - ) - } else { - // Macro case: the macro definition site (`self.span`) distinguishes constants - // within one invocation; the call site distinguishes between invocations. - let original = source_map.lookup_char_pos(self.span.lo()); - vir::vir_format_identifier!( - vcx, - "const_{}_{}_{}__{}_{}_{}", - callsite.line, - callsite.col_display, - source_span.lo().0, - original.line, - original.col_display, - self.span.lo().0, - ) - }; - let gen_snap_func_idn: FunctionIdn<'_, (), vir::CSnap> = - FunctionIdn::new(name, (), kind.snapshot.downcast_ty()); + span_pos.line, + span_pos.col_display, + id, + ), + (), + kind.snapshot.downcast_ty(), + ); self.functions.push(vcx.mk_function( gen_snap_func_idn, (), diff --git a/prusti-tests/tests/v2/pass/macro_const_naming.rs b/prusti-tests/tests/v2/pass/macro_const_naming.rs index e9bb5e9e10f..d4bb15d63df 100644 --- a/prusti-tests/tests/v2/pass/macro_const_naming.rs +++ b/prusti-tests/tests/v2/pass/macro_const_naming.rs @@ -1,4 +1,21 @@ +struct Wrap(i32); +impl Wrap { + fn get(&self) -> i32 { + self.0 + } +} +const ARR: [Wrap; 3] = [Wrap(1), Wrap(2), Wrap(3)]; + +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. assert_eq!([1, 2, 3], [1, 2, 3]); assert_eq!([4, 5, 6], [4, 5, 6]); + // Nested array literal: recursive emissions inside one task share the span. + assert_eq!([[1, 2], [3, 4]], [[1, 2], [3, 4]]); } From d5a77d21ff95884eda1f3d9ba11e471d1152be2b Mon Sep 17 00:00:00 2001 From: Richard Wohlbold Date: Thu, 21 May 2026 13:09:42 +0200 Subject: [PATCH 3/3] Fix failing test --- prusti-tests/tests/v2/pass/macro_const_naming.rs | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/prusti-tests/tests/v2/pass/macro_const_naming.rs b/prusti-tests/tests/v2/pass/macro_const_naming.rs index d4bb15d63df..1b529321d91 100644 --- a/prusti-tests/tests/v2/pass/macro_const_naming.rs +++ b/prusti-tests/tests/v2/pass/macro_const_naming.rs @@ -6,6 +6,13 @@ impl Wrap { } 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. @@ -14,8 +21,8 @@ fn test_const_multi_use() { fn test() { // Same macro invoked twice: identical macro-definition span across calls. - assert_eq!([1, 2, 3], [1, 2, 3]); - assert_eq!([4, 5, 6], [4, 5, 6]); + 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. - assert_eq!([[1, 2], [3, 4]], [[1, 2], [3, 4]]); + check_eq!([[1, 2], [3, 4]], [[1, 2], [3, 4]]); }