diff --git a/.gitignore b/.gitignore index 03050c5e2..12e089ecf 100644 --- a/.gitignore +++ b/.gitignore @@ -61,4 +61,5 @@ __pycache__ # Misc *.pprof -*.vpr \ No newline at end of file +*.vpr +test.pvl diff --git a/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/2-TTTlast.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/2-TTTlast.pvl index 1d970580e..8733acd40 100644 --- a/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/2-TTTlast.pvl +++ b/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/2-TTTlast.pvl @@ -61,6 +61,8 @@ choreography Main() { (!\sender.gameFinished() ==> ([1\2]\sender.returnerMark())); communicate p2.move <- p1.move.copy(); p2.doMove(); + assert (\endpoint p2; p2.equalBoard(p1)); + assert (\endpoint p2; !p1.gameFinished() == !p2.gameFinished()); } else { p2.createNewMove(); p2.doMove(); @@ -76,13 +78,15 @@ choreography Main() { (!\sender.gameFinished() ==> ([1\2]\sender.returnerMark())); communicate p1.move <- p2.move.copy(); p1.doMove(); + assert (\endpoint p1; p1.equalBoard(p2)); + assert (\endpoint p1; !p1.gameFinished() == !p2.gameFinished()); } p1.turn := !p1.turn; p2.turn := !p2.turn; // Assumption required for shortcoming in backend. Can be removed after implementing the lightweight encoding. - assume (\chor p1.gameFinished() == p2.gameFinished()); + // assume (\chor p1.gameFinished() == p2.gameFinished()); } - assume (\chor p1.gameFinished() == p2.gameFinished()); + // assume (\chor p1.gameFinished() == p2.gameFinished()); p1.finish(); p2.finish(); diff --git a/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/Player.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/Player.pvl index b7be576e8..b2618b8ee 100644 --- a/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/Player.pvl +++ b/examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/Player.pvl @@ -9,8 +9,9 @@ class Player { Move move; boolean turn; Returner returner; - - inline resource boardPerm() = + + // TODO (RR): Remove comment if it works + /* inline */ resource boardPerm() = Perm(c00, 1) ** Perm(c01, 1) ** Perm(c02, 1) ** Perm(c10, 1) ** Perm(c11, 1) ** Perm(c12, 1) ** Perm(c20, 1) ** Perm(c21, 1) ** Perm(c22, 1); @@ -27,10 +28,11 @@ class Player { ; requires [1\2]boardPerm(); - pure boolean emptyBoard() = - c00 == -1 && c01 == -1 && c02 == -1 && - c10 == -1 && c11 == -1 && c12 == -1 && - c20 == -1 && c21 == -1 && c22 == -1; + pure boolean emptyBoard() = + (\unfolding [1\2]boardPerm() \in + c00 == -1 && c01 == -1 && c02 == -1 && + c10 == -1 && c11 == -1 && c12 == -1 && + c20 == -1 && c21 == -1 && c22 == -1); requires tok == 0 || tok == 1; ensures boardPerm(); @@ -55,6 +57,7 @@ class Player { myMark = tok; turn = t; move = new Move(0, 0, 0); + fold boardPerm(); } requires tok == 0 || tok == 1; @@ -88,38 +91,41 @@ class Player { fold returnerBound(other); fold returnerMark(); + fold boardPerm(); } requires ([1\100]boardPerm()) ** ([1\100]other.boardPerm()); requires Perm(move.i, read) ** Perm(move.j, read) ** Perm(move.mark, read); requires 0 <= move.i && move.i <= 2; requires 0 <= move.j && move.j <= 2; - pure boolean oneMoveAheadOf(Move move, Player other) = - readMoveCell(move,this) == move.mark && readMoveCell(move,other) == -1 - && (move.i != 0 || move.j != 0 ==> other.c00 == c00) - && (move.i != 0 || move.j != 1 ==> other.c01 == c01) - && (move.i != 0 || move.j != 2 ==> other.c02 == c02) - && (move.i != 1 || move.j != 0 ==> other.c10 == c10) - && (move.i != 1 || move.j != 1 ==> other.c11 == c11) - && (move.i != 1 || move.j != 2 ==> other.c12 == c12) - && (move.i != 2 || move.j != 0 ==> other.c20 == c20) - && (move.i != 2 || move.j != 1 ==> other.c21 == c21) - && (move.i != 2 || move.j != 2 ==> other.c22 == c22); + pure boolean oneMoveAheadOf(Move move, Player other) = + readMoveCell(move,this) == move.mark && readMoveCell(move,other) == -1 && + (\unfolding [1\100]boardPerm() \in (\unfolding [1\100]other.boardPerm() \in + (move.i != 0 || move.j != 0 ==> other.c00 == c00) + && (move.i != 0 || move.j != 1 ==> other.c01 == c01) + && (move.i != 0 || move.j != 2 ==> other.c02 == c02) + && (move.i != 1 || move.j != 0 ==> other.c10 == c10) + && (move.i != 1 || move.j != 1 ==> other.c11 == c11) + && (move.i != 1 || move.j != 2 ==> other.c12 == c12) + && (move.i != 2 || move.j != 0 ==> other.c20 == c20) + && (move.i != 2 || move.j != 1 ==> other.c21 == c21) + && (move.i != 2 || move.j != 2 ==> other.c22 == c22))); context boardPerm(); context Perm(move,1\2) ** ([1\2]move.state()); requires readMoveCell(move,this) == -1; ensures readMoveCell(move,this) == move.mark; - ensures move.i != 0 || move.j != 0 ==> \old(c00) == c00; - ensures move.i != 0 || move.j != 1 ==> \old(c01) == c01; - ensures move.i != 0 || move.j != 2 ==> \old(c02) == c02; - ensures move.i != 1 || move.j != 0 ==> \old(c10) == c10; - ensures move.i != 1 || move.j != 1 ==> \old(c11) == c11; - ensures move.i != 1 || move.j != 2 ==> \old(c12) == c12; - ensures move.i != 2 || move.j != 0 ==> \old(c20) == c20; - ensures move.i != 2 || move.j != 1 ==> \old(c21) == c21; - ensures move.i != 2 || move.j != 2 ==> \old(c22) == c22; + ensures move.i != 0 || move.j != 0 ==> \old((\unfolding boardPerm() \in c00)) == (\unfolding boardPerm() \in c00); + ensures move.i != 0 || move.j != 1 ==> \old((\unfolding boardPerm() \in c01)) == (\unfolding boardPerm() \in c01); + ensures move.i != 0 || move.j != 2 ==> \old((\unfolding boardPerm() \in c02)) == (\unfolding boardPerm() \in c02); + ensures move.i != 1 || move.j != 0 ==> \old((\unfolding boardPerm() \in c10)) == (\unfolding boardPerm() \in c10); + ensures move.i != 1 || move.j != 1 ==> \old((\unfolding boardPerm() \in c11)) == (\unfolding boardPerm() \in c11); + ensures move.i != 1 || move.j != 2 ==> \old((\unfolding boardPerm() \in c12)) == (\unfolding boardPerm() \in c12); + ensures move.i != 2 || move.j != 0 ==> \old((\unfolding boardPerm() \in c20)) == (\unfolding boardPerm() \in c20); + ensures move.i != 2 || move.j != 1 ==> \old((\unfolding boardPerm() \in c21)) == (\unfolding boardPerm() \in c21); + ensures move.i != 2 || move.j != 2 ==> \old((\unfolding boardPerm() \in c22)) == (\unfolding boardPerm() \in c22); void doMove() { + unfold boardPerm(); if(move.i == 0 && move.j == 0) { c00 = move.mark; } else if(move.i == 0 && move.j == 1) { @@ -139,24 +145,27 @@ class Player { } else if(move.i == 2 && move.j == 2) { c22 = move.mark; } + fold boardPerm(); } requires [1\100]boardPerm(); pure boolean boardFull() = - c00 != -1 && c01 != -1 && c02 != -1 && - c10 != -1 && c11 != -1 && c12 != -1 && - c20 != -1 && c21 != -1 && c22 != -1; + (\unfolding [1\100]boardPerm() \in + c00 != -1 && c01 != -1 && c02 != -1 && + c10 != -1 && c11 != -1 && c12 != -1 && + c20 != -1 && c21 != -1 && c22 != -1); requires [1\100]boardPerm(); pure boolean boardWin() = - c00 != -1 && c00 == c01 && c01 == c02 || - c10 != -1 && c10 == c11 && c11 == c12 || - c20 != -1 && c20 == c21 && c21 == c22 || - c00 != -1 && c00 == c10 && c10 == c20 || - c01 != -1 && c01 == c11 && c11 == c21 || - c02 != -1 && c02 == c12 && c12 == c22 || - c00 != -1 && c00 == c11 && c11 == c22 || - c02 != -1 && c02 == c11 && c11 == c20; + (\unfolding [1\100]boardPerm() \in + c00 != -1 && c00 == c01 && c01 == c02 || + c10 != -1 && c10 == c11 && c11 == c12 || + c20 != -1 && c20 == c21 && c21 == c22 || + c00 != -1 && c00 == c10 && c10 == c20 || + c01 != -1 && c01 == c11 && c11 == c21 || + c02 != -1 && c02 == c12 && c12 == c22 || + c00 != -1 && c00 == c11 && c11 == c22 || + c02 != -1 && c02 == c11 && c11 == c20); requires [1\100]boardPerm(); pure boolean gameFinished() = boardFull() || boardWin(); @@ -164,22 +173,24 @@ class Player { requires [1\100]boardPerm(); requires [1\100]other.boardPerm(); pure boolean equalBoard(Player other) = - c00 == other.c00 && c01 == other.c01 && c02 == other.c02 && - c10 == other.c10 && c11 == other.c11 && c12 == other.c12 && - c20 == other.c20 && c21 == other.c21 && c22 == other.c22; + (\unfolding [1\100]boardPerm() \in (\unfolding [1\100]other.boardPerm() \in + c00 == other.c00 && c01 == other.c01 && c02 == other.c02 && + c10 == other.c10 && c11 == other.c11 && c12 == other.c12 && + c20 == other.c20 && c21 == other.c21 && c22 == other.c22)); requires [1\100]boardPerm(); - pure int boardCount() = 0 - + (c00 != -1 ? 1 : 0) - + (c01 != -1 ? 1 : 0) - + (c02 != -1 ? 1 : 0) - + (c10 != -1 ? 1 : 0) - + (c11 != -1 ? 1 : 0) - + (c12 != -1 ? 1 : 0) - + (c20 != -1 ? 1 : 0) - + (c21 != -1 ? 1 : 0) - + (c22 != -1 ? 1 : 0) - ; + pure int boardCount() = + (\unfolding [1\100]boardPerm() \in + 0 + (c00 != -1 ? 1 : 0) + + (c01 != -1 ? 1 : 0) + + (c02 != -1 ? 1 : 0) + + (c10 != -1 ? 1 : 0) + + (c11 != -1 ? 1 : 0) + + (c12 != -1 ? 1 : 0) + + (c20 != -1 ? 1 : 0) + + (c21 != -1 ? 1 : 0) + + (c22 != -1 ? 1 : 0) + ); context Perm(move,1) ** Perm(myMark, 1\2); context [1\100]boardPerm(); @@ -199,12 +210,13 @@ requires 0 <= move.i && move.i <= 2; requires 0 <= move.j && move.j <= 2; requires [1\100]p.boardPerm(); pure int readMoveCell(Move move, Player p) = - (move.i == 0 && move.j == 0) ? p.c00 - : (move.i == 0 && move.j == 1) ? p.c01 - : (move.i == 0 && move.j == 2) ? p.c02 - : (move.i == 1 && move.j == 0) ? p.c10 - : (move.i == 1 && move.j == 1) ? p.c11 - : (move.i == 1 && move.j == 2) ? p.c12 - : (move.i == 2 && move.j == 0) ? p.c20 - : (move.i == 2 && move.j == 1) ? p.c21 - : p.c22; + (\unfolding [1\100]p.boardPerm() \in + ((move.i == 0 && move.j == 0) ? p.c00 + : (move.i == 0 && move.j == 1) ? p.c01 + : (move.i == 0 && move.j == 2) ? p.c02 + : (move.i == 1 && move.j == 0) ? p.c10 + : (move.i == 1 && move.j == 1) ? p.c11 + : (move.i == 1 && move.j == 2) ? p.c12 + : (move.i == 2 && move.j == 0) ? p.c20 + : (move.i == 2 && move.j == 1) ? p.c21 + : p.c22)); diff --git a/src/main/vct/main/modes/VeyMont.scala b/src/main/vct/main/modes/VeyMont.scala index ca77c7490..f285a516c 100644 --- a/src/main/vct/main/modes/VeyMont.scala +++ b/src/main/vct/main/modes/VeyMont.scala @@ -48,10 +48,14 @@ object VeyMont extends LazyLogging { ) extends UserError { override def code: String = s"$codePrefix:${error.code}" override def text: String = s"$textPrefix\n${error.text}" + + initCause(error) } case class WrapSystemError(textPrefix: String, error: SystemError) extends SystemError { override def text: String = s"$textPrefix\n${error.text}" + + initCause(error) } def choreographyWithOptions( diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala index 88d60f97d..00bf9b5ee 100644 --- a/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala @@ -57,11 +57,11 @@ case class EncodePermissionStratification[Pre <: Generation]( val inChor = ScopedStack[Boolean]() lazy val specializedApplicables - : mut.LinkedHashMap[ContractApplicable[Pre], Seq[Endpoint[Pre]]] = - findInContext { - case inv: AnyFunctionInvocation[Pre] => inv.ref.decl - case inv: MethodInvocation[Pre] => inv.ref.decl - } + : mut.LinkedHashMap[Applicable[Pre], Seq[Endpoint[Pre]]] = findInContext { + case inv: AnyFunctionInvocation[Pre] => inv.ref.decl + case inv: MethodInvocation[Pre] => inv.ref.decl + case app: ApplyAnyPredicate[Pre] => app.ref.decl + } // Given a function f that finds Nodes inside nodes, findInContext keeps applying f // to nodes that f itself finds, until no more new nodes are found. The search is started @@ -106,9 +106,7 @@ case class EncodePermissionStratification[Pre <: Generation]( } val specializedApplicableSucc = - SuccessionMap[(Endpoint[Pre], ContractApplicable[Pre]), ContractApplicable[ - Post - ]]() + SuccessionMap[(Endpoint[Pre], Applicable[Pre]), Applicable[Post]]() // Keeps track of the current anchoring/endpoint context identity expression for the current endpoint context. // E.g. within a choreograph, it is EndpointName(succ(endpoint)), within a specialized function it is a local @@ -119,11 +117,14 @@ case class EncodePermissionStratification[Pre <: Generation]( // this endpoint reference comes from one of the arguments of the function, not a literal endpointname expression. val specializing = ScopedStack[Expr[Post]]() + // TODO (RR): I think this key can be simplified - InstanceField always belongs to a particular class, + // so the Type could theoretically be omitted? type WrapperPredicateKey = (Type[Pre], InstanceField[Pre]) val wrapperPredicates = mut .LinkedHashMap[WrapperPredicateKey, Predicate[Post]]() // TODO (RR): It does not really wrap anymore, rename + // marker predicate to allow marking field permissions with an endpoint owner def wrapperPredicate(objT: Type[Pre], field: InstanceField[Pre])( implicit o: Origin ): Ref[Post, Predicate[Post]] = { @@ -220,21 +221,24 @@ case class EncodePermissionStratification[Pre <: Generation]( case m: InstanceMethod[Pre] if specializedApplicables.contains(m) => m.rewriteDefault().succeed(m) specializeApplicable(m) + case p: Predicate[Pre] if specializedApplicables.contains(p) => + p.rewriteDefault().succeed(p) + specializeApplicable(p) + case p: InstancePredicate[Pre] if specializedApplicables.contains(p) => + p.rewriteDefault().succeed(p) + specializeApplicable(p) case _ => super.dispatch(decl) } - def specializeApplicable(app: ContractApplicable[Pre]): Unit = { + def specializeApplicable(app: Applicable[Pre]): Unit = { assert(app match { - case _: InstanceMethod[Pre] | - _: InstanceFunction[Pre] | _: Function[Pre] => + case _: InstanceMethod[Pre] | _: InstanceFunction[Pre] | + _: Function[Pre] | _: Predicate[Pre] | _: InstancePredicate[Pre] => true case _ => false }) - def nameOrigin( - endpoint: Endpoint[Pre], - f: ContractApplicable[Pre], - ): Origin = { + def nameOrigin(endpoint: Endpoint[Pre], f: Applicable[Pre]): Origin = { f.o.where(indirect = Name.names( f.o.getPreferredNameOrElse(), @@ -256,7 +260,7 @@ case class EncodePermissionStratification[Pre <: Generation]( // Make sure plain perms are rewritten into wrapped perms specializing.having(endpointCtxVar.get(app.o)) { - val newF: ContractApplicable[Post] = + val newF: Applicable[Post] = app match { case f: InstanceFunction[Pre] => val newF = f.rewrite( @@ -283,6 +287,18 @@ case class EncodePermissionStratification[Pre <: Generation]( o = nameOrigin(endpoint, m), ) newM.declare() + case p: InstancePredicate[Pre] => + val newP = p.rewrite( + args = endpointCtxVar +: variables.dispatch(p.args), + o = nameOrigin(endpoint, p), + ) + newP.declare() + case p: Predicate[Pre] => + val newP = p.rewrite( + args = endpointCtxVar +: variables.dispatch(p.args), + o = nameOrigin(endpoint, p), + ) + newP.declare() } specializedApplicableSucc((endpoint, app)) = newF } @@ -340,6 +356,10 @@ case class EncodePermissionStratification[Pre <: Generation]( expr.o ) + case InEndpoint(_, _, cp: ChorPerm[Pre]) => + // Matching on cp above already put the required specializing in place, so we can ignore it here + Perm(dispatch(cp.loc), dispatch(cp.perm))(cp.o) + case InEndpoint(_, endpoint, Perm(loc: FieldLocation[Pre], perm)) => makeWrappedPerm(loc, perm, specializing.top)(expr.o) @@ -390,10 +410,32 @@ case class EncodePermissionStratification[Pre <: Generation]( ref = specializedApplicableSucc.ref(k), args = specializing.top +: inv.args.map(dispatch), ) - case _ => expr.rewriteDefault() } + override def dispatch(app: ApplyAnyPredicate[Pre]): ApplyAnyPredicate[Post] = + app match { + case InEndpoint(_, endpoint, app: PredicateApply[Pre]) => + val k = (endpoint, app.ref.decl) + app.rewrite( + ref = specializedApplicableSucc.ref(k), + args = specializing.top +: app.args.map(dispatch), + ) + case InEndpoint(_, endpoint, app: InstancePredicateApply[Pre]) => + val k = (endpoint, app.ref.decl) + app.rewrite( + ref = specializedApplicableSucc.ref(k), + args = specializing.top +: app.args.map(dispatch), + ) + case InEndpoint(_, endpoint, app: CoalesceInstancePredicateApply[Pre]) => + val k = (endpoint, app.ref.decl) + app.rewrite( + ref = specializedApplicableSucc.ref(k), + args = specializing.top +: app.args.map(dispatch), + ) + case _ => app.rewriteDefault() + } + override def dispatch(statement: Statement[Pre]): Statement[Post] = statement match { case EndpointStatement(None, Assign(_, _)) =>