summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2010-10-15 00:23:14 +0000
committerGravatar MichalMoskal <unknown>2010-10-15 00:23:14 +0000
commit2bd631d07570bf81611486d01bcd5a21dee2d2c9 (patch)
tree7ed182d56576ecfea56f9e384058855d626aef7b
parent9e1f99c02907899e6b37427567d62719e38dde5c (diff)
Make it display maps
-rw-r--r--Source/ModelViewer/DataModel.cs13
-rw-r--r--Source/ModelViewer/Main.cs10
-rw-r--r--Source/ModelViewer/VccProvider.cs171
3 files changed, 154 insertions, 40 deletions
diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index ff5206c7..0c470bcf 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -37,6 +37,7 @@ namespace Microsoft.Boogie.ModelViewer
string Name { get; }
NodeState State { get; }
IEnumerable<string> Values { get; }
+ string ToolTip { get; }
object ViewSync { get; set; }
}
@@ -86,6 +87,11 @@ namespace Microsoft.Boogie.ModelViewer
get { yield break; }
}
+ public virtual string ToolTip
+ {
+ get { return null; }
+ }
+
public virtual bool Expandable
{
get { return false; }
@@ -152,6 +158,13 @@ namespace Microsoft.Boogie.ModelViewer
{
foreach (var s in inp) fn(s);
}
+
+ public static T OrElse<T>(T a, T b)
+ where T : class
+ {
+ if (a != null) return a;
+ return b;
+ }
}
}
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 3b5efd0d..7e45a558 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -261,8 +261,16 @@ namespace Microsoft.Boogie.ModelViewer
}
}
+ var tooltip = dispNode.ToolTip;
+ var values = ValuesAsString(dispNode);
+ if (tooltip != null) {
+ this.ToolTipText = tooltip;
+ } else {
+ this.ToolTipText = values;
+ }
+
this.SubItems[0].Text = dispNode.Name;
- this.SubItems[1].Text = ValuesAsString(dispNode).ToString();
+ this.SubItems[1].Text = values;
}
internal DisplayItem()
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index dd39b1b2..ea0544bf 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -27,11 +27,19 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
}
}
+ enum DataKind
+ {
+ Flat,
+ PhysPtr,
+ SpecPtr,
+ Map
+ }
+
class VccModel
{
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_type, f_int_to_ptr, f_ptr_to_int, f_ptr;
+ f_select_value, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t;
Dictionary<Model.Element, string> primaryName = new Dictionary<Model.Element, string>();
Dictionary<Model.Element, string[]> allNames = new Dictionary<Model.Element, string[]>();
public List<StateNode> states = new List<StateNode>();
@@ -52,6 +60,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
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);
}
public void ComputeNames()
@@ -98,9 +107,26 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
deref = Image(elt, f_spec_ptr_to);
if (deref != null)
return TypeName(deref) + "^";
+ var mapt = f_map_t.AppWithResult(elt);
+ if (mapt != null)
+ return string.Format("{1}[{0}]", TypeName(mapt.Args[0]), TypeName(mapt.Args[1]));
+
foreach (var app in elt.Names)
- if (app.Func.Arity == 0 && app.Func.Name.StartsWith("^"))
- return app.Func.Name.Substring(1);
+ if (app.Func.Arity == 0 && app.Func.Name.StartsWith("^")) {
+ var n = app.Func.Name.Substring(1);
+ switch (n) {
+ case "^i1": return "int8_t";
+ case "^u1": return "uint8_t";
+ case "^i2": return "int16_t";
+ case "^u2": return "uint16_t";
+ case "^i4": return "int32_t";
+ case "^u4": return "uint32_t";
+ case "^i8": return "int64_t";
+ case "^u8": return "uint64_t";
+ case "^bool": return "bool";
+ default: return n;
+ }
+ }
return elt.ToString();
}
@@ -132,47 +158,100 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
return s2 - s1;
}
- public Model.Element WrapForUse(Model.Element elt, Model.Element tp)
+ public DataKind GetKind(Model.Element tp, out Model.FuncTuple tpl)
{
- var derefPh = Image(tp, f_ptr_to);
- var derefSp = Image(tp, f_spec_ptr_to);
+ 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;
+ }
- if (derefPh == null && derefSp == null)
- return elt;
+ public DataKind GetKind(Model.Element tp)
+ {
+ Model.FuncTuple dummy;
+ return GetKind(tp, out dummy);
+ }
- Model.Element casted = null;
- if (elt.Kind == Model.ElementKind.Integer) {
- var tmp = f_int_to_ptr.TryEval(elt);
- if (tmp != null)
- elt = tmp;
+ public Model.Element WrapForUse(Model.Element elt, Model.Element tp)
+ {
+ Model.FuncTuple tpl;
+ var kind = GetKind(tp, out tpl);
+
+ if (kind == DataKind.Flat) return elt;
+
+ if (kind == DataKind.Map) {
+ if (elt.Kind == Model.ElementKind.Integer) {
+ Model.Element theMap = null;
+ foreach (var conv in model.Functions)
+ // really, we should reconstruct the name of this function, but this is painful
+ if (conv.Arity == 1 && conv.Name.StartsWith("$int_to_map_t")) {
+ var app = conv.AppWithArg(0, elt);
+ if (app != null) {
+ theMap = app.Result;
+ break;
+ }
+ }
+ if (theMap == null) return elt;
+ return theMap;
+ }
+ return elt;
}
- if (derefPh != null) {
- casted = f_phys_ptr_cast.TryEval(elt, derefPh);
- } else if (derefSp != null) {
- casted = f_spec_ptr_cast.TryEval(elt, derefSp);
+ if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr) {
+ if (elt.Kind == Model.ElementKind.Integer) {
+ var tmp = f_int_to_ptr.TryEval(elt);
+ if (tmp != null)
+ elt = tmp;
+ }
}
- if (casted != null) return casted;
+ if (kind == DataKind.PhysPtr)
+ return Util.OrElse(f_phys_ptr_cast.TryEval(elt, tpl.Args[0]), elt);
+
+ if (kind == DataKind.SpecPtr)
+ return Util.OrElse(f_spec_ptr_cast.TryEval(elt, tpl.Args[0]), elt);
+
+ Util.Assert(false);
return elt;
}
- public IEnumerable<FieldNode> GetFields(StateNode state, Model.Element elt, Model.Element tp)
+ public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt, Model.Element tp)
{
- var heap = state.state.TryGet("$s");
- if (heap != null)
- heap = f_heap.TryEval(heap);
- if (heap != null) {
- foreach (var fld in f_select_field.AppsWithArg(0, heap)) {
- var val = f_select_value.TryEval(fld.Result, elt);
- if (val != null) {
- var ftp = f_field_type.TryEval(fld.Args[1]);
- val = WrapForUse(val, ftp);
- yield return new FieldNode(state, FieldName(fld.Args[1]), val, ftp);
+ List<ElementNode> result = new List<ElementNode>();
+ Model.FuncTuple tpl;
+
+ var kind = GetKind(tp, out tpl);
+ if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr) {
+ var heap = state.state.TryGet("$s");
+ if (heap != null)
+ heap = f_heap.TryEval(heap);
+ if (heap != null) {
+ foreach (var fld in f_select_field.AppsWithArg(0, heap)) {
+ var val = f_select_value.TryEval(fld.Result, elt);
+ if (val != null) {
+ var ftp = f_field_type.TryEval(fld.Args[1]);
+ val = WrapForUse(val, ftp);
+ result.Add(new FieldNode(state, FieldName(fld.Args[1]), val, ftp));
+ }
}
+ result.Sort(CompareFields);
}
+ } else if (kind == DataKind.Map) {
+ var elTp = tpl.Args[1];
+ foreach (var sel in model.Functions)
+ if (sel.Arity == 2 && sel.Name.StartsWith("$select.$map_t")) {
+ foreach (var app in sel.AppsWithArg(0, elt)) {
+ var val = WrapForUse(app.Result, elTp);
+ result.Add(new MapletNode(state, "[" + ElementNames(app.Args[1])[0] + "]", val, elTp));
+ }
+ }
}
+
+ return result;
}
public string[] ElementNames(Model.Element elt)
@@ -467,6 +546,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
protected virtual void DoInitChildren()
{
+ children.AddRange(vm.GetExpansion(stateNode, elt, tp));
}
protected void InitChildren()
@@ -493,6 +573,24 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
}
}
+ public override string ToolTip
+ {
+ get
+ {
+ var sb = new StringBuilder();
+ sb.AppendFormat("Type: {0}\n", vm.TypeName(tp));
+ int limit = 30;
+ foreach (var n in Values){
+ sb.AppendFormat(" = {0}\n", n);
+ if (limit-- < 0) {
+ sb.Append("...");
+ break;
+ }
+ }
+ return sb.ToString();
+ }
+ }
+
public override bool Expandable
{
get
@@ -520,15 +618,16 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
name = realName.Substring(idx + 1);
*/
}
+ }
- protected override void DoInitChildren()
+ class MapletNode : ElementNode
+ {
+ public MapletNode(StateNode par, string realName, Model.Element elt, Model.Element tp)
+ : base(par, realName, elt, tp)
{
- children.AddRange(vm.GetFields(stateNode, elt, tp));
- children.Sort(vm.CompareFields);
}
}
-
class VariableNode : ElementNode
{
public bool updatedHere;
@@ -539,12 +638,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
name = vm.GetUserVariableName(realName);
}
- protected override void DoInitChildren()
- {
- children.AddRange(vm.GetFields(stateNode, elt, tp));
- children.Sort(vm.CompareFields);
- }
-
public override NodeState State
{
get