Skip to content

Disambiguate adt names#156

Open
Trzyq0712 wants to merge 3 commits into
Aurel300:rewrite-2023from
Trzyq0712:disambiguate_types
Open

Disambiguate adt names#156
Trzyq0712 wants to merge 3 commits into
Aurel300:rewrite-2023from
Trzyq0712:disambiguate_types

Conversation

@Trzyq0712
Copy link
Copy Markdown

@Trzyq0712 Trzyq0712 commented Mar 19, 2026

Addresses #155.

Problem

Using base names for types caused ConsistencyError collisions in the VIPER backend, notably for:

  • Cross-module (or crate) collisions: e.g., std::ascii::EscapeDefault vs. std::char::EscapeDefault.
  • Local shadowing: Multiple struct Bar definitions in different scopes of the same function.

Solution

  1. Joining the crate name and all path segments with $$.
  2. Appending the compiler's internal disambiguator (using $) when it is non-zero.
  3. Explicitly handling anonymous namespaces and associated types to ensure local uniqueness.

Example Output:

  • 0$$core$$ascii$$EscapeDefault
  • 0$$main$$Bar vs. 0$$main$$Bar$1

Comment thread prusti-encoder/src/encoders/ty/rust_ty.rs Outdated
@JonasAlaif
Copy link
Copy Markdown
Collaborator

JonasAlaif commented Mar 20, 2026

I'm not such a big fan of this since it'll make the Viper program virtually unreadable (even more so than it already is), even for small programs. Any solution that does this would need to use the simple name if there is no conflict and the complex name otherwise. Alternatively, to be able to toggle this under a configuration flag.

Note that you could probably replace your implementation with rustc's debug formatting for DefId followed by a sanitize (to replace all the :: with Viper-valid stuff).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants