summaryrefslogtreecommitdiff
path: root/Source/ModelViewer
diff options
context:
space:
mode:
Diffstat (limited to 'Source/ModelViewer')
-rw-r--r--Source/ModelViewer/BaseProvider.cs2
-rw-r--r--Source/ModelViewer/DafnyProvider.cs2
-rw-r--r--Source/ModelViewer/DataModel.cs15
-rw-r--r--Source/ModelViewer/Main.Designer.cs110
-rw-r--r--Source/ModelViewer/Main.cs97
-rw-r--r--Source/ModelViewer/Main.resx3
-rw-r--r--Source/ModelViewer/TreeSkeleton.cs20
-rw-r--r--Source/ModelViewer/VccProvider.cs308
8 files changed, 516 insertions, 41 deletions
diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index dddc8c30..b4ed0977 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -15,7 +15,7 @@ namespace Microsoft.Boogie.ModelViewer.Base
return true;
}
- public ILanguageSpecificModel GetLanguageSpecificModel(Model m)
+ public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts)
{
return new GenericModel(m);
}
diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index cbb4e424..56ecd5e5 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -17,7 +17,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
return m.TryGetFunc("$$Language$Dafny") != null;
}
- public ILanguageSpecificModel GetLanguageSpecificModel(Model m)
+ public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts)
{
var dm = new DafnyModel(m);
foreach (var s in m.States) {
diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index d83dfdd5..1330640e 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -5,10 +5,16 @@ using System.Text;
namespace Microsoft.Boogie.ModelViewer
{
+ public class ViewOptions
+ {
+ public int ViewLevel;
+ public bool DebugMode;
+ }
+
public interface ILanguageProvider
{
bool IsMyModel(Model m);
- ILanguageSpecificModel GetLanguageSpecificModel(Model m);
+ ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts);
}
public interface ILanguageSpecificModel
@@ -48,6 +54,8 @@ namespace Microsoft.Boogie.ModelViewer
string Value { get; }
string ToolTip { get; }
+ int ViewLevel { get; }
+
/// <summary>
/// Used to determine aliasing. Can be null.
/// </summary>
@@ -105,6 +113,11 @@ namespace Microsoft.Boogie.ModelViewer
get { return null; }
}
+ public virtual int ViewLevel
+ {
+ get; set;
+ }
+
public virtual IEnumerable<IDisplayNode> Children
{
get
diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index fc3c5291..ae201690 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -46,6 +46,15 @@
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.menuStrip1 = new System.Windows.Forms.MenuStrip();
+ this.fileToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();
+ this.exitToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();
+ this.viewToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();
+ this.normalToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();
+ this.expertToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();
+ this.everythingToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();
+ this.toolStripMenuItem1 = new System.Windows.Forms.ToolStripSeparator();
+ this.debugToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();
this.stateViewMenu.SuspendLayout();
((System.ComponentModel.ISupportInitialize)(this.splitContainer1)).BeginInit();
this.splitContainer1.Panel1.SuspendLayout();
@@ -55,6 +64,7 @@
this.splitContainer2.Panel1.SuspendLayout();
this.splitContainer2.Panel2.SuspendLayout();
this.splitContainer2.SuspendLayout();
+ this.menuStrip1.SuspendLayout();
this.SuspendLayout();
//
// currentStateView
@@ -74,7 +84,7 @@
this.currentStateView.Name = "currentStateView";
this.currentStateView.OwnerDraw = true;
this.currentStateView.ShowItemToolTips = true;
- this.currentStateView.Size = new System.Drawing.Size(596, 558);
+ this.currentStateView.Size = new System.Drawing.Size(596, 539);
this.currentStateView.TabIndex = 0;
this.currentStateView.UseCompatibleStateImageBehavior = false;
this.currentStateView.View = System.Windows.Forms.View.Details;
@@ -117,7 +127,7 @@
// splitContainer1
//
this.splitContainer1.Dock = System.Windows.Forms.DockStyle.Fill;
- this.splitContainer1.Location = new System.Drawing.Point(0, 0);
+ this.splitContainer1.Location = new System.Drawing.Point(0, 24);
this.splitContainer1.Name = "splitContainer1";
//
// splitContainer1.Panel1
@@ -127,7 +137,7 @@
// splitContainer1.Panel2
//
this.splitContainer1.Panel2.Controls.Add(this.stateList);
- this.splitContainer1.Size = new System.Drawing.Size(915, 726);
+ this.splitContainer1.Size = new System.Drawing.Size(915, 702);
this.splitContainer1.SplitterDistance = 596;
this.splitContainer1.TabIndex = 1;
//
@@ -148,8 +158,8 @@
this.splitContainer2.Panel2.Controls.Add(this.linkLabel1);
this.splitContainer2.Panel2.Controls.Add(this.label1);
this.splitContainer2.Panel2.Controls.Add(this.textBox1);
- this.splitContainer2.Size = new System.Drawing.Size(596, 726);
- this.splitContainer2.SplitterDistance = 558;
+ this.splitContainer2.Size = new System.Drawing.Size(596, 702);
+ this.splitContainer2.SplitterDistance = 539;
this.splitContainer2.TabIndex = 1;
//
// matchesList
@@ -168,7 +178,7 @@
this.matchesList.Name = "matchesList";
this.matchesList.OwnerDraw = true;
this.matchesList.ShowItemToolTips = true;
- this.matchesList.Size = new System.Drawing.Size(596, 135);
+ this.matchesList.Size = new System.Drawing.Size(596, 130);
this.matchesList.TabIndex = 4;
this.matchesList.UseCompatibleStateImageBehavior = false;
this.matchesList.View = System.Windows.Forms.View.Details;
@@ -235,7 +245,7 @@
this.stateList.MultiSelect = false;
this.stateList.Name = "stateList";
this.stateList.ShowItemToolTips = true;
- this.stateList.Size = new System.Drawing.Size(315, 726);
+ this.stateList.Size = new System.Drawing.Size(315, 702);
this.stateList.TabIndex = 0;
this.stateList.UseCompatibleStateImageBehavior = false;
this.stateList.View = System.Windows.Forms.View.Details;
@@ -256,12 +266,86 @@
this.columnHeader2.Text = "Value";
this.columnHeader2.Width = 116;
//
+ // menuStrip1
+ //
+ this.menuStrip1.Items.AddRange(new System.Windows.Forms.ToolStripItem[] {
+ this.fileToolStripMenuItem,
+ this.viewToolStripMenuItem});
+ this.menuStrip1.Location = new System.Drawing.Point(0, 0);
+ this.menuStrip1.Name = "menuStrip1";
+ this.menuStrip1.Size = new System.Drawing.Size(915, 24);
+ this.menuStrip1.TabIndex = 1;
+ this.menuStrip1.Text = "menuStrip1";
+ //
+ // fileToolStripMenuItem
+ //
+ this.fileToolStripMenuItem.DropDownItems.AddRange(new System.Windows.Forms.ToolStripItem[] {
+ this.exitToolStripMenuItem});
+ this.fileToolStripMenuItem.Name = "fileToolStripMenuItem";
+ this.fileToolStripMenuItem.Size = new System.Drawing.Size(37, 20);
+ this.fileToolStripMenuItem.Text = "&File";
+ //
+ // exitToolStripMenuItem
+ //
+ this.exitToolStripMenuItem.Name = "exitToolStripMenuItem";
+ this.exitToolStripMenuItem.Size = new System.Drawing.Size(152, 22);
+ this.exitToolStripMenuItem.Text = "&Exit";
+ this.exitToolStripMenuItem.Click += new System.EventHandler(this.exitToolStripMenuItem_Click);
+ //
+ // viewToolStripMenuItem
+ //
+ this.viewToolStripMenuItem.DropDownItems.AddRange(new System.Windows.Forms.ToolStripItem[] {
+ this.normalToolStripMenuItem,
+ this.expertToolStripMenuItem,
+ this.everythingToolStripMenuItem,
+ this.toolStripMenuItem1,
+ this.debugToolStripMenuItem});
+ this.viewToolStripMenuItem.Name = "viewToolStripMenuItem";
+ this.viewToolStripMenuItem.Size = new System.Drawing.Size(44, 20);
+ this.viewToolStripMenuItem.Text = "&View";
+ //
+ // normalToolStripMenuItem
+ //
+ this.normalToolStripMenuItem.Checked = true;
+ this.normalToolStripMenuItem.CheckState = System.Windows.Forms.CheckState.Checked;
+ this.normalToolStripMenuItem.Name = "normalToolStripMenuItem";
+ this.normalToolStripMenuItem.Size = new System.Drawing.Size(152, 22);
+ this.normalToolStripMenuItem.Text = "&Normal";
+ this.normalToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click);
+ //
+ // expertToolStripMenuItem
+ //
+ this.expertToolStripMenuItem.Name = "expertToolStripMenuItem";
+ this.expertToolStripMenuItem.Size = new System.Drawing.Size(152, 22);
+ this.expertToolStripMenuItem.Text = "E&xpert";
+ this.expertToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click);
+ //
+ // everythingToolStripMenuItem
+ //
+ this.everythingToolStripMenuItem.Name = "everythingToolStripMenuItem";
+ this.everythingToolStripMenuItem.Size = new System.Drawing.Size(152, 22);
+ this.everythingToolStripMenuItem.Text = "&Everything";
+ this.everythingToolStripMenuItem.Click += new System.EventHandler(this.normalToolStripMenuItem_Click);
+ //
+ // toolStripMenuItem1
+ //
+ this.toolStripMenuItem1.Name = "toolStripMenuItem1";
+ this.toolStripMenuItem1.Size = new System.Drawing.Size(149, 6);
+ //
+ // debugToolStripMenuItem
+ //
+ this.debugToolStripMenuItem.Name = "debugToolStripMenuItem";
+ this.debugToolStripMenuItem.Size = new System.Drawing.Size(152, 22);
+ this.debugToolStripMenuItem.Text = "Debug";
+ this.debugToolStripMenuItem.Click += new System.EventHandler(this.debugToolStripMenuItem_Click);
+ //
// Main
//
this.AutoScaleDimensions = new System.Drawing.SizeF(6F, 13F);
this.AutoScaleMode = System.Windows.Forms.AutoScaleMode.Font;
this.ClientSize = new System.Drawing.Size(915, 726);
this.Controls.Add(this.splitContainer1);
+ this.Controls.Add(this.menuStrip1);
this.Name = "Main";
this.Text = "Boogie Verification Debugger";
this.stateViewMenu.ResumeLayout(false);
@@ -274,7 +358,10 @@
this.splitContainer2.Panel2.PerformLayout();
((System.ComponentModel.ISupportInitialize)(this.splitContainer2)).EndInit();
this.splitContainer2.ResumeLayout(false);
+ this.menuStrip1.ResumeLayout(false);
+ this.menuStrip1.PerformLayout();
this.ResumeLayout(false);
+ this.PerformLayout();
}
@@ -298,6 +385,15 @@
private System.Windows.Forms.TextBox textBox1;
private System.Windows.Forms.ContextMenuStrip stateViewMenu;
private System.Windows.Forms.ToolStripMenuItem dummyItemToolStripMenuItem;
+ private System.Windows.Forms.MenuStrip menuStrip1;
+ private System.Windows.Forms.ToolStripMenuItem fileToolStripMenuItem;
+ private System.Windows.Forms.ToolStripMenuItem exitToolStripMenuItem;
+ private System.Windows.Forms.ToolStripMenuItem viewToolStripMenuItem;
+ private System.Windows.Forms.ToolStripMenuItem normalToolStripMenuItem;
+ private System.Windows.Forms.ToolStripMenuItem expertToolStripMenuItem;
+ private System.Windows.Forms.ToolStripMenuItem everythingToolStripMenuItem;
+ private System.Windows.Forms.ToolStripSeparator toolStripMenuItem1;
+ private System.Windows.Forms.ToolStripMenuItem debugToolStripMenuItem;
}
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 816043bd..5e1fc0ce 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -22,6 +22,9 @@ namespace Microsoft.Boogie.ModelViewer
IState[] states;
internal ILanguageProvider langProvider;
internal ILanguageSpecificModel langModel;
+ ToolStripMenuItem[] viewItems;
+ Model currentModel;
+ internal ViewOptions viewOpts = new ViewOptions();
// TODO this should be dynamically loaded
IEnumerable<ILanguageProvider> Providers()
@@ -35,6 +38,12 @@ namespace Microsoft.Boogie.ModelViewer
{
InitializeComponent();
+ viewItems = new ToolStripMenuItem[] {
+ normalToolStripMenuItem,
+ expertToolStripMenuItem,
+ everythingToolStripMenuItem
+ };
+
var debugBreak = false;
string filename = null;
var args = Environment.GetCommandLineArgs();
@@ -52,26 +61,36 @@ namespace Microsoft.Boogie.ModelViewer
throw new Exception("error: usage: ModelViewer.exe MyProgram.model"); // (where does this exception go?)
}
- Model m;
-
using (var rd = File.OpenText(filename)) {
var models = Model.ParseModels(rd);
- m = models[0];
+ currentModel = models[0];
}
this.Text = Path.GetFileName(filename) + " - Boogie Verification Debugger";
langProvider = null;
foreach (var p in Providers()) {
- if (p.IsMyModel(m)) {
+ if (p.IsMyModel(currentModel)) {
langProvider = p;
break;
}
}
-
+
+ BuildModel();
+ }
+
+ private void BuildModel()
+ {
+ stateList.Items.Clear();
+
var items = new List<ListViewItem>();
- langModel = langProvider.GetLanguageSpecificModel(m);
+ langModel = langProvider.GetLanguageSpecificModel(currentModel, viewOpts);
states = langModel.States.ToArray();
+ var oldRoot = unfoldingRoot;
+ SkeletonItem selectedSkel = null;
+ if (oldRoot != null && SelectedNode() != null) {
+ selectedSkel = SelectedNode().skel;
+ }
unfoldingRoot = new SkeletonItem(this, states.Length);
allItems = unfoldingRoot.PopulateRoot(states);
@@ -84,9 +103,22 @@ namespace Microsoft.Boogie.ModelViewer
}
stateList.Items.AddRange(items.ToArray());
unfoldingRoot.Expanded = true;
- SetState(0);
- stateList.Items[0].Selected = true;
- SetColumnSizes();
+
+ if (oldRoot == null) {
+ SetState(0);
+ stateList.Items[0].Selected = true;
+ SetColumnSizes();
+ } else {
+ var mapping = new Dictionary<SkeletonItem, SkeletonItem>();
+ unfoldingRoot.SyncWith(mapping, oldRoot);
+ SkeletonItem newIt = null;
+ while (selectedSkel != null) {
+ if (mapping.TryGetValue(selectedSkel, out newIt)) break;
+ selectedSkel = selectedSkel.parent;
+ }
+ if (newIt != null) GotoNode(newIt);
+ UpdateMatches(true);
+ }
}
private void SetColumnSizes()
@@ -283,7 +315,6 @@ namespace Microsoft.Boogie.ModelViewer
private void stateList_SelectedIndexChanged(object sender, EventArgs e)
{
-
if (stateList.SelectedItems.Count == 0) return;
var sel = stateList.SelectedItems[0].Index;
@@ -295,10 +326,16 @@ namespace Microsoft.Boogie.ModelViewer
SetState(sel);
}
+ DisplayItem SelectedNode()
+ {
+ if (currentStateView.SelectedItems.Count == 0) return null;
+ return (DisplayItem)currentStateView.SelectedItems[0];
+ }
+
private void currentStateView_SelectedIndexChanged(object sender, EventArgs e)
{
- if (currentStateView.SelectedItems.Count == 0) return;
- var sel = (DisplayItem) currentStateView.SelectedItems[0];
+ var sel = SelectedNode();
+ if (sel == null) return;
stateList.BeginUpdate();
for (int i = 0; i < sel.skel.displayNodes.Length; ++i) {
@@ -443,10 +480,9 @@ namespace Microsoft.Boogie.ModelViewer
{
IDisplayNode sel = null;
SkeletonItem skel = null;
- if (currentStateView.SelectedItems.Count > 0) {
- var it = currentStateView.SelectedItems[0];
- sel = ((DisplayItem)it).dispNode;
- skel = ((DisplayItem)it).skel;
+ if (SelectedNode() != null) {
+ sel = SelectedNode().dispNode;
+ skel = SelectedNode().skel;
}
var items = stateViewMenu.Items;
@@ -472,6 +508,35 @@ namespace Microsoft.Boogie.ModelViewer
AddMenuItems(aliases, items, " = ", 10);
}
}
+
+ private void normalToolStripMenuItem_Click(object sender, EventArgs e)
+ {
+ int viewLev = -1;
+ for (int i = 0; i < viewItems.Length; ++i) {
+ if (viewItems[i] == sender) {
+ viewLev = i;
+ viewItems[i].Checked = true;
+ } else {
+ viewItems[i].Checked = false;
+ }
+ }
+ if (viewLev != -1 && viewLev != viewOpts.ViewLevel) {
+ viewOpts.ViewLevel = viewLev;
+ BuildModel();
+ }
+ }
+
+ private void debugToolStripMenuItem_Click(object sender, EventArgs e)
+ {
+ debugToolStripMenuItem.Checked = !debugToolStripMenuItem.Checked;
+ viewOpts.DebugMode = debugToolStripMenuItem.Checked;
+ BuildModel();
+ }
+
+ private void exitToolStripMenuItem_Click(object sender, EventArgs e)
+ {
+ this.Close();
+ }
}
internal class DisplayItem : ListViewItem
diff --git a/Source/ModelViewer/Main.resx b/Source/ModelViewer/Main.resx
index 0bf101c2..9a1cff5d 100644
--- a/Source/ModelViewer/Main.resx
+++ b/Source/ModelViewer/Main.resx
@@ -120,4 +120,7 @@
<metadata name="stateViewMenu.TrayLocation" type="System.Drawing.Point, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
<value>17, 17</value>
</metadata>
+ <metadata name="menuStrip1.TrayLocation" type="System.Drawing.Point, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
+ <value>152, 17</value>
+ </metadata>
</root> \ No newline at end of file
diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs
index eb0b3059..0c7e6607 100644
--- a/Source/ModelViewer/TreeSkeleton.cs
+++ b/Source/ModelViewer/TreeSkeleton.cs
@@ -65,7 +65,11 @@ namespace Microsoft.Boogie.ModelViewer
public bool Expandable
{
- get { return displayNodes.Any(d => d != null && d.Children.Count() > 0); }
+ get {
+ if (wasExpanded)
+ return children.Count > 0;
+ return displayNodes.Any(d => d != null && d.Children.Count() > 0);
+ }
}
public bool Expanded
@@ -132,6 +136,8 @@ namespace Microsoft.Boogie.ModelViewer
var dn = displayNodes[i];
if (dn == null) continue;
foreach (var child in dn.Children) {
+ if (child.ViewLevel > main.viewOpts.ViewLevel)
+ continue;
SkeletonItem skelChild;
var name = child.Name;
if (!created.TryGetValue(name, out skelChild)) {
@@ -183,6 +189,18 @@ namespace Microsoft.Boogie.ModelViewer
parents.Reverse();
return main.langModel.PathName(parents);
}
+
+ public void SyncWith(Dictionary<SkeletonItem, SkeletonItem> mapping, SkeletonItem old)
+ {
+ mapping[old] = this;
+ Expanded = old.Expanded;
+ var oldCh = old.children.ToDictionary(c => c.name);
+ foreach (var c in children) {
+ SkeletonItem oc;
+ if (oldCh.TryGetValue(c.name, out oc))
+ c.SyncWith(mapping, oc);
+ }
+ }
}
}
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index b155f1a1..1eabc9df 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -15,13 +15,9 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
return m.TryGetFunc("$is_ghost_field") != null && m.TryGetFunc("$fk_vol_version") != null;
}
- public ILanguageSpecificModel GetLanguageSpecificModel(Model m)
+ public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts)
{
- var vm = new VccModel(m);
- foreach (var s in m.States) {
- var sn = new StateNode(vm.states.Count, vm, s);
- vm.states.Add(sn);
- }
+ var vm = new VccModel(m, opts);
return vm;
}
}
@@ -31,6 +27,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
Flat,
PhysPtr,
SpecPtr,
+ Object,
+ Ptrset,
Map
}
@@ -38,12 +36,19 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
{
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;
+ f_select_value, f_field, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t, f_select_ptr,
+ f_owners, f_closed, f_roots, f_timestamps, f_select_bool, f_select_int, f_is_null, f_good_state,
+ f_int_to_version, f_int_to_ptrset, f_set_in0;
+ public readonly Model.Element tp_object, tp_mathint, tp_bool, tp_state, tp_ptrset;
+ public readonly Model.Element elt_me, elt_null;
Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();
+ Dictionary<Model.Element, string> literalName = new Dictionary<Model.Element, string>();
public List<StateNode> states = new List<StateNode>();
+ public readonly ViewOptions viewOpts;
- public VccModel(Model m)
+ public VccModel(Model m, ViewOptions opts)
{
+ viewOpts = opts;
model = m;
f_ptr_to = m.MkFunc("$ptr_to", 1);
f_spec_ptr_to = m.MkFunc("$spec_ptr_to", 1);
@@ -54,14 +59,150 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
f_heap = m.MkFunc("$heap", 1);
f_select_field = m.MkFunc("Select_[$field][$ptr]$int", 2);
f_select_value = m.MkFunc("Select_[$ptr]$int", 2);
+ f_select_ptr = m.MkFunc("Select_[$ptr]$ptr", 2);
+ f_select_int = m.MkFunc("Select_[$ptr]$int", 2);
+ f_select_bool = m.MkFunc("Select_[$ptr]$bool", 2);
+ f_owners = m.MkFunc("$f_owner", 1);
+ f_closed = m.MkFunc("$f_closed", 1);
+ f_roots = m.MkFunc("$roots", 1);
+ f_timestamps = m.MkFunc("$f_timestamp", 1);
f_field = m.MkFunc("$field", 1);
f_field_type = m.MkFunc("$field_type", 1);
f_int_to_ptr = m.MkFunc("$int_to_ptr", 1);
f_ptr_to_int = m.MkFunc("$ptr_to_int", 1);
f_ptr = m.MkFunc("$ptr", 2);
f_map_t = m.MkFunc("$map_t", 2);
+ f_is_null = m.MkFunc("$is_null", 1);
+ f_good_state = m.MkFunc("$good_state", 1);
+ f_int_to_version = m.MkFunc("$int_to_version", 1);
+ f_int_to_ptrset = m.MkFunc("$int_to_ptrset", 1);
+ f_set_in0 = m.MkFunc("$set_in0", 2);
+
+ tp_bool = m.GetFunc("^^bool").GetConstant();
+ tp_mathint = m.GetFunc("^^mathint").GetConstant();
+ tp_object = m.GetFunc("^^object").GetConstant();
+ tp_state = m.GetFunc("^$#state_t").GetConstant();
+ tp_ptrset = m.GetFunc("^$#ptrset").GetConstant();
+
+ elt_me = m.GetFunc("$me").GetConstant();
+ elt_null = m.GetFunc("$null").GetConstant();
+
+ literalName[elt_me] = "\\me";
+ literalName[elt_null] = "NULL";
+ foreach (var tpl in f_phys_ptr_cast.Apps) {
+ if (tpl.Args[0] == elt_null)
+ literalName[tpl.Result] = "(" + TypeName(tpl.Args[1]) + "*)NULL";
+ }
+ foreach (var tpl in f_spec_ptr_cast.Apps) {
+ if (tpl.Args[0] == elt_null)
+ literalName[tpl.Result] = "(" + TypeName(tpl.Args[1]) + "^)NULL";
+ }
+ foreach (var fn in model.Functions) {
+ if (fn.Arity == 0 && fn.Name.StartsWith("l#"))
+ literalName[fn.GetConstant()] = ":" + fn.Name.Substring(2);
+ }
+
+ var idx = 0;
+ foreach (var s in m.States) {
+ var elt = s.TryGet("$s");
+ if (elt != null)
+ literalName[elt] = "\\state'" + idx;
+ idx++;
+ }
+
+ foreach (var s in m.States) {
+ var sn = new StateNode(states.Count, this, s);
+ states.Add(sn);
+ }
}
+ #region Function name scoring
+ static string[][] prefixes = new string[][] {
+ new string[] { "F#", "$eq.$map", },
+ new string[] { "#lambda", },
+ new string[] { "$int_to_", "lambda@", "distinct-aux-f", "Select_","Store_", "$select.", "$store.", },
+ };
+
+ static string[][] totals = new string[][] {
+ new string[] {
+ "$addr", "$current_timestamp",
+ "$full_stop", "$function_entry", "$ptr_to_i4",
+ "$ptr_to_i8", "$ptr_to_u4", "$ptr_to_u8",
+ "$span", "$sizeof", "$in_domain",
+ "$inv2",
+ "$is_claimable",
+ "$set_cardinality", "$set_difference", "$set_union",
+ "$thread_local", "$unchecked", "$writes_at",
+ },
+
+ new string[] {
+ "$dot", "$emb0", "$fetch_from_domain", "$in_range_phys_ptr",
+ "$in_range_spec_ptr", "$is_sequential_field", "$is_volatile_field",
+ "$is_ghost_field", "$is_phys_field", "$is_math_type", "$invok_state",
+ "$is_primitive",
+ "$spec_ptr_cast",
+ "$phys_ptr_cast",
+ "$is_null",
+ "$in_domain_lab",
+ "$inv_lab",
+ "$set_in0",
+ },
+
+ new string[] {
+ "$_pow2", "$as_composite_field", "$as_field_with_type", "$as_in_range_t",
+ "$as_primitive_field", "$base", "$call_transition", "tickleBool", "Ctor",
+ "@MV_state", "$field", "$field_arr_root", "$field_kind", "$field_offset",
+ "$field_parent_type", "$field_type", "$file_name_is", "$good_state",
+ "$good_state_ext", "$function_arg_type", "$has_field_at0", "$map_domain",
+ "$map_range", "$map_t", "$ptr_to", "$ptr_to_i1", "$ptr_to_i2",
+ "$ptr_to_u1", "$ptr_to_u2", "$is_unwrapped", "$is_unwrapped_dynamic",
+ "$heap", "$closed", "$owner", "$owns", "$modifies", "$post_unwrap",
+ "$pow2", "$pre_unwrap", "$ptr", "$is", "$in_range_t", "$roots",
+ "$timestamp", "$type_branch", "$type_code_is", "$type_project_0",
+ "$typemap", "$set_in_pos", "$updated_owns", "$ver_domain", "$vs_state",
+ "$set_singleton",
+ "$f_owner", "$f_closed", "$f_timestamps",
+ "$local_value_is",
+ },
+ };
+
+ string[] state_props = new string[] { };
+
+ Dictionary<string, int> functionScores = new Dictionary<string, int>();
+
+ int FunctionScore(string name)
+ {
+ if (functionScores.Count == 0) {
+ for (int i = 0; i < totals.Length; ++i)
+ foreach (var s in totals[i])
+ functionScores[s] = i;
+ }
+
+ int res;
+ if (functionScores.TryGetValue(name, out res))
+ return res;
+
+ res = -1;
+ if (name[0] == '$' && name.EndsWith("_to_int"))
+ res = 1;
+ else {
+ for (int i = 0; i < prefixes.Length; ++i)
+ foreach (var p in prefixes[i])
+ if (name.StartsWith(p)) {
+ res = i;
+ goto stop;
+ }
+ stop: ;
+ }
+
+ if (res == -1)
+ res = 1; // default
+
+ functionScores[name] = res;
+ return res;
+ }
+ #endregion
+
public string GetUserVariableName(string name)
{
if (name.StartsWith("L#") || name.StartsWith("P#"))
@@ -69,6 +210,22 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
return null;
}
+ protected override string LiteralName(Model.Element elt)
+ {
+ string r;
+
+ if (literalName.TryGetValue(elt, out r))
+ return r;
+
+ r = TryTypeName(elt);
+ if (r != null) {
+ literalName[elt] = r;
+ return r;
+ }
+
+ return base.LiteralName(elt);
+ }
+
public Model.Element LocalType(string localName)
{
var v = GetUserVariableName(localName);
@@ -118,11 +275,20 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
default: return n;
}
}
- return elt.ToString();
+
+ return null;
}
public string TypeName(Model.Element elt)
{
+ var r = TryTypeName(elt);
+ if (r == null)
+ return elt.ToString();
+ else return r;
+ }
+
+ public string TryTypeName(Model.Element elt)
+ {
string res;
if (!typeName.TryGetValue(elt, out res)) {
typeName[elt] = elt.ToString(); // avoid infinite recursion
@@ -164,14 +330,47 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
return bestName;
}
+ bool IsState(Model.Element elt)
+ {
+ return GuessType(elt) == tp_state;
+ }
+
+ Model.Element GuessType(Model.Element element)
+ {
+ if (element is Model.Boolean)
+ return tp_bool;
+
+ foreach (var tpl in element.References) {
+ if (element == tpl.Result) {
+ if (tpl.Func == f_ptr)
+ return tp_object;
+ }
+
+ if (tpl.Args.Length >= 1 && tpl.Args[0] == element) {
+ if (tpl.Func == f_heap || tpl.Func == f_closed || tpl.Func == f_good_state)
+ return tp_state;
+ }
+ }
+
+ return tp_mathint;
+ }
+
public DataKind GetKind(Model.Element tp, out Model.FuncTuple tpl)
{
+ tpl = null;
+
+ if (tp == tp_object)
+ return DataKind.Object;
+ else if (tp == tp_ptrset)
+ return DataKind.Ptrset;
+
tpl = f_ptr_to.AppWithResult(tp);
if (tpl != null) return DataKind.PhysPtr;
tpl = f_spec_ptr_to.AppWithResult(tp);
if (tpl != null) return DataKind.SpecPtr;
tpl = f_map_t.AppWithResult(tp);
if (tpl != null) return DataKind.Map;
+
return DataKind.Flat;
}
@@ -203,11 +402,16 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
}
if (theMap == null) return elt;
return theMap;
- }
+ }
+ return elt;
+ } else if (kind == DataKind.Ptrset) {
+ var tmp = f_int_to_ptrset.TryEval(elt);
+ if (tmp != null)
+ return tmp;
return elt;
}
- if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr) {
+ if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr || kind == DataKind.Object) {
if (elt.Kind == Model.ElementKind.Integer) {
var tmp = f_int_to_ptr.TryEval(elt);
if (tmp != null)
@@ -215,6 +419,9 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
}
}
+ if (kind == DataKind.Object)
+ return elt;
+
if (kind == DataKind.PhysPtr)
return Util.OrElse(f_phys_ptr_cast.TryEval(elt, tpl.Args[0]), elt);
@@ -225,13 +432,36 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
return elt;
}
+ void AddSpecialField(StateNode state, Model.Element elt, List<ElementNode> res, string name, Model.Func select_map)
+ {
+ var map = state.state.TryGet("$s");
+ if (map != null)
+ map = select_map.TryEval(map);
+ if (map != null) {
+ var model = elt.Model;
+ Model.Element val = f_select_bool.TryEval(map, elt);
+ Model.Element tp = tp_bool;
+ if (val == null) {
+ val = f_select_ptr.TryEval(map, elt);
+ tp = tp_object;
+ }
+ if (val == null) {
+ val = f_select_int.TryEval(map, elt);
+ tp = tp_mathint;
+ }
+ if (val != null) {
+ res.Add(new FieldNode(state, new EdgeName(name), val, tp));
+ }
+ }
+ }
+
public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt, Model.Element tp)
{
List<ElementNode> result = new List<ElementNode>();
Model.FuncTuple tpl;
var kind = GetKind(tp, out tpl);
- if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr) {
+ if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr || kind == DataKind.Object) {
var heap = state.state.TryGet("$s");
if (heap != null)
heap = f_heap.TryEval(heap);
@@ -246,6 +476,12 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
result.Add(new FieldNode(state, edgname, val, ftp));
}
}
+
+ AddSpecialField(state, elt, result, "\\closed", f_closed);
+ AddSpecialField(state, elt, result, "\\owner", f_owners);
+ AddSpecialField(state, elt, result, "\\root", f_roots);
+ AddSpecialField(state, elt, result, "\\timestamp", f_timestamps);
+
//result.Sort(CompareFields);
}
} else if (kind == DataKind.Map) {
@@ -258,6 +494,38 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
result.Add(new MapletNode(state, edgname, val, elTp));
}
}
+ } else if (kind == DataKind.Ptrset) {
+ foreach (var sel in f_select_bool.AppsWithArg(0, elt)) {
+ var edgname = new EdgeName(this, "[%0]", sel.Args[1]);
+ result.Add(new MapletNode(state, edgname, sel.Result, tp_bool));
+ }
+ }
+
+ if (!(elt is Model.Boolean)) {
+ var curState = state.state.TryGet("$s");
+ foreach (var tupl in elt.References) {
+ if (!tupl.Args.Contains(elt)) continue; // not looking for aliases (maybe we should?)
+ if (tupl.Args.Any(IsState) && !tupl.Args.Contains(curState))
+ continue;
+ var argsFmt = new StringBuilder();
+ var name = tupl.Func.Name;
+ argsFmt.Append(name).Append("(");
+ var args = new List<Model.Element>();
+ foreach (var a in tupl.Args) {
+ if (a == curState)
+ argsFmt.Append("\\now, ");
+ else if (a == elt)
+ argsFmt.Append("*, ");
+ else {
+ argsFmt.AppendFormat("%{0}, ", args.Count);
+ args.Add(a);
+ }
+ }
+ argsFmt.Length -= 2;
+ argsFmt.Append(")");
+ var edgeName = new EdgeName(this, argsFmt.ToString(), args.ToArray());
+ result.Add(new MapletNode(state, edgeName, tupl.Result, GuessType(tupl.Result)) { ViewLevel = FunctionScore(tupl.Func.Name) });
+ }
}
return result;
@@ -274,6 +542,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
protected override string CanonicalBaseName(Model.Element elt)
{
var vm = this;
+
var name = base.CanonicalBaseName(elt);
if (name.Contains("[") || name.Contains("'") || name.Contains("-"))
@@ -288,6 +557,15 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
return "map";
if (fn.Name.StartsWith("$int_to_map_t") && tpl.Result == elt)
return "map";
+
+ if (fn.Arity >= 1 && tpl.Args[0] == elt) {
+ if (fn == f_select_bool)
+ return "ptrset";
+ }
+
+ if (tpl.Result == elt)
+ if (fn == f_int_to_version)
+ return "version";
}
var fld = vm.f_field.TryEval(elt);
@@ -298,8 +576,10 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
}
}
- // return elt.ToString(); // for debugging
- return "";
+ if (viewOpts.DebugMode)
+ return elt.ToString();
+ else
+ return "";
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 19:36:26 +0000