Merge remote-tracking branch 'origin/dev' into better-c-support

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

@@ -56,7 +56,8 @@ 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._
+import vct.col.ast.family.pvlcommunicate.{PVLAccessImpl, PVLCommunicateImpl, PVLSubjectImpl, PVLEndpointNameImpl, PVLFamilyRangeImpl, PVLIndexedFamilyNameImpl}
+import vct.col.ast.family.seqguard._
 import vct.col.ast.family.seqrun.SeqRunImpl
 import vct.col.ast.family.signals._
 import vct.col.ast.family.subject.EndpointNameImpl
@@ -159,6 +160,9 @@ final case class IterVariable[G](variable: Variable[G], from: Expr[G], to: Expr[
 
 sealed trait Statement[G] extends NodeFamily[G] with StatementImpl[G]
 
+final case class PVLBranch[G](branches: Seq[(Expr[G], Statement[G])])(val blame: Blame[FrontendIfFailure])(implicit val o: Origin) extends Statement[G]
+final case class PVLLoop[G](init: Statement[G], cond: Expr[G], update: Statement[G], contract: LoopContract[G], body: Statement[G])(val blame: Blame[FrontEndLoopFailure])(implicit val o: Origin) extends Statement[G]
+
 sealed trait NonExecutableStatement[G] extends Statement[G] with NonExecutableStatementImpl[G]
 final case class LocalDecl[G](local: Variable[G])(implicit val o: Origin) extends NonExecutableStatement[G] with LocalDeclImpl[G]
 final case class SpecIgnoreStart[G]()(implicit val o: Origin) extends NonExecutableStatement[G] with SpecIgnoreStartImpl[G]
@@ -565,7 +569,6 @@ final case class Star[G](left: Expr[G], right: Expr[G])(implicit val o: Origin)
 final case class Wand[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends Expr[G] with WandImpl[G]
 final case class Scale[G](scale: Expr[G], res: Expr[G])(val blame: Blame[ScaleNegative])(implicit val o: Origin) extends Expr[G] with ScaleImpl[G]
 final case class ScaleByParBlock[G](block: Ref[G, ParBlockDecl[G]], res: Expr[G])(implicit val o: Origin) extends Expr[G] with ScaleByParBlockImpl[G]
-final case class VeyMontCondition[G](condition: Seq[(Ref[G, Endpoint[G]], Expr[G])])(implicit val o: Origin) extends Expr[G] with VeyMontConditionImpl[G]
 final case class PolarityDependent[G](onInhale: Expr[G], onExhale: Expr[G])(implicit val o: Origin) extends Expr[G] with PolarityDependentImpl[G]
 
 final case class Unfolding[G](res: Expr[G], body: Expr[G])(val blame: Blame[UnfoldFailed])(implicit val o: Origin) extends Expr[G] with UnfoldingImpl[G]
@@ -1289,35 +1292,45 @@ final case class TEndpoint[G](cls: Ref[G, Endpoint[G]])(implicit val o: Origin =
 final class PVLEndpoint[G](val name: String, val cls: Ref[G, Class[G]], val args: Seq[Expr[G]])(implicit val o: Origin) extends ClassDeclaration[G] {
   var ref: Option[PVLConstructorTarget[G]] = None
 }
-final class PVLSeqProg[G](val name: String, val declarations: Seq[ClassDeclaration[G]], val contract: ApplicableContract[G], val args: Seq[Variable[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with PVLSeqProgImpl[G] with Declarator[G]
-final case class PVLSeqRun[G](body: Statement[G], contract: ApplicableContract[G])(val blame: Blame[CallableFailure])(implicit val o: Origin) extends ClassDeclaration[G]
+final class PVLSeqProg[G](val name: String, val declarations: Seq[ClassDeclaration[G]], val contract: ApplicableContract[G], val args: Seq[Variable[G]])(val blame: Blame[SeqCallableFailure])(implicit val o: Origin) extends GlobalDeclaration[G] with PVLSeqProgImpl[G] with Declarator[G]
+final case class PVLSeqRun[G](body: Statement[G], contract: ApplicableContract[G])(val blame: Blame[SeqCallableFailure])(implicit val o: Origin) extends ClassDeclaration[G]
 
-sealed trait PVLCommunicateSubject[G] extends NodeFamily[G] with PVLCommunicateSubjectImpl[G]
-case class PVLEndpointName[G](name: String)(implicit val o: Origin) extends PVLCommunicateSubject[G] with PVLEndpointNameImpl[G] {
+sealed trait PVLSubject[G] extends NodeFamily[G] with PVLSubjectImpl[G]
+case class PVLEndpointName[G](name: String)(implicit val o: Origin) extends PVLSubject[G] with PVLEndpointNameImpl[G] {
   var ref: Option[RefPVLEndpoint[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 PVLSubject[G] with PVLIndexedFamilyNameImpl[G] {
   var ref: Option[RefPVLEndpoint[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 PVLSubject[G] with PVLFamilyRangeImpl[G] {
   var ref: Option[RefPVLEndpoint[G]] = None
 }
-case class PVLCommunicateAccess[G](subject: PVLCommunicateSubject[G], field: String)(implicit val o: Origin) extends NodeFamily[G] with PVLCommunicateAccessImpl[G] {
+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: PVLCommunicateAccess[G], receiver: PVLCommunicateAccess[G])(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])(implicit val o: Origin) extends Statement[G] with PVLSeqAssignImpl[G]
+case class PVLCommunicate[G](sender: PVLAccess[G], receiver: PVLAccess[G])(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]])(implicit val o: Origin) extends Declaration[G] with EndpointImpl[G]
-final class SeqProg[G](val contract: ApplicableContract[G], val args : Seq[Variable[G]], val endpoints: Seq[Endpoint[G]], val run: SeqRun[G], val decls: Seq[ClassDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with SeqProgImpl[G]
-final case class SeqRun[G](body: Statement[G], contract: ApplicableContract[G])(val blame: Blame[CallableFailure])(implicit val o: Origin) extends NodeFamily[G] with SeqRunImpl[G]
+final class SeqProg[G](val contract: ApplicableContract[G], val args : Seq[Variable[G]], val endpoints: Seq[Endpoint[G]], val run: SeqRun[G], val decls: Seq[ClassDeclaration[G]])(val blame: Blame[SeqCallableFailure])(implicit val o: Origin) extends GlobalDeclaration[G] with SeqProgImpl[G]
+final case class SeqRun[G](body: Statement[G], contract: ApplicableContract[G])(val blame: Blame[SeqCallableFailure])(implicit val o: Origin) extends NodeFamily[G] with SeqRunImpl[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]])(implicit val o: Origin) extends NodeFamily[G] with AccessImpl[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 SeqAssign[G](receiver: Ref[G, Endpoint[G]], field: Ref[G, InstanceField[G]], value: Expr[G])(implicit val o: Origin) extends Statement[G] with SeqAssignImpl[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]
 
+final case class UnresolvedSeqBranch[G](branches: Seq[(Expr[G], Statement[G])])(val blame: Blame[SeqBranchFailure])(implicit val o: Origin) extends Statement[G]
+final case class UnresolvedSeqLoop[G](cond: Expr[G], contract: LoopContract[G], body: Statement[G])(val blame: Blame[SeqLoopFailure])(implicit val o: Origin) extends Statement[G]
+
+sealed trait SeqGuard[G] extends NodeFamily[G] with SeqGuardImpl[G]
+final case class EndpointGuard[G](endpoint: Ref[G, Endpoint[G]], condition: Expr[G])(implicit val o: Origin) extends SeqGuard[G] with EndpointGuardImpl[G]
+final case class UnpointedGuard[G](condition: Expr[G])(implicit val o: Origin) extends SeqGuard[G] with UnpointedGuardImpl[G]
+
+final case class SeqBranch[G](guards: Seq[SeqGuard[G]], yes: Statement[G], no:  Option[Statement[G]])(val blame: Blame[SeqBranchFailure])(implicit val o: Origin) extends Statement[G] with SeqBranchImpl[G]
+final case class SeqLoop[G](guards: Seq[SeqGuard[G]], contract: LoopContract[G], body: Statement[G])(val blame: Blame[SeqLoopFailure])(implicit val o: Origin) extends Statement[G] with SeqLoopImpl[G]
+
 final case class VeyMontAssignExpression[G](endpoint: Ref[G, Endpoint[G]], assign: Statement[G])(implicit val o: Origin) extends Statement[G] with VeyMontAssignExpressionImpl[G]
 final case class CommunicateX[G](receiver: Ref[G, Endpoint[G]], sender: Ref[G, Endpoint[G]], chanType: Type[G], assign: Statement[G])(implicit val o: Origin) extends Statement[G] with CommunicateXImpl[G]
 

src/col/vct/col/ast/declaration/global/SeqProgImpl.scala

@@ -1,10 +1,22 @@
 package vct.col.ast.declaration.global
 
-import vct.col.ast.{Class, Declaration, SeqProg}
+import vct.col.ast.{Class, Declaration, Endpoint, EndpointGuard, EndpointName, Node, SeqAssign, SeqProg}
 import vct.col.ast.util.Declarator
 import vct.col.check.{CheckContext, CheckError}
 import vct.col.origin.Origin
 import vct.col.print._
+import vct.col.ref.Ref
+
+import scala.collection.immutable.ListSet
+
+object SeqProgImpl {
+  def participants[G](node: Node[G]): ListSet[Endpoint[G]] =
+    ListSet.from(node.collect {
+      case EndpointGuard(Ref(endpoint), _) => endpoint
+      case SeqAssign(Ref(endpoint), _, _) => endpoint
+      case EndpointName(Ref(endpoint)) => endpoint
+    })
+}
 
 trait SeqProgImpl[G] extends Declarator[G] { this: SeqProg[G] =>
   override def declarations: Seq[Declaration[G]] = args ++ endpoints ++ decls
@@ -18,5 +30,7 @@ trait SeqProgImpl[G] extends Declarator[G] { this: SeqProg[G] =>
     ))
 
   override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    super.enterCheckContext(context).withSeqProg(this)
+    super.enterCheckContext(context)
+      .withSeqProg(this)
+      .withCurrentParticipatingEndpoints(endpoints)
 }

src/col/vct/col/ast/family/pvlcommunicate/PVLAccessImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.family.pvlcommunicate
+
+import vct.col.ast.{PVLAccess, Type}
+
+trait PVLAccessImpl[G] { this: PVLAccess[G] =>
+  def fieldType: Type[G] = ref.get.decl.t
+}

src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala → src/col/vct/col/ast/family/pvlcommunicate/PVLSubjectImpl.scala

@@ -1,9 +1,9 @@
 package vct.col.ast.family.pvlcommunicate
 
-import vct.col.ast.{PVLCommunicateSubject, TClass, Class, Type}
+import vct.col.ast.{PVLSubject, TClass, Class, Type}
 import vct.col.resolve.ctx.RefPVLEndpoint
 
-trait PVLCommunicateSubjectImpl[G] { this: PVLCommunicateSubject[G] =>
+trait PVLSubjectImpl[G] { this: PVLSubject[G] =>
   def cls: Class[G] = ref.get.decl.cls.decl
   def ref: Option[RefPVLEndpoint[G]]
 }

src/col/vct/col/ast/family/seqguard/EndpointGuardImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.family.seqguard
+
+import vct.col.ast.EndpointGuard
+
+trait EndpointGuardImpl[G] { this: EndpointGuard[G] =>
+  def endpointOpt = Some(endpoint.decl)
+}

src/col/vct/col/ast/family/seqguard/SeqGuardImpl.scala

@@ -0,0 +1,8 @@
+package vct.col.ast.family.seqguard
+
+import vct.col.ast.{Endpoint, Expr, SeqGuard, UnpointedGuard}
+
+trait SeqGuardImpl[G] { this: SeqGuard[G] =>
+  def condition: Expr[G]
+  def endpointOpt: Option[Endpoint[G]]
+}

src/col/vct/col/ast/family/seqguard/UnpointedGuardImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.family.seqguard
+
+import vct.col.ast.UnpointedGuard
+
+trait UnpointedGuardImpl[G] { this: UnpointedGuard[G] =>
+  def endpointOpt = None
+}

src/col/vct/col/ast/statement/StatementImpl.scala

@@ -1,10 +1,9 @@
 package vct.col.ast.statement
 
-import vct.col.ast.{Assert, Assign, Block, Branch, Communicate, CommunicateX, EndpointUse, Eval, Loop, MethodInvocation, SeqAssign, Scope, Statement, ThisSeqProg, VeyMontAssignExpression}
 import vct.col.ast.node.NodeFamilyImpl
+import vct.col.ast._
 import vct.col.check.{CheckContext, CheckError, SeqProgStatement}
 import vct.col.print._
-import vct.col.ref.Ref
 
 trait StatementImpl[G] extends NodeFamilyImpl[G] { this: Statement[G] =>
   def layoutAsBlock(implicit ctx: Ctx): Doc =
@@ -26,7 +25,12 @@ trait StatementImpl[G] extends NodeFamilyImpl[G] { this: Statement[G] =>
         _: Scope[G] |
         _: Block[G] |
         _: Eval[G] |
-        _: Assert[G] => Seq()
+        _: Assert[G] |
+        _: UnresolvedSeqBranch[G] |
+        _: UnresolvedSeqLoop[G] |
+        _: SeqBranch[G] |
+        _: SeqLoop[G]
+        => Seq()
       case _ => Seq(SeqProgStatement(this))
     }
   })

src/col/vct/col/ast/statement/veymont/CommunicateImpl.scala

@@ -1,9 +1,19 @@
 package vct.col.ast.statement.veymont
 
-import vct.col.ast.Communicate
+import vct.col.ast.{Access, Communicate, EndpointName}
+import vct.col.check.{CheckContext, CheckError, SeqProgParticipant}
 import vct.col.print.{Ctx, Doc, Text}
+import vct.col.ref.Ref
 
 trait CommunicateImpl[G] { this: Communicate[G] =>
   override def layout(implicit ctx: Ctx): Doc =
     Text("communicate") <+> receiver.show <+> "<-" <+> sender.show <> ";"
+
+  override def check(context: CheckContext[G]): Seq[CheckError] = this match {
+    case Communicate(Access(name@EndpointName(Ref(receiver)), _), _) if !context.currentParticipatingEndpoints.get.contains(receiver) =>
+      Seq(SeqProgParticipant(name))
+    case Communicate(_, Access(name@EndpointName(Ref(sender)), _)) if !context.currentParticipatingEndpoints.get.contains(sender) =>
+      Seq(SeqProgParticipant(name))
+    case _ => Nil
+  }
 }

src/col/vct/col/ast/statement/veymont/SeqAssignImpl.scala

@@ -2,7 +2,7 @@ package vct.col.ast.statement.veymont
 
 import vct.col.ast.SeqAssign
 import vct.col.ast.statement.StatementImpl
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckError, SeqProgParticipant}
 import vct.col.print.{Ctx, Doc, Group, Text}
 
 trait SeqAssignImpl[G] extends StatementImpl[G] { this: SeqAssign[G] =>
@@ -13,4 +13,8 @@ trait SeqAssignImpl[G] extends StatementImpl[G] { this: SeqAssign[G] =>
   override def layout(implicit ctx: Ctx): Doc =
     Group(Text(ctx.name(receiver)) <> "." <> ctx.name(field) <+> ":=" <+> value.show)
 
+  override def check(context: CheckContext[G]): Seq[CheckError] =
+    if (!context.currentParticipatingEndpoints.get.contains(this.receiver.decl))
+      Seq(SeqProgParticipant(this))
+    else Nil
 }

src/col/vct/col/ast/statement/veymont/SeqBranchImpl.scala

@@ -0,0 +1,48 @@
+package vct.col.ast.statement.veymont
+
+import vct.col.ast.{Access, Communicate, Endpoint, EndpointGuard, EndpointName, SeqAssign, SeqBranch, UnpointedGuard}
+import vct.col.ast.statement.StatementImpl
+import vct.col.check.{CheckContext, CheckError, SeqProgParticipant}
+import vct.col.ref.Ref
+
+import scala.collection.immutable.ListSet
+
+trait SeqBranchImpl[G] extends StatementImpl[G] { this: SeqBranch[G] =>
+  def hasUnpointed: Boolean = guards.exists { case _: UnpointedGuard[G] => true; case _ => false }
+  def explicitParticipants: Seq[Endpoint[G]] = guards.collect { case EndpointGuard(Ref(endpoint), condition) => endpoint }
+
+  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] = {
+    // Assume SeqProg sets participatingEndpoints
+    assert(context.currentParticipatingEndpoints.isDefined)
+
+    if (hasUnpointed) {
+      // Everyone that is participating keeps participating, as well as any endpoints explicitly mentioned
+      context.appendCurrentParticipatingEndpoints(explicitParticipants)
+    } else {
+      // We can refine the set of participants down to the set of endpoints actually present in the guard
+      context.withCurrentParticipatingEndpoints(explicitParticipants)
+    }
+  }
+
+  override def check(context: CheckContext[G]): Seq[CheckError] = super.check(context) ++ {
+    // Assume SeqProg sets participatingEndpoints
+    assert(context.currentParticipatingEndpoints.isDefined)
+
+    // Ensure the set of participants is at most refined
+    if (Set.from(explicitParticipants).subsetOf(context.currentParticipatingEndpoints.get)) {
+      Seq()
+    } else {
+      // There are participants in this if that have been excluded from participation: error
+      Seq(SeqProgParticipant(this))
+    }
+  }
+
+  // All participants that concretely participate in the branch by being named explicitly through the condition,
+  // an assignment, or a communicate.
+  def participants: Set[Endpoint[G]] =
+    ListSet.from(subnodes.collect {
+      case Communicate(Access(EndpointName(Ref(receiver)), _), Access(EndpointName(Ref(sender)), _)) => Seq(receiver, sender)
+      case SeqAssign(Ref(receiver), _, _) => Seq(receiver)
+      case branch: SeqBranch[G] => branch.explicitParticipants
+    }.flatten)
+}

src/col/vct/col/ast/statement/veymont/SeqLoopImpl.scala

@@ -0,0 +1,46 @@
+package vct.col.ast.statement.veymont
+
+import vct.col.ast.statement.StatementImpl
+import vct.col.ast.{Access, Communicate, Endpoint, EndpointGuard, EndpointName, SeqAssign, SeqBranch, SeqLoop, UnpointedGuard}
+import vct.col.check.{CheckContext, CheckError, SeqProgParticipant}
+import vct.col.ref.Ref
+
+import scala.collection.immutable.ListSet
+
+trait SeqLoopImpl[G] extends StatementImpl[G] { this: SeqLoop[G] =>
+  def hasUnpointed: Boolean = guards.exists { case _: UnpointedGuard[G] => true; case _ => false }
+  def explicitParticipants: Seq[Endpoint[G]] = guards.collect { case EndpointGuard(Ref(endpoint), condition) => endpoint }
+
+  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] = {
+    // Assume SeqProg sets participatingEndpoints
+    assert(context.currentParticipatingEndpoints.isDefined)
+
+    if (hasUnpointed) {
+      // Everyone that is participating keeps participating, as well as any endpoints explicitly mentioned
+      context.appendCurrentParticipatingEndpoints(explicitParticipants)
+    } else {
+      // We can refine the set of participants down to the set of endpoints actually present in the guard
+      context.withCurrentParticipatingEndpoints(explicitParticipants)
+    }
+  }
+
+  override def check(context: CheckContext[G]): Seq[CheckError] = super.check(context) ++ {
+    // Assume SeqProg sets participatingEndpoints
+    assert(context.currentParticipatingEndpoints.isDefined)
+
+    // Ensure the set of participants is at most refined
+    if (Set.from(explicitParticipants).subsetOf(context.currentParticipatingEndpoints.get)) {
+      Seq()
+    } else {
+      // There are participants in this if that have been excluded from participation: error
+      Seq(SeqProgParticipant(this))
+    }
+  }
+
+  def participants: Set[Endpoint[G]] =
+    ListSet.from(subnodes.collect {
+      case Communicate(Access(EndpointName(Ref(receiver)), _), Access(EndpointName(Ref(sender)), _)) => Seq(receiver, sender)
+      case SeqAssign(Ref(receiver), _, _) => Seq(receiver)
+      case branch: SeqBranch[G] => branch.explicitParticipants
+    }.flatten)
+}