diff --git a/src/main/resources/stubs/encoding/binary/binary.gobra b/src/main/resources/stubs/encoding/binary/binary.gobra index b5c63d26b..542c6e5d2 100644 --- a/src/main/resources/stubs/encoding/binary/binary.gobra +++ b/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 } @@ -250,6 +254,4 @@ pure func (b bigEndian) GoString() (res string) { return "binary.BigEndian" } // If v is neither of these, Size returns -1. // (joao) requires support for the reflect package decreases -func Size(v interface{}) int /*{ - return dataSize(reflect.Indirect(reflect.ValueOf(v))) -}*/ +func Size(v interface{}) int \ No newline at end of file diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index 1e83156a9..59a326cb9 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/src/main/scala/viper/gobra/ast/frontend/Ast.scala @@ -874,9 +874,15 @@ object PGhostifier { * Termination Measures */ -sealed trait PTerminationMeasure extends PNode -case class PWildcardMeasure(cond: Option[PExpression]) extends PTerminationMeasure -case class PTupleTerminationMeasure(tuple: Vector[PExpression], cond: Option[PExpression]) extends PTerminationMeasure +sealed trait PTerminationMeasure extends PNode { + val isConditional: Boolean +} +case class PWildcardMeasure(cond: Option[PExpression]) extends PTerminationMeasure { + override val isConditional: Boolean = cond.nonEmpty +} +case class PTupleTerminationMeasure(tuple: Vector[PExpression], cond: Option[PExpression]) extends PTerminationMeasure { + override val isConditional: Boolean = cond.nonEmpty +} /** * Specification diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala index f38cd8aef..d45d71a7b 100644 --- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala +++ b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala @@ -428,7 +428,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole override def visitMethodSpec(ctx: GobraParser.MethodSpecContext): PMethodSig = { val ghost = has(ctx.GHOST()) val spec = if (ctx.specification() != null) - visitSpecification(ctx.specification()) + visitSpecification(ctx.specification()).at(ctx) else PFunctionSpec(Vector.empty,Vector.empty,Vector.empty, Vector.empty, Vector.empty).at(ctx) // The name of each explicitly specified method must be unique and not blank. diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala index d7c03e0f6..96573ae7f 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala @@ -26,13 +26,11 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl => wellDefVariadicArgs(n.args) ++ wellDefIfPureFunction(n) ++ wellDefIfInitBlock(n) ++ - wellDefIfMain(n) ++ - wellFoundedIfNeeded(n) + wellDefIfMain(n) case m: PMethodDecl => wellDefVariadicArgs(m.args) ++ isReceiverType.errors(miscType(m.receiver))(member) ++ - wellDefIfPureMethod(m) ++ - wellFoundedIfNeeded(m) + wellDefIfPureMethod(m) case b: PConstDecl => b.specs.flatMap(wellDefConstSpec) case g: PVarDecl if isGlobalVarDeclaration(g) => diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index 7f98def93..d8dabd3fe 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala @@ -66,6 +66,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => case t: PInterfaceType => val isRecursiveInterface = error(t, "invalid recursive interface", cyclicInterfaceDef(t)) if (isRecursiveInterface.isEmpty) { + val wellDefIfPureSig = t.methSpecs.flatMap { sig => wellDefIfPureSpec(sig.spec, sig.args, sig.result) } // The semantics of wildcard termination measures in interface method specifications is not clear. // Thus, they are rejected. val sigsWithWildcardMeasuresErrors = t.methSpecs.flatMap { sig => @@ -76,6 +77,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => } } addressableMethodSet(InterfaceT(t, this)).errors(t) ++ + wellDefIfPureSig ++ sigsWithWildcardMeasuresErrors ++ containsRedeclarations(t) // temporary check } else { diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala index d25b98706..bfaa8526b 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala @@ -7,17 +7,20 @@ 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, PMember, PMPredicateDecl, PMethodDecl, PMethodImplementationProof, PParameter, PReturn, PVariadicType, PWithBody} +import viper.gobra.ast.frontend._ 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 import viper.gobra.frontend.info.implementation.typing.BaseTyping -import viper.gobra.util.Violation trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => private[typing] def wellDefGhostMember(member: PGhostMember): Messages = member match { - case PExplicitGhostMember(_) => noMessages + case PExplicitGhostMember(m) => m match { + case f: PFunctionDecl => wellFoundedIfNeeded(f.spec) + case m: PMethodDecl => wellFoundedIfNeeded(m.spec) + case _ => noMessages + } case PFPredicateDecl(_, args, body) => body.fold(noMessages)(assignableToSpec) ++ nonVariadicArguments(args) @@ -28,28 +31,38 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => nonVariadicArguments(args) } - private[typing] def wellFoundedIfNeeded(member: PMember): Messages = { - val spec = member match { - case m: PMethodDecl => m.spec - case f: PFunctionDecl => f.spec - case _ => Violation.violation("Unexpected member type") + // spec must come from a ghost or pure function + private[typing] def wellFoundedIfNeeded(spec: PFunctionSpec): Messages = { + val needsMeasure = !config.disableCheckTerminationPureFns + if (needsMeasure) { + isValidMeasureForGhostOrPure(spec) + } else noMessages + } + + private def isValidMeasureForGhostOrPure(spec: PFunctionSpec): Messages = { + // TODO: eventually, we should deprecate the flag `config.disableCheckTerminationPureFns` + val hasTerminationMeasureErrors = + error(spec, s"Pure and ghost functions and methods must have termination measures.", + spec.terminationMeasures.isEmpty) + // (João) Conditional termination measures are a very rarely used feature. They allow defining termination measures + // case-per-case. However, for pure or ghost functions and methods, we need to show that all conditions provided + // do cover all possible inputs, otherwise the function is not guaranteed to terminate. Implementing such a + // check would not be hard, but it would be more cumbersome (and in general, less efficient) than this syntactic check. + // If this feature is requested, I am happy to implement the more complete check, but for now, I will stick to + // this syntactic check. + val hasConditionalTerminationMeasureErrors = { + val conditionalMeasure = spec.terminationMeasures.find(_.isConditional) + conditionalMeasure match { + case Some(n) => error(n, "Conditional termination measures are not allowed in pure members.") + case None => noMessages + } } - 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 + hasTerminationMeasureErrors ++ hasConditionalTerminationMeasureErrors } private[typing] def wellDefIfPureMethod(member: PMethodDecl): Messages = { if (member.spec.isPure) { - isSingleResultArg(member) ++ - isSinglePureReturnExpr(member) ++ - isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) + wellDefIfPureSpec(member.spec, member.args, member.result) ++ isSinglePureReturnExpr(member) } else noMessages } @@ -61,15 +74,23 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => private[typing] def wellDefIfPureFunction(member: PFunctionDecl): Messages = { if (member.spec.isPure) { - isSingleResultArg(member) ++ - isSinglePureReturnExpr(member) ++ - isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) + wellDefIfPureSpec(member.spec, member.args, member.result) ++ isSinglePureReturnExpr(member) } else noMessages } - private def isSingleResultArg(member: PCodeRootWithResult): Messages = { - error(member, "For now, pure methods and pure functions must have exactly one result argument", member.result.outs.size != 1) + // This implements checks that are common to pure functions and pure methods. Checks that are specific to either + // (e.g., checks that may depend on the receiver of a method) should be implemented elsewhere. + private[typing] def wellDefIfPureSpec(spec: PFunctionSpec, args: Vector[PParameter], result: PResult) : Messages = { + if (spec.isPure) { + isSingleResultArg(result) ++ + isPurePostcondition(spec) ++ + nonVariadicArguments(args) ++ + wellFoundedIfNeeded(spec) + } else noMessages + } + + private def isSingleResultArg(result: PResult): Messages = { + error(result, "For now, pure methods and pure functions must have exactly one result argument", result.outs.size != 1) } private def isSinglePureReturnExpr(member: PWithBody): Messages = { @@ -93,6 +114,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => p: PParameter => error(p, s"Pure members cannot have variadic arguments, but got $p", p.typ.isInstanceOf[PVariadicType]) } + + override lazy val localImplementationProofs: Vector[(Type, InterfaceT, Vector[String], Vector[String])] = { val implementationProofs = tree.root.programs.flatMap(_.declarations.collect{ case m: PImplementationProof => m}) implementationProofs.flatMap { ip => diff --git a/src/test/resources/regressions/issues/000841.gobra b/src/test/resources/regressions/issues/000841.gobra new file mode 100644 index 000000000..d67371613 --- /dev/null +++ b/src/test/resources/regressions/issues/000841.gobra @@ -0,0 +1,18 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue000841 + +type J interface { + // Type error, pure function does not have termination measures. + //:: ExpectedOutput(type_error) + pure + // Type error, pure function cannot have variadic parameters. + //:: ExpectedOutput(type_error) + M(a ...int) int +} + +pure +//:: ExpectedOutput(type_error) +decreases _ if b +func f(b bool) bool \ No newline at end of file