Dafny: implemented the wellformedness check that datatype destructors are only applied to values created by the corresponding constructor

Dafny: implement ghost destructors properly

3 files changed, 19 insertions, 1 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 04b6b00e..e07c6f1d 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -867,6 +867,17 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class DatatypeDestructor : SpecialField

+  {

+    public readonly DatatypeCtor EnclosingCtor;

+

+    public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, string name, string compiledName, string preString, string postString, bool isGhost, Type type, Attributes attributes)

+      : base(tok, name, compiledName, preString, postString, isGhost, false, type, attributes)

+    {

+      EnclosingCtor = enclosingCtor;

+    }

+  }

+

   public class CouplingInvariant : MemberDecl {

     public readonly Expression Expr;

     public readonly List<IToken/*!*/>/*!*/ Toks;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index df2d2b0b..b6bc4059 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -254,7 +254,7 @@ namespace Microsoft.Dafny {
                 if (members.ContainsKey(formal.Name)) {

                   Error(ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);

                 } else {

-                  dtor = new SpecialField(formal.tok, formal.Name, "dtor_" + formal.Name, "", "", false, false, formal.Type, null);

+                  dtor = new DatatypeDestructor(formal.tok, ctor, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);

                   dtor.EnclosingClass = dt;  // resolve here

                   members.Add(formal.Name, dtor);

                 }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 37f80bf1..028891b5 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1650,6 +1650,9 @@ namespace Microsoft.Dafny {
           var t = IsTotal(e.Obj, etran);

           if (e.Obj.Type.IsRefType) {

             t = BplAnd(t, Bpl.Expr.Neq(etran.TrExpr(e.Obj), predef.Null));

+          } else if (e.Field is DatatypeDestructor) {

+            var dtor = (DatatypeDestructor)e.Field;

+            t = BplAnd(t, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)));

           }

           return t;

         }

@@ -2110,6 +2113,10 @@ namespace Microsoft.Dafny {
         CheckWellformed(e.Obj, options, locals, builder, etran);

         if (e.Obj.Type.IsRefType) {

           CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv);

+        } else if (e.Field is DatatypeDestructor) {

+          var dtor = (DatatypeDestructor)e.Field;

+          builder.Add(Assert(expr.tok, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)),

+            string.Format("destructor '{0}' can only be applied to datatype values constructed by '{1}'", dtor.Name, dtor.EnclosingCtor.Name)));

         }

         if (options.DoReadsChecks && e.Field.IsMutable) {

           builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field", options.AssertKv));