No longer marking blocks with labels with invariants as loop head blocks if they aren't loop heads

src/main/scala/viper/silver/cfg/Block.scala

@@ -41,12 +41,14 @@ object Block {
 /**
   * A basic block containing statements.
   *
-  * @param id    The id of the basic block.
-  * @param stmts The list of statements of the basic block.
+  * @param id     The id of the basic block.
+  * @param stmts  The list of statements of the basic block.
+  * @param invs   The list of invariants of this basic block *in case* it turns out to be a loop head.
+  * @param loopId The loopId of this basic block *in case* it turns out to be a loop head.
   * @tparam S The type of the statements.
   * @tparam E The type of the expressions.
   */
-final class StatementBlock[S, E] private(val id: Int, val stmts: Seq[S])
+final class StatementBlock[S, E] private(val id: Int, val stmts: Seq[S], val invs: Option[Seq[E]] = None, val loopId: Option[Option[Int]] = None)
   extends Block[S, E] {
 
   override lazy val elements: Seq[Either[S, E]] = stmts.map(Left(_))
@@ -58,6 +60,9 @@ object StatementBlock {
   def apply[S, E](stmts: Seq[S] = Nil): StatementBlock[S, E] =
     new StatementBlock(Block.nextId(), stmts)
 
+  def apply[S, E](stmts: Seq[S], invs: Seq[E], loopId: Option[Int]): StatementBlock[S, E] =
+    new StatementBlock(Block.nextId(), stmts, Some(invs), Some(loopId))
+
   def unapply[S, E](block: StatementBlock[S, E]): Some[Seq[S]] =
     Some(block.stmts)
 }

src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala

@@ -429,7 +429,10 @@ object CfgGenerator {
           case (l@Label(_, invs)) :: rest if invs.nonEmpty =>
             val loopId = l.info.getUniqueInfo[IdInfo].map(_.id)
             val label = Label(l.name, Nil)(pos = l.pos, l.info)
-            LoopHeadBlock(invs, label :: rest, loopId)
+            // This block may or may not be a loop head.
+            // We store the invariant and loopId in an ordinary statement block; if it turns out to be a loop head,
+            // the block will be transformed to a LoopHeadBlock in LoopDetector.augment.
+            StatementBlock(label :: rest, invs, loopId)
           case stmts =>
             StatementBlock(stmts)
         }

src/main/scala/viper/silver/cfg/utility/LoopDetector.scala

@@ -179,6 +179,7 @@ object LoopDetector {
             // update after info
             val after = edge.target match {
               case LoopHeadBlock(_, _, loopId) => loopId
+              case sb: StatementBlock[_, _] if sb.loopId.isDefined => sb.loopId.get
               case block => getFirst(block).flatMap(getId)
             }
             val map3 = after
@@ -283,13 +284,13 @@ object LoopDetector {
         // turn target into loop head if edge is an in-edge
         val last = if (0 < in && out == 0) edge.target match {
           case head@LoopHeadBlock(_, _, _) => head
-          case block@StatementBlock(stmts) =>
+          case sBlock@StatementBlock(stmts) =>
             val loopId = stmts.head match {
               case stmt: Stmt => stmt.info.getUniqueInfo[IdInfo].map(_.id)
               case _ => None
             }
-            val head: Block[S, E] = LoopHeadBlock(Seq.empty, stmts, loopId)
-            heads.put(block, head)
+            val head: Block[S, E] = LoopHeadBlock(sBlock.invs.getOrElse(Seq.empty), stmts, loopId)
+            heads.put(sBlock, head)
             head
           case _ => ??? // We don't expect this to happen.
         } else heads.getOrElse(edge.target, edge.target)

src/test/resources/all/invariants/loops1.vpr

@@ -1,8 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/carbon/issue/368/)
-
 field f: Int
 
 method test01(x: Ref)
@@ -44,6 +42,125 @@ method test01(x: Ref)
   label endofprogram
 }
 
+method test01f(x: Ref)
+  requires acc(x.f)
+  ensures  acc(x.f) && x.f == old(x.f)
+{
+  var n1: Int
+  var n2: Int
+
+  label dummy
+    invariant acc(x.f, 1/2)
+    /* TODO: Label does not represent a loop head - warn about unused invariant? */
+
+  //:: ExpectedOutput(assert.failed:insufficient.permission)
+  assert acc(x.f, 2/1)
+
+  label lh1
+    invariant acc(x.f, 1/2)
+
+  assert perm(x.f) == 1/2
+
+  n1 := n1 + 1
+  if (n1 != 0) {
+    goto lh1
+  }
+
+  assert acc(x.f)
+
+  label lh2
+    invariant acc(x.f, 1/3)
+
+  assert perm(x.f) == 1/3
+
+  n2 := n2 + 1
+  if (n2 == 0) {
+    goto endofprogram
+  }
+  goto lh2
+
+  label endofprogram
+}
+
+method test01f2(x: Ref)
+  requires acc(x.f)
+  ensures  acc(x.f) && x.f == old(x.f)
+{
+  var n1: Int
+  var n2: Int
+
+  label dummy
+    invariant acc(x.f, 1/2)
+    /* TODO: Label does not represent a loop head - warn about unused invariant? */
+
+  assert acc(x.f)
+
+  //:: ExpectedOutput(invariant.not.preserved:insufficient.permission)
+  label lh1 invariant acc(x.f, 1/2)
+
+  assert perm(x.f) == 1/2
+
+  n1 := n1 + 1
+  if (n1 != 0) {
+    exhale acc(x.f, 1/2)
+    goto lh1
+  }
+
+  assert acc(x.f)
+
+  label lh2
+    invariant acc(x.f, 1/3)
+
+  assert perm(x.f) == 1/3
+
+  n2 := n2 + 1
+  if (n2 == 0) {
+    goto endofprogram
+  }
+  goto lh2
+
+  label endofprogram
+}
+
+method test01f3(x: Ref)
+  requires acc(x.f)
+  ensures  acc(x.f) && x.f == old(x.f)
+{
+  var n1: Int
+  var n2: Int
+
+  label dummy
+    invariant acc(x.f, 1/2)
+    /* TODO: Label does not represent a loop head - warn about unused invariant? */
+
+  assert acc(x.f)
+
+  label lh1
+    invariant acc(x.f, 1/2)
+
+  assert perm(x.f) == 1/2
+
+  n1 := n1 + 1
+  if (n1 != 0) {
+    goto lh1
+  }
+
+  assert acc(x.f)
+
+  //:: ExpectedOutput(invariant.not.established:assertion.false)
+  label lh2 invariant false
+
+  assert perm(x.f) == 1/3
+
+  n2 := n2 + 1
+  if (n2 == 0) {
+    goto endofprogram
+  }
+  goto lh2
+
+  label endofprogram
+}
+
 method test02(x: Ref)
   requires acc(x.f)
   ensures  acc(x.f) && x.f == old(x.f)
@@ -89,8 +206,44 @@ method test03(x: Ref)
   label lh1 // outer loop head
     invariant acc(x.f, 1/2)
 
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert perm(x.f) == 1/2
+
+  label lh2 // inner loop head
+    invariant acc(x.f, 1/3)
+
+  assert perm(x.f) == 1/3
+
+  n2 := n2 + 1
+  if (n2 == 0) {
+    goto endofprogram
+  }
+  goto lh2 // back-edge inner loop
+
+  // ----- begin dead code
   assert perm(x.f) == 1/2
 
+  n1 := n1 + 1
+  if (n1 != 0) {
+    goto lh1 // back-edge outer loop
+  }
+
+  // ----- end dead code
+
+  label endofprogram
+  assert n2 == 0 || n1 == 0
+}
+
+method test03p(x: Ref)
+  requires acc(x.f)
+  ensures  acc(x.f) && x.f == old(x.f)
+{
+  var n1: Int
+  var n2: Int
+
+  label lh1 // outer loop head
+    invariant acc(x.f, 1/2)
+
   label lh2 // inner loop head
     invariant acc(x.f, 1/3)
 
@@ -115,3 +268,4 @@ method test03(x: Ref)
   label endofprogram
   assert n2 == 0 || n1 == 0
 }
+

src/test/resources/all/issues/silicon/0525.vpr

@@ -0,0 +1,15 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+method testLabel(x: Ref)
+  requires acc(x.f)
+{
+  label dummy
+    invariant acc(x.f, 1/2)
+
+  assert acc(x.f)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}
+
+field f: Int

src/test/resources/all/issues/silicon/0607.vpr

@@ -0,0 +1,20 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method f() returns (i:Int, j:Int)
+{
+    i := 10
+    j := 10
+    label W
+    invariant i == j
+    i := i - 1
+    goto X
+    j := j - 1
+    if (i > 0) {
+        goto W
+    }
+    label X
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert i == j
+}