Add break and continue support (#432)

* added break and continue without labels

* changes

* continue with goto

* removed print

* pretty printing to continue

* violation instead of not implemented

* fix nomessages returned at stmttyping

* unchecked

* changed enclosinglabeledloop

* some comments

* pattern matching instead of isinstanceof

* enclosedIn*Loop -> enclosingLoop*Node

* fixed bug of not typechecking continue with label correctly, tests

* added some unit tests

* more unit tests and indentation fixed

* continue redone

* continue updates

* temp

* redone continue, more test cases

* added header

* prettyprinting

* some comments

* more comments

* more comments

* simplifications and test updates

* test changes

* consistency

* loop label in continue node for prettyprinting and debugging

* removed obsolete comment

* label test

* small refactoring

* unneeded spaces removed

* fixed duplicate labels test case annotation

* implemented joao's and felix's feedback

* removed obsolete label from while

* moved label declaration

* goodbye stack

* replaced - with _ in label names, some documentation

Co-authored-by: Felix A. Wolf <felix.wolf@inf.ethz.ch>

Author: Dspil

src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala

@@ -304,6 +304,9 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       showVar(resTarget) <> "," <+> showVar(successTarget) <+> "=" <+> showExpr(mapLookup)
     case PredExprFold(base, args, p) => "fold" <+> "acc" <> parens(showExpr(base) <> parens(showExprList(args)) <> "," <+> showExpr(p))
     case PredExprUnfold(base, args, p) => "unfold" <+> "acc" <> parens(showExpr(base) <> parens(showExprList(args)) <> "," <+> showExpr(p))
+
+    case Continue(l, _) => "continue" <+> opt(l)(text)
+    case Break(l, _) => "break" <+> opt(l)(text)
   })
 
   def showProxy(x: Proxy): Doc = updatePositionStore(x) <> (x match {
@@ -705,5 +708,7 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
       showVar(resTarget) <> "," <+> showVar(successTarget) <+> "=" <+> "<-" <+> showExpr(channel)
     case PredExprFold(base, args, p) => "fold" <+> "acc" <> parens(showExpr(base) <> parens(showExprList(args)) <> "," <+> showExpr(p))
     case PredExprUnfold(base, args, p) => "unfold" <+> "acc" <> parens(showExpr(base) <> parens(showExprList(args)) <> "," <+> showExpr(p))
+    case Continue(l, _) => "continue" <+> opt(l)(text)
+    case Break(l, _) => "break" <+> opt(l)(text)
   }
 }

src/main/scala/viper/gobra/ast/internal/Program.scala

@@ -267,6 +267,21 @@ case class Seqn(stmts: Vector[Stmt])(val info: Source.Parser.Info) extends Stmt
 
 case class Label(id: LabelProxy)(val info: Source.Parser.Info) extends Stmt
 
+/**
+  * 'label' corresponds to the loop label we want to continue. In case it is a normal
+  * continue node, it is None.
+  * The continue node will be replaced by a goto statement to 'escLabel' which has
+  * been placed properly while desugaring for loops.
+  */
+case class Continue(label: Option[String], escLabel: String)(val info: Source.Parser.Info) extends Stmt
+
+/**
+  * 'label' corresponds to the loop label we want to break out of. In case it is a normal
+  * break node, it is 'None'.
+  * The break node will be replaced by a goto statement to 'escLabel'.
+  */
+case class Break(label: Option[String], escLabel: String)(val info: Source.Parser.Info) extends Stmt
+
 case class If(cond: Expr, thn: Stmt, els: Stmt)(val info: Source.Parser.Info) extends Stmt
 
 case class While(cond: Expr, invs: Vector[Assertion], terminationMeasure: Option[TerminationMeasure], body: Stmt)(val info: Source.Parser.Info) extends Stmt

src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala

