Dafny: better error reporting on resolution of refinements. Replace assertions with "if"s to handle errors gently and add cycle detection check.

5 files changed, 153 insertions, 64 deletions

diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc
index 58992dea..18160f39 100644
--- a/Dafny/Resolver.ssc
+++ b/Dafny/Resolver.ssc
@@ -38,10 +38,12 @@ namespace Microsoft.Dafny {
     readonly Dictionary<ClassDecl!,Dictionary<string!,MemberDecl!>!>! classMembers = new Dictionary<ClassDecl!,Dictionary<string!,MemberDecl!>!>();

     readonly Dictionary<DatatypeDecl!,Dictionary<string!,DatatypeCtor!>!>! datatypeCtors = new Dictionary<DatatypeDecl!,Dictionary<string!,DatatypeCtor!>!>();

     readonly Graph<ModuleDecl!>! importGraph = new Graph<ModuleDecl!>();

-

+    

+    bool checkRefinements = true; 

+      

     public void ResolveProgram(Program! prog) {

       // register modules

-      Dictionary<string,ModuleDecl!> modules = new Dictionary<string,ModuleDecl!>();

+      Dictionary<string,ModuleDecl!> modules = new Dictionary<string,ModuleDecl!>();      

       foreach (ModuleDecl m in prog.Modules) {

         if (modules.ContainsKey(m.Name)) {

           Error(m, "Duplicate module name: {0}", m.Name);

@@ -50,6 +52,7 @@ namespace Microsoft.Dafny {
         }

       }

       // resolve imports and register top-level declarations

+      Graph<TopLevelDecl!>! refines = new Graph<TopLevelDecl!>();

       foreach (ModuleDecl m in prog.Modules) {

         importGraph.AddVertex(m);

         foreach (string imp in m.Imports) {

@@ -64,6 +67,7 @@ namespace Microsoft.Dafny {
           }

         }

         RegisterTopLevelDecls(m.TopLevelDecls);

+        foreach (TopLevelDecl! decl in m.TopLevelDecls) refines.AddVertex(decl);

       }

       // check for cycles in the import graph

       List<ModuleDecl!> cycle = importGraph.TryFindCycle();

@@ -86,11 +90,27 @@ namespace Microsoft.Dafny {
         }

       }

 

-      // resolve top-level declarations of refinements

+      // resolve top-level declarations of refinements      

       foreach (ModuleDecl m in prog.Modules) 

         foreach (TopLevelDecl decl in m.TopLevelDecls) 

-          if (decl is ClassRefinementDecl) 

-            ResolveTopLevelRefinement((ClassRefinementDecl) decl);            

+          if (decl is ClassRefinementDecl) {

+            ClassRefinementDecl! rdecl = (ClassRefinementDecl) decl;

+            ResolveTopLevelRefinement(rdecl);          

+            if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);

+          }

+      

+      // attempt finding refinement cycles

+      List<TopLevelDecl!> refinesCycle = refines.TryFindCycle();      

+      if (refinesCycle != null) {

+        string cy = "";

+        string sep = "";

+        foreach (TopLevelDecl decl in refinesCycle) {

+          cy = decl + sep + cy;

+          sep = " -> ";

+        }

+        Error(refinesCycle[0], "Detected a cyclic refinement declaration: {0}", cy);

+        checkRefinements = false;

+      } 

       

       // resolve top-level declarations

       Graph<DatatypeDecl!> datatypeDependencies = new Graph<DatatypeDecl!>();

@@ -162,7 +182,6 @@ namespace Microsoft.Dafny {
     }

       

     public void ResolveTopLevelRefinement(ClassRefinementDecl! decl) {

-      // TODO: check for loops in refinement

       if (!classes.ContainsKey(decl.RefinedClass.val)) {

         Error(decl.RefinedClass, "Refined class declaration is missing: {0}", decl.RefinedClass.val);

       } else {

@@ -243,26 +262,28 @@ namespace Microsoft.Dafny {
           CouplingInvariant inv = (CouplingInvariant)member;

           if (currentClass is ClassRefinementDecl) {      

             ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;                          

-            assert refined != null;

-            assert classMembers.ContainsKey(refined);

-            Dictionary<string!,MemberDecl!> members = classMembers[refined];

+            if (refined != null) {

+              assert classMembers.ContainsKey(refined);

+              Dictionary<string!,MemberDecl!> members = classMembers[refined];

+            

+              // resolve abstracted fields in the refined class

+              List<Field!> fields = new List<Field!>();

+              foreach (IToken tok in inv.Toks) {

+                if (!members.ContainsKey(tok.val))

+                  Error(tok, "Refined class does not declare a field: {0}", tok.val);              

+                else {

+                  MemberDecl! field = members[tok.val];

+                  if (!(field is Field)) 

+                    Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);

+                  else if (fields.Contains((Field!)field))

+                    Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val); 

+                  else

+                    fields.Add((Field!)field);

+                }                  

+              }            

+              inv.Refined = fields;

+            }

             

-            // resolve abstracted fields in the refined class

-            List<Field!> fields = new List<Field!>();

-            foreach (IToken tok in inv.Toks) {

-              if (!members.ContainsKey(tok.val))

-                Error(tok, "Refined class does not declare a field: {0}", tok.val);              

-              else {

-                MemberDecl! field = members[tok.val];

-                if (!(field is Field)) 

-                  Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);

-                else if (fields.Contains((Field!)field))

-                  Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val); 

-                else

-                  fields.Add((Field!)field);

-              }                  

-            }            

-            inv.Refined = fields;

           } else {

             Error(member, "Coupling invariants can only be declared in refinement classes");

           }

