Chore: Generated Id are now declaration-specific

Source/DafnyCore/AST/CompilationData.cs

@@ -5,8 +5,6 @@
 namespace Microsoft.Dafny;
 
 public class CompilationData {
-  public readonly FreshIdGenerator IdGenerator = new();
-
   public CompilationData(ErrorReporter errorReporter, List<Include> includes, IList<Uri> rootSourceUris, ISet<Uri> alreadyVerifiedRoots, ISet<Uri> alreadyCompiledRoots) {
     Includes = includes;
     ErrorReporter = errorReporter;

Source/DafnyCore/AST/Expressions/Variables/Formal.cs

@@ -35,11 +35,11 @@ public Formal(IToken tok, string name, Type type, bool inParam, bool isGhost, Ex
 
   public bool HasName => !Name.StartsWith("#");
 
-  private string sanitizedName;
-  public override string SanitizedName =>
-    sanitizedName ??= SanitizeName(Name); // No unique-ification
-  public override string CompileName =>
-    compileName ??= SanitizeName(NameForCompilation);
+  public override string GetOrCreateCompileName(CodeGenIdGenerator generator) {
+    return CompileName;
+  }
+
+  public string CompileName => compileName ??= SanitizeName(NameForCompilation);
 
   public override IEnumerable<INode> Children =>
     (DefaultValue != null ? new List<Node> { DefaultValue } : Enumerable.Empty<Node>()).Concat(base.Children);

Source/DafnyCore/AST/Expressions/Variables/IVariable.cs

@@ -19,18 +19,14 @@ string UniqueName {
   bool HasBeenAssignedUniqueName {  // unique names are not assigned until the Translator; if you don't already know if that stage has run, this boolean method will tell you
     get;
   }
-  static FreshIdGenerator CompileNameIdGenerator = new FreshIdGenerator();
-  string AssignUniqueName(FreshIdGenerator generator);
-  string SanitizedName {
-    get;
-  }
-  string SanitizedNameShadowable { // A name suitable for compilation, but without the unique identifier.
-                                   // Useful to generate readable identifiers in the generated source code.
-    get;
-  }
-  string CompileName {
-    get;
-  }
+  string AssignUniqueName(VerificationIdGenerator generator);
+
+  /// <summary>
+  /// A name suitable for compilation, but without the unique identifier.
+  /// Useful to generate readable identifiers in the generated source code.
+  /// </summary>
+  string CompileNameShadowable { get; }
+  string GetOrCreateCompileName(CodeGenIdGenerator generator);
 
   PreType PreType {
     get;

Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs

@@ -35,24 +35,20 @@ public bool HasBeenAssignedUniqueName {
       throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here
     }
   }
-  public string SanitizedName {
-    get {
-      Contract.Ensures(Contract.Result<string>() != null);
-      throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here
-    }
+  public string SanitizedName(CodeGenIdGenerator generator) {
+    Contract.Ensures(Contract.Result<string>() != null);
+    throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here
   }
 
-  public string SanitizedNameShadowable {
+  public string CompileNameShadowable {
     get {
       Contract.Ensures(Contract.Result<string>() != null);
       throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here
     }
   }
-  public string CompileName {
-    get {
-      Contract.Ensures(Contract.Result<string>() != null);
-      throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here
-    }
+  public string GetOrCreateCompileName(CodeGenIdGenerator generator) {
+    Contract.Ensures(Contract.Result<string>() != null);
+    throw new NotImplementedException();  // this getter implementation is here only so that the Ensures contract can be given here
   }
   public Type Type {
     get {
@@ -88,7 +84,7 @@ public bool IsGhost {
   public void MakeGhost() {
     throw new NotImplementedException();
   }
-  public string AssignUniqueName(FreshIdGenerator generator) {
+  public string AssignUniqueName(VerificationIdGenerator generator) {
     Contract.Ensures(Contract.Result<string>() != null);
     throw new NotImplementedException();
   }

Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs

@@ -38,7 +38,7 @@ public string Name {
   private string uniqueName;
   public string UniqueName => uniqueName;
   public bool HasBeenAssignedUniqueName => uniqueName != null;
-  public string AssignUniqueName(FreshIdGenerator generator) {
+  public string AssignUniqueName(VerificationIdGenerator generator) {
     return uniqueName ??= generator.FreshId(Name + "#");
   }
 
@@ -87,16 +87,14 @@ public static string SanitizeName(string nm) {
 
   private string sanitizedNameShadowable;
 
-  public virtual string SanitizedNameShadowable =>
+  public virtual string CompileNameShadowable =>
     sanitizedNameShadowable ??= SanitizeName(Name);
 
-  private string sanitizedName;
-  public virtual string SanitizedName =>
-    sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";
-
   protected string compileName;
-  public virtual string CompileName =>
-    compileName ??= SanitizedName;
+
+  public virtual string GetOrCreateCompileName(CodeGenIdGenerator generator) {
+    return compileName ??= $"_{generator.FreshNumericId()}_{CompileNameShadowable}";
+  }
 
   Type type;
   public bool IsTypeExplicit { get; set; }

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -30,6 +30,8 @@ public override bool CanBeRevealed() {
   public ModuleDefinition EnclosingModule { get { return this.EnclosingClass.EnclosingModuleDefinition; } }
   public bool MustReverify { get { return false; } }
   public bool AllowsNontermination { get { throw new cce.UnreachableException(); } }
+  CodeGenIdGenerator ICodeContext.CodeGenIdGenerator => CodeGenIdGenerator;
+
   public string NameRelativeToModule {
     get {
       if (EnclosingClass is DefaultClassDecl) {

Source/DafnyCore/AST/Members/Function.cs

@@ -200,6 +200,8 @@ public bool AllowsNontermination {
     }
   }
 
+  CodeGenIdGenerator ICodeContext.CodeGenIdGenerator => CodeGenIdGenerator;
+
   /// <summary>
   /// The "AllCalls" field is used for non-ExtremePredicate, non-PrefixPredicate functions only (so its value should not be relied upon for ExtremePredicate and PrefixPredicate functions).
   /// It records all function calls made by the Function, including calls made in the body as well as in the specification.

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -14,6 +14,7 @@ public interface ICodeContext : IASTVisitorContext {
   bool MustReverify { get; }
   string FullSanitizedName { get; }
   bool AllowsNontermination { get; }
+  CodeGenIdGenerator CodeGenIdGenerator { get; }
 }
 
 
@@ -37,6 +38,7 @@ public CodeContextWrapper(ICodeContext inner, bool isGhostContext) {
   public bool MustReverify => inner.MustReverify;
   public string FullSanitizedName => inner.FullSanitizedName;
   public bool AllowsNontermination => inner.AllowsNontermination;
+  CodeGenIdGenerator ICodeContext.CodeGenIdGenerator => inner.CodeGenIdGenerator;
 
   public static ICodeContext Unwrap(ICodeContext codeContext) {
     while (codeContext is CodeContextWrapper ccw) {
@@ -129,6 +131,8 @@ public NoContext(ModuleDefinition module) {
   bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
   public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
   public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
+  CodeGenIdGenerator ICodeContext.CodeGenIdGenerator { get; } = new();
+
   public bool AllowsAllocation => true;
 }
 
@@ -144,7 +148,7 @@ public interface RedirectingTypeDecl : ICallable {
   Expression/*?*/ Constraint { get; }
   SubsetTypeDecl.WKind WitnessKind { get; }
   Expression/*?*/ Witness { get; }  // non-null iff WitnessKind is Compiled or Ghost
-  FreshIdGenerator IdGenerator { get; }
+  VerificationIdGenerator IdGenerator { get; }
 
   [FilledInDuringResolution] bool ConstraintIsCompilable { get; set; }
 }

Source/DafnyCore/AST/Members/Method.cs

@@ -200,6 +200,8 @@ public bool AllowsNontermination {
     }
   }
 
+  CodeGenIdGenerator ICodeContext.CodeGenIdGenerator => CodeGenIdGenerator;
+
   public override string GetCompileName(DafnyOptions options) {
     var nm = base.GetCompileName(options);
     if (nm == Dafny.Compilers.SinglePassCodeGenerator.DefaultNameMain && IsStatic && !IsEntryPoint) {

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -4,6 +4,7 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using Microsoft.Dafny.Auditor;
+using Microsoft.Dafny.Compilers;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;

Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs

@@ -65,23 +65,20 @@ public string DisplayName {
   private string uniqueName;
   public string UniqueName => uniqueName;
   public bool HasBeenAssignedUniqueName => uniqueName != null;
-  public string AssignUniqueName(FreshIdGenerator generator) {
+  public string AssignUniqueName(VerificationIdGenerator generator) {
     return uniqueName ??= generator.FreshId(Name + "#");
   }
 
   private string sanitizedNameShadowable;
 
-  public string SanitizedNameShadowable =>
+  public string CompileNameShadowable =>
     sanitizedNameShadowable ??= NonglobalVariable.SanitizeName(Name);
 
-  private string sanitizedName;
-
-  public string SanitizedName =>
-    sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";
-
   string compileName;
-  public string CompileName =>
-    compileName ??= SanitizedName;
+
+  public string GetOrCreateCompileName(CodeGenIdGenerator generator) {
+    return compileName ??= $"_{generator.FreshNumericId()}_{CompileNameShadowable}";
+  }
 
   // TODO rename and update comment? Or make it nullable?
   public readonly Type SyntacticType;  // this is the type mentioned in the declaration, if any

Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs

@@ -55,6 +55,7 @@ public bool IsRecordType {
   ModuleDefinition IASTVisitorContext.EnclosingModule { get { return EnclosingModuleDefinition; } }
   bool ICodeContext.MustReverify { get { return false; } }
   bool ICodeContext.AllowsNontermination { get { return false; } }
+  CodeGenIdGenerator ICodeContext.CodeGenIdGenerator => CodeGenIdGenerator;
   string ICallable.NameRelativeToModule { get { return Name; } }
   Specification<Expression> ICallable.Decreases {
     get {

Source/DafnyCore/AST/TypeDeclarations/Declaration.cs

@@ -132,9 +132,14 @@ public override string ToString() {
     return Name;
   }
 
-  internal FreshIdGenerator IdGenerator = new();
+  // For Boogie
+  internal VerificationIdGenerator IdGenerator = new();
   public override IEnumerable<INode> Children => (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>());
   public override IEnumerable<INode> PreResolveChildren => Children;
   public abstract SymbolKind? Kind { get; }
   public abstract string GetDescription(DafnyOptions options);
+
+
+  // For Compilation
+  internal CodeGenIdGenerator CodeGenIdGenerator = new();
 }

Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using Microsoft.Dafny.Compilers;
 
 namespace Microsoft.Dafny;
 
@@ -151,6 +152,8 @@ public bool AllowsNontermination {
     }
   }
 
+  CodeGenIdGenerator ICodeContext.CodeGenIdGenerator => CodeGenIdGenerator;
+
   public override bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     formatter.SetMethodLikeIndent(StartToken, OwnedTokens, indentBefore);
     foreach (var req in Requires) {

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -116,7 +116,7 @@ public TypeParameter.EqualitySupportValue EqualitySupport {
   Expression RedirectingTypeDecl.Constraint { get { return Constraint; } }
   SubsetTypeDecl.WKind RedirectingTypeDecl.WitnessKind { get { return WitnessKind; } }
   Expression RedirectingTypeDecl.Witness { get { return Witness; } }
-  FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } }
+  VerificationIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } }
 
   bool ICodeContext.IsGhost {
     get { throw new NotSupportedException(); }  // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper
@@ -126,6 +126,7 @@ bool ICodeContext.IsGhost {
   ModuleDefinition IASTVisitorContext.EnclosingModule { get { return EnclosingModuleDefinition; } }
   bool ICodeContext.MustReverify { get { return false; } }
   bool ICodeContext.AllowsNontermination { get { return false; } }
+  CodeGenIdGenerator ICodeContext.CodeGenIdGenerator => CodeGenIdGenerator;
   string ICallable.NameRelativeToModule { get { return Name; } }
   Specification<Expression> ICallable.Decreases {
     get {

Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs

@@ -73,7 +73,7 @@ bool RedirectingTypeDecl.ConstraintIsCompilable {
 
   SubsetTypeDecl.WKind RedirectingTypeDecl.WitnessKind { get { return SubsetTypeDecl.WKind.CompiledZero; } }
   Expression RedirectingTypeDecl.Witness { get { return null; } }
-  FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } }
+  VerificationIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } }
 
   bool ICodeContext.IsGhost {
     get { throw new NotSupportedException(); }  // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper
@@ -83,6 +83,7 @@ bool ICodeContext.IsGhost {
   ModuleDefinition IASTVisitorContext.EnclosingModule { get { return EnclosingModuleDefinition; } }
   bool ICodeContext.MustReverify { get { return false; } }
   bool ICodeContext.AllowsNontermination { get { return false; } }
+  CodeGenIdGenerator ICodeContext.CodeGenIdGenerator => CodeGenIdGenerator;
   string ICallable.NameRelativeToModule { get { return Name; } }
   Specification<Expression> ICallable.Decreases {
     get {

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -2046,18 +2046,18 @@ protected override void EmitHalt(IToken tok, Expression/*?*/ messageExpr, Concre
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
       List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
 
-      wr.Write($"for ({TypeName(loopIndex.Type, wr, tok)} {loopIndex.CompileName} = ");
+      wr.Write($"for ({TypeName(loopIndex.Type, wr, tok)} {loopIndex.GetOrCreateCompileName(currentIdGenerator)} = ");
       var startWr = wr.Fork();
       wr.Write($"; ");
 
       ConcreteSyntaxTree bodyWr;
       if (goingUp) {
-        wr.Write(endVarName != null ? $"{loopIndex.CompileName} < {endVarName}" : "");
-        bodyWr = wr.NewBlock($"; {loopIndex.CompileName}++)");
+        wr.Write(endVarName != null ? $"{loopIndex.GetOrCreateCompileName(currentIdGenerator)} < {endVarName}" : "");
+        bodyWr = wr.NewBlock($"; {loopIndex.GetOrCreateCompileName(currentIdGenerator)}++)");
       } else {
-        wr.Write(endVarName != null ? $"{endVarName} < {loopIndex.CompileName}" : "");
+        wr.Write(endVarName != null ? $"{endVarName} < {loopIndex.GetOrCreateCompileName(currentIdGenerator)}" : "");
         bodyWr = wr.NewBlock($"; )");
-        bodyWr.WriteLine($"{loopIndex.CompileName}--;");
+        bodyWr.WriteLine($"{loopIndex.GetOrCreateCompileName(currentIdGenerator)}--;");
       }
       bodyWr = EmitContinueLabel(labels, bodyWr);
       TrStmtList(body, bodyWr);

Source/DafnyCore/Backends/CSharp/CsharpSynthesizer.cs

@@ -92,7 +92,7 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method,
       o => codeGenerator.idGenerator.FreshId(o.CompileName + "Return"));
     foreach (var (obj, returnName) in objectToReturnName) {
       parameterString = Regex.Replace(parameterString,
-        $"(^|[^a-zA-Z0-9_]){obj.CompileName}([^a-zA-Z0-9_]|$)",
+        $"(^|[^a-zA-Z0-9_]){obj.GetOrCreateCompileName(codeGenerator.currentIdGenerator)}([^a-zA-Z0-9_]|$)",
         "$1" + returnName + "$2");
     }
     wr.FormatLine($"{keywords}{returnType} {codeGenerator.PublicIdProtect(method.GetCompileName(Options))}{typeParameters}({parameterString}) {{");
@@ -110,7 +110,7 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method,
         wr.FormatLine($"var {mockName} = new Mock<{typeName}>();");
         wr.FormatLine($"{mockName}.CallBase = true;");
       }
-      wr.FormatLine($"var {obj.CompileName} = {mockName}.Object;");
+      wr.FormatLine($"var {obj.GetOrCreateCompileName(method.CodeGenIdGenerator)} = {mockName}.Object;");
     }
 
     // Stub methods and fields according to the Dafny post-conditions:
@@ -244,7 +244,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr,
       var typeName = codeGenerator.TypeName(arg.Type, wr, arg.tok);
       var bound = GetBound(arg);
       if (bound != null) {
-        wr.Format($"{typeName} {bound.Item1.CompileName}");
+        wr.Format($"{typeName} {bound.Item1.GetOrCreateCompileName(codeGenerator.currentIdGenerator)}");
       } else {
         // if the argument is not a bound variable, it is irrelevant to the
         // expression in the lambda
@@ -274,7 +274,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, ForallExpr forallExpr,
       var boundVar = forallExpr.BoundVars[i];
       var varType = codeGenerator.TypeName(boundVar.Type, wr, boundVar.tok);
       bounds[boundVar] = $"It.Is<{varType}>(x => {matcherName}.Match(x))";
-      declarations.Add($"var {boundVar.CompileName} = ({varType}) {tmpId}[{i}];");
+      declarations.Add($"var {boundVar.GetOrCreateCompileName(codeGenerator.currentIdGenerator)} = ({varType}) {tmpId}[{i}];");
     }
 
     wr.WriteLine($"var {matcherName} = new Dafny.MultiMatcher({declarations.Count}, {tmpId} => {{");

Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs

@@ -558,12 +558,12 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT
                   for (int i = 0; i < n - 1; i++) {
                     var ctor_i = dtor.EnclosingCtors[i];
                     var ctor_name = DatatypeSubStructName(ctor_i);
-                    Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[i].CompileName);
+                    Contract.Assert(arg.GetOrCreateCompileName(currentIdGenerator) == dtor.CorrespondingFormals[i].GetOrCreateCompileName(currentIdGenerator));
                     wDtor.WriteLine("if (is_{0}()) {{ return std::get<{0}{1}>(v).{2}; }}",
                       ctor_name, InstantiateTemplate(dt.TypeArgs), IdName(arg));
                   }
 
-                  Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[n - 1].CompileName);
+                  Contract.Assert(arg.GetOrCreateCompileName(currentIdGenerator) == dtor.CorrespondingFormals[n - 1].GetOrCreateCompileName(currentIdGenerator));
                   var final_ctor_name = DatatypeSubStructName(dtor.EnclosingCtors[n - 1], true);
                   wDtor.WriteLine("return std::get<{0}>(v).{1}; ",
                     final_ctor_name, IdName(arg));