adapts channel encoding to allow assignable instead of equal message …

…types for channel send operations

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 {

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)
   }

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
+}