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
|
//-----------------------------------------------------------------------------
//
// 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;
// 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> {
private readonly FreeVariableCollector! FreeVarCollector =
new FreeVariableCollector ();
private List<VCExprVar!>! FreeVarsIn(VCExpr! expr) {
FreeVarCollector.Collect(expr);
List<VCExprVar!>! freeVars = new List<VCExprVar!> (FreeVarCollector.FreeTermVars.Keys);
FreeVarCollector.Reset();
return freeVars;
}
public LetBindingSorter(VCExpressionGenerator! gen) {
base(gen);
}
public override VCExpr! Visit(VCExprLet! node, bool arg) {
IDictionary<VCExprVar!, Binding!> boundVars =
new Dictionary<VCExprVar!, Binding!> ();
// recurse and collect the free variables in bound terms and formulae
foreach (VCExprLetBinding! binding in node) {
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) {
Binding! b = pair.Value;
foreach (VCExprVar! v in b.FreeVars) {
Binding b2;
if (boundVars.TryGetValue(v, out b2)) {
((!)b2).Occurrences.Add(b);
b.InvOccurrencesNum = b.InvOccurrencesNum + 1;
}
}
}
// topological sort
Stack<Binding!> rootBindings = new Stack<Binding!> ();
foreach (KeyValuePair<VCExprVar!, Binding!> pair in boundVars)
if (pair.Value.InvOccurrencesNum == 0)
rootBindings.Push(pair.Value);
List<Binding!>! sortedBindings = new List<Binding!> ();
while (rootBindings.Count > 0) {
Binding! b = rootBindings.Pop();
sortedBindings.Add(b);
foreach (Binding! b2 in b.Occurrences) {
b2.InvOccurrencesNum = b2.InvOccurrencesNum - 1;
if (b2.InvOccurrencesNum == 0)
rootBindings.Push(b2);
}
}
if (exists{KeyValuePair<VCExprVar!, Binding!> pair in boundVars;
pair.Value.InvOccurrencesNum > 0})
System.Diagnostics.Debug.Fail("Cyclic let-bindings");
assert node.Length == sortedBindings.Count;
// check which of the bindings can be dropped
VCExpr! newBody = Mutate(node.Body, arg);
IDictionary<VCExprVar!, VCExprVar!>! usedVars =
new Dictionary<VCExprVar!, VCExprVar!> ();
foreach (VCExprVar! v in FreeVarsIn(newBody))
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)
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;
// 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) {
this.V = v;
this.E = e;
this.FreeVars = freeVars;
this.Occurrences = new List<Binding> ();
this.InvOccurrencesNum = 0;
}
}
}
}
|
