From c9dfa023ddcc6ea1ff3b8f7598f87bd200ab6c9e Mon Sep 17 00:00:00 2001 From: rustanleino Date: Tue, 2 Nov 2010 23:40:03 +0000 Subject: ModelViewer: * map back values introduced by bool_2_U and int_2_U * map back internal names for select/store to [n] and [n:=], where n is the arity of the map * added /break switch to ModelViewer * display more things (including sequences) in Dafny provider --- Source/ModelViewer/DafnyProvider.cs | 139 +++++++++++++++--------------------- Source/ModelViewer/Main.cs | 19 ++++- Source/ModelViewer/Namer.cs | 2 +- 3 files changed, 74 insertions(+), 86 deletions(-) (limited to 'Source/ModelViewer') diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs index 8ac0d033..33ae8a0b 100644 --- a/Source/ModelViewer/DafnyProvider.cs +++ b/Source/ModelViewer/DafnyProvider.cs @@ -17,7 +17,6 @@ namespace Microsoft.Boogie.ModelViewer.Dafny public IEnumerable GetStates(Model m) { - System.Diagnostics.Debugger.Launch(); // KRML DEBUG var dm = new DafnyModel(m); foreach (var s in m.States) { var sn = new StateNode(dm.states.Count, dm, s); @@ -31,32 +30,21 @@ namespace Microsoft.Boogie.ModelViewer.Dafny } } - //KRML: todo: make this Dafny specific - enum DataKind - { - Flat, - PhysPtr, - SpecPtr, - Map - } - class DafnyModel { public readonly Model model; - public readonly Model.Func f_heap_select, f_class_int, f_class_bool, f_class_set, f_class_seq, f_dtype; + public readonly Model.Func f_heap_select, f_set_select, f_seq_length, f_seq_index, f_box; Dictionary typeName = new Dictionary(); public List states = new List(); public DafnyModel(Model m) { model = m; - f_heap_select = m.MkFunc("MapType1Select", 3); // todo: this is a hardcoded hack, we need a disciplined way of getting the name of this built-in select function - - f_class_int = m.MkFunc("class.int", 0); - f_class_bool = m.MkFunc("class.bool", 0); - f_class_set = m.MkFunc("class.set", 0); - f_class_seq = m.MkFunc("class.seq", 0); - f_dtype = m.MkFunc("dtype", 1); + f_heap_select = m.MkFunc("[3]", 3); + f_set_select = m.MkFunc("[2]", 2); + f_seq_length = m.MkFunc("Seq#Length", 1); + f_seq_index = m.MkFunc("Seq#Index", 2); + f_box = m.MkFunc("$Box", 1); } public string GetUserVariableName(string name) @@ -69,19 +57,6 @@ namespace Microsoft.Boogie.ModelViewer.Dafny return name; } - public Model.Element LocalType(Model.Element e) - { - if (e is Model.Integer) - return f_class_int.GetConstant(); - if (e is Model.Boolean) - return f_class_bool.GetConstant(); - var className = f_dtype.AppWithArg(0, e); - if (className != null) - return className.Result; - // don't know - return f_class_int.GetConstant(); - } - public Model.Element Image(Model.Element elt, Model.Func f) { var r = f.AppWithResult(elt); @@ -90,52 +65,54 @@ namespace Microsoft.Boogie.ModelViewer.Dafny return null; } - public string TypeName(Model.Element elt) - { - string res; - if (!typeName.TryGetValue(elt, out res)) { - if (elt == f_class_bool.GetConstant()) { - res = "bool"; - } else if (elt == f_class_int.GetConstant()) { - res = "int"; - } else if (elt == f_class_set.GetConstant()) { - res = "set"; // todo: instantiation? - } else if (elt == f_class_seq.GetConstant()) { - res = "seq"; // todo: instantiation? - } else { - res = "object"; // todo: specific class type; also todo: datatypes - } - typeName[elt] = res; - } - return res; - } - - public IEnumerable GetExpansion(StateNode state, Model.Element elt, Model.Element tp) + public IEnumerable GetExpansion(StateNode state, Model.Element elt) { List result = new List(); - var heap = state.state.TryGet("$Heap"); - if (heap != null) { - foreach (var tpl in f_heap_select.AppsWithArgs(0, heap, 1, elt)) { - var field = tpl.Args[2]; - var fieldName = field.ToString(); - foreach (var n in field.Names) { - fieldName = n.Func.Name; - int dot = fieldName.LastIndexOf('.'); - if (0 <= dot) { - fieldName = fieldName.Substring(dot + 1); + if (elt.Kind == Model.ElementKind.Uninterpreted) { + var seqLen = f_seq_length.AppWithArg(0, elt); + if (seqLen != null) { + // elt is a sequence + var edgname = new EdgeName(state.namer, "|%0|", "|.|", 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); + result.Add(new FieldNode(state, edgname, Unbox(tpl.Result))); + } + } else { + + var heap = state.state.TryGet("$Heap"); + if (heap != null) { + foreach (var tpl in f_heap_select.AppsWithArgs(0, heap, 1, elt)) { + var field = tpl.Args[2]; + var fieldName = field.ToString(); + foreach (var n in field.Names) { + fieldName = n.Func.Name; + int dot = fieldName.LastIndexOf('.'); + if (0 <= dot) { + fieldName = fieldName.Substring(dot + 1); + } + break; + } + var val = tpl.Result; + var edgname = new EdgeName(state.namer, "%0." + fieldName, fieldName, elt); + result.Add(new FieldNode(state, edgname, val)); } - break; } - var val = tpl.Result; - var ftp = LocalType(val); - var edgname = new EdgeName(state.namer, "%0." + fieldName, fieldName, elt); - result.Add(new FieldNode(state, edgname, val, ftp)); } } return result; } + + Model.Element Unbox(Model.Element elt) { + var unboxed = f_box.AppWithResult(elt); + if (unboxed != null) + return unboxed.Args[0]; + else + return elt; + } } class StateNode : IState @@ -186,9 +163,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny foreach (var v in names) { if (dm.GetUserVariableName(v) != null) { var val = state.TryGet(v); - var tp = dm.LocalType(val); - // val = dm.WrapForUse(val, tp); - var vn = new VariableNode(this, v, val, tp); + var vn = new VariableNode(this, v, val); vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v); vars.Add(vn); } @@ -222,20 +197,19 @@ namespace Microsoft.Boogie.ModelViewer.Dafny class ElementNode : DisplayNode { protected StateNode stateNode; - protected Model.Element elt, tp; + protected Model.Element elt; protected DafnyModel vm { get { return stateNode.dm; } } protected List children; - public ElementNode(StateNode st, IEdgeName name, Model.Element elt, Model.Element tp) + public ElementNode(StateNode st, IEdgeName name, Model.Element elt) : base(name) { 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 ElementNode(StateNode st, string name, Model.Element elt) + : this(st, new EdgeName(name), elt) { } public override Model.Element Element { @@ -247,7 +221,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny protected virtual void DoInitChildren() { - children.AddRange(vm.GetExpansion(stateNode, elt, tp)); + children.AddRange(vm.GetExpansion(stateNode, elt)); } protected void InitChildren() @@ -285,7 +259,6 @@ namespace Microsoft.Boogie.ModelViewer.Dafny get { 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); @@ -316,8 +289,8 @@ namespace Microsoft.Boogie.ModelViewer.Dafny class FieldNode : ElementNode { - public FieldNode(StateNode par, IEdgeName realName, Model.Element elt, Model.Element tp) - : base(par, realName, elt, tp) + public FieldNode(StateNode par, IEdgeName realName, Model.Element elt) + : base(par, realName, elt) { /* var idx = realName.LastIndexOf('.'); @@ -329,8 +302,8 @@ namespace Microsoft.Boogie.ModelViewer.Dafny class MapletNode : ElementNode { - public MapletNode(StateNode par, IEdgeName realName, Model.Element elt, Model.Element tp) - : base(par, realName, elt, tp) + public MapletNode(StateNode par, IEdgeName realName, Model.Element elt) + : base(par, realName, elt) { } } @@ -340,8 +313,8 @@ namespace Microsoft.Boogie.ModelViewer.Dafny public bool updatedHere; public string realName; - public VariableNode(StateNode par, string realName, Model.Element elt, Model.Element tp) - : base(par, realName, elt, tp) + 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 dbb91390..08869c17 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -32,11 +32,26 @@ namespace Microsoft.Boogie.ModelViewer { InitializeComponent(); - + var debugBreak = false; + string filename = null; var args = Environment.GetCommandLineArgs(); + for (int i = 1; i < args.Length; i++) { + var arg = args[i]; + if (arg == "/break") + debugBreak = true; + else + filename = arg; + } + if (debugBreak) { + System.Diagnostics.Debugger.Launch(); + } + if (filename == null) { + throw new Exception("error: usage: ModelViewer.exe MyProgram.model"); // (where does this exception go?) + } + Model m; - using (var rd = File.OpenText(args[1])) { + using (var rd = File.OpenText(filename)) { var models = Model.ParseModels(rd); m = models[0]; } diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs index 5d9f41d9..282a2530 100644 --- a/Source/ModelViewer/Namer.cs +++ b/Source/ModelViewer/Namer.cs @@ -124,7 +124,7 @@ namespace Microsoft.Boogie.ModelViewer if (n.elt is Model.Boolean || n.elt is Model.Number) canonicals[n.elt] = n.nodes[0].FullName(); else - canonicals[n.elt] = n.nodes[0].FullName() + "." + n.stateIdx; + canonicals[n.elt] = "'" + n.nodes[0].FullName() + "-" + n.stateIdx; } var unnamedIdx = 1; -- cgit v1.2.3