Add syntax for communicate statements

utwente-fmt · Oct 12, 2023 · c364f85 · c364f85
1 parent 6c0cfea
commit c364f85
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 1 deletion.
diff --git a/examples/technical/veymont-seq-progs/veymont-swap.pvl b/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);

diff --git a/src/parsers/antlr4/LangPVLLexer.g4 b/src/parsers/antlr4/LangPVLLexer.g4
@@ -76,6 +76,8 @@ NOTIFY: 'notify';
 FORK: 'fork';
 JOIN: 'join';
 
+COMMUNICATE: 'communicate';
+
 THIS: 'this';
 NULL: 'null';
 TRUE: 'true';

diff --git a/src/parsers/antlr4/LangPVLParser.g4 b/src/parsers/antlr4/LangPVLParser.g4
@@ -187,6 +187,14 @@ statement
  | 'goto' identifier ';' # pvlGoto
  | 'label' identifier ';' # pvlLabel
  | allowedForStatement ';' # pvlForStatement
+ | 'communicate' participant direction participant ';' # communicate
+ ;
+
+participant: identifier communicateRange? '.' identifier ;
+communicateRange: '[' identifier ':' expr '..' expr ']' ;
+direction
+ : '<-'
+ | '->'
  ;
 
 elseBlock: 'else' statement;

diff --git a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala
@@ -3,5 +3,29 @@ package vct.test.integration.examples
 import vct.test.integration.helper.VercorsSpec
 
 class TechnicalVeymontSpec extends VercorsSpec {
+  vercors should verify using silicon 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 "unsupported" in "parameterized sends not yet supported " pvl
+    """
+   seq_program Example() {
+      run {
+        communicate alice[i: 0 .. 10].x <- bob[i: 0 .. 10].y;
+      }
+   }
+"""
 }