1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
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;
}
}
}
|
