Dafny: Recheck specifications that contain refined (extended) predicates, even if they are contained inside a split expression. Superposition is thought to be sound.

7 files changed, 168 insertions, 65 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index a064064c..a15d236a 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -558,7 +558,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   [ FunctionBody<out bb, out bodyStart, out bodyEnd>  (. body = bb; .)

   ]

   (. if (isPredicate) {

-       f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals, reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs);

+       f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals, reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs);

      } else {

        f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals, returnType, reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs);

      }

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index e8fe2780..35829a15 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1098,11 +1098,14 @@ namespace Microsoft.Dafny {
 

   public class Predicate : Function

   {

+    public readonly bool BodyIsExtended;  // says that this predicate definition is a refinement extension of a predicate definition is a refining module

     public Predicate(IToken tok, string name, bool isStatic, bool isGhost, bool isUnlimited,

                      List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,

                      List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,

-                     Expression body, Attributes attributes)

+                     Expression body, bool bodyIsExtended, Attributes attributes)

       : base(tok, name, isStatic, isGhost, isUnlimited, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes) {

+      Contract.Requires(!bodyIsExtended || body != null);

+      BodyIsExtended = bodyIsExtended;

     }

   }

 

@@ -1908,44 +1911,56 @@ namespace Microsoft.Dafny {
 

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

 

-  public class NestedToken : IToken

+  public abstract class TokenWrapper : IToken

   {

-    public NestedToken(IToken outer, IToken inner) {

-      Outer = outer;

-      Inner = inner;

+    protected readonly IToken WrappedToken;

+    protected TokenWrapper(IToken wrappedToken) {

+      Contract.Requires(wrappedToken != null);

+      WrappedToken = wrappedToken;

     }

-    public readonly IToken Outer;

-    public readonly IToken Inner;

 

     public int col {

-      get { return Outer.col; }

-      set { Outer.col = value; }

+      get { return WrappedToken.col; }

+      set { throw new NotSupportedException(); }

     }

-    public string filename {

-      get { return Outer.filename; }

-      set { Outer.filename = value; }

+    public virtual string filename {

+      get { return WrappedToken.filename; }

+      set { throw new NotSupportedException(); }

     }

     public bool IsValid {

-      get { return Outer.IsValid; }

+      get { return WrappedToken.IsValid; }

     }

     public int kind {

-      get { return Outer.kind; }

-      set { Outer.kind = value; }

+      get { return WrappedToken.kind; }

+      set { throw new NotSupportedException(); }

     }

     public int line {

-      get { return Outer.line; }

-      set { Outer.line = value; }

+      get { return WrappedToken.line; }

+      set { throw new NotSupportedException(); }

     }

     public int pos {

-      get { return Outer.pos; }

-      set { Outer.pos = value; }

+      get { return WrappedToken.pos; }

+      set { throw new NotSupportedException(); }

     }

     public string val {

-      get { return Outer.val; }

-      set { Outer.val = value; }

+      get { return WrappedToken.val; }

+      set { throw new NotSupportedException(); }

     }

   }

 

+  public class NestedToken : TokenWrapper

+  {

+    public NestedToken(IToken outer, IToken inner)

+      : base(outer)

+    {

+      Contract.Requires(outer != null);

+      Contract.Requires(inner != null);

+      Inner = inner;

+    }

+    public IToken Outer { get { return WrappedToken; } }

+    public readonly IToken Inner;

+  }

+

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

 

   public abstract class Expression

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 1454121e..f070c6df 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -504,7 +504,7 @@ bool IsAttribute() {
 			body = bb; 

 		}

 		if (isPredicate) {

-		 f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals, reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs);

+		 f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals, reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs);

 		} else {

 		  f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals, returnType, reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs);

 		}

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index c97f47aa..6954ee87 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -19,13 +19,14 @@ using System.Diagnostics.Contracts;
 using IToken = Microsoft.Boogie.IToken;

 

 namespace Microsoft.Dafny {

-  public class RefinementToken : IToken

+  public class RefinementToken : TokenWrapper

   {

-    readonly IToken tok;

     public readonly ModuleDecl InheritingModule;

     public RefinementToken(IToken tok, ModuleDecl m)

+      : base(tok)

     {

-      this.tok = tok;

+      Contract.Requires(tok != null);

+      Contract.Requires(m != null);

       this.InheritingModule = m;

     }

 

@@ -43,34 +44,10 @@ namespace Microsoft.Dafny {
       var rtok = tok as RefinementToken;

       return rtok != null && rtok.InheritingModule == m;

     }

-

-    public int kind {

-      get { return tok.kind; }

-      set { throw new NotSupportedException(); }

-    }

-    public string filename {

-      get { return tok.filename + "[" + InheritingModule.Name + "]"; }

-      set { throw new NotSupportedException(); }

-    }

-    public int pos {

-      get { return tok.pos; }

-      set { throw new NotSupportedException(); }

-    }

-    public int col {

-      get { return tok.col; }

-      set { throw new NotSupportedException(); }

-    }

-    public int line {

-      get { return tok.line; }

+    public override string filename {

+      get { return WrappedToken.filename + "[" + InheritingModule.Name + "]"; }

       set { throw new NotSupportedException(); }

     }

-    public string/*!*/ val {

-      get { return tok.val; }

-      set { throw new NotSupportedException(); }

-    }

-    public bool IsValid {

-      get { return tok.IsValid; }

-    }

   }

 

   public class RefinementTransformer

@@ -548,12 +525,16 @@ namespace Microsoft.Dafny {
       var decreases = CloneSpecExpr(f.Decreases);

       var body = CloneExpr(f.Body);

       if (moreBody != null) {

-        body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, body, moreBody);

+        if (body == null) {

+          body = moreBody;

+        } else {

+          body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, body, moreBody);

+        }

       }

 

       if (f is Predicate) {

         return new Predicate(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, f.OpenParen, formals,

-          req, reads, ens, decreases, body, null);

+          req, reads, ens, decreases, body, moreBody != null, null);

       } else {

         return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, f.OpenParen, formals, CloneType(f.ResultType),

           req, reads, ens, decreases, body, null);

