From 660e662e74f331f9cb819737f183ed377cf0302f Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Thu, 26 Oct 2023 16:55:04 -0700 Subject: [PATCH] adapts channel encoding to allow assignable instead of equal message types for channel send operations --- .../viper/gobra/reporting/VerifierError.scala | 2 +- .../encodings/channels/ChannelEncoding.scala | 19 +++++------ .../resources/regressions/issues/000695.gobra | 32 +++++++++++++++++++ 3 files changed, 43 insertions(+), 10 deletions(-) create mode 100644 src/test/resources/regressions/issues/000695.gobra diff --git a/src/main/scala/viper/gobra/reporting/VerifierError.scala b/src/main/scala/viper/gobra/reporting/VerifierError.scala index a2877f4cb..dc997bd12 100644 --- a/src/main/scala/viper/gobra/reporting/VerifierError.scala +++ b/src/main/scala/viper/gobra/reporting/VerifierError.scala @@ -340,7 +340,7 @@ case class ChannelReceiveError(info: Source.Verifier.Info) extends VerificationE case class ChannelSendError(info: Source.Verifier.Info) extends VerificationError { override def localId: String = "send_error" - override def localMessage: String = s"The receive expression ${info.trySrc[PSendStmt](" ")}might fail" + override def localMessage: String = s"The send expression ${info.trySrc[PSendStmt](" ")}might fail" } case class FunctionTerminationError(info: Source.Verifier.Info) extends VerificationError { diff --git a/src/main/scala/viper/gobra/translator/encodings/channels/ChannelEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/channels/ChannelEncoding.scala index 39ece2598..4a6d21074 100644 --- a/src/main/scala/viper/gobra/translator/encodings/channels/ChannelEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/channels/ChannelEncoding.scala @@ -67,7 +67,7 @@ class ChannelEncoding extends LeafTypeEncoding { ) // exhale [c].RecvGivenPerm()() - recvGivenPermInst = getChannelInvariantAccess(channel, recvGivenPerm, Vector())(exp.info) + recvGivenPermInst = getChannelInvariantAccess(channel, recvGivenPerm, Vector.empty, Vector.empty)(exp.info) vprRecvGivenPermInst <- ctx.assertion(recvGivenPermInst) _ <- exhale(vprRecvGivenPermInst, (info, _) => ChannelReceiveError(info) dueTo InsufficientPermissionFromTagError(s"${channel.info.tag}.RecvGivenPerm()()") @@ -84,7 +84,7 @@ class ChannelEncoding extends LeafTypeEncoding { // inhale res != Dflt[T] ==> [c].RecvGotPerm()(res) isNotZero = in.UneqCmp(res, in.DfltVal(res.typ)(exp.info))(exp.info) - recvGotPermInst = getChannelInvariantAccess(channel, recvGotPerm, Vector(res))(exp.info) + recvGotPermInst = getChannelInvariantAccess(channel, recvGotPerm, Vector(res), Vector(typeParam))(exp.info) notZeroImpl = in.Implication(isNotZero, recvGotPermInst)(exp.info) vprNotZeroImpl <- ctx.assertion(notZeroImpl) vprInhaleNotZeroImpl = vpr.Inhale(vprNotZeroImpl)(pos, info, errT) @@ -166,7 +166,7 @@ class ChannelEncoding extends LeafTypeEncoding { } yield ass ) - case stmt@in.Send(channel :: ctx.Channel(_), message, sendChannel, sendGivenPerm, sendGotPerm) => + case stmt@in.Send(channel :: ctx.Channel(typeParam), message, sendChannel, sendGivenPerm, sendGotPerm) => // note that the message type might not be identical to the channel element type but is assignable (as checked by the type checker)! val (pos, info, errT) = stmt.vprMeta val sendChannelPred = in.Accessible.Predicate(in.MPredicateAccess(channel, sendChannel, Vector())(stmt.info)) @@ -179,14 +179,14 @@ class ChannelEncoding extends LeafTypeEncoding { ) // exhale [c].SendGivenPerm()([m]) - sendGivenPermInst = getChannelInvariantAccess(channel, sendGivenPerm, Vector(message))(stmt.info) + sendGivenPermInst = getChannelInvariantAccess(channel, sendGivenPerm, Vector(message), Vector(typeParam))(stmt.info) vprSendGivenPermInst <- ctx.assertion(sendGivenPermInst) _ <- exhale(vprSendGivenPermInst, (info, _) => ChannelSendError(info) dueTo InsufficientPermissionFromTagError(s"${channel.info.tag}.SendGivenPerm()(${message.info.tag})") ) // inhale [c].SendGotPerm()() - sendGotPermInst = getChannelInvariantAccess(channel, sendGotPerm, Vector())(stmt.info) + sendGotPermInst = getChannelInvariantAccess(channel, sendGotPerm, Vector.empty, Vector.empty)(stmt.info) vprSendGotPermInst <- ctx.assertion(sendGotPermInst) vprInhaleSendGotPermInst = vpr.Inhale(vprSendGotPermInst)(pos, info, errT) } yield vprInhaleSendGotPermInst @@ -208,7 +208,7 @@ class ChannelEncoding extends LeafTypeEncoding { ) // exhale [c].RecvGivenPerm()() - recvGivenPermInst = getChannelInvariantAccess(channel, recvGivenPerm, Vector())(stmt.info) + recvGivenPermInst = getChannelInvariantAccess(channel, recvGivenPerm, Vector.empty, Vector.empty)(stmt.info) vprRecvGivenPermInst <- ctx.assertion(recvGivenPermInst) _ <- exhale(vprRecvGivenPermInst, (info, _) => ChannelReceiveError(info) dueTo InsufficientPermissionFromTagError(s"${channel.info.tag}.RecvGivenPerm()()") @@ -227,7 +227,7 @@ class ChannelEncoding extends LeafTypeEncoding { _ <- write(vprInhaleRecvChannelFull) // inhale ok ==> [c].RecvGotPerm()(res) - recvGotPermInst = getChannelInvariantAccess(channel, recvGotPerm, Vector(res))(stmt.info) + recvGotPermInst = getChannelInvariantAccess(channel, recvGotPerm, Vector(res), Vector(typeParam))(stmt.info) okImpl = in.Implication(ok, recvGotPermInst)(stmt.info) vprOkImpl <- ctx.assertion(okImpl) vprInhaleOkImpl = vpr.Inhale(vprOkImpl)(pos, info, errT) @@ -259,8 +259,9 @@ class ChannelEncoding extends LeafTypeEncoding { /** * Constructs `[channel].invariant()([args])` */ - private def getChannelInvariantAccess(channel: in.Expr, invariant: in.MethodProxy, args: Vector[in.Expr])(src: Source.Parser.Info): in.Access = { - val permReturnT = in.PredT(args.map(_.typ), Addressability.outParameter) + private def getChannelInvariantAccess(channel: in.Expr, invariant: in.MethodProxy, args: Vector[in.Expr], argTypes: Vector[in.Type])(src: Source.Parser.Info): in.Access = { + require(args.length == argTypes.length) + val permReturnT = in.PredT(argTypes, Addressability.outParameter) val permPred = in.PureMethodCall(channel, invariant, Vector(), permReturnT)(src) in.Access(in.Accessible.PredExpr(in.PredExprInstance(permPred, args)(src)), in.FullPerm(src))(src) } diff --git a/src/test/resources/regressions/issues/000695.gobra b/src/test/resources/regressions/issues/000695.gobra new file mode 100644 index 000000000..4edad1b2a --- /dev/null +++ b/src/test/resources/regressions/issues/000695.gobra @@ -0,0 +1,32 @@ +package issue000695 + +type ChannelMsgType int + +const ChannelMsg1 = 42 +const ChannelMsg2 ChannelMsgType = 43 + +pred sendInvariant(v ChannelMsgType) { + true +} + +requires acc(channel.SendChannel(), 1/2) +requires channel.SendGivenPerm() == sendInvariant!<_!> +requires channel.SendGotPerm() == PredTrue! +func sendMsg1(channel chan ChannelMsgType) { + fold sendInvariant!<_!>(ChannelMsg1) + fold PredTrue!() + assert acc(channel.SendChannel(), _) && sendInvariant!<_!>(ChannelMsg1) + assert acc(channel.SendChannel(), _) && channel.SendGivenPerm()(ChannelMsg1) + channel <- ChannelMsg1 +} + +requires acc(channel.SendChannel(), 1/2) +requires channel.SendGivenPerm() == sendInvariant!<_!> +requires channel.SendGotPerm() == PredTrue! +func sendMsg2(channel chan ChannelMsgType) { + fold sendInvariant!<_!>(ChannelMsg2) + fold PredTrue!() + assert acc(channel.SendChannel(), _) && sendInvariant!<_!>(ChannelMsg2) + assert acc(channel.SendChannel(), _) && channel.SendGivenPerm()(ChannelMsg2) + channel <- ChannelMsg2 +}