Dafny: a partial first crack at a Dafny model-viewer provider, including captureState mark-ups in the Boogie code generated from Dafny

8 files changed, 414 insertions, 21 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 476a6bd9..5675d2a1 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -4,6 +4,9 @@
 // Edited sequence axioms 20 October 2009 by Alex Summers.

 // Copyright (c) 2008-2010, Microsoft.

 

+const $$Language$Dafny: bool;  // To be recognizable to the ModelViewer as

+axiom $$Language$Dafny;        // coming from a Dafny program.

+

 // ---------------------------------------------------------------

 // -- References -------------------------------------------------

 // ---------------------------------------------------------------

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 55769d0f..44e05a41 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -948,6 +948,19 @@ namespace Microsoft.Dafny {
       // set up the information used to verify the method's modifies clause

       DefineFrame(m.tok, m.Mod, builder, localVariables);

     }

+

+    Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {

+      Contract.Requires(tok != null);

+      Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);

+      string description = string.Format("{0}({1},{2}){3}{4}", tok.filename, tok.line, tok.col, additionalInfo == null ? "" : ": ", additionalInfo ?? "");

+      QKeyValue kv = new QKeyValue(tok, "captureState", new List<object>() { description }, null);

+      return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv);

+    }

+    Bpl.Cmd CaptureState(IToken tok) {

+      Contract.Requires(tok != null);

+      Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);

+      return CaptureState(tok, null);

+    }

     

     void CEVPrelude(Method m, Bpl.VariableSeq inParams, Bpl.VariableSeq outParams, Bpl.StmtListBuilder builder) 

     {

@@ -959,7 +972,7 @@ namespace Microsoft.Dafny {
     

       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Add(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Literal(1))));

       foreach (Bpl.Variable p in inParams) {

-        Contract.Assert( p != null);

+        Contract.Assert(p != null);

         builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",

           new Bpl.ExprSeq(

             CevLocation(p.tok),

@@ -2576,6 +2589,7 @@ void ObjectInvariant()
             new Bpl.IdentifierExprSeq()));

         }

         builder.Add(new Bpl.CallCmd(stmt.Tok, "CevStep", new Bpl.ExprSeq(CevLocation(stmt.Tok)), new Bpl.IdentifierExprSeq()));

+        builder.Add(CaptureState(stmt.Tok));

         

       } else if (stmt is BlockStmt) {

         foreach (Statement ss in ((BlockStmt)stmt).Body) {

@@ -2800,6 +2814,7 @@ void ObjectInvariant()
         loopBodyBuilder.Add(new Bpl.CallCmd(stmt.Tok, "CevStepEvent",

           new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_entered", predef.CevEventType)),

           new Bpl.IdentifierExprSeq()));

+        loopBodyBuilder.Add(CaptureState(stmt.Tok, "loop entered"));

         // termination checking

         if (Contract.Exists(theDecreases,e=> e is WildcardExpr)) {

           // omit termination checking for this loop

@@ -2826,6 +2841,7 @@ void ObjectInvariant()
         builder.Add(new Bpl.CallCmd(stmt.Tok, "CevStepEvent",

           new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_exited", predef.CevEventType)),

           new Bpl.IdentifierExprSeq()));

+        builder.Add(CaptureState(stmt.Tok, "loop exit"));

 

       } else if (stmt is ForeachStmt) {

         AddComment(builder, stmt, "foreach statement");

@@ -2952,6 +2968,7 @@ void ObjectInvariant()
         builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHeap",

           new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, predef.HeapVarName), etran.HeapExpr),

           new Bpl.IdentifierExprSeq()));

+        builder.Add(CaptureState(stmt.Tok));

         

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

@@ -3460,6 +3477,7 @@ void ObjectInvariant()
         // assume $IsGoodHeap($Heap);

         builder.Add(AssumeGoodHeap(tok, etran));

       }

+      builder.Add(CaptureState(tok));

     }

     

     Bpl.AssumeCmd AssumeGoodHeap(IToken tok, ExpressionTranslator etran) {

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 48c85d27..bd87186b 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -717,8 +717,11 @@ void ObjectInvariant()
                       }

                     }

                   }

-                  errorCount++;

+                  if (CommandLineOptions.Clo.ModelViewFile != null) {

+                    error.PrintModel();

                   }

+                  errorCount++;

+                }

               }

               Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

               break;

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 3e5ff0c3..3d1df65e 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -123,6 +123,13 @@ namespace Microsoft.Boogie
         }

       }

 

