VeyMont: Add communicate statement

examples/technical/veymont-seq-progs/veymont-swap.pvl

@@ -29,7 +29,7 @@ seq_program SeqProgram(int x, int y) {
   }
 
   //void bar(int a) {}
-
+  requires x >= 0;
   run {
     if(s1.v == 5 && s2.v == 6) {
     	s1.temp = s1.num();
@@ -54,6 +54,7 @@ seq_program SeqProgram(int x, int y) {
     s1.inc();
     s1.bla(s1.temp);
     // s1.bla(s2.temp);
+    communicate s1.v => s2.temp;
     s1.v = s2.temp;
     s2.v = s1.temp;
     assert s1.v == \old(s2.v);

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

@@ -1210,6 +1210,21 @@ final case class PVLNew[G](t: Type[G], args: Seq[Expr[G]], givenMap: Seq[(Ref[G,
 sealed trait PVLClassDeclaration[G] extends ClassDeclaration[G] with PVLClassDeclarationImpl[G]
 final class PVLConstructor[G](val contract: ApplicableContract[G], val args: Seq[Variable[G]], val body: Option[Statement[G]])(val blame: Blame[ConstructorFailure])(implicit val o: Origin) extends PVLClassDeclaration[G] with PVLConstructorImpl[G]
 
+sealed trait PVLCommunicateSubject[G] extends NodeFamily[G]
+case class PVLThreadName[G](name: String)(implicit val o: Origin) extends PVLCommunicateSubject[G] {
+  var ref: Option[PVLNameTarget[G]] = None
+}
+case class PVLIndexedFamilyName[G](family: String, index: Expr[G])(implicit val o: Origin) extends PVLCommunicateSubject[G] {
+  var ref: Option[PVLNameTarget[G]] = None
+}
+case class PVLFamilyRange[G](family: String, binder: String, start: Expr[G], end: Expr[G])(implicit val o: Origin) extends PVLCommunicateSubject[G] {
+  var ref: Option[PVLNameTarget[G]] = None
+}
+case class PVLCommunicateAccess[G](subjectX: PVLCommunicateSubject[G], field: String)(implicit val o: Origin) extends NodeFamily[G] {
+  var ref: Option[PVLDerefTarget[G]] = None
+}
+case class PVLCommunicate[G](sender: PVLCommunicateAccess[G], receiver: PVLCommunicateAccess[G])(implicit val o: Origin) extends Statement[G]
+
 sealed trait SilverExpr[G] extends Expr[G] with SilverExprImpl[G]
 final case class SilverDeref[G](obj: Expr[G], field: Ref[G, SilverField[G]])(val blame: Blame[InsufficientPermission])(implicit val o: Origin) extends SilverExpr[G] with HeapDeref[G] with SilverDerefImpl[G]
 final case class SilverIntToRat[G](perm: Expr[G])(implicit val o: Origin) extends SilverExpr[G] with SilverIntToRatImpl[G]

src/col/vct/col/rewrite/NonLatchingRewriter.scala

@@ -64,4 +64,7 @@ class NonLatchingRewriter[Pre, Post]() extends AbstractRewriter[Pre, Post] {
 
   override def dispatch(node: LlvmFunctionContract[Pre]): LlvmFunctionContract[Post] = rewriteDefault(node)
   override def dispatch(node: LlvmLoopContract[Pre]): LlvmLoopContract[Post] = rewriteDefault(node)
+
+  override def dispatch(node: PVLCommunicateAccess[Pre]): PVLCommunicateAccess[Post] = rewriteDefault(node)
+  override def dispatch(node: PVLCommunicateSubject[Pre]): PVLCommunicateSubject[Post] = rewriteDefault(node)
 }

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

@@ -247,6 +247,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
     case node: LlvmLoopContract[Pre] => node
     case node: ProverLanguage[Pre] => node
     case node: SmtlibFunctionSymbol[Pre] => node
+    case node: PVLCommunicateAccess[Pre] => node
+    case node: PVLCommunicateSubject[Pre] => node
   }
 
   def preCoerce(e: Expr[Pre]): Expr[Pre] = e
@@ -445,6 +447,14 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
   def postCoerce(node: SmtlibFunctionSymbol[Pre]): SmtlibFunctionSymbol[Post] = rewriteDefault(node)
   override final def dispatch(node: SmtlibFunctionSymbol[Pre]): SmtlibFunctionSymbol[Post] = postCoerce(coerce(preCoerce(node)))
 
+  def preCoerce(node: PVLCommunicateAccess[Pre]): PVLCommunicateAccess[Pre] = node
+  def postCoerce(node: PVLCommunicateAccess[Pre]): PVLCommunicateAccess[Post] = rewriteDefault(node)
+  override final def dispatch(node: PVLCommunicateAccess[Pre]): PVLCommunicateAccess[Post] = postCoerce(coerce(preCoerce(node)))
+
+  def preCoerce(node: PVLCommunicateSubject[Pre]): PVLCommunicateSubject[Pre] = node
+  def postCoerce(node: PVLCommunicateSubject[Pre]): PVLCommunicateSubject[Post] = rewriteDefault(node)
+  override final def dispatch(node: PVLCommunicateSubject[Pre]): PVLCommunicateSubject[Post] = postCoerce(coerce(preCoerce(node)))
+
   def coerce(value: Expr[Pre], target: Type[Pre]): Expr[Pre] =
     ApplyCoercion(value, CoercionUtils.getCoercion(value.t, target) match {
       case Some(coercion) => coercion
@@ -1630,6 +1640,7 @@ 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 VeyMontCommExpression(r,s,t,a) => VeyMontCommExpression(r,s,t,a)
+      case PVLCommunicate(s, r) => PVLCommunicate(s, r)
     }
   }
 
@@ -2099,4 +2110,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
 
   def coerce(node: ProverLanguage[Pre]): ProverLanguage[Pre] = node
   def coerce(node: SmtlibFunctionSymbol[Pre]): SmtlibFunctionSymbol[Pre] = node
+
+  def coerce(node: PVLCommunicateAccess[Pre]): PVLCommunicateAccess[Pre] = node
+  def coerce(node: PVLCommunicateSubject[Pre]): PVLCommunicateSubject[Pre] = node
 }

src/parsers/antlr4/LangPVLLexer.g4

@@ -76,6 +76,8 @@ NOTIFY: 'notify';
 FORK: 'fork';
 JOIN: 'join';
 
+COMMUNICATE: 'communicate';
+
 THIS: 'this';
 NULL: 'null';
 TRUE: 'true';

src/parsers/antlr4/LangPVLParser.g4

@@ -187,8 +187,20 @@ statement
  | 'goto' identifier ';' # pvlGoto
  | 'label' identifier ';' # pvlLabel
  | allowedForStatement ';' # pvlForStatement
+ | 'communicate' access direction access ';' # pvlCommunicateStatement
  ;
 
+direction
+ : '<-'
+ | '->'
+ ;
+
+access: subject '.' identifier;
+subject
+ : identifier
+ | identifier '[' expr ']'
+ | identifier '[' identifier ':' expr '..' expr ']';
+
 elseBlock: 'else' statement;
 barrierTags: ';' identifierList;
 barrierBody: '{' contract '}' | contract block;

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

@@ -356,6 +356,10 @@ case class PVLToCol[G](override val baseOrigin: Origin,
     case PvlGoto(_, label, _) => Goto(new UnresolvedRef[G, LabelDecl[G]](convert(label)))
     case PvlLabel(_, label, _) => Label(new LabelDecl()(origin(stat).replacePrefName(convert(label))), Block(Nil))
     case PvlForStatement(inner, _) => convert(inner)
+    case PvlCommunicateStatement(_, receiver, Direction0("<-"), sender, _) =>
+      PVLCommunicate(convert(sender), convert(receiver))
+    case PvlCommunicateStatement(_, sender, Direction1("->"), receiver, _) =>
+      PVLCommunicate(convert(sender), convert(receiver))
   }
 
   def convert(implicit stat: ForStatementListContext): Statement[G] =
@@ -379,6 +383,16 @@ case class PVLToCol[G](override val baseOrigin: Origin,
     case PvlAssign(target, _, value) => Assign(convert(target), convert(value))(blame(stat))
   }
 
+  def convert(implicit acc: AccessContext): PVLCommunicateAccess[G] = acc match {
+    case Access0(subject, _, field) => PVLCommunicateAccess(convert(subject), convert(field))
+  }
+
+  def convert(implicit subject: SubjectContext): PVLCommunicateSubject[G] = subject match {
+    case Subject0(name) => PVLThreadName(convert(name))
+    case Subject1(family, _, expr, _) => ??(subject)
+    case Subject2(family, _, binder, _, start, _, end, _) => ??(subject)
+  }
+
   def convert(implicit region: ParRegionContext): ParRegion[G] = region match {
     case PvlParallel(_, _, regions, _) => ParParallel(regions.map(convert(_)))(blame(region))
     case PvlSequential(_, _, regions, _) => ParSequential(regions.map(convert(_)))(blame(region))

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

@@ -10,6 +10,15 @@ import vct.col.rewrite.lang.LangSpecificToCol.{NotAValue, ThisVar}
 import vct.col.ref.Ref
 import vct.col.resolve.ctx.{BuiltinField, BuiltinInstanceMethod, ImplicitDefaultPVLConstructor, PVLBuiltinInstanceMethod, RefADTFunction, RefAxiomaticDataType, RefClass, RefEnum, RefEnumConstant, RefField, RefFunction, RefInstanceFunction, RefInstanceMethod, RefInstancePredicate, RefModel, RefModelAction, RefModelField, RefModelProcess, RefPVLConstructor, RefPredicate, RefProcedure, RefProverFunction, RefVariable, RefVeyMontThread, SpecDerefTarget, SpecInvocationTarget, SpecNameTarget}
 import vct.col.util.{AstBuildHelpers, SuccessionMap}
+import vct.result.VerificationError.{SystemError, UserError}
+import LangPVLToCol.CommunicateNotSupported
+
+case object LangPVLToCol {
+  case object CommunicateNotSupported extends UserError {
+    override def text: String = "The `communicate` statement is not yet supported"
+    override def code: String = "communicateNotSupported"
+  }
+}
 
 case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging {
   type Post = Rewritten[Pre]
@@ -116,4 +125,8 @@ case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
           yields.map { case (e, Ref(v)) => (rw.dispatch(e), rw.succ(v)) })(inv.blame)
     }
   }
+
+  def communicate(comm: PVLCommunicate[Pre]): VeyMontCommExpression[Post] = {
+    throw CommunicateNotSupported
+  }
 }

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

@@ -164,6 +164,8 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
     case goto: CGoto[Pre] => c.rewriteGoto(goto)
     case barrier: GpgpuBarrier[Pre] => c.gpuBarrier(barrier)
 
+    case communicate: PVLCommunicate[Pre] => pvl.communicate(communicate)
+
     case other => rewriteDefault(other)
   }
 

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

@@ -3,5 +3,31 @@ package vct.test.integration.examples
 import vct.test.integration.helper.VercorsSpec
 
 class TechnicalVeymontSpec extends VercorsSpec {
+  vercors should error withCode "communicateNotSupported" in "example using communicate" pvl
+  """
+     class Storage {
+        int x;
+     }
+     seq_program Example() {
+        thread alice = Storage();
+        thread bob = Storage();
 
+        run {
+          communicate alice.x <- bob.x;
+          communicate bob.x -> alice.x;
+          assert alice.x == bob.x;
+        }
+     }
+  """
+
+  vercors should error withCode "parseError" in "parameterized sends not yet supported " pvl
+  """
+    seq_program Example() {
+      thread alice[10] = Storage();
+      thread bob[10] = Storage();
+      run {
+        communicate alice[i: 0 .. 9].x <- bob[i + 1].y;
+      }
+    }
+  """
 }