Add support for exhaleMode annotation

src/main/antlr4/GobraLexer.g4

@@ -89,3 +89,6 @@ PROOF       : 'proof';
 GHOST_EQUALS     : '===';
 GHOST_NOT_EQUALS : '!==';
 WITH        : 'with';
+EXHALEMODE  : 'exhaleMode' -> mode(NLSEMI);
+MCE         : 'mce';
+GREEDY      : 'greedy';

src/main/antlr4/GobraParser.g4

@@ -162,7 +162,12 @@ sqType: (kind=(SEQ | SET | MSET | OPT) L_BRACKET type_ R_BRACKET)
 // Specifications
 
 specification returns[boolean trusted = false, boolean pure = false;]:
-  ((specStatement | PURE {$pure = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? // Non-greedily match PURE to avoid missing eos errors.
+  ((specStatement | PURE {$pure = true;} | (EXHALEMODE L_PAREN exhaleMode R_PAREN) | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? // Non-greedily match PURE to avoid missing eos errors.
+  ;
+
+exhaleMode
+  : MCE
+  | GREEDY
   ;
 
 specStatement

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

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.0
+// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 
@@ -376,6 +376,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitSpecification(GobraParser.SpecificationContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitExhaleMode(GobraParser.ExhaleModeContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *

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

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.0
+// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 
@@ -326,6 +326,12 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitSpecification(GobraParser.SpecificationContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#exhaleMode}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitExhaleMode(GobraParser.ExhaleModeContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#specStatement}.
 	 * @param ctx the parse tree

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

@@ -876,13 +876,18 @@ case class PTupleTerminationMeasure(tuple: Vector[PExpression], cond: Option[PEx
 
 sealed trait PSpecification extends PGhostNode
 
+sealed trait PExhaleMode extends PNode
+case class PGreedy() extends PExhaleMode
+case class PMce() extends PExhaleMode
+
 case class PFunctionSpec(
                       pres: Vector[PExpression],
                       preserves: Vector[PExpression],
                       posts: Vector[PExpression],
                       terminationMeasures: Vector[PTerminationMeasure],
+                      exhaleMode: Vector[PExhaleMode],
                       isPure: Boolean = false,
-                      isTrusted: Boolean = false
+                      isTrusted: Boolean = false,
                       ) extends PSpecification
 
 case class PBodyParameterInfo(

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

@@ -50,6 +50,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case n: PInterfaceClause => showInterfaceClause(n)
     case n: PBodyParameterInfo => showBodyParameterInfo(n)
     case n: PTerminationMeasure => showTerminationMeasure(n)
+    case n: PExhaleMode => showExhaleMode(n)
     case PPos(_) => emptyDoc
   }
 
@@ -142,14 +143,20 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     "decreases" <+> measureDoc(measure)
   }
 
+  def showExhaleMode(mode: PExhaleMode): Doc = mode match {
+    case PGreedy() => "greedy"
+    case PMce() => "mce"
+  }
+
   def showSpec(spec: PSpecification): Doc = spec match {
-    case PFunctionSpec(pres, preserves, posts, measures, isPure, isTrusted) =>
+    case PFunctionSpec(pres, preserves, posts, measures, exhaleMode, isPure, isTrusted) =>
       (if (isPure) showPure else emptyDoc) <>
       (if (isTrusted) showTrusted else emptyDoc) <>
       hcat(pres map (showPre(_) <> line)) <>
-        hcat(preserves map (showPreserves(_) <> line)) <>
-        hcat(posts map (showPost(_) <> line)) <>
-        hcat(measures map (showTerminationMeasure(_) <> line))
+      hcat(preserves map (showPreserves(_) <> line)) <>
+      hcat(posts map (showPost(_) <> line)) <>
+      hcat(measures map (showTerminationMeasure(_) <> line)) <>
+      hcat(exhaleMode map (showExhaleMode(_) <> line))
 
     case PLoopSpec(inv, measure) =>
       hcat(inv map (showInv(_) <> line)) <> opt(measure)(showTerminationMeasure) <> line

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

@@ -15,7 +15,6 @@ import viper.silver.ast.{Position => GobraPosition}
 
 import scala.collection.mutable
 import scala.collection.mutable.ListBuffer
-import viper.gobra.util.Violation.violation
 
 trait PrettyPrinter {
   def format(node : Node): String
@@ -144,28 +143,36 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     }
   }
 
+  def showExhaleMode(mode: ExhaleMode): Doc = {
+    val modDoc = mode match {
+      case Mce => "mce"
+      case Greedy => "greedy"
+    }
+    "exhaleMode" <> parens(modDoc) <> line
+  }
+
   def showFunction(f: Function): Doc = f match {
-    case Function(name, args, results, pres, posts, measures, body) =>
+    case Function(name, args, results, pres, posts, measures, exhaleMode, body) =>
       "func" <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block(showStmt(b)))
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block(showStmt(b)))
   }
 
   def showPureFunction(f: PureFunction): Doc = f match {
-    case PureFunction(name, args, results, pres, posts, measures, body) =>
+    case PureFunction(name, args, results, pres, posts, measures, exhaleMode, body) =>
       "pure func" <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block("return" <+> showExpr(b)))
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block("return" <+> showExpr(b)))
   }
 
   def showMethod(m: Method): Doc = m match {
-    case Method(receiver, name, args, results, pres, posts, measures, body) =>
+    case Method(receiver, name, args, results, pres, posts, measures, exhaleMode, body) =>
       "func" <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block(showStmt(b)))
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block(showStmt(b)))
   }
 
   def showPureMethod(m: PureMethod): Doc = m match {
-    case PureMethod(receiver, name, args, results, pres, posts, measures, body) =>
+    case PureMethod(receiver, name, args, results, pres, posts, measures, exhaleMode, body) =>
       "pure func" <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block("return" <+> showExpr(b)))
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block("return" <+> showExpr(b)))
   }
 
   def showMethodSubtypeProof(m: MethodSubtypeProof): Doc = m match {
@@ -350,8 +357,8 @@ 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 Outline(_, pres, posts, measures, body, trusted) =>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <>
+    case Outline(_, pres, posts, measures, exhaleMode, body, trusted) =>
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <>
           "outline" <> (if (trusted) emptyDoc else parens(nest(line <> showStmt(body)) <> line))
     case Continue(l, _) => "continue" <+> opt(l)(text)
     case Break(l, _) => "break" <+> opt(l)(text)
@@ -602,14 +609,17 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case BoolLit(b) => if (b) "true" else "false"
     case NilLit(t) => parens("nil" <> ":" <> showType(t))
 
-    case FunctionLit(name, args, captured, results, pres, posts, measures, body) =>
-      "func" <+> showProxy(name) <> showCaptured(captured) <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <>
+    case FunctionLit(name, args, captured, results, pres, posts, measures, exhaleMode, body) =>
+      "func" <+> showProxy(name) <> showCaptured(captured) <> parens(showFormalArgList(args)) <+>
+        parens(showVarDeclList(results)) <>
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <>
         opt(body)(b => block(showStmt(b)))
 
-    case PureFunctionLit(name, args, captured, results, pres, posts, measures, body) =>
-      "pure func" <+> showProxy(name)  <> showCaptured(captured) <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block("return" <+> showExpr(b)))
+    case PureFunctionLit(name, args, captured, results, pres, posts, measures, exhaleMode, body) =>
+      "pure func" <+> showProxy(name)  <> showCaptured(captured) <> parens(showFormalArgList(args)) <+>
+        parens(showVarDeclList(results)) <>
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <>
+        opt(body)(b => block("return" <+> showExpr(b)))
 
     case ArrayLit(len, typ, elems) => {
       val lenP = brackets(len.toString)
@@ -675,27 +685,27 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
 
 
   override def showFunction(f: Function): Doc = f match {
-    case Function(name, args, results, pres, posts, measures, _) =>
+    case Function(name, args, results, pres, posts, measures, exhaleMode, _) =>
       "func" <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
   }
 
   override def showPureFunction(f: PureFunction): Doc = f match {
-    case PureFunction(name, args, results, pres, posts, measures, _) =>
+    case PureFunction(name, args, results, pres, posts, measures, exhaleMode, _) =>
       "pure func" <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
   }
 
   override def showMethod(m: Method): Doc = m match {
-    case Method(receiver, name, args, results, pres, posts, measures, _) =>
+    case Method(receiver, name, args, results, pres, posts, measures, exhaleMode, _) =>
       "func" <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
   }
 
   override def showPureMethod(m: PureMethod): Doc = m match {
-    case PureMethod(receiver, name, args, results, pres, posts, measures, _) =>
+    case PureMethod(receiver, name, args, results, pres, posts, measures, exhaleMode, _) =>
       "pure func" <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
+        spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
   }
 
   override def showFPredicate(predicate: FPredicate): Doc = predicate match {
@@ -787,8 +797,8 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
     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)
-    case Outline(_, pres, posts, measures, _, _) =>
-      spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <>
+    case Outline(_, pres, posts, measures, exhaleMode, _, _) =>
+      spec(opt(exhaleMode)(showExhaleMode) <> showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <>
         "outline"
   }
 }

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

@@ -136,6 +136,10 @@ sealed trait BuiltInMember extends Member {
   def argsT: Vector[Type]
 }
 
+sealed trait ExhaleMode
+case object Greedy extends ExhaleMode
+case object Mce extends ExhaleMode
+
 sealed trait MethodLikeMember extends Member {
   def name: MethodProxy
 }
@@ -146,6 +150,7 @@ sealed trait MethodMember extends MethodLikeMember {
   def results: Vector[Parameter.Out]
   def pres: Vector[Assertion]
   def posts: Vector[Assertion]
+  def exhaleMode: Option[ExhaleMode]
   def terminationMeasures: Vector[TerminationMeasure]
 }
 
@@ -158,6 +163,7 @@ sealed trait FunctionLikeMemberOrLit extends Node {
   def results: Vector[Parameter.Out]
   def pres: Vector[Assertion]
   def posts: Vector[Assertion]
+  def exhaleMode: Option[ExhaleMode]
   def terminationMeasures: Vector[TerminationMeasure]
 }
 
@@ -185,7 +191,8 @@ case class Method(
                  override val pres: Vector[Assertion],
                  override val posts: Vector[Assertion],
                  override val terminationMeasures: Vector[TerminationMeasure],
-                 body: Option[MethodBody]
+                 override val exhaleMode: Option[ExhaleMode],
+                 body: Option[MethodBody],
                  )(val info: Source.Parser.Info) extends Member with MethodMember
 
 case class PureMethod(
@@ -196,7 +203,8 @@ case class PureMethod(
                        override val pres: Vector[Assertion],
                        override val posts: Vector[Assertion],
                        override val terminationMeasures: Vector[TerminationMeasure],
-                       body: Option[Expr]
+                       override val exhaleMode: Option[ExhaleMode],
+                       body: Option[Expr],
                      )(val info: Source.Parser.Info) extends Member with MethodMember {
   require(results.size <= 1)
 }
@@ -241,6 +249,7 @@ case class Function(
                      override val pres: Vector[Assertion],
                      override val posts: Vector[Assertion],
                      override val terminationMeasures: Vector[TerminationMeasure],
+                     override val exhaleMode: Option[ExhaleMode],
                      body: Option[MethodBody]
                    )(val info: Source.Parser.Info) extends Member with FunctionMember
 
@@ -251,6 +260,7 @@ case class PureFunction(
                          override val pres: Vector[Assertion],
                          override val posts: Vector[Assertion],
                          override val terminationMeasures: Vector[TerminationMeasure],
+                         override val exhaleMode: Option[ExhaleMode],
                          body: Option[Expr]
                        )(val info: Source.Parser.Info) extends Member with FunctionMember {
   require(results.size <= 1)
@@ -449,6 +459,7 @@ case class Outline(
                     pres: Vector[Assertion],
                     posts: Vector[Assertion],
                     terminationMeasures: Vector[TerminationMeasure],
+                    exhaleMode: Option[ExhaleMode],
                     body: Stmt,
                     trusted: Boolean,
                   )(val info: Source.Parser.Info) extends Stmt
@@ -1112,7 +1123,8 @@ case class FunctionLit(
                      override val pres: Vector[Assertion],
                      override val posts: Vector[Assertion],
                      override val terminationMeasures: Vector[TerminationMeasure],
-                     body: Option[MethodBody]
+                     override val exhaleMode: Option[ExhaleMode],
+                     body: Option[MethodBody],
                    )(val info: Source.Parser.Info) extends FunctionLitLike {
   override def typ: Type = FunctionT(args.map(_.typ), results.map(_.typ), Addressability.literal)
 }
@@ -1125,7 +1137,9 @@ case class PureFunctionLit(
                          override val pres: Vector[Assertion],
                          override val posts: Vector[Assertion],
                          override val terminationMeasures: Vector[TerminationMeasure],
-                         body: Option[Expr]
+                          // TODO: encoding, and clean warnings everywhere
+                         override val exhaleMode: Option[ExhaleMode],
+                         body: Option[Expr],
                        )(val info: Source.Parser.Info) extends FunctionLitLike {
   override def typ: Type = FunctionT(args.map(_.typ), results.map(_.typ), Addressability.literal)
   require(results.size <= 1)

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

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