Parser and consistency fixes

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.

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)}
 
@@ -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)
   })
 

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])
+}

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])
+}

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;
+}

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)
+    )
+  }
 }