diff --git a/src/col/vct/col/origin/Blame.scala b/src/col/vct/col/origin/Blame.scala index 85c9cc182..0c6615cf7 100644 --- a/src/col/vct/col/origin/Blame.scala +++ b/src/col/vct/col/origin/Blame.scala @@ -590,17 +590,6 @@ case class ChannelInvariantNotEstablished( s"The channel invariant at `$node` cannot be established, since $failure" } -case class ChannelInvariantNotEstablishedLocally( - failure: ContractFailure, - node: Communicate[_], -) extends CommunicateFailure with WithContractFailure { - override def baseCode: String = "channelInvariantNotEstablishedLocally" - override def descInContext: String = - "This channel invariant cannot be estalished when `\\chor` expressions are removed, since" - override def inlineDescWithSource(node: String, failure: String): String = - s"The channel invariant at `$node` cannot be established without `\\chor`, since $failure" -} - sealed trait DerefInsufficientPermission extends FrontendDerefError case class InsufficientPermission(node: HeapDeref[_]) extends DerefInsufficientPermission with NodeVerificationFailure { diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index 888e6a470..8de7a33d8 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -2123,8 +2123,8 @@ abstract class CoercingRewriter[Pre <: Generation]() case Receiver(_) => e case Message(_) => e case PVLEndpointExpr(endpoint, expr) => e - case EndpointExpr(ref, expr) => e - case ChorExpr(expr) => e + case EndpointExpr(ref, expr) => EndpointExpr(ref, res(expr)) + case ChorExpr(expr) => ChorExpr(bool(expr)) } } diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodeChannels.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodeChannels.scala index 10a1f480e..ac704fc40 100644 --- a/src/rewrite/vct/rewrite/veymont/verification/EncodeChannels.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/EncodeChannels.scala @@ -9,10 +9,7 @@ import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.col.util.AstBuildHelpers._ import vct.col.util.SuccessionMap import vct.rewrite.veymont.VeymontContext -import vct.rewrite.veymont.verification.EncodeChannels.{ - AssertFailedToChannelInvariantNotEstablished, - ExhaleFailedToChannelInvariantNotEstablished, -} +import vct.rewrite.veymont.verification.EncodeChannels.ExhaleFailedToChannelInvariantNotEstablished object EncodeChannels extends RewriterBuilder { override def key: String = "encodeChannels" @@ -20,24 +17,16 @@ object EncodeChannels extends RewriterBuilder { override def desc: String = "Encodes channels using plain assignment. Encodes channel invariants using exhale/inhale." - case class AssertFailedToChannelInvariantNotEstablished(comm: Communicate[_]) - extends Blame[AssertFailed] { - override def blame(error: AssertFailed): Unit = - comm.blame.blame(ChannelInvariantNotEstablished(error.failure, comm)) - } - case class ExhaleFailedToChannelInvariantNotEstablished(comm: Communicate[_]) extends Blame[ExhaleFailed] { override def blame(error: ExhaleFailed): Unit = - comm.blame - .blame(ChannelInvariantNotEstablishedLocally(error.failure, comm)) + comm.blame.blame(ChannelInvariantNotEstablished(error.failure, comm)) } } case class EncodeChannels[Pre <: Generation]() extends Rewriter[Pre] with LazyLogging with VeymontContext[Pre] { val msgSucc = SuccessionMap[Communicate[Pre], Variable[Post]]() - val includeChorExpr = ScopedStack[Boolean]() val substitutions = ScopedStack[Map[Expr[Pre], Expr[Post]]]() override def dispatch(p: Program[Pre]): Program[Post] = { @@ -61,6 +50,14 @@ case class EncodeChannels[Pre <: Generation]() val m = new Variable(dispatch(comm.msg.t))(comm.o.where(name = "m")) msgSucc(comm) = m + // Helper for rewriting the invariant. Regular expressions we wrap in the EndpointExpr of the sender/receiver + // ChorExpr's we leave untouched. Those will be encoded by the EncodeStratifiedPermissions pass. + def wrapEndpointExpr(expr: Expr[Pre], ep: Endpoint[Pre]): Expr[Post] = + foldAny(comm.invariant.t)(unfoldStar(comm.invariant).map { + case e: ChorExpr[Pre] => dispatch(e) + case e => EndpointExpr(succ(ep), dispatch(e)) + }) + Scope( Seq(m), Block(Seq( @@ -68,17 +65,8 @@ case class EncodeChannels[Pre <: Generation]() m.get, EndpointExpr[Post](succ(sender), dispatch(comm.msg)), ), - Assert(currentEndpoint.having(comm.sender.get.decl) { - includeChorExpr.having(true) { - EndpointExpr[Post](succ(sender), dispatch(comm.invariant)) - } - })(AssertFailedToChannelInvariantNotEstablished(comm)), Exhale(currentEndpoint.having(comm.sender.get.decl) { - includeChorExpr.having(false) { - foldAny(comm.invariant.t)(unfoldStar(comm.invariant).map { e => - EndpointExpr[Post](succ(sender), dispatch(e)) - }) - } + wrapEndpointExpr(comm.invariant, sender) })(ExhaleFailedToChannelInvariantNotEstablished(comm)), EndpointStatement[Post]( Some(succ(receiver)), @@ -89,14 +77,7 @@ case class EncodeChannels[Pre <: Generation]() Inhale(currentEndpoint.having(comm.receiver.get.decl) { substitutions.having(Map.from(Seq( (Message(new DirectRef(comm)), dispatch(comm.target)) - ))) { - includeChorExpr.having(true) { - foldAny(comm.invariant.t)(unfoldStar(comm.invariant).map { - case e: ChorExpr[Pre] => e.rewriteDefault() - case e => EndpointExpr[Post](succ(receiver), dispatch(e)) - }) - } - } + ))) { wrapEndpointExpr(comm.invariant, receiver) } }), )), ) @@ -109,25 +90,14 @@ case class EncodeChannels[Pre <: Generation]() substitutions.top(e) case InEndpoint(_, endpoint, Perm(loc, perm)) => ChorPerm[Post](succ(endpoint), dispatch(loc), dispatch(perm))(expr.o) - case InEndpoint(_, endpoint, cp: ChorPerm[Pre]) => assert(false); ??? + case InEndpoint(_, _, _: ChorPerm[Pre]) => + assert(false); + ??? // TODO (RR): This is an error, remove when getting rid of ChorPerm as well case Message(Ref(comm)) => Local[Post](msgSucc.ref(comm))(comm.o) case Sender(Ref(comm)) => EndpointName[Post](succ(comm.sender.get.decl))(expr.o) case Receiver(Ref(comm)) => EndpointName[Post](succ(comm.receiver.get.decl))(expr.o) - case chor: ChorExpr[Pre] if includeChorExpr.topOption.contains(true) => - // Case chor must be kept: include the expression. The top level invariant rewrite will wrap - // it into a proper EndpointExpr, hence, remove the \chor layer - chor.expr.rewriteDefault() - case chor: ChorExpr[Pre] if includeChorExpr.topOption.contains(false) => - // Case chor must not be kept: exhaling the invariant. Since the validity of the invariant, including - // the chor part, is already established, it doesn't need to be included when exhaling - BooleanValue(true)(chor.o) - case chor: ChorExpr[Pre] => - // Case no boolean in includeChor: just rewrite the expression plainly and keep the chor expr - // This also happens to be the case we need for the inhale case, where we just want the plain \chor expr - // Such that all the necessary wrapped perms will be unwrapped by the EncodePermissionStratification phase - chor.rewriteDefault() case _ => expr.rewriteDefault() } } diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala index 49d7ce3a7..014badc3d 100644 --- a/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala @@ -50,18 +50,6 @@ object EncodePermissionStratification extends RewriterBuilderArg[Boolean] { } } -/* At the time of writing, under the heavy-weight stratified permissions model, supporting \chor is an enormous hack. - It currently consists of 3 parts: - - Making \chor work when generating permissions in plain asserts, loop invariants, contracts - This is done using the simplifying assumption that, when generating permissions, each field is completely and transitively - owned by the anchor (either a local or a method argument). Then chor just transitively unfolds all fields of all anchors - in scope. Inside this unfolded expression, plain functions (meaning, with non-specialized contracts), are used. - - Making \chor work when not generating permissions in plain asserts, ... - Here, we rely on the user to add (\endpoint e; ...) annotations inside \chor. - - Making \chor work in channel invariants - This is also quite annoying. Because the heavyweight approach does not allow easy peeking into wrapped permissions, - we implement an incomplete approach in EncodeChannels.scala. - */ case class EncodePermissionStratification[Pre <: Generation]( generatePermissions: Boolean ) extends Rewriter[Pre] with VeymontContext[Pre] with LazyLogging { @@ -370,7 +358,7 @@ case class EncodePermissionStratification[Pre <: Generation]( } } - case InEndpoint(_, endpoint, deref @ Deref(obj, Ref(field))) => + case InEndpoint(_, _, deref @ Deref(obj, Ref(field))) => implicit val o = expr.o functionInvocation( ref = readFunction(obj, field)(expr.o), @@ -378,72 +366,14 @@ case class EncodePermissionStratification[Pre <: Generation]( blame = ForwardInvocationFailureToDeref(deref), ) - case ChorExpr(inner) if generatePermissions => - implicit val o = expr.o - - def predicates( - seenClasses: Set[TClass[Pre]], - endpoint: Endpoint[Pre], - baseT: TClass[Pre], - base: Expr[Post], - ): Seq[FoldTarget[Post]] = { - val cls = baseT.cls.decl - // Permission generation makes sure no cycles exist at this point by crashing, but lets make sure anyway - assert(!seenClasses.contains(baseT)) - val newSeenClasses = seenClasses.incl(baseT) - val predicatesForClass = cls.fields.map { field => - ScaledPredicateApply( - PredicateApply[Post]( - wrapperPredicate(baseT, field), - Seq(EndpointName(succ(endpoint)), base), - ), - WritePerm(), - ) - } - predicatesForClass ++ - (cls.fields.filter { _.t.asClass.nonEmpty }.flatMap { field => - val newBase = - Deref[Post](base, succ(field))(PanicBlame( - "Permissions were unfolded earlier" - )) - predicates( - newSeenClasses, - endpoint, - baseT.instantiate(field.t).asClass.get, - newBase, - ) - }) - } - - val newInner = inChor.having(true) { dispatch(inner) } - - InferEndpointContexts.getEndpoints(inner).flatMap { endpoint => - predicates( - HashSet(), - endpoint, - endpoint.t, - EndpointName[Post](succ(endpoint)), - ) - }.foldRight[Expr[Post]](newInner) { case (app, inner) => - Unfolding[Post](app, inner)(PanicBlame( - "Generating permissions guarantee permissions are in scope" - )) - } - - case ChorExpr(inner) if !generatePermissions => - // If not generating permissions, we rely on endpoint expressions to indicate the owner - // of relevant permissions - inChor.having(true) { dispatch(inner) } + case ChorExpr(inner) => inChor.having(true) { dispatch(inner) } // Generate an invocation to the unspecialized function version if we're inside a \chor - // This is safe because \chor unfold all predicates of all endpoints that occur within the expression... - // ... in the case of permission generation. Otherwise it just does nothing...? // The natural successor of the function will be the unspecialized one - case inv: FunctionInvocation[Pre] - if inChor.topOption.contains(true) && generatePermissions => + case inv: FunctionInvocation[Pre] if inChor.topOption.contains(true) => inv.rewriteDefault() case inv: InstanceFunctionInvocation[Pre] - if inChor.topOption.contains(true) && generatePermissions => + if inChor.topOption.contains(true) => inv.rewriteDefault() case InEndpoint(_, endpoint, inv: FunctionInvocation[Pre]) =>