Fix issue #841

src/main/resources/stubs/encoding/binary/binary.gobra

@@ -11,13 +11,16 @@ package binary
 // 16-, 32-, or 64-bit unsigned integers.
 type ByteOrder interface {
 	requires acc(&b[0], _) && acc(&b[1], _)
+	decreases
 	pure Uint16(b []byte) uint16
 
 	requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _)
+	decreases
 	pure Uint32(b []byte) uint32
 
 	requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _)
 	requires acc(&b[4], _) && acc(&b[5], _) && acc(&b[6], _) && acc(&b[7], _)
+	decreases
 	pure Uint64(b []byte) uint64
 
 	requires acc(&b[0]) && acc(&b[1])
@@ -37,6 +40,7 @@ type ByteOrder interface {
 	decreases
 	PutUint64(b []byte, uint64)
 
+	decreases
 	pure String() string
 }
 

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

@@ -157,9 +157,19 @@ sealed trait PDependentDef extends PNode {
 sealed trait PCodeRoot extends PNode
 
 sealed trait PCodeRootWithResult extends PCodeRoot {
+  def args: Vector[PParameter]
   def result: PResult
 }
 
+/**
+  * A code root that carries a specification: a function or method declaration, a closure declaration, or the
+  * signature of an interface method. Notably, this excludes `PMethodImplementationProof`, which inherits the
+  * specification of the interface method that it proves and thus does not have one of its own.
+  */
+sealed trait PCodeRootWithSpec extends PCodeRootWithResult {
+  def spec: PFunctionSpec
+}
+
 case class PConstDecl(specs: Vector[PConstSpec]) extends PActualMember with PActualStatement with PGhostifiableStatement with PGhostifiableMember with PDeclaration
 
 case class PConstSpec(typ: Option[PType], right: Vector[PExpression], left: Vector[PDefLikeId]) extends PNode
@@ -183,7 +193,7 @@ case class PFunctionDecl(
                           result: PResult,
                           spec: PFunctionSpec,
                           body: Option[(PBodyParameterInfo, PBlock)]
-                        ) extends PFunctionOrClosureDecl with PFunctionOrMethodDecl with PCodeRootWithResult with PWithBody with PGhostifiableMember
+                        ) extends PFunctionOrClosureDecl with PFunctionOrMethodDecl with PCodeRootWithSpec with PWithBody with PGhostifiableMember
 
 case class PMethodDecl(
                         id: PIdnDef,
@@ -192,7 +202,7 @@ case class PMethodDecl(
                         result: PResult,
                         spec: PFunctionSpec,
                         body: Option[(PBodyParameterInfo, PBlock)]
-                      ) extends PFunctionOrMethodDecl with PDependentDef with PScope with PCodeRootWithResult with PWithBody with PGhostifiableMember
+                      ) extends PFunctionOrMethodDecl with PDependentDef with PScope with PCodeRootWithSpec with PWithBody with PGhostifiableMember
 
 sealed trait PTypeDecl extends PActualMember with PActualStatement with PGhostifiableStatement with PGhostifiableMember with PDeclaration {
 
@@ -468,7 +478,7 @@ case class PFunctionLit(id: Option[PIdnDef], decl: PClosureDecl) extends PLitera
 case class PClosureDecl(args: Vector[PParameter],
                   result: PResult,
                   spec: PFunctionSpec,
-                  body: Option[(PBodyParameterInfo, PBlock)]) extends PFunctionOrClosureDecl with PCodeRootWithResult with PActualMisc
+                  body: Option[(PBodyParameterInfo, PBlock)]) extends PFunctionOrClosureDecl with PCodeRootWithSpec with PWithBody with PActualMisc
 
 case class PClosureSpecInstance(func: PNameOrDot, params: Vector[PKeyedElement]) extends PGhostMisc {
   require(params.forall(p => p.exp.isInstanceOf[PExpCompositeVal]))
@@ -785,7 +795,7 @@ case class PInterfaceName(typ: PTypeName) extends PInterfaceClause
 
 // Felix: I see `isGhost` as part of the declaration and not as port of the specification.
 //        In the past, I usually created some ghost wrapper for these cases, but I wanted to get rid of them in the future.
-case class PMethodSig(id: PIdnDef, args: Vector[PParameter], result: PResult, spec: PFunctionSpec, isGhost: Boolean) extends PInterfaceClause with PDependentDef with PScope with PCodeRootWithResult
+case class PMethodSig(id: PIdnDef, args: Vector[PParameter], result: PResult, spec: PFunctionSpec, isGhost: Boolean) extends PInterfaceClause with PDependentDef with PScope with PCodeRootWithSpec
 
 /**
   * Identifiers

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

@@ -939,7 +939,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
       isAtomic = ctx.atomic,
       opensInvs = ctx.opensInv,
       mayBeUsedInInit = ctx.mayInit,
-    )
+    ).at(ctx)
   }
 
   /**

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

@@ -247,7 +247,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
       capturedLocalVariables(f.decl).flatMap(v => addressable.errors(enclosingExpr(v).get)(v)) ++
         wellDefVariadicArgs(f.args) ++
         f.id.fold(noMessages)(id => wellDefID(id).out) ++
-        error(f, "Opaque function literals are not yet supported.", f.spec.isOpaque)
+        error(f, "Opaque function literals are not yet supported.", f.spec.isOpaque) ++
+        wellDefIfPureClosure(f)
 
     case n: PInvoke =>
       val mayInit = isEnclosingMayInit(n)

src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala

@@ -26,16 +26,14 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl =>
         wellDefIfPureFunction(n) ++
         wellDefIfInitBlock(n) ++
         wellDefIfMain(n) ++
-        wellFoundedIfNeeded(n) ++
-        atomicMemberIsWellFormed(n) ++
-        noConditionalMeasureIfGhostOrPure(n)
+        wellFoundedIfGhost(n) ++
+        atomicMemberIsWellFormed(n)
     case m: PMethodDecl =>
       wellDefVariadicArgs(m.args) ++
         isReceiverType.errors(miscType(m.receiver))(member) ++
         wellDefIfPureMethod(m) ++
-        wellFoundedIfNeeded(m) ++
-        atomicMemberIsWellFormed(m) ++
-        noConditionalMeasureIfGhostOrPure(m)
+        wellFoundedIfGhost(m) ++
+        atomicMemberIsWellFormed(m)
     case b: PConstDecl =>
       b.specs.flatMap(wellDefConstSpec)
     case g: PVarDecl if isGlobalVarDeclaration(g) =>

src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala

@@ -6,8 +6,8 @@
 
 package viper.gobra.frontend.info.implementation.typing
 
-import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error}
-import viper.gobra.ast.frontend.{PTerminationMeasure, PTupleTerminationMeasure, PWildcardMeasure}
+import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages}
+import viper.gobra.ast.frontend.{PFunctionSpec, PNode, PTerminationMeasure, PTupleTerminationMeasure, PWildcardMeasure}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
 /**
@@ -39,13 +39,43 @@ trait TerminationTyping extends BaseTyping { this: TypeInfoImpl =>
       case _ => false
     }
 
+  /**
+    * The semantics of wildcard termination measures in interface method specifications is not clear.
+    * Thus, they are rejected.
+    */
+  private[typing] def noWildcardMeasureErrors(measures: Vector[PTerminationMeasure]): Messages =
+    measures.flatMap {
+      case w: PWildcardMeasure =>
+        error(w, "Wildcard termination measures are not allowed in the specifications of interface methods.")
+      case _ => noMessages
+    }
+
   private[typing] def noConditionalMeasureErrors(measures: Vector[PTerminationMeasure]): Messages =
     measures.flatMap { m =>
       error(m,
         "Conditional termination measures are not allowed on ghost or pure functions, methods, and interface methods.",
         isConditional(m))
     }
 
+  /**
+    * Checks that `spec` guarantees that the member it belongs to terminates on every call, as Gobra
+    * requires of all ghost and pure members: functions, methods, and interface method signatures alike.
+    * The missing-measure error is reported on `node`, which should be the member or signature that
+    * `spec` specifies.
+    *
+    * Ghost and pure members are held to a stricter rule than `measuresGuaranteeTermination`: they may
+    * not carry a conditional measure at all because we do not check that the conditions of conditional
+    * measures cover all inputs. The two problems are therefore reported separately, the missing
+    * measure on `node` and each conditional measure on the measure itself, and only the former
+    * is subject to `disableCheckTerminationPureFns`.
+    */
+  private[typing] def mustTerminateErrors(node: PNode, spec: PFunctionSpec): Messages = {
+    val missingMeasureError = error(node,
+      "Ghost and pure functions, methods, and interface methods must have termination measures, but none was found.",
+      !config.disableCheckTerminationPureFns && spec.terminationMeasures.isEmpty)
+    missingMeasureError ++ noConditionalMeasureErrors(spec.terminationMeasures)
+  }
+
   private[typing] def hasSameMeasureType(measures: Vector[PTerminationMeasure]): Boolean = {
     val tupleMeasureTypes = measures
       .collect { case ttm: PTupleTerminationMeasure => ttm }

src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala

@@ -75,28 +75,9 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
           }
         }
 
