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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
//-----------------------------------------------------------------------------
//
// 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;
// Sort the bindings in a let-expression so that terms bound earlier do
// not contain variables bound later
namespace Microsoft.Boogie.VCExprAST {
// (argument is not used)
public class LetBindingSorter : MutatingVCExprVisitor<bool> {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(FreeVarCollector != null);
}
private readonly FreeVariableCollector/*!*/ FreeVarCollector =
new FreeVariableCollector();
private List<VCExprVar/*!*/>/*!*/ FreeVarsIn(VCExpr expr) {
Contract.Requires(expr != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
FreeVarCollector.Collect(expr);
List<VCExprVar/*!*/>/*!*/ freeVars = new List<VCExprVar/*!*/>(FreeVarCollector.FreeTermVars.Keys);
FreeVarCollector.Reset();
return freeVars;
}
public LetBindingSorter(VCExpressionGenerator gen):base(gen) {
Contract.Requires(gen != null);
}
public override VCExpr Visit(VCExprLet node, bool arg){
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
IDictionary<VCExprVar/*!*/, Binding/*!*/> boundVars =
new Dictionary<VCExprVar/*!*/, Binding/*!*/> ();
// recurse and collect the free variables in bound terms and formulae
foreach (VCExprLetBinding/*!*/ binding in node) {Contract.Assert(binding != null);
VCExpr/*!*/ newE = Mutate(binding.E, arg);
Binding/*!*/ b = new Binding (binding.V, newE, FreeVarsIn(newE));
boundVars.Add(b.V, b);
}
// generate the occurrence edges
foreach (KeyValuePair<VCExprVar/*!*/, Binding/*!*/> pair in boundVars) {Contract.Assert(cce.NonNullElements(pair));
Binding/*!*/ b = pair.Value;
Contract.Assert(b != null);
foreach (VCExprVar/*!*/ v in b.FreeVars) {Contract.Assert(v != null);
Binding b2;
if (boundVars.TryGetValue(v, out b2)) {
cce.NonNull(b2).Occurrences.Add(b);
b.InvOccurrencesNum = b.InvOccurrencesNum + 1;
}
}
}
// topological sort
Stack<Binding/*!*/> rootBindings = new Stack<Binding/*!*/> ();
foreach (KeyValuePair<VCExprVar/*!*/, Binding/*!*/> pair in boundVars)
{Contract.Assert(cce.NonNullElements(pair));
if (pair.Value.InvOccurrencesNum == 0)
rootBindings.Push(pair.Value);}
List<Binding/*!*/>/*!*/ sortedBindings = new List<Binding/*!*/> ();
while (rootBindings.Count > 0) {
Binding/*!*/ b = rootBindings.Pop();
Contract.Assert(b != null);
sortedBindings.Add(b);
foreach (Binding/*!*/ b2 in b.Occurrences) {
Contract.Assert(b2 != null);
b2.InvOccurrencesNum = b2.InvOccurrencesNum - 1;
if (b2.InvOccurrencesNum == 0)
rootBindings.Push(b2);
}
}
if (Contract.Exists(boundVars, pair=> pair.Value.InvOccurrencesNum > 0))
System.Diagnostics.Debug.Fail("Cyclic let-bindings");
Contract.Assert(node.Length == sortedBindings.Count);
// check which of the bindings can be dropped
VCExpr newBody = Mutate(node.Body, arg);
Contract.Assert(newBody != null);
IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ usedVars =
new Dictionary<VCExprVar/*!*/, VCExprVar/*!*/> ();
foreach (VCExprVar/*!*/ v in FreeVarsIn(newBody)){Contract.Assert(v != null);
if (!usedVars.ContainsKey(v))
usedVars.Add(v, v);}
for (int i = sortedBindings.Count - 1; i >= 0; --i) {
if (usedVars.ContainsKey(sortedBindings[i].V)) {
foreach (VCExprVar/*!*/ v in sortedBindings[i].FreeVars){
Contract.Assert(v != null);
if (!usedVars.ContainsKey(v))
usedVars.Add(v, v);}
} else {
sortedBindings.RemoveAt(i);
}
}
// assemble the resulting let-expression
List<VCExprLetBinding/*!*/>/*!*/ newBindings = new List<VCExprLetBinding/*!*/>();
foreach (Binding b in sortedBindings)
newBindings.Add(Gen.LetBinding(b.V, b.E));
return Gen.Let(newBindings, newBody);
}
private class Binding {
public readonly VCExprVar/*!*/ V;
public readonly VCExpr/*!*/ E;
public readonly List<VCExprVar/*!*/>/*!*/ FreeVars;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(V != null);
Contract.Invariant(E != null);
Contract.Invariant(cce.NonNullElements(FreeVars));
Contract.Invariant(Occurrences != null);
}
// list of all bound expression in which the variable V occurs
// (outgoing edges)
public readonly List<Binding>/*!*/ Occurrences;
// number of variables that are bound in this let-expression
// and that occur in FreeVars
// (incoming edges)
public int InvOccurrencesNum;
public Binding(VCExprVar v, VCExpr e, List<VCExprVar/*!*/>/*!*/ freeVars) {
Contract.Requires(e != null);
Contract.Requires(v != null);
Contract.Requires(cce.NonNullElements(freeVars));
this.V = v;
this.E = e;
this.FreeVars = freeVars;
this.Occurrences = new List<Binding>();
this.InvOccurrencesNum = 0;
}
}
}
}
|
