backup

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

@@ -877,8 +877,8 @@ case class PTupleTerminationMeasure(tuple: Vector[PExpression], cond: Option[PEx
 sealed trait PSpecification extends PGhostNode
 
 sealed trait PExhaleMode extends PNode
-case object PStrict extends PExhaleMode
-case object PMce extends PExhaleMode
+case class PStrict() extends PExhaleMode
+case class PMce() extends PExhaleMode
 
 case class PFunctionSpec(
                       pres: Vector[PExpression],

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

@@ -143,8 +143,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   }
 
   def showExhaleMode(mode: PExhaleMode): Doc = mode match {
-    case PStrict => "strict"
-    case PMce => "mce"
+    case PStrict() => "strict"
+    case PMce() => "mce"
   }
 
   def showSpec(spec: PSpecification): Doc = spec match {

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

@@ -147,16 +147,24 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     }
   }
 
+  def showExhaleMode(mode: ExhaleMode): Doc = {
+    val modDoc = mode match {
+      case Mce => "mce"
+      case Strict => "strict"
+    }
+    "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 {
@@ -678,15 +686,15 @@ 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 {

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 Strict extends ExhaleMode
+case object Mce extends ExhaleMode
+
 sealed trait MethodLikeMember extends Member {
   def name: MethodProxy
 }
@@ -146,6 +150,8 @@ sealed trait MethodMember extends MethodLikeMember {
   def results: Vector[Parameter.Out]
   def pres: Vector[Assertion]
   def posts: Vector[Assertion]
+  // TODO: same in outline and below
+  //  def exhaleMode: Option[ExhaleMode]
   def terminationMeasures: Vector[TerminationMeasure]
 }
 
@@ -158,6 +164,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]
 }
 
@@ -241,6 +248,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 +259,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)
@@ -1115,6 +1124,8 @@ case class FunctionLit(
                      body: Option[MethodBody]
                    )(val info: Source.Parser.Info) extends FunctionLitLike {
   override def typ: Type = FunctionT(args.map(_.typ), results.map(_.typ), Addressability.literal)
+  // todo: add type system check
+  override val exhaleMode: Option[ExhaleMode] = None
 }
 
 case class PureFunctionLit(
@@ -1129,6 +1140,8 @@ case class PureFunctionLit(
                        )(val info: Source.Parser.Info) extends FunctionLitLike {
   override def typ: Type = FunctionT(args.map(_.typ), results.map(_.typ), Addressability.literal)
   require(results.size <= 1)
+  // todo: add type system check
+  override val exhaleMode: Option[ExhaleMode] = None
 }
 
 case class ClosureImplements(closure: Expr, spec: ClosureSpec)(override val info: Source.Parser.Info) extends Expr {

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

@@ -25,19 +25,19 @@ object OverflowChecksTransform extends InternalTransform {
     // adds overflow checks per statement that contains subexpressions of bounded integer type and adds assume
     /// statements at the beginning of a function or method body assuming that the value of an argument (of
     // bounded integer type) respects the bounds.
-    case f@Function(name, args, results, pres, posts, terminationMeasure, body) =>
-      Function(name, args, results, pres, posts, terminationMeasure, body map computeNewBody)(f.info)
+    case f@Function(name, args, results, pres, posts, terminationMeasure, exhaleMode, body) =>
+      Function(name, args, results, pres, posts, terminationMeasure, exhaleMode, body map computeNewBody)(f.info)
 
     // same as functions
     case m@Method(receiver, name, args, results, pres, posts, terminationMeasure,body) =>
       Method(receiver, name, args, results, pres, posts, terminationMeasure, body map computeNewBody)(m.info)
 
     // Adds pre-conditions stating the bounds of each argument and a post-condition to check if the body expression
     // overflows
-    case f@PureFunction(name, args, results, pres, posts, terminationMeasure, body) => body match {
+    case f@PureFunction(name, args, results, pres, posts, terminationMeasure, exhaleMode, body) => body match {
       case Some(expr) =>
         val newPost = posts ++ getPureBlockPosts(expr, results)
-        PureFunction(name, args, results, pres, newPost, terminationMeasure, body)(f.info)
+        PureFunction(name, args, results, pres, newPost, terminationMeasure, exhaleMode, body)(f.info)
       case None => f
     }
 

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

@@ -564,6 +564,11 @@ object Desugar extends LazyLogging {
       typeD(DeclaredT(decl, info), Addressability.Exclusive)(meta(decl, info))
     }
 
+    def exhaleModeD(mode: PExhaleMode): in.ExhaleMode = mode match {
+      case PMce() => in.Mce
+      case PStrict() => in.Strict
+    }
+
     def functionD(decl: PFunctionDecl): in.FunctionMember =
       if (decl.spec.isPure) pureFunctionD(decl) else {
 
@@ -572,7 +577,7 @@ object Desugar extends LazyLogging {
       val functionInfo = functionMemberOrLitD(decl, fsrc, new FunctionContext(_ => _ => in.Seqn(Vector.empty)(fsrc)))
 
       in.Function(name, functionInfo.args, functionInfo.results, functionInfo.pres, functionInfo.posts,
-        functionInfo.terminationMeasures, functionInfo.body)(fsrc)
+        functionInfo.terminationMeasures, functionInfo.exhaleMode, functionInfo.body)(fsrc)
     }
 
     private case class FunctionInfo(args: Vector[in.Parameter.In],
@@ -581,6 +586,7 @@ object Desugar extends LazyLogging {
                                     pres: Vector[in.Assertion],
                                     posts: Vector[in.Assertion],
                                     terminationMeasures: Vector[in.TerminationMeasure],
+                                    exhaleMode: Option[in.ExhaleMode],
                                     body: Option[in.MethodBody])
 
     private def functionMemberOrLitD(decl: PFunctionOrClosureDecl, fsrc: Meta, outerCtx: FunctionContext): FunctionInfo = {
@@ -645,6 +651,7 @@ object Desugar extends LazyLogging {
       val pres = (decl.spec.pres ++ decl.spec.preserves) map preconditionD(specCtx, info)
       val posts = (decl.spec.preserves ++ decl.spec.posts) map postconditionD(specCtx, info)
       val terminationMeasures = sequence(decl.spec.terminationMeasures map terminationMeasureD(specCtx, info)).res
+      val exhaleMode = decl.spec.exhaleMode.headOption.map(exhaleModeD)
 
       // p1' := p1; ... ; pn' := pn
       val argInits = argsWithSubs.flatMap{
@@ -693,15 +700,16 @@ object Desugar extends LazyLogging {
         in.MethodBody(vars, in.MethodBodySeqn(body)(fsrc), resultAssignments)(fsrc)
       }
 
-      FunctionInfo(args, capturedWithAliases, returns, pres, posts, terminationMeasures, bodyOpt)
+      FunctionInfo(args, capturedWithAliases, returns, pres, posts, terminationMeasures, exhaleMode, bodyOpt)
     }
 
     def pureFunctionD(decl: PFunctionDecl): in.PureFunction = {
       val name = functionProxyD(decl, info)
       val fsrc = meta(decl, info)
       val funcInfo = pureFunctionMemberOrLitD(decl, fsrc, new FunctionContext(_ => _ => in.Seqn(Vector.empty)(fsrc)), info)
 
-      in.PureFunction(name, funcInfo.args, funcInfo.results, funcInfo.pres, funcInfo.posts, funcInfo.terminationMeasures, funcInfo.body)(fsrc)
+      in.PureFunction(name, funcInfo.args, funcInfo.results, funcInfo.pres, funcInfo.posts, funcInfo.terminationMeasures,
+        funcInfo.exhaleMode, funcInfo.body)(fsrc)
     }
 
     private case class PureFunctionInfo(args: Vector[in.Parameter.In],
@@ -710,6 +718,7 @@ object Desugar extends LazyLogging {
                                         pres: Vector[in.Assertion],
                                         posts: Vector[in.Assertion],
                                         terminationMeasures: Vector[in.TerminationMeasure],
+                                        exhaleMode: Option[in.ExhaleMode],
                                         body: Option[in.Expr])
 
 
@@ -755,6 +764,7 @@ object Desugar extends LazyLogging {
       val pres = decl.spec.pres map preconditionD(ctx, info)
       val posts = decl.spec.posts map postconditionD(ctx, info)
       val terminationMeasure = sequence(decl.spec.terminationMeasures map terminationMeasureD(ctx, info)).res
+      val exhaleMode = decl.spec.exhaleMode.headOption.map(exhaleModeD)
 
       val capturedWithAliases = (captured.map { v => in.Ref(localVarD(outerCtx, info)(v))(meta(v, info)) } zip capturedPar)
 
@@ -767,7 +777,7 @@ object Desugar extends LazyLogging {
           implicitConversion(res.typ, returns.head.typ, res)
       }
 
-      PureFunctionInfo(args, capturedWithAliases, returns, pres, posts, terminationMeasure, bodyOpt)
+      PureFunctionInfo(args, capturedWithAliases, returns, pres, posts, terminationMeasure, exhaleMode, bodyOpt)
     }
 
 
@@ -3485,6 +3495,7 @@ object Desugar extends LazyLogging {
           a.withInfo(a.info.asInstanceOf[Source.Parser.Single].createAnnotatedInfo(ImportPreNotEstablished))
         },
         terminationMeasures = Vector.empty,
+        exhaleMode = None,
         body = Some(in.MethodBody(Vector.empty, in.MethodBodySeqn(Vector.empty)(src), Vector.empty)(src)),
       )(src)
     }
@@ -3519,6 +3530,7 @@ object Desugar extends LazyLogging {
           pres = mainPkgPosts,
           posts = mainFuncPreD,
           terminationMeasures = Vector.empty,
+          exhaleMode = None,
           body = Some(in.MethodBody(Vector.empty, in.MethodBodySeqn(Vector.empty)(src), Vector.empty)(src)),
         )(src)
       }
@@ -3556,6 +3568,7 @@ object Desugar extends LazyLogging {
         posts = progPosts,
         // in our verification approach, the initialization code must be proven to terminate
         terminationMeasures = Vector(in.TupleTerminationMeasure(Vector(), None)(src)),
+        exhaleMode = None,
         body = Some(
           in.MethodBody(
             decls = Vector(),

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

@@ -880,8 +880,8 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     val preserves = groups.getOrElse(GobraParser.PRESERVES, Vector.empty).toVector.map(s => visitNode[PExpression](s.assertion().expression()))
     val posts = groups.getOrElse(GobraParser.POST, Vector.empty).toVector.map(s => visitNode[PExpression](s.assertion().expression()))
     val terms = groups.getOrElse(GobraParser.DEC, Vector.empty).toVector.map(s => visitTerminationMeasure(s.terminationMeasure()))
-
-    PFunctionSpec(pres, preserves, posts, terms, isPure = ctx.pure, isTrusted = ctx.trusted)
+    val exhaleModes = ctx.exhaleMode().asScala.toVector.map(visitExhaleMode)
+    PFunctionSpec(pres, preserves, posts, terms, exhaleModes, isPure = ctx.pure, isTrusted = ctx.trusted)
   }
 
   /**
@@ -1966,6 +1966,16 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     }
   }
 
+  override def visitExhaleMode(ctx: ExhaleModeContext): PExhaleMode = {
+    if (has(ctx.MCE())) {
+      PMce().at(ctx)
+    } else if (has(ctx.STRICT())) {
+      PStrict().at(ctx)
+    } else {
+      violation(s"Found unexpected exhaleMode")
+    }
+  }
+
   /** Visits a loop specification.
     *
     * @param ctx the loop spec context

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

@@ -493,7 +493,7 @@ object Parser extends LazyLogging {
           case n@PTupleTerminationMeasure(_, cond) => PWildcardMeasure(cond).at(n)
           case t => t
         }
-        PFunctionSpec(spec.pres, spec.preserves, spec.posts, replacedMeasures, spec.isPure, spec.isTrusted)
+        PFunctionSpec(spec.pres, spec.preserves, spec.posts, replacedMeasures, spec.exhaleMode, spec.isPure, spec.isTrusted)
       }
 
       val replaceTerminationMeasuresForFunctionsAndMethods: Strategy =

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala

@@ -219,11 +219,12 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl =>
   }
 
   implicit lazy val wellDefSpec: WellDefinedness[PSpecification] = createWellDef {
-    case n@ PFunctionSpec(pres, preserves, posts, terminationMeasures, _, _) =>
+    case n@ PFunctionSpec(pres, preserves, posts, terminationMeasures, exhaleMode, _, _) =>
       pres.flatMap(assignableToSpec) ++ preserves.flatMap(assignableToSpec) ++ posts.flatMap(assignableToSpec) ++
       preserves.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++
       pres.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++
       terminationMeasures.flatMap(wellDefTerminationMeasure) ++
+      error(n, "At most one exhaleMode may be specified per member", exhaleMode.length > 1) ++
       // if has conditional clause, all clauses must be conditional
       // can only have one non-conditional clause
       error(n, "Specifications can either contain one non-conditional termination measure or multiple conditional-termination measures.", terminationMeasures.length > 1 && !terminationMeasures.forall(isConditional)) ++

src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala

@@ -298,6 +298,7 @@ class StringEncoding extends LeafTypeEncoding {
         pres = Vector(pre),
         posts = Vector(),
         terminationMeasures = Vector(in.WildcardMeasure(None)(info)),
+        exhaleMode = None,
         body = None
       )(info)
       val translatedFunc = ctx.function(func)

src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala

@@ -208,7 +208,8 @@ protected class ClosureSpecsEncoder {
     val result = in.Parameter.Out(Names.closureArg, genericFuncType)(info)
     val satisfiesSpec = in.ExprAssertion(in.ClosureImplements(result, in.ClosureSpec(func, Map.empty)(info))(info))(info)
     val (args, captAssertions) = capturedArgsAndAssertions(ctx)(result, captured(ctx)(func), info)
-    val getter = in.PureFunction(proxy, args, Vector(result), Vector.empty, Vector(satisfiesSpec) ++ captAssertions, Vector.empty, None)(memberOrLit(ctx)(func).info)
+    // TODO: reject exhaleMode in type system closures
+    val getter = in.PureFunction(proxy, args, Vector(result), Vector.empty, Vector(satisfiesSpec) ++ captAssertions, Vector.empty, None, None)(memberOrLit(ctx)(func).info)
     ctx.defaultEncoding.pureFunction(getter)(ctx)
   }
 
@@ -292,20 +293,20 @@ protected class ClosureSpecsEncoder {
 
     func match {
       case _: in.Function =>
-        val m = in.Function(proxy, args, func.results, pres, func.posts, func.terminationMeasures, None)(spec.info)
+        val m = in.Function(proxy, args, func.results, pres, func.posts, func.terminationMeasures, func.exhaleMode, None)(spec.info)
         ctx.defaultEncoding.function(m)(ctx)
       case lit: in.FunctionLit =>
         val body = if (spec.params.isEmpty) lit.body else None
-        val func = in.Function(proxy, args, lit.results, pres, lit.posts, lit.terminationMeasures, body)(lit.info)
+        val func = in.Function(proxy, args, lit.results, pres, lit.posts, lit.terminationMeasures, lit.exhaleMode, body)(lit.info)
         ctx.defaultEncoding.function(func)(ctx)
       case f: in.PureFunction =>
         val posts = func.posts ++ assertionFromPureFunctionBody(f.body, f.results.head)
-        val m = in.PureFunction(proxy, args, f.results, pres, posts, f.terminationMeasures, None)(spec.info)
+        val m = in.PureFunction(proxy, args, f.results, pres, posts, f.terminationMeasures, f.exhaleMode, None)(spec.info)
         ctx.defaultEncoding.pureFunction(m)(ctx)
       case lit: in.PureFunctionLit =>
         val body = if (spec.params.isEmpty) lit.body else None
         val posts = lit.posts ++ (if (spec.params.isEmpty) Vector.empty else assertionFromPureFunctionBody(lit.body, lit.results.head).toVector)
-        val func = in.PureFunction(proxy, args, lit.results, pres, posts, lit.terminationMeasures, body)(lit.info)
+        val func = in.PureFunction(proxy, args, lit.results, pres, posts, lit.terminationMeasures, lit.exhaleMode, body)(lit.info)
         ctx.defaultEncoding.pureFunction(func)(ctx)
     }
   }