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
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
namespace Microsoft.Boogie.ModelViewer.BCT {
public class Provider : ILanguageProvider {
public static Provider Instance = new Provider();
private Provider() { }
public bool IsMyModel(Model m) {
return m.TryGetFunc("$Alloc") != null;
}
public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts) {
var dm = new BCTModel(m, opts);
foreach (var s in m.States) {
var sn = new StateNode(dm.states.Count, dm, s);
dm.states.Add(sn);
}
dm.FinishStates();
return dm;
}
}
class BCTModel : LanguageModel {
public readonly Model.Func f_heap_select;
public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();
Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();
public List<StateNode> states = new List<StateNode>();
public BCTModel(Model m, ViewOptions opts)
: base(m, opts) {
f_heap_select = m.MkFunc("[3]", 3);
foreach (Model.Func fn in m.Functions) {
}
}
internal void FinishStates() {
GenerateSourceLocations(states);
}
public override IEnumerable<IState> States {
get { return states; }
}
public string GetUserVariableName(string name) {
if (name == "$this")
return "this";
if (name.Contains("$"))
return null;
if (name == "isControlChecked" || name == "isControlEnabled")
return null;
return name;
}
public Model.Element Image(Model.Element elt, Model.Func f) {
var r = f.AppWithResult(elt);
if (r != null)
return r.Args[0];
return null;
}
public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt) {
List<ElementNode> result = new List<ElementNode>();
return result;
}
}
class StateNode : NamedState {
internal readonly BCTModel dm;
internal readonly List<VariableNode> vars = new List<VariableNode>();
internal readonly int index;
public StateNode(int i, BCTModel parent, Model.CapturedState s)
: base(s, parent) {
dm = parent;
state = s;
index = i;
SetupVars();
}
void SetupVars() {
var names = Util.Empty<string>();
if (dm.states.Count > 0) {
var prev = dm.states.Last();
names = prev.vars.Map(v => v.realName);
}
names = names.Concat(state.Variables).Distinct();
var curVars = state.Variables.ToDictionary(x => x);
foreach (var v in names) {
if (dm.GetUserVariableName(v) != null) {
var val = state.TryGet(v);
var vn = new VariableNode(this, v, val);
vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v);
if (curVars.ContainsKey(v))
dm.RegisterLocalValue(vn.Name, val);
vars.Add(vn);
}
}
dm.Flush(Nodes);
}
public override IEnumerable<IDisplayNode> Nodes {
get {
return vars;
}
}
}
class ElementNode : DisplayNode {
protected StateNode stateNode;
protected Model.Element elt;
protected BCTModel vm { get { return stateNode.dm; } }
public ElementNode(StateNode st, EdgeName name, Model.Element elt)
: base(st.dm, name, elt) {
this.stateNode = st;
this.elt = elt;
}
public ElementNode(StateNode st, string name, Model.Element elt)
: this(st, new EdgeName(name), elt) { }
protected override void ComputeChildren() {
children.AddRange(vm.GetExpansion(stateNode, elt));
}
}
class VariableNode : ElementNode {
public bool updatedHere;
public string realName;
public VariableNode(StateNode par, string realName, Model.Element elt)
: base(par, realName, elt) {
this.realName = realName;
name = new EdgeName(vm.GetUserVariableName(realName));
}
}
}
|
