Dafny: added verification that replaced expressions are the same as the original

6 files changed, 37 insertions, 24 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 958726fd..c63c5d3c 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1504,7 +1504,7 @@ NamedExpr<out Expression e>
     NoUSIdent<out d>

     ":"

     Expression<out e>               (. expr = e;

-                                       e = new NamedExpr(x, d, expr); .)

+                                       e = new NamedExpr(x, d.val, expr); .)

   .

 

 MatchExpression<out Expression/*!*/ e>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c2a4ace3..d20d0d56 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -904,7 +904,7 @@ namespace Microsoft.Dafny {
   }

 

   public class DefaultModuleDecl : ModuleDefinition {

-    public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, false) {

+    public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, true) {

     }

     public override bool IsDefaultModule {

       get {

@@ -3382,25 +3382,31 @@ namespace Microsoft.Dafny {
       }

     }

   }

-

+  // Represents expr Name: Body

+  //         or expr Name: (assert Body == Contract; Body)

   public class NamedExpr : Expression

   {

     public readonly string Name;

     public readonly Expression Body;

-    public NamedExpr(IToken tok, IToken name, Expression body)

+    public readonly Expression Contract;

+    public readonly IToken ReplacerToken;

+

+    public NamedExpr(IToken tok, string p, Expression body)

       : base(tok) {

-      Name = name.val;

+      Name = p;

       Body = body;

     }

-

-    public NamedExpr(IToken tok, string p, Expression body)

+    public NamedExpr(IToken tok, string p, Expression body, Expression contract, IToken token)

       : base(tok) {

       Name = p;

       Body = body;

+      Contract = contract;

+      ReplacerToken = token;

     }

     public override IEnumerable<Expression> SubExpressions {

       get {

         yield return Body;

+        if (Contract != null) yield return Contract;

       }

     }

   }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 6adc4df0..b8324dab 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2658,7 +2658,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(5);

 		Expression(out e);

 		expr = e;

-		e = new NamedExpr(x, d, expr); 

