Fixed a bug in the Substituter for datatype update expressions.

5 files changed, 35 insertions, 16 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index cbbd2c2e..fa7fde12 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -4709,7 +4709,9 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// Returns the non-null subexpressions of the Expression.

+    /// Returns the non-null subexpressions of the Expression.  To be called after the expression has been resolved; this

+    /// means, for example, that any concrete syntax that resolves to some other expression will return the subexpressions

+    /// of the resolved expression.

     /// </summary>

     public virtual IEnumerable<Expression> SubExpressions {

       get { yield break; }

@@ -5469,11 +5471,26 @@ namespace Microsoft.Dafny {
     }

   }

 

+  /// <summary>

+  /// Represents an expression of the form A[B := C], where, syntactically, A, B, and C are expressions.

+  /// Successfully resolved, the expression stands for one of the following:

+  /// * if A is a sequence, then B is an integer-based index into the sequence and C's type is the sequence element type

+  /// * if A is a map(T,U), then B is a key of type T and C is a value of type U

+  /// * if A is a multiset, then B's type is the multiset element type and C is an integer-based numeric

+  /// * if A is a datatype, then B is the name of a destructor of A's type and C's type is the type of that destructor -- in

+  ///   this case, the resolver will set the ResolvedUpdateExpr to an expression that constructs an appropriate datatype value

+  /// </summary>

   public class SeqUpdateExpr : Expression {

     public readonly Expression Seq;

     public readonly Expression Index;

     public readonly Expression Value;

-    public Expression ResolvedUpdateExpr;       // May be filled in during resolution

+    public Expression ResolvedUpdateExpr;       // filled in during resolution, if the SeqUpdateExpr corresponds to a datatype update

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(Seq != null);

+      Contract.Invariant(Index != null);

+      Contract.Invariant(Value != null);

+    }

 

     public SeqUpdateExpr(IToken tok, Expression seq, Expression index, Expression val)

       : base(tok) {

@@ -5484,7 +5501,6 @@ namespace Microsoft.Dafny {
       Seq = seq;

       Index = index;

       Value = val;

-      ResolvedUpdateExpr = null;

     }

 

     public override IEnumerable<Expression> SubExpressions {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a2ffec6e..a44491de 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -6459,7 +6459,7 @@ namespace Microsoft.Dafny
                 // Build the arguments to the datatype constructor, using the updated value in the appropriate slot

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

                 foreach (Formal d in ctor.Formals) {

-                  if (d.Name == destructor.Name) {

+                  if (d == destructor.CorrespondingFormal) {

                     ctor_args.Add(e.Value);

                   } else {                    

                     ctor_args.Add(new ExprDotName(expr.tok, tmpVarIdExpr, d.Name));

@@ -8652,8 +8652,8 @@ namespace Microsoft.Dafny
       } else if (expr is SeqUpdateExpr) {

         SeqUpdateExpr e = (SeqUpdateExpr)expr;

         return UsesSpecFeatures(e.Seq) ||

-               (e.Index != null && UsesSpecFeatures(e.Index)) ||

-               (e.Value != null && UsesSpecFeatures(e.Value));

+               UsesSpecFeatures(e.Index) ||

+               UsesSpecFeatures(e.Value);

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         if (cce.NonNull(e.Function).IsGhost) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index df5b65a0..402a070c 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -13022,18 +13022,14 @@ namespace Microsoft.Dafny {
           }

 

         } else if (expr is SeqUpdateExpr) {

-          SeqUpdateExpr sse = (SeqUpdateExpr)expr;

-          if (sse.ResolvedUpdateExpr != null)

-          {

-            newExpr = Substitute(sse.ResolvedUpdateExpr);

-          }

-          else

-          {

+          var sse = (SeqUpdateExpr)expr;

+          if (sse.ResolvedUpdateExpr != null) {

+            return Substitute(sse.ResolvedUpdateExpr);

+          } else {

             Expression seq = Substitute(sse.Seq);

             Expression index = Substitute(sse.Index);

             Expression val = Substitute(sse.Value);

-            if (seq != sse.Seq || index != sse.Index || val != sse.Value)

-            {

+            if (seq != sse.Seq || index != sse.Index || val != sse.Value) {

               newExpr = new SeqUpdateExpr(sse.tok, seq, index, val);

             }

           }

diff --git a/Test/dafny0/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy
index 09f07dd3..7869fba3 100644
--- a/Test/dafny0/DatatypeUpdate.dfy
+++ b/Test/dafny0/DatatypeUpdate.dfy
@@ -21,3 +21,10 @@ method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:
 

     assert abc[myint := abc.myint - 2] == foo[myint := x];

 }

+

+// regression test (for a previous bug in the Translator.Substituter):

+datatype Dt = Ctor(x: int, y: bool)

+function F(d: Dt): Dt

+{

+  d[x := 5]

+}

diff --git a/Test/dafny0/DatatypeUpdate.dfy.expect b/Test/dafny0/DatatypeUpdate.dfy.expect
index 069e7767..52595bf9 100644
--- a/Test/dafny0/DatatypeUpdate.dfy.expect
+++ b/Test/dafny0/DatatypeUpdate.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 2 verified, 0 errors

+Dafny program verifier finished with 3 verified, 0 errors