Dafny: Improved default decreases clauses for methods and functions

Dafny:  Don't display "alloc" field in BVD
Chalice:  Fixed error-message parsing error in VS mode

7 files changed, 50 insertions, 33 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index f83dd67a..d2c955c1 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1597,7 +1597,7 @@ namespace Microsoft.Dafny {
     }

   }

 

-  class MatchStmt : Statement {

+  public class MatchStmt : Statement {

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Source != null);

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 44e05a41..6c21ecd0 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -1571,17 +1571,10 @@ namespace Microsoft.Dafny {
           ModuleDecl module = cce.NonNull(e.Function.EnclosingClass).Module;

           if (module == cce.NonNull(func.EnclosingClass).Module) {

             if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(func)) {

-              List<Expression> contextDecreases = func.Decreases;

-              if (contextDecreases.Count == 0) {

-                contextDecreases = new List<Expression>();

-                contextDecreases.Add(FrameToObjectSet(func.Reads));  // use its reads clause instead

-              }

-              List<Expression> calleeDecreases = e.Function.Decreases;

-              if (calleeDecreases.Count == 0) {

-                calleeDecreases = new List<Expression>();

-                calleeDecreases.Add(FrameToObjectSet(e.Function.Reads));  // use its reads clause instead

-              }

-              CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);

+              bool contextDecrInferred, calleeDecrInferred;

+              List<Expression> contextDecreases = FunctionDecreasesWithDefault(func, out contextDecrInferred);

+              List<Expression> calleeDecreases = FunctionDecreasesWithDefault(e.Function, out calleeDecrInferred);

+              CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder, contextDecrInferred);

             }

           }

         }

@@ -1684,7 +1677,45 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

       }

     }

-    

+

+    List<Expression> MethodDecreasesWithDefault(Method m, out bool inferredDecreases) {

+      Contract.Requires(m != null);

+

+      inferredDecreases = false;

+      List<Expression> decr = m.Decreases;

+      if (decr.Count == 0) {

+        decr = new List<Expression>();

+        foreach (Formal p in m.Ins) {

+          IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

+          ie.Var = p; ie.Type = ie.Var.Type;  // resolve it here

+          decr.Add(ie);  // use the method's first parameter instead

+        }

+        inferredDecreases = true;

+      }

+      return decr;

+    }

+

+    List<Expression> FunctionDecreasesWithDefault(Function f, out bool inferredDecreases) {

+      Contract.Requires(f != null);

+

+      inferredDecreases = false;

+      List<Expression> decr = f.Decreases;

+      if (decr.Count == 0) {

+        decr = new List<Expression>();

+        if (f.Reads.Count == 0) {

+          foreach (Formal p in f.Formals) {

+            IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

+            ie.Var = p; ie.Type = ie.Var.Type;  // resolve it here

+            decr.Add(ie);  // use the function's first parameter instead

+          }

+          inferredDecreases = true;

+        } else {

+          decr.Add(FrameToObjectSet(f.Reads));  // use its reads clause instead

+        }

+      }

+      return decr;

+    }

+

     Expression FrameToObjectSet(List<FrameExpression> fexprs) {

       Contract.Requires(fexprs != null);

       Contract.Ensures(Contract.Result<Expression>() != null);

@@ -2568,7 +2599,10 @@ void ObjectInvariant()
         ModuleDecl module = cce.NonNull(s.Method.EnclosingClass).Module;

         if (module == cce.NonNull(currentMethod.EnclosingClass).Module) {

           if (module.CallGraph.GetSCCRepresentative(s.Method) == module.CallGraph.GetSCCRepresentative(currentMethod)) {

-            CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);

+            bool contextDecrInferred, calleeDecrInferred;

+            List<Expression> contextDecreases = MethodDecreasesWithDefault(currentMethod, out contextDecrInferred);

+            List<Expression> calleeDecreases = MethodDecreasesWithDefault(s.Method, out calleeDecrInferred);

+            CheckCallTermination(stmt.Tok, contextDecreases, calleeDecreases, s.Receiver, substMap, etran, builder, contextDecrInferred);

           }

         }

 

@@ -3108,7 +3142,7 @@ void ObjectInvariant()
         

     void CheckCallTermination(IToken/*!*/ tok, List<Expression/*!*/>/*!*/ contextDecreases, List<Expression/*!*/>/*!*/ calleeDecreases,

                               Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap,

-                              ExpressionTranslator/*!*/ etran, Bpl.StmtListBuilder/*!*/ builder){

+                              ExpressionTranslator/*!*/ etran, Bpl.StmtListBuilder/*!*/ builder, bool inferredDecreases) {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(contextDecreases));

       Contract.Requires(cce.NonNullElements(calleeDecreases));

