From 82c6bb694ff1b5d9c5abc2a1e56abed28e036d76 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 14 Oct 2022 15:56:44 +0200 Subject: [PATCH 1/4] Fixing bug 520, 521, 500 --- src/main/scala/viper/silver/ast/Expression.scala | 4 +++- src/main/scala/viper/silver/parser/FastParser.scala | 4 ++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala index 71c83a0ba..b08c275cf 100644 --- a/src/main/scala/viper/silver/ast/Expression.scala +++ b/src/main/scala/viper/silver/ast/Expression.scala @@ -558,6 +558,7 @@ case class Forall(variables: Seq[LocalVarDecl], triggers: Seq[Trigger], exp: Exp //require(isValid, s"Invalid quantifier: { $this } .") override lazy val check : Seq[ConsistencyError] = (if(!(exp isSubtype Bool)) Seq(ConsistencyError(s"Body of universal quantifier must be of Bool type, but found ${exp.typ}", exp.pos)) else Seq()) ++ + (if (variables.isEmpty) Seq(ConsistencyError("Quantifier must have at least one quantified variable.", pos)) else Seq()) ++ Consistency.checkAllVarsMentionedInTriggers(variables, triggers) ++ checkNoNestedQuantsForQuantPermissions ++ checkQuantifiedPermission @@ -624,7 +625,8 @@ case class Forall(variables: Seq[LocalVarDecl], triggers: Seq[Trigger], exp: Exp /** Existential quantification. */ case class Exists(variables: Seq[LocalVarDecl], triggers: Seq[Trigger], exp: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends QuantifiedExp { override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(exp) ++ - (if(!(exp isSubtype Bool)) Seq(ConsistencyError(s"Body of existential quantifier must be of Bool type, but found ${exp.typ}", exp.pos)) else Seq()) + (if(!(exp isSubtype Bool)) Seq(ConsistencyError(s"Body of existential quantifier must be of Bool type, but found ${exp.typ}", exp.pos)) else Seq()) ++ + (if (variables.isEmpty) Seq(ConsistencyError("Quantifier must have at least one quantified variable.", pos)) else Seq()) /** Returns an identical forall quantification that has some automatically generated triggers * if necessary and possible. diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index e220d4cb9..279ac7f8a 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -799,11 +799,11 @@ class FastParser { def result[_: P]: P[PResultLit] = FP(keyword("result")).map { case (pos, _) => PResultLit()(pos) } - def unExp[_: P]: P[PUnExp] = FP(CharIn("\\-\\!").! ~~ !" " ~~ suffixExpr).map { case (pos, (a, b)) => PUnExp(a, b)(pos) } + def unExp[_: P]: P[PUnExp] = FP(CharIn("\\-\\!").! ~ suffixExpr).map { case (pos, (a, b)) => PUnExp(a, b)(pos) } def strInteger[_: P]: P[String] = P(CharIn("0-9").rep(1)).! - def integer[_: P]: P[PIntLit] = FP(strInteger.filter(s => !s.contains(' '))).map { case (pos, s) => PIntLit(BigInt(s))(pos) } + def integer[_: P]: P[PIntLit] = FP(strInteger.filter(s => s.matches("\\S+"))).map { case (pos, s) => PIntLit(BigInt(s))(pos) } def booltrue[_: P]: P[PBoolLit] = FP(keyword("true")).map {case (pos, _) => PBoolLit(b = true)(pos)} From d742af980bf6620d2a006ac69f824f2b9932e7b5 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 14 Oct 2022 16:00:19 +0200 Subject: [PATCH 2/4] Fixing issue 606 --- src/main/scala/viper/silver/ast/Expression.scala | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala index b08c275cf..1f047b646 100644 --- a/src/main/scala/viper/silver/ast/Expression.scala +++ b/src/main/scala/viper/silver/ast/Expression.scala @@ -475,7 +475,6 @@ case class CondExp(cond: Exp, thn: Exp, els: Exp)(val pos: Position = NoPosition // --- Prover hint expressions case class Unfolding(acc: PredicateAccessPredicate, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp { - override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(body) lazy val typ = body.typ } From ad113f049de02201e6c99681eb7efef13cf59083 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 14 Oct 2022 16:11:27 +0200 Subject: [PATCH 3/4] Fix for issue 517 --- src/main/scala/viper/silver/parser/FastParser.scala | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index 279ac7f8a..5b16a5686 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -1034,11 +1034,11 @@ class FastParser { def setTypedEmpty[_: P]: P[PExp] = collectionTypedEmpty("Set", (a, b) => PEmptySet(a)(b)) - def explicitSetNonEmpty[_: P]: P[PExp] = P(FP("Set" ~ "(" ~/ exp.rep(sep = ",", min = 1) ~ ")").map { + def explicitSetNonEmpty[_: P]: P[PExp] = P(FP("Set" ~ "(" ~ exp.rep(sep = ",", min = 1) ~ ")").map { case (pos, exps) => PExplicitSet(exps)(pos) }) - def explicitMultisetNonEmpty[_: P]: P[PExp] = P(FP("Multiset" ~ "(" ~/ exp.rep(min = 1, sep = ",") ~ ")").map { + def explicitMultisetNonEmpty[_: P]: P[PExp] = P(FP("Multiset" ~ "(" ~ exp.rep(min = 1, sep = ",") ~ ")").map { case (pos, exps) => PExplicitMultiset(exps)(pos) }) @@ -1050,16 +1050,16 @@ class FastParser { case (pos, e) => PSize(e)(pos) }) - def explicitSeqNonEmpty[_: P]: P[PExp] = P(FP("Seq" ~ "(" ~/ exp.rep(min = 1, sep = ",") ~ ")").map { + def explicitSeqNonEmpty[_: P]: P[PExp] = P(FP("Seq" ~ "(" ~ exp.rep(min = 1, sep = ",") ~ ")").map { case (pos, exps) => PExplicitSeq(exps)(pos) }) private def collectionTypedEmpty[_: P](name: String, typeConstructor: (PType, (Position, Position)) => PExp): P[PExp] = - FP(`name` ~ ("[" ~/ typ ~ "]").? ~ "(" ~ ")").map{ case (pos, typ) => typeConstructor(typ.getOrElse(PTypeVar("#E")), pos)} + FP(`name` ~ ("[" ~ typ ~ "]").? ~ "(" ~ ")").map{ case (pos, typ) => typeConstructor(typ.getOrElse(PTypeVar("#E")), pos)} def seqRange[_: P]: P[PExp] = FP("[" ~ exp ~ ".." ~ exp ~ ")").map { case (pos, (a, b)) => PRangeSeq(a, b)(pos) } - def mapTypedEmpty[_: P] : P[PMapLiteral] = P(FP("Map" ~ ("[" ~/ typ ~ "," ~ typ ~ "]").? ~ "(" ~ ")").map { + def mapTypedEmpty[_: P] : P[PMapLiteral] = P(FP("Map" ~ ("[" ~ typ ~ "," ~ typ ~ "]").? ~ "(" ~ ")").map { case (pos, Some((keyType, valueType))) => PEmptyMap(keyType, valueType)(pos) case (pos, None) => PEmptyMap(PTypeVar("#K"), PTypeVar("#E"))(pos) }) @@ -1068,7 +1068,7 @@ class FastParser { case (pos, (key, value)) => PMaplet(key, value)(pos) }) - def explicitMapNonEmpty[_: P]: P[PMapLiteral] = P(FP("Map" ~ "(" ~/ maplet.rep(sep = ",", min = 1) ~ ")").map { + def explicitMapNonEmpty[_: P]: P[PMapLiteral] = P(FP("Map" ~ "(" ~ maplet.rep(sep = ",", min = 1) ~ ")").map { case (pos, maplets) => PExplicitMap(maplets)(pos) }) From 3719ddd2ed0fef73e946abdf13544daf39db4a35 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 14 Oct 2022 19:37:11 +0200 Subject: [PATCH 4/4] Undid unfolding change (issue 606) because Silicon crashes, added tests for all others --- .../scala/viper/silver/ast/Expression.scala | 1 + .../resources/all/issues/silver/0271-1.vpr | 8 -- .../resources/all/issues/silver/0271-2.vpr | 8 -- src/test/resources/all/issues/silver/0500.vpr | 129 ++++++++++++++++++ src/test/resources/all/issues/silver/0517.vpr | 14 ++ src/test/resources/all/issues/silver/0520.vpr | 17 +++ src/test/scala/ConsistencyTests.scala | 15 ++ 7 files changed, 176 insertions(+), 16 deletions(-) delete mode 100644 src/test/resources/all/issues/silver/0271-1.vpr delete mode 100644 src/test/resources/all/issues/silver/0271-2.vpr create mode 100644 src/test/resources/all/issues/silver/0500.vpr create mode 100644 src/test/resources/all/issues/silver/0517.vpr create mode 100644 src/test/resources/all/issues/silver/0520.vpr diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala index 1f047b646..b08c275cf 100644 --- a/src/main/scala/viper/silver/ast/Expression.scala +++ b/src/main/scala/viper/silver/ast/Expression.scala @@ -475,6 +475,7 @@ case class CondExp(cond: Exp, thn: Exp, els: Exp)(val pos: Position = NoPosition // --- Prover hint expressions case class Unfolding(acc: PredicateAccessPredicate, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp { + override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(body) lazy val typ = body.typ } diff --git a/src/test/resources/all/issues/silver/0271-1.vpr b/src/test/resources/all/issues/silver/0271-1.vpr deleted file mode 100644 index c5835381a..000000000 --- a/src/test/resources/all/issues/silver/0271-1.vpr +++ /dev/null @@ -1,8 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -method m() -{ - //:: ExpectedOutput(parser.error) - var i: Int := - 1 // No whitespace is allowed after "-" -} diff --git a/src/test/resources/all/issues/silver/0271-2.vpr b/src/test/resources/all/issues/silver/0271-2.vpr deleted file mode 100644 index 35c38bc82..000000000 --- a/src/test/resources/all/issues/silver/0271-2.vpr +++ /dev/null @@ -1,8 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -method m() -{ - //:: ExpectedOutput(parser.error) - var b: Bool := ! true // No whitespace is allowed after "!" -} diff --git a/src/test/resources/all/issues/silver/0500.vpr b/src/test/resources/all/issues/silver/0500.vpr new file mode 100644 index 000000000..4195b45c8 --- /dev/null +++ b/src/test/resources/all/issues/silver/0500.vpr @@ -0,0 +1,129 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +method t1(x: Int, xs: Seq[Int]) { + var n: Seq[Int] := Seq[Int]() + assert |n| == 0 + assert n != Seq(x) + assert |Seq(1)| == 1 + assert |Seq(0)| == 0 +} + +method t2() { + assert 1 in Seq(1,2,3) + assert |[-1..10)| == 11 + assert Seq(1) ++ Seq(2) == Seq(1,2) + + var a: Seq[Int] := Seq(0,1,-11,22) + assert a[2] == -11 + + assert a[..1] == Seq(0) + assert a[1..] == Seq(1,-11,22) + assert a[1..2] == Seq(1) + + assert a[1 := 22] == (a[1 := -1][1 := 22]) + assert a[1 := 22] == Seq(0,22,-11,22) + assert |a[1 := 22]| == 4 + assert a[1 := 22][1] == 22 + assert a[1 := 22][2] == -11 + assert a[1 := 22][0] == 22 +} + +method test3() { + var xs: Seq[Int] := Seq(0, 1, 2, 3, 4, 5, 6, 7) + var bs: Seq[Bool] := Seq(true, true, false, true) ++ Seq(false, true) + + assert |xs[1..][..6]| == |bs| + assert |xs[1..]| == |xs| +} + +method test4(s:Seq[Int], i : Int, j:Int) + requires 0 <= i + requires i <= j +{ + assert s == s[..i] ++ s[i..] + assert s == s[..i] ++ s[i..j] ++ s[j..] + assert (s[..i] ++ s[i..j]) ++ s[j..] assert a[1..2] == Seq(1) + + assert a[1 := 22] == (a[1 := -1][1 := 22]) + assert a[1 := 22] == Seq(0,22,-11,22) + assert |a[1 := 22]| == 4 + assert a[1 := 22][1] == 22 + assert a[1 := 22][2] == -11 + assert a[1 := 22][0] == 22 +} + +method test3() { + var xs: Seq[Int] := Seq(0, 1, 2, 3, 4, 5, 6, 7) + var bs: Seq[Bool] := Seq(true, true, false, true) ++ Seq(false, true) + + assert |xs[1..][..6]| == |bs| + assert |xs[1..]| == |xs| +} + +method test4(s:Seq[Int], i : Int, j:Int) + requires 0 <= i + requires i <= j +{ + assert s == s[..i] ++ s[i..] + assert s == s[..i] ++ s[i..j] ++ s[j..] + assert (s[..i] ++ s[i..j]) ++ s[j..] == s[..i] ++ (s[i..j] ++ s[j..]) + assert |s[j..]| == |s| - j +} + +method test5(s:Seq[Int], i : Int, j:Int) +{ + assert s == s[..i] ++ s[i..] +} + +method test6() { + assert Seq(3,4,5,6)[0] == 3 + //:: ExpectedOutput(parser.error) + assert Seq(3,4,5,6)[1] == 4 +5,6)[i]) +} + +me== s[..i] ++ (s[i..j] ++ s[j..]) + assert |s[j..]| == |s| - j +} + +method test5(s:Seq[Int], i : Int, j:Int) +{ + assert s == s[..i] ++ s[i..] +} + +method test6() { + assert Seq(3,4,5,6)[0] == 3 + assert Seq(3,4,5,6)[1] == 4 + assert Seq(3,4,5,6)[2] == 5 + assert Seq(3,4,5,6)[3] == 6 + assert Seq(3,4,5,6)[3] == 5 +} + +function trivial(i:Int) : Bool { true } + +method test_index_definedness_small(i : Int) + requires i < 4 +{ + assert trivial(Seq(3,4,5,6)[i]) +} + +method test_index_definedness_large(i : Int) + requires i >= 0 +{ + assefrt trivial(Seq(3,4,5,6)[i]) +} + +method test_build_index_definedness_small(i : Int) + requires i < 4 +{ +(assert.failed:seq.index.negative, /carbon/issue/232/) + assert trivial(Seq(3,4,5,6)[i := 3][0]) +} + +method test_build_index_definedness_large(] : Int) + requires i >= 0 +{ + var s : Seq[Int] := Seq(3,4,5,6)[i := 3] + assert trivial(s[0]) +} \ No newline at end of file diff --git a/src/test/resources/all/issues/silver/0517.vpr b/src/test/resources/all/issues/silver/0517.vpr new file mode 100644 index 000000000..eccadd8ca --- /dev/null +++ b/src/test/resources/all/issues/silver/0517.vpr @@ -0,0 +1,14 @@ +domain Either[T, V] { + function left(t: T): Either[T, V] + function right(v: V): Either[T, V] +} + +method client(s: Seq[Int]) +{ + var x: Either[Seq[Int], Ref] + // okay + x := (left(s): Either[Seq[Int], Ref]) + x := (left(Seq[Int]())) + // parse error + x := (left(Seq[Int]()): Either[Seq[Int], Ref]) +} \ No newline at end of file diff --git a/src/test/resources/all/issues/silver/0520.vpr b/src/test/resources/all/issues/silver/0520.vpr new file mode 100644 index 000000000..f6d9c93a8 --- /dev/null +++ b/src/test/resources/all/issues/silver/0520.vpr @@ -0,0 +1,17 @@ +method test(n: Int, d: Int) returns (q: Int, r: Int) + requires n >= 0 && d > 0; + ensures n == q * d + r && r >= 0 && r < d; +{ + r := n; + q := 0; + + while(r >= 0) + invariant r >= - d && n == q * d + r; + { + r := r - d; + q := q + 1; + } + + r := r + d; + q := q - 1; +} \ No newline at end of file diff --git a/src/test/scala/ConsistencyTests.scala b/src/test/scala/ConsistencyTests.scala index 08a5f8ad6..8ff3f1f8e 100644 --- a/src/test/scala/ConsistencyTests.scala +++ b/src/test/scala/ConsistencyTests.scala @@ -256,4 +256,19 @@ class ConsistencyTests extends AnyFunSuite with Matchers { ConsistencyError("Quantified permissions must have an implication as expression, with the access predicate in its right-hand side.", NoPosition) ) } + + test("Testing if Forall AST nodes have at least one quantified variable, and all variables are mentioned in the trigger.") { + + val f = Function("f", Seq(LocalVarDecl("i", Int)()), Int, Seq(), Seq(), None)() + val forallNoVar = Forall(Seq(), Seq(), TrueLit()())() + val forallUnusedVar = Forall(Seq(LocalVarDecl("i", Int)()), Seq(Trigger(Seq(FuncApp(f, Seq(IntLit(0)()))()))()), TrueLit()())() + + forallNoVar.checkTransitively shouldBe Seq( + ConsistencyError("Quantifier must have at least one quantified variable.", NoPosition) + ) + + forallUnusedVar.checkTransitively shouldBe Seq( + ConsistencyError("Variable i is not mentioned in one or more triggers.", NoPosition) + ) + } }