Apply patches for disabling assign and communicate checks

src/col/vct/col/ast/Node.scala

@@ -1271,7 +1271,7 @@ case class PVLFamilyRange[G](family: String, binder: String, start: Expr[G], end
 case class PVLAccess[G](subject: PVLSubject[G], field: String)(val blame: Blame[PVLAccessFailure])(implicit val o: Origin) extends NodeFamily[G] with PVLAccessImpl[G] {
   var ref: Option[RefField[G]] = None
 }
-case class PVLCommunicate[G](sender: PVLAccess[G], receiver: PVLAccess[G])(implicit val o: Origin) extends Statement[G] with PVLCommunicateImpl[G]
+case class PVLCommunicate[G](sender: PVLAccess[G], receiver: PVLAccess[G])(val blame: Blame[PVLCommunicateFailure])(implicit val o: Origin) extends Statement[G] with PVLCommunicateImpl[G]
 final case class PVLSeqAssign[G](receiver: Ref[G, PVLEndpoint[G]], field: Ref[G, InstanceField[G]], value: Expr[G])(val blame: Blame[PVLSeqAssignFailure])(implicit val o: Origin) extends Statement[G] with PVLSeqAssignImpl[G]
 
 final class Endpoint[G](val cls: Ref[G, Class[G]], val constructor: Ref[G, Procedure[G]], val args: Seq[Expr[G]])(val blame: Blame[EndpointFailure])(implicit val o: Origin) extends Declaration[G] with EndpointImpl[G]
@@ -1280,7 +1280,7 @@ final case class SeqRun[G](body: Statement[G], contract: ApplicableContract[G])(
 sealed trait Subject[G] extends NodeFamily[G]
 final case class EndpointName[G](ref: Ref[G, Endpoint[G]])(implicit val o: Origin) extends Subject[G] with EndpointNameImpl[G]
 case class Access[G](subject: Subject[G], field: Ref[G, InstanceField[G]])(val blame: Blame[AccessFailure])(implicit val o: Origin) extends NodeFamily[G] with AccessImpl[G]
-final case class Communicate[G](receiver: Access[G], sender: Access[G])(implicit val o: Origin) extends Statement[G] with CommunicateImpl[G]
+final case class Communicate[G](receiver: Access[G], sender: Access[G])(val blame: Blame[CommunicateFailure])(implicit val o: Origin) extends Statement[G] with CommunicateImpl[G]
 final case class SeqAssign[G](receiver: Ref[G, Endpoint[G]], field: Ref[G, InstanceField[G]], value: Expr[G])(val blame: Blame[SeqAssignFailure])(implicit val o: Origin) extends Statement[G] with SeqAssignImpl[G]
 final case class EndpointUse[G](ref: Ref[G, Endpoint[G]])(implicit val o: Origin) extends Expr[G] with EndpointUseImpl[G]
 

src/col/vct/col/origin/Blame.scala

@@ -390,6 +390,15 @@ case class SeqAssignInsufficientPermission(node: SeqAssign[_]) extends SeqAssign
   override def inlineDescWithSource(source: String): String = s"There may be insufficient permission to access `$source`."
 }
 
+sealed trait PVLCommunicateFailure extends VerificationFailure
+sealed trait CommunicateFailure extends PVLCommunicateFailure
+
+case class ParticipantsNotDistinct(node: Communicate[_]) extends CommunicateFailure with NodeVerificationFailure {
+  override def code: String = "participantsNotDistinct"
+  override def descInContext: String = "The participants in this communicate statement might not be distinct."
+  override def inlineDescWithSource(source: String): String = s"The participants of `$source` might not be distinct."
+}
+
 sealed trait DerefInsufficientPermission extends FrontendDerefError
 case class InsufficientPermission(node: HeapDeref[_]) extends DerefInsufficientPermission with NodeVerificationFailure {
   override def code: String = "perm"

src/col/vct/col/rewrite/RewriterBuilderArg.scala

@@ -34,3 +34,21 @@ trait RewriterBuilderArg[T] {
       override def desc: String = RewriterBuilderArg.this.desc
     }
 }
+
+/**
+ * As RewriterBuilderArg, but with 2 parameters.
+ * @tparam T
+ * @tparam U
+ */
+trait RewriterBuilderArg2[T, U] {
+  def apply[Pre <: Generation](t: T, u: U): AbstractRewriter[Pre, _ <: Generation]
+  def key: String
+  def desc: String
+
+  def withArg(t: T, u: U): RewriterBuilder =
+    new RewriterBuilder {
+      override def apply[Pre <: Generation](): AbstractRewriter[Pre, _ <: Generation] = RewriterBuilderArg2.this.apply(t, u)
+      override def key: String = RewriterBuilderArg2.this.key
+      override def desc: String = RewriterBuilderArg2.this.desc
+    }
+}

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -1683,9 +1683,9 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case w @ WandPackage(expr, stat) => WandPackage(res(expr), stat)(w.blame)
       case VeyMontAssignExpression(t,a) => VeyMontAssignExpression(t,a)
       case CommunicateX(r,s,t,a) => CommunicateX(r,s,t,a)
-      case c @ PVLCommunicate(s, r) if r.fieldType == s.fieldType => PVLCommunicate(s, r)
+      case c @ PVLCommunicate(s, r) if r.fieldType == s.fieldType => PVLCommunicate(s, r)(c.blame)
       case comm@PVLCommunicate(s, r) => throw IncoercibleExplanation(comm, s"The receiver should have type ${s.fieldType}, but actually has type ${r.fieldType}.")
-      case c @ Communicate(r, s) if r.field.decl.t == s.field.decl.t => Communicate(r, s)
+      case c @ Communicate(r, s) if r.field.decl.t == s.field.decl.t => Communicate(r, s)(c.blame)
       case comm@Communicate(r, s) => throw IncoercibleExplanation(comm, s"The receiver should have type ${s.field.decl.t}, but actually has type ${r.field.decl.t}.")
       case a @ PVLSeqAssign(r, f, v) =>
         try { PVLSeqAssign(r, f, coerce(v, f.decl.t))(a.blame) } catch {

src/main/vct/main/stages/Resolution.scala

@@ -36,7 +36,8 @@ case object Resolution {
         case ClassPathEntry.SourcePackageRoot => ResolveTypes.JavaClassPathEntry.SourcePackageRoot
         case ClassPathEntry.SourcePath(root) => ResolveTypes.JavaClassPathEntry.Path(root)
       },
-      options.veymontGeneratePermissions
+      options.veymontGeneratePermissions,
+      options.devVeymontAllowAssign,
     )
 }
 
