From d90c9ffbdea204a39259dde5bfa2beac564ee8d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 5 Feb 2025 12:20:37 +0100 Subject: [PATCH 1/8] add witness of bug --- .../resources/regressions/issues/000815.gobra | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 src/test/resources/regressions/issues/000815.gobra diff --git a/src/test/resources/regressions/issues/000815.gobra b/src/test/resources/regressions/issues/000815.gobra new file mode 100644 index 000000000..913692068 --- /dev/null +++ b/src/test/resources/regressions/issues/000815.gobra @@ -0,0 +1,17 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue815 + +type cell struct { + value int +} + +pure +requires acc(c) +//:: ExpectedOutput(type_error) +ensures r == old(c.value) +decreases +func read(c *cell) (r int) { + return c.value +} \ No newline at end of file From dc71130e04c0a966fcb25fc895378db08e6491e4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 5 Feb 2025 12:21:41 +0100 Subject: [PATCH 2/8] fix 815 --- .../typing/ghost/GhostMemberTyping.scala | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) 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..f016380e8 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,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, PMember, PMPredicateDecl, PMethodDecl, PMethodImplementationProof, PParameter, PReturn, PVariadicType, PWithBody} +import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PExplicitGhostMember, PExpression, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMember, PMethodDecl, PMethodImplementationProof, POld, PParameter, 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 @@ -64,7 +64,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => isSingleResultArg(member) ++ isSinglePureReturnExpr(member) ++ isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) + nonVariadicArguments(member.args) ++ + member.spec.posts.flatMap(hasOldExpression) } else noMessages } @@ -87,6 +88,11 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => } } + private def hasOldExpression(n: PExpression): Messages = { + val hasOld = allChildren(n).exists(_.isInstanceOf[POld]) + error(n, "old(_) expressions cannot occur in postconditions of pure functions.", hasOld) + } + private def isPurePostcondition(spec: PFunctionSpec): Messages = (spec.posts ++ spec.preserves) flatMap isPureExpr private[typing] def nonVariadicArguments(args: Vector[PParameter]): Messages = args.flatMap { From ded98e5825a5136478d03440f143264d872db7dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 5 Feb 2025 17:05:48 +0100 Subject: [PATCH 3/8] add check for ghost pure members too --- .../info/implementation/typing/ghost/GhostMemberTyping.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 f016380e8..87865aa4a 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 @@ -49,7 +49,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => isSingleResultArg(member) ++ isSinglePureReturnExpr(member) ++ isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) + nonVariadicArguments(member.args) ++ + member.spec.posts.flatMap(hasOldExpression) } else noMessages } From 6ac78ae33682f168c0fb63f2f129fd3a91dda4cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 14 Feb 2025 13:58:29 +0100 Subject: [PATCH 4/8] add witness of missing checks --- src/test/resources/regressions/issues/000815.gobra | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/test/resources/regressions/issues/000815.gobra b/src/test/resources/regressions/issues/000815.gobra index 913692068..15fe5bd0f 100644 --- a/src/test/resources/regressions/issues/000815.gobra +++ b/src/test/resources/regressions/issues/000815.gobra @@ -9,9 +9,20 @@ type cell struct { pure requires acc(c) +// old expressions not allowed in postconditions of pure functions //:: ExpectedOutput(type_error) ensures r == old(c.value) decreases func read(c *cell) (r int) { return c.value -} \ No newline at end of file +} + +// old expressions not allowed in preconditions +//:: ExpectedOutput(type_error) +requires old(true) +func oldInPre() + +// old expressions not allowed in termination measures +//:: ExpectedOutput(type_error) +decreases old(1) +func oldInDecreasesClause() \ No newline at end of file From ceeb7c9c4d1a58af7be24153666003c05d733a09 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 14 Feb 2025 13:58:42 +0100 Subject: [PATCH 5/8] add fixes --- .../typing/ghost/GhostMemberTyping.scala | 12 ++------ .../typing/ghost/GhostMiscTyping.scala | 30 +++++++++++++++++-- 2 files changed, 31 insertions(+), 11 deletions(-) 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 87865aa4a..a162e49fb 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,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, PExpression, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMember, PMethodDecl, PMethodImplementationProof, POld, PParameter, PReturn, PVariadicType, PWithBody} +import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMember, PMethodDecl, PMethodImplementationProof, PParameter, 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 @@ -49,8 +49,7 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => isSingleResultArg(member) ++ isSinglePureReturnExpr(member) ++ isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) ++ - member.spec.posts.flatMap(hasOldExpression) + nonVariadicArguments(member.args) } else noMessages } @@ -65,8 +64,7 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => isSingleResultArg(member) ++ isSinglePureReturnExpr(member) ++ isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) ++ - member.spec.posts.flatMap(hasOldExpression) + nonVariadicArguments(member.args) } else noMessages } @@ -89,10 +87,6 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => } } - private def hasOldExpression(n: PExpression): Messages = { - val hasOld = allChildren(n).exists(_.isInstanceOf[POld]) - error(n, "old(_) expressions cannot occur in postconditions of pure functions.", hasOld) - } private def isPurePostcondition(spec: PFunctionSpec): Messages = (spec.posts ++ spec.preserves) flatMap isPureExpr diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala index 198ce6433..5287512e1 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala @@ -155,6 +155,8 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => preserves.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++ pres.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++ terminationMeasures.flatMap(wellDefTerminationMeasure) ++ + presFreeOfOld(n.pres) ++ + postsFreeOfOldIfPure(n.posts, isPure) ++ // 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)) ++ @@ -167,12 +169,36 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => error(n, "Termination measures of loops cannot be conditional.", terminationMeasure.exists(isConditional)) } + private[typing] def hasOldExpression(n: PExpression): Boolean = + (n +: allChildren(n)).exists{ e => e.isInstanceOf[POld] || e.isInstanceOf[PLabeledOld]} + + private def presFreeOfOld(pres: Vector[PExpression]): Messages = { + pres.flatMap { pre => + error(pre, "old(_) expressions cannot occur in preconditions of functions and methods.", hasOldExpression(pre)) + } + } + + private def postsFreeOfOldIfPure(posts: Vector[PExpression], isPure: Boolean): Messages = { + if (isPure) + posts.flatMap { post => + error(post, "old(_) expressions cannot occur in postconditions of pure functions.", hasOldExpression(post)) + } + else + noMessages + } + private def wellDefTerminationMeasure(measure: PTerminationMeasure): Messages = measure match { case PTupleTerminationMeasure(tuple, cond) => tuple.flatMap(p => comparableType.errors(exprType(p))(p) ++ isWeaklyPureExpr(p)) ++ - cond.toVector.flatMap(p => assignableToSpec(p) ++ isPureExpr(p)) + cond.toVector.flatMap(p => assignableToSpec(p) ++ isPureExpr(p)) ++ + (tuple ++ cond).flatMap { expr => + error(expr, "old(_) expressions cannot occur in termination measures.", hasOldExpression(expr)) + } case PWildcardMeasure(cond) => - cond.toVector.flatMap(p => assignableToSpec(p) ++ isPureExpr(p)) + cond.toVector.flatMap(p => assignableToSpec(p) ++ isPureExpr(p)) ++ + cond.map { expr => + error(expr, "old(_) expressions cannot occur in termination measures.", hasOldExpression(expr)) + }.getOrElse(noMessages) } private def wellDefClosureSpecInstanceParams(c: PClosureSpecInstance, fArgs: Vector[(PParameter, Type)]): Messages = c match { From 091279f23b03156758fe26ccaa3cdb4084e4e9ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 14 Feb 2025 13:59:30 +0100 Subject: [PATCH 6/8] Update src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala --- .../info/implementation/typing/ghost/GhostMemberTyping.scala | 1 - 1 file changed, 1 deletion(-) 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 a162e49fb..60bed6abe 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 @@ -87,7 +87,6 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => } } - private def isPurePostcondition(spec: PFunctionSpec): Messages = (spec.posts ++ spec.preserves) flatMap isPureExpr private[typing] def nonVariadicArguments(args: Vector[PParameter]): Messages = args.flatMap { From df2432a40cd031e1612e03c1668bb1de1cab835b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 14 Feb 2025 14:24:24 +0100 Subject: [PATCH 7/8] Update GhostMemberTyping.scala --- .../info/implementation/typing/ghost/GhostMemberTyping.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 60bed6abe..d25b98706 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,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, PReturn, PVariadicType, PWithBody} +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.frontend.info.base.SymbolTable.{MPredicateSpec, MethodImpl, MethodSpec} import viper.gobra.frontend.info.base.Type.{InterfaceT, Type, UnknownType} import viper.gobra.frontend.info.implementation.TypeInfoImpl From c1b9e5b232558b58c8877eedfa6cb1e6f75a2e32 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 14 Feb 2025 22:52:08 +0100 Subject: [PATCH 8/8] fix tests --- .../implementation/resolution/Enclosing.scala | 3 +++ .../typing/ghost/GhostMiscTyping.scala | 18 ++++++++++++------ 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala index c25c4c9a3..5097c911e 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala @@ -93,6 +93,9 @@ trait Enclosing { this: TypeInfoImpl => lazy val isEnclosingDomain: PNode => Boolean = down(false){ case _: PDomainType => true } + lazy val isEnclosingMagicWand: PNode => Boolean = + down(false) { case _: PMagicWand => true } + def isGlobalVarDeclaration(n: PVarDecl): Boolean = enclosingCodeRoot(n).isInstanceOf[PPackage] diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala index 5287512e1..8e071b332 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala @@ -7,6 +7,7 @@ package viper.gobra.frontend.info.implementation.typing.ghost import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, message, noMessages} +import viper.gobra.ast.frontend.PLabelNode.lhsLabel import viper.gobra.ast.frontend._ import viper.gobra.frontend.info.base.SymbolTable import viper.gobra.frontend.info.base.SymbolTable.{BuiltInMPredicate, GhostTypeMember, MPredicateImpl, MPredicateSpec} @@ -169,19 +170,24 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => error(n, "Termination measures of loops cannot be conditional.", terminationMeasure.exists(isConditional)) } - private[typing] def hasOldExpression(n: PExpression): Boolean = - (n +: allChildren(n)).exists{ e => e.isInstanceOf[POld] || e.isInstanceOf[PLabeledOld]} + private[typing] def hasOldExpressionExceptValidWand(n: PExpression): Boolean = + (n +: allChildren(n)).exists { + case _: POld => true + case o: PLabeledOld if o.label.name == lhsLabel => !isEnclosingMagicWand(o) + case _: PLabeledOld => true + case _ => false + } private def presFreeOfOld(pres: Vector[PExpression]): Messages = { pres.flatMap { pre => - error(pre, "old(_) expressions cannot occur in preconditions of functions and methods.", hasOldExpression(pre)) + error(pre, "old(_) expressions cannot occur in preconditions of functions and methods.", hasOldExpressionExceptValidWand(pre)) } } private def postsFreeOfOldIfPure(posts: Vector[PExpression], isPure: Boolean): Messages = { if (isPure) posts.flatMap { post => - error(post, "old(_) expressions cannot occur in postconditions of pure functions.", hasOldExpression(post)) + error(post, "old(_) expressions cannot occur in postconditions of pure functions.", hasOldExpressionExceptValidWand(post)) } else noMessages @@ -192,12 +198,12 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => tuple.flatMap(p => comparableType.errors(exprType(p))(p) ++ isWeaklyPureExpr(p)) ++ cond.toVector.flatMap(p => assignableToSpec(p) ++ isPureExpr(p)) ++ (tuple ++ cond).flatMap { expr => - error(expr, "old(_) expressions cannot occur in termination measures.", hasOldExpression(expr)) + error(expr, "old(_) expressions cannot occur in termination measures.", hasOldExpressionExceptValidWand(expr)) } case PWildcardMeasure(cond) => cond.toVector.flatMap(p => assignableToSpec(p) ++ isPureExpr(p)) ++ cond.map { expr => - error(expr, "old(_) expressions cannot occur in termination measures.", hasOldExpression(expr)) + error(expr, "old(_) expressions cannot occur in termination measures.", hasOldExpressionExceptValidWand(expr)) }.getOrElse(noMessages) }