From c364f85d79a0df1f23861e3b913348395edaf4ee Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Thu, 12 Oct 2023 14:22:22 +0200 Subject: [PATCH 1/7] Add syntax for communicate statements --- .../veymont-seq-progs/veymont-swap.pvl | 3 ++- src/parsers/antlr4/LangPVLLexer.g4 | 2 ++ src/parsers/antlr4/LangPVLParser.g4 | 8 +++++++ .../examples/TechnicalVeymontSpec.scala | 24 +++++++++++++++++++ 4 files changed, 36 insertions(+), 1 deletion(-) diff --git a/examples/technical/veymont-seq-progs/veymont-swap.pvl b/examples/technical/veymont-seq-progs/veymont-swap.pvl index e39a0abd21..f98ec31dec 100644 --- 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 index 0dbc74136b..cdeedf22bb 100644 --- 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 index bc3e255b48..e5dbb10a0f 100644 --- 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 index efb144f312..380f910190 100644 --- 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; + } + } +""" } From 11febcf690a8bde454e037ce6e9999e74c4eb309 Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Thu, 12 Oct 2023 15:40:03 +0200 Subject: [PATCH 2/7] Think I have the dataypes and syntax partially done now. --- src/col/vct/col/ast/Node.scala | 15 +++++++++++++++ src/col/vct/col/rewrite/NonLatchingRewriter.scala | 2 ++ src/col/vct/col/typerules/CoercingRewriter.scala | 7 +++++++ src/parsers/antlr4/LangPVLParser.g4 | 10 +++++++--- src/parsers/vct/parsers/transform/PVLToCol.scala | 14 ++++++++++++++ 5 files changed, 45 insertions(+), 3 deletions(-) diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 1f1b171c40..b61def3a5c 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -1211,6 +1211,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] diff --git a/src/col/vct/col/rewrite/NonLatchingRewriter.scala b/src/col/vct/col/rewrite/NonLatchingRewriter.scala index 1e2ec1d4b7..3d24956a5b 100644 --- a/src/col/vct/col/rewrite/NonLatchingRewriter.scala +++ b/src/col/vct/col/rewrite/NonLatchingRewriter.scala @@ -64,4 +64,6 @@ 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: PVLCommunicator[Pre]): PVLCommunicator[Post] = rewriteDefault(node) } \ No newline at end of file diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index 73e8257812..29b7a85e8c 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -445,6 +445,10 @@ 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: PVLCommunicator[Pre]): PVLCommunicator[Pre] = node + def postCoerce(node: PVLCommunicator[Pre]): PVLCommunicator[Post] = rewriteDefault(node) + override final def dispatch(node: PVLCommunicator[Pre]): PVLCommunicator[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 @@ -2099,4 +2103,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 } diff --git a/src/parsers/antlr4/LangPVLParser.g4 b/src/parsers/antlr4/LangPVLParser.g4 index e5dbb10a0f..d731844db8 100644 --- a/src/parsers/antlr4/LangPVLParser.g4 +++ b/src/parsers/antlr4/LangPVLParser.g4 @@ -187,16 +187,20 @@ statement | 'goto' identifier ';' # pvlGoto | 'label' identifier ';' # pvlLabel | allowedForStatement ';' # pvlForStatement - | 'communicate' participant direction participant ';' # communicate + | 'communicate' access direction access ';' # pvlCommunicate ; -participant: identifier communicateRange? '.' identifier ; -communicateRange: '[' identifier ':' expr '..' expr ']' ; direction : '<-' | '->' ; +access: subject '.' identifier; +subject: + : identifier + | identifier '[' expr ']' + | identifier '[' identifier ':' expr '..' expr ']'; + elseBlock: 'else' statement; barrierTags: ';' identifierList; barrierBody: '{' contract '}' | contract block; diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala index 5d19f1ba49..e9293efb9f 100644 --- a/src/parsers/vct/parsers/transform/PVLToCol.scala +++ b/src/parsers/vct/parsers/transform/PVLToCol.scala @@ -354,6 +354,10 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val case PvlGoto(_, label, _) => Goto(new UnresolvedRef[G, LabelDecl[G]](convert(label))) case PvlLabel(_, label, _) => Label(new LabelDecl()(SourceNameOrigin(convert(label), origin(stat))), Block(Nil)) case PvlForStatement(inner, _) => convert(inner) + case PvlCommunicate0(receiver, Direction0("<-"), sender) => + PVLCommunicate(convert(sender), convert(receiver)) + case PvlCommunicate0(sender, Direction1("->"), receiver) => + PVLCommunicate(convert(sender), convert(receiver)) } def convert(implicit stat: ForStatementListContext): Statement[G] = @@ -377,6 +381,16 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val 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(acc), field) + } + + def convert(implicit subject: SubjectContext): PVLCommunicateAccess[G] = subject match { + case Subject0(name) => PVLThreadName(name) + case Subject1(family, _, expr, _) => PVLIndexedFamilyName(family, expr) + case Subject2(family, _, binder, _, start, _, end, _) => PVLFamilyRange(family, binder, start, end) + } + 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)) From d225c89f485a4330baa1142aa0a9bda81093b390 Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Fri, 13 Oct 2023 11:48:42 +0200 Subject: [PATCH 3/7] Syntax and PVL datatypes now look decent --- src/col/vct/col/rewrite/NonLatchingRewriter.scala | 3 ++- src/col/vct/col/typerules/CoercingRewriter.scala | 13 ++++++++++--- src/parsers/antlr4/LangPVLParser.g4 | 4 ++-- src/parsers/vct/parsers/transform/PVLToCol.scala | 14 +++++++------- 4 files changed, 21 insertions(+), 13 deletions(-) diff --git a/src/col/vct/col/rewrite/NonLatchingRewriter.scala b/src/col/vct/col/rewrite/NonLatchingRewriter.scala index 3d24956a5b..0b8b79b9aa 100644 --- a/src/col/vct/col/rewrite/NonLatchingRewriter.scala +++ b/src/col/vct/col/rewrite/NonLatchingRewriter.scala @@ -65,5 +65,6 @@ 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: PVLCommunicator[Pre]): PVLCommunicator[Post] = rewriteDefault(node) + override def dispatch(node: PVLCommunicateAccess[Pre]): PVLCommunicateAccess[Post] = rewriteDefault(node) + override def dispatch(node: PVLCommunicateSubject[Pre]): PVLCommunicateSubject[Post] = rewriteDefault(node) } \ No newline at end of file diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index 29b7a85e8c..8ae669782c 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/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,9 +447,13 @@ 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: PVLCommunicator[Pre]): PVLCommunicator[Pre] = node - def postCoerce(node: PVLCommunicator[Pre]): PVLCommunicator[Post] = rewriteDefault(node) - override final def dispatch(node: PVLCommunicator[Pre]): PVLCommunicator[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 { @@ -1634,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) } } diff --git a/src/parsers/antlr4/LangPVLParser.g4 b/src/parsers/antlr4/LangPVLParser.g4 index d731844db8..48bae3bdf9 100644 --- a/src/parsers/antlr4/LangPVLParser.g4 +++ b/src/parsers/antlr4/LangPVLParser.g4 @@ -187,7 +187,7 @@ statement | 'goto' identifier ';' # pvlGoto | 'label' identifier ';' # pvlLabel | allowedForStatement ';' # pvlForStatement - | 'communicate' access direction access ';' # pvlCommunicate + | 'communicate' access direction access ';' # pvlCommunicateStatement ; direction @@ -196,7 +196,7 @@ direction ; access: subject '.' identifier; -subject: +subject : identifier | identifier '[' expr ']' | identifier '[' identifier ':' expr '..' expr ']'; diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala index e9293efb9f..39cdc67ab2 100644 --- a/src/parsers/vct/parsers/transform/PVLToCol.scala +++ b/src/parsers/vct/parsers/transform/PVLToCol.scala @@ -354,9 +354,9 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val case PvlGoto(_, label, _) => Goto(new UnresolvedRef[G, LabelDecl[G]](convert(label))) case PvlLabel(_, label, _) => Label(new LabelDecl()(SourceNameOrigin(convert(label), origin(stat))), Block(Nil)) case PvlForStatement(inner, _) => convert(inner) - case PvlCommunicate0(receiver, Direction0("<-"), sender) => + case PvlCommunicateStatement(_, receiver, Direction0("<-"), sender, _) => PVLCommunicate(convert(sender), convert(receiver)) - case PvlCommunicate0(sender, Direction1("->"), receiver) => + case PvlCommunicateStatement(_, sender, Direction1("->"), receiver, _) => PVLCommunicate(convert(sender), convert(receiver)) } @@ -382,13 +382,13 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val } def convert(implicit acc: AccessContext): PVLCommunicateAccess[G] = acc match { - case Access0(subject, _, field) => PVLCommunicateAccess(convert(acc), field) + case Access0(subject, _, field) => PVLCommunicateAccess(convert(subject), convert(field)) } - def convert(implicit subject: SubjectContext): PVLCommunicateAccess[G] = subject match { - case Subject0(name) => PVLThreadName(name) - case Subject1(family, _, expr, _) => PVLIndexedFamilyName(family, expr) - case Subject2(family, _, binder, _, start, _, end, _) => PVLFamilyRange(family, binder, start, end) + def convert(implicit subject: SubjectContext): PVLCommunicateSubject[G] = subject match { + case Subject0(name) => PVLThreadName(convert(name)) + case Subject1(family, _, expr, _) => PVLIndexedFamilyName(convert(family), convert(expr)) + case Subject2(family, _, binder, _, start, _, end, _) => PVLFamilyRange(convert(family), convert(binder), convert(start), convert(end)) } def convert(implicit region: ParRegionContext): ParRegion[G] = region match { From 2af1f53c3bfad2e32c1a545914097a870069d010 Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Fri, 13 Oct 2023 12:05:31 +0200 Subject: [PATCH 4/7] Add placeholder failure for communicate statements. Start on extending syntax a bit for proper parameterization --- src/rewrite/vct/rewrite/lang/LangPVLToCol.scala | 11 +++++++++++ .../vct/rewrite/lang/LangSpecificToCol.scala | 2 ++ .../examples/TechnicalVeymontSpec.scala | 14 ++++++++------ 3 files changed, 21 insertions(+), 6 deletions(-) diff --git a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala index d961345e7d..64a8dc82c1 100644 --- a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala @@ -10,6 +10,13 @@ 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} import vct.col.util.{AstBuildHelpers, SuccessionMap} +import vct.result.VerificationError.SystemError + +case object LangPVLToCol { + case object CommunicateNotSupported extends SystemError { + override def text: String = "The `communicate` statement is not yet supported" + } +} case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging { type Post = Rewritten[Pre] @@ -157,4 +164,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 LangPVLToCol.CommunicateNotSupported + } } diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index 7e1786bb06..f4dface306 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -114,6 +114,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) } diff --git a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala index 380f910190..0b1afe0cd8 100644 --- a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala +++ b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala @@ -20,12 +20,14 @@ class TechnicalVeymontSpec extends VercorsSpec { } """ - vercors should error withCode "unsupported" in "parameterized sends not yet supported " pvl - """ - seq_program Example() { + vercors should verify using silicon in "parameterized sends not yet supported " pvl + """ + seq_program Example() { + thread alice[10] = Storage(); + thread bob[10] = Storage(); run { - communicate alice[i: 0 .. 10].x <- bob[i: 0 .. 10].y; + communicate alice[i: 0 .. 9].x <- bob[i + 1].y; } - } -""" + } + """ } From 477a6dd296ca2279ae8506cd409a89c78ecfee9b Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Fri, 13 Oct 2023 15:03:22 +0200 Subject: [PATCH 5/7] Lets wait with full parameterized syntax for now --- src/parsers/vct/parsers/transform/PVLToCol.scala | 4 ++-- src/rewrite/vct/rewrite/lang/LangPVLToCol.scala | 8 +++++--- .../test/integration/examples/TechnicalVeymontSpec.scala | 4 ++-- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala index 39cdc67ab2..f0b4c3438f 100644 --- a/src/parsers/vct/parsers/transform/PVLToCol.scala +++ b/src/parsers/vct/parsers/transform/PVLToCol.scala @@ -387,8 +387,8 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val def convert(implicit subject: SubjectContext): PVLCommunicateSubject[G] = subject match { case Subject0(name) => PVLThreadName(convert(name)) - case Subject1(family, _, expr, _) => PVLIndexedFamilyName(convert(family), convert(expr)) - case Subject2(family, _, binder, _, start, _, end, _) => PVLFamilyRange(convert(family), convert(binder), convert(start), convert(end)) + case Subject1(family, _, expr, _) => ??(subject) + case Subject2(family, _, binder, _, start, _, end, _) => ??(subject) } def convert(implicit region: ParRegionContext): ParRegion[G] = region match { diff --git a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala index 64a8dc82c1..66dc182481 100644 --- a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala @@ -10,11 +10,13 @@ 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} import vct.col.util.{AstBuildHelpers, SuccessionMap} -import vct.result.VerificationError.SystemError +import vct.result.VerificationError.{SystemError, UserError} +import LangPVLToCol.CommunicateNotSupported case object LangPVLToCol { - case object CommunicateNotSupported extends SystemError { + case object CommunicateNotSupported extends UserError { override def text: String = "The `communicate` statement is not yet supported" + override def code: String = "communicateNotSupported" } } @@ -166,6 +168,6 @@ case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L } def communicate(comm: PVLCommunicate[Pre]): VeyMontCommExpression[Post] = { - throw LangPVLToCol.CommunicateNotSupported + throw CommunicateNotSupported } } diff --git a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala index 0b1afe0cd8..960d77642b 100644 --- a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala +++ b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala @@ -3,7 +3,7 @@ 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 + vercors should error withCode "communicateNotSupported" in "example using communicate" pvl """ class Storage { int x; @@ -20,7 +20,7 @@ class TechnicalVeymontSpec extends VercorsSpec { } """ - vercors should verify using silicon in "parameterized sends not yet supported " pvl + vercors should error withCode "parseError" in "parameterized sends not yet supported " pvl """ seq_program Example() { thread alice[10] = Storage(); From d666db98a58afd0fd6b93b78ff2f70b17d919c3c Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Fri, 13 Oct 2023 18:11:08 +0200 Subject: [PATCH 6/7] Save work --- src/col/vct/col/ast/Node.scala | 11 +++++----- .../PVLCommunicateAccesImpl.scala | 7 +++++++ .../PVLCommunicateSubjectImpl.scala | 7 +++++++ .../pvlcommunicate/PVLFamilyRangeImpl.scala | 5 +++++ .../PVLIndexedFamilyNameImpl.scala | 7 +++++++ .../pvlcommunicate/PVLThreadNameImpl.scala | 7 +++++++ src/col/vct/col/resolve/Resolve.scala | 7 +++++++ src/col/vct/col/resolve/ctx/Referrable.scala | 2 +- .../examples/TechnicalVeymontSpec.scala | 21 +++++++++++++++++++ 9 files changed, 68 insertions(+), 6 deletions(-) create mode 100644 src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccesImpl.scala create mode 100644 src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala create mode 100644 src/col/vct/col/ast/family/pvlcommunicate/PVLFamilyRangeImpl.scala create mode 100644 src/col/vct/col/ast/family/pvlcommunicate/PVLIndexedFamilyNameImpl.scala create mode 100644 src/col/vct/col/ast/family/pvlcommunicate/PVLThreadNameImpl.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index b61def3a5c..33e11ea20e 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -55,6 +55,7 @@ import vct.col.ast.family.javavar.JavaVariableDeclarationImpl import vct.col.ast.family.location._ import vct.col.ast.family.loopcontract._ import vct.col.ast.family.parregion._ +import vct.col.ast.family.pvlcommunicate.{PVLCommunicateSubjectImpl, PVLFamilyRangeImpl, PVLIndexedFamilyNameImpl, PVLThreadNameImpl} import vct.col.ast.family.signals._ import vct.col.ast.lang._ import vct.col.ast.lang.smt._ @@ -1211,17 +1212,17 @@ 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] { +sealed trait PVLCommunicateSubject[G] extends NodeFamily[G] with PVLCommunicateSubjectImpl[G] +case class PVLThreadName[G](name: String)(implicit val o: Origin) extends PVLCommunicateSubject[G] with PVLThreadNameImpl[G] { var ref: Option[PVLNameTarget[G]] = None } -case class PVLIndexedFamilyName[G](family: String, index: Expr[G])(implicit val o: Origin) extends PVLCommunicateSubject[G] { +case class PVLIndexedFamilyName[G](family: String, index: Expr[G])(implicit val o: Origin) extends PVLCommunicateSubject[G] with PVLIndexedFamilyNameImpl[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] { +case class PVLFamilyRange[G](family: String, binder: String, start: Expr[G], end: Expr[G])(implicit val o: Origin) extends PVLCommunicateSubject[G] with PVLFamilyRangeImpl[G] { var ref: Option[PVLNameTarget[G]] = None } -case class PVLCommunicateAccess[G](subjectX: PVLCommunicateSubject[G], field: String)(implicit val o: Origin) extends NodeFamily[G] { +case class PVLCommunicateAccess[G](subjectX: PVLCommunicateSubject[G], field: String)(implicit val o: Origin) extends NodeFamily[G] with PVLCommunicateAccessImpl[G] { var ref: Option[PVLDerefTarget[G]] = None } case class PVLCommunicate[G](sender: PVLCommunicateAccess[G], receiver: PVLCommunicateAccess[G])(implicit val o: Origin) extends Statement[G] diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccesImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccesImpl.scala new file mode 100644 index 0000000000..1603af50f8 --- /dev/null +++ b/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccesImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.family.pvlcommunicate + +import vct.col.ast.PVLCommunicateAccess + +trait PVLCommunicateAccesImpl[G] { this: PVLCommunicateAccess[G] => + +} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala new file mode 100644 index 0000000000..ce78463ace --- /dev/null +++ b/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.family.pvlcommunicate + +import vct.col.ast.PVLCommunicateSubject + +trait PVLCommunicateSubjectImpl[G] { this: PVLCommunicateSubject[G] => + +} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLFamilyRangeImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLFamilyRangeImpl.scala new file mode 100644 index 0000000000..71afce982d --- /dev/null +++ b/src/col/vct/col/ast/family/pvlcommunicate/PVLFamilyRangeImpl.scala @@ -0,0 +1,5 @@ +package vct.col.ast.family.pvlcommunicate + +trait PVLFamilyRangeImpl[G] { this: PVLFamilyRangeImpl[G] => + +} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLIndexedFamilyNameImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLIndexedFamilyNameImpl.scala new file mode 100644 index 0000000000..016dd25e94 --- /dev/null +++ b/src/col/vct/col/ast/family/pvlcommunicate/PVLIndexedFamilyNameImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.family.pvlcommunicate + +import vct.col.ast.PVLIndexedFamilyName + +trait PVLIndexedFamilyNameImpl[G] { this: PVLIndexedFamilyName[G] => + +} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLThreadNameImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLThreadNameImpl.scala new file mode 100644 index 0000000000..a06093306a --- /dev/null +++ b/src/col/vct/col/ast/family/pvlcommunicate/PVLThreadNameImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.family.pvlcommunicate + +import vct.col.ast.PVLThreadName + +trait PVLThreadNameImpl[G] { this: PVLThreadName[G] => + +} diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala index 277b41d3b6..4555843ccc 100644 --- a/src/col/vct/col/resolve/Resolve.scala +++ b/src/col/vct/col/resolve/Resolve.scala @@ -277,6 +277,11 @@ case object ResolveReferences extends LazyLogging { case cls: Class[G] => ctx .copy(currentThis=Some(RefClass(cls))) .declare(cls.declarations) + case seqProg: VeyMontSeqProg[G] => ctx + .copy(currentThis=Some(RefSeqProg(seqProg))) + .declare(seqProg.methods) + .declare(seqProg.threads) + .declare(seqProg.progArgs) case method: JavaMethod[G] => ctx .copy(currentResult=Some(RefJavaMethod(method))) .copy(inStaticJavaContext=method.modifiers.collectFirst { case _: JavaStatic[_] => () }.nonEmpty) @@ -376,6 +381,8 @@ case object ResolveReferences extends LazyLogging { local.ref = Some(PVL.findName(name, ctx).getOrElse(throw NoSuchNameError("local", name, local))) case local@Local(ref) => ref.tryResolve(name => Spec.findLocal(name, ctx).getOrElse(throw NoSuchNameError("local", name, local))) + case local @ PVLThreadName(name) => + local.ref = Some(PVL.findName(name, ctx).getOrElse(throw NoSuchNameError("VeyMont thread", name, local))) case local@TVar(ref) => ref.tryResolve(name => Spec.findLocal(name, ctx).getOrElse(throw NoSuchNameError("type variable", name, local))) case funcOf@FunctionOf(v, vars) => diff --git a/src/col/vct/col/resolve/ctx/Referrable.scala b/src/col/vct/col/resolve/ctx/Referrable.scala index 0c77f3357d..2828396d74 100644 --- a/src/col/vct/col/resolve/ctx/Referrable.scala +++ b/src/col/vct/col/resolve/ctx/Referrable.scala @@ -296,7 +296,7 @@ case class RefBipTransitionSynchronization[G](decl: BipTransitionSynchronization case class RefBipConstructor[G](decl: BipConstructor[G]) extends Referrable[G] case class RefLlvmSpecFunction[G](decl: LlvmSpecFunction[G]) extends Referrable[G] with SpecInvocationTarget[G] with ResultTarget[G] -case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G] +case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G] with ThisTarget[G] case class RefVeyMontThread[G](decl: VeyMontThread[G]) extends Referrable[G] with PVLNameTarget[G] case class RefProverType[G](decl: ProverType[G]) extends Referrable[G] with SpecTypeNameTarget[G] case class RefProverFunction[G](decl: ProverFunction[G]) extends Referrable[G] with SpecInvocationTarget[G] diff --git a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala index 960d77642b..4138714a0d 100644 --- a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala +++ b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala @@ -20,8 +20,29 @@ class TechnicalVeymontSpec extends VercorsSpec { } """ + vercors should error withCode "noSuchName" in "non-existent thread name in communicate fails" pvl + """ + seq_program Example() { + run { + communicate charlie.x <- charlie.x; + } + } + """ + + vercors should error withCode "???" in "non-existent field in communicate fails" pvl + """ + class Storage { int x; } + seq_program Example() { + thread charlie = Storage(); + run { + communicate charlie.nonExistent <- charlie.nonExistent; + } + } + """ + vercors should error withCode "parseError" in "parameterized sends not yet supported " pvl """ + class Storage { int x; } seq_program Example() { thread alice[10] = Storage(); thread bob[10] = Storage(); From 2973b56668b8c4835a5232be3d45f54889ad6056 Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Tue, 17 Oct 2023 10:40:44 +0200 Subject: [PATCH 7/7] Revert "Save work" This reverts commit d666db98a58afd0fd6b93b78ff2f70b17d919c3c. --- src/col/vct/col/ast/Node.scala | 11 +++++----- .../PVLCommunicateAccesImpl.scala | 7 ------- .../PVLCommunicateSubjectImpl.scala | 7 ------- .../pvlcommunicate/PVLFamilyRangeImpl.scala | 5 ----- .../PVLIndexedFamilyNameImpl.scala | 7 ------- .../pvlcommunicate/PVLThreadNameImpl.scala | 7 ------- src/col/vct/col/resolve/Resolve.scala | 7 ------- src/col/vct/col/resolve/ctx/Referrable.scala | 2 +- .../examples/TechnicalVeymontSpec.scala | 21 ------------------- 9 files changed, 6 insertions(+), 68 deletions(-) delete mode 100644 src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccesImpl.scala delete mode 100644 src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala delete mode 100644 src/col/vct/col/ast/family/pvlcommunicate/PVLFamilyRangeImpl.scala delete mode 100644 src/col/vct/col/ast/family/pvlcommunicate/PVLIndexedFamilyNameImpl.scala delete mode 100644 src/col/vct/col/ast/family/pvlcommunicate/PVLThreadNameImpl.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 33e11ea20e..b61def3a5c 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -55,7 +55,6 @@ import vct.col.ast.family.javavar.JavaVariableDeclarationImpl import vct.col.ast.family.location._ import vct.col.ast.family.loopcontract._ import vct.col.ast.family.parregion._ -import vct.col.ast.family.pvlcommunicate.{PVLCommunicateSubjectImpl, PVLFamilyRangeImpl, PVLIndexedFamilyNameImpl, PVLThreadNameImpl} import vct.col.ast.family.signals._ import vct.col.ast.lang._ import vct.col.ast.lang.smt._ @@ -1212,17 +1211,17 @@ 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] with PVLCommunicateSubjectImpl[G] -case class PVLThreadName[G](name: String)(implicit val o: Origin) extends PVLCommunicateSubject[G] with PVLThreadNameImpl[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] with PVLIndexedFamilyNameImpl[G] { +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] with PVLFamilyRangeImpl[G] { +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] with PVLCommunicateAccessImpl[G] { +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] diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccesImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccesImpl.scala deleted file mode 100644 index 1603af50f8..0000000000 --- a/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccesImpl.scala +++ /dev/null @@ -1,7 +0,0 @@ -package vct.col.ast.family.pvlcommunicate - -import vct.col.ast.PVLCommunicateAccess - -trait PVLCommunicateAccesImpl[G] { this: PVLCommunicateAccess[G] => - -} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala deleted file mode 100644 index ce78463ace..0000000000 --- a/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala +++ /dev/null @@ -1,7 +0,0 @@ -package vct.col.ast.family.pvlcommunicate - -import vct.col.ast.PVLCommunicateSubject - -trait PVLCommunicateSubjectImpl[G] { this: PVLCommunicateSubject[G] => - -} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLFamilyRangeImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLFamilyRangeImpl.scala deleted file mode 100644 index 71afce982d..0000000000 --- a/src/col/vct/col/ast/family/pvlcommunicate/PVLFamilyRangeImpl.scala +++ /dev/null @@ -1,5 +0,0 @@ -package vct.col.ast.family.pvlcommunicate - -trait PVLFamilyRangeImpl[G] { this: PVLFamilyRangeImpl[G] => - -} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLIndexedFamilyNameImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLIndexedFamilyNameImpl.scala deleted file mode 100644 index 016dd25e94..0000000000 --- a/src/col/vct/col/ast/family/pvlcommunicate/PVLIndexedFamilyNameImpl.scala +++ /dev/null @@ -1,7 +0,0 @@ -package vct.col.ast.family.pvlcommunicate - -import vct.col.ast.PVLIndexedFamilyName - -trait PVLIndexedFamilyNameImpl[G] { this: PVLIndexedFamilyName[G] => - -} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLThreadNameImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLThreadNameImpl.scala deleted file mode 100644 index a06093306a..0000000000 --- a/src/col/vct/col/ast/family/pvlcommunicate/PVLThreadNameImpl.scala +++ /dev/null @@ -1,7 +0,0 @@ -package vct.col.ast.family.pvlcommunicate - -import vct.col.ast.PVLThreadName - -trait PVLThreadNameImpl[G] { this: PVLThreadName[G] => - -} diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala index 4555843ccc..277b41d3b6 100644 --- a/src/col/vct/col/resolve/Resolve.scala +++ b/src/col/vct/col/resolve/Resolve.scala @@ -277,11 +277,6 @@ case object ResolveReferences extends LazyLogging { case cls: Class[G] => ctx .copy(currentThis=Some(RefClass(cls))) .declare(cls.declarations) - case seqProg: VeyMontSeqProg[G] => ctx - .copy(currentThis=Some(RefSeqProg(seqProg))) - .declare(seqProg.methods) - .declare(seqProg.threads) - .declare(seqProg.progArgs) case method: JavaMethod[G] => ctx .copy(currentResult=Some(RefJavaMethod(method))) .copy(inStaticJavaContext=method.modifiers.collectFirst { case _: JavaStatic[_] => () }.nonEmpty) @@ -381,8 +376,6 @@ case object ResolveReferences extends LazyLogging { local.ref = Some(PVL.findName(name, ctx).getOrElse(throw NoSuchNameError("local", name, local))) case local@Local(ref) => ref.tryResolve(name => Spec.findLocal(name, ctx).getOrElse(throw NoSuchNameError("local", name, local))) - case local @ PVLThreadName(name) => - local.ref = Some(PVL.findName(name, ctx).getOrElse(throw NoSuchNameError("VeyMont thread", name, local))) case local@TVar(ref) => ref.tryResolve(name => Spec.findLocal(name, ctx).getOrElse(throw NoSuchNameError("type variable", name, local))) case funcOf@FunctionOf(v, vars) => diff --git a/src/col/vct/col/resolve/ctx/Referrable.scala b/src/col/vct/col/resolve/ctx/Referrable.scala index 2828396d74..0c77f3357d 100644 --- a/src/col/vct/col/resolve/ctx/Referrable.scala +++ b/src/col/vct/col/resolve/ctx/Referrable.scala @@ -296,7 +296,7 @@ case class RefBipTransitionSynchronization[G](decl: BipTransitionSynchronization case class RefBipConstructor[G](decl: BipConstructor[G]) extends Referrable[G] case class RefLlvmSpecFunction[G](decl: LlvmSpecFunction[G]) extends Referrable[G] with SpecInvocationTarget[G] with ResultTarget[G] -case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G] with ThisTarget[G] +case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G] case class RefVeyMontThread[G](decl: VeyMontThread[G]) extends Referrable[G] with PVLNameTarget[G] case class RefProverType[G](decl: ProverType[G]) extends Referrable[G] with SpecTypeNameTarget[G] case class RefProverFunction[G](decl: ProverFunction[G]) extends Referrable[G] with SpecInvocationTarget[G] diff --git a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala index 4138714a0d..960d77642b 100644 --- a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala +++ b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala @@ -20,29 +20,8 @@ class TechnicalVeymontSpec extends VercorsSpec { } """ - vercors should error withCode "noSuchName" in "non-existent thread name in communicate fails" pvl - """ - seq_program Example() { - run { - communicate charlie.x <- charlie.x; - } - } - """ - - vercors should error withCode "???" in "non-existent field in communicate fails" pvl - """ - class Storage { int x; } - seq_program Example() { - thread charlie = Storage(); - run { - communicate charlie.nonExistent <- charlie.nonExistent; - } - } - """ - vercors should error withCode "parseError" in "parameterized sends not yet supported " pvl """ - class Storage { int x; } seq_program Example() { thread alice[10] = Storage(); thread bob[10] = Storage();