@@ -100,6 +101,7 @@ case class Resolution[G <: Generation]
     ResolveTypes.JavaClassPathEntry.SourcePackageRoot
   ),
   veymontGeneratePermissions: Boolean = false,
+  veymontAllowAssign: Boolean = false,
 ) extends Stage[ParseResult[G], Verification[_ <: Generation]] with LazyLogging {
   override def friendlyName: String = "Name Resolution"
 
@@ -117,7 +119,7 @@ case class Resolution[G <: Generation]
       case Nil => // ok
       case some => throw InputResolutionError(some)
     }
-    val resolvedProgram = LangSpecificToCol(veymontGeneratePermissions).dispatch(typedProgram)
+    val resolvedProgram = LangSpecificToCol(veymontGeneratePermissions, veymontAllowAssign).dispatch(typedProgram)
     resolvedProgram.check match {
       case Nil => // ok
       // PB: This explicitly allows LangSpecificToCol to generate invalid ASTs, and will blame the input for them. The

src/main/vct/options/Options.scala

@@ -244,6 +244,10 @@ case object Options {
         .action((_, c) => c.copy(veymontGeneratePermissions = true))
         .text("Generate permissions for the entire sequential program in the style of VeyMont 1.4"),
 
+      opt[Unit]("dev-veymont-allow-assign").maybeHidden()
+        .action((p, c) => c.copy(devVeymontAllowAssign = true))
+        .text("Do not error when plain assignment is used in seq_programs"),
+
       note(""),
       note("VeyMont Mode"),
       opt[Unit]("veymont")
@@ -394,6 +398,7 @@ case class Options
   veymontOutput: Path = null, // required
   veymontChannel: PathOrStd = PathOrStd.Path(getVeymontChannel),
   veymontGeneratePermissions: Boolean = false,
+  devVeymontAllowAssign: Boolean = false,
 
   // VeSUV options
   vesuvOutput: Path = null,

src/parsers/vct/parsers/transform/PVLToCol.scala

@@ -357,9 +357,9 @@ case class PVLToCol[G](override val baseOrigin: Origin,
     case PvlLabel(_, label, _) => Label(new LabelDecl()(origin(stat).sourceName(convert(label))), Block(Nil))
     case PvlForStatement(inner, _) => convert(inner)
     case PvlCommunicateStatement(_, receiver, Direction0("<-"), sender, _) =>
-      PVLCommunicate(convert(sender), convert(receiver))
+      PVLCommunicate(convert(sender), convert(receiver))(blame(stat))
     case PvlCommunicateStatement(_, sender, Direction1("->"), receiver, _) =>
-      PVLCommunicate(convert(sender), convert(receiver))
+      PVLCommunicate(convert(sender), convert(receiver))(blame(stat))
     case PvlSeqAssign(endpoint, _, field, _, _, expr, _) =>
       PVLSeqAssign(
         new UnresolvedRef[G, PVLEndpoint[G]](convert(endpoint)),

src/rewrite/vct/rewrite/lang/LangPVLToCol.scala

@@ -145,4 +145,11 @@ case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre], veymontGe
     case PVLLoop(init, cond, update, contract, body) =>
       Loop(rw.dispatch(init), rw.dispatch(cond), rw.dispatch(update), rw.dispatch(contract), rw.dispatch(body))(loop.o)
   }
+
+  def assign(assign: Assign[Pre]): Statement[Post] =
+    if (rw.veymont.currentProg.nonEmpty)
+      rw.veymont.rewriteAssign(assign)
+    else
+      assign.rewriteDefault()
+
 }

src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala

@@ -10,11 +10,11 @@ import vct.col.ref.Ref
 import vct.col.resolve.ctx._
 import vct.col.resolve.lang.Java
 import vct.rewrite.lang.LangSpecificToCol.NotAValue
-import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, RewriterBuilderArg}
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, RewriterBuilderArg, RewriterBuilderArg2}
 import vct.result.VerificationError.UserError
 import vct.rewrite.lang.LangVeyMontToCol
 