@@ -604,7 +585,7 @@ namespace Microsoft.Dafny {
                 reporter.Error(nwMember, "a refining function is not allowed to provided a body");

                 newBody = null;

               }

-              nw.Members[index] = CloneFunction((Function)member, f.Ens, f.Body);

+              nw.Members[index] = CloneFunction((Function)member, f.Ens, newBody);

             }

 

           } else {

@@ -637,5 +618,29 @@ namespace Microsoft.Dafny {
 

       return nw;

     }

+

+    // ---------------------- additional methods -----------------------------------------------------------------------------

+

+    public static bool ContainsChange(Expression expr, ModuleDecl m) {

+      Contract.Requires(expr != null);

+      Contract.Requires(m != null);

+

+      if (expr is FunctionCallExpr) {

+        var e = (FunctionCallExpr)expr;

+        if (e.Function.EnclosingClass.Module == m) {

+          var p = e.Function as Predicate;

+          if (p != null && p.BodyIsExtended) {

+            return true;

+          }

+        }

+      }

+

+      foreach (var ee in expr.SubExpressions) {

+        if (ContainsChange(ee, m)) {

+          return true;

+        }

+      }

+      return false;

+    }

   }

 }

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index a0e67ad1..a936899e 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3139,6 +3139,23 @@ namespace Microsoft.Dafny {
 

     // ----- Statement ----------------------------------------------------------------------------

 

+    /// <summary>

+    /// A ForceCheckToken is a token wrapper whose purpose is to hide inheritance.

+    /// </summary>

+    public class ForceCheckToken : TokenWrapper

+    {

+      public ForceCheckToken(IToken tok)

+        : base(tok) {

+        Contract.Requires(tok != null);

+      }

+      public static IToken Unwrap(IToken tok) {

+        Contract.Requires(tok != null);

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

+        var ftok = tok as ForceCheckToken;

+        return ftok != null ? ftok.WrappedToken : tok;

+      }

+    }

+

     Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage)

     {

       Contract.Requires(tok != null);

@@ -3150,7 +3167,7 @@ namespace Microsoft.Dafny {
         // produce an assume instead

         return new Bpl.AssumeCmd(tok, condition);

       } else {

-        var cmd = new Bpl.AssertCmd(tok, condition);

+        var cmd = new Bpl.AssertCmd(ForceCheckToken.Unwrap(tok), condition);

         cmd.ErrorData = "Error: " + errorMessage;

         return cmd;

       }

@@ -3167,6 +3184,7 @@ namespace Microsoft.Dafny {
         // produce a "skip" instead

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

       } else {

+        tok = ForceCheckToken.Unwrap(tok);

         var args = new List<object>();

         args.Add(Bpl.Expr.Literal(0));

         Bpl.QKeyValue kv = new Bpl.QKeyValue(tok, "subsumption", args, null);

@@ -3186,7 +3204,7 @@ namespace Microsoft.Dafny {
         // produce an assume instead

         return new Bpl.AssumeCmd(tok, condition, kv);

       } else {

-        var cmd = new Bpl.AssertCmd(tok, condition, kv);

+        var cmd = new Bpl.AssertCmd(ForceCheckToken.Unwrap(tok), condition, kv);

         cmd.ErrorData = "Error: " + errorMessage;

         return cmd;

       }

@@ -3198,7 +3216,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(condition != null);

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

 

-      Bpl.Ensures ens = new Bpl.Ensures(tok, free, condition, comment);

+      Bpl.Ensures ens = new Bpl.Ensures(ForceCheckToken.Unwrap(tok), free, condition, comment);

       if (errorMessage != null) {

         ens.ErrorData = errorMessage;

       }

@@ -3209,7 +3227,7 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(tok != null);

       Contract.Requires(condition != null);

-      Bpl.Requires req = new Bpl.Requires(tok, free, condition, comment);

+      Bpl.Requires req = new Bpl.Requires(ForceCheckToken.Unwrap(tok), free, condition, comment);

       if (errorMessage != null) {

         req.ErrorData = errorMessage;

       }

@@ -6597,14 +6615,25 @@ namespace Microsoft.Dafny {
         }

       }

 

+      Bpl.Expr translatedExpression;

+      bool splitHappened;

       if ((position && expr is ExistsExpr) || (!position && expr is ForallExpr)) {

-        splits.Add(new SplitExprInfo(false, etran.TrExpr(expr)));

-        return false;

+        translatedExpression = etran.TrExpr(expr);

+        splitHappened = false;

       } else {

         etran = etran.LayerOffset(1);

-        splits.Add(new SplitExprInfo(false, etran.TrExpr(expr)));

-        return etran.Statistics_CustomLayerFunctionCount != 0;  // return true if the LayerOffset(1) came into play

-      }

+        translatedExpression = etran.TrExpr(expr);

+        splitHappened = etran.Statistics_CustomLayerFunctionCount != 0;  // return true if the LayerOffset(1) came into play

+      }

