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

5 files changed, 125 insertions, 94 deletions

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<IState> 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<Model.Element, string> typeName = new Dictionary<Model.Element, string>();

     public List<StateNode> states = new List<StateNode>();

 

     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<ElementNode> GetExpansion(StateNode state, Model.Element elt, Model.Element tp)

+    public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt)

     {

       List<ElementNode> result = new List<ElementNode>();

 

-      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<ElementNode> 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;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index ef2501de..840599f5 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -8,6 +8,7 @@ using System.Collections;
 using System.Collections.Generic;

 using System.Threading;

 using System.IO;

+using System.Text.RegularExpressions;

 using System.Diagnostics;

 using System.Diagnostics.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

@@ -358,8 +359,8 @@ namespace Microsoft.Boogie {
     public Model ToModel()

     {

       Model m = new Model();

+      // create an Element for every partition

       Model.Element[] elts = new Model.Element[partitionToValue.Count];

-

       for (int i = 0; i < partitionToValue.Count; ++i) {

         var v = partitionToValue[i];

         if (v == null)

@@ -372,13 +373,39 @@ namespace Microsoft.Boogie {
           f.SetConstant(elts[i]);

         }

       }

+      // compute and apply redirections

+      foreach (var pr in Redirections(definedFunctions)) {

+        elts[pr.Key] = elts[pr.Value];

+      }

 

+      // create functions

+      var selectFunctions = new Dictionary<int, Model.Func>();

+      var storeFunctions = new Dictionary<int, Model.Func>();

       foreach (var t in definedFunctions) {

         var tuples = t.Value;

         if (tuples.Count == 0) continue;

 

-        var f = m.MkFunc(t.Key, tuples[0].Count - 1);

-        var args = new Model.Element[f.Arity];

+        // get the Func ("it doesn't matter if you get the funk, just as long as the funk gets you", from Ulco Bed's "Get The Funk" on Candy Dulfer's 1990 album Saxuality)

+        var name = t.Key;

+        var arity = tuples[0].Count - 1;

+        Model.Func f;

+        if (Regex.IsMatch(name, "^MapType[0-9]*Select$")) {

+          name = string.Format("[{0}]", arity);

+          if (!selectFunctions.TryGetValue(arity, out f)) {

+            f = m.MkFunc(name, arity);

+            selectFunctions.Add(arity, f);

+          }

+        } else if (Regex.IsMatch(name, "^MapType[0-9]*Store$")) {

+          name = string.Format("[{0}:=]", arity);

+          if (!storeFunctions.TryGetValue(arity, out f)) {

+            f = m.MkFunc(name, arity);

+            storeFunctions.Add(arity, f);

+          }

+        } else {

+          f = m.MkFunc(name, arity);

+        }

+

+        var args = new Model.Element[arity];

         foreach (var l in tuples) {

           if (l.Count == 1) continue;

           for (int i = 0; i < f.Arity; ++i)

@@ -390,6 +417,22 @@ namespace Microsoft.Boogie {
       return m;

     }

 

+    IEnumerable<KeyValuePair<int,int>> Redirections(Dictionary<string, List<List<int>>> functions) {

+      List<List<int>> fn;

+      if (functions.TryGetValue("U_2_bool", out fn)) {

+        foreach (var tpl in fn) {

+          if (tpl.Count == 2)  // the last tuple (the default value) has length 1

+            yield return new KeyValuePair<int,int>(tpl[0], tpl[1]);

+        }

+      }

+      if (functions.TryGetValue("U_2_int", out fn)) {

+        foreach (var tpl in fn) {

+          if (tpl.Count == 2)  // the last tuple (the default value) has length 1

+            yield return new KeyValuePair<int,int>(tpl[0], tpl[1]);

+        }

+      }

+    }

+

     public virtual void Print(TextWriter writer) {

       Contract.Requires(writer != null);

     }

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 8f2fbaf3..4d0b3bad 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -234,7 +234,7 @@ type -> {
   *8 -> *18

   *9 -> *6

   *10 -> *7

-  *20 -> *4

+  -2 -> *4

 }

 MapType0Type -> {

   *6 *7 *4 -> *18

@@ -254,14 +254,14 @@ MapType0TypeInv0 -> {
   2 -> true

   5 -> true

 }

-MapType0Select -> {

-  *8 *9 *10 -> *20

+[3] -> {

+  *8 *9 *10 -> -2

 }

 U_2_int -> {

-  *20 -> -2

+  -2 -> -2

 }

 int_2_U -> {

-  -2 -> *20

+  -2 -> -2

 }

 *** STATE <initial>

   Heap -> *8