-case object LangSpecificToCol extends RewriterBuilderArg[Boolean] {
+case object LangSpecificToCol extends RewriterBuilderArg2[Boolean, Boolean] {
   override def key: String = "langSpecific"
   override def desc: String = "Translate language-specific constructs to a common subset of nodes."
 
@@ -31,13 +31,13 @@ case object LangSpecificToCol extends RewriterBuilderArg[Boolean] {
   }
 }
 
-case class LangSpecificToCol[Pre <: Generation](veymontGeneratePermissions: Boolean = false) extends Rewriter[Pre] with LazyLogging {
+case class LangSpecificToCol[Pre <: Generation](veymontGeneratePermissions: Boolean = false, veymontAllowAssign: Boolean = false) extends Rewriter[Pre] with LazyLogging {
   val java: LangJavaToCol[Pre] = LangJavaToCol(this)
   val bip: LangBipToCol[Pre] = LangBipToCol(this)
   val c: LangCToCol[Pre] = LangCToCol(this)
   val cpp: LangCPPToCol[Pre] = LangCPPToCol(this)
   val pvl: LangPVLToCol[Pre] = LangPVLToCol(this, veymontGeneratePermissions)
-  val veymont: LangVeyMontToCol[Pre] = LangVeyMontToCol(this)
+  val veymont: LangVeyMontToCol[Pre] = LangVeyMontToCol(this, veymontAllowAssign)
   val silver: LangSilverToCol[Pre] = LangSilverToCol(this)
   val llvm: LangLLVMToCol[Pre] = LangLLVMToCol(this)
 
@@ -173,6 +173,7 @@ case class LangSpecificToCol[Pre <: Generation](veymontGeneratePermissions: Bool
 
     case communicate: PVLCommunicate[Pre] => veymont.rewriteCommunicate(communicate)
     case assign: PVLSeqAssign[Pre] => veymont.rewriteSeqAssign(assign)
+    case assign: Assign[Pre] => pvl.assign(assign)
 
     case other => rewriteDefault(other)
   }

src/rewrite/vct/rewrite/lang/LangVeyMontToCol.scala

@@ -2,13 +2,14 @@ package vct.rewrite.lang
 
 import com.typesafe.scalalogging.LazyLogging
 import hre.util.ScopedStack
+import vct.col.ast.RewriteHelpers.RewriteAssign
 import vct.col.ast._
 import vct.col.origin.Origin
 import vct.col.resolve.ctx.RefPVLEndpoint
 import vct.col.rewrite.{Generation, Rewritten}
 import vct.col.util.SuccessionMap
 import vct.result.VerificationError.UserError
-import vct.rewrite.lang.LangVeyMontToCol.NoRunMethod
+import vct.rewrite.lang.LangVeyMontToCol.{AssignNotAllowed, NoRunMethod}
 
 case object LangVeyMontToCol {
   case object EndpointUseNotSupported extends UserError {
@@ -22,9 +23,16 @@ case object LangVeyMontToCol {
       s"This `seq_program` has no `run` method."
     )
   }
+
+  case class AssignNotAllowed(assign: Assign[_]) extends UserError {
+    override def code: String = "assignNotAllowed"
+    override def text: String = assign.o.messageInContext(
+      "Plain assignment is not allowed in `seq_program`. Use `:=` instead."
+    )
+  }
 }
 
-case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging {
+case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre], allowAssign: Boolean = false) extends LazyLogging {
   type Post = Rewritten[Pre]
   implicit val implicitRewriter: AbstractRewriter[Pre, Post] = rw
 
@@ -34,7 +42,7 @@ case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) exten
   val currentProg: ScopedStack[PVLSeqProg[Pre]] = ScopedStack()
 
   def rewriteCommunicate(comm: PVLCommunicate[Pre]): Communicate[Post] =
-    Communicate(rewriteAccess(comm.receiver), rewriteAccess(comm.sender))(comm.o)
+    Communicate(rewriteAccess(comm.receiver), rewriteAccess(comm.sender))(comm.blame)(comm.o)
 
   def rewriteAccess(access: PVLAccess[Pre]): Access[Post] =
     Access[Post](rewriteSubject(access.subject), rw.succ(access.ref.get.decl))(access.blame)(access.o)
@@ -93,6 +101,10 @@ case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) exten
   def rewriteSeqAssign(assign: PVLSeqAssign[Pre]): SeqAssign[Post] =
     SeqAssign[Post](endpointSucc.ref(assign.receiver.decl), rw.succ(assign.field.decl), rw.dispatch(assign.value))(assign.blame)(assign.o)
 
+  def rewriteAssign(assign: Assign[Pre]): Statement[Post] =
+    if (allowAssign) assign.rewriteDefault()
+    else throw AssignNotAllowed(assign)
+
   def rewriteBranch(branch: PVLBranch[Pre]): UnresolvedSeqBranch[Post] =
     UnresolvedSeqBranch(branch.branches.map { case (e, s) => (rw.dispatch(e), rw.dispatch(s)) })(branch.blame)(branch.o)
 

src/rewrite/vct/rewrite/veymont/EncodeSeqProg.scala

@@ -2,12 +2,13 @@ package vct.rewrite.veymont
 
 import com.typesafe.scalalogging.LazyLogging
 import hre.util.ScopedStack
-import vct.col.ast.{Access, Assign, Block, Class, Communicate, Declaration, Deref, Endpoint, EndpointName, EndpointUse, Eval, Expr, InstanceMethod, Local, LocalDecl, MethodInvocation, Node, Procedure, Scope, SeqAssign, SeqProg, SeqRun, Statement, Subject, TClass, TVoid, ThisSeqProg, Variable}
-import vct.col.origin.{AccessFailure, AccessInsufficientPermission, AssignFailed, AssignLocalOk, Blame, CallableFailure, ContextEverywhereFailedInPost, ContextEverywhereFailedInPre, ContractedFailure, DiagnosticOrigin, EndpointContextEverywhereFailedInPre, EndpointPreconditionFailed, ExceptionNotInSignals, InsufficientPermission, InvocationFailure, Origin, PanicBlame, PostconditionFailed, PreconditionFailed, SeqAssignFailure, SeqAssignInsufficientPermission, SeqCallableFailure, SeqRunContextEverywhereFailedInPre, SeqRunPreconditionFailed, SignalsFailed, TerminationMeasureFailed, VerificationFailure}
+import vct.col.ast.{Access, Assert, Assign, Block, Class, Communicate, Declaration, Deref, Endpoint, EndpointName, EndpointUse, Eval, Expr, InstanceMethod, Local, LocalDecl, MethodInvocation, Node, Procedure, Scope, SeqAssign, SeqProg, SeqRun, Statement, Subject, TClass, TVoid, ThisSeqProg, Variable}
+import vct.col.origin.{AccessFailure, AccessInsufficientPermission, AssertFailed, AssignFailed, AssignLocalOk, Blame, CallableFailure, ContextEverywhereFailedInPost, ContextEverywhereFailedInPre, ContractedFailure, DiagnosticOrigin, EndpointContextEverywhereFailedInPre, EndpointPreconditionFailed, ExceptionNotInSignals, InsufficientPermission, InvocationFailure, Origin, PanicBlame, ParticipantsNotDistinct, PostconditionFailed, PreconditionFailed, SeqAssignFailure, SeqAssignInsufficientPermission, SeqCallableFailure, SeqRunContextEverywhereFailedInPre, SeqRunPreconditionFailed, SignalsFailed, TerminationMeasureFailed, VerificationFailure}
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
 import vct.col.util.AstBuildHelpers._
 import vct.col.util.SuccessionMap
 import vct.result.VerificationError.{Unreachable, UserError}
+import EncodeSeqProg.{AssertFailedToParticipantsNotDistinct, AssignFailedToSeqAssignFailure, CallableFailureToSeqCallableFailure, InsufficientPermissionToAccessFailure}
 import vct.col.ref.Ref
 
 import scala.collection.{mutable => mut}
@@ -54,6 +55,10 @@ object EncodeSeqProg extends RewriterBuilder {
       case ContextEverywhereFailedInPre(failure, _) => endpoint.blame.blame(EndpointContextEverywhereFailedInPre(failure, endpoint))
     }
   }