+		e = new NamedExpr(x, d.val, expr); 

 	}

 

 	void CaseExpression(out MatchCaseExpr/*!*/ c) {

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 68ab2c20..d27ef13d 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -806,7 +806,7 @@ namespace Microsoft.Dafny {
 

       return nw;

     }

-    private Statement SubstituteNamedExpr(Statement s, string p, Expression E, ref int subCount) {

+    private Statement SubstituteNamedExpr(Statement s, IToken p, Expression E, ref int subCount) {

       if (s == null) {

         return null;

       } else if (s is AssertStmt) {

@@ -886,15 +886,15 @@ namespace Microsoft.Dafny {
       }

 

     }

-    private Expression SubstituteNamedExpr(Expression expr, string p, Expression E, ref int subCount) {

+    private Expression SubstituteNamedExpr(Expression expr, IToken p, Expression E, ref int subCount) {

       if (expr == null) {

         return null;

       }

       if (expr is NamedExpr) {

         NamedExpr n = (NamedExpr)expr;

-        if (n.Name == p) {

+        if (n.Name == p.val) {

           subCount++;

-          return new NamedExpr(n.tok, n.Name, E);

+          return new NamedExpr(n.tok, n.Name, E, CloneExpr(n.Body), p);

         } else return new NamedExpr(n.tok, n.Name, SubstituteNamedExpr(n.Body, p, E, ref subCount));

       } else if (expr is LiteralExpr || expr is WildcardExpr | expr is ThisExpr || expr is IdentifierExpr) {

         return expr;

@@ -1021,7 +1021,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    private List<Expression> SubstituteNamedExprList(List<Expression> list, string p, Expression E, ref int subCount) {

+    private List<Expression> SubstituteNamedExprList(List<Expression> list, IToken p, Expression E, ref int subCount) {

       List<Expression> res = new List<Expression>();

       foreach (Expression e in list) {

         res.Add(SubstituteNamedExpr(e, p, E, ref subCount));

@@ -1165,14 +1165,14 @@ namespace Microsoft.Dafny {
                   // loop invariant:  oldS == oldStmt.Body[j]

                   var s = CloneStmt(oldS);

                   if (c.NameReplacements != null)

-                    s = SubstituteNamedExpr(s, c.NameReplacements[0].val, c.ExprReplacements[0], ref subCount);

+                    s = SubstituteNamedExpr(s, c.NameReplacements[0], c.ExprReplacements[0], ref subCount);

                   body.Add(s);

                   j++;

                   if (j == oldStmt.Body.Count) { break; }

                   oldS = oldStmt.Body[j];

                 }

                 if (c.NameReplacements != null && subCount == 0)

-                  reporter.Error(c.NameReplacements[0], "did not find expression labeld {0}", c.NameReplacements[0].val);

+                  reporter.Error(c.NameReplacements[0], "did not find expression labeled {0}", c.NameReplacements[0].val);

               }

               i++;

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index b226c3fe..33f86258 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3906,6 +3906,7 @@ namespace Microsoft.Dafny {
       } else if (expr is NamedExpr) {

         var e = (NamedExpr)expr;

         ResolveExpression(e.Body, twoState);

+        if (e.Contract != null) ResolveExpression(e.Contract, twoState);

         e.Type = e.Body.Type;

       }else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 5d0baaed..75b2e845 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2050,7 +2050,11 @@ namespace Microsoft.Dafny {
         return BplAnd(canCall, CanCallAssumption(etran.GetSubstitutedBody(e), etran));

 

       } else if (expr is NamedExpr) {

-        return CanCallAssumption(((NamedExpr)expr).Body, etran);

+        var e = (NamedExpr)expr;

+        var canCall = CanCallAssumption(e.Body, etran);

+        if (e.Contract != null)

+          return BplAnd(canCall, CanCallAssumption(e.Contract, etran));

+        else return canCall;

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var total = CanCallAssumption(e.Term, etran);

@@ -2080,9 +2084,7 @@ namespace Microsoft.Dafny {
         total = BplAnd(total, Bpl.Expr.Imp(test, CanCallAssumption(e.Thn, etran)));

         total = BplAnd(total, Bpl.Expr.Imp(Bpl.Expr.Not(test), CanCallAssumption(e.Els, etran)));

         return total;

-      } else if (expr is NamedExpr) {

-        return CanCallAssumption(((NamedExpr)expr).Body, etran);

-       } else if (expr is ConcreteSyntaxExpression) {

+      } else if (expr is ConcreteSyntaxExpression) {

         var e = (ConcreteSyntaxExpression)expr;

         return CanCallAssumption(e.ResolvedExpression, etran);

       } else {

@@ -2517,7 +2519,13 @@ namespace Microsoft.Dafny {
         result = null;

 

       } else if (expr is NamedExpr) {

-        CheckWellformedWithResult(((NamedExpr)expr).Body, options, result, resultType, locals, builder, etran);

+        var e = (NamedExpr)expr;

+        CheckWellformedWithResult(e.Body, options, result, resultType, locals, builder, etran);

+        if (e.Contract != null) {

+          CheckWellformedWithResult(e.Contract, options, result, resultType, locals, builder, etran);

+          var theSame = Bpl.Expr.Eq(etran.TrExpr(e.Body), etran.TrExpr(e.Contract));

+          builder.Add(Assert(new ForceCheckToken(e.ReplacerToken), theSame, "replacement must be the same value"));

+        }

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran);

@@ -6011,7 +6019,6 @@ namespace Microsoft.Dafny {
         } else if (expr is LetExpr) {

           var e = (LetExpr)expr;

           return TrExpr(GetSubstitutedBody(e));

-

         } else if (expr is NamedExpr) {

           return TrExpr(((NamedExpr)expr).Body);

         } else if (expr is QuantifierExpr) {

@@ -7684,9 +7691,8 @@ namespace Microsoft.Dafny {
       } else if (expr is NamedExpr) {

         var e = (NamedExpr)expr;

         var body = Substitute(e.Body, receiverReplacement, substMap);

-        if (body != e.Body) {

-          newExpr = new NamedExpr(e.tok, e.Name, body);

-        }

+        var contract = e.Contract == null ? null : Substitute(e.Contract, receiverReplacement, substMap);

+        newExpr = new NamedExpr(e.tok, e.Name, body, contract, e.ReplacerToken);

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);