diff options
Diffstat (limited to 'Source/ModelViewer/BCTProvider.cs')
-rw-r--r-- | Source/ModelViewer/BCTProvider.cs | 294 |
1 files changed, 147 insertions, 147 deletions
diff --git a/Source/ModelViewer/BCTProvider.cs b/Source/ModelViewer/BCTProvider.cs index 6b48c396..3126084f 100644 --- a/Source/ModelViewer/BCTProvider.cs +++ b/Source/ModelViewer/BCTProvider.cs @@ -1,147 +1,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));
- }
- }
-}
+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)); + } + } +} |