diff options
| -rw-r--r-- | Source/ModelViewer/BaseProvider.cs | 87 | ||||
| -rw-r--r-- | Source/ModelViewer/DafnyProvider.cs | 129 | ||||
| -rw-r--r-- | Source/ModelViewer/DataModel.cs | 141 | ||||
| -rw-r--r-- | Source/ModelViewer/Main.cs | 31 | ||||
| -rw-r--r-- | Source/ModelViewer/Namer.cs | 350 | ||||
| -rw-r--r-- | Source/ModelViewer/TreeSkeleton.cs | 22 | ||||
| -rw-r--r-- | Source/ModelViewer/VccProvider.cs | 117 |
7 files changed, 301 insertions, 576 deletions
diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs index c4bae59e..8875cce6 100644 --- a/Source/ModelViewer/BaseProvider.cs +++ b/Source/ModelViewer/BaseProvider.cs @@ -15,22 +15,39 @@ namespace Microsoft.Boogie.ModelViewer.Base return true;
}
- IEnumerable<IDisplayNode> GetStateNodes(Model m)
+ public ILanguageSpecificModel GetLanguageSpecificModel(Model m)
{
- yield return GenericNodes.Functions(m);
- yield return GenericNodes.Constants(m);
- foreach (var s in m.States)
- yield return new StateNode(s);
+ return new GenericModel(m);
+ }
+ }
+
+ public class GenericModel : LanguageModel
+ {
+ Model m;
+
+ public GenericModel(Model m)
+ {
+ this.m = m;
}
- public IEnumerable<IState> GetStates(Model m)
+ public IDisplayNode Function(Model.Func f)
{
- yield return new TopState("TOP", GetStateNodes(m));
+ return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(this, a), f.Apps);
}
- public IEnumerable<string> SortFields(IEnumerable<string> fields)
+ IEnumerable<IDisplayNode> GetStateNodes()
{
- return GlobalNamer.DefaultSortFields(fields);
+ yield return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);
+ yield return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.Functions);
+ foreach (var s in m.States)
+ yield return new StateNode(this, s);
+ }
+
+ public override IEnumerable<IState> States
+ {
+ get {
+ yield return new TopState("TOP", GetStateNodes());
+ }
}
}
@@ -38,73 +55,41 @@ namespace Microsoft.Boogie.ModelViewer.Base {
protected Model.CapturedState state;
- public StateNode(Model.CapturedState s) : base(s.Name)
+ public StateNode(ILanguageSpecificModel p, Model.CapturedState s) : base(p, s.Name, null)
{
state = s;
}
- public override IEnumerable<string> Aliases
+ public override string Value
{
- get { foreach (var v in state.Variables) yield return v; }
+ get {
+ return state.Variables.Concat(", ");
+ }
}
- public override bool Expandable { get { return state.VariableCount != 0; } }
-
- public override IEnumerable<IDisplayNode> Expand()
+ protected override void ComputeChildren()
{
foreach (var v in state.Variables) {
- yield return new ElementNode(v, state.TryGet(v));
+ children.Add(new ElementNode(langModel, v, state.TryGet(v)));
}
}
}
public class ElementNode : DisplayNode
{
- protected Model.Element elt;
-
- public ElementNode(string name, Model.Element elt) : base(name)
- {
- this.elt = elt;
- }
-
- public override IEnumerable<string> Aliases
- {
- get
- {
- if (!(elt is Model.Uninterpreted))
- yield return elt.ToString();
- foreach (var tupl in elt.Names) {
- if (tupl.Func.Arity == 0)
- yield return tupl.Func.Name;
- }
- }
- }
+ public ElementNode(ILanguageSpecificModel p, string name, Model.Element elt) : base(p, name, elt) {}
}
public static class GenericNodes
{
- public static IDisplayNode Function(Model.Func f)
- {
- return new ContainerNode<Model.FuncTuple>(f.Name, a => new AppNode(a), f.Apps);
- }
-
- public static IDisplayNode Functions(Model m)
- {
- return new ContainerNode<Model.Func>("Functions", f => f.Arity == 0 ? null : Function(f), m.Functions);
- }
-
- public static IDisplayNode Constants(Model m)
- {
- return new ContainerNode<Model.Func>("Constants", f => f.Arity != 0 ? null : new AppNode(f.Apps.First()), m.Functions);
- }
}
public class AppNode : ElementNode
{
protected Model.FuncTuple tupl;
- public AppNode(Model.FuncTuple t)
- : base(t.Func.Name, t.Result)
+ public AppNode(ILanguageSpecificModel m, Model.FuncTuple t)
+ : base(m, t.Func.Name, t.Result)
{
tupl = t;
var sb = new StringBuilder();
diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs index 41d02a21..cbb4e424 100644 --- a/Source/ModelViewer/DafnyProvider.cs +++ b/Source/ModelViewer/DafnyProvider.cs @@ -17,27 +17,19 @@ namespace Microsoft.Boogie.ModelViewer.Dafny return m.TryGetFunc("$$Language$Dafny") != null;
}
- public IEnumerable<IState> GetStates(Model m)
+ public ILanguageSpecificModel GetLanguageSpecificModel(Model m)
{
var dm = new DafnyModel(m);
foreach (var s in m.States) {
var sn = new StateNode(dm.states.Count, dm, s);
dm.states.Add(sn);
}
- foreach (var s in dm.states) s.ComputeNames();
- dm.gn.ComputeCanonicalNames();
- return dm.states;
- }
-
- public IEnumerable<string> SortFields(IEnumerable<string> fields)
- {
- return GlobalNamer.DefaultSortFields(fields);
+ return dm;
}
}
- class DafnyModel : INamerCallbacks
+ class DafnyModel : LanguageModel
{
- public readonly GlobalNamer gn;
public readonly Model model;
public readonly Model.Func f_heap_select, f_set_select, f_seq_length, f_seq_index, f_box, f_dim, f_index_field, f_multi_index_field;
public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();
@@ -46,7 +38,6 @@ namespace Microsoft.Boogie.ModelViewer.Dafny public DafnyModel(Model m)
{
- gn = new GlobalNamer(this);
model = m;
f_heap_select = m.MkFunc("[3]", 3);
f_set_select = m.MkFunc("[2]", 2);
@@ -78,6 +69,11 @@ namespace Microsoft.Boogie.ModelViewer.Dafny }
}
+ public override IEnumerable<IState> States
+ {
+ get { return states; }
+ }
+
public string GetUserVariableName(string name)
{
if (name == "$Heap" || name == "$_Frame" || name == "#cev_pc")
@@ -104,11 +100,10 @@ namespace Microsoft.Boogie.ModelViewer.Dafny var seqLen = f_seq_length.AppWithArg(0, elt);
if (seqLen != null) {
// elt is a sequence
- var edgname = new EdgeName(state.namer, "|%0|", "|.|", elt);
+ var edgname = new EdgeName(this, "|.|", elt);
result.Add(new FieldNode(state, edgname, seqLen.Result));
foreach (var tpl in f_seq_index.AppsWithArg(0, elt)) {
- var fieldName = string.Format("[{0}]", tpl.Args[1].ToString());
- edgname = new EdgeName(state.namer, "%0" + fieldName, fieldName, elt);
+ edgname = new EdgeName(this, "[%0]", tpl.Args[1]);
result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));
}
@@ -119,7 +114,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny int i = 0;
foreach (var len in lengths) {
var name = lengths.Length == 1 ? "Length" : "Length" + i;
- var edgname = new EdgeName(state.namer, "%0." + name, name, elt);
+ var edgname = new EdgeName(this, name);
result.Add(new FieldNode(state, edgname, len));
i++;
}
@@ -128,7 +123,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny if (heap != null) {
foreach (var tpl in f_heap_select.AppsWithArgs(0, heap, 1, elt)) {
var field = new FieldName(tpl.Args[2], this);
- var edgname = new EdgeName(state.namer, "%0" + (field.Dims == 0 ? "." : "") + field.Name, field.Name, elt);
+ var edgname = new EdgeName(this, field.Name, elt);
result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));
}
}
@@ -193,11 +188,6 @@ namespace Microsoft.Boogie.ModelViewer.Dafny else
return elt;
}
-
- public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)
- {
- return GlobalNamer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);
- }
}
class StateNode : IState
@@ -206,13 +196,11 @@ namespace Microsoft.Boogie.ModelViewer.Dafny readonly string name;
internal readonly DafnyModel dm;
internal readonly List<VariableNode> vars = new List<VariableNode>();
- internal readonly StateNamer namer;
internal readonly int index;
public StateNode(int i, DafnyModel parent, Model.CapturedState s)
{
dm = parent;
- namer = new StateNamer(dm.gn);
state = s;
index = i;
@@ -251,19 +239,13 @@ namespace Microsoft.Boogie.ModelViewer.Dafny 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);
}
}
- foreach (var e in dm.model.Elements) {
- if (e is Model.Number || e is Model.Boolean)
- namer.AddName(e, new EdgeName(e.ToString()));
- }
- }
-
- internal void ComputeNames()
- {
- namer.ComputeNames(vars);
+ dm.Flush(vars);
}
public string Name
@@ -285,10 +267,9 @@ namespace Microsoft.Boogie.ModelViewer.Dafny protected StateNode stateNode;
protected Model.Element elt;
protected DafnyModel vm { get { return stateNode.dm; } }
- protected List<ElementNode> children;
- public ElementNode(StateNode st, IEdgeName name, Model.Element elt)
- : base(name)
+ public ElementNode(StateNode st, EdgeName name, Model.Element elt)
+ : base(st.dm, name, elt)
{
this.stateNode = st;
this.elt = elt;
@@ -297,85 +278,15 @@ namespace Microsoft.Boogie.ModelViewer.Dafny public ElementNode(StateNode st, string name, Model.Element elt)
: this(st, new EdgeName(name), elt) { }
- public override Model.Element Element
- {
- get
- {
- return elt;
- }
- }
-
- protected virtual void DoInitChildren()
+ protected override void ComputeChildren()
{
children.AddRange(vm.GetExpansion(stateNode, elt));
}
-
- protected void InitChildren()
- {
- if (children == null) {
- children = new List<ElementNode>();
- DoInitChildren();
- }
- }
-
- public override string CanonicalValue
- {
- get
- {
- return stateNode.namer.CanonicalName(Element);
- }
- }
-
- public override IEnumerable<string> Aliases
- {
- get
- {
- if (Element is Model.Boolean) {
- yield break;
- } else {
- foreach (var edge in stateNode.namer.Aliases(Element))
- if (!edge.Equals(Name))
- yield return edge.FullName();
- }
- }
- }
-
- public override string ToolTip
- {
- get
- {
- var sb = new StringBuilder();
- int limit = 30;
- foreach (var n in Aliases){
- sb.AppendFormat(" = {0}\n", n);
- if (limit-- < 0) {
- sb.Append("...");
- break;
- }
- }
- return sb.ToString();
- }
- }
-
- public override bool Expandable
- {
- get
- {
- InitChildren();
- return children.Count > 0;
- }
- }
-
- public override IEnumerable<IDisplayNode> Expand()
- {
- InitChildren();
- return children;
- }
}
class FieldNode : ElementNode
{
- public FieldNode(StateNode par, IEdgeName realName, Model.Element elt)
+ public FieldNode(StateNode par, EdgeName realName, Model.Element elt)
: base(par, realName, elt)
{
/*
@@ -388,7 +299,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny class MapletNode : ElementNode
{
- public MapletNode(StateNode par, IEdgeName realName, Model.Element elt)
+ public MapletNode(StateNode par, EdgeName realName, Model.Element elt)
: base(par, realName, elt)
{
}
diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs index 05bc6168..5fedf732 100644 --- a/Source/ModelViewer/DataModel.cs +++ b/Source/ModelViewer/DataModel.cs @@ -8,24 +8,24 @@ namespace Microsoft.Boogie.ModelViewer public interface ILanguageProvider
{
bool IsMyModel(Model m);
- IEnumerable<IState> GetStates(Model m);
+ ILanguageSpecificModel GetLanguageSpecificModel(Model m);
+ }
+
+ public interface ILanguageSpecificModel
+ {
+ string CanonicalName(Model.Element elt);
+
+ string PathName(IEnumerable<IDisplayNode> path);
+
+ IEnumerable<IState> States { get; }
+
IEnumerable<string> SortFields(IEnumerable<string> fields);
}
- public interface INamerCallbacks
+ public interface IState
{
- // Elements (other than integers and Booleans) get canonical names of the form
- // "<base>'<idx>", where <base> is returned by this function, and <idx> is given
- // starting with 0, and incrementing when they are conflicts between bases.
- //
- // This function needs to return an appropriate base name for the element. It is given
- // the element, and if possible an IEdgeName in a particular stat that seems to be the
- // best bet to construct the canonical name from.
- //
- // A reasonable strategy is to check if it's a name of the local, and if so return it,
- // and otherwise use the type of element (e.g., return "seq" for elements representing
- // sequences). It is also possible to return "" in such cases.
- string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx);
+ string Name { get; }
+ IEnumerable<IDisplayNode> Nodes { get; }
}
[Flags]
@@ -35,45 +35,29 @@ namespace Microsoft.Boogie.ModelViewer Changed = 1
}
- public interface IEdgeName
- {
- int CompareTo(IEdgeName other);
- string FullName();
- string ShortName();
- IEnumerable<Model.Element> Dependencies { get; }
- int Score { get; }
- }
-
public interface IDisplayNode
{
/// <summary>
/// Used for indexing the state tree.
/// </summary>
- IEdgeName Name { get; }
+ string Name { get; }
+
+ NodeState State { get; }
+ string Value { get; }
+ string ToolTip { get; }
/// <summary>
/// Used to determine aliasing. Can be null.
/// </summary>
Model.Element Element { get; }
- bool Expandable { get; }
- IEnumerable<IDisplayNode> Expand();
+ IEnumerable<Model.Element> References { get; }
- // Things displayed to the user.
- NodeState State { get; }
- string CanonicalValue { get; }
- IEnumerable<string> Aliases { get; }
- string ToolTip { get; }
+ IEnumerable<IDisplayNode> Children { get; }
object ViewSync { get; set; }
}
- public interface IState
- {
- string Name { get; }
- IEnumerable<IDisplayNode> Nodes { get; }
- }
-
public class TopState : IState
{
@@ -99,26 +83,19 @@ namespace Microsoft.Boogie.ModelViewer public abstract class DisplayNode : IDisplayNode
{
- protected IEdgeName name;
+ protected EdgeName name;
+ protected Model.Element element;
+ protected ILanguageSpecificModel langModel;
+ protected List<IDisplayNode> children;
- public DisplayNode(string n)
- {
- name = new EdgeName(n);
- }
+ public DisplayNode(ILanguageSpecificModel model, string n, Model.Element elt)
+ : this(model, new EdgeName(n), elt) {}
- public DisplayNode(IEdgeName n)
+ public DisplayNode(ILanguageSpecificModel model, EdgeName n, Model.Element elt)
{
+ langModel = model;
name = n;
- }
-
- public virtual string CanonicalValue
- {
- get { return name.FullName(); }
- }
-
- public virtual IEnumerable<string> Aliases
- {
- get { yield break; }
+ element = elt;
}
public virtual string ToolTip
@@ -126,28 +103,55 @@ namespace Microsoft.Boogie.ModelViewer get { return null; }
}
- public virtual bool Expandable
+ public virtual IEnumerable<IDisplayNode> Children
{
- get { return false; }
+ get
+ {
+ if (children == null) {
+ children = new List<IDisplayNode>();
+ ComputeChildren();
+ }
+ return children;
+ }
}
- public virtual IEnumerable<IDisplayNode> Expand()
+ protected virtual void ComputeChildren()
{
- yield break;
}
public virtual NodeState State { get { return NodeState.Normal; } }
public object ViewSync { get; set; }
- public virtual IEdgeName Name
+ public virtual string Name
{
- get { return name; }
+ get { return name.ToString(); }
}
public virtual Model.Element Element
{
- get { return null; }
+ get { return element; }
+ }
+
+ public virtual string Value
+ {
+ get
+ {
+ if (element == null)
+ return "";
+ return langModel.CanonicalName(element);
+ }
+ }
+
+ public IEnumerable<Model.Element> References
+ {
+ get
+ {
+ foreach (var r in name.Dependencies)
+ yield return r;
+ if (element != null)
+ yield return element;
+ }
}
}
@@ -156,7 +160,7 @@ namespace Microsoft.Boogie.ModelViewer protected Func<T, IDisplayNode> convert;
protected IEnumerable<T> data;
- public ContainerNode(IEdgeName name, Func<T, IDisplayNode> convert, IEnumerable<T> data) : base(name)
+ public ContainerNode(EdgeName name, Func<T, IDisplayNode> convert, IEnumerable<T> data) : base(null, name, null)
{
this.convert = convert;
this.data = data;
@@ -167,13 +171,12 @@ namespace Microsoft.Boogie.ModelViewer {
}
- public override bool Expandable { get { return true; } }
- public override IEnumerable<IDisplayNode> Expand()
+ protected override void ComputeChildren()
{
foreach (var f in data) {
var res = convert(f);
if (res != null)
- yield return res;
+ children.Add(res);
}
}
}
@@ -186,6 +189,16 @@ namespace Microsoft.Boogie.ModelViewer if (!cond) throw new System.Exception("assertion violation");
}
+ public static string Concat(this IEnumerable<string> strs, string sep)
+ {
+ var res = new StringBuilder();
+ foreach (var e in strs)
+ res.Append(e).Append(sep);
+ if (res.Length > 0)
+ res.Length -= sep.Length;
+ return res.ToString();
+ }
+
public static IEnumerable<T> Empty<T>() { yield break; }
public static IEnumerable<T> Singleton<T>(T e) { yield return e; }
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 37c7676b..e8a9df36 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -21,12 +21,13 @@ namespace Microsoft.Boogie.ModelViewer int currentState;
IState[] states;
internal ILanguageProvider langProvider;
+ internal ILanguageSpecificModel langModel;
// TODO this should be dynamically loaded
IEnumerable<ILanguageProvider> Providers()
{
yield return Vcc.Provider.Instance;
- yield return Dafny.Provider.Instance;
+ //yield return Dafny.Provider.Instance;
yield return Base.Provider.Instance;
}
@@ -69,7 +70,8 @@ namespace Microsoft.Boogie.ModelViewer }
var items = new List<ListViewItem>();
- states = langProvider.GetStates(m).ToArray();
+ langModel = langProvider.GetLanguageSpecificModel(m);
+ states = langModel.States.ToArray();
unfoldingRoot = new SkeletonItem(this, states.Length);
allItems = unfoldingRoot.PopulateRoot(states);
@@ -279,7 +281,7 @@ namespace Microsoft.Boogie.ModelViewer stateList.BeginUpdate();
for (int i = 0; i < sel.skel.displayNodes.Length; ++i) {
var dn = sel.skel.displayNodes[i];
- stateList.Items[i].SubItems[2].Text = dn == null ? "" : dn.CanonicalValue;
+ stateList.Items[i].SubItems[2].Text = dn == null ? "" : dn.Value;
}
stateList.EndUpdate();
}
@@ -382,7 +384,7 @@ namespace Microsoft.Boogie.ModelViewer }
var tooltip = dispNode.ToolTip;
- var aliases = AliasesAsString(dispNode);
+ var aliases = ""; // AliasesAsString(dispNode);
if (IsMatchListItem)
aliases = "";
if (tooltip != null) {
@@ -391,9 +393,22 @@ namespace Microsoft.Boogie.ModelViewer this.ToolTipText = aliases;
}
- this.SubItems[0].Text = IsMatchListItem ? dispNode.Name.FullName() : dispNode.Name.ShortName();
- this.SubItems[1].Text = active ? dispNode.CanonicalValue : "";
- this.SubItems[2].Text = active ? aliases : "";
+ var name = dispNode.Name;
+
+ if (IsMatchListItem) {
+ Util.Assert(active);
+ var parents = new List<IDisplayNode>();
+ for (var curr = skel; curr != null; curr = curr.parent) {
+ if (curr.parent != null) // skip the root
+ parents.Add(curr.displayNodes[stateId]);
+ }
+ parents.Reverse();
+ name = skel.main.langModel.PathName(parents);
+ }
+
+ this.SubItems[0].Text = name;
+ this.SubItems[1].Text = active ? dispNode.Value : "";
+ // this.SubItems[2].Text = active ? aliases : "";
}
internal DisplayItem()
@@ -401,6 +416,7 @@ namespace Microsoft.Boogie.ModelViewer {
}
+ /*
static internal string AliasesAsString(IDisplayNode dn)
{
if (dn == null) return "";
@@ -417,5 +433,6 @@ namespace Microsoft.Boogie.ModelViewer if (sb.Length > 2) sb.Length -= 2;
return sb.ToString();
}
+ */
}
}
diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs index fc22afef..afbcf4ee 100644 --- a/Source/ModelViewer/Namer.cs +++ b/Source/ModelViewer/Namer.cs @@ -5,42 +5,107 @@ using System.Text; namespace Microsoft.Boogie.ModelViewer
{
- class EltName
+ public abstract class LanguageModel : ILanguageSpecificModel
{
- internal Model.Element elt;
- internal List<IEdgeName> nodes = new List<IEdgeName>();
- internal int score = StateNamer.maxScore;
- internal string theName;
- internal bool unfolded;
- internal int stateIdx;
-
- internal EltName(Model.Element e)
+ protected Dictionary<string, int> baseNameUse = new Dictionary<string, int>();
+ protected Dictionary<Model.Element, string> canonicalName = new Dictionary<Model.Element, string>();
+ protected Dictionary<Model.Element, string> localValue = new Dictionary<Model.Element, string>();
+
+ // Elements (other than integers and Booleans) get canonical names of the form
+ // "<base>'<idx>", where <base> is returned by this function, and <idx> is given
+ // starting with 0, and incrementing when there are conflicts between bases.
+ //
+ // This function needs to return an appropriate base name for the element. It is given
+ // the element.
+ //
+ // A reasonable strategy is to check if it's a name of the local, and if so return it,
+ // and otherwise use the type of element (e.g., return "seq" for elements representing
+ // sequences). It is also possible to return "" in such cases.
+ protected virtual string CanonicalBaseName(Model.Element elt)
{
- elt = e;
- theName = e.ToString();
+ string res;
+ if (localValue.TryGetValue(elt, out res))
+ return res;
+ return "";
}
- }
- public class GlobalNamer
- {
- internal Dictionary<Model.Element, string> canonicalNames;
- INamerCallbacks cb;
- internal List<StateNamer> stateNamers = new List<StateNamer>();
+ public virtual void RegisterLocalValue(string name, Model.Element elt)
+ {
+ string curr;
+ if (localValue.TryGetValue(elt, out curr) && CompareFields(name, curr) >= 0)
+ return;
+ localValue[elt] = name;
+ }
+
+ protected virtual string LiteralName(Model.Element elt)
+ {
+ if (elt is Model.Integer)
+ return elt.ToString();
+ if (elt is Model.Boolean)
+ return elt.ToString();
+ return null;
+ }
- public GlobalNamer(INamerCallbacks cb)
+ public virtual string CanonicalName(Model.Element elt)
{
- this.cb = cb;
+ string res;
+ if (canonicalName.TryGetValue(elt, out res)) return res;
+ res = LiteralName(elt);
+ if (res == null) {
+ var baseName = CanonicalBaseName(elt);
+ int cnt;
+ if (!baseNameUse.TryGetValue(baseName, out cnt)) {
+ cnt = -1;
+ }
+ cnt++;
+ res = baseName + "'" + cnt;
+ baseNameUse[baseName] = cnt;
+ }
+ canonicalName.Add(elt, res);
+ return res;
}
- #region default namer callback implementations
- public static string DefaultCanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)
+ public virtual string PathName(IEnumerable<IDisplayNode> path)
{
- if (edgeName == null)
- return "";
- var name = edgeName.FullName();
- return name;
+ return path.Select(n => n.Name).Concat(".");
}
+ public abstract IEnumerable<IState> States { get; }
+
+ /// <summary>
+ /// Walks each input tree in BFS order, and force evaluation of Name and Value properties
+ /// (to get reasonable numbering of canonical values).
+ /// </summary>
+ public void Flush(IEnumerable<IDisplayNode> roots)
+ {
+ var workList = new Queue<IDisplayNode>();
+
+ Action<IEnumerable<IDisplayNode>> addList = (IEnumerable<IDisplayNode> nodes) =>
+ {
+ var ch = nodes.ToDictionary(x => x.Name);
+ foreach (var k in SortFields(ch.Keys))
+ workList.Enqueue(ch[k]);
+ };
+
+ addList(roots);
+
+ var visited = new HashSet<Model.Element>();
+ while (workList.Count > 0) {
+ var n = workList.Dequeue();
+
+ var dummy1 = n.Name;
+ var dummy2 = n.Value;
+
+ if (n.Element != null) {
+ if (visited.Contains(n.Element))
+ continue;
+ visited.Add(n.Element);
+ }
+
+ addList(n.Children);
+ }
+ }
+ #region field name sorting
static bool HasAny(string s, string chrs)
{
foreach (var c in s)
@@ -60,7 +125,7 @@ namespace Microsoft.Boogie.ModelViewer return res;
}
- public static int CompareFields(string f1, string f2)
+ public virtual int CompareFields(string f1, string f2)
{
bool s1 = HasAny(f1, "[<>]");
bool s2 = HasAny(f2, "[<>]");
@@ -90,233 +155,40 @@ namespace Microsoft.Boogie.ModelViewer return string.CompareOrdinal(f1, f2);
}
- public static IEnumerable<string> DefaultSortFields(IEnumerable<string> fields_)
+ public virtual IEnumerable<string> SortFields(IEnumerable<string> fields_)
{
var fields = new List<string>(fields_);
fields.Sort(CompareFields);
return fields;
}
#endregion
-
- public void ComputeCanonicalNames()
- {
- for (int i = 0; i < 2; i++)
- ComputeCanonicalNamesCore();
- }
-
- void ComputeCanonicalNamesCore()
- {
- var names = new Dictionary<Model.Element, EltName>();
- var namersArr = stateNamers.ToArray();
- for (int i = 0; i < namersArr.Length; ++i) {
- foreach (var n in namersArr[i].eltNames) {
- n.stateIdx = i;
- //if (n.nodes.Count == 0) continue;
- EltName curr;
- if (names.TryGetValue(n.elt, out curr) && curr.score <= n.score)
- continue;
- names[n.elt] = n;
- }
- }
-
- var canonicals = new Dictionary<Model.Element, string>();
- var usedNames = new Dictionary<string, int>();
- Model model = null;
- foreach (var n in names.Values) {
- string name = "";
- model = n.elt.Model;
- if (n.nodes.Count == 0) {
- name = cb.CanonicalBaseName(n.elt, null, 0);
- name = AppendIndex(usedNames, name);
- } else if (n.elt is Model.Boolean || n.elt is Model.Number)
- name = n.nodes[0].FullName();
- else {
- name = cb.CanonicalBaseName(n.elt, n.nodes[0], n.stateIdx);
- name = AppendIndex(usedNames, name);
- }
- canonicals[n.elt] = name;
- }
-
- canonicalNames = canonicals;
-
- foreach (var e in model.Elements) {
- if (!canonicals.ContainsKey(e)) {
- var name = cb.CanonicalBaseName(e, null, 0);
- canonicals[e] = AppendIndex(usedNames, name);
- }
- }
-
- for (int i = 0; i < namersArr.Length; ++i) {
- namersArr[i].ComputeBestName();
- }
- }
-
- private static string AppendIndex(Dictionary<string, int> usedNames, string name)
- {
- var idx = 0;
- if (!usedNames.TryGetValue(name, out idx))
- idx = 0;
- usedNames[name] = idx + 1;
- name = name + "'" + idx;
- return name;
- }
-
- public virtual string CanonicalName(Model.Element elt)
- {
- string res;
- if (canonicalNames != null && canonicalNames.TryGetValue(elt, out res))
- return res; // +" " + elt.ToString();
- return elt.ToString();
- }
}
- public class StateNamer
- {
- GlobalNamer globalNamer;
- internal const int maxScore = 10000;
- internal List<EltName> eltNames = new List<EltName>();
- Dictionary<Model.Element, EltName> unfoldings = new Dictionary<Model.Element, EltName>();
-
- public StateNamer(GlobalNamer gn)
- {
- globalNamer = gn;
- gn.stateNamers.Add(this);
- }
-
- EltName GetName(Model.Element elt)
- {
- EltName res;
- if (unfoldings.TryGetValue(elt, out res))
- return res;
- res = new EltName(elt);
- eltNames.Add(res);
- unfoldings.Add(elt, res);
- return res;
- }
-
- int EdgeNameScore(IEdgeName name)
- {
- return name.Dependencies.Select(e => GetName(e).score).Concat1(0).Max() + name.Score;
- }
-
- internal void ComputeBestName()
- {
- foreach (var n in eltNames) {
- n.score = maxScore;
- string s;
- if (globalNamer.canonicalNames != null && globalNamer.canonicalNames.TryGetValue(n.elt, out s))
- n.theName = s;
- }
-
- while (true) {
- var changes = 0;
- var thisElts = eltNames.ToArray();
- foreach (var elt in thisElts) {
- var newScore = elt.nodes.Select(EdgeNameScore).Concat1(int.MaxValue).Min();
- if (newScore < elt.score) {
- elt.score = newScore;
- changes++;
- }
- }
- if (changes == 0 && thisElts.Length == eltNames.Count)
- break;
- }
- eltNames.Sort((x,y) => x.score - y.score);
- foreach (var elt in eltNames) {
- if (elt.nodes.Count > 0) {
- elt.nodes.Sort((x, y) => EdgeNameScore(x) - EdgeNameScore(y));
- elt.theName = elt.nodes[0].FullName();
- }
- }
- }
-
- void Unfold(IEnumerable<IDisplayNode> ns)
- {
- var workList = new Queue<IDisplayNode>(); // do BFS
- ns.Iter(workList.Enqueue);
-
- while (workList.Count > 0) {
- var n = workList.Dequeue();
-
- if (n.Element != null) {
- var prev = GetName(n.Element);
- prev.nodes.Add(n.Name);
- if (prev.unfolded) // we've already been here
- continue;
- prev.unfolded = true;
- }
-
- if (!n.Expandable) return;
-
- n.Expand().Iter(workList.Enqueue);
- }
- }
-
- public void AddName(Model.Element elt, IEdgeName name)
- {
- var e = GetName(elt);
- e.nodes.Add(name);
- }
-
- public void ComputeNames(IEnumerable<IDisplayNode> n)
- {
- Unfold(n);
- ComputeBestName();
- }
-
- public virtual string ElementName(Model.Element elt)
- {
- return GetName(elt).theName;
- }
-
- public virtual IEnumerable<IEdgeName> Aliases(Model.Element elt)
- {
- return GetName(elt).nodes;
- }
-
- public virtual string CanonicalName(Model.Element elt)
- {
- return globalNamer.CanonicalName(elt);
- }
- }
-
- public class EdgeName : IEdgeName
+ public class EdgeName
{
static readonly Model.Element[] emptyArgs = new Model.Element[0];
- string formatFull, formatShort;
+ ILanguageSpecificModel langModel;
+ string format;
Model.Element[] args;
- StateNamer namer;
- public EdgeName(StateNamer n, string formatFull, string formatShort, params Model.Element[] args)
+ public EdgeName(ILanguageSpecificModel n, string format, params Model.Element[] args)
{
- this.namer = n;
- this.formatFull = formatFull;
- this.formatShort = formatShort;
+ this.langModel = n;
+ this.format = format;
this.args = args;
- Score = args.Length * 10;
- }
-
- public EdgeName(StateNamer n, string formatBoth, params Model.Element[] args)
- : this(n, formatBoth, formatBoth, args)
- {
}
public EdgeName(string name) : this(null, name, emptyArgs) { }
- public virtual int CompareTo(IEdgeName other)
- {
- return string.CompareOrdinal(this.FullName(), other.FullName());
- }
-
public override string ToString()
{
- return FullName();
+ return Format();
}
public override int GetHashCode()
{
- int res = formatFull.GetHashCode() + formatShort.GetHashCode() * 17;
+ int res = format.GetHashCode();
foreach (var c in args) {
res += c.GetHashCode();
res *= 13;
@@ -329,7 +201,7 @@ namespace Microsoft.Boogie.ModelViewer EdgeName e = obj as EdgeName;
if (e == null) return false;
if (e == this) return true;
- if (e.formatFull != this.formatFull || e.formatShort != this.formatShort || e.args.Length != this.args.Length)
+ if (e.format != this.format || e.args.Length != this.args.Length)
return false;
for (int i = 0; i < this.args.Length; ++i)
if (this.args[i] != e.args[i])
@@ -337,7 +209,7 @@ namespace Microsoft.Boogie.ModelViewer return true;
}
- protected virtual string Format(string format)
+ protected virtual string Format()
{
if (args.Length == 0)
return format;
@@ -345,14 +217,16 @@ namespace Microsoft.Boogie.ModelViewer var res = new StringBuilder(format.Length);
for (int i = 0; i < format.Length; ++i) {
var c = format[i];
- var canonical = false;
+ /*
+ var canonical = false;
if (c == '%' && i < format.Length - 1) {
if (format[i + 1] == 'c') {
++i;
canonical = true;
}
}
+ */
if (c == '%' && i < format.Length - 1) {
var j = i + 1;
@@ -361,7 +235,7 @@ namespace Microsoft.Boogie.ModelViewer var len = j - i - 1;
if (len > 0) {
var idx = int.Parse(format.Substring(i + 1, len));
- res.Append(canonical ? namer.CanonicalName(args[idx]) : namer.ElementName(args[idx]));
+ res.Append(langModel.CanonicalName(args[idx]));
i = j - 1;
continue;
}
@@ -373,22 +247,10 @@ namespace Microsoft.Boogie.ModelViewer return res.ToString();
}
- public virtual string FullName()
- {
- return Format(formatFull);
- }
-
- public virtual string ShortName()
- {
- return Format(formatShort);
- }
-
public virtual IEnumerable<Model.Element> Dependencies
{
get { return args; }
}
-
- public virtual int Score { get; set; }
}
}
diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs index 3663f926..b7a83dee 100644 --- a/Source/ModelViewer/TreeSkeleton.cs +++ b/Source/ModelViewer/TreeSkeleton.cs @@ -7,12 +7,12 @@ namespace Microsoft.Boogie.ModelViewer {
internal class SkeletonItem
{
- readonly IEdgeName name;
+ readonly string name;
readonly List<SkeletonItem> children = new List<SkeletonItem>();
internal readonly IDisplayNode[] displayNodes;
internal bool[] isPrimary;
internal readonly SkeletonItem parent;
- readonly Main main;
+ internal readonly Main main;
internal readonly int level;
internal bool expanded, wasExpanded;
internal bool isMatch;
@@ -49,13 +49,13 @@ namespace Microsoft.Boogie.ModelViewer public SkeletonItem(Main m, int stateCount)
{
- name = new EdgeName("<root>");
+ name = "<root>";
main = m;
displayNodes = new IDisplayNode[stateCount];
isPrimary = new bool[stateCount];
}
- internal SkeletonItem(IEdgeName n, SkeletonItem par)
+ internal SkeletonItem(string n, SkeletonItem par)
: this(par.main, par.displayNodes.Length)
{
parent = par;
@@ -65,7 +65,7 @@ namespace Microsoft.Boogie.ModelViewer public bool Expandable
{
- get { return displayNodes.Any(d => d != null && d.Expandable); }
+ get { return displayNodes.Any(d => d != null && d.Children.Count() > 0); }
}
public bool Expanded
@@ -130,10 +130,10 @@ namespace Microsoft.Boogie.ModelViewer var names = new List<string>();
for (int i = 0; i < displayNodes.Length; ++i) {
var dn = displayNodes[i];
- if (dn == null || !dn.Expandable) continue;
- foreach (var child in dn.Expand()) {
+ if (dn == null) continue;
+ foreach (var child in dn.Children) {
SkeletonItem skelChild;
- var name = child.Name.ShortName();
+ var name = child.Name;
if (!created.TryGetValue(name, out skelChild)) {
skelChild = new SkeletonItem(child.Name, this);
created.Add(name, skelChild);
@@ -144,7 +144,7 @@ namespace Microsoft.Boogie.ModelViewer }
}
- foreach (var name in main.langProvider.SortFields(names)) {
+ foreach (var name in main.langModel.SortFields(names)) {
children.Add(created[name]);
}
}
@@ -154,8 +154,8 @@ namespace Microsoft.Boogie.ModelViewer var node = displayNodes[stateId];
if (node == null)
return false;
- var s1 = node.Name.FullName().ToLower();
- var s2 = node.CanonicalValue.ToLower();
+ var s1 = node.Name.ToLower();
+ var s2 = node.Value.ToLower();
foreach (var w in words) {
if (!s1.Contains(w) && !s2.Contains(w))
return false;
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index 8eb9f331..b155f1a1 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -15,23 +15,15 @@ namespace Microsoft.Boogie.ModelViewer.Vcc return m.TryGetFunc("$is_ghost_field") != null && m.TryGetFunc("$fk_vol_version") != null;
}
- public IEnumerable<IState> GetStates(Model m)
+ public ILanguageSpecificModel GetLanguageSpecificModel(Model m)
{
var vm = new VccModel(m);
foreach (var s in m.States) {
var sn = new StateNode(vm.states.Count, vm, s);
vm.states.Add(sn);
}
- foreach (var s in vm.states) s.ComputeNames();
- vm.gn.ComputeCanonicalNames();
- return vm.states;
+ return vm;
}
-
- public IEnumerable<string> SortFields(IEnumerable<string> fields)
- {
- return GlobalNamer.DefaultSortFields(fields);
- }
-
}
enum DataKind
@@ -42,9 +34,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc Map
}
- class VccModel : INamerCallbacks
+ class VccModel : LanguageModel
{
- public readonly GlobalNamer gn;
public readonly Model model;
public readonly Model.Func f_ptr_to, f_phys_ptr_cast, f_spec_ptr_cast, f_mathint, f_local_value_is, f_spec_ptr_to, f_heap, f_select_field,
f_select_value, f_field, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t;
@@ -53,7 +44,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc public VccModel(Model m)
{
- gn = new GlobalNamer(this);
model = m;
f_ptr_to = m.MkFunc("$ptr_to", 1);
f_spec_ptr_to = m.MkFunc("$spec_ptr_to", 1);
@@ -252,7 +242,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc var ftp = f_field_type.TryEval(fld.Args[1]);
val = WrapForUse(val, ftp);
var nm = ConstantFieldName(fld.Args[1]);
- var edgname = nm == null ? new EdgeName(fld.Args[1].ToString()) { Score = 100 } : new EdgeName(state.namer, "%0->" + nm, nm, elt) { Score = 10 };
+ var edgname = nm == null ? new EdgeName(fld.Args[1].ToString()) : new EdgeName(this, nm);
result.Add(new FieldNode(state, edgname, val, ftp));
}
}
@@ -264,7 +254,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc if (sel.Arity == 2 && sel.Name.StartsWith("$select.$map_t")) {
foreach (var app in sel.AppsWithArg(0, elt)) {
var val = WrapForUse(app.Result, elTp);
- var edgname = new EdgeName(state.namer, "%0[%c1]", "[%c1]", elt, app.Args[1]) { Score = 20 };
+ var edgname = new EdgeName(this, "[%0]", app.Args[1]);
result.Add(new MapletNode(state, edgname, val, elTp));
}
}
@@ -273,10 +263,18 @@ namespace Microsoft.Boogie.ModelViewer.Vcc return result;
}
- public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)
+ public override IEnumerable<IState> States
+ {
+ get
+ {
+ return states;
+ }
+ }
+
+ protected override string CanonicalBaseName(Model.Element elt)
{
var vm = this;
- var name = GlobalNamer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);
+ var name = base.CanonicalBaseName(elt);
if (name.Contains("[") || name.Contains("'") || name.Contains("-"))
name = "";
@@ -311,13 +309,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc string name;
internal VccModel vm;
internal List<VariableNode> vars;
- internal StateNamer namer;
internal int index;
public StateNode(int i, VccModel parent, Model.CapturedState s)
{
this.vm = parent;
- this.namer = new StateNamer(vm.gn);
state = s;
index = i;
@@ -361,21 +357,15 @@ namespace Microsoft.Boogie.ModelViewer.Vcc val = vm.WrapForUse(val, tp);
var vn = new VariableNode(this, v, val, tp);
vn.updatedHere = vm.states.Count > 0 && curVars.ContainsKey(v);
+ if (curVars.ContainsKey(v))
+ vm.RegisterLocalValue(vn.Name, val);
vars.Add(vn);
}
}
- foreach (var e in vm.model.Elements) {
- if (e is Model.Number || e is Model.Boolean)
- namer.AddName(e, new EdgeName(e.ToString()));
- }
+ vm.Flush(vars);
}
- internal void ComputeNames()
- {
- namer.ComputeNames(vars);
- }
-
public string Name
{
get { return name; }
@@ -393,62 +383,22 @@ namespace Microsoft.Boogie.ModelViewer.Vcc class ElementNode : DisplayNode
{
protected StateNode stateNode;
- protected Model.Element elt, tp;
+ protected Model.Element tp;
protected VccModel vm { get { return stateNode.vm; } }
- protected List<ElementNode> children;
- public ElementNode(StateNode st, IEdgeName name, Model.Element elt, Model.Element tp)
- : base(name)
+ public ElementNode(StateNode st, EdgeName name, Model.Element elt, Model.Element tp)
+ : base(st.vm, name, elt)
{
this.stateNode = st;
this.tp = tp;
- this.elt = elt;
}
public ElementNode(StateNode st, string name, Model.Element elt, Model.Element tp)
: this(st, new EdgeName(name), elt, tp) { }
- public override Model.Element Element
- {
- get
- {
- return elt;
- }
- }
-
- protected virtual void DoInitChildren()
+ protected override void ComputeChildren()
{
- children.AddRange(vm.GetExpansion(stateNode, elt, tp));
- }
-
- protected void InitChildren()
- {
- if (children == null) {
- children = new List<ElementNode>();
- DoInitChildren();
- }
- }
-
- public override string CanonicalValue
- {
- get
- {
- return stateNode.namer.CanonicalName(Element);
- }
- }
-
- public override IEnumerable<string> Aliases
- {
- get
- {
- if (Element is Model.Boolean) {
- yield break;
- } else {
- foreach (var edge in stateNode.namer.Aliases(Element))
- if (!edge.Equals(Name))
- yield return edge.FullName();
- }
- }
+ children.AddRange(vm.GetExpansion(stateNode, element, tp));
}
public override string ToolTip
@@ -457,6 +407,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc {
var sb = new StringBuilder();
sb.AppendFormat("Type: {0}\n", vm.TypeName(tp));
+ /*
int limit = 30;
foreach (var n in Aliases){
sb.AppendFormat(" = {0}\n", n);
@@ -465,29 +416,15 @@ namespace Microsoft.Boogie.ModelViewer.Vcc break;
}
}
+ */
return sb.ToString();
}
}
-
- public override bool Expandable
- {
- get
- {
- InitChildren();
- return children.Count > 0;
- }
- }
-
- public override IEnumerable<IDisplayNode> Expand()
- {
- InitChildren();
- return children;
- }
}
class FieldNode : ElementNode
{
- public FieldNode(StateNode par, IEdgeName realName, Model.Element elt, Model.Element tp)
+ public FieldNode(StateNode par, EdgeName realName, Model.Element elt, Model.Element tp)
: base(par, realName, elt, tp)
{
/*
@@ -500,7 +437,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc class MapletNode : ElementNode
{
- public MapletNode(StateNode par, IEdgeName realName, Model.Element elt, Model.Element tp)
+ public MapletNode(StateNode par, EdgeName realName, Model.Element elt, Model.Element tp)
: base(par, realName, elt, tp)
{
}
|