-        // The semantics of wildcard termination measures in interface method specifications is not clear.
-        // Thus, they are rejected.
-        val sigsWithWildcardMeasuresErrors = t.methSpecs.flatMap { sig =>
-          sig.spec.terminationMeasures.flatMap {
-            case w: PWildcardMeasure =>
-              error(w, s"Wildcard termination measures are not allowed in the specifications of interface methods.")
-            case _ => noMessages
-          }
-        }
-        val sigsWithConditionalMeasuresErrors = t.methSpecs.flatMap { sig =>
-          if (sig.isGhost || sig.spec.isPure)
-            noConditionalMeasureErrors(sig.spec.terminationMeasures)
-          else noMessages
-        }
-        val interfaceMethodsNotAtomic = t.methSpecs.flatMap { sig =>
-          error(sig, s"Interface methods cannot be marked as atomic.", sig.spec.isAtomic)
-        }
         methodSet.errors(t) ++
           error(t, "Interface declaration contains methods annotated with 'mayInit'.", methodsContainMayInit) ++
-          interfaceMethodsNotAtomic ++
-          sigsWithWildcardMeasuresErrors ++
-          sigsWithConditionalMeasuresErrors ++
+          t.methSpecs.flatMap(wellDefMethodSig) ++
           containsRedeclarations(t) // temporary check
       } else {
         isRecursiveInterface

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

@@ -7,7 +7,7 @@
 package viper.gobra.frontend.info.implementation.typing.ghost
 
 import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages}
