diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index eb543ed16..29204983e 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/src/main/scala/viper/gobra/ast/frontend/Ast.scala @@ -261,7 +261,9 @@ case class PIfStmt(ifs: Vector[PIfClause], els: Option[PBlock]) extends PActualS case class PIfClause(pre: Option[PSimpleStmt], condition: PExpression, body: PBlock) extends PNode -case class PExprSwitchStmt(pre: Option[PSimpleStmt], exp: PExpression, cases: Vector[PExprSwitchCase], dflt: Vector[PBlock]) extends PActualStatement with PScope with PGhostifiableStatement +sealed trait PBreakableStmt extends PActualStatement + +case class PExprSwitchStmt(pre: Option[PSimpleStmt], exp: PExpression, cases: Vector[PExprSwitchCase], dflt: Vector[PBlock]) extends PBreakableStmt with PScope with PGhostifiableStatement sealed trait PExprSwitchClause extends PNode @@ -269,7 +271,7 @@ case class PExprSwitchDflt(body: PBlock) extends PExprSwitchClause case class PExprSwitchCase(left: Vector[PExpression], body: PBlock) extends PExprSwitchClause -case class PTypeSwitchStmt(pre: Option[PSimpleStmt], exp: PExpression, binder: Option[PIdnDef], cases: Vector[PTypeSwitchCase], dflt: Vector[PBlock]) extends PActualStatement with PScope with PGhostifiableStatement +case class PTypeSwitchStmt(pre: Option[PSimpleStmt], exp: PExpression, binder: Option[PIdnDef], cases: Vector[PTypeSwitchCase], dflt: Vector[PBlock]) extends PBreakableStmt with PScope with PGhostifiableStatement sealed trait PTypeSwitchClause extends PNode @@ -277,7 +279,7 @@ case class PTypeSwitchDflt(body: PBlock) extends PTypeSwitchClause case class PTypeSwitchCase(left: Vector[PExpressionOrType], body: PBlock) extends PTypeSwitchClause -sealed trait PGeneralForStmt extends PActualStatement +sealed trait PGeneralForStmt extends PBreakableStmt case class PForStmt(pre: Option[PSimpleStmt], cond: PExpression, post: Option[PSimpleStmt], spec: PLoopSpec, body: PBlock) extends PGeneralForStmt with PScope with PGhostifiableStatement @@ -290,7 +292,7 @@ case class PGoStmt(exp: PExpression) extends PActualStatement sealed trait PDeferrable extends PNode case class PDeferStmt(exp: PDeferrable) extends PActualStatement with PGhostifiableStatement -case class PSelectStmt(send: Vector[PSelectSend], rec: Vector[PSelectRecv], aRec: Vector[PSelectAssRecv], sRec: Vector[PSelectShortRecv], dflt: Vector[PSelectDflt]) extends PActualStatement with PScope +case class PSelectStmt(send: Vector[PSelectSend], rec: Vector[PSelectRecv], aRec: Vector[PSelectAssRecv], sRec: Vector[PSelectShortRecv], dflt: Vector[PSelectDflt]) extends PBreakableStmt with PScope sealed trait PSelectClause extends PNode diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index 241421109..d28eddd1f 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -4928,11 +4928,11 @@ object Desugar extends LazyLogging { def continueLabel(loop: PGeneralForStmt, info: TypeInfo) : String = relativeId(loop, info) + CONTINUE_LABEL_SUFFIX /** returns the relativeId with the BREAK_LABEL_SUFFIX appended */ - def breakLabel(loop: PGeneralForStmt, info: TypeInfo) : String = relativeId(loop, info) + BREAK_LABEL_SUFFIX + def breakLabel(loop: PBreakableStmt, info: TypeInfo) : String = relativeId(loop, info) + BREAK_LABEL_SUFFIX /** * Finds the enclosing loop which the continue statement refers to and fetches its - * continue label. + * continue label. Note that `continue` always refers to the inner-most for loop. */ def fetchContinueLabel(n: PContinue, info: TypeInfo) : String = { n.label match { @@ -4947,15 +4947,15 @@ object Desugar extends LazyLogging { /** * Finds the enclosing loop which the break statement refers to and fetches its - * break label. + * break label. Note that `break` refers to the inner-most for loop, switch or select statement. */ def fetchBreakLabel(n: PBreak, info: TypeInfo) : String = { n.label match { case None => - val Some(loop) = info.enclosingLoopNode(n) + val Some(loop) = info.enclosingBreakableNode(n) breakLabel(loop, info) case Some(label) => - val Some(loop) = info.enclosingLabeledLoopNode(label, n) + val Some(loop) = info.enclosingBreakableNode(label, n) breakLabel(loop, info) } } diff --git a/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala b/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala index fc72758b5..d5e517362 100644 --- a/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala +++ b/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala @@ -6,7 +6,7 @@ package viper.gobra.frontend.info -import viper.gobra.ast.frontend.{PCodeRoot, PEmbeddedDecl, PExpression, PFieldDecl, PFunctionDecl, PFunctionOrMethodDecl, PGeneralForStmt, PIdnNode, PIdnUse, PKeyedElement, PLabelUse, PMPredicateDecl, PMPredicateSig, PMember, PMethodDecl, PMethodSig, PMisc, PNode, PParameter, PPkgDef, PScope, PType} +import viper.gobra.ast.frontend.{PActualStatement, PBreakableStmt, PCodeRoot, PEmbeddedDecl, PExpression, PFieldDecl, PFunctionDecl, PFunctionOrMethodDecl, PGeneralForStmt, PIdnNode, PIdnUse, PKeyedElement, PLabelUse, PMPredicateDecl, PMPredicateSig, PMember, PMethodDecl, PMethodSig, PMisc, PNode, PParameter, PPkgDef, PScope, PType} import viper.gobra.frontend.PackageInfo import viper.gobra.frontend.PackageResolver.AbstractImport import viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInMemberTag @@ -119,6 +119,12 @@ trait ExternalTypeInfo { /** if it exists, it returns the for loop node that contains 'n' */ def enclosingLoopNode(n: PNode) : Option[PGeneralForStmt] + /** if it exists, it returns the for loop, switch or select node that contains 'n' with label 'label' */ + def enclosingBreakableNode(label: PLabelUse, n: PNode): Option[PBreakableStmt] + + /** if it exists, it returns the for loop, switch or select node that contains 'n' */ + def enclosingBreakableNode(n: PNode): Option[PBreakableStmt] + /** returns the enclosing invariant of 'n' */ def enclosingInvariantNode(n: PExpression) : PExpression diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala index 5ca81f4c4..857df9a81 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala @@ -95,6 +95,10 @@ class TypeInfoImpl(final val tree: Info.GoTree, final val dependentTypeInfo: Map override def enclosingLoopNode(n: PNode) : Option[PGeneralForStmt] = enclosingLoopUntilOutline(n).toOption + override def enclosingBreakableNode(label: PLabelUse, n: PNode): Option[PBreakableStmt] = enclosingLabeledBreakable(label, n).toOption + + override def enclosingBreakableNode(n: PNode): Option[PBreakableStmt] = enclosingBreakableUntilOutline(n).toOption + override def enclosingInvariantNode(n: PExpression) : PExpression = enclosingInvariant(n) override def samePkgDepsOfGlobalVar(n: SymbolTable.GlobalVariable): Vector[SymbolTable.GlobalVariable] = diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala index c25c4c9a3..b589f99d7 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala @@ -50,6 +50,25 @@ trait Enclosing { this: TypeInfoImpl => } } + lazy val enclosingBreakableUntilOutline: PNode => Either[Option[PNode], PBreakableStmt] = { + down[Either[Option[PNode], PBreakableStmt]](Left(None)) { + case x: POutline => Left(Some(x)) + case x: PBreakableStmt => Right(x) + } + } + + // Returns the enclosing breakable statement that has a specific label + def enclosingLabeledBreakable(label: PLabelUse, node: PNode): Either[Option[PNode], PBreakableStmt] = { + enclosingBreakableUntilOutline(node) match { + case Right(breakable) => breakable match { + case tree.parent(l: PLabeledStmt) if l.label.name == label.name => Right(breakable) + case tree.parent(p) => enclosingLabeledBreakable(label, p) + case _ => Left(None) + } + case r => r + } + } + def enclosingInvariant(n: PExpression) : PExpression = { n match { case tree.parent(p) if enclosingExpr(p).isDefined => enclosingExpr(p).get diff --git a/src/test/resources/regressions/issues/000719.gobra b/src/test/resources/regressions/issues/000719.gobra new file mode 100644 index 000000000..f67f6dfbf --- /dev/null +++ b/src/test/resources/regressions/issues/000719.gobra @@ -0,0 +1,16 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue000719 + +decreases +func foo() { + //:: ExpectedOutput(loop_termination_error) + decreases + for i := 0; ; i++ { + switch i { + default: + break + } + } +}