do continue/break encoding in constructors, but do not generate return

src/col/vct/col/ast/statement/exceptional/ExceptionalStatementImpl.scala

@@ -1,7 +1,8 @@
 package vct.col.ast.statement.exceptional
 
 import vct.col.ast.ExceptionalStatement
+import vct.col.ast.statement.StatementImpl
 
-trait ExceptionalStatementImpl[G] { this: ExceptionalStatement[G] =>
+trait ExceptionalStatementImpl[G] extends StatementImpl[G] { this: ExceptionalStatement[G] =>
 
 }

src/col/vct/col/ast/statement/exceptional/ReturnImpl.scala

@@ -1,10 +1,19 @@
 package vct.col.ast.statement.exceptional
 
-import vct.col.ast.{Return, Void}
-import vct.col.print.{Ctx, Doc, Text, Empty}
+import vct.col.ast.{AbstractMethod, Constructor, Return, Void}
+import vct.col.print.{Ctx, Doc, Empty, Text}
 import vct.col.ast.ops.ReturnOps
+import vct.col.check.{CheckContext, CheckError, ReturnOutsideMethod}
+
+trait ReturnImpl[G] extends ExceptionalStatementImpl[G] with ReturnOps[G] { this: Return[G] =>
+  override def check(context: CheckContext[G]): Seq[CheckError] =
+    super.check(context) ++ (context.currentApplicable match {
+      case None => Seq(ReturnOutsideMethod(this))
+      case Some(_: Constructor[G]) => Seq(ReturnOutsideMethod(this))
+      case Some(_: AbstractMethod[G]) => Nil
+      case Some(_) => Seq(ReturnOutsideMethod(this))
+    })
 
-trait ReturnImpl[G] extends ReturnOps[G] { this: Return[G] =>
   override def layout(implicit ctx: Ctx): Doc =
     Text("return") <> (if(result == Void[G]()) Text(";") else Empty <+> result <> ";")
 }

src/col/vct/col/check/Check.scala

@@ -63,6 +63,8 @@ sealed trait CheckError {
         Seq(context(clause) -> "This catch clause is redundant, because it is subsumed by the caught types of earlier catch clauses in this block.")
       case ResultOutsidePostcondition(res) =>
         Seq(context(res) -> "\\result may only occur in the postcondition.")
+      case ReturnOutsideMethod(ret) =>
+        Seq(context(ret) -> "return may only occur in methods and procedures.")
       case FinalPermission(loc) =>
         Seq(context(loc) -> "Specifying permission over final fields is not allowed, since they are treated as constants.")
       case SeqProgStatement(s) =>
@@ -126,6 +128,9 @@ case class RedundantCatchClause(clause: CatchClause[_]) extends CheckError {
 case class ResultOutsidePostcondition(res: Expr[_]) extends CheckError {
   val subcode = "resultOutsidePostcondition"
 }
+case class ReturnOutsideMethod(ret: Return[_]) extends CheckError {
+  val subcode = "resultOutsideMethod"
+}
 case class FinalPermission(loc: FieldLocation[_]) extends CheckError {
   override def subcode: String = "finalPerm"
 }

src/hre/hre/stages/Stages.scala

@@ -23,9 +23,9 @@ trait Stages[-Input, +Output] {
       Progress.stages(flatNames) { progressNext =>
         var cur: Any = in
 
-        for(stage <- stages) {
+        for((stage, idx) <- stages.zipWithIndex) {
+          if(idx > 0) progressNext()
           cur = stage.run(cur)
-          progressNext()
         }
 
         Right(cur.asInstanceOf[Output])

src/rewrite/vct/rewrite/exc/EncodeBreakReturn.scala

@@ -62,7 +62,15 @@ case class EncodeBreakReturn[Pre <: Generation]() extends Rewriter[Pre] {
       case _ => false
     }
 
-  case class BreakReturnToGoto(returnTarget: LabelDecl[Post], resultVariable: Local[Post]) extends Rewriter[Pre] {
+  def needReturn(method: AbstractMethod[Pre]): Boolean =
+    method match {
+      case procedure: Procedure[Pre] => true
+      case constructor: Constructor[Pre] => false
+      case method: InstanceMethod[Pre] => true
+      case method: InstanceOperatorMethod[Pre] => true
+    }
+
+  case class BreakReturnToGoto(returnTarget: Option[LabelDecl[Post]], resultVariable: Option[Local[Post]]) extends Rewriter[Pre] {
     val breakLabels: mutable.Set[LabelDecl[Pre]] = mutable.Set()
     val postLabeledStatement: SuccessionMap[LabelDecl[Pre], LabelDecl[Post]] = SuccessionMap()
 
@@ -97,16 +105,16 @@ case class EncodeBreakReturn[Pre <: Generation]() extends Rewriter[Pre] {
 
         case Return(result) =>
           Block(Seq(
-            assignLocal(resultVariable, dispatch(result)),
-            Goto(returnTarget.ref),
+            assignLocal(resultVariable.get, dispatch(result)),
+            Goto(returnTarget.get.ref),
           ))
 
         case other => rewriteDefault(other)
       }
     }
   }
 
-  case class BreakReturnToException(returnClass: Class[Post], valueField: InstanceField[Post]) extends Rewriter[Pre] {
+  case class BreakReturnToException(returnClass: Option[Class[Post]], valueField: Option[InstanceField[Post]]) extends Rewriter[Pre] {
     val breakLabelException: SuccessionMap[LabelDecl[Pre], Class[Post]] = SuccessionMap()
 
     override val allScopes: AllScopes[Pre, Post] = EncodeBreakReturn.this.allScopes
@@ -143,10 +151,10 @@ case class EncodeBreakReturn[Pre <: Generation]() extends Rewriter[Pre] {
           Throw(NewObject[Post](cls.ref))(PanicBlame("The result of NewObject is never null"))
 
         case Return(result) =>
-          val exc = new Variable[Post](TClass(returnClass.ref))
+          val exc = new Variable[Post](TClass(returnClass.get.ref))
           Scope(Seq(exc), Block(Seq(
-            assignLocal(exc.get, NewObject(returnClass.ref)),
-            assignField(exc.get, valueField.ref, dispatch(result), PanicBlame("Have write permission immediately after NewObject")),
+            assignLocal(exc.get, NewObject(returnClass.get.ref)),
+            assignField(exc.get, valueField.get.ref, dispatch(result), PanicBlame("Have write permission immediately after NewObject")),
             Throw(exc.get)(PanicBlame("The result of NewObject is never null")),
           )))
 
@@ -156,38 +164,47 @@ case class EncodeBreakReturn[Pre <: Generation]() extends Rewriter[Pre] {
   }
 
   override def dispatch(decl: Declaration[Pre]): Unit = decl match {
-    case cons: Constructor[Pre] =>
-      rewriteDefault(cons)
     case method: AbstractMethod[Pre] =>
       method.body match {
         case None => rewriteDefault(method)
         case Some(body) =>
           allScopes.anyDeclare(allScopes.anySucceedOnly(method, method.rewrite(body = Some({
             if (needBreakReturnExceptions(body)) {
               implicit val o: Origin = body.o
-              val returnField = new InstanceField[Post](dispatch(method.returnType), Nil)(ReturnField)
-              val returnClass = new Class[Post](Seq(returnField), Nil, tt)(ReturnClass)
-              globalDeclarations.declare(returnClass)
-
-              val caughtReturn = new Variable[Post](TClass(returnClass.ref))
-
-              TryCatchFinally(
-                body = BreakReturnToException(returnClass, returnField).dispatch(body),
-                catches = Seq(CatchClause(caughtReturn,
-                  Return(Deref[Post](caughtReturn.get, returnField.ref)(PanicBlame("Permission for the field of a return exception cannot be non-write, as the class is only instantiated at a return site, and caught immediately.")))
-                )),
-                after = Block(Nil)
-              )
+
+              if(needReturn(method)) {
+                val returnField = new InstanceField[Post](dispatch(method.returnType), Nil)(ReturnField)
+                val returnClass = new Class[Post](Seq(returnField), Nil, tt)(ReturnClass)
+                globalDeclarations.declare(returnClass)
+
+                val caughtReturn = new Variable[Post](TClass(returnClass.ref))
+
+                TryCatchFinally(
+                  body = BreakReturnToException(Some(returnClass), Some(returnField)).dispatch(body),
+                  catches = Seq(CatchClause(caughtReturn,
+                    Return(Deref[Post](caughtReturn.get, returnField.ref)(PanicBlame("Permission for the field of a return exception cannot be non-write, as the class is only instantiated at a return site, and caught immediately.")))
+                  )),
+                  after = Block(Nil)
+                )
+              } else {
+                BreakReturnToException(None, None).dispatch(body)
+              }
             } else {
-              val resultTarget = new LabelDecl[Post]()(ReturnTarget)
-              val resultVar = new Variable(dispatch(method.returnType))(ReturnVariable)
-              val newBody = BreakReturnToGoto(resultTarget, resultVar.get(ReturnVariable)).dispatch(body)
               implicit val o: Origin = body.o
-              Scope(Seq(resultVar), Block(Seq(
-                newBody,
-                Label(resultTarget, Block(Nil)),
-                Return(resultVar.get),
-              )))
+
+              if(needReturn(method)) {
+                val resultTarget = new LabelDecl[Post]()(ReturnTarget)
+                val resultVar = new Variable(dispatch(method.returnType))(ReturnVariable)
+                val newBody = BreakReturnToGoto(Some(resultTarget), Some(resultVar.get(ReturnVariable))).dispatch(body)
+
+                Scope(Seq(resultVar), Block(Seq(
+                  newBody,
+                  Label(resultTarget, Block(Nil)),
+                  Return(resultVar.get),
+                )))
+              } else {
+                BreakReturnToGoto(None, None).dispatch(body)
+              }
             }
           }))))
       }