@@ -86,7 +86,7 @@ object OverflowChecksTransform extends InternalTransform {
       val ifStmt = If(cond, stmtTransform(thn), stmtTransform(els))(i.info)
       Seqn(Vector(assertCond, ifStmt))(i.info)
 
-    case w@While(cond, invs, terminationMeasure,body) =>
+    case w@While(cond, invs, terminationMeasure, body) =>
       val condInfo = createAnnotatedInfo(cond.info)
       val assertCond = Assert(assertionExprInBounds(cond, cond.typ)(condInfo))(condInfo)
       val whileStmt = While(cond, invs, terminationMeasure,stmtTransform(body))(w.info)

src/main/scala/viper/gobra/ast/internal/utility/GobraStrategy.scala

@@ -41,6 +41,8 @@ object GobraStrategy {
       case (_: Label, Seq(label: LabelProxy)) => Label(label)(meta)
       case (_: If, Seq(cond: Expr, thn: Stmt, els: Stmt)) => If(cond, thn, els)(meta)
       case (_: While, Seq(cond: Expr, invs: Vector[Assertion@unchecked], terminationMeasure: Option[TerminationMeasure@unchecked], body: Stmt)) => While(cond, invs, terminationMeasure, body)(meta)
+      case (_: Break, Seq(label: Option[String@unchecked], escLabel: String)) => Break(label, escLabel)(meta)
+      case (_: Continue, Seq(label: Option[String@unchecked], escLabel: String)) => Continue(label, escLabel)(meta)
       case (_: New, Seq(target: LocalVar, expr: Expr)) => New(target, expr)(meta)
       case (_: MakeSlice, Seq(target: LocalVar, typeParam: SliceT, lenArg: Expr, capArg: Option[Expr@unchecked])) => MakeSlice(target, typeParam, lenArg, capArg)(meta)
       case (_: MakeChannel, Seq(target: LocalVar, typeParam: ChannelT, bufferSizeArg: Option[Expr@unchecked], isChannel: MPredicateProxy, bufferSize: MethodProxy)) => MakeChannel(target, typeParam, bufferSizeArg, isChannel, bufferSize)(meta)

src/main/scala/viper/gobra/ast/internal/utility/Nodes.scala

@@ -39,6 +39,8 @@ object Nodes {
       case DomainFunc(_, args, results) => args ++ Seq(results)
       case DomainAxiom(expr) => Seq(expr)
       case s: Stmt => s match {
+        case Break(_, _) => Seq.empty
+        case Continue(_, _) => Seq.empty
         case Block(decls, stmts) => decls ++ stmts
         case Seqn(stmts) => stmts
         case Label(label) => Seq(label)

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -813,13 +813,14 @@ object Desugar {
 
           case b: PBlock => unit(blockD(ctx)(b))
 
-          case l: PLabeledStmt =>
+          case l: PLabeledStmt => {
             val proxy = labelProxy(l.label)
             for {
               _ <- declare(proxy)
               _ <- write(in.Label(proxy)(src))
               s <- goS(l.stmt)
             } yield s
+          }
 
           case PIfStmt(ifs, els) =>
             val elsStmt = maybeStmtD(ctx)(els)(src)
@@ -835,22 +836,31 @@ object Desugar {
               }
             ))
 
-          case PForStmt(pre, cond, post, spec, body) =>
+          case n@PForStmt(pre, cond, post, spec, body) =>
             unit(block( // is a block because 'pre' might define new variables
               for {
                 dPre <- maybeStmtD(ctx)(pre)(src)
                 (dCondPre, dCond) <- prelude(exprD(ctx)(cond))
                 (dInvPre, dInv) <- prelude(sequence(spec.invariants map assertionD(ctx)))
                 (dTerPre, dTer) <- prelude(option(spec.terminationMeasure map terminationMeasureD(ctx)))
 
+                continueLabelName = nm.continueLabel(n, info)
+                continueLoopLabelProxy = in.LabelProxy(continueLabelName)(src)
+                continueLoopLabel = in.Label(continueLoopLabelProxy)(src)
+
+                breakLabelName = nm.breakLabel(n, info)
+                breakLoopLabelProxy = in.LabelProxy(breakLabelName)(src)
+                _ <- declare(breakLoopLabelProxy)
+                breakLoopLabel = in.Label(breakLoopLabelProxy)(src)
+
                 dBody = blockD(ctx)(body)
                 dPost <- maybeStmtD(ctx)(post)(src)
 
                 wh = in.Seqn(
                   Vector(dPre) ++ dCondPre ++ dInvPre ++ dTerPre ++ Vector(
-                    in.While(dCond, dInv, dTer, in.Seqn(
-                      Vector(dBody, dPost) ++ dCondPre ++ dInvPre ++ dTerPre
-                    )(src))(src)
+                    in.While(dCond, dInv, dTer, in.Block(Vector(continueLoopLabelProxy),
+                      Vector(dBody, continueLoopLabel, dPost) ++ dCondPre ++ dInvPre ++ dTerPre
+                    )(src))(src), breakLoopLabel
                   )
                 )(src)
               } yield wh
@@ -1044,6 +1054,10 @@ object Desugar {
               }
             } yield in.Seqn(Vector(dPre, exprAss, clauseBody))(src)
 
+          case n@PContinue(label) => unit(in.Continue(label.map(x => x.name), nm.fetchContinueLabel(n, info))(src))
+
+          case n@PBreak(label) => unit(in.Break(label.map(x => x.name), nm.fetchBreakLabel(n, info))(src))
+
           case _ => ???
         }
       }
@@ -3115,6 +3129,8 @@ object Desugar {
     private val LABEL_PREFIX = "L"
     private val GLOBAL_PREFIX = "G"
     private val BUILTIN_PREFIX = "B"
+    private val CONTINUE_LABEL_SUFFIX = "$Continue"
+    private val BREAK_LABEL_SUFFIX = "$Break"
 
     /** the counter to generate fresh names depending on the current code root for which a fresh name should be generated */
     private var nonceCounter: Map[PCodeRoot, Int] = Map.empty
@@ -3188,6 +3204,61 @@ object Desugar {
       f
     }
 
+    /**
+      * Returns a unique id for a for loop node with respect to its code root.
+      * The id is of the form 'L_<a>_<b>' where a is the difference of the lines
+      * of the for loop with the code root and b is the difference of the columns
+      * of the for loop with the code root.
+      * If a differce is negative, the '-' character is replaced with '_'.
+      *
+      * @param loop the for loop we are interested in
+      * @param info type info to get position information
+      * @return     string
+      */
+    private def loopId(loop: PForStmt, info: TypeInfo) : String = {
+      val pom = info.getTypeInfo.tree.originalRoot.positions
+      val lpos = pom.positions.getStart(loop).get
+      val rpos = pom.positions.getStart(info.codeRoot(loop)).get
+      return ("L_" + (lpos.line - rpos.line) + "_" + (lpos.column - rpos.column)).replace("-", "_")
+    }
+
+    /** returns the loopId with the CONTINUE_LABEL_SUFFIX appended */
+    def continueLabel(loop: PForStmt, info: TypeInfo) : String = loopId(loop, info) + CONTINUE_LABEL_SUFFIX
+
+    /** returns the loopId with the BREAK_LABEL_SUFFIX appended */
+    def breakLabel(loop: PForStmt, info: TypeInfo) : String = loopId(loop, info) + BREAK_LABEL_SUFFIX
+
+    /**
+      * Finds the enclosing loop which the continue statement refers to and fetches its
+      * continue label.
+      */
+    def fetchContinueLabel(n: PContinue, info: TypeInfo) : String = {
+      n.label match {
+        case None =>
+          val Some(loop) = info.enclosingLoopNode(n)
+          continueLabel(loop, info)
+        case Some(label) =>
+          val Some(loop) = info.enclosingLabeledLoopNode(label, n)
+          continueLabel(loop, info)
+      }
+    }
+
+    /**
+      * Finds the enclosing loop which the break statement refers to and fetches its
+      * break label.
+      */
+    def fetchBreakLabel(n: PBreak, info: TypeInfo) : String = {
+      n.label match {
+        case None =>
+          val Some(loop) = info.enclosingLoopNode(n)
+          breakLabel(loop, info)
+        case Some(label) =>
+          val Some(loop) = info.enclosingLabeledLoopNode(label, n)
+          breakLabel(loop, info)
+      }
+    }
+
+
     def inParam(idx: Int, s: PScope, context: ExternalTypeInfo): String = name(IN_PARAMETER_PREFIX)("P" + idx, s, context)
     def outParam(idx: Int, s: PScope, context: ExternalTypeInfo): String = name(OUT_PARAMETER_PREFIX)("P" + idx, s, context)
     def receiver(s: PScope, context: ExternalTypeInfo): String = name(RECEIVER_PREFIX)("R", s, context)

src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala

@@ -6,13 +6,14 @@
 
 package viper.gobra.frontend.info
 
-import viper.gobra.ast.frontend.{PCodeRoot, PEmbeddedDecl, PExpression, PFieldDecl, PIdnNode, PIdnUse, PKeyedElement, PMPredicateDecl, PMPredicateSig, PMember, PMethodDecl, PMethodSig, PMisc, PNode, PParameter, PPkgDef, PScope, PType}
+import viper.gobra.ast.frontend.{PCodeRoot, PEmbeddedDecl, PExpression, PFieldDecl, PIdnNode, PIdnUse, PKeyedElement, PMPredicateDecl, PMPredicateSig, PMember, PMethodDecl, PMethodSig, PMisc, PNode, PParameter, PPkgDef, PScope, PType, PLabelUse}
 import viper.gobra.frontend.PackageInfo
 import viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInMemberTag
 import viper.gobra.frontend.info.base.Type.{AbstractType, InterfaceT, StructT, Type}
 import viper.gobra.frontend.info.base.SymbolTable.{Embbed, Field, MPredicateImpl, MPredicateSpec, MethodImpl, MethodSpec, Regular, TypeMember}
 import viper.gobra.frontend.info.implementation.resolution.{AdvancedMemberSet, MemberPath}
 import viper.gobra.frontend.info.implementation.typing.ghost.separation.GhostType
+import viper.gobra.ast.frontend.PForStmt
 
 trait ExternalTypeInfo {
 
@@ -92,4 +93,10 @@ trait ExternalTypeInfo {
 
   /** returns the code root for a given node; can only be called on nodes that are enclosed in a code root */
   def codeRoot(n: PNode): PCodeRoot with PScope
+
+  /** if it exists, it returns the for loop node that contains 'n' with label 'label' */
+  def enclosingLabeledLoopNode(label: PLabelUse, n: PNode) : Option[PForStmt]
+
+  /** if it exists, it returns the for loop node that contains 'n' */
+  def enclosingLoopNode(n: PNode) : Option[PForStmt]
 }

src/main/scala/viper/gobra/frontend/info/implementation/Errors.scala

@@ -29,6 +29,7 @@ trait Errors { this: TypeInfoImpl =>
           //        case n: PIdnUnk if isDef(n) => wellDefID(n).out
           case n: PMisc       => wellDefMisc(n).out
           case n: PSpecification => wellDefSpec(n).out
+          case n: PLabelNode => wellDefLabel(n).out
           case _ => noMessages
         }
 

src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala

@@ -83,6 +83,10 @@ class TypeInfoImpl(final val tree: Info.GoTree, final val context: Info.Context,
 
   override def codeRoot(n: PNode): PCodeRoot with PScope = enclosingCodeRoot(n)
 
+  override def enclosingLabeledLoopNode(label: PLabelUse, n: PNode) : Option[PForStmt] = enclosingLabeledLoop(label, n)
+
+  override def enclosingLoopNode(n: PNode) : Option[PForStmt] = enclosingLoop(n)
+
   override def regular(n: PIdnNode): SymbolTable.Regular = entity(n) match {
     case r: Regular => r
     case _ => violation("found non-regular entity")

src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala

@@ -30,6 +30,23 @@ trait Enclosing { this: TypeInfoImpl =>
     case _ => id
   })
 
+  lazy val enclosingLoop: PNode => Option[PForStmt] = {
+    down[Option[PForStmt]](None){ case x: PForStmt => Some(x) }
+  }
+
+  // Returns the enclosing loop that has a specific label
+  // It also returns the invariants of that loop
+  def enclosingLabeledLoop(label: PLabelUse, node: PNode) : Option[PForStmt] = {
+    enclosingLoop(node) match {
+      case None => None
+      case Some(encLoop) => encLoop match {
+        case tree.parent(l: PLabeledStmt) if l.label.name == label.name => Some(encLoop)
+        case tree.parent(p) => enclosingLabeledLoop(label, p)
+        case _ => violation("No parent found for a loop statement.")
+      }
+    }
+  }
+
   lazy val tryEnclosingUnorderedScope: PNode => Option[PUnorderedScope] =
     down[Option[PUnorderedScope]](None) { case x: PUnorderedScope => Some(x) }