+      public IEnumerable<FuncTuple> AppsWithArgs(int argIdx0, Element elt0, int argIdx1, Element elt1) {

+        foreach (var r in elt0.References) {

+          if (r.Func == this && r.Args[argIdx0] == elt0 && r.Args[argIdx1] == elt1)

+            yield return r;

+        }

+      }

+

       public IEnumerable<FuncTuple> AppsWithResult(Element elt)

       {

         foreach (var r in elt.References) {

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
new file mode 100644
index 00000000..8ac0d033
--- /dev/null
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -0,0 +1,358 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+namespace Microsoft.Boogie.ModelViewer.Dafny

+{

+  public class Provider : ILanguageProvider

+  {

+    public static Provider Instance = new Provider();

+    private Provider() { }

+

+    public bool IsMyModel(Model m)

+    {

+      return m.TryGetFunc("$$Language$Dafny") != null;

+    }

+

+    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);

+        dm.states.Add(sn);

+      }

+      foreach (var s in dm.states) s.ComputeNames();

+      Namer.ComputeCanonicalNames(dm.states.Select(s => s.namer));

+      Namer.ComputeCanonicalNames(dm.states.Select(s => s.namer));

+      // Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));

+      return dm.states;

+    }

+  }

+

+  //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;

+    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);

+    }

+

+    public string GetUserVariableName(string name)

+    {

+      if (name == "$Heap" || name == "$_Frame" || name == "#cev_pc")

+        return null;

+      var hash = name.IndexOf('#');

+      if (0 < hash)

+        return name.Substring(0, hash);

+      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);

+      if (r != null)

+        return r.Args[0];

+      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)

+    {

+      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);

+            }

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

+    }

+  }

+  

+  class StateNode : IState

+  {

+    internal readonly Model.CapturedState state;

+    readonly string name;

+    internal readonly DafnyModel dm;

+    internal readonly List<VariableNode> vars = new List<VariableNode>();

+    internal readonly Namer namer = new Namer();

+    internal readonly int index;

+    

+    public StateNode(int i, DafnyModel parent, Model.CapturedState s)

+    {

+      dm = parent;

+      state = s;

+      index = i;

+

+      name = s.Name;

+      var idx = name.LastIndexOfAny(new char[] { '\\', '/' });

+      if (0 <= idx)

+        name = name.Substring(idx + 1);

+      var limit = 16;

+      if (name.Length > limit) {

+        idx = name.IndexOf('(');

+        if (idx > 0) {

+          var prefLen = limit - (name.Length - idx);

+          if (prefLen > 2) {

+            name = name.Substring(0,prefLen) + ".." + name.Substring(idx);

+          }

+        }

+      }

+

+      SetupVars();

+    }

+

+    void SetupVars()

+    {

+      var names = Util.Empty<string>();

+

+      if (dm.states.Count > 0) {

+        var prev = dm.states.Last();

+        names = prev.vars.Map(v => v.realName);

+      }

+

+      names = names.Concat(state.Variables).Distinct();

+

+      var curVars = state.Variables.ToDictionary(x => x);

+      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);

+          vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v);

+          vars.Add(vn);

+        }

+      }

+

+      foreach (var e in dm.model.Elements) {        

+        if (e is Model.Number || e is Model.Boolean)

+          namer.AddName(e, new EdgeName(e.ToString()));

+      }

+    } 

+

+    internal void ComputeNames()

+    {

+      namer.ComputeNames(vars);

+    }

+

+    public string Name

+    {

+      get { return name; }

+    }

+

+    public IEnumerable<IDisplayNode> Nodes

+    {

+      get {

+        return vars; 

+      }

+    }

+

+  }

+

+  class ElementNode : DisplayNode

+  {

+    protected StateNode stateNode;

+    protected Model.Element elt, tp;

+    protected DafnyModel vm { get { return stateNode.dm; } }

+    protected List<ElementNode> children;

+

+    public ElementNode(StateNode st, IEdgeName name, Model.Element elt, Model.Element tp)

+      : 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 override Model.Element Element

+    {

+      get

+      {

+        return elt;

+      }

+    }

+

+    protected virtual void DoInitChildren()

+    {

+      children.AddRange(vm.GetExpansion(stateNode, elt, tp));

+    }

+

+    protected void InitChildren()

+    {

+      if (children == null) {

+        children = new List<ElementNode>();

+        DoInitChildren();

+      }

+    }

+

+    public override string CanonicalValue

+    {

+      get

+      {

+        return stateNode.namer.CanonicalName(Element);

+      }

+    }

+

+    public override IEnumerable<string> Aliases

+    {

+      get

+      {

+        if (Element is Model.Boolean) {

+          yield break;

+        } else {

+          foreach (var edge in stateNode.namer.Aliases(Element))

+            if (!edge.Equals(Name))

+              yield return edge.FullName();

+        }

+      }

+    }

+

+    public override string ToolTip

+    {

+      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); 

+          if (limit-- < 0) {

+            sb.Append("...");

+            break;

+          }

+        }

