From cd2643c9f8b6069771e0e9ab5ff9f33f975ae4f8 Mon Sep 17 00:00:00 2001 From: MichalMoskal Date: Tue, 26 Oct 2010 01:36:51 +0000 Subject: Handle aliases better --- Source/ModelViewer/Main.Designer.cs | 13 +-- Source/ModelViewer/Main.cs | 10 ++ Source/ModelViewer/Namer.cs | 2 +- Source/ModelViewer/VccProvider.cs | 189 +----------------------------------- 4 files changed, 20 insertions(+), 194 deletions(-) (limited to 'Source') diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs index eae222aa..46125e74 100644 --- a/Source/ModelViewer/Main.Designer.cs +++ b/Source/ModelViewer/Main.Designer.cs @@ -30,12 +30,12 @@ this.currentStateView = new System.Windows.Forms.ListView(); this.name = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader())); this.value = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader())); + this.aliases = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader())); this.splitContainer1 = new System.Windows.Forms.SplitContainer(); this.stateList = new System.Windows.Forms.ListView(); this.columnHeader3 = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader())); this.columnHeader1 = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader())); this.columnHeader2 = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader())); - this.aliases = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader())); ((System.ComponentModel.ISupportInitialize)(this.splitContainer1)).BeginInit(); this.splitContainer1.Panel1.SuspendLayout(); this.splitContainer1.Panel2.SuspendLayout(); @@ -80,6 +80,11 @@ this.value.Text = "Value"; this.value.Width = 99; // + // aliases + // + this.aliases.Text = "Aliases"; + this.aliases.Width = 325; + // // splitContainer1 // this.splitContainer1.Dock = System.Windows.Forms.DockStyle.Fill; @@ -107,6 +112,7 @@ this.stateList.FullRowSelect = true; this.stateList.GridLines = true; this.stateList.HeaderStyle = System.Windows.Forms.ColumnHeaderStyle.Nonclickable; + this.stateList.HideSelection = false; this.stateList.Location = new System.Drawing.Point(0, 0); this.stateList.MultiSelect = false; this.stateList.Name = "stateList"; @@ -132,11 +138,6 @@ this.columnHeader2.Text = "Value"; this.columnHeader2.Width = 116; // - // aliases - // - this.aliases.Text = "Aliases"; - this.aliases.Width = 325; - // // Main // this.AutoScaleDimensions = new System.Drawing.SizeF(6F, 13F); diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 800455f0..609bf571 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -223,8 +223,15 @@ namespace Microsoft.Boogie.ModelViewer private void stateList_SelectedIndexChanged(object sender, EventArgs e) { + if (stateList.SelectedItems.Count == 0) return; var sel = stateList.SelectedItems[0].Index; + + var normalFont = stateList.Font; + var boldFont = new Font(normalFont, FontStyle.Bold); + stateList.Items[currentState].Font = normalFont; + stateList.Items[sel].Font = boldFont; + SetState(sel); } @@ -294,7 +301,10 @@ namespace Microsoft.Boogie.ModelViewer if (dn == null) return ""; var sb = new StringBuilder(); + var canon = dn.CanonicalValue; foreach (var n in dn.Aliases) { + if (n == canon) + continue; sb.Append(n).Append(", "); if (sb.Length > 300) break; diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs index 859b718a..5d9f41d9 100644 --- a/Source/ModelViewer/Namer.cs +++ b/Source/ModelViewer/Namer.cs @@ -147,7 +147,7 @@ namespace Microsoft.Boogie.ModelViewer { string res; if (canonicalNames.TryGetValue(elt, out res)) - return res; + return res; // +" " + elt.ToString(); return elt.ToString(); } diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index cabc6171..5fbcb86c 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -25,6 +25,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc foreach (var s in vm.states) s.ComputeNames(); Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer)); Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer)); + // Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer)); return vm.states; } } @@ -265,192 +266,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc return result; } } - -#if false - class Namer - { - VccModel vm; - Model model { get { return vm.model; } } - List states { get { return vm.states; } } - - internal Namer(VccModel v) { vm = v; } - - public static readonly string[] synthethic_fields = new string[] { "$f_owns", "$f_ref_cnt", "$f_vol_version", "$f_root", "$f_group_root" }; - Dictionary> names = new Dictionary>(); - Dictionary bestNameFor = new Dictionary(); - List resolutionOrder = new List(); - Dictionary finalNames = new Dictionary(); - - - class EltName - { - public Model.Element For; - public int Score; - public string Format; - public Model.Element[] Arguments; - public string Resolved; - } - - private void AddName(Model.Element elt, int sc, string fmt, params Model.Element[] args) - { - List l; - if (!names.TryGetValue(elt, out l)) { - l = new List(); - names.Add(elt, l); - } - l.Add(new EltName() { Arguments = args, Format = fmt, Score = sc, For = elt }); - } - - private void AddAnyName(Model.Element elt) - { - if (names.ContainsKey(elt)) return; - var nm = new EltName() { Arguments = new Model.Element[0], Format = string.Format("<{0}>", elt.ToString()), Score = 50, For = elt }; - var l = new List(); - l.Add(nm); - names[elt] = l; - } - - private int GetApproxScore(Model.Element e) - { - EltName n; - if (bestNameFor.TryGetValue(e, out n)) - return n.Score; - return 100; - } - - private int CompareNames(EltName x, EltName y) - { - if (x == y) return 0; - if (x.Score == y.Score) { - if (x.Arguments.Length == y.Arguments.Length) - return x.Arguments.Map(GetApproxScore).Sum() - y.Arguments.Map(GetApproxScore).Sum(); - else - return x.Arguments.Length - y.Arguments.Length; - } else { - return x.Score - y.Score; - } - } - - - private void WorkOutBestNameFor(Model.Element e) - { - if (bestNameFor.ContainsKey(e)) return; - if (!names.ContainsKey(e)) AddAnyName(e); - var nm = names[e]; - nm.Sort(CompareNames); - var best = nm[0]; - bestNameFor[e] = best; - foreach (var a in best.Arguments) - WorkOutBestNameFor(a); - resolutionOrder.Add(best); - } - - private void ResolveNames() - { - var keys = names.Keys.ToArray(); - foreach (var e in keys) - WorkOutBestNameFor(e); - var res1 = resolutionOrder.ToArray(); - foreach (var nm in res1) { - var nms = names[nm.For]; - foreach (var subname in nms.Skip(1)) { - subname.Arguments.Iter(WorkOutBestNameFor); - resolutionOrder.Add(subname); - } - } - - foreach (var nm in resolutionOrder) { - var s = nm.Format; - for (int i = nm.Arguments.Length - 1; i >= 0; --i) { - var argName = bestNameFor[nm.Arguments[i]]; - var strName = argName.Resolved; - if (strName == null) strName = argName.For.ToString(); - s = s.Replace("&" + i, strName); - } - nm.Resolved = s; - } - - foreach (var e in names) { - finalNames[e.Key] = e.Value.Map(n => n.Resolved).ToArray(); - } - } - - public Dictionary ComputeNames() - { - ComputeFields(); - ComputeLocals(); - ComputeLiterals(); - ComputeFieldRefs(); - - ResolveNames(); - - return finalNames; - } - - private void ComputeFieldRefs() - { - var fieldStateId = new Dictionary(); - for (int i = 0; i < states.Count; ++i) { - var hp = vm.f_heap.TryEval(states[i].state.TryGet("$s")); - foreach (var fld in vm.f_select_field.AppsWithArg(0, hp)) { - if (!fieldStateId.ContainsKey(fld.Result)) { - fieldStateId[fld.Result] = i; - foreach (var sel in vm.f_select_value.AppsWithArg(0, fld.Result)) { - var val = sel.Result; - var ftp = vm.f_field_type.TryEval(fld.Args[1]); - val = vm.WrapForUse(val, ftp); - AddName(val, 20, string.Format("&0->&1.{0}", i), sel.Args[1], fld.Args[1]); - } - } - } - } - } - - private void ComputeLiterals() - { - foreach (var e in model.Elements) { - Model.Number n = e as Model.Number; - if (n != null) - AddName(n, 5, n.ToString()); - } - } - - private void ComputeLocals() - { - var defined = new HashSet>(); - for (int i = 0; i < states.Count; ++i) { - foreach (var v in states[i].vars) { - var t = Tuple.Create(v.Element, v.Name); - if (!defined.Contains(t)) { - defined.Add(t); - AddName(v.Element, 10, string.Format("{0}.{1}", v.Name, i)); - } - } - } - } - - private void ComputeFields() - { - var fields = vm.f_select_field.Apps.Map(a => a.Args[1]).Concat(vm.f_ptr.Apps.Map(a => a.Args[0])); - foreach (var f in fields) { - foreach (var fn in synthethic_fields) { - foreach (var tpl in model.MkFunc(fn, 1).AppsWithResult(f)) - AddName(f, 5, string.Format("{0}<{1}>", fn.Substring(3), vm.TypeName(tpl.Args[0]))); - } - foreach (var nm in f.Names) { - if (nm.Func.Arity == 0) { - var n = nm.Func.Name; - var idx = n.LastIndexOf('.'); - if (idx > 0) n = n.Substring(idx + 1); - AddName(f, 5, n); - } - } - AddAnyName(f); - } - } - - } -#endif class StateNode : IState { @@ -592,7 +407,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc yield break; } else { foreach (var edge in stateNode.namer.Aliases(Element)) - if (edge != Name) + if (!edge.Equals(Name)) yield return edge.FullName(); } } -- cgit v1.2.3