Simple defer

src/main/antlr4/GobraParser.g4

@@ -299,6 +299,9 @@ specForStmt: loopSpec forStmt;
 
 loopSpec: (INV expression eos)* (DEC terminationMeasure eos)?;
 
+deferStmt:
+  DEFER expression
+  | DEFER fold_stmt=(FOLD | UNFOLD) predicateAccess;
 
 // Added true, false as literals
 basicLit:

src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java

@@ -599,6 +599,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitLoopSpec(GobraParser.LoopSpecContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitDeferStmt(GobraParser.DeferStmtContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -991,13 +998,6 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitFallthroughStmt(GobraParser.FallthroughStmtContext ctx) { return visitChildren(ctx); }
-	/**
-	 * {@inheritDoc}
-	 *
-	 * <p>The default implementation returns the result of calling
-	 * {@link #visitChildren} on {@code ctx}.</p>
-	 */
-	@Override public T visitDeferStmt(GobraParser.DeferStmtContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *

src/main/java/viper/gobra/frontend/GobraParserVisitor.java

@@ -530,6 +530,12 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitLoopSpec(GobraParser.LoopSpecContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#deferStmt}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitDeferStmt(GobraParser.DeferStmtContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#basicLit}.
 	 * @param ctx the parse tree
@@ -880,12 +886,6 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitFallthroughStmt(GobraParser.FallthroughStmtContext ctx);
-	/**
-	 * Visit a parse tree produced by {@link GobraParser#deferStmt}.
-	 * @param ctx the parse tree
-	 * @return the visitor result
-	 */
-	T visitDeferStmt(GobraParser.DeferStmtContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#ifStmt}.
 	 * @param ctx the parse tree

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -259,6 +259,9 @@ case class PShortForRange(range: PRange, shorts: Vector[PIdnUnk], body: PBlock)
 
 case class PGoStmt(exp: PExpression) extends PActualStatement
 
+sealed trait PDeferrable extends PNode
+case class PDeferStmt(exp: PDeferrable) extends PActualStatement
+
 case class PSelectStmt(send: Vector[PSelectSend], rec: Vector[PSelectRecv], aRec: Vector[PSelectAssRecv], sRec: Vector[PSelectShortRecv], dflt: Vector[PSelectDflt]) extends PActualStatement with PScope
 
 sealed trait PSelectClause extends PNode
@@ -281,8 +284,6 @@ case class PContinue(label: Option[PLabelUse]) extends PActualStatement
 
 case class PGoto(label: PLabelUse) extends PActualStatement
 
-case class PDeferStmt(exp: PExpression) extends PActualStatement
-
 // case class PFallThrough() extends PStatement
 
 
@@ -316,7 +317,7 @@ case class POutline(body: PStatement, spec: PFunctionSpec) extends PActualStatem
 sealed trait PExpressionOrType extends PNode
 sealed trait PExpressionAndType extends PNode with PExpression with PType
 
-sealed trait PExpression extends PNode with PExpressionOrType
+sealed trait PExpression extends PNode with PExpressionOrType with PDeferrable
 
 sealed trait PActualExpression extends PExpression
 
@@ -899,9 +900,9 @@ case class PExhale(exp: PExpression) extends PGhostStatement
 
 case class PInhale(exp: PExpression) extends PGhostStatement
 
-case class PFold(exp: PPredicateAccess) extends PGhostStatement
+case class PFold(exp: PPredicateAccess) extends PGhostStatement with PDeferrable
 
-case class PUnfold(exp: PPredicateAccess) extends PGhostStatement
+case class PUnfold(exp: PPredicateAccess) extends PGhostStatement with PDeferrable
 
 case class PPackageWand(wand: PMagicWand, proofScript: Option[PBlock]) extends PGhostStatement
 

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

@@ -247,7 +247,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PBreak(label) => "break" <> opt(label)(space <> showLabel(_))
       case PContinue(label) => "continue" <> opt(label)(space <> showLabel(_))
       case PGoto(label) => "goto" <+> showLabel(label)
-      case PDeferStmt(exp) => "defer" <+> showExpr(exp)
+      case PDeferStmt(exp: PExpression) => "defer" <+> showExpr(exp)
+      case PDeferStmt(exp: PStatement) => "defer" <+> showStmt(exp)
       case PBlock(stmts) => block(showStmtList(stmts))
       case PSeq(stmts) => showStmtList(stmts)
       case POutline(body, spec) => showSpec(spec) <> "outline" <> parens(nest(line <> showStmt(body)) <> line)

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

@@ -246,6 +246,11 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   // statements
 
   def showStmt(s: Stmt): Doc = updatePositionStore(s) <> (s match {
+    case s: MethodBody =>
+      "decl" <+> showBlockDeclList(s.decls) <> line <>
+        showStmtList(s.seqn.stmts) <> line <>
+        showStmtList(s.postprocessing)
+    case s: MethodBodySeqn => showStmtList(s.stmts)
     case Block(decls, stmts) => "decl" <+> showBlockDeclList(decls) <> line <> showStmtList(stmts)
     case Seqn(stmts) => ssep(stmts map showStmt, line)
     case Label(label) => showProxy(label)
@@ -288,6 +293,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case GoMethodCall(recv, meth, args) =>
       "go" <+> showExpr(recv) <> "." <>  meth.name <> parens(showExprList(args))
 
+    case s: Defer => "defer" <+> showStmt(s.stmt)
+
     case Return() => "return"
     case Assert(ass) => "assert" <+> showAss(ass)
     case Assume(ass) => "assume" <+> showAss(ass)
@@ -653,6 +660,8 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
   // statements
 
   override def showStmt(s: Stmt): Doc = s match {
+    case s: MethodBody => "decl" <+> showBlockDeclList(s.decls)
+    case _: MethodBodySeqn => emptyDoc
     case Block(decls, _) => "decl" <+> showBlockDeclList(decls)
     case Seqn(_) => emptyDoc
     case Label(label) => showProxy(label)
@@ -698,6 +707,8 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
     case GoMethodCall(recv, meth, args) =>
       "go" <+> showExpr(recv) <> "." <> meth.name <> parens(showExprList(args))
 
+    case s: Defer => "defer" <+> showStmt(s.stmt)
+
     case Return() => "return"
     case Assert(ass) => "assert" <+> showAss(ass)
     case Assume(ass) => "assume" <+> showAss(ass)

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

@@ -129,7 +129,7 @@ case class Method(
                  override val pres: Vector[Assertion],
                  override val posts: Vector[Assertion],
                  override val terminationMeasures: Vector[TerminationMeasure],
-                 body: Option[Block]
+                 body: Option[MethodBody]
                  )(val info: Source.Parser.Info) extends Member with MethodMember
 
 case class PureMethod(
@@ -185,7 +185,7 @@ case class Function(
                      override val pres: Vector[Assertion],
                      override val posts: Vector[Assertion],
                      override val terminationMeasures: Vector[TerminationMeasure],
-                     body: Option[Block]
+                     body: Option[MethodBody]
                    )(val info: Source.Parser.Info) extends Member with FunctionMember
 
 case class PureFunction(
@@ -259,13 +259,27 @@ case class DomainFunc(
                        results: Parameter.Out
                      )(val info: Source.Parser.Info) extends Node
 
-
 sealed trait Stmt extends Node
 
+/** This node serves as a target of encoding extensions. See [[viper.gobra.translator.encodings.combinators.TypeEncoding.Extension]]*/
+case class MethodBody(
+                       decls: Vector[BlockDeclaration],
+                       seqn: MethodBodySeqn,
+                       postprocessing: Vector[Stmt] = Vector.empty,
+                     )(val info: Source.Parser.Info) extends Stmt
+
+/**
+  * This node serves as a target of encoding extensions. See [[viper.gobra.translator.encodings.combinators.TypeEncoding.Extension]]
+  * Return statements jump exactly to the end of the encoding of this statement.
+  * */
+case class MethodBodySeqn(stmts: Vector[Stmt])(val info: Source.Parser.Info) extends Stmt
+
 case class Block(
                   decls: Vector[BlockDeclaration],
                   stmts: Vector[Stmt]
-                )(val info: Source.Parser.Info) extends Stmt
+                )(val info: Source.Parser.Info) extends Stmt {
+  def toMethodBody: MethodBody = MethodBody(decls, MethodBodySeqn(stmts)(info))(info)
+}
 
 case class Seqn(stmts: Vector[Stmt])(val info: Source.Parser.Info) extends Stmt
 
@@ -336,26 +350,30 @@ case class New(target: LocalVar, expr: Expr)(val info: Source.Parser.Info) exten
   * */
 case class SafeTypeAssertion(resTarget: LocalVar, successTarget: LocalVar, expr: Expr, typ: Type)(val info: Source.Parser.Info) extends Stmt
 
-case class FunctionCall(targets: Vector[LocalVar], func: FunctionProxy, args: Vector[Expr])(val info: Source.Parser.Info) extends Stmt
-case class MethodCall(targets: Vector[LocalVar], recv: Expr, meth: MethodProxy, args: Vector[Expr])(val info: Source.Parser.Info) extends Stmt
+
+case class FunctionCall(targets: Vector[LocalVar], func: FunctionProxy, args: Vector[Expr])(val info: Source.Parser.Info) extends Stmt with Deferrable
+case class MethodCall(targets: Vector[LocalVar], recv: Expr, meth: MethodProxy, args: Vector[Expr])(val info: Source.Parser.Info) extends Stmt with Deferrable
 case class GoFunctionCall(func: FunctionProxy, args: Vector[Expr])(val info: Source.Parser.Info) extends Stmt
 case class GoMethodCall(recv: Expr, meth: MethodProxy, args: Vector[Expr])(val info: Source.Parser.Info) extends Stmt
 
+sealed trait Deferrable extends Stmt
+case class Defer(stmt: Deferrable)(val info: Source.Parser.Info) extends Stmt
+
 case class Return()(val info: Source.Parser.Info) extends Stmt
 
 case class Assert(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
 case class Assume(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
 case class Inhale(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
 case class Exhale(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
 
-case class Fold(acc: Access)(val info: Source.Parser.Info) extends Stmt {
+case class Fold(acc: Access)(val info: Source.Parser.Info) extends Stmt with Deferrable {
   require(acc.e.isInstanceOf[Accessible.Predicate])
   lazy val op: PredicateAccess = acc.e.asInstanceOf[Accessible.Predicate].op
 }
 
 
 
-case class Unfold(acc: Access)(val info: Source.Parser.Info) extends Stmt {
+case class Unfold(acc: Access)(val info: Source.Parser.Info) extends Stmt with Deferrable {
   require(acc.e.isInstanceOf[Accessible.Predicate])
   lazy val op: PredicateAccess = acc.e.asInstanceOf[Accessible.Predicate].op
 }
@@ -549,8 +567,8 @@ case class PredicateConstructor(proxy: PredicateProxy, proxyT: PredT, args: Vect
 
 case class PredExprInstance(base: Expr, args: Vector[Expr])(val info: Source.Parser.Info) extends Node
 
-case class PredExprFold(base: PredicateConstructor, args: Vector[Expr], p: Expr)(val info: Source.Parser.Info) extends Stmt
-case class PredExprUnfold(base: PredicateConstructor, args: Vector[Expr], p: Expr)(val info: Source.Parser.Info) extends Stmt
+case class PredExprFold(base: PredicateConstructor, args: Vector[Expr], p: Expr)(val info: Source.Parser.Info) extends Stmt with Deferrable
+case class PredExprUnfold(base: PredicateConstructor, args: Vector[Expr], p: Expr)(val info: Source.Parser.Info) extends Stmt with Deferrable
 
 
 /* ** Option type expressions */

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

@@ -75,7 +75,7 @@ object CGEdgesTerminationTransform extends InternalTransform {
                       }
                     )(src)
                   }
-                  val newMember = in.Method(m.receiver, m.name, m.args, m.results, m.pres, m.posts, m.terminationMeasures, Some(newBody))(src)
+                  val newMember = in.Method(m.receiver, m.name, m.args, m.results, m.pres, m.posts, m.terminationMeasures, Some(newBody.toMethodBody))(src)
                   methodsToRemove += m
                   methodsToAdd += newMember
                   definedMethodsDelta += proxy -> newMember

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

@@ -58,11 +58,14 @@ object OverflowChecksTransform extends InternalTransform {
   }
 
   /**
-    * Adds overflow checks to the body of a block.
+    * Adds overflow checks to the body of a method.
     */
-  private def computeNewBody(body: Block): Block = {
-    val blockStmts = body.stmts map stmtTransform
-    Block(body.decls, blockStmts)(body.info)
+  private def computeNewBody(body: MethodBody): MethodBody = {
+    MethodBody(
+      body.decls,
+      MethodBodySeqn(body.seqn.stmts map stmtTransform)(body.seqn.info),
+      body.postprocessing map stmtTransform,
+    )(body.info)
   }
 
   /**
@@ -112,6 +115,10 @@ object OverflowChecksTransform extends InternalTransform {
     case m@GoMethodCall(recv, _, args) =>
       Seqn(genOverflowChecksExprs(recv +: args) :+ m)(m.info)
 
+    case d@Defer(FunctionCall(_, _, args)) => Seqn(genOverflowChecksExprs(args) :+ d)(d.info)
+    case d@Defer(MethodCall(_, recv, _, args)) => Seqn(genOverflowChecksExprs(recv +: args) :+ d)(d.info)
+    case d@Defer(_: Fold | _: Unfold | _: PredExprFold | _: PredExprUnfold) => d
+
     case m@Send(_, expr, _, _, _) =>
       Seqn(genOverflowChecksExprs(Vector(expr)) :+ m)(m.info)
 

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

@@ -23,9 +23,9 @@ object GobraStrategy {
     val node: Node = (x, args) match {
         // Members
       case (p: Program, Seq(t: Vector[TopType@unchecked], m: Vector[Member@unchecked])) => Program(t, m, p.table)(meta)
-      case (_: Method, Seq(rec: Parameter.In, name: MethodProxy, arg: Vector[Parameter.In@unchecked], res: Vector[Parameter.Out@unchecked], pre: Vector[Assertion@unchecked], post: Vector[Assertion@unchecked], terminationMeasures: Vector[TerminationMeasure@unchecked], b: Option[Block@unchecked])) => Method(rec, name, arg, res, pre, post, terminationMeasures, b)(meta)
+      case (_: Method, Seq(rec: Parameter.In, name: MethodProxy, arg: Vector[Parameter.In@unchecked], res: Vector[Parameter.Out@unchecked], pre: Vector[Assertion@unchecked], post: Vector[Assertion@unchecked], terminationMeasures: Vector[TerminationMeasure@unchecked], b: Option[MethodBody@unchecked])) => Method(rec, name, arg, res, pre, post, terminationMeasures, b)(meta)
       case (_: PureMethod, Seq(rec: Parameter.In, name: MethodProxy, arg: Vector[Parameter.In@unchecked], res: Vector[Parameter.Out@unchecked], pre: Vector[Assertion@unchecked], post: Vector[Assertion@unchecked], terminationMeasures: Vector[TerminationMeasure@unchecked], b: Option[Expr@unchecked])) => PureMethod(rec, name, arg, res, pre, post, terminationMeasures, b)(meta)
-      case (_: Function, Seq(name: FunctionProxy, arg: Vector[Parameter.In@unchecked], res: Vector[Parameter.Out@unchecked], pre: Vector[Assertion@unchecked], post: Vector[Assertion@unchecked], terminationMeasures: Vector[TerminationMeasure@unchecked], b: Option[Block@unchecked])) => Function(name, arg, res, pre, post, terminationMeasures, b)(meta)
+      case (_: Function, Seq(name: FunctionProxy, arg: Vector[Parameter.In@unchecked], res: Vector[Parameter.Out@unchecked], pre: Vector[Assertion@unchecked], post: Vector[Assertion@unchecked], terminationMeasures: Vector[TerminationMeasure@unchecked], b: Option[MethodBody@unchecked])) => Function(name, arg, res, pre, post, terminationMeasures, b)(meta)
       case (_: PureFunction, Seq(name: FunctionProxy, arg: Vector[Parameter.In@unchecked], res: Vector[Parameter.Out@unchecked], pre: Vector[Assertion@unchecked], post: Vector[Assertion@unchecked], terminationMeasures: Vector[TerminationMeasure@unchecked], b: Option[Expr@unchecked])) => PureFunction(name, arg, res, pre, post, terminationMeasures, b)(meta)
       case (_: MPredicate, Seq(recv: Parameter.In, name: MPredicateProxy, args: Vector[Parameter.In@unchecked], b: Option[Assertion@unchecked])) => MPredicate(recv, name, args, b)(meta)
       case (_: FPredicate, Seq(name: FPredicateProxy, args: Vector[Parameter.In@unchecked], b: Option[Assertion@unchecked])) => FPredicate(name, args, b)(meta)
@@ -36,6 +36,8 @@ object GobraStrategy {
       case (_: DomainFunc, Seq(name: DomainFuncProxy, args: Vector[Parameter.In@unchecked], res: Parameter.Out)) => DomainFunc(name, args, res)(meta)
       case (_: DomainAxiom, Seq(expr: Expr)) => DomainAxiom(expr)(meta)
         // Statements
+      case (_: MethodBody, Seq(v: Vector[BlockDeclaration@unchecked], s: MethodBodySeqn, p: Vector[Stmt@unchecked])) => MethodBody(v, s, p)(meta)
+      case (_: MethodBodySeqn, Seq(s: Vector[Stmt@unchecked])) => MethodBodySeqn(s)(meta)
       case (_: Block, Seq(v: Vector[BlockDeclaration@unchecked], s: Vector[Stmt@unchecked])) => Block(v, s)(meta)
       case (_: Seqn, Seq(stmts: Vector[Stmt@unchecked])) => Seqn(stmts)(meta)
       case (_: Label, Seq(label: LabelProxy)) => Label(label)(meta)
@@ -55,6 +57,7 @@ object GobraStrategy {
       case (_: Assignee.Index, Seq(e: IndexedExp)) => Assignee.Index(e)
       case (_: FunctionCall, Seq(targets: Vector[LocalVar@unchecked], func: FunctionProxy, args: Vector[Expr@unchecked])) => FunctionCall(targets, func, args)(meta)
       case (_: MethodCall, Seq(targets: Vector[LocalVar@unchecked], recv: Expr, meth: MethodProxy, args: Vector[Expr@unchecked])) => MethodCall(targets, recv, meth, args)(meta)
+      case (_: Defer, Seq(stmt: Deferrable)) => Defer(stmt)(meta)
       case (_: Return, Seq()) => Return()(meta)
       case (_: Assert, Seq(ass: Assertion)) => Assert(ass)(meta)
       case (_: Assume, Seq(ass: Assertion)) => Assume(ass)(meta)

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

@@ -41,6 +41,8 @@ object Nodes {
       case s: Stmt => s match {
         case Break(_, _) => Seq.empty
         case Continue(_, _) => Seq.empty
+        case MethodBody(decls, seqn, postprocessing) => decls ++ Seq(seqn) ++ postprocessing
+        case MethodBodySeqn(stmts) => stmts
         case Block(decls, stmts) => decls ++ stmts
         case Seqn(stmts) => stmts
         case Label(label) => Seq(label)
@@ -69,6 +71,7 @@ object Nodes {
         case SafeTypeAssertion(resTarget, successTarget, expr, _) => Seq(resTarget, successTarget, expr)
         case GoFunctionCall(func, args) => Seq(func) ++ args
         case GoMethodCall(recv, meth, args) => Seq(recv, meth) ++ args
+        case Defer(stmt) => Seq(stmt)
         case SafeReceive(resTarget, successTarget, channel, recvChannel, recvGivenPerm, recvGotPerm, closed) =>
           Seq(resTarget, successTarget, channel, recvChannel, recvGivenPerm, recvGotPerm, closed)
         case Send(channel, expr, sendChannel, sendGivenPerm, sendGotPerm) =>