From 8bed69a4867c6e613cd06838f76d4e7985afd8b5 Mon Sep 17 00:00:00 2001 From: Josua Stuck Date: Tue, 6 Jul 2021 15:53:48 +0200 Subject: [PATCH 1/6] add FailureContext to Silver --- .../silver/verifier/VerificationError.scala | 20 +++++++++---------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala index 13200549f..2e1bd432f 100644 --- a/src/main/scala/viper/silver/verifier/VerificationError.scala +++ b/src/main/scala/viper/silver/verifier/VerificationError.scala @@ -154,17 +154,15 @@ trait ErrorMessage { trait VerificationError extends AbstractError with ErrorMessage { def reason: ErrorReason def readableMessage(withId: Boolean = false, withPosition: Boolean = false): String - override def readableMessage : String = { - val rm : String = readableMessage(false, true) - if (counterexample.isDefined){ - rm + "\n" + counterexample.get.toString - }else{ - rm - } - } + override def readableMessage : String = (readableMessage(false, true) + failureContexts.map(e => e.toString).mkString("\n")) def loggableMessage: String = s"$fullId-$pos" + (if (cached) "-cached" else "") def fullId = s"$id:${reason.id}" - var counterexample : Option[Counterexample] = None + var failureContexts: Seq[FailureContext] = Seq() //TODO: make immutable + +} +trait FailureContext { + def counterExample: Option[Counterexample] + def toString: String } /// used when an error/reason has no sensible node to use @@ -230,8 +228,8 @@ abstract class AbstractVerificationError extends VerificationError { val reasonT = errorT.reason.offendingNode.transformReason(errorT.reason) val res = errorT.withReason(reasonT) - res.counterexample = counterexample - res.branchConditions = branchConditions + res.failureContexts = failureContexts +// res.counterexample = counterexample res } From 6001a500ef8fb19117ce4e32cc186883a19e178c Mon Sep 17 00:00:00 2001 From: Josua Stuck Date: Tue, 6 Jul 2021 15:55:30 +0200 Subject: [PATCH 2/6] remove unneeded comment --- src/main/scala/viper/silver/verifier/VerificationError.scala | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala index 2e1bd432f..dafac60fe 100644 --- a/src/main/scala/viper/silver/verifier/VerificationError.scala +++ b/src/main/scala/viper/silver/verifier/VerificationError.scala @@ -229,7 +229,6 @@ abstract class AbstractVerificationError extends VerificationError { val res = errorT.withReason(reasonT) res.failureContexts = failureContexts -// res.counterexample = counterexample res } From c7ae6e831cf32fb8b39b783386ae53893fcc2a92 Mon Sep 17 00:00:00 2001 From: Josua Stuck Date: Mon, 12 Jul 2021 20:59:09 +0200 Subject: [PATCH 3/6] cosmetic changes --- src/main/scala/viper/silver/verifier/VerificationError.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala index dafac60fe..433a9c65b 100644 --- a/src/main/scala/viper/silver/verifier/VerificationError.scala +++ b/src/main/scala/viper/silver/verifier/VerificationError.scala @@ -154,12 +154,13 @@ trait ErrorMessage { trait VerificationError extends AbstractError with ErrorMessage { def reason: ErrorReason def readableMessage(withId: Boolean = false, withPosition: Boolean = false): String - override def readableMessage : String = (readableMessage(false, true) + failureContexts.map(e => e.toString).mkString("\n")) + override def readableMessage: String = readableMessage(false, true) + failureContexts.map(e => e.toString).mkString("\n") def loggableMessage: String = s"$fullId-$pos" + (if (cached) "-cached" else "") def fullId = s"$id:${reason.id}" var failureContexts: Seq[FailureContext] = Seq() //TODO: make immutable } + trait FailureContext { def counterExample: Option[Counterexample] def toString: String From 8be7f1525fc1ed76355e69c831346b06c0b93a29 Mon Sep 17 00:00:00 2001 From: Josua Stuck Date: Sun, 5 Sep 2021 19:33:37 +0200 Subject: [PATCH 4/6] Revert "fix test annotations for carbon/issue/388" This reverts commit 23d52ed5886fcd34ce8842dcaf0f8fb958bf78d4. --- .../resources/all/issues/silicon/0083.vpr | 76 ++++++++++--------- 1 file changed, 39 insertions(+), 37 deletions(-) diff --git a/src/test/resources/all/issues/silicon/0083.vpr b/src/test/resources/all/issues/silicon/0083.vpr index 7d1126b18..0b3f55408 100644 --- a/src/test/resources/all/issues/silicon/0083.vpr +++ b/src/test/resources/all/issues/silicon/0083.vpr @@ -1,37 +1,39 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -field f: Int - -method test1(xs: Seq[Int]) - //:: ExpectedOutput(not.wellformed:seq.index.negative) - requires xs[-1] != 0 - -method test10(xs: Seq[Int]) - //:: ExpectedOutput(not.wellformed:seq.index.length) - ensures xs[1] != 0 - -method test2(xs: Seq[Int], n: Int) - requires 5 < n - //:: ExpectedOutput(not.wellformed:seq.index.length) - requires forall i: Int :: i in [0..n) ==> xs[i] != 0 -{ - //:: UnexpectedOutput(assert.failed:seq.index.length, /Carbon/issue/388/) - assert xs[3] != 0 -} - -method test3(xs: Seq[Ref], n: Int) - requires 5 < n && n < |xs| - requires xs[0] != null - requires forall i: Int :: i in [0..n) ==> acc(xs[i].f) -{ - var y: Int := xs[3].f -} - -function fun(i: Int): Bool - -method test20(xs: Seq[Int], i: Int) { - //:: ExpectedOutput(assignment.failed:seq.index.negative) - //:: ExpectedOutput(assignment.failed:seq.index.length) - var b: Bool := fun(xs[i]) -} +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +field f: Int + +method test1(xs: Seq[Int]) + //:: ExpectedOutput(not.wellformed:seq.index.negative) + requires xs[-1] != 0 + +method test10(xs: Seq[Int]) + //:: ExpectedOutput(not.wellformed:seq.index.length) + ensures xs[1] != 0 + +method test2(xs: Seq[Int], n: Int) + requires 5 < n + //:: ExpectedOutput(not.wellformed:seq.index.length) + requires forall i: Int :: i in [0..n) ==> xs[i] != 0 +{ + //:: ExpectedOutput(assert.failed:seq.index.length) + //:: MissingOutput(assert.failed:seq.index.length, /silicon/issue/34/) + assert xs[3] != 0 +} + +method test3(xs: Seq[Ref], n: Int) + requires 5 < n && n < |xs| + requires xs[0] != null + requires forall i: Int :: i in [0..n) ==> acc(xs[i].f) +{ + var y: Int := xs[3].f +} + +function fun(i: Int): Bool + +method test20(xs: Seq[Int], i: Int) { + //:: ExpectedOutput(assignment.failed:seq.index.negative) + //:: ExpectedOutput(assignment.failed:seq.index.length) + //:: MissingOutput(assignment.failed:seq.index.length, /silicon/issue/34/) + var b: Bool := fun(xs[i]) +} From 53bd7a44179973cd2671ffb83ebe1f77f3b6c054 Mon Sep 17 00:00:00 2001 From: Josua Stuck Date: Sun, 5 Sep 2021 19:34:33 +0200 Subject: [PATCH 5/6] Revert "add UnexpectedOutput annotations" This reverts commit 87e4f2a2bbe5f9bcb1c2d3fc558fec18f01e6cf5. --- .../wands/examples/list_insert_tmp.vpr | 1 - .../resources/wands/new_syntax/QPWands.vpr | 217 +++++++++--------- 2 files changed, 108 insertions(+), 110 deletions(-) diff --git a/src/test/resources/wands/examples/list_insert_tmp.vpr b/src/test/resources/wands/examples/list_insert_tmp.vpr index 9b4cf897b..3d9baf2c5 100644 --- a/src/test/resources/wands/examples/list_insert_tmp.vpr +++ b/src/test/resources/wands/examples/list_insert_tmp.vpr @@ -129,7 +129,6 @@ method insert(xs: Ref, x: Int) returns (i: Int) acc(List(xs)) && elems(xs) == old(elems(xs))[0..i] ++ (Seq(x) ++ crtElems) //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/290/) - //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/550/) assert acc(List(crt))&& elems(crt) == Seq(x) ++ crtElems apply diff --git a/src/test/resources/wands/new_syntax/QPWands.vpr b/src/test/resources/wands/new_syntax/QPWands.vpr index 97eaa4069..5e5e105e5 100644 --- a/src/test/resources/wands/new_syntax/QPWands.vpr +++ b/src/test/resources/wands/new_syntax/QPWands.vpr @@ -1,112 +1,111 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ -//:: IgnoreFile(/carbon/issue/216/) -field f: Int - -define injectiveSeq(xs) forall i: Int, j: Int :: 0 <= i && 0 <= j && i < |xs| && j < |xs| && i != j ==> xs[i] != xs[j] - -method test0(xs: Seq[Ref], y: Ref) -requires forall x: Ref :: x in xs ==> acc(x.f) -requires injectiveSeq(xs) -requires |xs| >= 1 -requires acc(y.f) { - xs[0].f := 0 - y.f := 1 - label setupComplete - var toGo: Seq[Ref] := xs - var completed: Seq[Ref] := Seq() - while (|toGo| != 0) - invariant forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f) - invariant forall i: Int, j: Int :: 0 <= i && 0 <= j && i < |toGo| && j < |toGo| && i != j ==> toGo[i] != toGo[j] - invariant forall x: Ref :: x in toGo ==> acc(x.f) - invariant xs == completed ++ toGo - invariant forall x: Ref :: x in toGo ==> x.f == old[setupComplete](x.f) - invariant acc(y.f) && y.f == 1 - //:: UnexpectedOutput(invariant.not.preserved:assertion.false, /silicon/issue/311/) - invariant forall x: Ref :: x in completed ==> - applying (acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f)) in - x.f == old[setupComplete](x.f) { - var localX: Ref := toGo[0] - package acc(y.f) --* acc(localX.f) && acc(y.f) && y.f == old[lhs](y.f) - completed := completed ++ Seq(localX) - toGo := toGo[1..] - } - assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f) - var some: Ref := xs[0] - apply acc(y.f) --* acc(some.f) && acc(y.f) && y.f == old[lhs](y.f) - //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/551/) - assert some.f == 0 //This shouldn't throw an error - assert y.f == 1 -} - -method test1(x: Ref) -requires forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f) { - exhale forall i: Int :: true ==> acc(x.f) && x.f == i-1 --* acc(x.f) - - //:: ExpectedOutput(assert.failed:wand.not.found) - assert forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f) -} - -method test2(xs: Seq[Ref], y: Ref) -requires forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) { - - //:: ExpectedOutput(assert.failed:wand.not.found) - assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(y.f) && acc(x.f) -} - -method test3(xs: Seq[Ref], y: Ref) -requires forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) -requires injectiveSeq(xs) -requires |xs| > 0 -requires acc(y.f) { - var some: Ref := xs[0] - package true --* acc(some.f) && acc(y.f) { - apply acc(y.f) --* acc(some.f) && acc(y.f) - } - assert forall x: Ref :: x in xs[1..] ==> acc(y.f) --* acc(x.f) && acc(y.f) - - //:: ExpectedOutput(assert.failed:wand.not.found) - assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) -} - -method test4(x: Ref) -requires forall i: Int, j: Int :: true ==> acc(x.f) && x.f == i + j --* acc(x.f) { - exhale acc(x.f) && x.f == 5 --* acc(x.f) - assert forall i: Int :: i != 5 ==> acc(x.f) && x.f == i --* acc(x.f) - - //:: ExpectedOutput(assert.failed:wand.not.found) - assert forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f) -} - -method test5(xs: Seq[Ref], y: Ref) -requires forall x: Ref :: x in xs ==> acc(x.f) -requires injectiveSeq(xs) -requires |xs| >= 1 -requires acc(y.f) { - xs[0].f := 0 - y.f := 1 - var some: Ref := xs[0] - package acc(y.f) --* acc(some.f) && acc(y.f) - var completed: Seq[Ref] := Seq(some) - assert forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f) - assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in some.f == 0 - assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in y.f == 1 - assert forall x: Ref :: x in xs[1..] ==> acc(x.f) - - //:: ExpectedOutput(assert.failed:insufficient.permission) - assert forall x: Ref :: x in xs ==> acc(x.f) -} - -method test6(xs: Seq[Ref]) -requires forall x: Ref :: x in xs ==> true --* acc(x.f) -requires |xs| > 0 { - assume applying (true --* acc(xs[0].f)) in xs[0].f == 0 - package true --* (forall x: Ref :: x in xs ==> true --* acc(x.f)) - apply true --* (forall x: Ref :: x in xs ==> true --* acc(x.f)) - apply true --* acc(xs[0].f) - assert xs[0].f == 0 - - //:: ExpectedOutput(assert.failed:assertion.false) - assert false -} +//:: IgnoreFile(/carbon/issue/216/) +field f: Int + +define injectiveSeq(xs) forall i: Int, j: Int :: 0 <= i && 0 <= j && i < |xs| && j < |xs| && i != j ==> xs[i] != xs[j] + +method test0(xs: Seq[Ref], y: Ref) +requires forall x: Ref :: x in xs ==> acc(x.f) +requires injectiveSeq(xs) +requires |xs| >= 1 +requires acc(y.f) { + xs[0].f := 0 + y.f := 1 + label setupComplete + var toGo: Seq[Ref] := xs + var completed: Seq[Ref] := Seq() + while (|toGo| != 0) + invariant forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f) + invariant forall i: Int, j: Int :: 0 <= i && 0 <= j && i < |toGo| && j < |toGo| && i != j ==> toGo[i] != toGo[j] + invariant forall x: Ref :: x in toGo ==> acc(x.f) + invariant xs == completed ++ toGo + invariant forall x: Ref :: x in toGo ==> x.f == old[setupComplete](x.f) + invariant acc(y.f) && y.f == 1 + //:: UnexpectedOutput(invariant.not.preserved:assertion.false, /silicon/issue/311/) + invariant forall x: Ref :: x in completed ==> + applying (acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f)) in + x.f == old[setupComplete](x.f) { + var localX: Ref := toGo[0] + package acc(y.f) --* acc(localX.f) && acc(y.f) && y.f == old[lhs](y.f) + completed := completed ++ Seq(localX) + toGo := toGo[1..] + } + assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f) + var some: Ref := xs[0] + apply acc(y.f) --* acc(some.f) && acc(y.f) && y.f == old[lhs](y.f) + assert some.f == 0 + assert y.f == 1 +} + +method test1(x: Ref) +requires forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f) { + exhale forall i: Int :: true ==> acc(x.f) && x.f == i-1 --* acc(x.f) + + //:: ExpectedOutput(assert.failed:wand.not.found) + assert forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f) +} + +method test2(xs: Seq[Ref], y: Ref) +requires forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) { + + //:: ExpectedOutput(assert.failed:wand.not.found) + assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(y.f) && acc(x.f) +} + +method test3(xs: Seq[Ref], y: Ref) +requires forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) +requires injectiveSeq(xs) +requires |xs| > 0 +requires acc(y.f) { + var some: Ref := xs[0] + package true --* acc(some.f) && acc(y.f) { + apply acc(y.f) --* acc(some.f) && acc(y.f) + } + assert forall x: Ref :: x in xs[1..] ==> acc(y.f) --* acc(x.f) && acc(y.f) + + //:: ExpectedOutput(assert.failed:wand.not.found) + assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) +} + +method test4(x: Ref) +requires forall i: Int, j: Int :: true ==> acc(x.f) && x.f == i + j --* acc(x.f) { + exhale acc(x.f) && x.f == 5 --* acc(x.f) + assert forall i: Int :: i != 5 ==> acc(x.f) && x.f == i --* acc(x.f) + + //:: ExpectedOutput(assert.failed:wand.not.found) + assert forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f) +} + +method test5(xs: Seq[Ref], y: Ref) +requires forall x: Ref :: x in xs ==> acc(x.f) +requires injectiveSeq(xs) +requires |xs| >= 1 +requires acc(y.f) { + xs[0].f := 0 + y.f := 1 + var some: Ref := xs[0] + package acc(y.f) --* acc(some.f) && acc(y.f) + var completed: Seq[Ref] := Seq(some) + assert forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f) + assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in some.f == 0 + assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in y.f == 1 + assert forall x: Ref :: x in xs[1..] ==> acc(x.f) + + //:: ExpectedOutput(assert.failed:insufficient.permission) + assert forall x: Ref :: x in xs ==> acc(x.f) +} + +method test6(xs: Seq[Ref]) +requires forall x: Ref :: x in xs ==> true --* acc(x.f) +requires |xs| > 0 { + assume applying (true --* acc(xs[0].f)) in xs[0].f == 0 + package true --* (forall x: Ref :: x in xs ==> true --* acc(x.f)) + apply true --* (forall x: Ref :: x in xs ==> true --* acc(x.f)) + apply true --* acc(xs[0].f) + assert xs[0].f == 0 + + //:: ExpectedOutput(assert.failed:assertion.false) + assert false +} From fc3f4a8af495350ae67c891eabe76425585a3a8e Mon Sep 17 00:00:00 2001 From: Josua Stuck Date: Sun, 5 Sep 2021 19:34:56 +0200 Subject: [PATCH 6/6] Revert "remove missingOutput annotation" This reverts commit f13bbdb23da7cbd9a260eb989e2bb778a643e5ce. --- src/test/resources/quantifiedpermissions/sequences/bsearch.vpr | 1 + 1 file changed, 1 insertion(+) diff --git a/src/test/resources/quantifiedpermissions/sequences/bsearch.vpr b/src/test/resources/quantifiedpermissions/sequences/bsearch.vpr index a591a08f2..546a50d0f 100644 --- a/src/test/resources/quantifiedpermissions/sequences/bsearch.vpr +++ b/src/test/resources/quantifiedpermissions/sequences/bsearch.vpr @@ -12,6 +12,7 @@ method bfind_orig(S: Seq[Ref], x: Int, p: Perm) returns (index: Int) ensures forall i: Int :: {S[i].f} i in [0..|S|) ==> acc(S[i].f, p) ensures index in [-1..|S|) //:: ExpectedOutput(postcondition.violated:assertion.false) + //:: MissingOutput(postcondition.violated:assertion.false, /silicon/issue/34/) ensures index in [0..|S|) ==> S[index].f == x //:: ExpectedOutput(postcondition.violated:assertion.false) ensures index == -1 ==> (forall i: Int :: {S[i].f} i in [0..|S|) ==> S[i].f != x)