-import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMember, PMethodDecl, PMethodImplementationProof, PParameter, PPreserves, PReturn, PVariadicType, PWithBody}
+import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PCodeRootWithSpec, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionLit, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMember, PMethodDecl, PMethodImplementationProof, PMethodSig, PParameter, PPreserves, PReturn, PVariadicType, PWithBody}
 import viper.gobra.frontend.info.base.SymbolTable.{MPredicateSpec, MethodImpl, MethodSpec}
 import viper.gobra.frontend.info.base.Type.{InterfaceT, Type, UnknownType}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
@@ -28,30 +28,15 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
         nonVariadicArguments(args)
   }
 
-  private[typing] def wellFoundedIfNeeded(member: PMember): Messages = {
+  // Ghost functions and methods must be guaranteed to terminate. Pure members, whether ghost or not, are
+  // checked uniformly in `wellDefPureSpec`, which is why they are excluded here.
+  private[typing] def wellFoundedIfGhost(member: PMember): Messages = {
     val spec = member match {
       case m: PMethodDecl => m.spec
       case f: PFunctionDecl => f.spec
       case _ => Violation.violation("Unexpected member type")
     }
-    val hasMeasureIfNeeded =
-      if (spec.isPure || isEnclosingGhost(member))
-        config.disableCheckTerminationPureFns || spec.terminationMeasures.nonEmpty
-      else
-        true
-    val needsMeasureError =
-      error(member, "All pure or ghost functions and methods must have termination measures, but none was found for this member.", !hasMeasureIfNeeded)
-    needsMeasureError
-  }
-
-  private[typing] def noConditionalMeasureIfGhostOrPure(member: PMember): Messages = {
-    val spec = member match {
-      case m: PMethodDecl => m.spec
-      case f: PFunctionDecl => f.spec
-      case _ => return noMessages
-    }
-    if (spec.isPure || isEnclosingGhost(member))
-      noConditionalMeasureErrors(spec.terminationMeasures)
+    if (isEnclosingGhost(member) && !spec.isPure) mustTerminateErrors(member, spec)
     else noMessages
   }
 
@@ -60,11 +45,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
 
   private[typing] def wellDefIfPureMethod(member: PMethodDecl): Messages = {
     if (member.spec.isPure) {
-      isSingleResultArg(member) ++
+      wellDefPureSpec(member) ++
         isSinglePureReturnExpr(member) ++
-        isPurePostcondition(member.spec) ++
-        pureMembersCannotHavePreserves(member.spec) ++
-        nonVariadicArguments(member.args) ++
         error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit)
     } else noMessages
   }
