From 899d1f3d30abf3343b88c0e4c6e44db130c6345b Mon Sep 17 00:00:00 2001 From: "peter mueller peter.mueller@inf.ethz.ch" Date: Thu, 29 Sep 2011 19:32:48 +0200 Subject: Dafny: Added TreeBarrier as a test case --- Test/dafny2/Answer | 6 ++ Test/dafny2/TreeBarrier.dfy | 143 ++++++++++++++++++++++++++++++++++++++++++++ Test/dafny2/runtest.bat | 2 +- 3 files changed, 150 insertions(+), 1 deletion(-) create mode 100644 Test/dafny2/TreeBarrier.dfy diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index 3eb32da8..bef70cf1 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -1,4 +1,10 @@ -------------------- SnapshotableTrees.dfy -------------------- +Dafny program verifier version 2.2.30705.1126, Copyright (c) 2003-2011, Microsoft. Dafny program verifier finished with 37 verified, 0 errors + +-------------------- TreeBarrier.dfy -------------------- +Dafny program verifier version 2.2.30705.1126, Copyright (c) 2003-2011, Microsoft. + +Dafny program verifier finished with 8 verified, 0 errors diff --git a/Test/dafny2/TreeBarrier.dfy b/Test/dafny2/TreeBarrier.dfy new file mode 100644 index 00000000..f4cc25d2 --- /dev/null +++ b/Test/dafny2/TreeBarrier.dfy @@ -0,0 +1,143 @@ +class Node { + var left: Node; + var right: Node; + var parent: Node; + var anc: set; + var desc: set; + var sense: bool; + var pc: int; + + + function validDown(): bool + reads this, desc; + { + this !in desc && + null !in desc && + left != right && // not needed, but speeds up verification + + (right != null ==> right in desc && left !in right.desc) && + + (left != null ==> + left in desc && + (right != null ==> desc == {left,right} + left.desc + right.desc) && + (right == null ==> desc == {left} + left.desc) && + left.validDown()) && + (left == null ==> + (right != null ==> desc == {right} + right.desc) && + (right == null ==> desc == {})) && + + (right != null ==> right.validDown()) && + + (blocked() ==> forall m :: m in desc ==> m.blocked()) && + (after() ==> forall m :: m in desc ==> m.blocked() || m.after()) +// (left != null && right != null ==> left.desc !! right.desc) // not needed + } + + + + + function validUp(): bool + reads this, anc; + { + this !in anc && + null !in anc && + (parent != null ==> parent in anc && anc == { parent } + parent.anc && parent.validUp()) && + (parent == null ==> anc == {}) && + (after() ==> forall m :: m in anc ==> m.after()) + } + + function valid(): bool + reads this, desc, anc; + { validUp() && validDown() && desc !! anc } + + function before(): bool + reads this; + { !sense && pc <= 2 } + + function blocked(): bool + reads this; + { sense } + + function after(): bool + reads this; + { !sense && 3 <= pc } + + + method barrier() + requires valid(); + requires before(); + modifies this, left, right; + { + +//A + pc := 1; + if(left != null) { + while(!left.sense) + modifies left; + invariant validDown(); // this seems necessary to get the necessary unfolding of functions + invariant valid(); + decreases *; // to by-pass termination checking for this loop + { + // this loop body is supposed to model what the "left" thread + // might do to its node. This body models a transition from + // "before" to "blocked" by setting sense to true. A transition + // all the way to "after" is not permitted; this would require + // a change of pc. + // We assume that "left" preserves the validity of its subtree, + // which means in particular that it goes to "blocked" only if + // all its descendants are already blocked. + left.sense := *; + assume left.blocked() ==> forall m :: m in left.desc ==> m.blocked(); + } + } + if(right != null) { + while(!right.sense) + modifies right; + invariant validDown(); // this seems necessary to get the necessary unfolding of functions + invariant valid(); + decreases *; // to by-pass termination checking for this loop + { + // analogous to the previous loop + right.sense := *; + assume right.blocked() ==> forall m :: m in right.desc ==> m.blocked(); + } + } + +//B + pc := 2; + if(parent != null) { + sense := true; + } +//C + pc := 3; + while(sense) + modifies this; + invariant validUp(); // this seems necessary to get the necessary unfolding of functions + invariant valid(); + invariant left == old(left); + invariant right == old(right); + invariant sense ==> parent != null; + decreases *; // to by-pass termination checking for this loop + { + // this loop body is supposed to model what the "parent" thread + // might do to its node. The body models a transition from + // "blocked" to "after" by setting sense to false. + // We assume that "parent" initiates this transition only + // after it went to state "after" itself. + sense := *; + assume !sense ==> parent.after(); + } +//D + pc := 4; + if(left != null) { + left.sense := false; + } +//E + pc := 5; + if(right != null) { + right.sense := false; + } +//F + pc := 6; + } +} diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index a58b03c6..62b0b6fe 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -5,7 +5,7 @@ set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe -for %%f in (SnapshotableTrees.dfy) do ( +for %%f in (SnapshotableTrees.dfy TreeBarrier.dfy) do ( echo. echo -------------------- %%f -------------------- -- cgit v1.2.3 From 8f65d1f0ba1397b57feb11256c0dc344fee465af Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 29 Sep 2011 18:33:09 -0700 Subject: Dafny: improved a resolution error message, and fixed a crash in the resolver --- Dafny/Resolver.cs | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index b9f5e7e6..54a3de3b 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -2809,15 +2809,17 @@ namespace Microsoft.Dafny { } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; - if (e.Function != null && e.Function.IsGhost) { - Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')"); - return; - } - // function is okay, so check all NON-ghost arguments - CheckIsNonGhost(e.Receiver); - for (int i = 0; i < e.Function.Formals.Count; i++) { - if (!e.Function.Formals[i].IsGhost) { - CheckIsNonGhost(e.Args[i]); + if (e.Function != null) { + if (e.Function.IsGhost) { + Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')"); + return; + } + // function is okay, so check all NON-ghost arguments + CheckIsNonGhost(e.Receiver); + for (int i = 0; i < e.Function.Formals.Count; i++) { + if (!e.Function.Formals[i].IsGhost) { + CheckIsNonGhost(e.Args[i]); + } } } return; @@ -2885,9 +2887,13 @@ namespace Microsoft.Dafny { #endif if (member == null) { // error has already been reported by ResolveMember - } else if (allowMethodCall && member is Method) { - // it's a method - return new CallRhs(e.tok, e.Receiver, e.Name, e.Args); + } else if (member is Method) { + if (allowMethodCall) { + // it's a method + return new CallRhs(e.tok, e.Receiver, e.Name, e.Args); + } else { + Error(e, "member {0} in type {1} refers to a method, but only functions can be used in this context", e.Name, cce.NonNull(ctype).Name); + } } else if (!(member is Function)) { Error(e, "member {0} in type {1} does not refer to a function", e.Name, cce.NonNull(ctype).Name); } else { -- cgit v1.2.3 From 2514560c58c60fa79850d12aee4cf2afeaedc5f5 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 29 Sep 2011 18:33:58 -0700 Subject: Dafny: beautification in one test case, and fixed an Answer file --- Test/dafny1/ExtensibleArray.dfy | 2 +- Test/dafny2/Answer | 2 -- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index 2dc49cd9..405f3e15 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -34,7 +34,7 @@ class ExtensibleArray { (forall i :: M <= i && i < length ==> Contents[i] == elements[i - M]) } - method Init() + constructor Init() modifies this; ensures Valid() && fresh(Repr - {this}); ensures Contents == []; diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index bef70cf1..d052c463 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -1,10 +1,8 @@ -------------------- SnapshotableTrees.dfy -------------------- -Dafny program verifier version 2.2.30705.1126, Copyright (c) 2003-2011, Microsoft. Dafny program verifier finished with 37 verified, 0 errors -------------------- TreeBarrier.dfy -------------------- -Dafny program verifier version 2.2.30705.1126, Copyright (c) 2003-2011, Microsoft. Dafny program verifier finished with 8 verified, 0 errors -- cgit v1.2.3 From c6b96cbc4f423acb60a5941ea0d58e1903faf675 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Fri, 30 Sep 2011 09:57:43 +0200 Subject: Dafny: Fixed the 'Answer' file for test 'dafny2'. --- Test/dafny2/Answer | 2 -- 1 file changed, 2 deletions(-) diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index bef70cf1..d052c463 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -1,10 +1,8 @@ -------------------- SnapshotableTrees.dfy -------------------- -Dafny program verifier version 2.2.30705.1126, Copyright (c) 2003-2011, Microsoft. Dafny program verifier finished with 37 verified, 0 errors -------------------- TreeBarrier.dfy -------------------- -Dafny program verifier version 2.2.30705.1126, Copyright (c) 2003-2011, Microsoft. Dafny program verifier finished with 8 verified, 0 errors -- cgit v1.2.3 From ad80221cf26f0a75c534548d6483c3f963b742cd Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 30 Sep 2011 16:03:43 -0700 Subject: Dafny: fixed bug in translator when LHS of a call was an array element or a nat --- Dafny/Translator.cs | 17 ++++++++++++++++- Test/dafny0/Answer | 14 +++++++++++++- Test/dafny0/Array.dfy | 21 +++++++++++++++++++++ 3 files changed, 50 insertions(+), 2 deletions(-) diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 3ec3c291..1e400599 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -3652,7 +3652,22 @@ namespace Microsoft.Dafny { } ProcessCallStmt(s.Tok, s.Receiver, actualReceiver, s.Method, s.Args, bLhss, lhsTypes, builder, locals, etran); for (int i = 0; i < lhsBuilders.Count; i++) { - lhsBuilders[i](bLhss[i], builder, etran); + var lhs = s.Lhs[i]; + Type lhsType = null; + if (lhs is IdentifierExpr) { + lhsType = lhs.Type; + } else if (lhs is FieldSelectExpr) { + var fse = (FieldSelectExpr)lhs; + lhsType = fse.Field.Type; + } + + Bpl.Expr bRhs = bLhss[i]; // the RHS (bRhs) of the assignment to the actual call-LHS (lhs) was a LHS (bLhss[i]) in the Boogie call statement + if (lhsType != null) { + CheckSubrange(lhs.tok, bRhs, lhsType, builder); + } + bRhs = etran.CondApplyBox(lhs.tok, bRhs, lhs.Type, lhsType); + + lhsBuilders[i](bRhs, builder, etran); } builder.Add(CaptureState(s.Tok)); } diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0c2e487a..a3e5e11f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -541,8 +541,20 @@ Array.dfy(183,1): Error BP5003: A postcondition might not hold on this return pa Array.dfy(182,11): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 +Array.dfy(198,10): Error: value assigned to a nat must be non-negative +Execution trace: + (0,0): anon0 + (0,0): anon5_Then + (0,0): anon2 + (0,0): anon6_Then +Array.dfy(199,5): Error: value assigned to a nat must be non-negative +Execution trace: + (0,0): anon0 + (0,0): anon5_Then + (0,0): anon2 + (0,0): anon6_Then -Dafny program verifier finished with 30 verified, 13 errors +Dafny program verifier finished with 31 verified, 15 errors -------------------- MultiDimArray.dfy -------------------- MultiDimArray.dfy(53,21): Error: assertion violation diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index 6699e648..613cdd83 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -182,3 +182,24 @@ ghost method Fill_None(s: seq) ensures forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j]; { // error: cannot prove postcondition } + +// -------------- some regression tests; there was a time when array-element LHSs of calls were not translated correctly + +method Test_ArrayElementLhsOfCall(a: array, i: int, c: Cdefg) returns (x: int) + requires a != null && c != null; + modifies a, c; +{ + if (0 <= i < a.Length) { + a[i] := x; + a[i] := Test_ArrayElementLhsOfCall(a, i-1, c); // this line used to crash Dafny + c.t := x; + c.t := Test_ArrayElementLhsOfCall(a, i-1, c); // this line used to crash Dafny + var n: nat; + n := x; // error: subrange check is applied and it cannot be verified + n := Test_ArrayElementLhsOfCall(a, i-1, c); // error: subrange check is applied and it cannot be verified + } +} + +class Cdefg { + var t: T; +} -- cgit v1.2.3 From 118cb0f58e5468b0801d2483875662831b8a82d6 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 30 Sep 2011 16:36:23 -0700 Subject: Dafny: Updated snapshotable tree to remove IsReadonly precondition for CreateIterator. --- Test/dafny2/SnapshotableTrees.dfy | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy index 0c31d8f3..3386b123 100644 --- a/Test/dafny2/SnapshotableTrees.dfy +++ b/Test/dafny2/SnapshotableTrees.dfy @@ -147,7 +147,7 @@ class Tree } method CreateIterator() returns (iter: Iterator) - requires Valid() && IsReadonly; + requires Valid(); // && IsReadonly; ensures iter != null && iter.Valid() && fresh(iter.IterRepr); ensures iter.T == this && iter.Contents == Contents && iter.N == -1; { @@ -459,3 +459,21 @@ class Iterator } datatype List = Nil | Cons(Node, List); + +/* The following method shows the problem of concurrent modifications and shows that the + * design of the snapshotable trees herein handle this correctly. That is, after inserting + * into a tree that is being iterated, use of the associated iterator can no longer be + * proved to be correct. + * +method TestConcurrentModification(t: Tree) + requires t != null && t.Valid() && !t.IsReadonly; + modifies t.MutableRepr; +{ + var it := t.CreateIterator(); + var more := it.MoveNext(); + if (more) { + var pos := t.Insert(52); // this modification of the collection renders all associated iterators invalid + more := it.MoveNext(); // error: operation t.Insert may have made this iterator invalid + } +} +*/ -- cgit v1.2.3