From d0411d08eba6e800509744dbb9e0b4c380964e9b Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 11 Jun 2010 02:02:36 +0000 Subject: Dafny: Added two additional heuristics for guessing missing loop decreases clauses (for loop guard A!=B and for loop guards with multiple conjuncts) --- Source/Dafny/Translator.ssc | 115 ++++++++++++++++++++++++++++++++-------- Test/VSI-Benchmarks/b1.dfy | 122 +++++++++++++++++++++---------------------- Test/VSI-Benchmarks/b2.dfy | 1 - Test/VSI-Benchmarks/b3.dfy | 2 - Test/VSI-Benchmarks/b8.dfy | 3 +- Test/dafny0/Answer | 68 ++++++++++++++++++------ Test/dafny0/Definedness.dfy | 3 -- Test/dafny0/SmallTests.dfy | 21 ++++++++ Test/dafny0/Termination.dfy | 58 +++++++++++++++++++- Test/dafny0/Use.dfy | 1 - Test/dafny1/SchorrWaite.dfy | 1 - Test/dafny1/Substitution.dfy | 1 - Test/vacid0/SparseArray.dfy | 2 - 13 files changed, 283 insertions(+), 115 deletions(-) diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index fd757b39..27103bd0 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -2047,25 +2047,58 @@ namespace Microsoft.Dafny { // use simple heuristics to create a default decreases clause, if none is given List theDecreases = s.Decreases; - if (theDecreases.Count == 0) { - Expression guess = null; - BinaryExpr bin = s.Guard as BinaryExpr; - if (bin != null) { - switch (bin.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.Lt: - case BinaryExpr.ResolvedOpcode.Le: - guess = IntSub(s.Tok, bin.E1, bin.E0); - break; - case BinaryExpr.ResolvedOpcode.Ge: - case BinaryExpr.ResolvedOpcode.Gt: - guess = IntSub(s.Tok, bin.E0, bin.E1); - break; - default: - break; + bool inferredDecreases = false; + if (theDecreases.Count == 0 && s.Guard != null) { + Expression prefix = null; + foreach (Expression guardConjunct in Conjuncts(s.Guard)) { + Expression guess = null; + BinaryExpr bin = guardConjunct as BinaryExpr; + if (bin != null) { + switch (bin.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Lt: + case BinaryExpr.ResolvedOpcode.Le: + // for A < B and A <= B, use the decreases B - A + guess = CreateIntSub(s.Tok, bin.E1, bin.E0); + break; + case BinaryExpr.ResolvedOpcode.Ge: + case BinaryExpr.ResolvedOpcode.Gt: + // for A >= B and A > B, use the decreases A - B + guess = CreateIntSub(s.Tok, bin.E0, bin.E1); + break; + case BinaryExpr.ResolvedOpcode.NeqCommon: + if (bin.E0.Type is IntType) { + // for A != B where A and B are integers, use the absolute difference between A and B (that is: if 0 <= A-B then A-B else B-A) + Expression AminusB = CreateIntSub(s.Tok, bin.E0, bin.E1); + Expression BminusA = CreateIntSub(s.Tok, bin.E1, bin.E0); + Expression zero = CreateIntLiteral(s.Tok, 0); + BinaryExpr test = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Le, zero, AminusB); + test.ResolvedOp = BinaryExpr.ResolvedOpcode.Le; // resolve here + test.Type = Type.Bool; // resolve here + guess = CreateIntITE(s.Tok, test, AminusB, BminusA); + } + break; + default: + break; + } + } + if (guess != null) { + if (prefix != null) { + // Make the following guess: if prefix then guess else -1 + Expression negativeOne = CreateIntLiteral(s.Tok, -1); + guess = CreateIntITE(s.Tok, prefix, guess, negativeOne); + } + theDecreases.Add(guess); + inferredDecreases = true; + break; // ignore any further conjuncts + } + if (prefix == null) { + prefix = guardConjunct; + } else { + BinaryExpr and = new BinaryExpr(s.Tok, BinaryExpr.Opcode.And, prefix, guardConjunct); + and.ResolvedOp = BinaryExpr.ResolvedOpcode.And; // resolve here + and.Type = Type.Bool; // resolve here + prefix = and; } - } - if (guess != null) { - theDecreases.Add(guess); } } @@ -2189,7 +2222,7 @@ namespace Microsoft.Dafny { decrs.Add(etran.TrExpr(e)); } Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, oldBfs, loopBodyBuilder, etran, " at end of loop iteration"); - loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, "decreases expression might not decrease")); + loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, inferredDecreases ? "cannot prove termination; try supplying a decreases clause for the loop" : "decreases expression might not decrease")); } Bpl.StmtList body = loopBodyBuilder.Collect(stmt.Tok); @@ -2368,15 +2401,53 @@ namespace Microsoft.Dafny { } } - static Expression! IntSub(Token! tok, Expression! e0, Expression! e1) + static Expression! CreateIntLiteral(Token! tok, int n) + { + if (0 <= n) { + Expression lit = new LiteralExpr(tok, n); + lit.Type = Type.Int; // resolve here + return lit; + } else { + return CreateIntSub(tok, CreateIntLiteral(tok, 0), CreateIntLiteral(tok, -n)); + } + } + + static Expression! CreateIntSub(Token! tok, Expression! e0, Expression! e1) requires e0.Type is IntType && e1.Type is IntType; { BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1); - s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub; - s.Type = Type.Int; + s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub; // resolve here + s.Type = Type.Int; // resolve here return s; } + static Expression! CreateIntITE(Token! tok, Expression! test, Expression! e0, Expression! e1) + requires test.Type is BoolType && e0.Type is IntType && e1.Type is IntType; + { + ITEExpr ite = new ITEExpr(tok, test, e0, e1); + ite.Type = Type.Int; // resolve here + return ite; + } + + public IEnumerable! Conjuncts(Expression! expr) + requires expr.Type is BoolType; + { + if (expr is BinaryExpr) { + BinaryExpr bin = (BinaryExpr)expr; + if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) { + foreach (Expression e in Conjuncts(bin.E0)) { + yield return e; + } + assert bin != null; // the necessity of this cast is a compiler bug, but perhaps an irrepairable one + foreach (Expression e in Conjuncts(bin.E1)) { + yield return e; + } + yield break; + } + } + yield return expr; + } + void CheckCallTermination(Token! tok, List! contextDecreases, List! calleeDecreases, Expression receiverReplacement, Dictionary! substMap, ExpressionTranslator! etran, Bpl.StmtListBuilder! builder) diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy index 1ab76a78..cd4a18c2 100644 --- a/Test/VSI-Benchmarks/b1.dfy +++ b/Test/VSI-Benchmarks/b1.dfy @@ -1,75 +1,71 @@ -// Note: To prove termination of calls, methods need -// a termination measure, but Dafny does not yet support -// termination measures for methods (but it will in -// the foreseeable future). - // Spec# and Boogie and Chalice: The program will be // the same, except that these languages do not check -// for any kind of termination. +// for any kind of termination. Also, in Spec#, there +// is an issue of potential overflows. + +// Benchmark1 -class Benchmark1 { - method Add(x: int, y: int) returns (r: int) - ensures r == x+y; - { - r := x; - if (y < 0) { - var n := y; - while (n != 0) - invariant r == x+y-n && 0 <= -n; - decreases -n; - { - r := r - 1; - n := n + 1; - } - } else { - var n := y; - while (n != 0) - invariant r == x+y-n && 0 <= n; - decreases n; - { - r := r + 1; - n := n - 1; - } +method Add(x: int, y: int) returns (r: int) + ensures r == x+y; +{ + r := x; + if (y < 0) { + var n := y; + while (n != 0) + invariant r == x+y-n && 0 <= -n; + { + r := r - 1; + n := n + 1; + } + } else { + var n := y; + while (n != 0) + invariant r == x+y-n && 0 <= n; + { + r := r + 1; + n := n - 1; } } +} - method Mul(x: int, y: int) returns (r: int) - ensures r == x*y; - decreases x < 0, x; - { - if (x == 0) { - r := 0; - } else if (x < 0) { - call r := Mul(-x, y); - r := -r; - } else { - call r := Mul(x-1, y); - call r := Add(r, y); - } +method Mul(x: int, y: int) returns (r: int) + ensures r == x*y; + decreases x < 0, x; +{ + if (x == 0) { + r := 0; + } else if (x < 0) { + call r := Mul(-x, y); + r := -r; + } else { + call r := Mul(x-1, y); + call r := Add(r, y); } +} - method Main() { - call TestAdd(3, 180); - call TestAdd(3, -180); - call TestAdd(0, 1); +// --------------------------- - call TestMul(3, 180); - call TestMul(3, -180); - call TestMul(180, 3); - call TestMul(-180, 3); - call TestMul(0, 1); - call TestMul(1, 0); - } +method Main() { + call TestAdd(3, 180); + call TestAdd(3, -180); + call TestAdd(0, 1); - method TestAdd(x: int, y: int) { - print x, " + ", y, " = "; - call z := Add(x, y); - print z, "\n"; - } + call TestMul(3, 180); + call TestMul(3, -180); + call TestMul(180, 3); + call TestMul(-180, 3); + call TestMul(0, 1); + call TestMul(1, 0); +} - method TestMul(x: int, y: int) { - print x, " * ", y, " = "; - call z := Mul(x, y); - print z, "\n"; - } +method TestAdd(x: int, y: int) { + print x, " + ", y, " = "; + call z := Add(x, y); + print z, "\n"; +} + +method TestMul(x: int, y: int) { + print x, " * ", y, " = "; + call z := Mul(x, y); + print z, "\n"; } diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index fd20a72b..1021ee85 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -14,7 +14,6 @@ class Benchmark2 { invariant 0 <= low && low <= high && high <= |a|; invariant (forall i :: 0 <= i && i < low ==> a[i] < key); invariant (forall i :: high <= i && i < |a| ==> key < a[i]); - decreases high - low; { var mid := low + (high - low) / 2; var midVal := a[mid]; diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 6d9c3ddd..d9acfe04 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -88,8 +88,6 @@ class Benchmark3 { // the current array is that permutation of the input array invariant (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]); invariant (forall i: int :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]); - - decreases |q.contents|; { call m,k := RemoveMin(q); perm := perm + [p[k]]; //adds index of min to perm diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index 34e0cfef..a37f86e4 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -78,14 +78,13 @@ class Glossary { var wr := new WriterStream; call wr.Create(); - while (0<|q.contents|) + while (0 < |q.contents|) invariant wr.Valid() && fresh(wr.footprint); invariant glossary.Valid(); invariant glossary !in wr.footprint && null !in glossary.keys; invariant (forall d :: d in glossary.values ==> null !in d); invariant q !in wr.footprint; invariant (forall k :: k in q.contents ==> k in glossary.keys); - decreases |q.contents|; { call term := q.Dequeue(); call present,definition := glossary.Find(term); diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index cc248c20..7456ffaa 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -101,26 +101,26 @@ Execution trace: SmallTests.dfy(81,5): anon7_LoopHead (0,0): anon7_LoopBody (0,0): anon8_Then -SmallTests.dfy(95,5): Error: call may violate caller's modifies clause +SmallTests.dfy(116,5): Error: call may violate caller's modifies clause Execution trace: (0,0): anon0 (0,0): anon4_Else (0,0): anon3 -SmallTests.dfy(108,7): Error: call may violate caller's modifies clause +SmallTests.dfy(129,7): Error: call may violate caller's modifies clause Execution trace: (0,0): anon0 (0,0): anon3_Then -SmallTests.dfy(110,7): Error: call may violate caller's modifies clause +SmallTests.dfy(131,7): Error: call may violate caller's modifies clause Execution trace: (0,0): anon0 (0,0): anon3_Else -SmallTests.dfy(150,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause +SmallTests.dfy(171,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause Execution trace: (0,0): anon0 (0,0): anon4_Else (0,0): anon3 -Dafny program verifier finished with 24 verified, 9 errors +Dafny program verifier finished with 28 verified, 9 errors -------------------- Definedness.dfy -------------------- Definedness.dfy(8,7): Error: possible division by zero @@ -226,7 +226,7 @@ Execution trace: (0,0): anon16_LoopBody Definedness.dfy(151,5): anon17_Else (0,0): anon9 -Definedness.dfy(172,44): Error: loop invariant must be well defined +Definedness.dfy(170,44): Error: loop invariant must be well defined Execution trace: (0,0): anon0 Definedness.dfy(162,5): anon16_LoopHead @@ -235,28 +235,28 @@ Execution trace: (0,0): anon3 (0,0): anon18_Then (0,0): anon6 - Definedness.dfy(170,5): anon19_LoopHead + Definedness.dfy(169,5): anon19_LoopHead (0,0): anon19_LoopBody (0,0): anon20_Then -Definedness.dfy(193,21): Error: collection expression must be well defined +Definedness.dfy(191,21): Error: collection expression must be well defined Execution trace: (0,0): anon0 -Definedness.dfy(195,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause +Definedness.dfy(193,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause Execution trace: (0,0): anon0 -Definedness.dfy(197,33): Error: range expression must be well defined +Definedness.dfy(195,33): Error: range expression must be well defined Execution trace: (0,0): anon0 -Definedness.dfy(203,18): Error: RHS of assignment must be well defined +Definedness.dfy(201,18): Error: RHS of assignment must be well defined Execution trace: (0,0): anon0 -Definedness.dfy(212,23): Error: loop invariant must be well defined +Definedness.dfy(210,23): Error: loop invariant must be well defined Execution trace: (0,0): anon0 - Definedness.dfy(210,5): anon7_LoopHead + Definedness.dfy(208,5): anon7_LoopHead (0,0): anon7_LoopBody (0,0): anon8_Then -Definedness.dfy(212,23): Error BP5004: This loop invariant might not hold on entry. +Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry. Execution trace: (0,0): anon0 @@ -335,8 +335,44 @@ Execution trace: Dafny program verifier finished with 2 verified, 1 error -------------------- Termination.dfy -------------------- +Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop +Execution trace: + (0,0): anon0 + Termination.dfy(102,3): anon7_LoopHead + (0,0): anon7_LoopBody + Termination.dfy(102,3): anon8_Else + (0,0): anon3 + Termination.dfy(102,12): anon9_Else + (0,0): anon5 +Termination.dfy(110,3): Error: cannot prove termination; try supplying a decreases clause for the loop +Execution trace: + (0,0): anon0 + Termination.dfy(110,3): anon7_LoopHead + (0,0): anon7_LoopBody + Termination.dfy(110,3): anon8_Else + (0,0): anon3 + Termination.dfy(110,16): anon9_Else + (0,0): anon5 +Termination.dfy(119,3): Error: decreases expression might not decrease +Execution trace: + (0,0): anon0 + Termination.dfy(119,3): anon7_LoopHead + (0,0): anon7_LoopBody + Termination.dfy(119,3): anon8_Else + (0,0): anon3 + Termination.dfy(119,16): anon9_Else + (0,0): anon5 +Termination.dfy(120,17): Error: decreases expression must be bounded below by 0 at end of loop iteration +Execution trace: + (0,0): anon0 + Termination.dfy(119,3): anon7_LoopHead + (0,0): anon7_LoopBody + Termination.dfy(119,3): anon8_Else + (0,0): anon3 + Termination.dfy(119,16): anon9_Else + (0,0): anon5 -Dafny program verifier finished with 13 verified, 0 errors +Dafny program verifier finished with 22 verified, 4 errors -------------------- Use.dfy -------------------- Use.dfy(16,18): Error: assertion violation @@ -363,7 +399,7 @@ Execution trace: Use.dfy(138,5): Error: assertion violation Execution trace: (0,0): anon0 -Use.dfy(209,19): Error: assertion violation +Use.dfy(208,19): Error: assertion violation Execution trace: (0,0): anon0 diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index b69fa4f6..d557de21 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -161,14 +161,12 @@ class StatementTwoShoes { var i := 0; while (i < 100) invariant i <= 100; - decreases 100 - i; invariant F(123 - i) == this; { i := i + 1; } i := 0; while (i < 100) - decreases 100 - i; invariant F(if i==77 then -3 else i) == this; // error: expression may not be well defined { i := i + 1; @@ -210,7 +208,6 @@ class StatementTwoShoes { while (i < 100) // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking invariant 5 / x != 5 / x; // error: not well-defined, and error: loop invariant does not hold initially - decreases 100 - i; { i := i + 1; } diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 4e3fab69..87bfd35f 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -85,6 +85,27 @@ class Modifies { } } + method Aprime(p: Modifies) + modifies this, p; + { + x := x + 1; + while (p != null && p.x < 75) + decreases if p != null then 75 - p.x else 0; // given explicitly (but see Adoubleprime below) + { + p.x := p.x + 1; + } + } + + method Adoubleprime(p: Modifies) + modifies this, p; + { + x := x + 1; + while (p != null && p.x < 75) // here, the decreases clause is heuristically inferred (to be the + { // same as the one in Aprime above) + p.x := p.x + 1; + } + } + method B(p: Modifies) modifies this; { diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 39361b7b..27004653 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -5,7 +5,7 @@ class Termination { var i := 0; while (i < N) invariant i <= N; - decreases N - i; + // this will be heuristically inferred: decreases N - i; { i := i + 1; } @@ -95,3 +95,59 @@ datatype List { Nil; Cons(T, List); } + +method FailureToProveTermination0(N: int) +{ + var n := N; + while (n < 100) { // error: may not terminate + n := n - 1; + } +} + +method FailureToProveTermination1(x: int, y: int, N: int) +{ + var n := N; + while (x < y && n < 100) // error: cannot prove termination from the heuristically chosen termination metric + { + n := n + 1; + } +} + +method FailureToProveTermination2(x: int, y: int, N: int) +{ + var n := N; + while (x < y && n < 100) // error: cannot prove termination from the given (bad) termination metric + decreases n - x; + { + n := n + 1; + } +} + +method FailureToProveTermination3(x: int, y: int, N: int) +{ + var n := N; + while (x < y && n < 100) + decreases 100 - n; + { + n := n + 1; + } +} + +method FailureToProveTermination4(x: int, y: int, N: int) +{ + var n := N; + while (n < 100 && x < y) + decreases 100 - n; + { + n := n + 1; + } +} + +method FailureToProveTermination5(b: bool, N: int) +{ + var n := N; + while (b && n < 100) // here, the heuristics are good enough to prove termination + { + n := n + 1; + } +} diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy index aaf41190..20928f41 100644 --- a/Test/dafny0/Use.dfy +++ b/Test/dafny0/Use.dfy @@ -191,7 +191,6 @@ class Recursive { while (k < n) invariant k <= n; invariant Gauss(k) == (k+1)*k / 2; - decreases n - k; { k := k + 1; } diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index a46e83a3..3e64a4bd 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -64,7 +64,6 @@ class Main { invariant (forall n :: n in S ==> n.childrenVisited == old(n.childrenVisited) && n.children == old(n.children)); - decreases |root.children| - i; { var c := root.children[i]; if (c != null) { diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index 72415fea..9e4da459 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -96,7 +96,6 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) while (j < N) invariant j <= N; invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]); - decreases N - j; { call TheoremSeq(args[j], v, val); j := j + 1; diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy index da1f63bb..0e6aff05 100644 --- a/Test/vacid0/SparseArray.dfy +++ b/Test/vacid0/SparseArray.dfy @@ -55,7 +55,6 @@ class SparseArray { // TODO: why doesn't this work instead of the next line? invariant (forall x :: x in s ==> x == zero); invariant (forall i :: 0 <= i && i < |s| ==> s[i] == zero); invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i); - decreases N - k; { s := s + [zero]; id := id + [k]; @@ -110,7 +109,6 @@ class SparseArray { var i := 0; while (i < n) invariant i <= n && |arr| == i; - decreases n - i; { var g: G; arr := arr + [g]; -- cgit v1.2.3