summaryrefslogtreecommitdiff
path: root/Source/VCExpr/NameClashResolver.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCExpr/NameClashResolver.cs')
-rw-r--r--Source/VCExpr/NameClashResolver.cs392
1 files changed, 196 insertions, 196 deletions
diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs
index a46105f8..0effb386 100644
--- a/Source/VCExpr/NameClashResolver.cs
+++ b/Source/VCExpr/NameClashResolver.cs
@@ -1,196 +1,196 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Text;
-using System.IO;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.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 string Spacer = "@@";
-
- public UniqueNamer() {
- GlobalNames = new Dictionary<Object, string>();
- LocalNames = TEHelperFuns.ToList(new Dictionary<Object/*!*/, string/*!*/>()
- as IDictionary<Object/*!*/, string/*!*/>);
- UsedNames = new HashSet<string>();
- CurrentCounters = new Dictionary<string, int>();
- GlobalPlusLocalNames = new Dictionary<Object, string>();
- }
-
- private UniqueNamer(UniqueNamer namer) {
- Contract.Requires(namer != null);
-
- Spacer = namer.Spacer;
- GlobalNames = new Dictionary<Object, string>(namer.GlobalNames);
- LocalNames = new List<IDictionary<Object, string>>();
-
- foreach (IDictionary<Object/*!*/, string/*!*/>/*!*/ d in namer.LocalNames)
- LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>(d));
-
- UsedNames = new HashSet<string>(namer.UsedNames);
- CurrentCounters = new Dictionary<string, int>(namer.CurrentCounters);
- GlobalPlusLocalNames = new Dictionary<Object, string>(namer.GlobalPlusLocalNames);
- }
-
- public Object Clone() {
- Contract.Ensures(Contract.Result<Object>() != null);
- return new UniqueNamer(this);
- }
-
- public void Reset()
- {
- GlobalNames.Clear();
- LocalNames.Clear();
- LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>());
- UsedNames.Clear();
- CurrentCounters.Clear();
- GlobalPlusLocalNames.Clear();
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalNames;
- [ContractInvariantMethod]
- void GlobalNamesInvariantMethod() {
- Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalNames));
- }
- private readonly List<IDictionary<Object/*!*/, string/*!*/>/*!*/>/*!*/ LocalNames;
- [ContractInvariantMethod]
- void LocalNamesInvariantMethod() {
- Contract.Invariant(Contract.ForAll(LocalNames, i => i != null && cce.NonNullDictionaryAndValues(i)));
- }
-
- // dictionary of all names that have already been used
- // (locally or globally)
- private readonly HashSet<string/*!*/>/*!*/ UsedNames;
- [ContractInvariantMethod]
- void UsedNamesInvariantMethod() {
- Contract.Invariant(cce.NonNull(UsedNames));
- }
- private readonly IDictionary<string/*!*/, int/*!*/>/*!*/ CurrentCounters;
- [ContractInvariantMethod]
- void CurrentCountersInvariantMethod() {
- Contract.Invariant(CurrentCounters != null);
- }
- private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalPlusLocalNames;
- [ContractInvariantMethod]
- void GlobalPlusLocalNamesInvariantMethod() {
- Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalPlusLocalNames));
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- public void PushScope() {
- LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>());
- }
-
- public void PopScope() {
- LocalNames.RemoveAt(LocalNames.Count - 1);
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- private string NextFreeName(Object thingie, string baseName) {
- Contract.Requires(baseName != null);
- Contract.Requires(thingie != null);
- Contract.Ensures(Contract.Result<string>() != null);
- string/*!*/ candidate;
- int counter;
-
- if (CurrentCounters.TryGetValue(baseName, out counter)) {
- candidate = baseName + Spacer + counter;
- counter = counter + 1;
- } else {
- candidate = baseName;
- counter = 0;
- }
-
- while (UsedNames.Contains(candidate)) {
- candidate = baseName + Spacer + counter;
- counter = counter + 1;
- }
-
- UsedNames.Add(candidate);
- CurrentCounters[baseName] = counter;
- GlobalPlusLocalNames[thingie] = candidate;
- 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) {
- Contract.Requires(inherentName != null);
- Contract.Requires(thingie != null);
- Contract.Ensures(Contract.Result<string>() != null);
- string res = this[thingie];
-
- if (res != null)
- return res;
-
- // if the object is not yet registered, create a name for it
- res = NextFreeName(thingie, inherentName);
- GlobalNames.Add(thingie, res);
-
- return res;
- }
-
- [Pure]
- public string this[Object/*!*/ thingie] {
- get {
- Contract.Requires(thingie != null);
-
- 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) {
- Contract.Requires(inherentName != null);
- Contract.Requires(thingie != null);
- Contract.Ensures(Contract.Result<string>() != null);
- string res = NextFreeName(thingie, inherentName);
- LocalNames[LocalNames.Count - 1][thingie] = res;
- return res;
- }
-
- public virtual string GetQuotedName(Object thingie, string inherentName)
- {
- return GetName(thingie, inherentName);
- }
-
- public virtual string GetQuotedLocalName(Object thingie, string inherentName)
- {
- return GetLocalName(thingie, inherentName);
- }
-
- public string Lookup(Object thingie) {
- Contract.Requires(thingie != null);
- Contract.Ensures(Contract.Result<string>() != null);
- string name;
- if (GlobalPlusLocalNames.TryGetValue(thingie, out name))
- return name;
- return Spacer + "undefined" + Spacer + thingie.GetHashCode() + Spacer;
- }
- }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics.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 string Spacer = "@@";
+
+ public UniqueNamer() {
+ GlobalNames = new Dictionary<Object, string>();
+ LocalNames = TEHelperFuns.ToList(new Dictionary<Object/*!*/, string/*!*/>()
+ as IDictionary<Object/*!*/, string/*!*/>);
+ UsedNames = new HashSet<string>();
+ CurrentCounters = new Dictionary<string, int>();
+ GlobalPlusLocalNames = new Dictionary<Object, string>();
+ }
+
+ private UniqueNamer(UniqueNamer namer) {
+ Contract.Requires(namer != null);
+
+ Spacer = namer.Spacer;
+ GlobalNames = new Dictionary<Object, string>(namer.GlobalNames);
+ LocalNames = new List<IDictionary<Object, string>>();
+
+ foreach (IDictionary<Object/*!*/, string/*!*/>/*!*/ d in namer.LocalNames)
+ LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>(d));
+
+ UsedNames = new HashSet<string>(namer.UsedNames);
+ CurrentCounters = new Dictionary<string, int>(namer.CurrentCounters);
+ GlobalPlusLocalNames = new Dictionary<Object, string>(namer.GlobalPlusLocalNames);
+ }
+
+ public Object Clone() {
+ Contract.Ensures(Contract.Result<Object>() != null);
+ return new UniqueNamer(this);
+ }
+
+ public void Reset()
+ {
+ GlobalNames.Clear();
+ LocalNames.Clear();
+ LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>());
+ UsedNames.Clear();
+ CurrentCounters.Clear();
+ GlobalPlusLocalNames.Clear();
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalNames;
+ [ContractInvariantMethod]
+ void GlobalNamesInvariantMethod() {
+ Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalNames));
+ }
+ private readonly List<IDictionary<Object/*!*/, string/*!*/>/*!*/>/*!*/ LocalNames;
+ [ContractInvariantMethod]
+ void LocalNamesInvariantMethod() {
+ Contract.Invariant(Contract.ForAll(LocalNames, i => i != null && cce.NonNullDictionaryAndValues(i)));
+ }
+
+ // dictionary of all names that have already been used
+ // (locally or globally)
+ private readonly HashSet<string/*!*/>/*!*/ UsedNames;
+ [ContractInvariantMethod]
+ void UsedNamesInvariantMethod() {
+ Contract.Invariant(cce.NonNull(UsedNames));
+ }
+ private readonly IDictionary<string/*!*/, int/*!*/>/*!*/ CurrentCounters;
+ [ContractInvariantMethod]
+ void CurrentCountersInvariantMethod() {
+ Contract.Invariant(CurrentCounters != null);
+ }
+ private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalPlusLocalNames;
+ [ContractInvariantMethod]
+ void GlobalPlusLocalNamesInvariantMethod() {
+ Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalPlusLocalNames));
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public void PushScope() {
+ LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>());
+ }
+
+ public void PopScope() {
+ LocalNames.RemoveAt(LocalNames.Count - 1);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private string NextFreeName(Object thingie, string baseName) {
+ Contract.Requires(baseName != null);
+ Contract.Requires(thingie != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ string/*!*/ candidate;
+ int counter;
+
+ if (CurrentCounters.TryGetValue(baseName, out counter)) {
+ candidate = baseName + Spacer + counter;
+ counter = counter + 1;
+ } else {
+ candidate = baseName;
+ counter = 0;
+ }
+
+ while (UsedNames.Contains(candidate)) {
+ candidate = baseName + Spacer + counter;
+ counter = counter + 1;
+ }
+
+ UsedNames.Add(candidate);
+ CurrentCounters[baseName] = counter;
+ GlobalPlusLocalNames[thingie] = candidate;
+ 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) {
+ Contract.Requires(inherentName != null);
+ Contract.Requires(thingie != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ string res = this[thingie];
+
+ if (res != null)
+ return res;
+
+ // if the object is not yet registered, create a name for it
+ res = NextFreeName(thingie, inherentName);
+ GlobalNames.Add(thingie, res);
+
+ return res;
+ }
+
+ [Pure]
+ public string this[Object/*!*/ thingie] {
+ get {
+ Contract.Requires(thingie != null);
+
+ 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) {
+ Contract.Requires(inherentName != null);
+ Contract.Requires(thingie != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ string res = NextFreeName(thingie, inherentName);
+ LocalNames[LocalNames.Count - 1][thingie] = res;
+ return res;
+ }
+
+ public virtual string GetQuotedName(Object thingie, string inherentName)
+ {
+ return GetName(thingie, inherentName);
+ }
+
+ public virtual string GetQuotedLocalName(Object thingie, string inherentName)
+ {
+ return GetLocalName(thingie, inherentName);
+ }
+
+ public string Lookup(Object thingie) {
+ Contract.Requires(thingie != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ string name;
+ if (GlobalPlusLocalNames.TryGetValue(thingie, out name))
+ return name;
+ return Spacer + "undefined" + Spacer + thingie.GetHashCode() + Spacer;
+ }
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 02:59:23 +0000