diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 157037e2cb..3cc6edaf6c 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/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] diff --git a/src/col/vct/col/ast/declaration/global/SeqProgImpl.scala b/src/col/vct/col/ast/declaration/global/SeqProgImpl.scala index ddbf0cb983..d5df0c2728 100644 --- a/src/col/vct/col/ast/declaration/global/SeqProgImpl.scala +++ b/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) } diff --git a/src/col/vct/col/ast/expr/op/bool/VeyMontConditionImpl.scala b/src/col/vct/col/ast/expr/op/bool/VeyMontConditionImpl.scala deleted file mode 100644 index 4821c0b9d2..0000000000 --- a/src/col/vct/col/ast/expr/op/bool/VeyMontConditionImpl.scala +++ /dev/null @@ -1,12 +0,0 @@ -package vct.col.ast.expr.op.bool - -import vct.col.ast.{TBool, Type, VeyMontCondition} -import vct.col.print._ - -trait VeyMontConditionImpl[G] { this: VeyMontCondition[G] => - override def t: Type[G] = TBool() - - override def precedence: Int = Precedence.AND - override def layout(implicit ctx: Ctx): Doc = - Group(Doc.fold(condition.map(_._2).map(assoc))(_ <+> "&&" <+/> _)) -} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLAccessImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLAccessImpl.scala new file mode 100644 index 0000000000..a03c168d4a --- /dev/null +++ b/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 +} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccessImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccessImpl.scala deleted file mode 100644 index 82d9bf5dbe..0000000000 --- a/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateAccessImpl.scala +++ /dev/null @@ -1,7 +0,0 @@ -package vct.col.ast.family.pvlcommunicate - -import vct.col.ast.{PVLCommunicateAccess, Type} - -trait PVLCommunicateAccessImpl[G] { this: PVLCommunicateAccess[G] => - def fieldType: Type[G] = ref.get.decl.t -} diff --git a/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala b/src/col/vct/col/ast/family/pvlcommunicate/PVLSubjectImpl.scala similarity index 55% rename from src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala rename to src/col/vct/col/ast/family/pvlcommunicate/PVLSubjectImpl.scala index 88a12964b7..85785136cf 100644 --- a/src/col/vct/col/ast/family/pvlcommunicate/PVLCommunicateSubjectImpl.scala +++ b/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]] } diff --git a/src/col/vct/col/ast/family/seqguard/EndpointGuardImpl.scala b/src/col/vct/col/ast/family/seqguard/EndpointGuardImpl.scala new file mode 100644 index 0000000000..cb0d4b72eb --- /dev/null +++ b/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) +} diff --git a/src/col/vct/col/ast/family/seqguard/SeqGuardImpl.scala b/src/col/vct/col/ast/family/seqguard/SeqGuardImpl.scala new file mode 100644 index 0000000000..0f7433cac0 --- /dev/null +++ b/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]] +} diff --git a/src/col/vct/col/ast/family/seqguard/UnpointedGuardImpl.scala b/src/col/vct/col/ast/family/seqguard/UnpointedGuardImpl.scala new file mode 100644 index 0000000000..2ce7c839af --- /dev/null +++ b/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 +} diff --git a/src/col/vct/col/ast/statement/StatementImpl.scala b/src/col/vct/col/ast/statement/StatementImpl.scala index 03586a1918..cb616e299c 100644 --- a/src/col/vct/col/ast/statement/StatementImpl.scala +++ b/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)) } }) diff --git a/src/col/vct/col/ast/statement/veymont/CommunicateImpl.scala b/src/col/vct/col/ast/statement/veymont/CommunicateImpl.scala index db1fc99727..fd55e6c63d 100644 --- a/src/col/vct/col/ast/statement/veymont/CommunicateImpl.scala +++ b/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 + } } diff --git a/src/col/vct/col/ast/statement/veymont/SeqAssignImpl.scala b/src/col/vct/col/ast/statement/veymont/SeqAssignImpl.scala index a3916b9c4f..8e91505c80 100644 --- a/src/col/vct/col/ast/statement/veymont/SeqAssignImpl.scala +++ b/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 } diff --git a/src/col/vct/col/ast/statement/veymont/SeqBranchImpl.scala b/src/col/vct/col/ast/statement/veymont/SeqBranchImpl.scala new file mode 100644 index 0000000000..93f26e2f2f --- /dev/null +++ b/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) +} diff --git a/src/col/vct/col/ast/statement/veymont/SeqLoopImpl.scala b/src/col/vct/col/ast/statement/veymont/SeqLoopImpl.scala new file mode 100644 index 0000000000..7c5d27e5be --- /dev/null +++ b/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) +} diff --git a/src/col/vct/col/check/Check.scala b/src/col/vct/col/check/Check.scala index 2fce30e270..20f6e6c7ca 100644 --- a/src/col/vct/col/check/Check.scala +++ b/src/col/vct/col/check/Check.scala @@ -8,6 +8,9 @@ import vct.col.ref.Ref import vct.col.resolve.ResolveReferences import vct.result.{HasContext, Message} +import scala.collection.immutable.ListSet +import scala.collection.mutable + case object Check { def inOrder(check1: => Seq[CheckError], check2: => Seq[CheckError]): Seq[CheckError] = check1 match { @@ -58,12 +61,20 @@ sealed trait CheckError { Seq(context(clause) -> "This catch clause is redundant, because it is subsumed by the caught types of earlier catch clauses in this block.") case ResultOutsidePostcondition(res) => Seq(context(res) -> "\\result may only occur in the postcondition.") - case SeqProgStatement(s) => Seq(context(s) -> "This statement is not allowed in `seq_prog`.") - case SeqProgInstanceMethodArgs(m) => Seq(context(m) -> "An instance method in a `seq_prog` cannot have any arguments.") - case SeqProgInstanceMethodBody(m) => Seq(context(m) -> "An instance method in a `seq_prog` must have a body.") - case SeqProgInstanceMethodNonVoid(m) => Seq(context(m) -> "An instance method in a `seq_prog` must have return type `void`.") - case SeqProgInvocation(s) => Seq(context(s) -> "Only invocations on `this` and endpoints are allowed.") - case SeqProgReceivingEndpoint(e) => Seq(context(e) -> s"Can only refer to the receiving endpoint of this statement") + case SeqProgStatement(s) => + Seq(context(s) -> "This statement is not allowed in `seq_prog`.") + case SeqProgInstanceMethodArgs(m) => + Seq(context(m) -> "An instance method in a `seq_prog` cannot have any arguments.") + case SeqProgInstanceMethodBody(m) => + Seq(context(m) -> "An instance method in a `seq_prog` must have a body.") + case SeqProgInstanceMethodNonVoid(m) => + Seq(context(m) -> "An instance method in a `seq_prog` must have return type `void`.") + case SeqProgInvocation(s) => + Seq(context(s) -> "Only invocations on `this` and endpoints are allowed.") + case SeqProgReceivingEndpoint(e) => + Seq(context(e) -> s"Can only refer to the receiving endpoint of this statement.") + case SeqProgParticipant(s) => + Seq(context(s) -> s"An endpoint is used in this branch which is not allowed to participate at this point in the program because of earlier branches.") }): _*) def subcode: String @@ -126,6 +137,9 @@ case class SeqProgInvocation(s: Statement[_]) extends CheckError { case class SeqProgReceivingEndpoint(e: Expr[_]) extends CheckError { val subcode = "seqProgReceivingEndpoint" } +case class SeqProgParticipant(s: Node[_]) extends CheckError { + val subcode = "seqProgParticipant" +} case object CheckContext { case class ScopeFrame[G](decls: Seq[Declaration[G]], scanLazily: Seq[Node[G]]) { @@ -146,6 +160,7 @@ case class CheckContext[G] inPostCondition: Boolean = false, currentSeqProg: Option[SeqProg[G]] = None, currentReceiverEndpoint: Option[Endpoint[G]] = None, + currentParticipatingEndpoints: Option[Set[Endpoint[G]]] = None, ) { def withScope(decls: Seq[Declaration[G]]): CheckContext[G] = copy(scopes = scopes :+ CheckContext.ScopeFrame(decls, Nil)) @@ -173,6 +188,17 @@ case class CheckContext[G] def withReceiverEndpoint(endpoint: Endpoint[G]): CheckContext[G] = copy(currentReceiverEndpoint = Some(endpoint)) + def withCurrentParticipatingEndpoints(endpoints: Seq[Endpoint[G]]): CheckContext[G] = + // ListSet to preserve insertion order + copy(currentParticipatingEndpoints = Some(ListSet.from(endpoints))) + + def appendCurrentParticipatingEndpoints(newEndpoints: Seq[Endpoint[G]]): CheckContext[G] = + // ListSet to preserve insertion order + currentParticipatingEndpoints match { + case None => withCurrentParticipatingEndpoints(newEndpoints) + case Some(endpoints) => copy(currentParticipatingEndpoints = Some(endpoints.union(ListSet.from(newEndpoints)))) + } + def inScope[Decl <: Declaration[G]](ref: Ref[G, Decl]): Boolean = !undeclared.exists(_.contains(ref.decl)) && scopes.exists(_.contains(ref.decl)) diff --git a/src/col/vct/col/origin/Blame.scala b/src/col/vct/col/origin/Blame.scala index df86d4195d..cb7ec89e09 100644 --- a/src/col/vct/col/origin/Blame.scala +++ b/src/col/vct/col/origin/Blame.scala @@ -232,12 +232,13 @@ case class SYCLItemMethodPreconditionFailed(node: InvokingNode[_]) extends NodeV sealed trait CallableFailure extends ConstructorFailure with JavaConstructorFailure sealed trait ContractedFailure extends CallableFailure -case class PostconditionFailed(path: Seq[AccountedDirection], failure: ContractFailure, node: ContractApplicable[_]) extends ContractedFailure with WithContractFailure { +sealed trait SeqCallableFailure extends CallableFailure +case class PostconditionFailed(path: Seq[AccountedDirection], failure: ContractFailure, node: ContractApplicable[_]) extends ContractedFailure with SeqCallableFailure with WithContractFailure { override def baseCode: String = "postFailed" override def descInContext: String = "Postcondition may not hold, since" override def inlineDescWithSource(node: String, failure: String): String = s"Postcondition of `$node` may not hold, since $failure." } -case class TerminationMeasureFailed(applicable: ContractApplicable[_], apply: Invocation[_], measure: DecreasesClause[_]) extends ContractedFailure with VerificationFailure { +case class TerminationMeasureFailed(applicable: ContractApplicable[_], apply: Invocation[_], measure: DecreasesClause[_]) extends ContractedFailure with SeqCallableFailure with VerificationFailure { override def code: String = "decreasesFailed" override def position: String = measure.o.shortPositionText override def desc: String = Message.messagesInContext( @@ -248,7 +249,7 @@ case class TerminationMeasureFailed(applicable: ContractApplicable[_], apply: In override def inlineDesc: String = s"${apply.o.inlineContextText} may not terminate, since `${measure.o.inlineContextText}` is not decreased or not bounded" } -case class ContextEverywhereFailedInPost(failure: ContractFailure, node: ContractApplicable[_]) extends ContractedFailure with WithContractFailure { +case class ContextEverywhereFailedInPost(failure: ContractFailure, node: ContractApplicable[_]) extends ContractedFailure with SeqCallableFailure with WithContractFailure { override def baseCode: String = "contextPostFailed" override def descInContext: String = "Context may not hold in postcondition, since" override def inlineDescWithSource(node: String, failure: String): String = s"Context of `$node` may not hold in the postcondition, since $failure." @@ -320,6 +321,66 @@ case class PlusProviderInvocationFailed(innerFailure: WithContractFailure) exten override def inlineDescWithSource(node: String, failure: String): String = innerFailure.inlineDescWithSource(node, failure) } +sealed trait FrontendIfFailure extends VerificationFailure +sealed trait SeqBranchFailure extends FrontendIfFailure + +case class BranchUnanimityFailed(guard1: Node[_], guard2: Node[_]) extends SeqBranchFailure { + override def code: String = "branchNotUnanimous" + + override def desc: String = Message.messagesInContext( + (guard1.o, "This condition..."), + (guard2.o, "...should agree with this condition, but this might not be the case") + ) + + override def position: String = guard1.o.shortPositionText + override def inlineDesc: String = "Two conditions in this branch might disagree." +} + +sealed trait FrontEndLoopFailure extends VerificationFailure +sealed trait SeqLoopFailure extends FrontEndLoopFailure + +case class LoopUnanimityNotEstablished(guard1: Node[_], guard2: Node[_]) extends SeqLoopFailure { + override def code: String = "loopUnanimityNotEstablished" + + override def desc: String = Message.messagesInContext( + (guard1.o, "This condition..."), + (guard2.o, "...should agree with this condition, but this could not be established before the loop.") + ) + + override def position: String = guard1.o.shortPositionText + override def inlineDesc: String = "The agreement of two conditions in this branch could not be established before the loop." +} + +case class LoopUnanimityNotMaintained(guard1: Node[_], guard2: Node[_]) extends SeqLoopFailure { + override def code: String = "loopUnanimityNotMaintained" + + override def desc: String = Message.messagesInContext( + (guard1.o, "This condition..."), + (guard2.o, "...should agree with this condition, but this could not be maintained for an arbitrary loop iteration.") + ) + + override def position: String = guard1.o.shortPositionText + override def inlineDesc: String = "The agreement of two conditions in this branch could not be maintained for an arbitrary loop iteration." +} + +sealed trait PVLAccessFailure extends VerificationFailure +sealed trait AccessFailure extends PVLAccessFailure + +case class AccessInsufficientPermission(node: Access[_]) extends AccessFailure with NodeVerificationFailure { + override def code: String = "accessPerm" + override def descInContext: String = "There may be insufficient permission to access this field on this endpoint." + override def inlineDescWithSource(source: String): String = s"There may be insufficient permission to access `$source`." +} + +sealed trait PVLSeqAssignFailure extends VerificationFailure +sealed trait SeqAssignFailure extends PVLSeqAssignFailure + +case class SeqAssignInsufficientPermission(node: SeqAssign[_]) extends SeqAssignFailure with NodeVerificationFailure { + override def code: String = "seqAssignPerm" + override def descInContext: String = "There may be insufficient permission to access this field on this endpoint." + override def inlineDescWithSource(source: String): String = s"There may be insufficient permission to access `$source`." +} + sealed trait DerefInsufficientPermission extends FrontendDerefError case class InsufficientPermission(node: HeapDeref[_]) extends DerefInsufficientPermission with NodeVerificationFailure { override def code: String = "perm" diff --git a/src/col/vct/col/origin/Name.scala b/src/col/vct/col/origin/Name.scala index 2fa015d4a6..52b94cbbcd 100644 --- a/src/col/vct/col/origin/Name.scala +++ b/src/col/vct/col/origin/Name.scala @@ -18,7 +18,7 @@ object Name { case class Preferred(parts: Seq[String]) extends Name { override def snake: String = parts.map(_.toLowerCase).mkString("_") override def usnake: String = parts.map(_.toUpperCase).mkString("_") - override def camel: String = (parts.head.toLowerCase +: parts.map(_.toLowerCase.capitalize)).mkString("") + override def camel: String = (parts.head.toLowerCase +: parts.tail.map(_.toLowerCase.capitalize)).mkString("") override def ucamel: String = camel.capitalize } } \ No newline at end of file diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala index aaa6def338..c27091ec8c 100644 --- a/src/col/vct/col/resolve/Resolve.scala +++ b/src/col/vct/col/resolve/Resolve.scala @@ -408,7 +408,7 @@ case object ResolveReferences extends LazyLogging { case Some(_) => throw ForbiddenEndpointNameType(local) case None => throw NoSuchNameError("endpoint", name, local) } - case access@PVLCommunicateAccess(subject, field) => + case access@PVLAccess(subject, field) => access.ref = Some(PVL.findDerefOfClass(subject.cls, field).getOrElse(throw NoSuchNameError("field", field, access))) case endpoint: PVLEndpoint[G] => endpoint.ref = Some(PVL.findConstructor(TClass(endpoint.cls.decl.ref[Class[G]]), endpoint.args).getOrElse(throw ConstructorNotFound(endpoint))) diff --git a/src/col/vct/col/rewrite/NonLatchingRewriter.scala b/src/col/vct/col/rewrite/NonLatchingRewriter.scala index 6066d3c32f..a5ec0bee03 100644 --- a/src/col/vct/col/rewrite/NonLatchingRewriter.scala +++ b/src/col/vct/col/rewrite/NonLatchingRewriter.scala @@ -66,9 +66,10 @@ 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) + override def dispatch(node: PVLAccess[Pre]): PVLAccess[Post] = rewriteDefault(node) + override def dispatch(node: PVLSubject[Pre]): PVLSubject[Post] = rewriteDefault(node) override def dispatch(node: SeqRun[Pre]): SeqRun[Post] = rewriteDefault(node) override def dispatch(node: Access[Pre]): Access[Post] = rewriteDefault(node) override def dispatch(node: Subject[Pre]): Subject[Post] = rewriteDefault(node) + override def dispatch(node: SeqGuard[Pre]): SeqGuard[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 ebf6eedc25..7a4f4e3fea 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -260,11 +260,12 @@ 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 + case node: PVLAccess[Pre] => node + case node: PVLSubject[Pre] => node case node: SeqRun[Pre] => node case node: Access[Pre] => node case node: Subject[Pre] => node + case node: SeqGuard[Pre] => coerce(node) } def preCoerce(e: Expr[Pre]): Expr[Pre] = e @@ -467,13 +468,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: 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: PVLAccess[Pre]): PVLAccess[Pre] = node + def postCoerce(node: PVLAccess[Pre]): PVLAccess[Post] = rewriteDefault(node) + override final def dispatch(node: PVLAccess[Pre]): PVLAccess[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 preCoerce(node: PVLSubject[Pre]): PVLSubject[Pre] = node + def postCoerce(node: PVLSubject[Pre]): PVLSubject[Post] = rewriteDefault(node) + override final def dispatch(node: PVLSubject[Pre]): PVLSubject[Post] = postCoerce(coerce(preCoerce(node))) def preCoerce(node: Access[Pre]): Access[Pre] = node def postCoerce(node: Access[Pre]): Access[Post] = rewriteDefault(node) @@ -487,6 +488,10 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr def postCoerce(node: SeqRun[Pre]): SeqRun[Post] = rewriteDefault(node) override final def dispatch(node: SeqRun[Pre]): SeqRun[Post] = postCoerce(coerce(preCoerce(node))) + def preCoerce(node: SeqGuard[Pre]): SeqGuard[Pre] = node + def postCoerce(node: SeqGuard[Pre]): SeqGuard[Post] = rewriteDefault(node) + override final def dispatch(node: SeqGuard[Pre]): SeqGuard[Post] = postCoerce(coerce(preCoerce(node))) + def coerce(value: Expr[Pre], target: Type[Pre], canCDemote: Boolean = false): Expr[Pre] = ApplyCoercion(value, CoercionUtils.getAnyCoercion(value.t, target) match { case Some(coercion) if canCDemote || coercion.isCPromoting => coercion @@ -1648,7 +1653,6 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr case Z3SeqSuffixOf(post, seq) => Z3SeqSuffixOf(z3seq(post)._1, z3seq(seq)._1) case Z3SeqUnit(arg) => Z3SeqUnit(arg) case Z3TransitiveClosure(ref, args) => Z3TransitiveClosure(ref, coerceArgs(args, ref.ref.decl)) - case VeyMontCondition(c) => VeyMontCondition(c) case localIncoming: BipLocalIncomingData[Pre] => localIncoming case glue: JavaBipGlue[Pre] => glue case LlvmLocal(name) => e @@ -1729,22 +1733,28 @@ 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 PVLCommunicate(s, r) if r.fieldType == s.fieldType => PVLCommunicate(s, r) + case c @ PVLCommunicate(s, r) if r.fieldType == s.fieldType => PVLCommunicate(s, r) case comm@PVLCommunicate(s, r) => throw IncoercibleExplanation(comm, s"The receiver should have type ${s.fieldType}, but actually has type ${r.fieldType}.") - case 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) 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 PVLSeqAssign(r, f, v) => - try { PVLSeqAssign(r, f, coerce(v, f.decl.t)) } catch { + case a @ PVLSeqAssign(r, f, v) => + try { PVLSeqAssign(r, f, coerce(v, f.decl.t))(a.blame) } catch { case err: Incoercible => println(err.text) throw err } - case SeqAssign(r, f, v) => - try { SeqAssign(r, f, coerce(v, f.decl.t)) } catch { + case a @ SeqAssign(r, f, v) => + try { SeqAssign(r, f, coerce(v, f.decl.t))(a.blame) } catch { case err: Incoercible => println(err.text) throw err } + case s: SeqBranch[Pre] => s + case s: SeqLoop[Pre] => s + case branch@UnresolvedSeqBranch(branches) => UnresolvedSeqBranch(branches.map { case (cond, effect) => (bool(cond), effect) })(branch.blame) + case branch@PVLBranch(branches) => PVLBranch(branches.map { case (cond, effect) => (bool(cond), effect) })(branch.blame) + case loop@UnresolvedSeqLoop(cond, contract, body) => UnresolvedSeqLoop(bool(cond), contract, body)(loop.blame) + case loop@PVLLoop(init, cond, update, contract, body) => PVLLoop(init, bool(cond), update, contract, body)(loop.blame) } } @@ -2238,9 +2248,14 @@ 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 + def coerce(node: PVLAccess[Pre]): PVLAccess[Pre] = node + def coerce(node: PVLSubject[Pre]): PVLSubject[Pre] = node def coerce(node: SeqRun[Pre]): SeqRun[Pre] = node def coerce(node: Access[Pre]): Access[Pre] = node def coerce(node: Subject[Pre]): Subject[Pre] = node + def coerce(node: SeqGuard[Pre]): SeqGuard[Pre] = node match { + case EndpointGuard(endpoint, cond) => EndpointGuard(endpoint, bool(cond))(node.o) + case UnpointedGuard(cond) => UnpointedGuard(bool(cond))(node.o) + } + } diff --git a/src/col/vct/col/util/AstBuildHelpers.scala b/src/col/vct/col/util/AstBuildHelpers.scala index 56eab0bdcf..c32d106d6b 100644 --- a/src/col/vct/col/util/AstBuildHelpers.scala +++ b/src/col/vct/col/util/AstBuildHelpers.scala @@ -485,4 +485,7 @@ object AstBuildHelpers { def foldOr[G](exprs: Seq[Expr[G]])(implicit o: Origin): Expr[G] = exprs.reduceOption(Or(_, _)).getOrElse(ff) + + def foldAnd[G](exprs: Seq[Expr[G]])(implicit o: Origin): Expr[G] = + exprs.reduceOption(And(_, _)).getOrElse(tt) } diff --git a/src/main/vct/main/stages/Resolution.scala b/src/main/vct/main/stages/Resolution.scala index f67e36b64a..5422931a69 100644 --- a/src/main/vct/main/stages/Resolution.scala +++ b/src/main/vct/main/stages/Resolution.scala @@ -36,6 +36,7 @@ case object Resolution { case ClassPathEntry.SourcePackageRoot => ResolveTypes.JavaClassPathEntry.SourcePackageRoot case ClassPathEntry.SourcePath(root) => ResolveTypes.JavaClassPathEntry.Path(root) }, + options.veymontGeneratePermissions ) } @@ -98,6 +99,7 @@ case class Resolution[G <: Generation] ResolveTypes.JavaClassPathEntry.Path(Resources.getJrePath), ResolveTypes.JavaClassPathEntry.SourcePackageRoot ), + veymontGeneratePermissions: Boolean = false, ) extends Stage[ParseResult[G], Verification[_ <: Generation]] with LazyLogging { override def friendlyName: String = "Name Resolution" @@ -115,7 +117,7 @@ case class Resolution[G <: Generation] case Nil => // ok case some => throw InputResolutionError(some) } - val resolvedProgram = LangSpecificToCol().dispatch(typedProgram) + val resolvedProgram = LangSpecificToCol(veymontGeneratePermissions).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 diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index 74bbf9c608..c95973ca3a 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -14,7 +14,7 @@ import vct.col.rewrite.adt._ import vct.col.rewrite.bip._ import vct.col.rewrite.exc._ import vct.rewrite.lang.NoSupportSelfLoop -import vct.col.rewrite.veymont.{AddVeyMontAssignmentNodes, AddVeyMontConditionNodes, StructureCheck} +import vct.col.rewrite.veymont.StructureCheck import vct.importer.{PathAdtImporter, Util} import vct.main.Main.TemporarilyUnsupported import vct.main.stages.Transformation.TransformationCheckError @@ -24,7 +24,7 @@ import vct.resources.Resources import vct.result.VerificationError.SystemError import vct.rewrite.{EncodeResourceValues, ExplicitResourceValues, HeapVariableToRef, SmtlibToProverTypes} import vct.rewrite.lang.ReplaceSYCLTypes -import vct.rewrite.veymont.{EncodeSeqProg, GenerateSeqProgPermissions} +import vct.rewrite.veymont.{DeduplicateSeqGuards, EncodeSeqBranchUnanimity, EncodeSeqProg, GenerateSeqProgPermissions, EncodeUnpointedGuard, SplitSeqGuards} object Transformation { case class TransformationCheckError(pass: RewriterBuilder, errors: Seq[(Program[_], CheckError)]) extends SystemError { @@ -67,6 +67,7 @@ object Transformation { inferHeapContextIntoFrame = options.inferHeapContextIntoFrame, bipResults = bipResults, splitVerificationByProcedure = options.devSplitVerificationByProcedure, + veymontGeneratePermissions = options.veymontGeneratePermissions, ) } @@ -172,6 +173,7 @@ case class SilverTransformation bipResults: BIP.VerificationResults, checkSat: Boolean = true, splitVerificationByProcedure: Boolean = false, + veymontGeneratePermissions: Boolean = false, ) extends Transformation(onBeforePassKey, onAfterPassKey, Seq( // Replace leftover SYCL types ReplaceSYCLTypes, @@ -195,7 +197,11 @@ case class SilverTransformation EncodeRangedFor, // VeyMont sequential program encoding - GenerateSeqProgPermissions, + SplitSeqGuards, + EncodeUnpointedGuard, + DeduplicateSeqGuards, + GenerateSeqProgPermissions.withArg(veymontGeneratePermissions), + EncodeSeqBranchUnanimity, EncodeSeqProg, EncodeString, // Encode spec string as seq @@ -310,8 +316,8 @@ case class SilverTransformation case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil, override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil) extends Transformation(onBeforePassKey, onAfterPassKey, Seq( - AddVeyMontAssignmentNodes, - AddVeyMontConditionNodes, + // AddVeyMontAssignmentNodes, +// AddVeyMontConditionNodes, StructureCheck, )) diff --git a/src/main/vct/options/Options.scala b/src/main/vct/options/Options.scala index 412f696814..9a6112db75 100644 --- a/src/main/vct/options/Options.scala +++ b/src/main/vct/options/Options.scala @@ -240,6 +240,10 @@ case object Options { .action((path, c) => c.copy(cPreprocessorPath = path)) .text("Set the location of the C preprocessor binary"), + opt[Unit]("veymont-generate-permissions") + .action((_, c) => c.copy(veymontGeneratePermissions = true)) + .text("Generate permissions for the entire sequential program in the style of VeyMont 1.4"), + note(""), note("VeyMont Mode"), opt[Unit]("veymont") @@ -389,6 +393,7 @@ case class Options // VeyMont options veymontOutput: Path = null, // required veymontChannel: PathOrStd = PathOrStd.Path(getVeymontChannel), + veymontGeneratePermissions: Boolean = false, // VeSUV options vesuvOutput: Path = null, diff --git a/src/parsers/antlr4/LangPVLParser.g4 b/src/parsers/antlr4/LangPVLParser.g4 index 2b3b84ddce..d061e89d8f 100644 --- a/src/parsers/antlr4/LangPVLParser.g4 +++ b/src/parsers/antlr4/LangPVLParser.g4 @@ -188,7 +188,7 @@ statement | 'label' identifier ';' # pvlLabel | allowedForStatement ';' # pvlForStatement | 'communicate' access direction access ';' # pvlCommunicateStatement - | identifier '.' identifier ':' '=' expr ';' # pvlParAssign + | identifier '.' identifier ':' '=' expr ';' # pvlSeqAssign ; direction diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala index 3878ce760e..58f168e365 100644 --- a/src/parsers/vct/parsers/transform/PVLToCol.scala +++ b/src/parsers/vct/parsers/transform/PVLToCol.scala @@ -30,7 +30,7 @@ case class PVLToCol[G](override val baseOrigin: Origin, case ProgramDecl1(cls) => Seq(convert(cls)) case ProgramDecl2(enum) => Seq(convert(enum)) case ProgramDecl3(method) => Seq(convertProcedure(method)) - case ProgramDecl4(seqProg) => Seq(convertVeyMontProg(seqProg)) + case ProgramDecl4(seqProg) => Seq(convertSeqProg(seqProg)) } def convert(implicit enum: EnumDeclContext): Enum[G] = enum match { @@ -50,7 +50,7 @@ case class PVLToCol[G](override val baseOrigin: Origin, PVLSeqRun( convert(body), contract.consumeApplicableContract(blame(decl)) - )(blame(decl))) + )(blame(decl))(origin(decl).where(name = "run"))) case PvlEndpoint(_, name, _, ClassType0(endpointType, None), _, args, _, _) => new PVLEndpoint( convert(name), @@ -60,15 +60,15 @@ case class PVLToCol[G](override val baseOrigin: Origin, case PvlEndpoint(_, name, _, t@ClassType0(_, Some(_)), _, args, _, _) => ??(t) } - def convertVeyMontProg(implicit cls: DeclVeyMontSeqProgContext): PVLSeqProg[G] = cls match { + def convertSeqProg(implicit decl: DeclVeyMontSeqProgContext): PVLSeqProg[G] = decl match { case DeclVeyMontSeqProg0(contract, _, name, _, args, _, _, decls, _) => withContract(contract, contract => { new PVLSeqProg( convert(name), decls.map(convert(_)), - contract.consumeApplicableContract(blame(cls)), + contract.consumeApplicableContract(blame(decl)), args.map(convert(_)).getOrElse(Seq()) - )(origin(cls).sourceName(convert(name))) + )(blame(decl))(origin(decl).sourceName(convert(name))) }) } @@ -301,7 +301,7 @@ case class PVLToCol[G](override val baseOrigin: Origin, case PvlJoin(_, obj, _) => Join(convert(obj))(blame(stat)) case PvlValStatement(inner) => convert(inner) case PvlIf(_, _, cond, _, body, None) => - Branch(Seq((convert(cond), convert(body)))) + PVLBranch(Seq((convert(cond), convert(body))))(blame(stat)) case PvlIf(_, _, cond, _, body, Some(ElseBlock0(_, otherwise))) => Branch(Seq( (convert(cond), convert(body)), @@ -335,7 +335,7 @@ case class PVLToCol[G](override val baseOrigin: Origin, ParAtomic(convert(invs).map(new UnresolvedRef[G, ParInvariantDecl[G]](_)), convert(body))(blame(stat)) case PvlWhile(contract, _, _, cond, _, body) => withContract(contract, contract => - Scope(Nil, Loop(Block(Nil), convert(cond), Block(Nil), contract.consumeLoopContract(stat), convert(body))) + Scope(Nil, PVLLoop(Block(Nil), convert(cond), Block(Nil), contract.consumeLoopContract(stat), convert(body))(blame(stat))) ) case PvlFor(contract, _, _, init, _, cond, _, update, _, body) => withContract(contract, contract => @@ -360,11 +360,11 @@ case class PVLToCol[G](override val baseOrigin: Origin, PVLCommunicate(convert(sender), convert(receiver)) case PvlCommunicateStatement(_, sender, Direction1("->"), receiver, _) => PVLCommunicate(convert(sender), convert(receiver)) - case PvlParAssign(endpoint, _, field, _, _, expr, _) => + case PvlSeqAssign(endpoint, _, field, _, _, expr, _) => PVLSeqAssign( new UnresolvedRef[G, PVLEndpoint[G]](convert(endpoint)), new UnresolvedRef[G, InstanceField[G]](convert(field)), - convert(expr)) + convert(expr))(blame(stat)) } def convert(implicit stat: ForStatementListContext): Statement[G] = @@ -388,11 +388,11 @@ 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 acc: AccessContext): PVLAccess[G] = acc match { + case Access0(subject, _, field) => PVLAccess(convert(subject), convert(field))(blame(acc)) } - def convert(implicit subject: SubjectContext): PVLCommunicateSubject[G] = subject match { + def convert(implicit subject: SubjectContext): PVLSubject[G] = subject match { case Subject0(name) => PVLEndpointName(convert(name))(origin(subject).sourceName(convert(name))) case Subject1(family, _, expr, _) => ??(subject) case Subject2(family, _, binder, _, start, _, end, _) => ??(subject) diff --git a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala index 88bd15ed9c..5519b00dde 100644 --- a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala +++ b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala @@ -344,6 +344,12 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() extends Rewriter[Pr case comm: CommunicateX[Pre] => rewriteDefault(comm) case comm: PVLCommunicate[Pre] => rewriteDefault(comm) case comm: Communicate[Pre] => rewriteDefault(comm) + case _: PVLBranch[Pre] => throw ExtraNode + case _: PVLLoop[Pre] => throw ExtraNode + case _: UnresolvedSeqBranch[Pre] => throw ExtraNode + case _: UnresolvedSeqLoop[Pre] => throw ExtraNode + case _: SeqBranch[Pre] => throw ExtraNode + case _: SeqLoop[Pre] => throw ExtraNode case _: CStatement[Pre] => throw ExtraNode case _: CPPStatement[Pre] => throw ExtraNode case _: JavaStatement[Pre] => throw ExtraNode diff --git a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala index 2e367c40c3..491640aa78 100644 --- a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala @@ -20,7 +20,7 @@ case object LangPVLToCol { } } -case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging { +case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre], veymontGeneratePermissions: Boolean) extends LazyLogging { type Post = Rewritten[Pre] implicit val implicitRewriter: AbstractRewriter[Pre, Post] = rw @@ -78,7 +78,7 @@ case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L ApplicableContract( UnitAccountedPredicate(tt), UnitAccountedPredicate(AstBuildHelpers.foldStar(cls.declarations.collect { - case field: InstanceField[Pre] if field.flags.collectFirst { case _: Final[Pre] => () }.isEmpty => + case field: InstanceField[Pre] if field.flags.collectFirst { case _: Final[Pre] => () }.isEmpty && !veymontGeneratePermissions => fieldPerm[Post](result, rw.succ(field), WritePerm()) }) &* (if (checkRunnable) IdleToken(result) else tt)), tt, Nil, Nil, Nil, None, )(TrueSatisfiable) @@ -131,4 +131,18 @@ 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 branch(branch: PVLBranch[Pre]): Statement[Post] = + if (rw.veymont.currentProg.nonEmpty) { + rw.veymont.rewriteBranch(branch) + } else { + Branch(branch.branches.map { case (e, s) => (rw.dispatch(e), rw.dispatch(s)) })(branch.o) + } + + def loop(loop: PVLLoop[Pre]): Statement[Post] = loop match { + case PVLLoop(Block(Nil), _, Block(Nil), _, _) if rw.veymont.currentProg.nonEmpty => + rw.veymont.rewriteLoop(loop) + 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) + } } diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index cef5e9e108..04ad2dcfd0 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/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} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, RewriterBuilderArg} import vct.result.VerificationError.UserError import vct.rewrite.lang.LangVeyMontToCol -case object LangSpecificToCol extends RewriterBuilder { +case object LangSpecificToCol extends RewriterBuilderArg[Boolean] { override def key: String = "langSpecific" override def desc: String = "Translate language-specific constructs to a common subset of nodes." @@ -31,12 +31,12 @@ case object LangSpecificToCol extends RewriterBuilder { } } -case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with LazyLogging { +case class LangSpecificToCol[Pre <: Generation](veymontGeneratePermissions: 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) + val pvl: LangPVLToCol[Pre] = LangPVLToCol(this, veymontGeneratePermissions) val veymont: LangVeyMontToCol[Pre] = LangVeyMontToCol(this) val silver: LangSilverToCol[Pre] = LangSilverToCol(this) val llvm: LangLLVMToCol[Pre] = LangLLVMToCol(this) @@ -158,6 +158,9 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz scanScope(body) }._1) + case branch: PVLBranch[Pre] => pvl.branch(branch) + case loop: PVLLoop[Pre] => pvl.loop(loop) + case JavaLocalDeclarationStatement(locals: JavaLocalDeclaration[Pre]) => java.initLocal(locals) case CDeclarationStatement(decl) => c.rewriteLocal(decl) @@ -169,7 +172,7 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz case eval@Eval(CPPInvocation(_, _, _, _)) => cpp.invocationStatement(eval) case communicate: PVLCommunicate[Pre] => veymont.rewriteCommunicate(communicate) - case assign: PVLSeqAssign[Pre] => veymont.rewriteParAssign(assign) + case assign: PVLSeqAssign[Pre] => veymont.rewriteSeqAssign(assign) case other => rewriteDefault(other) } diff --git a/src/rewrite/vct/rewrite/lang/LangVeyMontToCol.scala b/src/rewrite/vct/rewrite/lang/LangVeyMontToCol.scala index 979fddd57d..1953345b51 100644 --- a/src/rewrite/vct/rewrite/lang/LangVeyMontToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangVeyMontToCol.scala @@ -1,17 +1,14 @@ package vct.rewrite.lang import com.typesafe.scalalogging.LazyLogging +import hre.util.ScopedStack import vct.col.ast._ -import vct.col.ast.RewriteHelpers._ -import vct.col.origin.{DiagnosticOrigin, Origin} -import vct.col.ref.Ref +import vct.col.origin.Origin import vct.col.resolve.ctx.RefPVLEndpoint import vct.col.rewrite.{Generation, Rewritten} -import vct.rewrite.lang.LangSpecificToCol import vct.col.util.SuccessionMap import vct.result.VerificationError.UserError -import vct.rewrite.lang.LangVeyMontToCol.{EndpointUseNotSupported, NoRunMethod} -import vct.rewrite.veymont.EncodeSeqProg.CommunicateNotSupported +import vct.rewrite.lang.LangVeyMontToCol.NoRunMethod case object LangVeyMontToCol { case object EndpointUseNotSupported extends UserError { @@ -34,13 +31,15 @@ case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) exten val seqProgSucc: SuccessionMap[PVLSeqProg[Pre], SeqProg[Post]] = SuccessionMap() val endpointSucc: SuccessionMap[PVLEndpoint[Pre], Endpoint[Post]] = SuccessionMap() + val currentProg: ScopedStack[PVLSeqProg[Pre]] = ScopedStack() + def rewriteCommunicate(comm: PVLCommunicate[Pre]): Communicate[Post] = Communicate(rewriteAccess(comm.receiver), rewriteAccess(comm.sender))(comm.o) - def rewriteAccess(access: PVLCommunicateAccess[Pre]): Access[Post] = - Access[Post](rewriteSubject(access.subject), rw.succ(access.ref.get.decl))(access.o) + def rewriteAccess(access: PVLAccess[Pre]): Access[Post] = + Access[Post](rewriteSubject(access.subject), rw.succ(access.ref.get.decl))(access.blame)(access.o) - def rewriteSubject(subject: PVLCommunicateSubject[Pre]): Subject[Post] = subject match { + def rewriteSubject(subject: PVLSubject[Pre]): Subject[Post] = subject match { case subject@PVLEndpointName(name) => EndpointName[Post](endpointSucc.ref(subject.ref.get.decl))(subject.o) case PVLIndexedFamilyName(family, index) => ??? case PVLFamilyRange(family, binder, start, end) => ??? @@ -56,28 +55,30 @@ case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) exten def rewriteSeqProg(prog: PVLSeqProg[Pre]): Unit = { implicit val o: Origin = prog.o rw.currentThis.having(ThisSeqProg[Post](seqProgSucc.ref(prog))) { - seqProgSucc(prog) = rw.globalDeclarations.declare( - new SeqProg( - rw.dispatch(prog.contract), - rw.variables.collect(prog.args.map(rw.dispatch(_)))._1, - rw.endpoints.collect( - prog.declarations.foreach { - case endpoint: PVLEndpoint[Pre] => rewriteEndpoint(endpoint) - case _ => - }, - )._1, - prog.declarations.collectFirst { - case run: PVLSeqRun[Pre] => rewriteRun(run) - }.getOrElse(throw NoRunMethod(prog)), - rw.classDeclarations.collect( - prog.declarations.foreach { - case _: PVLSeqRun[Pre] => - case _: PVLEndpoint[Pre] => - case decl => rw.dispatch(decl) - } - )._1 - )(prog.o) - ) + currentProg.having(prog) { + seqProgSucc(prog) = rw.globalDeclarations.declare( + new SeqProg( + rw.dispatch(prog.contract), + rw.variables.collect(prog.args.map(rw.dispatch(_)))._1, + rw.endpoints.collect( + prog.declarations.foreach { + case endpoint: PVLEndpoint[Pre] => rewriteEndpoint(endpoint) + case _ => + }, + )._1, + prog.declarations.collectFirst { + case run: PVLSeqRun[Pre] => rewriteRun(run) + }.getOrElse(throw NoRunMethod(prog)), + rw.classDeclarations.collect( + prog.declarations.foreach { + case _: PVLSeqRun[Pre] => + case _: PVLEndpoint[Pre] => + case decl => rw.dispatch(decl) + } + )._1 + )(prog.blame)(prog.o) + ) + } } } @@ -89,6 +90,13 @@ case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) exten SeqRun(rw.dispatch(run.body), rw.dispatch(run.contract))(run.blame)(run.o) } - def rewriteParAssign(assign: PVLSeqAssign[Pre]): SeqAssign[Post] = - SeqAssign[Post](endpointSucc.ref(assign.receiver.decl), rw.succ(assign.field.decl), rw.dispatch(assign.value))(assign.o) + 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 rewriteBranch(branch: PVLBranch[Pre]): UnresolvedSeqBranch[Post] = + UnresolvedSeqBranch(branch.branches.map { case (e, s) => (rw.dispatch(e), rw.dispatch(s)) })(branch.blame)(branch.o) + + def rewriteLoop(loop: PVLLoop[Pre]): UnresolvedSeqLoop[Post] = + UnresolvedSeqLoop(rw.dispatch(loop.cond), rw.dispatch(loop.contract), rw.dispatch(loop.body))(loop.blame)(loop.o) + } diff --git a/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala b/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala deleted file mode 100644 index ad206cbe2e..0000000000 --- a/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala +++ /dev/null @@ -1,111 +0,0 @@ -package vct.col.rewrite.veymont - -import hre.util.ScopedStack -import vct.col.ast.{Assign, Declaration, Deref, EndpointUse, Expr, MethodInvocation, Node, ProcedureInvocation, RunMethod, Statement, VeyMontAssignExpression, CommunicateX, SeqProg, Endpoint} -import vct.col.ref.Ref -import vct.col.rewrite.veymont.AddVeyMontAssignmentNodes.{AddVeyMontAssignmentError, getDerefsFromExpr, getThreadDeref} -import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} -import vct.result.VerificationError.UserError - -object AddVeyMontAssignmentNodes extends RewriterBuilder { - - override def key: String = "addVeyMontAssignmentNodes" - - override def desc: String = "Add nodes for VeyMont assignments" - - case class AddVeyMontAssignmentError(node : Node[_], msg: String) extends UserError { - override def code: String = "addVeyMontAssignmentError" - - override def text: String = node.o.messageInContext(msg) - } - - /** - * Utility function to extract all derefs from an expression - * @param exp - * @tparam Pre - * @return - */ - def getDerefsFromExpr[Pre](exp : Expr[Pre]): Seq[Deref[Pre]] = { - exp.collect { case d@Deref(_, _) => d }.distinct - } - - /** - * Utility function to get Endpoint from a Deref, and throw error err in case of other dereferences - * @param deref to be matched - * @param err to be thrown if match unsuccessful - * @tparam Pre type of expression - * @return list of threads that are dereferenced in the expression - */ - def getThreadDeref[Pre](deref: Deref[Pre], err: UserError) : Endpoint[Pre] = deref.obj match { - case EndpointUse(threadref) => threadref.decl - case _ => throw err - } - -} -case class AddVeyMontAssignmentNodes[Pre <: Generation]() extends Rewriter[Pre] { - - val inSeqProg: ScopedStack[Unit] = ScopedStack() - - override def dispatch(decl: Declaration[Pre]): Unit = - decl match { - case dcl: SeqProg[Pre] => inSeqProg.having(()) { - rewriteDefault(dcl) - } - case _ => rewriteDefault(decl) - } - - override def dispatch(st: Statement[Pre]): Statement[Post] = st match { - case a@Assign(target, value) => - if(inSeqProg.nonEmpty) { - val receiver = getAssignmentReceiver(target) - checkAssignmentMethodCalls(value) - createVeyMontAssignNode(receiver,a) - } else rewriteDefault(st) - case _ => rewriteDefault(st) - } - - def getAssignmentReceiver(target: Expr[Pre]): Endpoint[Pre] = target match { - case Deref(obj, _) => obj match { - case EndpointUse(ref) => ref.decl //target is correct ref to thread - case _ => throw AddVeyMontAssignmentError(target, "The target of this assignment must refer to a thread") - } - case _ => throw AddVeyMontAssignmentError(target, "The target of this assignment must be a dereference to a thread, e.g. someThread.someField") - } - - /** - * - * @param value is the expression to be checked on occurring method calls. - * @return Whether all method calls of the assignment are method calls on thread objects - */ - private def checkAssignmentMethodCalls(value: Expr[Pre]): Boolean = { - !value.exists { - case m: ProcedureInvocation[Pre] => throw AddVeyMontAssignmentError(m, "Cannot call non-thread method in assignment!") - case m: MethodInvocation[Pre] => m.obj match { - case t: EndpointUse[Pre] => false - case m => throw AddVeyMontAssignmentError(m, "Cannot call non-thread method in assignment!") - } - } - } - - def createVeyMontAssignNode(receiver: Endpoint[Pre], a: Assign[Pre]): Statement[Post] = { - val derefs = getDerefsFromExpr(a.value) - if (derefs.isEmpty) - new VeyMontAssignExpression[Post](succ(receiver), rewriteDefault(a))(a.o) - else if (derefs.size == 1) { - val thread = derefs.head.obj match { - case t: EndpointUse[Pre] => t - case _ => throw AddVeyMontAssignmentError(a.value, "The value of this assignment is expected to be a Deref of a thread!") - } - if(thread.ref.decl == receiver) - new VeyMontAssignExpression[Post](succ(receiver),rewriteDefault(a))(a.o) - else { - val sender = getAssignmentSender(derefs.head) - new CommunicateX[Post](succ(receiver), succ(sender), dispatch(derefs.head.ref.decl.t), rewriteDefault(a))(a.o) - } - } else throw AddVeyMontAssignmentError(a.value, "The value of this assignment is not allowed to refer to multiple threads!") - } - - def getAssignmentSender(deref : Deref[Pre]): Endpoint[Pre] = - getThreadDeref(deref,AddVeyMontAssignmentError (deref, "Object identifiers in the value of this assignment can only refer to a thread!") ) - -} diff --git a/src/rewrite/vct/rewrite/veymont/AddVeyMontConditionNodes.scala b/src/rewrite/vct/rewrite/veymont/AddVeyMontConditionNodes.scala deleted file mode 100644 index c11e027044..0000000000 --- a/src/rewrite/vct/rewrite/veymont/AddVeyMontConditionNodes.scala +++ /dev/null @@ -1,108 +0,0 @@ -package vct.col.rewrite.veymont - - -import hre.util.ScopedStack -import vct.col.ast.{And, Block, BooleanValue, Branch, Declaration, Expr, Loop, Node, Statement, VeyMontCondition, SeqProg, Endpoint} -import vct.col.ref.Ref -import vct.col.rewrite.veymont.AddVeyMontAssignmentNodes.{getDerefsFromExpr, getThreadDeref} -import vct.col.rewrite.veymont.AddVeyMontConditionNodes.AddVeyMontConditionError -import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} -import vct.result.VerificationError.UserError - -import scala.reflect.internal.util.TriState.True - -object AddVeyMontConditionNodes extends RewriterBuilder { - override def key: String = "addVeyMontConditionNodes" - - override def desc: String = "Add nodes for VeyMont conditions" - - case class AddVeyMontConditionError(node : Node[_], msg: String) extends UserError { - override def code: String = "addVeyMontConditionError" - - override def text: String = node.o.messageInContext(msg) - } -} - -case class AddVeyMontConditionNodes[Pre <: Generation]() extends Rewriter[Pre] { - - val inSeqProg: ScopedStack[Int] = ScopedStack() - - override def dispatch(decl: Declaration[Pre]): Unit = - decl match { - case dcl: SeqProg[Pre] => - inSeqProg.push(dcl.endpoints.size) - try { - rewriteDefault(dcl) - } finally { - inSeqProg.pop() - } - case _ => rewriteDefault(decl) - } - - override def dispatch(st: Statement[Pre]): Statement[Post] = { - if(inSeqProg.nonEmpty) { - st match { - case Branch(branches) => { - val postbranches = branches.map{case (c,s) => rewriteBranch(c,s)} - Branch(postbranches)(st.o) - } - case l: Loop[Pre] => - rewriteLoop(l) - case _ => rewriteDefault(st) - } - } else rewriteDefault(st) - } - - private def rewriteBranch(cond: Expr[Pre], st: Statement[Pre]) : (Expr[Post],Statement[Post]) = { - val condMap = checkConditionAndGetConditionMap(cond) - if(condMap.isEmpty) //in case of else statement - (dispatch(cond),dispatch(st)) - else (VeyMontCondition[Post](condMap.toList)(st.o), dispatch(st)) - } - - private def rewriteLoop(l: Loop[Pre]): Loop[Post] = { - val condMap = checkConditionAndGetConditionMap(l.cond) - if (condMap.isEmpty) - throw AddVeyMontConditionError(l.cond, "Conditions of loops cannot be `true'!") - else Loop(rewriteDefault(l.init), - VeyMontCondition[Post](condMap.toList)(l.cond.o), - rewriteDefault(l.update), - rewriteDefault(l.contract), - dispatch(l.body))(l.o) - } - - private def checkConditionAndGetConditionMap(e: Expr[Pre]): Map[Ref[Post, Endpoint[Post]], Expr[Post]] = { - if (isTrue(e)) - Map.empty - else { - val condEls = collectConditionElements(e) - val m = getConditionMap(condEls,e) - if(m.keys.toSet.size == inSeqProg.top) { - m - } else throw AddVeyMontConditionError(e, "Conditions of if/while need to reference each thread exactly once!") - } - } - - private def getConditionMap(condEls: List[Expr[Pre]], e : Expr[Pre]): Map[Ref[Post, Endpoint[Post]], Expr[Post]] = { - val derefs = condEls.map(el => (getDerefsFromExpr(el), el)) - derefs.foldRight(Map.empty[Ref[Post, Endpoint[Post]], Expr[Post]]) { case ((d, el), m) => - if (d.size != 1) - throw AddVeyMontConditionError(e, "Conditions of if/while need to reference each thread exactly once!") - else { - val thread = getThreadDeref(d.head, AddVeyMontConditionError(e, "Conditions of if/while can only reference threads, so nothing else!")) - m + (succ(thread) -> dispatch(el)) - } - } - } - - private def isTrue(e : Expr[Pre]) = e match { - case BooleanValue(value) => value - case _ => false - } - - private def collectConditionElements(e: Expr[Pre]) : List[Expr[Pre]] = e match { - case And(left,right) => collectConditionElements(left) ++ collectConditionElements(right) - case _ => List(e) - } - -} diff --git a/src/rewrite/vct/rewrite/veymont/DeduplicateSeqGuards.scala b/src/rewrite/vct/rewrite/veymont/DeduplicateSeqGuards.scala new file mode 100644 index 0000000000..53dc628d73 --- /dev/null +++ b/src/rewrite/vct/rewrite/veymont/DeduplicateSeqGuards.scala @@ -0,0 +1,48 @@ +package vct.rewrite.veymont + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.{DiagnosticOrigin, Origin} +import vct.col.ref.Ref +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.util.AstBuildHelpers._ +import vct.result.VerificationError.UserError +import vct.rewrite.veymont.SplitSeqGuards.MultipleEndpoints + +import scala.collection.mutable + +object DeduplicateSeqGuards extends RewriterBuilder { + override def key: String = "deduplicateSeqGuards" + override def desc: String = "Deduplicates SeqGuard nodes with syntactically identical endpoints" +} + +case class DeduplicateSeqGuards[Pre <: Generation]() extends Rewriter[Pre] { + override def dispatch(statement: Statement[Pre]): Statement[Post] = statement match { + case branch: SeqBranch[Pre] => + val guards: Seq[EndpointGuard[Pre]] = branch.guards.map { + case guard: EndpointGuard[Pre] => guard + case guard: UnpointedGuard[Pre] => ??? // Excluded by RemoveUnpointedGuard + } + branch.rewrite(guards = dedup(guards)) + + case loop: SeqLoop[Pre] => + val guards: Seq[EndpointGuard[Pre]] = loop.guards.map { + case guard: EndpointGuard[Pre] => guard + case guard: UnpointedGuard[Pre] => ??? // Excluded by RemoveUnpointedGuard + } + loop.rewrite(guards = dedup(guards)) + + case _ => rewriteDefault(statement) + } + + def dedup(guards: Seq[EndpointGuard[Pre]]): Seq[EndpointGuard[Post]] = { + val m: mutable.LinkedHashMap[Endpoint[Pre], Seq[Expr[Pre]]] = mutable.LinkedHashMap() + guards.foreach { guard => + m.updateWith(guard.endpoint.decl)(exprs => Some(exprs.getOrElse(Nil) :+ guard.condition)) + } + m.iterator.map { case (endpoint, exprs) => + EndpointGuard[Post](succ(endpoint), foldAnd(exprs.map(dispatch))(DiagnosticOrigin))(exprs.head.o) + }.toSeq + } +} diff --git a/src/rewrite/vct/rewrite/veymont/EncodeSeqBranchUnanimity.scala b/src/rewrite/vct/rewrite/veymont/EncodeSeqBranchUnanimity.scala new file mode 100644 index 0000000000..f80076c56a --- /dev/null +++ b/src/rewrite/vct/rewrite/veymont/EncodeSeqBranchUnanimity.scala @@ -0,0 +1,99 @@ +package vct.rewrite.veymont + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.{AssertFailed, Blame, BranchUnanimityFailed, LoopUnanimityNotEstablished, LoopUnanimityNotMaintained, Origin} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.util.AstBuildHelpers._ +import vct.col.util.SuccessionMap +import vct.result.VerificationError.UserError +import vct.rewrite.veymont.EncodeSeqBranchUnanimity.{ForwardBranchUnanimity, ForwardLoopUnanimityNotEstablished, ForwardLoopUnanimityNotMaintained} + +import scala.collection.mutable + +object EncodeSeqBranchUnanimity extends RewriterBuilder { + override def key: String = "encodeSeqBranchUnanimity" + override def desc: String = "Encodes the branch unanimity requirement imposed by VeyMont on branches and loops in seq_program nodes." + + case class ForwardBranchUnanimity(branch: SeqBranch[_], c1: SeqGuard[_], c2: SeqGuard[_]) extends Blame[AssertFailed] { + override def blame(error: AssertFailed): Unit = + branch.blame.blame(BranchUnanimityFailed(c1, c2)) + } + + case class ForwardLoopUnanimityNotEstablished(loop: SeqLoop[_], c1: SeqGuard[_], c2: SeqGuard[_]) extends Blame[AssertFailed] { + override def blame(error: AssertFailed): Unit = + loop.blame.blame(LoopUnanimityNotEstablished(c1, c2)) + } + + case class ForwardLoopUnanimityNotMaintained(loop: SeqLoop[_], c1: SeqGuard[_], c2: SeqGuard[_]) extends Blame[AssertFailed] { + override def blame(error: AssertFailed): Unit = + loop.blame.blame(LoopUnanimityNotMaintained(c1, c2)) + } +} + +case class EncodeSeqBranchUnanimity[Pre <: Generation]() extends Rewriter[Pre] { + + val currentLoop = ScopedStack[SeqLoop[Pre]]() + + override def dispatch(statement: Statement[Pre]): Statement[Post] = statement match { + case branch @ SeqBranch(guards, yes, no) => + implicit val o = statement.o + + val assertions: Block[Post] = Block(guards.indices.init.map { i => + Assert(rewriteGuard(guards(i)) === rewriteGuard(guards(i + 1)))( + ForwardBranchUnanimity(branch, guards(i), guards(i + 1))) + }) + + Block(Seq( + assertions, + Branch[Post]( + Seq((foldAnd(guards.map(rewriteGuard)), dispatch(yes))) ++ + no.map { no => Seq((tt[Post], dispatch(no))) }.getOrElse(Nil)) + )) + + case loop @ SeqLoop(guards, contract, body) => + implicit val o = statement.o + + val establishAssertions: Statement[Post] = Block(guards.indices.init.map { i => + Assert(rewriteGuard(guards(i)) === rewriteGuard(guards(i + 1)))( + ForwardLoopUnanimityNotEstablished(loop, guards(i), guards(i + 1))) + }) + + val maintainAssertions: Statement[Post] = Block(guards.indices.init.map { i => + Assert(rewriteGuard(guards(i)) === rewriteGuard(guards(i + 1)))( + ForwardLoopUnanimityNotMaintained(loop, guards(i), guards(i + 1))) + }) + + val finalLoop: Loop[Post] = Loop( + establishAssertions, + foldAnd(guards.map(rewriteGuard)), + maintainAssertions, + currentLoop.having(loop) { + dispatch(contract) + }, + dispatch(body) + ) + + finalLoop + + case statement => rewriteDefault(statement) + } + + def rewriteGuard(guard: SeqGuard[Pre]): Expr[Post] = dispatch(guard.condition) + + def allEqual[G](exprs: Seq[Expr[G]])(implicit o: Origin): Expr[G] = + foldAnd[G](exprs.indices.init.map(i => exprs(i) === exprs(i + 1))) + + override def dispatch(contract: LoopContract[Pre]): LoopContract[Post] = (currentLoop.topOption, contract) match { + case (Some(loop), inv: LoopInvariant[Pre]) => + implicit val o = contract.o + inv.rewrite(invariant = dispatch(inv.invariant) &* allEqual(loop.guards.map(rewriteGuard))) + case (Some(loop), inv @ IterationContract(requires, ensures, _)) => + implicit val o = contract.o + inv.rewrite( + requires = dispatch(requires) &* allEqual(loop.guards.map(rewriteGuard)), + ensures = dispatch(ensures) &* allEqual(loop.guards.map(rewriteGuard))) + case _ => rewriteDefault(contract) + } +} diff --git a/src/rewrite/vct/rewrite/veymont/EncodeSeqProg.scala b/src/rewrite/vct/rewrite/veymont/EncodeSeqProg.scala index bb164eda7f..9dc3bb4cd9 100644 --- a/src/rewrite/vct/rewrite/veymont/EncodeSeqProg.scala +++ b/src/rewrite/vct/rewrite/veymont/EncodeSeqProg.scala @@ -2,13 +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, Local, LocalDecl, Node, Procedure, Scope, SeqAssign, SeqProg, SeqRun, Statement, Subject, TClass, TVoid, Variable} -import vct.col.origin.{Blame, CallableFailure, DiagnosticOrigin, Origin, PanicBlame, VerificationFailure} +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, Blame, CallableFailure, ContextEverywhereFailedInPost, ContractedFailure, DiagnosticOrigin, ExceptionNotInSignals, InsufficientPermission, Origin, PanicBlame, PostconditionFailed, SeqAssignFailure, SeqAssignInsufficientPermission, SeqCallableFailure, SignalsFailed, TerminationMeasureFailed, VerificationFailure} import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.col.util.AstBuildHelpers._ import vct.col.util.SuccessionMap -import vct.result.VerificationError.UserError -import EncodeSeqProg.{CallableFailureNotSupportedBlame, CommunicateNotSupported, GeneratedPerm, SeqAssignNotSupported} +import vct.result.VerificationError.{Unreachable, UserError} +import EncodeSeqProg.{AssignFailedToSeqAssignFailure, CallableFailureToSeqCallableFailure, InsufficientPermissionToAccessFailure} import vct.col.ref.Ref import scala.collection.{mutable => mut} @@ -17,25 +17,29 @@ object EncodeSeqProg extends RewriterBuilder { override def key: String = "encodeSeqProg" override def desc: String = "Encodes the semantics of a parallel VeyMont program." - case object CommunicateNotSupported extends UserError { - override def code: String = "communicateNotSupported" - override def text: String = "The `communicate` statement is not yet supported" - } + object SignalsAlwaysEmpty extends PanicBlame("signals always empty") - case object SeqAssignNotSupported extends UserError { - override def code: String = "seqAssignNotSupported" - override def text: String = "The `:=` statement is not yet supported" + case class CallableFailureToSeqCallableFailure(seqBlame: Blame[SeqCallableFailure]) extends Blame[CallableFailure] { + override def blame(error: CallableFailure): Unit = error match { + case failure: SeqCallableFailure => seqBlame.blame(failure) + case SignalsFailed(failure, node) => SignalsAlwaysEmpty.blame(error) + case ExceptionNotInSignals(node) => SignalsAlwaysEmpty.blame(error) + } } - object GeneratedPerm extends PanicBlame("Permissions for these locations should be generated.") - - case class CallableFailureNotSupported(n: Node[_]) extends UserError { - override def code: String = "callableFailureNotSupported" - override def text: String = n.o.messageInContext("Failures of type CallableFailure are not yet supported for this node") + case class InsufficientPermissionToAccessFailure(access: Access[_]) extends Blame[VerificationFailure] { + override def blame(error: VerificationFailure): Unit = error match { + case _: AssignFailed => + access.blame.blame(AccessInsufficientPermission(access)) + case _: InsufficientPermission => + access.blame.blame(AccessInsufficientPermission(access)) + case _ => PanicBlame("Error should either be AssignFailed or InsufficientPermission").blame(error) + } } - case class CallableFailureNotSupportedBlame(node: Node[_]) extends Blame[CallableFailure] { - override def blame(error: CallableFailure): Unit = throw CallableFailureNotSupported(node) + case class AssignFailedToSeqAssignFailure(assign: SeqAssign[_]) extends Blame[AssignFailed] { + override def blame(error: AssignFailed): Unit = + assign.blame.blame(SeqAssignInsufficientPermission(assign)) } } @@ -43,34 +47,42 @@ case class EncodeSeqProg[Pre <: Generation]() extends Rewriter[Pre] with LazyLog val currentProg: ScopedStack[SeqProg[Pre]] = ScopedStack() val currentRun: ScopedStack[SeqRun[Pre]] = ScopedStack() + val currentInstanceMethod: ScopedStack[InstanceMethod[Pre]] = ScopedStack() sealed trait Mode case object Top extends Mode case class InProg(prog: SeqProg[Pre]) extends Mode case class InRun(prog: SeqProg[Pre], run: SeqRun[Pre]) extends Mode - - def mode: Mode = (currentProg.topOption, currentRun.topOption) match { - case (None, None) => Top - case (Some(prog), None) => InProg(prog) - case (Some(prog), Some(run)) => InRun(prog, run) - case (None, Some(_)) => throw new RuntimeException() + case class InMethod(prog: SeqProg[Pre], method: InstanceMethod[Pre]) extends Mode + + def mode: Mode = (currentProg.topOption, currentRun.topOption, currentInstanceMethod.topOption) match { + case (None, None, None) => Top + case (Some(prog), None, None) => InProg(prog) + case (Some(prog), Some(run), None) => InRun(prog, run) + case (Some(prog), None, Some(method)) => InMethod(prog, method) + case (None, None, Some(_)) => Top + case (_, _, _) => throw Unreachable("AST structure should prevent this case") } val runSucc: mut.Map[SeqRun[Pre], Procedure[Post]] = mut.LinkedHashMap() val progSucc: SuccessionMap[SeqProg[Pre], Procedure[Post]] = SuccessionMap() + val methodSucc: SuccessionMap[InstanceMethod[Pre], Procedure[Post]] = SuccessionMap() val endpointSucc: SuccessionMap[(Mode, Endpoint[Pre]), Variable[Post]] = SuccessionMap() val variableSucc: SuccessionMap[(Mode, Variable[Pre]), Variable[Post]] = SuccessionMap() - override def dispatch(decl: Declaration[Pre]): Unit = decl match { - case prog: SeqProg[Pre] => currentProg.having(prog) { + override def dispatch(decl: Declaration[Pre]): Unit = (mode, decl) match { + case (Top, prog: SeqProg[Pre]) => currentProg.having(prog) { // First generate a procedure that implements the run method - rewriteRun(prog.run) + rewriteRun(prog) + + // And also process all auxiliary instance methods + prog.decls.foreach(dispatch) // Then generate a procedure that initializes all the endpoints and calls the run procedure // First set up the succesor variables that will be encoding the seq_program argument and endpoints implicit val o = prog.o prog.endpoints.foreach(_.drop()) - for (endpoint <- currentProg.top.endpoints) { + for (endpoint <- prog.endpoints) { endpointSucc((mode, endpoint)) = new Variable(TClass(succ[Class[Post]](endpoint.cls.decl)))(endpoint.o) } @@ -111,32 +123,51 @@ case class EncodeSeqProg[Pre <: Generation]() extends Rewriter[Pre] with LazyLog args = prog.args.map(arg => variableSucc((mode, arg))), contract = dispatch(prog.contract), body = Some(body) - )(PanicBlame("TODO: callable failure blame"))) + )(CallableFailureToSeqCallableFailure(prog.blame))) + } + + case (InProg(prog), method: InstanceMethod[Pre]) => currentInstanceMethod.having(method) { + for (endpoint <- prog.endpoints) { + endpointSucc((mode, endpoint)) = new Variable(TClass(succ[Class[Post]](endpoint.cls.decl)))(endpoint.o) + } + + prog.args.foreach(_.drop()) + for (arg <- prog.args) { + variableSucc((mode, arg)) = new Variable(dispatch(arg.t))(arg.o) + } + + methodSucc(method) = globalDeclarations.declare(new Procedure( + args = prog.args.map(arg => variableSucc((mode, arg))) ++ + prog.endpoints.map(endpoint => endpointSucc((mode, endpoint))), + body = method.body.map(dispatch), + outArgs = Nil, typeArgs = Nil, returnType = dispatch(method.returnType), contract = dispatch(method.contract) + )(method.blame)(method.o)) } case _ => rewriteDefault(decl) } - def rewriteRun(run: SeqRun[Pre]): Unit = { + def rewriteRun(prog: SeqProg[Pre]): Unit = { + val run = prog.run implicit val o: Origin = run.o.where(name = currentProg.top.o.getPreferredNameOrElse().snake + "_run") currentRun.having(run) { - for (endpoint <- currentProg.top.endpoints) { - endpointSucc((mode, endpoint)) = new Variable(TClass(succ[Class[Post]](endpoint.cls.decl))) + for (endpoint <- prog.endpoints) { + endpointSucc((mode, endpoint)) = new Variable(TClass(succ[Class[Post]](endpoint.cls.decl)))(endpoint.o) } - for (arg <- currentProg.top.args) { + for (arg <- prog.args) { variableSucc((mode, arg)) = new Variable(dispatch(arg.t))(arg.o) } runSucc(run) = globalDeclarations.declare(new Procedure( - args = currentProg.top.args.map(arg => variableSucc((mode, arg))) ++ - currentProg.top.endpoints.map(endpoint => endpointSucc((mode, endpoint))), + args = prog.args.map(arg => variableSucc((mode, arg))) ++ + prog.endpoints.map(endpoint => endpointSucc((mode, endpoint))), contract = dispatch(run.contract), body = Some(dispatch(run.body)), outArgs = Seq(), typeArgs = Seq(), returnType = TVoid(), - )(CallableFailureNotSupportedBlame(run))) + )(CallableFailureToSeqCallableFailure(run.blame))) } } @@ -147,20 +178,20 @@ case class EncodeSeqProg[Pre <: Generation]() extends Rewriter[Pre] with LazyLog Deref[Post]( Local(endpointSucc((mode, endpoint)).ref), succ(field) - )(GeneratedPerm), + )(PanicBlame("Unused by Silver encoding")), dispatch(e) - )(GeneratedPerm) - case comm@Communicate(receiver, sender) => + )(AssignFailedToSeqAssignFailure(assign)) + case comm @ Communicate(receiver, sender) => implicit val o = comm.o Assign[Post]( rewriteAccess(receiver), rewriteAccess(sender) - )(GeneratedPerm) + )(InsufficientPermissionToAccessFailure(receiver)) case stat => rewriteDefault(stat) } def rewriteAccess(access: Access[Pre]): Expr[Post] = - Deref[Post](rewriteSubject(access.subject), succ(access.field.decl))(GeneratedPerm)(access.o) + Deref[Post](rewriteSubject(access.subject), succ(access.field.decl))(InsufficientPermissionToAccessFailure(access))(access.o) def rewriteSubject(subject: Subject[Pre]): Expr[Post] = subject match { case EndpointName(Ref(endpoint)) => Local[Post](endpointSucc((mode, endpoint)).ref)(subject.o) @@ -171,6 +202,16 @@ case class EncodeSeqProg[Pre <: Generation]() extends Rewriter[Pre] with LazyLog Local[Post](endpointSucc((mode, endpoint)).ref)(expr.o) case (mode, Local(Ref(v))) if mode != Top && currentProg.top.args.contains(v) => Local[Post](variableSucc((mode, v)).ref)(expr.o) + case (mode, invocation @ MethodInvocation(ThisSeqProg(_), Ref(method), args, _, _, _, _)) if mode != Top => + implicit val o = invocation.o + val prog = currentProg.top + assert(args.isEmpty) + procedureInvocation( + ref = methodSucc.ref(method), + args = prog.args.map(arg => Local[Post](variableSucc.ref((mode, arg)))(arg.o)) ++ + prog.endpoints.map(endpoint => Local[Post](endpointSucc.ref((mode, endpoint)))(invocation.o)), + blame = invocation.blame + ) case (_, expr) => rewriteDefault(expr) } } diff --git a/src/rewrite/vct/rewrite/veymont/EncodeUnpointedGuard.scala b/src/rewrite/vct/rewrite/veymont/EncodeUnpointedGuard.scala new file mode 100644 index 0000000000..380f14206c --- /dev/null +++ b/src/rewrite/vct/rewrite/veymont/EncodeUnpointedGuard.scala @@ -0,0 +1,61 @@ +package vct.rewrite.veymont + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.origin.{Origin} +import vct.col.ref.Ref +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.util.AstBuildHelpers._ +import vct.result.VerificationError.UserError +import vct.rewrite.veymont.SplitSeqGuards.MultipleEndpoints + +import scala.collection.immutable.ListSet + +object EncodeUnpointedGuard extends RewriterBuilder { + override def key: String = "encodeUnpointedGuard" + override def desc: String = "Encodes unpointed guard by duplicating the condition to all guards currently participating" +} + +case class EncodeUnpointedGuard[Pre <: Generation]() extends Rewriter[Pre] { + val currentParticipants: ScopedStack[ListSet[Endpoint[Pre]]] = ScopedStack() + + override def dispatch(decl: Declaration[Pre]): Unit = decl match { + case prog: SeqProg[Pre] => currentParticipants.having(ListSet.from(prog.endpoints)) { + rewriteDefault(prog) + } + + case decl => rewriteDefault(decl) + } + + override def dispatch(statement: Statement[Pre]): Statement[Post] = statement match { + case branch: SeqBranch[Pre] => + val newParticipants = if (branch.hasUnpointed) { + currentParticipants.top + } else { + ListSet.from(branch.participants) + } + currentParticipants.having(newParticipants) { + branch.rewrite(guards = branch.guards.flatMap(rewriteGuard)) + } + + case loop: SeqLoop[Pre] => + val newParticipants = if (loop.hasUnpointed) { + currentParticipants.top + } else { + ListSet.from(loop.participants) + } + currentParticipants.having(newParticipants) { + loop.rewrite(guards = loop.guards.flatMap(rewriteGuard)) + } + + case statement => rewriteDefault(statement) + } + + def rewriteGuard(guard: SeqGuard[Pre]): Seq[SeqGuard[Post]] = guard match { + case guard: EndpointGuard[Pre] => Seq(guard.rewriteDefault()) + case UnpointedGuard(expr) => currentParticipants.top.map { endpoint => + EndpointGuard[Post](succ(endpoint), dispatch(expr))(guard.o) + }.toSeq + } +} diff --git a/src/rewrite/vct/rewrite/veymont/GenerateSeqProgPermissions.scala b/src/rewrite/vct/rewrite/veymont/GenerateSeqProgPermissions.scala index 141124feda..b67955eb59 100644 --- a/src/rewrite/vct/rewrite/veymont/GenerateSeqProgPermissions.scala +++ b/src/rewrite/vct/rewrite/veymont/GenerateSeqProgPermissions.scala @@ -4,65 +4,153 @@ import com.typesafe.scalalogging.LazyLogging import hre.util.ScopedStack import vct.col.ast.RewriteHelpers._ import vct.col.util.AstBuildHelpers._ -import vct.col.ast.{ApplicableContract, ArraySubscript, Declaration, Deref, Endpoint, EndpointUse, EnumUse, Expr, FieldLocation, InstanceField, IterationContract, Length, Local, LoopContract, LoopInvariant, Null, Perm, SeqProg, SeqRun, SplitAccountedPredicate, TArray, TClass, TInt, Type, UnitAccountedPredicate, WritePerm} +import vct.col.ast.{Applicable, ApplicableContract, ArraySubscript, BooleanValue, Class, ContractApplicable, Declaration, Deref, Endpoint, EndpointGuard, EndpointName, SeqLoop, EndpointUse, EnumUse, Expr, FieldLocation, Function, InstanceField, InstanceFunction, InstanceMethod, IterationContract, Length, Local, LoopContract, LoopInvariant, Node, Null, Perm, Procedure, Result, SeqAssign, SeqProg, SeqRun, SplitAccountedPredicate, Statement, TArray, TClass, TInt, ThisObject, Type, UnitAccountedPredicate, Variable, WritePerm} +import vct.col.ast.declaration.global.SeqProgImpl.participants import vct.col.origin.{Origin, PanicBlame} import vct.col.ref.Ref -import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg} +import scala.collection.immutable.ListSet -object GenerateSeqProgPermissions extends RewriterBuilder { +object GenerateSeqProgPermissions extends RewriterBuilderArg[Boolean] { override def key: String = "generateSeqProgPermissions" - override def desc: String = "Generates permissions for fields of some types (int, bool, and arrays of simple datatypes) for constructs used inside seq_program." + override def desc: String = "Generates permissions for fields of some types (classes, int, bool, and arrays of these) for constructs used inside seq_program." } -case class GenerateSeqProgPermissions[Pre <: Generation]() extends Rewriter[Pre] with LazyLogging { +case class GenerateSeqProgPermissions[Pre <: Generation](enabled: Boolean = false) extends Rewriter[Pre] with LazyLogging { + val currentPerm: ScopedStack[Expr[Post]] = ScopedStack() val currentProg: ScopedStack[SeqProg[Pre]] = ScopedStack() - val currentRun: ScopedStack[SeqRun[Pre]] = ScopedStack() + + /* - Permission generation table - + Only considers nodes as necessary for VeyMont case studies. + + Pre Post Invariant + Function: args N.a + Procedure: args args, return args + + Instance function: args, fields N.a + Instance method: args, fields args, fields, return args, fields + + SeqProg: args args N.a + SeqRun: endpoints endpoints endpoints + */ override def dispatch(decl: Declaration[Pre]): Unit = decl match { - case prog: SeqProg[Pre] => currentProg.having(prog) { rewriteDefault(prog) } + case fun: Function[Pre] if enabled => + globalDeclarations.succeed(fun, fun.rewrite( + contract = prependContract(fun.contract, variablesPerm(fun.args)(fun.o), tt)(fun.o) + )) + case proc: Procedure[Pre] if enabled => + implicit val o = proc.o + globalDeclarations.succeed(proc, proc.rewrite( + contract = prependContract( + proc.contract, + variablesPerm(proc.args), + variablesPerm(proc.args) &* resultPerm(proc)(proc.o)), + body = proc.body.map(body => currentPerm.having(variablesPerm(proc.args)) { dispatch(body) }) + )) + + case cls: Class[Pre] if enabled => currentPerm.having(classPerm(cls)) { rewriteDefault(cls) } + + case fun: InstanceFunction[Pre] if enabled => + implicit val o = fun.o + classDeclarations.succeed(fun, fun.rewrite(contract = prependContract(fun.contract, currentPerm.top, tt))) + + case method: InstanceMethod[Pre] if enabled && currentProg.nonEmpty => + implicit val o = method.o + classDeclarations.succeed(method, method.rewrite( + contract = prependContract( + method.contract, + endpointsPerm(participants(method).toSeq), + endpointsPerm(participants(method).toSeq) + ) + )) + + case method: InstanceMethod[Pre] if enabled => + // Permission generation for InstanceMethods in classes + implicit val o = method.o + classDeclarations.succeed(method, method.rewrite( + contract = prependContract( + method.contract, + currentPerm.top, + currentPerm.top &* resultPerm(method) + ) + )) + + case prog: SeqProg[Pre] if enabled => + val run = prog.run + currentProg.having(prog) { + globalDeclarations.succeed(prog, prog.rewrite( + contract = prependContract( + prog.contract, + variablesPerm(prog.args)(prog.o), + variablesPerm(prog.args)(prog.o) + )(prog.o), + run = run.rewrite( + contract = prependContract( + run.contract, + endpointsPerm(prog.endpoints)(run.o), + endpointsPerm(prog.endpoints)(run.o), + )(run.o), + body = currentPerm.having(endpointsPerm(prog.endpoints)(run.o)) { + rewriteDefault(run.body) + }))) + } + case decl => rewriteDefault(decl) } - override def dispatch(run: SeqRun[Pre]): SeqRun[Post] = currentRun.having(run) { rewriteDefault(run) } - - override def dispatch(contract: ApplicableContract[Pre]): ApplicableContract[Post] = - (currentProg.topOption, currentRun.topOption) match { - case (Some(prog), Some(_)) => - implicit val o = contract.o - contract.rewrite( - requires = - SplitAccountedPredicate[Post]( - UnitAccountedPredicate(foldStar[Post](prog.endpoints.map(endpointPerm))), - dispatch(contract.requires) - ), - ensures = - SplitAccountedPredicate[Post]( - UnitAccountedPredicate(foldStar[Post](prog.endpoints.map(endpointPerm))), - dispatch(contract.ensures) - ) - ) - case _ => rewriteDefault(contract) - } - - override def dispatch(loopContract: LoopContract[Pre]): LoopContract[Post] = (currentProg.topOption, currentRun.topOption, loopContract) match { - case (Some(prog), Some(_), invariant: LoopInvariant[pre]) => - implicit val o = loopContract.o - invariant.rewrite( - invariant = foldStar[Post](prog.endpoints.map(endpointPerm) :+ dispatch(invariant.invariant)) - ) - case (Some(prog), Some(_), iteration: IterationContract[pre]) => - implicit val o = loopContract.o - iteration.rewrite( - requires = foldStar[Post](prog.endpoints.map(endpointPerm) :+ dispatch(iteration.requires)), - ensures = foldStar[Post](prog.endpoints.map(endpointPerm) :+ dispatch(iteration.ensures)) - ) - case _ => rewriteDefault(loopContract) + def prependContract(contract: ApplicableContract[Pre], pre: Expr[Post], post: Expr[Post])(implicit o: Origin) = + contract.rewrite( + requires = pre match { + case BooleanValue(true) => dispatch(contract.requires) + case pre => SplitAccountedPredicate[Post](UnitAccountedPredicate(pre), dispatch(contract.requires)) + }, + ensures = post match { + case BooleanValue(true) => dispatch(contract.ensures) + case post => SplitAccountedPredicate[Post](UnitAccountedPredicate(post), dispatch(contract.ensures)) + } + ) + + override def dispatch(statement: Statement[Pre]): Statement[Post] = statement match { + case loop: SeqLoop[Pre] => + currentPerm.having(endpointsPerm(participants(statement).toSeq)(loop.contract.o)) { + loop.rewriteDefault() + } + case statement => rewriteDefault(statement) } + override def dispatch(loopContract: LoopContract[Pre]): LoopContract[Post] = + (currentPerm.topOption, loopContract) match { + case (Some(perm), invariant: LoopInvariant[pre]) => + implicit val o = loopContract.o + invariant.rewrite(invariant = perm &* dispatch(invariant.invariant)) + case (Some(perm), iteration: IterationContract[pre]) => + implicit val o = loopContract.o + iteration.rewrite( + requires = perm &* dispatch(iteration.requires), + ensures = perm &* dispatch(iteration.ensures)) + case _ => rewriteDefault(loopContract) + } + def endpointPerm(endpoint: Endpoint[Pre])(implicit o: Origin): Expr[Post] = transitivePerm(EndpointUse[Post](succ(endpoint)), TClass(endpoint.cls)) + def endpointsPerm(endpoints: Seq[Endpoint[Pre]])(implicit o: Origin): Expr[Post] = + foldStar(endpoints.map(endpointPerm)) + + def variablePerm(variable: Variable[Pre]): Expr[Post] = + transitivePerm(Local[Post](succ(variable))(variable.o), variable.t)(variable.o) + + def variablesPerm(variables: Seq[Variable[Pre]])(implicit o: Origin): Expr[Post] = + foldStar(variables.map(variablePerm)) + + def resultPerm(app: ContractApplicable[Pre])(implicit o: Origin): Expr[Post] = + transitivePerm(Result[Post](anySucc(app)), app.returnType) + + def classPerm(cls: Class[Pre]): Expr[Post] = + transitivePerm(ThisObject[Post](succ(cls))(cls.o), TClass(cls.ref))(cls.o) + /* int x; @@ -99,5 +187,4 @@ case class GenerateSeqProgPermissions[Pre <: Generation]() extends Rewriter[Pre] fieldPerm[Post](`this`, succ(f), WritePerm()) &* transitivePerm(Deref[Post](`this`, succ(f))(PanicBlame("Permission for this field is already established")), f.t) } - } diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala index e24b9286de..1a06e44e2f 100644 --- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala +++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala @@ -2,8 +2,8 @@ package vct.rewrite.veymont import hre.util.ScopedStack import vct.col.ast.RewriteHelpers.{RewriteApplicableContract, RewriteClass, RewriteDeref, RewriteJavaClass, RewriteJavaConstructor, RewriteMethodInvocation} -import vct.col.ast.{AbstractRewriter, ApplicableContract, Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, CommunicateX, Declaration, Deref, Endpoint, EndpointUse, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaLocal, JavaMethod, JavaNamedType, JavaParam, JavaPublic, JavaTClass, Local, Loop, MethodInvocation, NewObject, Node, Procedure, Program, RunMethod, Scope, SeqProg, SeqRun, Statement, TClass, TVeyMontChannel, TVoid, ThisObject, ThisSeqProg, Type, UnitAccountedPredicate, Variable, VeyMontAssignExpression, VeyMontCondition} -import vct.col.origin.Origin +import vct.col.ast.{AbstractRewriter, ApplicableContract, Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, CommunicateX, Declaration, Deref, Endpoint, EndpointUse, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaLocal, JavaMethod, JavaNamedType, JavaParam, JavaPublic, JavaTClass, Local, Loop, MethodInvocation, NewObject, Node, Procedure, Program, RunMethod, Scope, SeqGuard, SeqProg, SeqRun, Statement, TClass, TVeyMontChannel, TVoid, ThisObject, ThisSeqProg, Type, UnitAccountedPredicate, Variable, VeyMontAssignExpression} +import vct.col.origin.{Origin, PanicBlame} import vct.col.resolve.ctx.RefJavaMethod import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, RewriterBuilderArg, Rewritten} import vct.col.util.SuccessionMap @@ -284,14 +284,15 @@ case class ParalleliseEndpoints[Pre <: Generation](channelClass: JavaClass[_]) e TVoid[Post](), Seq.empty,Seq.empty,Seq.empty, Some(dispatch(run.body)), - dispatch(run.contract))(run.blame)(RunMethodOrigin(run)) + dispatch(run.contract))(PanicBlame("TODO: Convert InstanceMethod blame to SeqRun blame")/* run.blame */)(RunMethodOrigin(run)) } override def dispatch(node: Expr[Pre]): Expr[Post] = { if(threadBuildingBlocks.nonEmpty) { val thread = threadBuildingBlocks.top.thread node match { - case c: VeyMontCondition[Pre] => paralleliseThreadCondition(node, thread, c) + // TODO: Disabled this because the AST changed, repair + // case c: SeqGuard[Pre] => paralleliseThreadCondition(node, thread, c) case m: MethodInvocation[Pre] => updateThreadRefMethodInvoc(thread, m) case d: Deref[Pre] => updateThreadRefInDeref(node, thread, d) case t: EndpointUse[Pre] => updateThreadRefVeyMontDeref(node, thread, t) @@ -326,13 +327,15 @@ case class ParalleliseEndpoints[Pre <: Generation](channelClass: JavaClass[_]) e } } - private def paralleliseThreadCondition(node: Expr[Pre], thread: Endpoint[Pre], c: VeyMontCondition[Pre]) = { - c.condition.find { case (threadRef, _) => - threadRef.decl == thread - } match { - case Some((_, threadExpr)) => dispatch(threadExpr) - case _ => throw ParalleliseEndpointsError(node, "Condition of if statement or while loop must contain an expression for every thread") - } + private def paralleliseThreadCondition(node: Expr[Pre], thread: Endpoint[Pre], c: SeqGuard[Pre]) = { + ??? + // TODO: Broke this because AST changed, repair +// c.conditions.find { case (threadRef, _) => +// threadRef.decl == thread +// } match { +// case Some((_, threadExpr)) => dispatch(threadExpr) +// case _ => throw ParalleliseEndpointsError(node, "Condition of if statement or while loop must contain an expression for every thread") +// } } private def getThisVeyMontDeref(thread: Endpoint[Pre], o: Origin, threadField: InstanceField[Rewritten[Pre]]) = { diff --git a/src/rewrite/vct/rewrite/veymont/SplitSeqGuards.scala b/src/rewrite/vct/rewrite/veymont/SplitSeqGuards.scala new file mode 100644 index 0000000000..8e2909ee6b --- /dev/null +++ b/src/rewrite/vct/rewrite/veymont/SplitSeqGuards.scala @@ -0,0 +1,102 @@ +package vct.rewrite.veymont + +import hre.util.ScopedStack +import vct.col.ast.RewriteHelpers._ +import vct.col.ast._ +import vct.col.check.SeqProgParticipant +import vct.col.origin.{Blame, Origin, SeqBranchFailure} +import vct.col.ref.Ref +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.util.AstBuildHelpers._ +import vct.result.VerificationError.UserError +import vct.rewrite.veymont.SplitSeqGuards.{MultipleEndpoints, SeqProgParticipantErrors} + +import scala.collection.immutable.ListSet +import scala.collection.mutable + +object SplitSeqGuards extends RewriterBuilder { + override def key: String = "splitSeqGuards" + override def desc: String = "Lifts conditions in loops and conditionals into the SeqGuard AST node, stratifying the condition per endpoint." + + case class MultipleEndpoints(e: Expr[_]) extends UserError { + override def code: String = "multipleEndpoints" + override def text: String = e.o.messageInContext("This expression references multiple endpoints, but that is not yet supported.") + } + + case class SeqProgParticipantErrors(es: Seq[SeqProgParticipant]) extends UserError { + override def code: String = "seqProgParticipantErrors" + override def text: String = es.map { + case err: SeqProgParticipant => err.message { n => n.o } + }.mkString("\n") + } +} + +case class SplitSeqGuards[Pre <: Generation]() extends Rewriter[Pre] { + val currentProg: ScopedStack[SeqProg[Pre]] = ScopedStack() + val currentParticipants: ScopedStack[ListSet[Pre]] = ScopedStack() + + override def dispatch(prog: Program[Pre]): Program[Post] = { + val newProg = prog.rewrite() + val errors = newProg.check + val seqBranchErrors = errors.collect { + case err: SeqProgParticipant => err + } + if (errors.nonEmpty && errors.length == seqBranchErrors.length) { + throw SeqProgParticipantErrors(seqBranchErrors) + } + newProg + } + + override def dispatch(decl: Declaration[Pre]): Unit = decl match { + case prog: SeqProg[Pre] => + currentProg.having(prog) { + rewriteDefault(prog) + } + case decl => rewriteDefault(decl) + } + + override def dispatch(statement: Statement[Pre]): Statement[Post] = statement match { + case branch: UnresolvedSeqBranch[Pre] => + assert(branch.branches.nonEmpty) + unfoldBranch(branch.branches)(branch.blame, branch.o) + + case loop: UnresolvedSeqLoop[Pre] if currentProg.nonEmpty => + SeqLoop( + inferSeqGuard(loop.cond), + dispatch(loop.contract), + dispatch(loop.body) + )(loop.blame)(loop.o) + + case statement => rewriteDefault(statement) + } + + def unfoldBranch(branches: Seq[(Expr[Pre], Statement[Pre])])(implicit blame: Blame[SeqBranchFailure], o: Origin): SeqBranch[Post] = branches match { + case Seq((e, s)) => SeqBranch(inferSeqGuard(e), dispatch(s), None)(blame) + case (e, s) +: (otherYes +: branches) => + SeqBranch(inferSeqGuard(e), dispatch(s), Some(unfoldBranch(otherYes +: branches)))(blame) + case _ => ??? + } + + // Infer guard conditions based on the classic syntactical restrictions - endpoint dereferences determine which + // endpoint is evaluating the expression. + def inferSeqGuard(e: Expr[Pre]): Seq[SeqGuard[Post]] = { + val exprs = unfoldStar(e) + val pointed = exprs.map(point) + pointed.map { + case (Some(endpoint), expr) => EndpointGuard[Post](succ(endpoint), dispatch(expr))(expr.o) + case (None, expr) => UnpointedGuard(dispatch(expr))(expr.o) + } + } + + // "Points" an expression in the direction of an endpoint if possible + def point(e: Expr[Pre]): (Option[Endpoint[Pre]], Expr[Pre]) = { + val endpoints: Seq[Endpoint[Pre]] = e.collect { case Deref(EndpointUse(Ref(endpoint)), _) => endpoint } + endpoints match { + case Seq(endpoint) => + // expr is totally in context of one endpoint and whatever else is in scope + (Some(endpoint), e) + case Seq() => (None, e) + case _ => throw MultipleEndpoints(e) // Expr uses multiple endpoints - for now we should disallow that. + } + } +} diff --git a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala b/src/rewrite/vct/rewrite/veymont/StructureCheck.scala index 8af70cef17..0930229885 100644 --- a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala +++ b/src/rewrite/vct/rewrite/veymont/StructureCheck.scala @@ -2,7 +2,6 @@ package vct.col.rewrite.veymont import hre.util.ScopedStack import vct.col.ast._ -import vct.col.rewrite.veymont.AddVeyMontAssignmentNodes.{getDerefsFromExpr,getThreadDeref} import vct.col.rewrite.veymont.StructureCheck.VeyMontStructCheckError import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.result.VerificationError.UserError @@ -79,13 +78,12 @@ case class StructureCheck[Pre <: Generation]() extends Rewriter[Pre] { case ThisSeqProg(_) => if (args.isEmpty) rewriteDefault(st) else throw VeyMontStructCheckError(st, "Calls to methods in seq_program cannot have any arguments!") - case EndpointUse(thread) => - val argderefs = args.flatMap(getDerefsFromExpr) - val argthreads = argderefs.map(d => getThreadDeref(d, - VeyMontStructCheckError(st, "A method call on a thread object may only refer to a thread in its arguments!"))) - if (argthreads.forall(_ == thread.decl)) - rewriteDefault(st) - else throw VeyMontStructCheckError(st, "A method call on a thread object may only refer to same thread in its arguments!") + case EndpointUse(thread) => ??? + // val argderefs = ??? // args.flatMap(getDerefsFromExpr) + // val argthreads = argderefs.map(d => ???) // getThreadDeref(d, VeyMontStructCheckError(st, "A method call on a thread object may only refer to a thread in its arguments!"))) + // if (argthreads.forall(_ == thread.decl)) + // rewriteDefault(st) + // else throw VeyMontStructCheckError(st, "A method call on a thread object may only refer to same thread in its arguments!") case _ => throw VeyMontStructCheckError(st, "This kind of method call is not allowed in seq_program") } case _ => throw VeyMontStructCheckError(st, "This is not a method call") diff --git a/test/main/vct/test/integration/examples/TechnicalVeyMontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeyMontSpec.scala index 9428c0d758..addb10d690 100644 --- a/test/main/vct/test/integration/examples/TechnicalVeyMontSpec.scala +++ b/test/main/vct/test/integration/examples/TechnicalVeyMontSpec.scala @@ -1,42 +1,56 @@ package vct.test.integration.examples +import hre.io.LiteralReadable +import vct.main.modes.Verify +import vct.options.Options +import vct.options.types.Verbosity import vct.test.integration.helper.VercorsSpec class TechnicalVeyMontSpec extends VercorsSpec { - // TODO: Should eventually become pass - vercors should verify using silicon in "example using communicate" pvl - """ - class Storage { - int x; - } - seq_program Example() { - endpoint alice = Storage(); - endpoint bob = Storage(); - - seq_run { - communicate alice.x <- bob.x; - communicate bob.x -> alice.x; - assert alice.x == bob.x; - } - } - """ - - vercors should fail withCode "assertFailed:false" using silicon in "plain endpoint field dereference should be possible" pvl - """ - class Storage { - int x; - } - seq_program Example() { - endpoint alice = Storage(); - - seq_run { - assert alice.x == 0; - } - } - """ + (vercors + should verify + using silicon + flag "--veymont-generate-permissions" + in "example using communicate" + pvl + """ + class Storage { + int x; + } + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + + seq_run { + communicate alice.x <- bob.x; + communicate bob.x -> alice.x; + assert alice.x == bob.x; + } + } + """) + + (vercors + should fail + withCode "assertFailed:false" + using silicon + flag "--veymont-generate-permissions" + in "plain endpoint field dereference should be possible" + pvl + """ + class Storage { + int x; + } + seq_program Example() { + endpoint alice = Storage(); + + seq_run { + assert alice.x == 0; + } + } + """) vercors should error withCode "noSuchName" in "non-existent thread name in communicate fails" pvl - """ + """ seq_program Example() { seq_run { communicate charlie.x <- charlie.x; @@ -45,7 +59,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should error withCode "noSuchName" in "non-existent field in communicate fails" pvl - """ + """ class Storage { int x; } seq_program Example() { endpoint charlie = Storage(); @@ -56,7 +70,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should error withCode "parseError" in "parameterized sends not yet supported " pvl - """ + """ class Storage { int x; } seq_program Example() { endpoint alice[10] = Storage(); @@ -68,31 +82,36 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should error withCode "noRunMethod" in "run method should always be present" pvl - """ + """ seq_program Example() { } """ vercors should error withCode "parseError" in "endpoints can only have class types" pvl - """ + """ seq_program Example() { endpoint alice = int(); } """ - vercors should verify using silicon in "Endpoint fields should be assignable" pvl - """ - class Storage { int x; int y; } - seq_program Example() { - endpoint alice = Storage(); + (vercors + should verify + using silicon + flag "--veymont-generate-permissions" + in "Endpoint fields should be assignable" + pvl + """ + class Storage { int x; int y; } + seq_program Example() { + endpoint alice = Storage(); - seq_run { - alice.x := alice.y; + seq_run { + alice.x := alice.y; + } } - } - """ + """) vercors should error withCode "resolutionError:seqProgInstanceMethodArgs" in "instance method in seq_program cannot have arguments" pvl - """ + """ seq_program Example() { void m(int x) { } @@ -101,7 +120,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should error withCode "resolutionError:seqProgInstanceMethodBody" in "instance method in seq_program must have a body" pvl - """ + """ seq_program Example() { void m(); @@ -110,7 +129,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should error withCode "resolutionError:seqProgInstanceMethodNonVoid" in "instance method in seq_program must have void return type" pvl - """ + """ seq_program Example() { int m() { } @@ -119,7 +138,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should error withCode "resolutionError:seqProgStatement" in "seq_prog excludes certain statements" pvl - """ + """ class C { } seq_program Example(C c) { seq_run { @@ -129,7 +148,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should error withCode "resolutionError:seqProgReceivingEndpoint" in "Dereferencing anything other than the receiving endpoint in the arguments of a endpoint method invocation is not supported yet" pvl - """ + """ class C { C d; void foo(int x); int x; } seq_program Example(C c) { endpoint c = C(); @@ -141,7 +160,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should error withCode "resolutionError:seqProgInvocation" in "Only method calls on endpoints or seq_program are allowed within seq_program" pvl - """ + """ class C { C d; void foo(); } seq_program Example(C c) { endpoint c = C(); @@ -152,7 +171,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should verify using silicon in "Empty seq_program must verify" pvl - """ + """ seq_program C() { seq_run { @@ -161,7 +180,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should error withCode "resolutionError:type" in "Assign must be well-typed" pvl - """ + """ class C { int x; } seq_program C() { endpoint charlie = C(); @@ -172,7 +191,7 @@ class TechnicalVeyMontSpec extends VercorsSpec { """ vercors should error withCode "resolutionError:type" in "Communicating parties must agree on the type" pvl - """ + """ class C { int c; } class A { bool a; } seq_program C() { @@ -184,64 +203,581 @@ class TechnicalVeyMontSpec extends VercorsSpec { } """ - /* TODO: In the new veymont, this test will probably be replaced by one that manually manages the - permissions for alice.x - */ - vercors should verify using silicon in "assignment should work" pvl - """ - class Storage { - int x; + (vercors + should verify + using silicon + flag "--veymont-generate-permissions" + in "assignment should work" + pvl + """ + class Storage { + int x; + + ensures x == 0; + constructor() { + x = 0; + } + } + seq_program Example() { + endpoint alice = Storage(); + + requires alice.x == 0; + ensures alice.x == 0; + seq_run { + assert alice.x == 0; + } + } + """) + + (vercors + should fail + withCode "postFailed:false" + using silicon + flag "--veymont-generate-permissions" + in "Postcondition of seq_run can fail" + pvl + """ + class Storage { + int x; + } + seq_program Example() { + endpoint alice = Storage(); + + ensures alice.x == 0; + seq_run { + } + } + """) + + (vercors + should fail + withCode "postFailed:false" + using silicon + flag "--veymont-generate-permissions" + in "Postcondition of seq_program can fail" + pvl + """ + class Storage { + int x; + } - ensures Perm(x, 1) ** x == 0; - constructor() { - x = 0; + ensures 1 == 0; + seq_program Example() { + endpoint alice = Storage(); + + seq_run { + } } + """) + + vercors should error withCode "resolutionError:seqProgReceivingEndpoint" in "Assignment statement only allows one endpoint in the assigned expression" pvl + """ + class Storage { + int x; } seq_program Example() { endpoint alice = Storage(); + endpoint bob = Storage(); - requires alice.x == 0; - ensures alice.x == 0; seq_run { - assert alice.x == 0; + alice.x := bob.x; } } """ - // TODO: Eventually should be postconditionFailed if the assignment statement works succesfully - vercors should error withCode "callableFailureNotSupported" in "assigning should change state" pvl + (vercors + should fail + withCode "branchNotUnanimous" + using silicon + flag "--veymont-generate-permissions" + in "Parts of condition in branch have to agree inside seqprog" + pvl + """ + class Storage { + int x; + } + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + + seq_run { + if (alice.x == 0 && bob.x == 0) { + // Alice might go here, bob might not: error + } + } + } + """) + + (vercors + should fail + withCode "branchNotUnanimous" + using silicon + flag "--veymont-generate-permissions" + in "Parts of condition in branch have to agree inside seqprog, including conditions for all endpoints" + pvl + """ + class Storage { + int x; + } + + pure int f() = 3; + + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + + seq_run { + if (alice.x == 0 && f() == 3) { + // Alice might go here, bob will definitely, because of the second expression: error + } + } + } + """) + + (vercors + should verify + using silicon + flag "--veymont-generate-permissions" + in "If there is only one endpoint, the conditions don't have to agree, as there is only one endpoint" + pvl + """ + class Storage { + int x; + } + + pure int f() = 3; + + seq_program Example() { + endpoint alice = Storage(); + + seq_run { + if (alice.x == 0 && f() == 3) { + // Alice might go here, bob will definitely, because of the second expression: error + } + } + } + """) + + vercors should error withCode "seqProgParticipantErrors" in "`if` cannot depend on bob, inside an `if` depending on alice" pvl + """ + class Storage { + int x; + } + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + + seq_run { + if (alice.x == 0) { + if (bob.x == 0) { + // Error + } + } + } + } """ + + vercors should error withCode "seqProgParticipantErrors" in "If alice branches, bob cannot communicate" pvl + """ class Storage { - int x; + int x; + } + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); - ensures Perm(x, write) ** x == v; - constructor(int v) { - x = v; + seq_run { + if (alice.x == 0) { + communicate alice.x <- bob.x; + } } } + """ + + vercors should error withCode "seqProgParticipantErrors" in "If alice branches, bob cannot assign" pvl + """ + class Storage { + int x; + } seq_program Example() { - endpoint alice = Storage(0); + endpoint alice = Storage(); + endpoint bob = Storage(); - requires alice.x == 0; - ensures alice.x == 0; seq_run { - alice.x := 1; + if (alice.x == 0) { + bob.x := 3; + } } } """ - vercors should error withCode "resolutionError:seqProgReceivingEndpoint" in "Assignment statement only allows one endpoint in the assigned expression" pvl + (vercors + should verify + using silicon + flag "--veymont-generate-permissions" + in "Programs where branch conditions agree should verify" + pvl + """ + class Storage { + bool x; + } + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + + seq_run { + alice.x := true; + bob.x := true; + while (alice.x && bob.x) { + bob.x := false; + communicate alice.x <- bob.x; + } + } + } + """) + + (vercors + should fail + withCode "loopUnanimityNotEstablished" + using silicon + flag "--veymont-generate-permissions" + in "Programs where branch condition unanimity cannot be established should fail" + pvl + """ + class Storage { + bool x; + } + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + + seq_run { + while (alice.x && bob.x) { + + } + } + } + """) + + (vercors + should fail + withCode "loopUnanimityNotMaintained" + using silicon + flag "--veymont-generate-permissions" + in "Programs where branch condition unanimity cannot be maintained should fail" + pvl + """ + class Storage { + bool x; + } + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + + seq_run { + alice.x := true; + bob.x := true; + while (alice.x && bob.x) { + alice.x := false; + } + } + } + """) + + vercors should error withCode "seqProgParticipantErrors" in "Loops should also limit the number of participants" pvl + """ + class Storage { + bool x; + } + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + endpoint charlie = Storage(); + + seq_run { + alice.x := true; + bob.x := true; + while (alice.x && bob.x) { + alice.x := false; + charlie.x := true; + } + } + } """ + + (vercors + should verify + using silicon + flag "--veymont-generate-permissions" + in "Loops should also limit the number of participants when combined with branches" + pvl + """ + class Storage { + bool x; + } + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + endpoint charlie = Storage(); + + seq_run { + alice.x := true; + bob.x := true; + while (alice.x && bob.x) { + alice.x := false; + if (bob.x == true) { + bob.x := false; + } + } + } + } + """) + + vercors should error withCode "seqProgParticipantErrors" in "Loops should also limit the number of participants when combined with branches" pvl + """ class Storage { - int x; + bool x; } seq_program Example() { endpoint alice = Storage(); endpoint bob = Storage(); + endpoint charlie = Storage(); seq_run { - alice.x := bob.x; + alice.x := true; + bob.x := true; + while (alice.x && bob.x) { + alice.x := false; + if (bob.x == true) { + bob.x := false; + charlie.x := true; + } + } } } """ + + (vercors should verify + using silicon + flag "--veymont-generate-permissions" + in "Permission should be generated for constructors as well" pvl + """ + class Storage { + int x; + + ensures x == 2; + int m() { + x = 2; + } + } + + seq_program Example() { + endpoint alice = Storage(); + seq_run { + alice.m(); + assert alice.x == 2; + } + } + """) + + (vercors + should fail + withCode "accessPerm" + using silicon + in "When no permission is generated, a failure should occur on endpoint field access" + pvl + """ + class Storage { + int x; + } + + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + seq_run { + communicate alice.x <- bob.x; + } + } + """) + + (vercors + should fail + withCode "seqAssignPerm" + using silicon + in "When no permission is generated, a failure should occur on seq assign field access" + pvl + """ + class Storage { + int x; + } + + seq_program Example() { + endpoint alice = Storage(); + seq_run { + alice.x := 3; + } + } + """) + + (vercors + should verify + using silicon + flag "--veymont-generate-permissions" + in "Permissions are generated for loop invariants, procedures, functions, instance methods, instance functions" + pvl + """ + class Storage { + int x; + + ensures x == \old(x); + ensures \result == x; + int imx() { + return x; + } + + pure int ifx() = x; + + ensures x == \old(x); + void all() { + assert imx() == ifx(); + assert ifx() == px(this); + assert px(this) == fx(this); + } + } + + ensures s.x == \old(s.x); + ensures \result == s.x; + int px(Storage s) { + return s.x; + } + + ensures \result == s.x; + pure int fx(Storage s) = s.x; + + seq_program Example(int N) { + endpoint alice = Storage(); + ensures alice.x == 10; + seq_run { + alice.x := 0; + loop_invariant 0 <= alice.x && alice.x <= 10; + while(alice.x < 10) { + alice.x := alice.x + 1; + } + + alice.all(); + } + } + """) + + (vercors + should verify + using silicon + flag "--veymont-generate-permissions" + in "Permission generation should only generate permissions that are strictly necessary" + pvl + """ + class Storage { + int x; + } + + seq_program Example() { + endpoint alice = Storage(); + endpoint bob = Storage(); + seq_run { + alice.x := 0; + bob.x := 3; + loop_invariant 0 <= alice.x && alice.x <= 10; + while(alice.x < 10) { + alice.x := alice.x + 1; + } + assert bob.x == 3; + } + } + """) + + (vercors + should verify + using silicon + flag "--veymont-generate-permissions" + in "Calling auxiliary methods in seq_prog should be possible" + pvl + """ + class Storage { + int x; + } + + seq_program Example(int N) { + endpoint alice = Storage(); + + ensures alice.x == \old(alice.x) + 1; + void step() { + alice.x := alice.x + 1; + } + + ensures alice.x == \old(alice.x + 1); + seq_run { + step(); + } + } + """) + + (vercors + should verify + using silicon + flag "--veymont-generate-permissions" + in "VeyMont should conservatively generate permissions for auxiliary methods" + pvl + """ + class Storage { + int x; + } + + seq_program Example(int N) { + endpoint alice = Storage(); + endpoint bob = Storage(); + + ensures alice.x == \old(alice.x) + 1; + void step() { + alice.x := alice.x + 1; + } + + ensures alice.x == \old(alice.x + 1); + seq_run { + bob.x := 3; + step(); + assert bob.x == 3; + } + } + """) + + (vercors + should fail + withCode "assertFailed:false" + using silicon + flag "--veymont-generate-permissions" + in "Permissions should be generated when an endpoint participates in an auxiliary method" + pvl + """ + class Storage { + int x; + } + + seq_program Example(int N) { + endpoint alice = Storage(); + endpoint bob = Storage(); + + ensures alice.x == \old(alice.x) + 1; + void step() { + bob.x := 0; + alice.x := alice.x + 1; + } + + ensures alice.x == \old(alice.x + 1); + seq_run { + bob.x := 3; + step(); + assert bob.x == 3; + } + } + """) } diff --git a/test/main/vct/test/integration/helper/VercorsSpec.scala b/test/main/vct/test/integration/helper/VercorsSpec.scala index 8031b5f647..99ff21efdd 100644 --- a/test/main/vct/test/integration/helper/VercorsSpec.scala +++ b/test/main/vct/test/integration/helper/VercorsSpec.scala @@ -8,11 +8,12 @@ import org.scalatest.concurrent.TimeLimits.failAfter import org.scalatest.flatspec.AnyFlatSpec import org.scalatest.time._ import org.slf4j.LoggerFactory +import scopt.OParser import vct.col.origin.{BlameUnreachable, VerificationFailure} import vct.col.rewrite.bip.BIP.Standalone.VerificationReport import vct.main.Main.TemporarilyUnsupported import vct.main.modes.Verify -import vct.options.types +import vct.options.{Options, types} import vct.options.types.{Backend, PathOrStd} import vct.parsers.ParseError import vct.result.VerificationError @@ -71,7 +72,7 @@ abstract class VercorsSpec extends AnyFlatSpec { } } - private def registerTest(verdict: Verdict, desc: String, tags: Seq[Tag], backend: Backend, inputs: Seq[Readable])(implicit pos: source.Position): Unit = { + private def registerTest(verdict: Verdict, desc: String, tags: Seq[Tag], backend: Backend, inputs: Seq[Readable], flags: Seq[String])(implicit pos: source.Position): Unit = { val fullDesc: String = s"${desc.capitalize} produces verdict $verdict with $backend".replaceAll("should", "shld") // PB: note that object typically do not have a deterministic hashCode, but Strings do. val matrixId = Math.floorMod(fullDesc.hashCode, MATRIX_COUNT) @@ -83,8 +84,16 @@ abstract class VercorsSpec extends AnyFlatSpec { failAfter(Span(300, Seconds)) { matchVerdict(verdict, backend match { - case types.Backend.Silicon => Verify.verifyWithSilicon(inputs) + case types.Backend.Silicon => + Verify.verifyWithOptions( + Options.parse((Seq("--backend", "silicon") ++ flags).toArray).get, + inputs + ) case types.Backend.Carbon => Verify.verifyWithCarbon(inputs) + Verify.verifyWithOptions( + Options.parse((Seq("--backend", "carbon") ++ flags).toArray).get, + inputs + ) }) } } @@ -133,7 +142,7 @@ abstract class VercorsSpec extends AnyFlatSpec { println(err) fail(s"Expected the test to fail with code $code, but it crashed with the above error instead.") case Right((Nil, _)) => - fail("Expected the test to fail with code $code, but it passed instead.") + fail(s"Expected the test to fail with code $code, but it passed instead.") case Right((fails, _)) => fails.filterNot(_.code == code) match { case Nil => // success case fails => @@ -167,14 +176,14 @@ abstract class VercorsSpec extends AnyFlatSpec { } class ErrorVerdictPhrase() { - def withCode(code: String): BackendPhrase = new BackendPhrase(Error(code), None, silicon) + def withCode(code: String): BackendPhrase = new BackendPhrase(Error(code), None, silicon, Nil) } class VerdictPhrase(val verdict: Verdict, val reportPath: Option[Path]) { - def using(backend: Seq[Backend]): BackendPhrase = new BackendPhrase(verdict, reportPath, backend) + def using(backend: Seq[Backend]): BackendPhrase = new BackendPhrase(verdict, reportPath, backend, Nil) } - class BackendPhrase(val verdict: Verdict, val reportPath: Option[Path], val backends: Seq[Backend]) { + class BackendPhrase(val verdict: Verdict, val reportPath: Option[Path], val backends: Seq[Backend], val _flags: Seq[String]) { def example(path: String)(implicit pos: source.Position): Unit = examples(path) def examples(examples: String*)(implicit pos: source.Position): Unit = { @@ -183,32 +192,35 @@ abstract class VercorsSpec extends AnyFlatSpec { val inputs = paths.map(PathOrStd.Path) for(backend <- backends) { - registerTest(verdict, s"Examples ${paths.mkString(", ")}", Seq(new Tag("exampleCase")), backend, inputs) + registerTest(verdict, s"Examples ${paths.mkString(", ")}", Seq(new Tag("exampleCase")), backend, inputs, _flags) } } - def in(desc: String): DescPhrase = new DescPhrase(verdict, backends, desc) + 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)) } - class DescPhrase(val verdict: Verdict, val backends: Seq[Backend], val desc: String) { + class DescPhrase(val verdict: Verdict, val backends: Seq[Backend], val desc: String, val flags: Seq[String]) { def pvl(data: String)(implicit pos: source.Position): Unit = { val inputs = Seq(LiteralReadable("test.pvl", data)) for(backend <- backends) { - registerTest(verdict, desc, Seq(new Tag("literalCase")), backend, inputs) + registerTest(verdict, desc, Seq(new Tag("literalCase")), backend, inputs, flags) } } def java(data: String)(implicit pos: source.Position): Unit = { val inputs = Seq(LiteralReadable("test.java", data)) for(backend <- backends) { - registerTest(verdict, desc, Seq(new Tag("literalCase")), backend, inputs) + registerTest(verdict, desc, Seq(new Tag("literalCase")), backend, inputs, flags) } } def c(data: String)(implicit pos: source.Position): Unit = { val inputs = Seq(LiteralReadable("test.c", data)) for(backend <- backends) { - registerTest(verdict, desc, Seq(new Tag("literalCase")), backend, inputs) + registerTest(verdict, desc, Seq(new Tag("literalCase")), backend, inputs, flags) } } }