+
+  case class AssertFailedToParticipantsNotDistinct(comm: Communicate[_]) extends Blame[AssertFailed] {
+    override def blame(error: AssertFailed): Unit = comm.blame.blame(ParticipantsNotDistinct(comm))
+  }
 }
 
 case class EncodeSeqProg[Pre <: Generation]() extends Rewriter[Pre] with LazyLogging {
@@ -197,10 +202,15 @@ case class EncodeSeqProg[Pre <: Generation]() extends Rewriter[Pre] with LazyLog
       )(AssignFailedToSeqAssignFailure(assign))
     case comm @ Communicate(receiver, sender) =>
       implicit val o = comm.o
-      Assign[Post](
-        rewriteAccess(receiver),
-        rewriteAccess(sender)
-      )(InsufficientPermissionToAccessFailure(receiver))
+      Block(Seq(
+        Assert(
+          rewriteSubject(receiver.subject) !== rewriteSubject(sender.subject)
+        )(AssertFailedToParticipantsNotDistinct(comm)),
+        Assign[Post](
+          rewriteAccess(receiver),
+          rewriteAccess(sender)
+        )(InsufficientPermissionToAccessFailure(receiver))
+      ))
     case stat => rewriteDefault(stat)
   }
 

test/main/vct/test/integration/examples/TechnicalVeyMontSpec.scala