@@ -87,15 +69,48 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
 
   private[typing] def wellDefIfPureFunction(member: PFunctionDecl): Messages = {
     if (member.spec.isPure) {
-      isSingleResultArg(member) ++
+      wellDefPureSpec(member) ++
         isSinglePureReturnExpr(member) ++
-        isPurePostcondition(member.spec) ++
-        pureMembersCannotHavePreserves(member.spec) ++
-        nonVariadicArguments(member.args) ++
         error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit)
     } else noMessages
   }
 
+  private[typing] def wellDefIfPureClosure(lit: PFunctionLit): Messages = {
+    if (lit.spec.isPure) {
+      wellDefPureSpec(lit.decl) ++
+        isSinglePureReturnExpr(lit.decl) ++
+        error(lit, pureFunctionsDoNotNeedMayInitMsg, lit.spec.mayBeUsedInInit)
+    } else noMessages
+  }
+
+  /**
+    * Well-definedness checks that every pure member must satisfy, whether it is a pure function, a pure method,
+    * a pure closure or the signature of a pure interface method: exactly one result, pure postconditions, no
+    * `preserves` clauses, non-variadic arguments, and a termination measure that guarantees termination. Checks
+    * specific to a particular kind of member (e.g., `mayInit`) are added by the callers.
+    */
+  private[typing] def wellDefPureSpec(member: PCodeRootWithSpec): Messages = {
+    Violation.violation(member.spec.isPure, "wellDefPureSpec may only be called for a pure member.")
+    isSingleResultArg(member) ++
+      isPurePostcondition(member.spec) ++
+      pureMembersCannotHavePreserves(member.spec) ++
+      nonVariadicArguments(member.args) ++
+      mustTerminateErrors(member, member.spec)
+  }
+
+  /**
+    * Well-definedness checks for the signature of an interface method. This is the counterpart of
+    * `wellDefActualMember` for the members declared by an interface, and imposes the same requirements on ghost
+    * and pure signatures as the ones imposed on ghost and pure implementations.
+    */
+  private[typing] def wellDefMethodSig(sig: PMethodSig): Messages = {
+    error(sig, "Interface methods cannot be marked as atomic.", sig.spec.isAtomic) ++
+      noWildcardMeasureErrors(sig.spec.terminationMeasures) ++
+      (if (sig.spec.isPure) wellDefPureSpec(sig)
+       else if (sig.isGhost) mustTerminateErrors(sig, sig.spec)
+       else noMessages)
+  }
+
   private[typing] def atomicMemberIsWellFormed(member: PMember): Messages = {
     val (bodyOpt, spec) = member match {
       case f: PFunctionDecl => (f.body, f.spec)