@@ -3133,7 +3167,7 @@ void ObjectInvariant()
         caller.Add(etran.TrExpr(e1));

       }

       Bpl.Expr decrExpr = DecreasesCheck(toks, types, callee, caller, etran, builder, "", false);

-      builder.Add(Assert(tok, decrExpr, "failure to decrease termination measure"));

+      builder.Add(Assert(tok, decrExpr, inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure"));

     }

     

     /// <summary>

diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
index 70b38a5d..540225a1 100644
--- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -166,7 +166,6 @@ class LinkedList<T> {
   }

 

   static function method ReverseSeq(s: seq<T>): seq<T>

-    decreases s;

   {

     if s == [] then [] else

     ReverseSeq(s[1..]) + [s[0]]

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 9e4da459..197d6916 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -10,7 +10,6 @@ datatype Expr {
 }

 

 static function Subst(e: Expr, v: int, val: int): Expr

-  decreases e;

 {

   match e

   case Const(c) => e

@@ -19,7 +18,6 @@ static function Subst(e: Expr, v: int, val: int): Expr
 }

 

 static function SubstList(l: List, v: int, val: int): List

-  decreases l;

 {

   match l

   case Nil => l

@@ -28,7 +26,6 @@ static function SubstList(l: List, v: int, val: int): List
 

 static ghost method Theorem(e: Expr, v: int, val: int)

   ensures Subst(Subst(e, v, val), v, val) == Subst(e, v, val);

-  decreases e;

 {

   match e {

     case Const(c) =>

@@ -40,7 +37,6 @@ static ghost method Theorem(e: Expr, v: int, val: int)
 

 static ghost method Lemma(l: List, v: int, val: int)

   ensures SubstList(SubstList(l, v, val), v, val) == SubstList(l, v, val);

-  decreases l;

 {

   match l {

     case Nil =>

@@ -110,7 +106,6 @@ static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>,
   ensures |SubstSeq(parent, q, v, val)| == |q|;

   ensures (forall k :: 0 <= k && k < |q| ==>

             SubstSeq(parent, q, v, val)[k] == Substitute(q[k], v, val));

-  decreases q;

 {

   if (q == []) {

   } else {

diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy
index b4fab490..2fecaee5 100644
--- a/Test/dafny1/SumOfCubes.dfy
+++ b/Test/dafny1/SumOfCubes.dfy
@@ -43,7 +43,6 @@ class SumOfCubes {
 

   static function GSum(k: int): int

     requires 0 <= k;

-    decreases k;

   {

     if k == 0 then 0 else GSum(k-1) + k-1

   }

@@ -86,7 +85,6 @@ class SumOfCubes {
 

   static function SumEmDown(n: int, m: int): int

     requires 0 <= n && n <= m;

-    decreases m;

   {

     if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)

   }

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index 6b63bfec..fb530258 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -3,7 +3,6 @@ class Example {
   {

     var i := 0;

     while (i < n)

-      decreases n - i;

     {

       i := i + 1;

     }

@@ -14,7 +13,6 @@ class Example {
 

 class Fibonacci {

   function Fib(n: int): int

-    decreases n;

   {

     if n < 2 then n else Fib(n-2) + Fib(n-1)

   }

@@ -24,7 +22,6 @@ class Fibonacci {
 

 class Ackermann {

   function F(m: int, n: int): int

-    decreases m, n;

   {

     if m <= 0 then

       n + 1

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index 58124171..7fc62feb 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -10,14 +10,12 @@ datatype Tree {
 }

 

 static function Inc(t: Tree): Tree

-  decreases t;

 {

   match t

   case Node(n, children) => #Tree.Node(n+1, ForestInc(children))

 }

 

 static function ForestInc(forest: List<Tree>): List<Tree>

-  decreases forest;

 {

   match forest

   case Nil => forest

@@ -31,14 +29,12 @@ datatype GTree<T> {
 }

 

 static function GInc(t: GTree<int>): GTree<int>

-  decreases t;

 {

   match t

   case Node(n, children) => #GTree.Node(n+1, GForestInc(children))

 }

 

 static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>

-  decreases forest;

 {

   match forest

   case Nil => forest

@@ -57,14 +53,12 @@ datatype OneTree {
 }

 

 static function XInc(t: OneTree): OneTree

-  decreases t;

 {

   match t

   case Node(n, children) => #OneTree.Node(n+1, XForestInc(children))

 }

 

 static function XForestInc(forest: TreeList): TreeList

-  decreases forest;

 {

   match forest

   case Nil => forest