1 files changed, 129 insertions, 0 deletions
diff --git a/Source/VCExpr/NameClashResolver.ssc b/Source/VCExpr/NameClashResolver.ssc
new file mode 100644
index 00000000..28a974a6
--- /dev/null
+++ b/Source/VCExpr/NameClashResolver.ssc
@@ -0,0 +1,129 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+
+// Visitor that establishes unique variable (or constant) names in a VCExpr.
+// This is done by adding a counter as suffix if name clashes occur
+
+// TODO: also handle type variables here
+
+namespace Microsoft.Boogie.VCExprAST {
+  using TEHelperFuns = Microsoft.Boogie.TypeErasure.HelperFuns;
+
+  public class UniqueNamer : ICloneable {
+
+    public UniqueNamer() {
+      GlobalNames = new Dictionary<Object!, string!> ();
+      LocalNames = TEHelperFuns.ToList(new Dictionary<Object!, string!> ()
+                                         as IDictionary<Object!, string!>);
+      UsedNames = new Dictionary<string!, bool> ();
+      CurrentCounters = new Dictionary<string!, int> ();
+    }
+
+    private UniqueNamer(UniqueNamer! namer) {
+      GlobalNames = new Dictionary<Object!, string!> (namer.GlobalNames);
+      
+      List<IDictionary<Object!, string!>!>! localNames =
+        new List<IDictionary<Object!, string!>!> ();
+      LocalNames = localNames;
+      
+      foreach (IDictionary<Object!, string!>! d in namer.LocalNames)
+        localNames.Add(new Dictionary<Object!, string!> (d));
+
+      UsedNames = new Dictionary<string!, bool> (namer.UsedNames);
+      CurrentCounters = new Dictionary<string!, int> (namer.CurrentCounters);
+    }
+
+    public Object! Clone() {
+      return new UniqueNamer (this);
+    }
+
+    ////////////////////////////////////////////////////////////////////////////
+
+    private readonly IDictionary<Object!, string!>! GlobalNames;
+    private readonly List<IDictionary<Object!, string!>!>! LocalNames;
+
+    // dictionary of all names that have already been used
+    // (locally or globally)
+    private readonly IDictionary<string!, bool>! UsedNames;
+    private readonly IDictionary<string!, int>! CurrentCounters;
+
+    ////////////////////////////////////////////////////////////////////////////
+
+    public void PushScope() {
+      LocalNames.Add(new Dictionary<Object!, string!> ());
+    }
+
+    public void PopScope() {
+      LocalNames.RemoveAt(LocalNames.Count - 1);
+    }    
+
+    ////////////////////////////////////////////////////////////////////////////
+
+    private string! NextFreeName(string! baseName) {
+      string! candidate;
+      int counter;
+
+      if (CurrentCounters.TryGetValue(baseName, out counter)) {
+        candidate = baseName + "@@" + counter;
+        counter = counter + 1;
+      } else {
+        candidate = baseName;
+        counter = 0;
+      }
+
+      bool dummy;
+      while (UsedNames.TryGetValue(candidate, out dummy)) {
+        candidate = baseName + "@@" + counter;
+        counter = counter + 1;
+      }
+
+      UsedNames.Add(candidate, true);
+      CurrentCounters[baseName] = counter;
+      return candidate;
+    }
+
+    // retrieve the name of a thingie; if it does not have a name yet,
+    // generate a unique name for it (as close as possible to its inherent
+    // name) and register it globally
+    public string! GetName(Object! thingie, string! inherentName) {
+      string res = this[thingie];
+
+      if (res != null)
+        return res;
+
+      // if the object is not yet registered, create a name for it
+      res = NextFreeName(inherentName);
+      GlobalNames.Add(thingie, res);
+
+      return res;
+    }
+
+    [Pure]
+    public string this[Object! thingie] { get {
+      string res;
+      for (int i = LocalNames.Count - 1; i >= 0; --i) {
+        if (LocalNames[i].TryGetValue(thingie, out res))
+          return res;
+      }
+
+      GlobalNames.TryGetValue(thingie, out res);
+      return res;
+    } }
+
+    public string! GetLocalName(Object! thingie, string! inherentName) {
+      string! res = NextFreeName(inherentName);
+      LocalNames[LocalNames.Count - 1][thingie] = res;
+      return res;
+    }
+  }
+}