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

Dafny: implement ghost destructors properly

6 files changed, 44 insertions, 5 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 04b6b00e..e07c6f1d 100644
--- a/Dafny/DafnyAst.cs
+++ b/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/Dafny/Resolver.cs b/Dafny/Resolver.cs
index df2d2b0b..b6bc4059 100644
--- a/Dafny/Resolver.cs
+++ b/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/Dafny/Translator.cs b/Dafny/Translator.cs
index 37f80bf1..028891b5 100644
--- a/Dafny/Translator.cs
+++ b/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));

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3198df33..50c238fc 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -484,7 +484,8 @@ ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called w
 ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)

 ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)

 ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)

-44 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts

+45 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -1154,8 +1155,15 @@ Execution trace:
     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon5_Then

+Datatypes.dfy(198,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'

+Execution trace:

+    (0,0): anon0

+Datatypes.dfy(201,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

 

-Dafny program verifier finished with 29 verified, 3 errors

+Dafny program verifier finished with 29 verified, 5 errors

 

 -------------------- TypeAntecedents.dfy --------------------

 TypeAntecedents.dfy(32,13): Error: assertion violation

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index eb527e0d..aff12fda 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -194,6 +194,17 @@ method InjectivityTests(d: XList)
   }

 }

 

+method MatchingDestructor(d: XList) returns (r: XList)

+  ensures r.Car == 5;  // error: specification is not well-formed (since r might not be an XCons)

+{

+  if (*) {

+    var x0 := d.Car;  // error: d might not be an XCons

+  } else if (d.XCons?) {

+    var x1 := d.Car;

+  }

+  r := XCons(5, XNil);

+}

+

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

 

 method FwdBug(f: Fwd, initialized: bool)

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 1b68ad91..e5e56d03 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -292,7 +292,7 @@ method ConstructorTests()
 

 // ------------------- datatype destructors ---------------------------------------

 

-datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List);

+datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List, ghost g: int);

 

 method DatatypeDestructors(d: DTD_List) {

   if {

@@ -304,6 +304,8 @@ method DatatypeDestructors(d: DTD_List) {
       assert hd == d.Cdr;  // type error

       assert tl == d.Car;  // type error

       assert d.DTD_Cons? == d.Car;  // type error

-      assert d == DTD_Cons(hd, tl);

+      assert d == DTD_Cons(hd, tl, 5);

+      ghost var g0 := d.g;  // fine

+      var g1 := d.g;  // error: cannot use ghost member in non-ghost code

   }

 }