diff options
author | 2011-11-11 17:40:39 -0800 | |
---|---|---|
committer | 2011-11-11 17:40:39 -0800 | |
commit | bde073a24d6a30c9e6f970d1a49d8281b7f986a7 (patch) | |
tree | 6c461f16bc7db54b34ff4eb070be360e5369a8ae | |
parent | c0f4d89c9a16d92b717de6694286f98b90ef76e9 (diff) |
Dafny: implemented the wellformedness check that datatype destructors are only applied to values created by the corresponding constructor
Dafny: implement ghost destructors properly
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 11 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 2 | ||||
-rw-r--r-- | Source/Dafny/Translator.cs | 7 | ||||
-rw-r--r-- | Test/dafny0/Answer | 12 | ||||
-rw-r--r-- | Test/dafny0/Datatypes.dfy | 11 | ||||
-rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 6 |
6 files changed, 44 insertions, 5 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));
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
}
}
|