+        return sb.ToString();

+      }

+    }

+

+    public override bool Expandable

+    {

+      get

+      {

+        InitChildren();

+        return children.Count > 0;

+      }

+    }

+

+    public override IEnumerable<IDisplayNode> Expand()

+    {

+      InitChildren();

+      return children;

+    }

+  }

+

+  class FieldNode : ElementNode

+  {

+    public FieldNode(StateNode par, IEdgeName realName, Model.Element elt, Model.Element tp)

+      : base(par, realName, elt, tp)

+    {

+      /*

+      var idx = realName.LastIndexOf('.');

+      if (idx > 0)

+        name = realName.Substring(idx + 1);

+       */

+    }

+  }

+

+  class MapletNode : ElementNode

+  {

+    public MapletNode(StateNode par, IEdgeName realName, Model.Element elt, Model.Element tp)

+      : base(par, realName, elt, tp)

+    {

+    }

+  }

+

+  class VariableNode : ElementNode

+  {

+    public bool updatedHere;

+    public string realName;

+

+    public VariableNode(StateNode par, string realName, Model.Element elt, Model.Element tp)

+      : base(par, realName, elt, tp)

+    {

+      this.realName = realName;

+      name = new EdgeName(vm.GetUserVariableName(realName));

+    }

+

+    public override NodeState State

+    {

+      get

+      {

+        return base.State | (updatedHere ? NodeState.Changed : NodeState.Normal);

+      }

+    }

+  }

+}

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 609bf571..dbb91390 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -24,6 +24,7 @@ namespace Microsoft.Boogie.ModelViewer
     IEnumerable<ILanguageProvider> Providers()

     {

       yield return Vcc.Provider.Instance;

+      yield return Dafny.Provider.Instance;

       yield return Base.Provider.Instance;

     }

 

diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index 413abd67..3027900a 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -68,6 +68,7 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="BaseProvider.cs" />

+    <Compile Include="DafnyProvider.cs" />

     <Compile Include="DataModel.cs" />

     <Compile Include="Main.cs">

       <SubType>Form</SubType>

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 927868b5..031f0f18 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -210,10 +210,7 @@ namespace Microsoft.Boogie {
       Contract.Assert(mvstates.Arity == 1);

 

       foreach (Variable v in MvInfo.AllVariables) {

-        var fn = m.TryGetFunc(v.Name);

-        if (fn != null && fn.Arity == 0) {

-          m.InitialState.AddBinding(v.Name, fn.GetConstant());

-        }

+        m.InitialState.AddBinding(v.Name, GetModelValue(m, v));

       }

 

       var states = new List<int>();

@@ -239,21 +236,7 @@ namespace Microsoft.Boogie {
 

             if (e is IdentifierExpr) {

               IdentifierExpr ide = (IdentifierExpr)e;

-

-              // first, get the unique name

-              string uniqueName;

-              VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(ide.Decl);

-              if (vvar == null) {

-                uniqueName = ide.Decl.Name;

-              } else {

-                uniqueName = Context.Lookup(vvar);

-              }

-

-              var f = m.TryGetFunc(uniqueName);

-              if (f == null) {

-                f = m.MkFunc(uniqueName, 0);

-              }              

-              elt = f.GetConstant();

+              elt = GetModelValue(m, ide.Decl);

             } else if (e is LiteralExpr) {

               LiteralExpr lit = (LiteralExpr)e;

               elt = m.MkElement(lit.Val.ToString());

@@ -272,6 +255,25 @@ namespace Microsoft.Boogie {
       return m;

     }

 

+    private Model.Element GetModelValue(Model m, Variable v) {

+      Model.Element elt;

+      // first, get the unique name

+      string uniqueName;

+      VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(v);

+      if (vvar == null) {

+        uniqueName = v.Name;

+      } else {

+        uniqueName = Context.Lookup(vvar);

+      }

+

+      var f = m.TryGetFunc(uniqueName);

+      if (f == null) {

+        f = m.MkFunc(uniqueName, 0);

+      }

+      elt = f.GetConstant();

+      return elt;

+    }

+

     public abstract int GetLocation();

   }