Merge

3 files changed, 149 insertions, 0 deletions

diff --git a/Source/ModelViewer/BCTProvider.cs b/Source/ModelViewer/BCTProvider.cs
new file mode 100644
index 00000000..6b48c396
--- /dev/null
+++ b/Source/ModelViewer/BCTProvider.cs
@@ -0,0 +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));

+    }

+  }

+}

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index bb6d8c11..afe0593c 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -33,6 +33,7 @@ namespace Microsoft.Boogie.ModelViewer
     // TODO this should be dynamically loaded

     IEnumerable<ILanguageProvider> Providers()

     {

+      yield return BCT.Provider.Instance;

       yield return Vcc.Provider.Instance;

       yield return Dafny.Provider.Instance;

       yield return Base.Provider.Instance;

diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index 6262ae2f..3a25e5cc 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -113,6 +113,7 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="BaseProvider.cs" />

+    <Compile Include="BCTProvider.cs" />

     <Compile Include="DafnyProvider.cs" />

     <Compile Include="DataModel.cs" />

     <Compile Include="Main.cs">