Ranged for syntax in PVL

src/col/vct/col/ast/Node.scala

@@ -207,6 +207,7 @@ final case class Branch[G](branches: Seq[(Expr[G], Statement[G])])(implicit val
 final case class IndetBranch[G](branches: Seq[Statement[G]])(implicit val o: Origin) extends CompositeStatement[G] with IndetBranchImpl[G]
 final case class Switch[G](expr: Expr[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with SwitchImpl[G]
 final case class Loop[G](init: Statement[G], cond: Expr[G], update: Statement[G], contract: LoopContract[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with LoopImpl[G]
+final case class RangedFor[G](iter: IterVariable[G], contract: LoopContract[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with Declarator[G] with RangedForImpl[G]
 final case class TryCatchFinally[G](body: Statement[G], after: Statement[G], catches: Seq[CatchClause[G]])(implicit val o: Origin) extends CompositeStatement[G] with TryCatchFinallyImpl[G]
 final case class Synchronized[G](obj: Expr[G], body: Statement[G])(val blame: Blame[LockRegionFailure])(implicit val o: Origin) extends CompositeStatement[G] with SynchronizedImpl[G]
 final case class ParInvariant[G](decl: ParInvariantDecl[G], inv: Expr[G], content: Statement[G])(val blame: Blame[ParInvariantNotEstablished])(implicit val o: Origin) extends CompositeStatement[G] with ParInvariantImpl[G]

src/col/vct/col/ast/statement/composite/RangedForImpl.scala

@@ -0,0 +1,13 @@
+package vct.col.ast.statement.composite
+
+import vct.col.ast.{Declaration, RangedFor}
+import vct.col.print._
+
+trait RangedForImpl[G] { this: RangedFor[G] =>
+  override def declarations: Seq[Declaration[G]] = Seq(iter.variable)
+
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      Group(Text("for") <> "(" <> Doc.arg(iter) <> ")"),
+    )) <+> body.layoutAsBlock
+}

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -1568,6 +1568,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case bar @ ParBarrier(block, invs, requires, ensures, content) => ParBarrier(block, invs, res(requires), res(ensures), content)(bar.blame)
       case p @ ParInvariant(decl, inv, content) => ParInvariant(decl, res(inv), content)(p.blame)
       case ParStatement(impl) => ParStatement(impl)
+      case RangedFor(iter, contract, body) => RangedFor(iter, contract, body)
       case Recv(ref) => Recv(ref)
       case r @ Refute(assn) => Refute(res(assn))(r.blame)
       case Return(result) => Return(result) // TODO coerce return, make AmbiguousReturn?

src/colhelper/ColDefs.scala

@@ -52,7 +52,7 @@ object ColDefs {
     "ModelDeclaration" -> Seq("Program"),
     "EnumConstant" -> Seq("Program"),
     "Variable" -> Seq(
-      "ParBlock", "VecBlock", "CatchClause", "Scope", "SignalsClause", // Explicit declarations
+      "ParBlock", "VecBlock", "CatchClause", "Scope", "SignalsClause", "RangedForLoop", // Explicit declarations
       "AxiomaticDataType", "JavaClass", "JavaInterface", // Type arguments
       "Predicate", "InstancePredicate", // Arguments
       "ModelProcess", "ModelAction", "ADTFunction",

src/main/vct/main/stages/Transformation.scala

@@ -182,6 +182,7 @@ case class SilverTransformation
     // Normalize AST
     Disambiguate, // Resolve overloaded operators (+, subscript, etc.)
     DisambiguateLocation, // Resolve location type
+    EncodeRangedFor,
 
     EncodeString, // Encode spec string as seq<int>
     EncodeChar,

src/parsers/antlr4/LangPVLParser.g4

@@ -182,6 +182,7 @@ statement
  | 'atomic' '(' identifierList ')' block # pvlAtomic
  | contract 'while' '(' expr ')' statement # pvlWhile
  | contract 'for' '(' forStatementList? ';' expr? ';' forStatementList? ')' statement # pvlFor
+ | contract 'for' '(' iter ')' statement # pvlRangedFor
  | block # pvlBlock
  | 'goto' identifier ';' # pvlGoto
  | 'label' identifier ';' # pvlLabel

src/parsers/vct/parsers/transform/PVLToCol.scala

@@ -345,6 +345,11 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val
           convert(body)
         ))
       )
+    case PvlRangedFor(contract, _, _, iter, _, body) =>
+      withContract(contract, contract =>
+        Scope(Nil, RangedFor(convert(iter),
+          contract.consumeLoopContract(stat),
+          convert(body))))
     case PvlBlock(inner) => convert(inner)
     case PvlGoto(_, label, _) => Goto(new UnresolvedRef[G, LabelDecl[G]](convert(label)))
     case PvlLabel(_, label, _) => Label(new LabelDecl()(SourceNameOrigin(convert(label), origin(stat))), Block(Nil))

src/rewrite/vct/rewrite/EncodeRangedFor.scala

@@ -0,0 +1,47 @@
+package vct.col.rewrite
+
+import hre.util.ScopedStack
+import vct.col.ast.{Select, Block, Assign, Expr, IterVariable, Local, LocalDecl, Loop, LoopInvariant, IterationContract, Eval, LoopContract, PostAssignExpression, Range, RangedFor, SeqMember, Statement, Variable}
+import vct.col.origin.AssignLocalOk
+import vct.col.util.AstBuildHelpers.const
+import vct.col.util.AstBuildHelpers._
+import vct.col.ast.RewriteHelpers._
+
+case object EncodeRangedFor extends RewriterBuilder {
+  override def key: String = "encodeRangedFor"
+  override def desc: String = "Encodes ranged for as a regular for loop"
+}
+
+case class EncodeRangedFor[Pre <: Generation]() extends Rewriter[Pre] {
+  val bounds = ScopedStack[(RangedFor[Pre], Expr[Post])]()
+
+  override def dispatch(stat: Statement[Pre]): Statement[Post] = stat match {
+    case rf @ RangedFor(iv @ IterVariable(iVar, from, to), contract, body) =>
+      implicit val o = iVar.o
+      val i: Local[Post] = Local(succ[Variable[Post]](iVar))(iVar.o)
+      Loop(
+        Block(Seq(
+          LocalDecl(variables.collect(dispatch(iVar))._1.head),
+          Assign(i, dispatch(from))(AssignLocalOk)
+        ))(iVar.o),
+        { implicit val o = iv.o; SeqMember(i, Range(dispatch(from), dispatch(to))) },
+        Eval(PostAssignExpression(i, i + const(1))(AssignLocalOk)),
+        bounds.having((rf,
+          { implicit val o = iv.o;
+            Select(dispatch(from) < dispatch(to),
+              SeqMember(i, Range(dispatch(from), dispatch(to) + const(1))),
+              i === dispatch(from))
+          }))(dispatch(contract)),
+        dispatch(body)
+      )(rf.o)
+    case stat => rewriteDefault(stat)
+  }
+
+  override def dispatch(contract: LoopContract[Pre]): LoopContract[Post] = (bounds.topOption, contract) match {
+    case (Some((rf, iBounds)), l: LoopInvariant[Pre]) =>
+      l.rewrite(invariant = (iBounds &* dispatch(l.invariant))(rf.o))
+    case (Some((rf, iBounds)), ic: IterationContract[Pre]) =>
+      ic.rewrite(context_everywhere = (iBounds &* dispatch(ic.context_everywhere))(rf.o))
+    case (None, c) => rewriteDefault(c)
+  }
+}

test/main/vct/test/integration/examples/TechnicalPvlSpec.scala

@@ -0,0 +1,18 @@
+package vct.test.integration.examples
+
+import vct.test.integration.helper.VercorsSpec
+
+class TechnicalPvlSpec extends VercorsSpec {
+  vercors should verify using silicon in "ranged for loop" pvl
+  """
+  void m() {
+    int max = -1;
+    loop_invariant max == i - 1;
+    for (int i = 0 .. 10) {
+      assert 0 <= i && i < 10;
+      max = i;
+    }
+    assert max == 9;
+  }
+  """
+}