From 27120ddc7adb3a0c789c1ee784d73a4be08de118 Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 5 Oct 2015 08:59:16 -0700 Subject: Implemented resolution, verification, and (poorly performing) compilation of existential if guards. Fixed bugs in ghost checks involving comprehensions and attributes. Added SubstituteBoundedPool method. --- Test/dafny0/Compilation.dfy | 35 ++++- Test/dafny0/Compilation.dfy.expect | 13 +- Test/dafny0/ExistentialGuards.dfy | 86 ++++++++++- Test/dafny0/ExistentialGuards.dfy.expect | 111 ++++++++++++-- Test/dafny0/ExistentialGuardsResolution.dfy | 154 +++++++++++++++++++ Test/dafny0/ExistentialGuardsResolution.dfy.expect | 167 +++++++++++++++++++++ Test/dafny0/ResolutionErrors.dfy | 20 +++ Test/dafny0/ResolutionErrors.dfy.expect | 7 +- 8 files changed, 571 insertions(+), 22 deletions(-) create mode 100644 Test/dafny0/ExistentialGuardsResolution.dfy create mode 100644 Test/dafny0/ExistentialGuardsResolution.dfy.expect (limited to 'Test') diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index a2b96996..7f9169da 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny "%s" > "%t" +// RUN: %dafny /compile:3 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // The tests in this file are designed to run through the compiler. They contain @@ -43,6 +43,8 @@ module CoRecursion { // 40 // 41 // 42 + // 9 + // 9 method Main() { var m := 17; var cell := new Cell; @@ -58,6 +60,37 @@ module CoRecursion { print l.car, "\n"; l := l.cdr; } + var nio := OneLess(0, 10); + print nio, "\n"; + nio := OneLess'(0, 10); + print nio, "\n"; + } + + method OneLess(lo: int, hi: int) returns (m: int) + requires lo < hi + // This method ensures m == hi - 1, but we don't care to prove it + decreases hi - lo + { + if y :| lo < y < hi { + m := OneLess(y, hi); + } else { + m := lo; + } + } + + method OneLess'(lo: int, hi: int) returns (m: int) + requires lo < hi + // This method ensures m == hi - 1, but we don't care to prove it + decreases hi - lo + { + if { + case y :| lo < y < hi => + m := OneLess'(y, hi); + case lo+1 < hi => + m := OneLess'(lo+1, hi); + case lo + 1 == hi => + m := lo; + } } } diff --git a/Test/dafny0/Compilation.dfy.expect b/Test/dafny0/Compilation.dfy.expect index 0a1938ae..2b76b107 100644 --- a/Test/dafny0/Compilation.dfy.expect +++ b/Test/dafny0/Compilation.dfy.expect @@ -1,3 +1,12 @@ -Dafny program verifier finished with 46 verified, 0 errors -Compiled assembly into Compilation.exe +Dafny program verifier finished with 50 verified, 0 errors +Program compiled successfully +Running... + +400 +320 +40 +41 +42 +9 +9 diff --git a/Test/dafny0/ExistentialGuards.dfy b/Test/dafny0/ExistentialGuards.dfy index 001acb55..5afb3979 100644 --- a/Test/dafny0/ExistentialGuards.dfy +++ b/Test/dafny0/ExistentialGuards.dfy @@ -2,12 +2,19 @@ // RUN: %diff "%s.expect" "%t" predicate P(n: int) +{ + n % 2 == 0 +} predicate R(r: real) +{ + 0.0 <= r +} method M0() { if x :| P(x) { + var y := x + 3; } } @@ -19,13 +26,19 @@ method M1() method M2() { - if x, y :| P(x) && R(y) { + var x := true; + if x, y :| P(x) && R(y) { // this declares a new 'x' + var z := x + 12; } + x := x && false; } method M3() { + var x := true; if x: int, y :| P(x) && R(y) { + var z := x + y.Trunc; + var w := real(x) + y; } } @@ -53,37 +66,94 @@ method M6() } } -method M7() +ghost method M7() returns (z: real, w: real) + ensures -2.0 <= z + ensures z == w // error: does not hold { + var k; if x :| P(x) { + k, z := 4, 18.0; } else if * { + z := z + -z; } else if y :| R(y) { + z := y; } else if y :| P(y) { + k := y; + } else { + z :| R(z); + } + if P(k) { + z := 18.0; + } +} + +ghost method M8(m: int, n: int) + requires forall y :: m <= y < n ==> P(y) +{ + var t := -1; + var u; + if y :| m <= y < n && P(y) { + u := y; + if * { + t := n - y; + } else if * { + t := y - m; + } else if P(y) { + t := 8; + } else { + t := -100; // will never happen + } + } + if t < 0 && m < n { + assert P(m) && !P(m); + assert false; } + assert t < 0 ==> n <= m; } method P0(m: int, n: int) requires m < n { + ghost var even, alsoEven := 4, 8; if { case x :| P(x) => + even := x; case x: int :| P(x) => + even := x; case x, y :| P(x) && R(y) => + even, alsoEven := x, y.Trunc; // this assigns to 'alsoEven' a possibly odd number case x: int, y :| P(x) && R(y) => + even := x; case m < n => // just to be different case x, y: real :| P(x) && R(y) => + even := x; case x: int, y: real :| P(x) && R(y) => + even := x; } + assert P(even); + assert P(alsoEven); // error: may not hold } method P1(m: int, n: int) - requires m < n { + if { // error: missing case + case x :| m <= x < n && P(x) => + } +} + +method P2(m: int, n: int) + requires forall y :: m <= y < n ==> P(y) +{ + if { // error: missing case + case x :| m <= x < n && P(x) => + } +} + +method P3(m: int, n: int) + requires m < n && forall y :: m <= y < n ==> P(y) +{ + assert P(m); // lemma that proves that the following 'if' covers all possibilities if { - case x {:myattribute x, "hello"} :| P(x) => - case x, y {:myattribute y, "sveika"} :| P(x) && R(y) => - case x: int {:myattribute x, "chello"} :| P(x) => - case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) => - case m < n => + case x :| m <= x < n && P(x) => } } diff --git a/Test/dafny0/ExistentialGuards.dfy.expect b/Test/dafny0/ExistentialGuards.dfy.expect index cf229553..21461067 100644 --- a/Test/dafny0/ExistentialGuards.dfy.expect +++ b/Test/dafny0/ExistentialGuards.dfy.expect @@ -3,12 +3,19 @@ // ExistentialGuards.dfy predicate P(n: int) +{ + n % 2 == 0 +} predicate R(r: real) +{ + 0.0 <= r +} method M0() { if x :| P(x) { + var y := x + 3; } } @@ -20,13 +27,19 @@ method M1() method M2() { + var x := true; if x, y :| P(x) && R(y) { + var z := x + 12; } + x := x && false; } method M3() { + var x := true; if x: int, y :| P(x) && R(y) { + var z := x + y.Trunc; + var w := real(x) + y; } } @@ -54,41 +67,119 @@ method M6() } } -method M7() +ghost method M7() returns (z: real, w: real) + ensures -2.0 <= z + ensures z == w { + var k; if x :| P(x) { + k, z := 4, 18.0; } else if * { + z := z + -z; } else if y :| R(y) { + z := y; } else if y :| P(y) { + k := y; + } else { + z :| R(z); + } + if P(k) { + z := 18.0; } } +ghost method M8(m: int, n: int) + requires forall y :: m <= y < n ==> P(y) +{ + var t := -1; + var u; + if y :| m <= y < n && P(y) { + u := y; + if * { + t := n - y; + } else if * { + t := y - m; + } else if P(y) { + t := 8; + } else { + t := -100; + } + } + if t < 0 && m < n { + assert P(m) && !P(m); + assert false; + } + assert t < 0 ==> n <= m; +} + method P0(m: int, n: int) requires m < n { + ghost var even, alsoEven := 4, 8; if { case x :| P(x) => + even := x; case x: int :| P(x) => + even := x; case x, y :| P(x) && R(y) => + even, alsoEven := x, y.Trunc; case x: int, y :| P(x) && R(y) => + even := x; case m < n => case x, y: real :| P(x) && R(y) => + even := x; case x: int, y: real :| P(x) && R(y) => + even := x; } + assert P(even); + assert P(alsoEven); } method P1(m: int, n: int) - requires m < n { if { - case x {:myattribute x, "hello"} :| P(x) => - case x, y {:myattribute y, "sveika"} :| P(x) && R(y) => - case x: int {:myattribute x, "chello"} :| P(x) => - case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) => - case m < n => + case x :| m <= x < n && P(x) => + } +} + +method P2(m: int, n: int) + requires forall y :: m <= y < n ==> P(y) +{ + if { + case x :| m <= x < n && P(x) => + } +} + +method P3(m: int, n: int) + requires m < n && forall y :: m <= y < n ==> P(y) +{ + assert P(m); + if { + case x :| m <= x < n && P(x) => } } +ExistentialGuards.dfy(85,10): Error BP5003: A postcondition might not hold on this return path. +ExistentialGuards.dfy(71,12): Related location: This is the postcondition that might not hold. +Execution trace: + (0,0): anon0 + (0,0): anon12_Then + (0,0): anon9 + (0,0): anon16_Then +ExistentialGuards.dfy(134,9): Error: assertion violation +ExistentialGuards.dfy(6,8): Related location +Execution trace: + (0,0): anon0 + (0,0): anon20_Then + (0,0): anon21_Then + (0,0): anon5 + (0,0): anon17 +ExistentialGuards.dfy(139,2): Error: alternative cases fail to cover all possibilties +Execution trace: + (0,0): anon0 + (0,0): anon7_Else +ExistentialGuards.dfy(147,2): Error: alternative cases fail to cover all possibilties +Execution trace: + (0,0): anon0 + (0,0): anon7_Else -Dafny program verifier finished with 22 verified, 0 errors -Compilation error: Function _module._default.P has no body -Compilation error: Function _module._default.R has no body +Dafny program verifier finished with 24 verified, 4 errors diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy b/Test/dafny0/ExistentialGuardsResolution.dfy new file mode 100644 index 00000000..8fce1de5 --- /dev/null +++ b/Test/dafny0/ExistentialGuardsResolution.dfy @@ -0,0 +1,154 @@ +// RUN: %dafny /dprint:- "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +predicate P(n: int) + +predicate R(r: real) + +method M0() +{ + if x :| P(x) { + var y := x + 3; + var x := true; // error: 'x' is already declared in this scope + } +} + +method M1() +{ + if x: int :| P(x) { + x := x + 1; // error: 'x' is an immutable variable + } +} + +method M2() +{ + var x := true; + if x, y :| P(x) && R(y) { // this declares a new 'x' + var z := x + 12; + } + x := x && false; +} + +method M3() +{ + var x := true; + if x: int, y :| P(x) && R(y) { + var z := x + int(y); + var w := real(x) + y; + } + var x := 0.0; // error: 'x' is already declared in this scope +} + +method M4() +{ + if x, y: real :| P(x) && R(y) { + } +} + +method M5() +{ + if x: int, y: real :| P(x) && R(y) { + } +} + +method M6() +{ + if x {:myattribute x, "hello"} :| P(x) { + } + if x, y {:myattribute y, "sveika"} :| P(x) && R(y) { + } + if x: int {:myattribute x, "chello"} :| P(x) { + } + if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) { + } +} + +method M7() +{ + if x :| P(x) { + } else if * { + } else if y :| R(y) { + } else if y :| P(y) { + } +} + +method P0(m: int, n: int) + requires m < n +{ + var x := true; + if { + case x :| P(x) => + var t := 3 * x; + case x: int :| P(x) => + case x, y :| P(x) && R(y) => + y := y + 1.0; // error: 'y' is an immutable variable + case x: int, y :| P(x) && R(y) => + case m < n => + x := x || m + 5 == n; + case x, y: real :| P(x) && R(y) => + case x: int, y: real :| P(x) && R(y) => + } + assert x; +} + +method P1(m: int, n: int) + requires m < n +{ + if { + case x {:myattribute x, "hello"} :| P(x) => + case x, y {:myattribute y, "sveika"} :| P(x) && R(y) => + case x: int {:myattribute x, "chello"} :| P(x) => + case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) => + case m < n => + } +} + +module TypesNotFullyDetermined { + method T0() + { + if x :| true { // error: type not entirely resolved + } + } + method T1() + { + if x :| true { + var y := x + 3; + } + } +} + +module Ghost { + predicate P(x: int) // note, P is ghost + predicate method R(x: int) + method M7() returns (z: int, b: bool) + { + if * { + z := z + -z; + } else if y :| 1000 <= y < 2000 && R(y) { + z := y; + } else if y :| 0 <= y < 100 && P(y) { + z := y; // error: not allowed, because the P in the guard makes this a ghost context + } else if y :| 0 <= y < 100 && R(y) { + z := y; // error: this is also in a ghost context, because it depends on the P above + } + + if * { + z := z + -z; + } else if exists y :: 1000 <= y < 2000 && R(y) { + z := 0; + } else if exists y :: 0 <= y < 100 && P(y) { + z := 0; // error: not allowed, because the P in the guard makes this a ghost context + } else if exists y :: 0 <= y < 100 && R(y) { + z := 0; // error: this is also in a ghost context, because it depends on the P above + } + + if P(z) { + z := 20; // error: blatant ghost context + } + + b := exists y :: 0 <= y < 100 && P(y); // error: assignment to non-ghost of something that depends on ghost + ghost var c; + c := exists y :: 0 <= y < 100 && P(y); + b := exists y {:myattribute P(y)} :: 0 <= y < 100; + } +} diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy.expect b/Test/dafny0/ExistentialGuardsResolution.dfy.expect new file mode 100644 index 00000000..681bb13d --- /dev/null +++ b/Test/dafny0/ExistentialGuardsResolution.dfy.expect @@ -0,0 +1,167 @@ +// Dafny program verifier version 1.9.5.20511, Copyright (c) 2003-2015, Microsoft. +// Command Line Options: -nologo -countVerificationErrors:0 -useBaseNameForFileName /dprint:- C:\dafny\Test\dafny0\ExistentialGuardsResolution.dfy +// ExistentialGuardsResolution.dfy + + +module TypesNotFullyDetermined { + method T0() + { + if x :| true { + } + } + + method T1() + { + if x :| true { + var y := x + 3; + } + } +} + +module Ghost { + predicate P(x: int) + + predicate method R(x: int) + + method M7() returns (z: int, b: bool) + { + if * { + z := z + -z; + } else if y :| 1000 <= y < 2000 && R(y) { + z := y; + } else if y :| 0 <= y < 100 && P(y) { + z := y; + } else if y :| 0 <= y < 100 && R(y) { + z := y; + } + if * { + z := z + -z; + } else if exists y :: 1000 <= y < 2000 && R(y) { + z := 0; + } else if exists y :: 0 <= y < 100 && P(y) { + z := 0; + } else if exists y :: 0 <= y < 100 && R(y) { + z := 0; + } + if P(z) { + z := 20; + } + b := exists y :: 0 <= y < 100 && P(y); + ghost var c; + c := exists y :: 0 <= y < 100 && P(y); + b := exists y {:myattribute P(y)} :: 0 <= y < 100; + } +} +predicate P(n: int) + +predicate R(r: real) + +method M0() +{ + if x :| P(x) { + var y := x + 3; + var x := true; + } +} + +method M1() +{ + if x: int :| P(x) { + x := x + 1; + } +} + +method M2() +{ + var x := true; + if x, y :| P(x) && R(y) { + var z := x + 12; + } + x := x && false; +} + +method M3() +{ + var x := true; + if x: int, y :| P(x) && R(y) { + var z := x + int(y); + var w := real(x) + y; + } + var x := 0.0; +} + +method M4() +{ + if x, y: real :| P(x) && R(y) { + } +} + +method M5() +{ + if x: int, y: real :| P(x) && R(y) { + } +} + +method M6() +{ + if x {:myattribute x, "hello"} :| P(x) { + } + if x, y {:myattribute y, "sveika"} :| P(x) && R(y) { + } + if x: int {:myattribute x, "chello"} :| P(x) { + } + if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) { + } +} + +method M7() +{ + if x :| P(x) { + } else if * { + } else if y :| R(y) { + } else if y :| P(y) { + } +} + +method P0(m: int, n: int) + requires m < n +{ + var x := true; + if { + case x :| P(x) => + var t := 3 * x; + case x: int :| P(x) => + case x, y :| P(x) && R(y) => + y := y + 1.0; + case x: int, y :| P(x) && R(y) => + case m < n => + x := x || m + 5 == n; + case x, y: real :| P(x) && R(y) => + case x: int, y: real :| P(x) && R(y) => + } + assert x; +} + +method P1(m: int, n: int) + requires m < n +{ + if { + case x {:myattribute x, "hello"} :| P(x) => + case x, y {:myattribute y, "sveika"} :| P(x) && R(y) => + case x: int {:myattribute x, "chello"} :| P(x) => + case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) => + case m < n => + } +} +ExistentialGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly +ExistentialGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ExistentialGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ExistentialGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ExistentialGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ExistentialGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ExistentialGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') +ExistentialGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x +ExistentialGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable +ExistentialGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x +ExistentialGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable +11 resolution/type errors detected in ExistentialGuardsResolution.dfy diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index e935c83d..58ba6701 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1692,3 +1692,23 @@ module LoopResolutionTests { } } } + +module UnderspecifiedTypesInAttributes { + function method P(x: T): int + method M() { + var {:myattr var u :| true; 6} v: int; // error: type of u is underspecified + var j {:myattr var u :| true; 6} :| 0 <= j < 100; // error: type of u is underspecified + + var a := new int[100]; + forall lp {:myattr var u :| true; 6} | 0 <= lp < 100 { // error: type of u is underspecified + a[lp] := 0; + } + + modify {:myattr P(10)} {:myattr var u :| true; 6} a; // error: type of u is underspecified + + calc {:myattr P(10)} {:myattr var u :| true; 6} // error: type of u is underspecified + { + 5; + } + } +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index be19eeac..b055184f 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -161,6 +161,11 @@ ResolutionErrors.dfy(1673,4): Error: 'decreases *' is not allowed on ghost loops ResolutionErrors.dfy(1677,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) ResolutionErrors.dfy(1687,4): Error: 'decreases *' is not allowed on ghost loops ResolutionErrors.dfy(1691,29): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ResolutionErrors.dfy(1699,17): Error: the type of the bound variable 'u' could not be determined +ResolutionErrors.dfy(1700,19): Error: the type of the bound variable 'u' could not be determined +ResolutionErrors.dfy(1703,23): Error: the type of the bound variable 'u' could not be determined +ResolutionErrors.dfy(1707,36): Error: the type of the bound variable 'u' could not be determined +ResolutionErrors.dfy(1709,34): Error: the type of the bound variable 'u' could not be determined ResolutionErrors.dfy(469,2): Error: More than one anonymous constructor ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny') @@ -224,4 +229,4 @@ ResolutionErrors.dfy(1123,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1144,13): Error: first argument to / must be of numeric type (instead got set) ResolutionErrors.dfy(1151,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating ResolutionErrors.dfy(1166,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating -226 resolution/type errors detected in ResolutionErrors.dfy +231 resolution/type errors detected in ResolutionErrors.dfy -- cgit v1.2.3