Unique constant names

[rgwohlbold]

Duplicate constant names account for a significant portion of the error category bug: duplicate identifier in consistency check (no crash) on https://prusti-stdlib-support.rgwohlbold.de.

The current implementation takes the line and col of the span where the constant is defined. This has several problems:

• It does not account for macros. Code which calls a macro twice with inline constants triggers a conflict, since the line and col are the ones of the macro definition site:

fn test() {
    assert_eq!([1, 2, 3], [1, 2, 3]);
    assert_eq!([4, 5, 6], [4, 5, 6]);
}

yields to the error

error: [Prusti internal error] Prusti encountered an unexpected internal error
  |
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: consistency error: ConsistencyError { message: "Consistency error: Duplicate identifier `const_44_15` found. (<no position>)", pos_id: None }

error: [Prusti internal error] Prusti encountered an unexpected internal error
  |
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: consistency error: ConsistencyError { message: "Consistency error: Duplicate identifier `const_44_23` found. (<no position>)", pos_id: None }

Note the spans 44:15 and 44:23 which are inside the standard library source code (where assert_eq! is defined), not user source code.

• If we use self.span.source_callsite() instead of self.span leads to the problem where within one macro invocation like assert_eq!([1, 2, 3], [1, 2, 3]), both constants have the same self.span.source_callsite().lo, another naming conflict:

fn test() {
    assert_eq!([1, 2, 3], [1, 2, 3]);
}

then yields the error

error: [Prusti internal error] Prusti encountered an unexpected internal error
  |
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: consistency error: ConsistencyError { message: "Consistency error: Duplicate identifier `const_2_4` found. (<no position>)", pos_id: None }

Notice the span 2:4 now refers to the a of assert_eq!, but it is the same for both arguments.

Combining self.span with self.span.source_callsite() is not sufficient either. We found two cases this goes wrong:

• There are code snippets where one constant leads to multiple mir::Consts. This can happen because of constant promotion, for example in the following code snippet:

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]]);
}

Here, we have one const ARR and one const test_const_multi_use::promoted[0]. The lo() of the spans is the same, but the hi() is different, corresponding to ARR and ARR[1] respectively.

• Constants like [[1, 2], [3, 4]] are problematic since the inner arrays are encoded separately on the Viper level, but don't have separate spans, triggering a conflict. A solution could be to thread a idx_path: &[usize] through the recursion in encode_const_val_tree

After this investigation, it seems like we can try to add more and more information to the constant names, but this makes them less and less readable, and the code more convoluted, just to get a reasonable identifier. Instead, I propose to add a global counter to the constant names for deduplication and use source_callsite() to translate to user source position (instead of macro definition site) as a compromise.