@@ -788,8 +788,8 @@ class TechnicalVeyMontSpec extends VercorsSpec {
     in "Precondition of seq_run should be checked"
     pvl
     """
-    seq_program Example() {
-      requires 1 == 0;
+    seq_program Example(int x) {
+      requires x == 0;
       seq_run {
       }
     }
@@ -799,11 +799,11 @@ class TechnicalVeyMontSpec extends VercorsSpec {
     should fail
     withCode "seqRunContextEverywhereFailed"
     using silicon
-    in "Precondition of seq_run should be checked"
+    in "Context everywhere of seq_run should be checked"
     pvl
     """
-    seq_program Example() {
-      context_everywhere 1 == 0;
+    seq_program Example(int x) {
+      context_everywhere x == 0;
       seq_run {
       }
     }
@@ -822,10 +822,69 @@ class TechnicalVeyMontSpec extends VercorsSpec {
     }
 
     seq_program Example() {
-        endpoint alice = Storage(1);
+      endpoint alice = Storage(1);
 
-        seq_run {
-        }
+      seq_run {
+      }
+    }
+    """)
+
+  (vercors
+    should error
+    withCode "assignNotAllowed"
+    flag "--veymont-generate-permissions"
+    in "Assignment should be disallowed in seq_program"
+    pvl
+    """
+    class Storage {
+      int x;
+    }
+
+    seq_program Example() {
+      endpoint alice = Storage();
+      seq_run {
+        alice.x = 0;
+      }
+    }
+    """)
+
+  (vercors
+    should verify
+    using silicon
+    flag "--veymont-generate-permissions"
+    flag "--dev-veymont-allow-assign"
+    in "At user discretion, assignment should be allowed"
+    pvl
+    """
+    class Storage {
+      int x;
+    }
+
+    seq_program Example() {
+      endpoint alice = Storage();
+      seq_run {
+        alice.x = 0;
+      }
+    }
+    """)
+
+  (vercors
+    should fail
+    withCode "participantsNotDistinct"
+    using silicon
+    flag "--veymont-generate-permissions"
+    in "Endpoints participating in a communicate should be distinct"
+    pvl
+    """
+    class Storage {
+      int x;
+    }
+
+    seq_program Example() {
+      endpoint alice = Storage();
+      seq_run {
+        communicate alice.x <- alice.x;
+      }
     }
     """)
 }

test/main/vct/test/integration/helper/VercorsSpec.scala

@@ -198,8 +198,8 @@ abstract class VercorsSpec extends AnyFlatSpec {
 
     def in(desc: String): DescPhrase = new DescPhrase(verdict, backends, desc, _flags)
 
-    def flags(args: Seq[String]): BackendPhrase = new BackendPhrase(verdict, reportPath, backends, args)
-    def flag(arg: String): BackendPhrase = new BackendPhrase(verdict, reportPath, backends, Seq(arg))
+    def flags(args: Seq[String]): BackendPhrase = new BackendPhrase(verdict, reportPath, backends, _flags ++ args)
+    def flag(arg: String): BackendPhrase = new BackendPhrase(verdict, reportPath, backends, _flags :+ arg)
   }
 
   class DescPhrase(val verdict: Verdict, val backends: Seq[Backend], val desc: String, val flags: Seq[String]) {