+      if (RefinementToken.IsInherited(expr.tok, currentModule) && RefinementTransformer.ContainsChange(expr, currentModule)) {

+        // If "expr" contains a subexpression that has changed from the inherited expression, we'll destructively

+        // change the token of the translated expression to make it look like it's not inherited.  This will cause "e" to

+        // be verified again in the refining module.

+        translatedExpression.tok = new ForceCheckToken(expr.tok);

+        splitHappened = true;  // count this as a split, so this translated expression is not ignored

+      }

+      splits.Add(new SplitExprInfo(false, translatedExpression));

+      return splitHappened;

     }

 

     List<BoundVar> ApplyInduction(QuantifierExpr e) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1702ad53..3be192cc 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1397,8 +1397,16 @@ Predicates.dfy(131,7): Related location: Related location
 Predicates.dfy[Tricky_Full](111,9): Related location: Related location

 Execution trace:

     (0,0): anon0

+Predicates.dfy(159,5): Error BP5003: A postcondition might not hold on this return path.

+Predicates.dfy(158,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+Predicates.dfy[Q1](149,5): Error BP5003: A postcondition might not hold on this return path.

+Predicates.dfy[Q1](148,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 33 verified, 4 errors

+Dafny program verifier finished with 52 verified, 6 errors

 

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index f7b6e07f..f8569b3a 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -132,3 +132,49 @@ module Tricky_Full refines Tricky_Base {
     }

   }

 }

+

+// -------- Quantifiers ----------------------------------------

+

+module Q0 {

+  class C {

+    var x: int;

+    predicate P

+      reads this;

+    {

+      true

+    }

+    method M()

+      modifies this;

+      ensures forall c: C :: c != null ==> c.P;

+    {

+    }

+    predicate Q

+      reads this;

+    {

+      x < 100

+    }

+    method N()

+      modifies this;

+      ensures forall c :: c == this ==> c.Q;

+    {

+      x := 102;  // error: fails to establish postcondition (but this error should not be repeated in Q1 below)

+    }

+    predicate R reads this;  // a body-less predicate

+  }

+}

+

+module Q1 refines Q0 {

+  class C {

+    predicate P

+    {

+      x == 18

+    }

+    predicate R  // no body yet

+  }

+}

+

+module Q2 refines Q1 {

+  class C {

+    predicate R { x % 3 == 2 }  // finally, give it a body

+  }

+}