@@ -272,12 +293,13 @@ namespace Microsoft.Dafny {
         

         if (currentClass is ClassRefinementDecl) {          

           ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;  

-          assert refined != null;

-          assert classMembers.ContainsKey(refined);                        

+          if (refined != null) {

+            assert classMembers.ContainsKey(refined);                        

           

-          // there is a member with the same name in refined class if and only if the member is a refined method

-          if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))

-            Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);

+            // there is a member with the same name in refined class if and only if the member is a refined method

+            if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))

+              Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);

+          }

         }

       }

       currentClass = null;

@@ -314,36 +336,41 @@ namespace Microsoft.Dafny {
           // check if signature of the refined method matches the refinement method

           if (member is MethodRefinement) {

             MethodRefinement mf = (MethodRefinement)member;

-            assert currentClass is ClassRefinementDecl;

-            assert ((ClassRefinementDecl)currentClass).Refined != null; // should have already been resolved

-            MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];

-            if (d is Method) {

-              mf.Refined = (Method)d;

-              if (mf.Ins.Count != mf.Refined.Ins.Count)

-                Error(mf, "Different number of input variables");

-              if (mf.Outs.Count != mf.Refined.Outs.Count)

-                Error(mf, "Different number of output variables");               

-              if (mf.IsStatic || mf.Refined.IsStatic) 

-                Error(mf, "Refined methods cannot be static");

+            if (currentClass is ClassRefinementDecl) {

+              // should have already been resolved

+              if (((ClassRefinementDecl)currentClass).Refined != null) { 

+                MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];

+                if (d is Method) {

+                  mf.Refined = (Method)d;

+                  if (mf.Ins.Count != mf.Refined.Ins.Count)

+                    Error(mf, "Different number of input variables");

+                  if (mf.Outs.Count != mf.Refined.Outs.Count)

+                    Error(mf, "Different number of output variables");               

+                  if (mf.IsStatic || mf.Refined.IsStatic) 

+                    Error(mf, "Refined methods cannot be static");

+                } else {

+                  Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);

+                }            

+              }

             } else {

-              Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);

-            }            

+              Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);          

+            }

           }

         

         } else if (member is CouplingInvariant) {        

           CouplingInvariant inv = (CouplingInvariant)member;

-          assert inv.Refined != null;

-          inv.Formals = new List<Formal!>();

-          scope.PushMarker();

-          for (int i = 0; i < inv.Refined.Count; i++) {

-            Field! field = inv.Refined[i];            

-            Formal! formal = new Formal(inv.Toks[i], field.Name, field.Type, true, field.IsGhost);

-            inv.Formals.Add(formal);

-            scope.Push(inv.Toks[i].val, formal);

-          }

-          ResolveExpression(inv.Expr, false, true);

-          scope.PopMarker();

-                

+          if (inv.Refined != null) {

+            inv.Formals = new List<Formal!>();

+            scope.PushMarker();

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

+              Field! field = inv.Refined[i];            

+              Formal! formal = new Formal(inv.Toks[i], field.Name, field.Type, true, field.IsGhost);

+              inv.Formals.Add(formal);

+              scope.Push(inv.Toks[i].val, formal);

+            }

+            ResolveExpression(inv.Expr, false, true);

+            scope.PopMarker();

+          }                

         } else {

           assert false;  // unexpected member type

         }

@@ -469,10 +496,10 @@ namespace Microsoft.Dafny {
         

     void ResolveTypeParameters(List<TypeParameter!>! tparams, bool emitErrors, TypeParameter.ParentType! parent) {

       // push type arguments of the refined class

-      if (parent is ClassRefinementDecl) {

+      if (checkRefinements && parent is ClassRefinementDecl) {

         ClassDecl refined = ((ClassRefinementDecl)parent).Refined;

-        assert refined != null;

-        ResolveTypeParameters(refined.TypeArgs, false, refined);

+        if (refined != null)

+          ResolveTypeParameters(refined.TypeArgs, false, refined);

       }

     

       // push non-duplicated type parameter names

diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index 5a762ef6..dcd1b60f 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -1747,12 +1747,8 @@ namespace Microsoft.Dafny {
       Bpl.IdentifierExpr heap = new Bpl.IdentifierExpr(m.tok, predef.HeapVarName, predef.HeapType);

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, heap, that);      

       

-      // for now, refinement is local -- if A.f is refined by B.g then f is shadowed by g in B.

-      // therefore, the abstract and concrete programs operate on different receivers thisA and thisB.

-      // there is still a possibility of A events polluting the heap that's used by B events, e.g. if another object is referenced by both thisA and thisB.

-

       // TODO: this straight inlining does not handle recursive calls

-      // TODO: we assume frame allows anything to be changed

+      // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure

             

       // generate procedure declaration with pre-condition wp(r, true)

       Bpl.Procedure! proc = AddMethod(r, false, true);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 82f1da59..b698f917 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -455,3 +455,12 @@ Dafny program verifier finished with 5 verified, 0 errors
 -------------------- Refinement.dfy --------------------

 

 Dafny program verifier finished with 53 verified, 0 errors

+

+-------------------- RefinementErrors.dfy --------------------

+RefinementErrors.dfy(1,6): Error: Detected a cyclic refinement declaration: C -> B -> A

+RefinementErrors.dfy(27,11): Error: Coupling invariants can only be declared in refinement classes

+RefinementErrors.dfy(40,6): Error: Refined class has a member with the same name as in the refinement class: x

+RefinementErrors.dfy(42,9): Error: Refined class has a member with the same name as in the refinement class: M

+RefinementErrors.dfy(12,10): Error: Refinement methods can only be declared in refinement classes: M

+RefinementErrors.dfy(34,10): Error: Different number of output variables

+6 resolution/type errors detected in RefinementErrors.dfy

diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy
new file mode 100644
index 00000000..de8694b3
--- /dev/null
+++ b/Test/dafny0/RefinementErrors.dfy
@@ -0,0 +1,57 @@
+class A refines C {
+}
+
+class B refines A {
+}
+
+class C refines B {
+}
+
+
+class D {
+  refines M()
+  {
+  }
+}
+
+class E {
+  var x: int;
+  
+  method M() 
+  {
+    x := 0;
+  }
+}
+
+class F {  
+  replaces M by x == y;
+}
+
+class G refines E {
+  var y: int;
+  replaces x by x == y;
+  
+  refines M() returns (i: int)
+  {
+  }
+}
+
+class H refines E {
+  var x: int;
+
+  method M() 
+  {
+  }
+}
+
+class J refines E {
+  var y: int;
+  replaces x by x == y;
+
+  refines M()
+  {
+    y := 1;
+  }
+}
+
+
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index e238f082..d29edd34 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -14,7 +14,7 @@ for %%f in (Simple.dfy) do (
 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy

-            TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Refinement.dfy) do (

+            TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Refinement.dfy RefinementErrors.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 %* %%f